Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/zorn.agda @ 939:187594116449
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 28 Oct 2022 19:16:34 +0900 |
| parents | 93a49ffa9183 |
| children | aee83a7f9f57 |
line wrap: on
line diff
--- a/src/zorn.agda Fri Oct 28 18:37:05 2022 +0900 +++ b/src/zorn.agda Fri Oct 28 19:16:34 2022 +0900 @@ -1474,33 +1474,22 @@ z24 = MinSUP.x<sup spd (init asc refl) z28 : supf mc o< & A z28 = z09 (ZChain.asupf zc) + -- + -- f ( f .. ( supf mc ) <= d1 + -- f d1 <= d1 + -- z25 : supf mc << d1 z25 with z24 ... | case2 lt = lt ... | case1 eq = ⊥-elim ( <-irr z29 (proj1 (cf-is-<-monotonic nmx d1 (MinSUP.asm spd)) ) ) where -- supf mc ≡ d1 - z27 : odef (ZChain.chain zc) (cf nmx d1) - z27 = ZChain.f-next zc (subst (λ k → odef (ZChain.chain zc) k ) eq (ZChain.csupf zc z28)) - z31 : {z w : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z - → (* w ≡ * z) ∨ (* w < * z) - → (* w ≡ * d1) ∨ (* w < * d1) - z31 {z} uz (case1 w=z) with MinSUP.x<sup spd uz - ... | case1 eq = case1 (trans w=z (cong (*) eq) ) - ... | case2 lt = case2 (subst (λ k → k < * d1 ) (sym w=z) lt ) - z31 {z} {w} uz (case2 w<z) with MinSUP.x<sup spd uz - ... | case1 eq = case2 (subst (λ k → * w < k ) (cong (*) eq) w<z ) - ... | case2 lt = case2 ( IsStrictPartialOrder.trans PO w<z lt) + z32 : ((cf nmx (supf mc)) ≡ d1) ∨ ( (cf nmx (supf mc)) << d1 ) + z32 = MinSUP.x<sup spd (fsuc _ (init asc refl)) z29 : (* (cf nmx d1) ≡ * d1) ∨ (* (cf nmx d1) < * d1) - z29 with z27 - ... | ⟪ aa , ch-init fc ⟫ = ? where - z30 : FClosure A (cf nmx) (& s) (cf nmx d1) - z30 = fc - ... | ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ with trio< u (supf mc) -- u<x : supf u o< supf (& A) - ... | tri< a ¬b ¬c = ? -- u o< supf mc - ... | tri> ¬a ¬b c = ? -- supf mc o< u - ... | tri≈ ¬a b ¬c with MinSUP.x<sup spd ( subst₂ (λ j k → FClosure A (cf nmx) j k ) (trans (ChainP.supu=u is-sup) b) refl fc ) - ... | case1 eq = case1 (cong (*) eq) - ... | case2 lt = case2 lt + z29 with z32 + ... | case1 eq1 = case1 (cong (*) (trans (cong (cf nmx) (sym eq)) eq1) ) + ... | case2 lt = case2 (subst (λ k → * k < * d1 ) (cong (cf nmx) eq) lt) + sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d sc<sd {mc} {d} sc<<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) ) ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) (sym eq) )) sc<<sd )