Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 967:cd0ef83189c5
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 05 Nov 2022 18:29:21 +0900 |
| parents | 39c680188738 |
| children | 9a8041a7f3c9 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 30 insertions(+), 33 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sat Nov 05 13:21:42 2022 +0900 +++ b/src/zorn.agda Sat Nov 05 18:29:21 2022 +0900 @@ -859,10 +859,30 @@ sup1 = minsupP pchainpx pcha ptotal sp1 = MinSUP.sup sup1 + sfpx<sp1 : supf0 px <= sp1 + sfpx<sp1 = MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl )) + -- -- supf0 px o≤ sp1 -- + --- x ≦ supf px ≦ x ≦ sp ≦ x + -- x may apper any place + + -- x < sp → supf x = supf px + -- x ≡ sp → supf x = sp + -- sp < x → supf x = sp ≡ supf px + -- UnionCF A f mf ay supf px ⊆ UnionCF A f mf ay supf x + + -- supf x does not affect UnionCF A f mf ay supf x + + -- supf px < px → UnionCF A f mf ay supf px ≡ UnionCF A f mf ay supf x + -- supf px ≡ px → UnionCF A f mf ay supf px ⊂ UnionCF A f mf ay supf x ≡ pchainx + -- 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 = ? + zc41 : ZChain A f mf ay x zc41 with MinSUP.x≤sup sup1 (case2 (init (ZChain.asupf zc {px}) refl )) zc41 | (case2 sfpx<sp1) = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ? @@ -923,6 +943,7 @@ fcup {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sf1=sf0 u≤px) fc fcpu : {u z : Ordinal } → FClosure A f (supf0 u) z → u o≤ px → FClosure A f (supf1 u) z fcpu {u} {z} fc u≤px = subst (λ k → FClosure A f k z ) (sym (sf1=sf0 u≤px)) fc + zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z zc11 {z} ⟪ az , ch-init fc ⟫ = case1 ⟪ az , ch-init fc ⟫ zc11 {z} ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ = zc21 fc where @@ -952,9 +973,10 @@ zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ u<px)) ( ChainP.fcy<sup is-sup fc ) ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) b (ZChain.asupf zc) ) (sym (trans (sf1=sf0 u≤px) b ))) ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ ZChain.supf-inject zc c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) - zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z - zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ - zc12 {z} (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where + + zc12 : {z : Ordinal} → supf0 px ≡ px → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z + zc12 {z} sfpx=px (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ + zc12 {z} sfpx=px (case1 ⟪ az , ch-is-sup u su<sx is-sup fc ⟫ ) = zc21 fc where u<px : u o< px u<px = ZChain.supf-inject zc su<sx u<x : u o< x @@ -1001,16 +1023,13 @@ s≤px : s o≤ px s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx) ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , u≤px ⟫ ) - zc12 {z} (case2 fc) = zc21 fc where + zc12 {z} sfpx=px (case2 fc) = zc21 fc where --- supf0 px o< sp1 - zc20 : (supf0 px ≡ px ) ∨ ( supf0 px o< px ) - zc20 = ? zc21 : {z1 : Ordinal } → FClosure A f (supf0 px) z1 → odef (UnionCF A f mf ay supf1 x) z1 zc21 {z1} (fsuc z2 fc ) with zc21 fc ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ ... | ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ - zc21 (init asp refl ) with zc20 - ... | case1 sfpx=px = ⟪ asp , ch-is-sup px zc18 + zc21 (init asp refl ) = ⟪ asp , ch-is-sup px zc18 record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where zc15 : supf1 px ≡ px zc15 = trans (sf1=sf0 o≤-refl ) (sfpx=px) @@ -1036,28 +1055,6 @@ csupf17 (init as refl ) = ZChain.csupf zc sf<px 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) - ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ ua1 , ch-init fc₁ ⟫ - ... | ⟪ ua1 , ch-is-sup u u<x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u zc18 - record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ ? ) ⟫ where - z10 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) - z10 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? )) (ChainP.fcy<sup is-sup fc) - z11 : {s z1 : Ordinal} → (lt : supf1 s o< supf1 u ) → FClosure A f (supf1 s ) z1 - → (z1 ≡ supf1 u ) ∨ ( z1 << supf1 u ) - z11 {s} {z} lt fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 ? )) - (ChainP.order is-sup lt0 (fcup fc s≤px )) where - s<u : s o< u - s<u = supf-inject0 supf1-mono lt - s≤px : s o≤ px - s≤px = ordtrans s<u ? -- (o<→≤ u<x) - lt0 : supf0 s o< supf0 u - lt0 = subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 ? ) lt - z12 : supf1 u ≡ u - z12 = trans (sf1=sf0 ? ) (ChainP.supu=u is-sup) - zc18 : supf1 u o< supf1 x - zc18 = ? - - record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where field @@ -1101,11 +1098,11 @@ 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 + ... | 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 ) ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) ) - ... | case1 sfz=sfpx = zc12 (case2 (init (ZChain.asupf zc) cs04 )) where + ... | 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) cs04 : supf0 px ≡ supf0 z1 @@ -1120,7 +1117,7 @@ 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 ¬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 ⟫ )