Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 997:908369b2d08b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 17 Nov 2022 17:04:47 +0900 |
| parents | 61d74b3d5456 |
| children | e5f46d08c074 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 38 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Thu Nov 17 09:51:36 2022 +0900 +++ b/src/zorn.agda Thu Nov 17 17:04:47 2022 +0900 @@ -1033,10 +1033,36 @@ fcs<sup {a} {b} {w} a<b b≤x fc with trio< a px ... | tri< a<px ¬b ¬c = z50 where z50 : odef (UnionCF A f mf ay supf1 b) w - z50 with ZChain.fcs<sup zc a<px o≤-refl fc + z50 with osuc-≡< b≤x + ... | case2 lt with ZChain.fcs<sup zc a<b (subst (λ k → b o< k) (sym (Oprev.oprev=x op)) lt) fc ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - ... | ⟪ az , ch-is-sup u u<x is-sup fc ⟫ = ⟪ az , ch-is-sup u ? ? ? ⟫ - ... | tri≈ ¬a a=px ¬c = ⟪ A∋fc _ f mf fc , ch-is-sup px px<b ? ? ⟫ where -- a ≡ px , b ≡ x, sp o≤ x → supf px o≤ supf x + ... | ⟪ az , ch-is-sup u u<b is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc u≤px ) ⟫ where -- u o< px → u o< b ? + u≤px : u o≤ px + u≤px = subst (λ k → u o< k) (sym (Oprev.oprev=x op)) (ordtrans<-≤ u<b b≤x ) + u<x : u o< x + u<x = ordtrans<-≤ u<b b≤x + cp1 : ChainP A f mf ay supf1 u + cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x) (ChainP.fcy<sup is-sup fc ) + ; order = λ {s} {z} s<u fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x) + (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) + (sym (sf=eq u<x)) s<u) + (subst (λ k → FClosure A f k z ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) fc )) + ; supu=u = trans (sym (sf=eq u<x)) (ChainP.supu=u is-sup) } + z50 | case1 eq with ZChain.fcs<sup zc a<px o≤-refl fc + ... | ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ + ... | ⟪ az , ch-is-sup u u<px is-sup fc ⟫ = ⟪ az , ch-is-sup u u<b cp1 (fcpu fc (o<→≤ u<px)) ⟫ where -- u o< px → u o< b ? + u<b : u o< b + u<b = subst (λ k → u o< k ) (trans (Oprev.oprev=x op) (sym eq) ) (ordtrans u<px <-osuc ) + u<x : u o< x + u<x = subst (λ k → u o< k ) (Oprev.oprev=x op) ( ordtrans u<px <-osuc ) + cp1 : ChainP A f mf ay supf1 u + cp1 = record { fcy<sup = λ {z} fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x) (ChainP.fcy<sup is-sup fc ) + ; order = λ {s} {z} s<u fc → subst (λ k → (z ≡ k) ∨ ( z << k ) ) (sf=eq u<x) + (ChainP.order is-sup (subst₂ (λ j k → j o< k ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) + (sym (sf=eq u<x)) s<u) + (subst (λ k → FClosure A f k z ) (sym (sf=eq (ordtrans (supf-inject0 supf1-mono s<u) u<x) )) fc )) + ; supu=u = trans (sym (sf=eq u<x)) (ChainP.supu=u is-sup) } + ... | tri≈ ¬a a=px ¬c = ⟪ A∋fc _ f mf fc , ch-is-sup px px<b cp1 z51 ⟫ where -- a ≡ px , b ≡ x, sp o≤ x → supf px o≤ supf x px<b : px o< b px<b = subst₂ (λ j k → j o< k) a=px refl a<b b=x : b ≡ x @@ -1044,6 +1070,12 @@ ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) a ⟫ ) -- px o< b o< x ... | tri≈ ¬a b ¬c = b ... | tri> ¬a ¬b c = ⊥-elim ( o≤> b≤x c ) -- x o< b + z51 : FClosure A f (supf1 px) w + z51 = subst (λ k → FClosure A f k w) (sym (trans (cong supf1 (sym a=px)) (sf1=sf0 (o≤-refl0 a=px) ))) fc + cp1 : ChainP A f mf ay supf1 px + cp1 = record { fcy<sup = λ {z} fc → ? + ; order = λ {s} {z} s<u fc → ? + ; supu=u = ? } ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) ( ordtrans<-≤ a<b b≤x) ⟫ ) -- px o< a o< b o≤ x zc11 : {z : Ordinal} → odef (UnionCF A f mf ay supf1 x) z → odef pchainpx z @@ -1088,7 +1120,7 @@ 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 ? ? + ms01 {sup2} us P = MinSUP.minsup m us ? ... | tri≈ ¬a b ¬c = record { tsup = record { sup = MinSUP.sup m ; asm = MinSUP.asm m ; 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) @@ -1096,7 +1128,7 @@ 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 ? ? + ms01 {sup2} us P = MinSUP.minsup m us ? ... | tri> ¬a ¬b px<z = record { tsup = record { sup = sp1 ; asm = MinSUP.asm sup1 ; x≤sup = ms00 ; minsup = ms01 } ; tsup=sup = sf1=sp1 px<z } where m = sup1 @@ -1104,7 +1136,7 @@ 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 ? ? + ms01 {sup2} us P = MinSUP.minsup m us ? zc41 | (case1 x<sp ) = record { supf = supf0 ; sup=u = ? ; asupf = ? ; supf-mono = ? ; supf-< = ?