Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 849:f1f779930fbf
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 04 Sep 2022 14:25:01 +0900 |
| parents | 56a150965988 |
| children | 2d8ce664ae31 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 43 insertions(+), 51 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sun Sep 04 08:50:53 2022 +0900 +++ b/src/zorn.agda Sun Sep 04 14:25:01 2022 +0900 @@ -774,6 +774,12 @@ ... | tri≈ ¬a b ¬c = refl ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤px c ) + supf1=sp : {z : Ordinal } → x o≤ z → supf1 z ≡ sp1 + supf1=sp {z} x≤z with trio< z px + ... | tri< a ¬b ¬c = ⊥-elim ( o≤> x≤z (subst (λ k → z o< k ) (Oprev.oprev=x op) (ordtrans a <-osuc ))) + ... | tri≈ ¬a refl ¬c = ⊥-elim ( o≤> x≤z (pxo<x op)) + ... | tri> ¬a ¬b c = refl + supf∈A : {b : Ordinal} → b o≤ x → odef A (supf1 b) supf∈A {b} b≤z = ? @@ -963,58 +969,44 @@ ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt → IsSup.x<sup is-sup (subst (λ k → odef k w) pchain0=1 lt) } } csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b) - csupf {b} b≤x with osuc-≡< b≤x - ... | case2 b<x = csupf1 where - b≤px : b o≤ px - b≤px = zc-b<x _ b<x - csupf0 : odef (UnionCF A f mf ay supf0 (supf1 b)) (supf1 b) - csupf0 = subst (λ k → odef (UnionCF A f mf ay supf0 k) k ) (supf0=1 b≤px) ( ZChain.csupf zc b≤px ) - csupf1 : odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b) - csupf1 with csupf0 - ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ - ... | ⟪ as , ch-is-sup u u≤x record { fcy<sup = fcy<sup ; order = order ; supu=u = supu=u } fc ⟫ - with osuc-≡< (subst₂ (λ j k → j o≤ k ) (sym supu=u ) (sym (supf0=1 b≤px)) u≤x) - ... | case1 eq = ⟪ as , ch-is-sup u u≤x record { fcy<sup = fcy<sup1 ; order = order1 ; supu=u = supu=u1 } fc1 ⟫ - where - s0b=s0u : supf0 u ≡ supf0 b -- u ≡ supf0 b - s0b=s0u = eq - u≤sb : u o≤ supf1 b - u≤sb = u≤x - supu=u1 : supf1 u ≡ u - supu=u1 with trio< u px - ... | tri< a ¬b ¬c = supu=u - ... | tri≈ ¬a b ¬c = supu=u - ... | tri> ¬a ¬b c = ? -- supf1 b ≡ sp1 , u o≤ sp1, x o≤ u o≤ supf1 b -- u ≡ x → xsup x → ⊥ - fc0 : FClosure A f (supf0 u) (supf1 b) - fc0 = fc - fc1 : FClosure A f (supf1 u) (supf1 b) - fc1 = ? - -- u > x → supf1 u ≡ sp1 → supf1 b o≤ supf1 u - -- px o< u o≤ sp1 , spuf1 u o≤ spuf1 sp1 - fcy<sup1 : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u) ∨ (z << supf1 u) - fcy<sup1 = ? - order1 : {s z1 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z1 + csupf {b} b≤x = ⟪ zc01 , ch-is-sup u o≤-refl + record { fcy<sup = fcy<sup ; order = order ; supu=u = supu=u } fc ⟫ where + csupf0 : b o≤ px → odef (UnionCF A f mf ay supf0 (supf1 b)) (supf1 b) + csupf0 b≤px = subst (λ k → odef (UnionCF A f mf ay supf0 k) k ) (supf0=1 b≤px) ( ZChain.csupf zc b≤px ) + zc04 : (b o≤ px ) ∨ (b ≡ x ) + zc04 with trio< b px + ... | tri< a ¬b ¬c = case1 (o<→≤ a) + ... | tri≈ ¬a b ¬c = case1 (o≤-refl0 b) + ... | tri> ¬a ¬b px<b with osuc-≡< b≤x + ... | case1 eq = case2 eq + ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) + zc01 : odef A (supf1 b) + zc01 with zc04 + ... | case1 le = proj1 ( csupf0 le ) + ... | case2 eq = subst (λ k → odef A k ) (sym (supf1=sp (o≤-refl0 (sym eq)))) (SUP.as sup1) + u = supf1 b + supu=u : supf1 u ≡ u + supu=u with zc04 + ... | case2 eq = begin + supf1 u ≡⟨ cong supf1 (supf1=sp ? ) ⟩ + supf1 sp1 ≡⟨ supf1=sp ? ⟩ + sp1 ≡⟨ sym (supf1=sp ?) ⟩ + u ∎ where open ≡-Reasoning + ... | case1 le = subst (λ k → k ≡ u ) (supf0=1 zc05 ) ( ZChain.sup=u zc zc01 zc05 ? ) where + zc06 : b o≤ px + zc06 = le + zc05 : supf1 b o≤ px + zc05 = ? + zc02 : odef A (supf1 u) + zc02 = subst (λ k → odef A k ) (sym supu=u) zc01 + zc03 : supf1 u ≡ supf1 b + zc03 = ? + fc : FClosure A f (supf1 u) (supf1 b) + fc = init zc02 zc03 + fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u) ∨ (z << supf1 u) + fcy<sup = ? + order : {s z1 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u) - order1 = ? - ... | case2 lt = chain-mono f mf ay supf1 b≤sb (UnionCF0⊆1 b≤px zc12 ) where - b≤sb : b o≤ supf1 b -- ≡ supf0 b - b≤sb = ? - lt1 : supf0 u o< supf0 b - lt1 = lt - zc12 : odef (UnionCF A f mf ay supf0 b) (supf1 b) - zc12 = subst (λ k → odef (UnionCF A f mf ay supf0 b) k) &iso ( ZChain.csupf-fc zc b≤px lt fc ) - ... | case1 refl = ⟪ supf∈A o≤-refl , ch-is-sup (supf1 x) o≤-refl - record { fcy<sup = fcy<sup ; order = order ; supu=u = zc11 } (init zc10 zc11 ) ⟫ where - zc12 : supf1 x ≡ sp1 - zc12 = ? - zc11 : supf1 (supf1 x) ≡ supf1 x - zc11 = ? - zc10 : odef A (supf1 (supf1 x)) - zc10 = subst (λ k → odef A k ) (sym zc11) ( supf∈A o≤-refl ) - fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 (supf1 x)) ∨ (z << supf1 (supf1 x)) - fcy<sup = ? - order : {s z1 : Ordinal} → supf1 s o< supf1 (supf1 b) → FClosure A f (supf1 s) z1 - → (z1 ≡ supf1 (supf1 b)) ∨ (z1 << supf1 (supf1 b)) order = ? sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x)) sis {z} z≤x = zc40 where