Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 903:5b6034ad8b98
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 09 Oct 2022 21:51:23 +0900 |
| parents | 49594badc9b4 |
| children | 4541c9974e53 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 111 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sun Oct 09 19:30:41 2022 +0900 +++ b/src/zorn.agda Sun Oct 09 21:51:23 2022 +0900 @@ -839,14 +839,14 @@ zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f (supf0 px) b → a <= b zc02 {a} {b} ca fb = zc05 fb where - zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ px - zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) ? + zc06 : MinSUP.sup (ZChain.minsup zc o≤-refl) ≡ supf0 px + zc06 = trans (sym ( ZChain.supf-is-minsup zc o≤-refl )) refl zc05 : {b : Ordinal } → FClosure A f (supf0 px) b → a <= b zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc (supf0 px) f mf fb )) ... | case1 eq = subst (λ k → a <= k ) (subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) eq)) (zc05 fb) ... | case2 lt = <-ftrans (zc05 fb) (case2 lt) - zc05 (init b1 refl) with MinSUP.x<sup (ZChain.minsup zc o≤-refl) ? -- - -- (subst (λ k → odef A k ∧ UChain A f mf ay supf0 (supf0 px) k) (sym &iso) ca ) + zc05 (init b1 refl) with MinSUP.x<sup (ZChain.minsup zc o≤-refl) + (subst (λ k → odef A k ∧ UChain A f mf ay supf0 px k) (sym &iso) ca ) ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso zc06 eq ) ... | case2 lt = case2 (subst₂ (λ j k → j < k ) *iso (cong (*) zc06) lt ) @@ -867,7 +867,7 @@ ... | case2 lt = tri> (<-irr (case2 lt1)) (λ eq → <-irr (case1 eq) lt1) lt1 where lt1 : a0 < b0 lt1 = subst₂ (λ j k → j < k ) *iso *iso lt - ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp px f mf a b) + ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp (supf0 px) f mf a b) pcha : pchainpx ⊆' A pcha (case1 lt) = proj1 lt @@ -895,6 +895,12 @@ ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (sym b) px<z ) ... | tri> ¬a ¬b c = refl + asupf1 : {z : Ordinal } → odef A (supf1 z) + asupf1 {z} with trio< z px + ... | tri< a ¬b ¬c = ZChain.asupf zc + ... | tri≈ ¬a b ¬c = ZChain.asupf zc + ... | tri> ¬a ¬b c = MinSUP.asm sup1 + supf1-mono : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b supf1-mono {a} {b} a≤b with trio< b px ... | tri< a ¬b ¬c = subst₂ (λ j k → j o≤ k ) (sym (sf1=sf0 (o<→≤ (ordtrans≤-< a≤b a)))) refl ( supf-mono a≤b ) @@ -918,6 +924,106 @@ zc18 = subst (λ k → k o≤ sp1) zc20( MinSUP.minsup zc21 (MinSUP.asm sup1) zc24 ) ... | tri> ¬a ¬b c = o≤-refl + + fcup : {u z : Ordinal } → FClosure A f (supf1 u) z → u o≤ px → FClosure A f (supf0 u) z + 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 u<x is-sup fc ⟫ = zc21 fc where + zc21 : {z1 : Ordinal } → FClosure A f (supf1 u) z1 → odef pchainpx z1 + zc21 {z1} (fsuc z2 fc ) with zc21 fc + ... | case1 ⟪ ua1 , ch-init fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ + ... | case1 ⟪ ua1 , ch-is-sup u u<x u1-is-sup fc₁ ⟫ = case1 ⟪ proj2 ( mf _ ua1) , ch-is-sup u u<x u1-is-sup (fsuc _ fc₁) ⟫ + ... | case2 fc = case2 (fsuc _ fc) + zc21 (init asp refl ) with trio< u px | inspect supf1 u + ... | tri< a ¬b ¬c | _ = case1 ⟪ asp , ch-is-sup u a record {fcy<sup = zc13 ; order = zc17 + ; supu=u = trans (sym (sf1=sf0 (o<→≤ a))) (ChainP.supu=u is-sup) } (init asp refl) ⟫ where + zc17 : {s : Ordinal} {z1 : Ordinal} → supf0 s o< supf0 u → + FClosure A f (supf0 s) z1 → (z1 ≡ supf0 u) ∨ (z1 << supf0 u) + zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) ((sf1=sf0 zc19)) ( ChainP.order is-sup + (subst₂ (λ j k → j o< k ) (sym (sf1=sf0 zc18)) (sym (sf1=sf0 zc19)) ss<spx) (fcpu fc zc18) ) where + zc19 : u o≤ px + zc19 = o<→≤ a + zc18 : s o≤ px + zc18 = ordtrans (ZChain.supf-inject zc ss<spx) zc19 + zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u ) + zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ a)) ( ChainP.fcy<sup is-sup fc ) + ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) (cong supf0 b) asp ) (cong supf0 (sym b)) ) + ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ 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 u<x is-sup fc ⟫ ) = zc21 fc where + zc21 : {z1 : Ordinal } → FClosure A f (supf0 u) 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 trio< u px | inspect supf1 u + ... | tri< a ¬b ¬c | _ = ⟪ asp , ch-is-sup u + (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc)) + record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sf1=sf0 (o<→≤ u<x)) (ChainP.supu=u is-sup) } zc14 ⟫ where + zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u → + FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u) + zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (sym (sf1=sf0 (o<→≤ u<x))) ( ChainP.order is-sup + (subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ u<x)) ss<spx) (fcup fc s≤px) ) where + s≤px : s o≤ px + s≤px = ordtrans ( supf-inject0 supf1-mono ss<spx ) (o<→≤ u<x) + zc14 : FClosure A f (supf1 u) (supf0 u) + zc14 = init (subst (λ k → odef A k ) (sym (sf1=sf0 (o<→≤ u<x))) asp) (sf1=sf0 (o<→≤ u<x)) + zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) + zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 (o<→≤ u<x))) ( ChainP.fcy<sup is-sup fc ) + ... | tri≈ ¬a b ¬c | _ = ⟪ asp , ch-is-sup px (pxo<x op) record { fcy<sup = zc13 + ; order = zc17 ; supu=u = zc18 } (init asupf1 (trans (sf1=sf0 o≤-refl ) (cong supf0 (sym b))) ) ⟫ where + zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px) ∨ ( z << supf1 px ) + zc13 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) (ChainP.fcy<sup is-sup fc ) + zc18 : supf1 px ≡ px + zc18 = begin + supf1 px ≡⟨ sf1=sf0 o≤-refl ⟩ + supf0 px ≡⟨ cong supf0 (sym b) ⟩ + supf0 u ≡⟨ ChainP.supu=u is-sup ⟩ + u ≡⟨ b ⟩ + px ∎ where open ≡-Reasoning + zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px → + FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px) + zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k)) (trans (cong supf0 b) (sym (sf1=sf0 o≤-refl))) + ( ChainP.order is-sup (subst₂ (λ j k → j o< k) (sf1=sf0 s≤px) zc19 ss<spx) (fcup fc s≤px) ) where + zc19 : supf1 px ≡ supf0 u + zc19 = trans (sf1=sf0 o≤-refl) (cong supf0 (sym b)) + s≤px : s o≤ px + s≤px = o<→≤ (supf-inject0 supf1-mono ss<spx) + ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , o<→≤ u<x ⟫ ) + zc12 {z} (case2 fc) = zc21 fc where + 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 ) = ⟪ asp , ch-is-sup (supf0 px) ? + record {fcy<sup = ? ; order = ? ; supu=u = ? } ? ⟫ where + zc15 : supf1 px ≡ px + zc15 = trans (sf1=sf0 o≤-refl ) ? + zc14 : FClosure A f (supf1 px) px + zc14 = init (subst (λ k → odef A k) ? asp) zc15 + zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 px ) ∨ ( z << supf1 px ) + zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 o≤-refl)) ( ZChain.fcy<sup zc o≤-refl fc ) + zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px → + FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px) + zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) mins-is-spx + (MinSUP.x<sup mins (csupf17 (fcup fc (o<→≤ s<px) )) ) where + mins : MinSUP A (UnionCF A f mf ay supf0 px) + mins = ZChain.minsup zc o≤-refl + mins-is-spx : MinSUP.sup mins ≡ supf1 px + mins-is-spx = trans (sym ( ZChain.supf-is-minsup zc o≤-refl ) ) (sym (sf1=sf0 o≤-refl )) + s<px : s o< px + s<px = supf-inject0 supf1-mono ss<spx + sf<px : supf0 s o< px + sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) ?) ss<spx + -- (sf1=sf0 ?) (trans ? 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 (fsuc x fc) = ZChain.f-next zc (csupf17 fc) + + record STMP {z : Ordinal} (z≤x : z o≤ x ) : Set (Level.suc n) where field tsup : MinSUP A (UnionCF A f mf ay supf0 z)