Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 902:49594badc9b4
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 09 Oct 2022 19:30:41 +0900 |
| parents | 6146d75131f5 |
| children | 5b6034ad8b98 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 24 insertions(+), 19 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sun Oct 09 17:58:41 2022 +0900 +++ b/src/zorn.agda Sun Oct 09 19:30:41 2022 +0900 @@ -828,20 +828,21 @@ -- supf1 x ≡ sp1, which is not included now pchainpx : HOD - pchainpx = record { od = record { def = λ z → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z } ; odmax = & A ; <odmax = zc00 } where - zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z → z o< & A + pchainpx = record { od = record { def = λ z → (odef A z ∧ UChain A f mf ay supf0 px z ) + ∨ FClosure A f (supf0 px) z } ; odmax = & A ; <odmax = zc00 } where + zc00 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f (supf0 px) z → z o< & A zc00 {z} (case1 lt) = z07 lt - zc00 {z} (case2 fc) = z09 ( A∋fc px f mf fc ) - zc01 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f px z → odef A z + zc00 {z} (case2 fc) = z09 ( A∋fc (supf0 px) f mf fc ) + zc01 : {z : Ordinal } → (odef A z ∧ UChain A f mf ay supf0 px z ) ∨ FClosure A f (supf0 px) z → odef A z zc01 {z} (case1 lt) = proj1 lt - zc01 {z} (case2 fc) = ( A∋fc px f mf fc ) + zc01 {z} (case2 fc) = ( A∋fc (supf0 px) f mf fc ) - zc02 : { a b : Ordinal } → odef A a ∧ UChain A f mf ay supf0 px a → FClosure A f px b → a <= b + 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 )) ? - zc05 : {b : Ordinal } → FClosure A f px b → a <= b - zc05 (fsuc b1 fb ) with proj1 ( mf b1 (A∋fc px f mf fb )) + 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) ? -- @@ -934,17 +935,21 @@ ; x<sup = ? ; minsup = ? } ; tsup=sup = sf1=sp1 px<z } csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) - csupf1 {z1} sz1<x with trio< (supf0 z1) px - ... | tri< a ¬b ¬c = subst₂ (λ j k → odef j k ) ? (sym (sf1=sf0 (o<→≤ a) )) (case1 (ZChain.csupf zc a )) where - z1≤px : z1 o≤ px - z1≤px = o<→≤ ( ZChain.supf-inject zc (subst (λ k → supf0 z1 o< k ) ? a )) - ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ zc21 , subst (λ k → z1 o< k ) (sym (Oprev.oprev=x op)) zc22 ⟫ ) where - zc21 : px o< z1 - zc21 = ZChain.supf-inject zc (subst (λ k → k o< supf0 z1) ? c ) - zc22 : z1 o< x -- c : px o< supf0 z1 - zc22 = ? -- supf-inject0 supf-mono1 (ordtrans<-≤ sz1<x ? ) - -- c : px ≡ spuf0 px o< supf0 z1 , px o< z1 o≤ supf1 z1 o< x + csupf1 {z1} sz1<x with trio< (supf1 z1) px + ... | tri< a ¬b ¬c = csupf0 where + zc18 : supf1 z1 ≡ supf0 z1 + zc18 = sf1=sf0 ? + csupf0 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) + csupf0 with ZChain.csupf zc (subst (λ k → k o< px) zc18 a ) + ... | ⟪ ab , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) (sym zc18) ab , ch-init ? ⟫ + ... | ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ subst (λ k → odef A k) (sym zc18) ab , + ch-is-sup u (subst (λ k → u o< k ) (Oprev.oprev=x op) (ordtrans u<x <-osuc) ) ? ? ⟫ + ... | tri≈ ¬a b ¬c = ⟪ asm , ch-is-sup (supf1 z1) sz1<x ? (init asm1 ? ) ⟫ where + asm : odef A (supf1 z1) + asm = subst (λ k → odef A k ) ? ( MinSUP.asm sup1) + asm1 : odef A (supf1 (supf1 z1)) + asm1 = subst (λ k → odef A k ) ? ( MinSUP.asm sup1) + ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x ⟫ ) zc4 : ZChain A f mf ay x --- supf px ≤ supf x zc4 with trio< x (supf0 px)