Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 906:02f250be89e2
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 10 Oct 2022 18:25:04 +0900 |
| parents | e6a282eb12fe |
| children | a6f075a164fa |
| files | src/zorn.agda |
| diffstat | 1 files changed, 20 insertions(+), 15 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Oct 10 12:20:38 2022 +0900 +++ b/src/zorn.agda Mon Oct 10 18:25:04 2022 +0900 @@ -1057,21 +1057,26 @@ ; 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< (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 ⟫ ) + csupf1 {z1} sz1<x = csupf2 where + -- z1 o< px → supf1 z1 ≡ supf0 z1 + -- z1 ≡ px , supf0 px o< px .. px o< z1, x o≤ z1 ... supf1 z1 ≡ sp1 + -- z1 ≡ px , supf0 px ≡ px + psz1≤px : supf1 z1 o≤ px + psz1≤px = subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x + csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) + csupf2 with trio< z1 px + csupf2 | tri< a ¬b ¬c with osuc-≡< psz1≤px + ... | case1 eq = ? -- supf0 z1 ≡ supf1 z1 ≡ px, z1 o< px + ... | case2 lt with ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) + ... | ⟪ ab , ch-init fc ⟫ = ⟪ subst (λ k → odef A k) ? ab , ch-init ? ⟫ + ... | ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ? , + ch-is-sup u (subst (λ k → u o< k ) (Oprev.oprev=x op) (ordtrans u<x <-osuc) ) ? ? ⟫ + csupf2 | tri≈ ¬a b ¬c = ? where -- supf1 z1 ≡ supf0 z1, z1 ≡ px + 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) + csupf2 | tri> ¬a ¬b c = ? zc4 : ZChain A f mf ay x --- x o≤ supf px zc4 with trio< x (supf0 px)