Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 907:a6f075a164fa
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 11 Oct 2022 10:41:19 +0900 |
| parents | 02f250be89e2 |
| children | d917831fb607 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 41 insertions(+), 12 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Oct 10 18:25:04 2022 +0900 +++ b/src/zorn.agda Tue Oct 11 10:41:19 2022 +0900 @@ -1042,19 +1042,35 @@ 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) + tsup : MinSUP A (UnionCF A f mf ay supf1 z) tsup=sup : supf1 z ≡ MinSUP.sup tsup sup : {z : Ordinal} → (z≤x : z o≤ x ) → STMP z≤x sup {z} z≤x with trio< z px ... | tri< a ¬b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.asm m - ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (sf1=sf0 (o<→≤ a) ) (ZChain.supf-is-minsup zc (o<→≤ a)) } where + ; x<sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o<→≤ a) ) (ZChain.supf-is-minsup zc (o<→≤ a)) } where m = ZChain.minsup zc (o<→≤ a) + ms00 : {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m) + ms00 {x} ux = MinSUP.x<sup m ? + ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} → + odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 + ms01 {sup2} us P = MinSUP.minsup m ? ? ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.asm m - ; x<sup = ? ; minsup = ? } ; tsup=sup = trans (sf1=sf0 (o≤-refl0 b) ) (ZChain.supf-is-minsup zc (o≤-refl0 b)) } where + ; x<sup = ms00 ; minsup = ms01 } ; tsup=sup = trans (sf1=sf0 (o≤-refl0 b) ) (ZChain.supf-is-minsup zc (o≤-refl0 b)) } where m = ZChain.minsup zc (o≤-refl0 b) + ms00 : {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m) + ms00 {x} ux = MinSUP.x<sup m ? + ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} → + odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 + ms01 {sup2} us P = MinSUP.minsup m ? ? ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1 - ; x<sup = ? ; minsup = ? } ; tsup=sup = sf1=sp1 px<z } + ; x<sup = ms00 ; minsup = ms01 } ; tsup=sup = sf1=sp1 px<z } where + m = sup1 + ms00 : {x : Ordinal} → odef (UnionCF A f mf ay supf1 z) x → (x ≡ MinSUP.sup m) ∨ (x << MinSUP.sup m) + ms00 {x} ux = MinSUP.x<sup m ? + ms01 : {sup2 : Ordinal} → odef A sup2 → ({x : Ordinal} → + odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 + ms01 {sup2} us P = MinSUP.minsup m ? ? csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) csupf1 {z1} sz1<x = csupf2 where @@ -1064,19 +1080,32 @@ 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 + csupf2 with trio< z1 px | inspect supf1 z1 + csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px + ... | case1 eq = ⟪ ZChain.asupf zc , 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 + -- supf0 z1 ≡ supf1 z1 ≡ px, z1 o< px + supu=u : supf1 (supf1 z1) ≡ supf1 z1 + supu=u = ? ... | 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 + ... | ⟪ ab , ch-init fc ⟫ = ⟪ ab , ch-init fc ⟫ + ... | ⟪ ab , ch-is-sup u u<x is-sup fc ⟫ = ⟪ ab , + ch-is-sup u (subst (λ k → u o< k ) (Oprev.oprev=x op) (ordtrans u<x <-osuc) ) + record { fcy<sup = ? ; order = ? ; supu=u = ? } (fcpu fc (o<→≤ u<x)) ⟫ + csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ ZChain.asupf zc , 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 ≡ 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 = ? + supu=u : supf1 (supf1 z1) ≡ supf1 z1 + supu=u = ? + csupf2 | tri> ¬a ¬b c | record { eq = eq1 } = ⟪ 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 + supu=u : supf1 (supf1 z1) ≡ supf1 z1 + supu=u = ? zc4 : ZChain A f mf ay x --- x o≤ supf px zc4 with trio< x (supf0 px)