Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 61:f2cb756084e0
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 29 May 2019 13:02:03 +0900 |
| parents | 6a1f67a4cc6e |
| children | 05494b4689ed |
| files | ordinal-definable.agda |
| diffstat | 1 files changed, 16 insertions(+), 25 deletions(-) [+] |
line wrap: on
line diff
--- a/ordinal-definable.agda Wed May 29 12:06:43 2019 +0900 +++ b/ordinal-definable.agda Wed May 29 13:02:03 2019 +0900 @@ -355,29 +355,20 @@ lemma0 m<x = def-subst {suc n} {ord→od (od→ord x)} {od→ord (ord→od (mino (minord x not)))} (o<→c< m<x) oiso refl regularity : (x : OD) (not : ¬ (x == od∅)) → (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) - regularity x not = regularity-ord (od→ord x) x (sym oiso ) not where - regularity-ord : (ox : Ordinal ) → (x : OD) → ( x ≡ ord→od ox ) → (not : ¬ (x == od∅)) + regularity x not = regularity-ord (od→ord x) {x} (sym oiso ) not where + regularity-ord : (ox : Ordinal ) → {x : OD} → ( x ≡ ord→od ox ) → (not : ¬ (x == od∅)) → (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) - regularity-ord ox x refl not = record { proj1 = minimul<x x not ; proj2 = record {eq→ = reg0 ; eq← = λ () } } where - noto : o∅ o< (od→ord (ord→od ox)) - noto = lemma {ox} {od→ord (ord→od ox)} diso (∅10 refl not) where - lemma : { ox oy : Ordinal {suc n}} → oy ≡ ox → o∅ o< ox → o∅ o< oy - lemma refl lt = lt - Min : Minimumo ox - Min = ominimal ox (∅10 refl not) - Mino : Minimumo (od→ord (ord→od ox )) - Mino = ominimal (od→ord (ord→od ox )) noto - m=mo : ox ≡ od→ord (ord→od ox ) → mino Mino ≡ mino Min - m=mo eq with ox - ... | xx = ? - reg0 : {y : Ordinal {suc n}} → def (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁))) y → def od∅ y - reg0 {y} t with trio< y ( mino Mino ) - reg0 {y} t | tri< a ¬b ¬c = {!!} - reg0 {y} t | tri≈ ¬a refl ¬c with o≡→¬c< {suc n} {ord→od (mino Mino)} refl lemma where - lemma : ord→od y c< ord→od (mino Mino) - lemma = subst (λ k → k c< ord→od (mino Mino) ) oiso {!!} -- (proj1 t) - reg0 {y} t | tri≈ ¬a b ¬c | () - reg0 {y} t | tri> ¬a ¬b c with o<> y (mino Mino) lemma c where - lemma : y o< mino Mino - lemma = {!!} - reg0 {y} t | tri> ¬a ¬b c | () + regularity-ord ox {x} refl not with ominimal ox (∅10 refl not) + regularity-ord record { lv = Zero ; ord = (Φ .0) } refl not | record { mino = mino ; min<x = case1 () } + regularity-ord record { lv = Zero ; ord = (Φ .0) } refl not | record { mino = mino ; min<x = case2 () } + regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) } refl not | record { mino = min ; min<x = case1 () } + regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) } refl not | record { mino = record { lv = Suc lv₁ ; ord = ord } ; min<x = case2 () } + regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) } refl not | record { mino = record { lv = Zero ; ord = Φ .0 } ; min<x = case2 Φ< } + = record { proj1 = {!!} ; proj2 = record { eq→ = {!!} ; eq← = λ () }} where + lemma : ? -- ominimal ox (∅10 refl not) ≡ minimul x not + lemma = {!!} + regularity-ord record { lv = Zero ; ord = (OSuc .0 ord₁) } refl not | record { mino = record { lv = Zero ; ord = OSuc .0 ord₂ } ; min<x = case2 (s< lt) } = {!!} + regularity-ord record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } refl not | record { mino = min ; min<x = case1 lt } = {!!} + regularity-ord record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } refl not | record { mino = min ; min<x = case2 () } + regularity-ord record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } refl not | record { mino = min ; min<x = min<x } = {!!} + regularity-ord record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) } refl not | record { mino = min ; min<x = min<x } = {!!}