Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 971:4fdf889ca95a
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 07 Nov 2022 10:23:53 +0900 |
| parents | 980bc43ca6c1 |
| children | 520aff512969 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 28 insertions(+), 13 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Nov 07 08:04:35 2022 +0900 +++ b/src/zorn.agda Mon Nov 07 10:23:53 2022 +0900 @@ -883,7 +883,10 @@ -- x < supf px → UnionCF A f mf ay supf px ≡ UnionCF A f mf ay supf x zc43 : ( x o< sp1 ) ∨ ( sp1 o≤ x ) - zc43 = ? + zc43 with trio< x sp1 + ... | tri< a ¬b ¬c = case1 a + ... | tri≈ ¬a b ¬c = case2 (o≤-refl0 (sym b)) + ... | tri> ¬a ¬b c = case2 (o<→≤ c) zc41 : ZChain A f mf ay x zc41 with zc43 @@ -1043,6 +1046,14 @@ (trans (ZChain.supfmax zc px<x) (sym (ZChain.supfmax zc px<z))) (o≤-refl0 b) ... | tri> ¬a ¬b sf0<sp1 = ⊥-elim ( lt ( ordtrans≤-< (ZChain.supf-mono zc (o<→≤ px<x)) sf0<sp1 )) + 3cases : (¬ (supf0 px ≡ px)) ∨ ( ¬ (supf0 px o< sp1 )) ∨ ( (supf0 px ≡ px) ∧ (supf0 px o< sp1 )) + 3cases with o≡? (supf0 px) px + ... | no ne = case1 ne + ... | yes eq with trio< (supf0 px) sp1 + ... | tri< a ¬b ¬c = case2 (case2 ⟪ eq , a ⟫ ) + ... | tri≈ ¬a b ¬c = case2 (case1 ¬a ) + ... | tri> ¬a ¬b c = case2 (case1 ¬a ) + zc12 : {z : Ordinal} → supf0 px ≡ px → supf0 px o< sp1 → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ zc12 {z} sfpx=px sfpx<sp (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where @@ -1164,18 +1175,15 @@ -- z1 ≡ px , supf0 px ≡ px psz1≤px : supf1 z1 o≤ px psz1≤px = subst (λ k → supf1 z1 o< k ) (sym opx=x) sz1<x - sf0px<sp1 : supf0 px o< sp1 -- px o< sp1 o≤ x .. sp1 ≡ x - sf0px<sp1 = ? csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) - csupf2 with trio< z1 px | inspect supf1 z1 - csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px - ... | case2 lt = zc12 ? ? (case1 cs03) where + csupf2 with 3cases + ... | case2 (case2 p) with trio< z1 px | inspect supf1 z1 + ... | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px + ... | case2 lt = zc12 (proj1 p) (proj2 p) (case1 cs03) where cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1) cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) ) - ... | case1 sfz=sfpx = zc12 ? ? (case2 (init (ZChain.asupf zc) cs04 )) where - supu=u : supf1 (supf1 z1) ≡ supf1 z1 - supu=u = trans (cong supf1 sfz=px) (sym sfz=sfpx) + ... | case1 sfz=sfpx = zc12 (proj1 p) (proj2 p) (case2 (init (ZChain.asupf zc) cs04 )) where cs04 : supf0 px ≡ supf0 z1 cs04 = begin supf0 px ≡⟨ sym (sf1=sf0 o≤-refl) ⟩ @@ -1187,10 +1195,17 @@ cs05 : px o< supf0 px cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx cs06 : supf0 px o< osuc px - cs06 = subst (λ k → supf0 px o< k ) (sym opx=x) ? - csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 ? ? (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) - csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ? - -- ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ ) + cs06 = subst₂ (λ j k → j o< k ) (sym (proj1 p)) (sym opx=x) px<x + csupf2 | case2 (case2 p) | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 (proj1 p) (proj2 p) + (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) + csupf2 | case2 (case2 p) | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ⊥-elim ( ¬p<x<op ⟪ cs08 , cs09 ⟫ ) where + cs08 : px o< sp1 + cs08 = subst (λ k → k o< sp1 ) (proj1 p) (proj2 p ) + cs09 : sp1 o< osuc px + cs09 = subst ( λ k → sp1 o< k ) (sym (Oprev.oprev=x op)) sz1<x + + csupf2 | case2 (case1 p) = ? + csupf2 | case1 p = ? zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?