Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1045:022d2ef3f20b
is-minsup in px case done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 05 Dec 2022 00:39:14 +0900 |
| parents | d7ffe919d463 |
| children | e99e2bcb885c |
| files | src/zorn.agda |
| diffstat | 1 files changed, 16 insertions(+), 17 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sun Dec 04 11:44:59 2022 +0900 +++ b/src/zorn.agda Mon Dec 05 00:39:14 2022 +0900 @@ -397,13 +397,13 @@ subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso fc-total where fc-total : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) fc-total with trio< ua ub - ... | tri< a₁ ¬b ¬c with ≤-ftrans (order (o<→≤ sub<x) a₁ ? fca ) (s≤fc (supf ub) f mf fcb ) + ... | tri< a₁ ¬b ¬c with ≤-ftrans (order (o<→≤ sub<x) a₁ (subst (λ k → k o< z) (sym sua=ua) sua<x) fca ) (s≤fc (supf ub) f mf fcb ) ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where ct00 : * (& a) ≡ * (& b) ct00 = cong (*) eq1 ... | case2 a<b = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt) fc-total | tri≈ _ refl _ = fcn-cmp _ f mf fca fcb - fc-total | tri> ¬a ¬b c with ≤-ftrans (order (o<→≤ sua<x) c ? fcb ) (s≤fc (supf ua) f mf fca ) + fc-total | tri> ¬a ¬b c with ≤-ftrans (order (o<→≤ sua<x) c (subst (λ k → k o< z) (sym sub=ub) sub<x) fcb ) (s≤fc (supf ua) f mf fca ) ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where ct00 : * (& a) ≡ * (& b) ct00 = cong (*) (sym eq1) @@ -454,9 +454,9 @@ supf-idem {b} b≤z sfb≤x = z52 where z54 : {w : Ordinal} → odef (UnionCF A f ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b) z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc - z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order b≤z su<b ? fc where - su<b : u o< b - su<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x ) + z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order b≤z u<b (ordtrans<-≤ (subst (λ k → k o< b) (sym su=u) u<b) b≤z) fc where + u<b : u o< b + u<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x ) z52 : supf (supf b) ≡ supf b z52 = sup=u asupf sfb≤x ⟪ record { ax = asupf ; x≤sup = z54 } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ @@ -860,7 +860,8 @@ m13 spx<x = IsMinSUP.minsup (ZChain.is-minsup zc o≤-refl ) (MinSUP.as sup1) m14 where m14 : {z : Ordinal} → odef (UnionCF A f ay (ZChain.supf zc) px) z → (z ≡ sp1) ∨ (z << sp1) m14 {z} ⟪ as , ch-init fc ⟫ = ≤-ftrans (ZChain.fcy<sup zc o≤-refl fc) (sfpx≤sp1 spx<x) - m14 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = ≤-ftrans (ZChain.order zc o≤-refl u<x ? fc) (sfpx≤sp1 spx<x ) + m14 {z} ⟪ as , ch-is-sup u u<x su=u fc ⟫ = + ≤-ftrans (ZChain.order zc o≤-refl u<x (subst (λ k → k o< px) (sym (su=u)) u<x ) fc) (sfpx≤sp1 spx<x ) zc41 : ZChain A f mf< ay x zc41 = record { supf = supf1 ; sup=u = sup=u ; asupf = asupf1 ; supf-mono = supf1-mono ; order = order @@ -1051,13 +1052,8 @@ zc22 : odef A (supf1 z) zc22 = subst (λ k → odef A k ) (sym (sf1=sp1 px<z )) ( MinSUP.as sup1 ) z23 : {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ supf1 z - z23 {w} uz with zc11 (subst (λ k → odef (UnionCF A f ay supf1 k) w) z=x uz ) - ... | case1 uz = ≤-ftrans z25 (subst₂ (λ j k → j ≤ supf1 k) (sf1=sf0 o≤-refl) (sym z=x) z26 ) where - z25 : w ≤ supf0 px - z25 = IsMinSUP.x≤sup (ZChain.is-minsup zc o≤-refl ) uz - z26 : supf1 px ≤ supf1 x - z26 = ? - ... | case2 fc = subst (λ k → w ≤ k ) (sym (sf1=sp1 px<z)) ( MinSUP.x≤sup sup1 (case2 fc) ) + z23 {w} uz = subst (λ k → w ≤ k ) (sym (sf1=sp1 px<z)) ( MinSUP.x≤sup sup1 ( + zc11 (subst (λ k → odef (UnionCF A f ay supf1 k) w) z=x uz ))) z24 : {s : Ordinal } → odef A s → ( {w : Ordinal } → odef ( UnionCF A f ay supf1 z ) w → w ≤ s ) → supf1 z o≤ s z24 {s} as sup = subst (λ k → k o≤ s ) (sym (sf1=sp1 px<z)) ( MinSUP.minsup sup1 as z25 ) where @@ -1072,9 +1068,6 @@ z27 = trans (sf1=sf0 z29) ( ZChain.supf-idem zc o≤-refl z29 ) fc1 : FClosure A f (supf1 (supf0 px)) w fc1 = subst (λ k → FClosure A f k w) (sym z27) (proj1 fc) - -- x o≤ supf0 px o≤ supf0 z ≡ supf0 x ≡ sp1 - -- x o≤ supf0 px o≤ supf0 x ≡ sp1 - -- fc : FClosure A f (supf0 px) w -- ¬ ( supf0 px o< x ) → ¬ odef ( UnionCF A f ay supf1 z ) w z25 {w} (case1 ⟪ ua , ch-init fc ⟫) = sup ⟪ ua , ch-init fc ⟫ z25 {w} (case1 ⟪ ua , ch-is-sup u u<x su=u fc ⟫) = sup ⟪ ua , ch-is-sup u u<z (trans (sf1=sf0 u≤px) su=u) (fcpu fc u≤px) ⟫ where @@ -1103,6 +1096,11 @@ u≤px : u o≤ px u≤px = ordtrans u<x z≤px + order1 : {a b : Ordinal} {w : Ordinal} → + b o≤ x → a o< b → supf1 a o< x → FClosure A f (supf1 a) w → w ≤ supf1 b + order1 {a} {b} {w} b≤x a<b sa<x fc with cfcs a<b b≤x ? fc + ... | t = ? + order : {a b : Ordinal} {w : Ordinal} → b o≤ x → a o< b → supf1 a o< x → FClosure A f (supf1 a) w → w ≤ supf1 b order {a} {b} {w} b≤x a<b sa<x fc with trio< b px @@ -1110,7 +1108,8 @@ ... | tri≈ ¬a b=px ¬c = ZChain.order zc (o≤-refl0 b=px) a<b ? (fcup fc (o<→≤ (subst (λ k → a o< k) b=px a<b ))) ... | tri> ¬a ¬b px<b with trio< a px ... | tri< a<px ¬b ¬c = ≤-ftrans (ZChain.order zc o≤-refl a<px ? fc) (sfpx≤sp1 ? ) -- supf1 a ≡ supf0 a - ... | tri≈ ¬a a=px ¬c = MinSUP.x≤sup sup1 (case2 ⟪ (subst (λ k → FClosure A f (supf0 k) w) a=px fc ) , ? ⟫ ) + ... | tri≈ ¬a a=px ¬c = MinSUP.x≤sup sup1 ( + case2 ⟪ (subst (λ k → FClosure A f (supf0 k) w) a=px fc ) , subst (λ k → supf0 k o< x) a=px sa<x ⟫ ) ... | tri> ¬a ¬b px<a = ⊥-elim (¬p<x<op ⟪ px<a , zc22 ⟫ ) where -- supf1 a ≡ sp1 zc22 : a o< osuc px zc22 = subst (λ k → a o< k ) (sym (Oprev.oprev=x op)) (ordtrans<-≤ a<b b≤x)