Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/zorn.agda @ 912:870a6b57dd39
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 12 Oct 2022 14:03:38 +0900 |
parents | 3105feb3c4e1 |
children | d5293a7c2ec4 |
line wrap: on
line diff
--- a/src/zorn.agda Wed Oct 12 11:11:42 2022 +0900 +++ b/src/zorn.agda Wed Oct 12 14:03:38 2022 +0900 @@ -407,7 +407,7 @@ minsup : {x : Ordinal } → x o≤ z → MinSUP A (UnionCF A f mf ay supf x) supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z ) - csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain + csupf : {b x : Ordinal } → supf b o< x → x o≤ z → odef (UnionCF A f mf ay supf x) (supf b) -- supf z is not an element of this chain chain : HOD chain = UnionCF A f mf ay supf z @@ -456,6 +456,9 @@ -- ordering is not proved here but in ZChain1 + -- csupf< : {a b : Ordinal } → a o≤ b → odef (UnionCF A f mf ay supf z) (supf a) → odef (UnionCF A f mf ay supf z) (supf b) + -- csupf< = ? + record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where supf = ZChain.supf zc @@ -608,7 +611,7 @@ s≤<z : s o≤ & A s≤<z = ordtrans s<b b≤z zc04 : odef (UnionCF A f mf ay supf (& A)) (supf s) - zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc)) + zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc)) o≤-refl zc05 : odef (UnionCF A f mf ay supf b) (supf s) zc05 with zc04 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ @@ -816,7 +819,7 @@ zc41 : supf0 px o< x → ZChain A f mf ay x zc41 sfpx<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ? - ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupf1 } where + ; supfmax = ? ; minsup = ? ; supf-is-minsup = ? ; csupf = csupfp } where -- supf0 px is included by the chain -- ( UnionCF A f mf ay supf0 px ∪ FClosure (supf0 px) ) ≡ UnionCF supf1 x -- supf1 x ≡ sp1, which is not included now @@ -1014,10 +1017,10 @@ sf<px : supf0 s o< px sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) (sfpx=px)) ss<spx csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 - csupf17 (init as refl ) = ZChain.csupf zc sf<px + csupf17 (init as refl ) = ZChain.csupf zc sf<px o≤-refl csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc) - ... | case2 sfp<px with ZChain.csupf zc sfp<px -- odef (UnionCF A f mf ay supf0 px) (supf0 px) + ... | case2 sfp<px with ZChain.csupf zc sfp<px o≤-refl -- odef (UnionCF A f mf ay supf0 px) (supf0 px) ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ ua1 , ch-init fc₁ ⟫ ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u (ordtrans u≤x px<x) record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ (o<→≤ u≤x) ) ⟫ where @@ -1078,13 +1081,13 @@ psz1≤px : supf1 z1 o≤ px psz1≤px = subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x cs01 : supf0 px o< px → odef (UnionCF A f mf ay supf0 px) (supf0 px) - cs01 spx<px = ZChain.csupf zc spx<px + cs01 spx<px = ZChain.csupf zc spx<px o≤-refl 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 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 ) + cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) o≤-refl ... | 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 @@ -1098,7 +1101,7 @@ ... | case2 sfz<sfpx = ? --- supf0 z1 o< supf0 px 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 } with trio< sp1 px - ... | tri< sp1<px ¬b ¬c = ? -- sp1 o< px, supf0 sp1 ≡ supf0 px, sp1 o< z1 + ... | tri< sp1<px ¬b ¬c = ? -- sp1 o< px, supf0 sp1 o≤ px, supf0 sp1 o≤ supf0 px, sp1 o< z1 ... | tri≈ ¬a sp1=px ¬c = ⟪ MinSUP.asm sup1 , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x) record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where -- supf1 z1 ≡ sp1, px o< z1, sp1 o< x -- sp1 o< z1 @@ -1114,6 +1117,13 @@ supu=u = ? ... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x ⟫ ) + csupfp : {w z : Ordinal } → supf1 w o< z → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 w) + csupfp {w} {z} sw1<z z≤x with osuc-≡< z≤x + ... | case1 eq = ? + ... | case2 lt = ? where + csupfpx : odef (UnionCF A f mf ay supf0 z) (supf0 w) + csupfpx = ZChain.csupf zc ? ? + zc4 : ZChain A f mf ay x --- x o≤ supf px zc4 with trio< x (supf0 px) ... | tri> ¬a ¬b c = zc41 c