Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison ordinal-definable.agda @ 42:4d5fc6381546
regurality
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 24 May 2019 10:28:02 +0900 |
parents | b60db5903f01 |
children | 0d9b9db14361 |
comparison
equal
deleted
inserted
replaced
41:b60db5903f01 | 42:4d5fc6381546 |
---|---|
92 | 92 |
93 record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where | 93 record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where |
94 field | 94 field |
95 mino : Ordinal {n} | 95 mino : Ordinal {n} |
96 min<x : mino o< x | 96 min<x : mino o< x |
97 defmin : def ( ord→od x ) mino | |
98 defmin = lemma ( o<→c< min<x ) where | |
99 lemma : def (ord→od x) (od→ord ( ord→od mino)) → def ( ord→od x ) mino | |
100 lemma m< = def-subst {n} {ord→od x} m< refl diso | |
101 | 97 |
102 ominimal : {n : Level} → (x : Ordinal {n} ) → o∅ o< x → Minimumo {n} x | 98 ominimal : {n : Level} → (x : Ordinal {n} ) → o∅ o< x → Minimumo {n} x |
103 ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case1 ()) | 99 ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case1 ()) |
104 ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case2 ()) | 100 ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case2 ()) |
105 ominimal {n} record { lv = Zero ; ord = (OSuc .0 ord) } (case1 ()) | 101 ominimal {n} record { lv = Zero ; ord = (OSuc .0 ord) } (case1 ()) |
227 minord : (x : OD {n} ) → ¬ x ≡ od∅ → Minimumo (od→ord x) | 223 minord : (x : OD {n} ) → ¬ x ≡ od∅ → Minimumo (od→ord x) |
228 minord x not = ominimal (od→ord x) (∅9 x not) | 224 minord x not = ominimal (od→ord x) (∅9 x not) |
229 minimul : (x : OD {n} ) → ¬ x ≡ od∅ → OD {n} | 225 minimul : (x : OD {n} ) → ¬ x ≡ od∅ → OD {n} |
230 minimul x not = ord→od ( mino (minord x not)) | 226 minimul x not = ord→od ( mino (minord x not)) |
231 minimul<x : (x : OD {n} ) → (not : ¬ x ≡ od∅ ) → x ∋ minimul x not | 227 minimul<x : (x : OD {n} ) → (not : ¬ x ≡ od∅ ) → x ∋ minimul x not |
232 minimul<x x not = lemma0 where | 228 minimul<x x not = lemma0 (min<x (minord x not)) where |
233 lemma : def x (mino (minord x not)) | 229 lemma0 : mino (minord x not) o< (od→ord x) → def x (od→ord (ord→od (mino (minord x not)))) |
234 lemma = def-subst (defmin (minord x not)) oiso refl | 230 lemma0 m<x = def-subst {n} {ord→od (od→ord x)} {od→ord (ord→od (mino (minord x not)))} (o<→c< m<x) oiso refl |
235 lemma0 : def x (od→ord (ord→od (mino (minord x not)))) | |
236 lemma0 = def-subst {n} {x} lemma refl {!!} | |
237 regularity : (x : OD) → (not : ¬ x ≡ od∅ ) → | 231 regularity : (x : OD) → (not : ¬ x ≡ od∅ ) → |
238 Lift (suc n) (x ∋ minimul x not ) ∧ | 232 Lift (suc n) (x ∋ minimul x not ) ∧ |
239 (Select x (λ x₁ → Lift (suc n) ( minimul x not ∋ x₁) ∧ Lift (suc n) (x ∋ x₁)) ≡ od∅) | 233 (Select x (λ x₁ → Lift (suc n) ( minimul x not ∋ x₁) ∧ Lift (suc n) (x ∋ x₁)) ≡ od∅) |
240 proj1 ( regularity x non ) = lift ( minimul<x x non ) | 234 proj1 ( regularity x non ) = lift ( minimul<x x non ) |
241 proj2 ( regularity x non ) = {!!} | 235 proj2 ( regularity x non ) = cong ( λ k → record { def = k } ) ( extensionality ( λ y → lemma0 y) ) where |
236 lemma : ( z : Ordinal {n} ) → def (Select x (λ y → Lift (suc n) (minimul x non ∋ y) ∧ Lift (suc n) (x ∋ y))) z | |
237 lemma z with (minimul x non ∋ (ord→od z)) | x ∋ (ord→od z) | |
238 ... | s | t = {!!} | |
239 lemma0 : ( z : Ordinal {n} ) → def (Select x (λ y → Lift (suc n) (minimul x non ∋ y) ∧ Lift (suc n) (x ∋ y))) z ≡ Lift n ⊥ | |
240 lemma0 = {!!} | |
241 |