Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/zorn.agda @ 951:86a2bfb7222e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
supf mc = mc
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 01 Nov 2022 11:57:52 +0900
parents 6e126013f056
children 05f54e16f138
comparison
equal deleted inserted replaced
950:6e126013f056 951:86a2bfb7222e
76 <-ftrans : {x y z : Ordinal } → x <= y → y <= z → x <= z 76 <-ftrans : {x y z : Ordinal } → x <= y → y <= z → x <= z
77 <-ftrans {x} {y} {z} (case1 refl ) (case1 refl ) = case1 refl 77 <-ftrans {x} {y} {z} (case1 refl ) (case1 refl ) = case1 refl
78 <-ftrans {x} {y} {z} (case1 refl ) (case2 y<z) = case2 y<z 78 <-ftrans {x} {y} {z} (case1 refl ) (case2 y<z) = case2 y<z
79 <-ftrans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y 79 <-ftrans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y
80 <-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z ) 80 <-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z )
81
82 ftrans<=-< : {x y z : Ordinal } → x <= y → y << z → x << z
83 ftrans<=-< {x} {y} {z} (case1 eq) y<z = subst (λ k → k < * z) ? y<z
84 ftrans<=-< {x} {y} {z} (case2 lt) y<z = IsStrictPartialOrder.trans PO lt y<z
81 85
82 <=to≤ : {x y : Ordinal } → x <= y → * x ≤ * y 86 <=to≤ : {x y : Ordinal } → x <= y → * x ≤ * y
83 <=to≤ (case1 eq) = case1 (cong (*) eq) 87 <=to≤ (case1 eq) = case1 (cong (*) eq)
84 <=to≤ (case2 lt) = case2 lt 88 <=to≤ (case2 lt) = case2 lt
85 89
1499 sc=c : supf mc ≡ mc 1503 sc=c : supf mc ≡ mc
1500 sc=c = ZChain.sup=u zc (MinSUP.asm msp1) (o<→≤ (∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ )) ⟪ is-sup , not-hasprev ⟫ where 1504 sc=c = ZChain.sup=u zc (MinSUP.asm msp1) (o<→≤ (∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫ )) ⟪ is-sup , not-hasprev ⟫ where
1501 is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (MinSUP.asm msp1) 1505 is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) (MinSUP.asm msp1)
1502 is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy )} 1506 is-sup = record { x≤sup = λ zy → MinSUP.x≤sup msp1 (chain-mono (cf nmx) (cf-is-≤-monotonic nmx) as0 supf (ZChain.supf-mono zc) (o<→≤ mc<A) zy )}
1503 not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) mc (cf nmx) 1507 not-hasprev : ¬ HasPrev A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) mc) mc (cf nmx)
1504 not-hasprev hp = <-irr z26 z30 where 1508 not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-init fc ⟫ ; x=fy = x=fy } = ?
1509 not-hasprev record { ax = ax ; y = y ; ay = ⟪ ua1 , ch-is-sup u u<x is-sup1 fc ⟫; x=fy = x=fy } = ⊥-elim ( <-irr z48 z32 ) where
1505 z30 : * mc < * (cf nmx mc) 1510 z30 : * mc < * (cf nmx mc)
1506 z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1)) 1511 z30 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1))
1507 z26 : (* (cf nmx mc) ≡ * mc) ∨ (* (cf nmx mc) < * mc) 1512 z31 : ( supf mc ≡ mc ) ∨ ( * (supf mc) < * mc )
1508 z26 = ? 1513 z31 = MinSUP.x≤sup msp1 (ZChain.csupf zc (z09 (ZChain.asupf zc) ))
1514 z32 : * (supf mc) < * (cf nmx (cf nmx y))
1515 z32 = ftrans<=-< z31 (subst (λ k → * mc < * k ) (cong (cf nmx) x=fy) z30 )
1516 z48 : ( * (cf nmx (cf nmx y)) ≡ * (supf mc)) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) )
1517 z48 = <=to≤ (ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A u<x (fsuc _ ( fsuc _ fc )))
1509 1518
1510 is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd) 1519 is-sup : IsSup A (UnionCF A (cf nmx) (cf-is-≤-monotonic nmx) as0 (ZChain.supf zc) d) (MinSUP.asm spd)
1511 is-sup = record { x≤sup = z22 } where 1520 is-sup = record { x≤sup = z22 } where
1512 z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd) 1521 z23 : {z : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc) z → (z ≡ MinSUP.sup spd) ∨ (z << MinSUP.sup spd)
1513 z23 lt = MinSUP.x≤sup spd lt 1522 z23 lt = MinSUP.x≤sup spd lt
1540 z51 = ? where 1549 z51 = ? where
1541 z56 : u ≡ mc → supf u ≡ supf mc 1550 z56 : u ≡ mc → supf u ≡ supf mc
1542 z56 eq = cong supf eq 1551 z56 eq = cong supf eq
1543 z57 : u << mc → supf u o≤ supf mc 1552 z57 : u << mc → supf u o≤ supf mc
1544 z57 lt = ZChain.supf-<= zc (case2 z58) where 1553 z57 lt = ZChain.supf-<= zc (case2 z58) where
1545 z58 : supf u << supf mc -- supf u o< supf d 1554 z58 : supf u << supf mc -- supf u o< supf d -- supf u << supf d
1546 z58 = ? 1555 z58 = subst₂ ( λ j k → j << k ) (sym (ChainP.supu=u is-sup1)) (sym sc=c) lt
1547 z59 : supf mc o< supf u → ⊥ → supf mc << supf u
1548 z59 lt = ?
1549 -- --with z52
1550 -- ... | case1 eq = ?
1551 -- ... | case2 lt = ? -- ZChain.supf-<= zc (case2 ? )
1552 z49 : supf u o< supf mc → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) 1556 z49 : supf u o< supf mc → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) )
1553 z49 su<smc = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A su<smc (fsuc _ ( fsuc _ fc )) 1557 z49 su<smc = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) mc<A su<smc (fsuc _ ( fsuc _ fc ))
1554 z50 : (cf nmx (cf nmx y) ≡ supf d) ∨ (* (cf nmx (cf nmx y)) < * (supf d) ) 1558 z50 : (cf nmx (cf nmx y) ≡ supf d) ∨ (* (cf nmx (cf nmx y)) < * (supf d) )
1555 z50 = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) d<A u<x (fsuc _ ( fsuc _ fc )) 1559 z50 = ZChain1.order (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc (& A)) d<A u<x (fsuc _ ( fsuc _ fc ))
1556 z47 : {mc d1 : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) 1560 z47 : {mc d1 : Ordinal } {asc : odef A (supf mc)} (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ))
1557 → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) 1561 → (cf nmx (cf nmx y) ≡ supf mc) ∨ (* (cf nmx (cf nmx y)) < * (supf mc) ) → supf mc << d1
1558 → supf mc << d1
1559 → * (cf nmx (cf nmx y)) < * d1 1562 → * (cf nmx (cf nmx y)) < * d1
1560 z47 {mc} {d1} {asc} spd (case1 eq) smc<d = subst (λ k → k < * d1 ) (sym (cong (*) eq)) smc<d 1563 z47 {mc} {d1} {asc} spd (case1 eq) smc<d = subst (λ k → k < * d1 ) (sym (cong (*) eq)) smc<d
1561 z47 {mc} {d1} {asc} spd (case2 lt) smc<d = IsStrictPartialOrder.trans PO lt smc<d 1564 z47 {mc} {d1} {asc} spd (case2 lt) smc<d = IsStrictPartialOrder.trans PO lt smc<d
1562 z30 : * d < * (cf nmx d) 1565 z30 : * d < * (cf nmx d)
1563 z30 = proj1 (cf-is-<-monotonic nmx d (MinSUP.asm spd)) 1566 z30 = proj1 (cf-is-<-monotonic nmx d (MinSUP.asm spd))
1585 1588
1586 sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d 1589 sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d
1587 sc<sd {mc} {d} sc<<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) ) 1590 sc<sd {mc} {d} sc<<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) )
1588 ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) (sym eq) )) sc<<sd ) 1591 ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) (sym eq) )) sc<<sd )
1589 ... | case2 lt = lt 1592 ... | case2 lt = lt
1593
1594 ¬sms=sa : ¬ ( supf mc ≡ supf (& A)) -- → supf mc ≡ supf d ≡ supf (& A), supf mc << d
1595 ¬sms=sa = ?
1590 1596
1591 sms<sa : supf mc o< supf (& A) 1597 sms<sa : supf mc o< supf (& A)
1592 sms<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫) )) 1598 sms<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫) ))
1593 ... | case2 lt = lt 1599 ... | case2 lt = lt
1594 ... | case1 eq = ⊥-elim ( o<¬≡ eq ( ordtrans<-≤ (sc<sd (subst (λ k → supf mc << k ) (sym sd=d) (sc<<d {mc} asc spd)) ) 1600 ... | case1 eq = ⊥-elim ( o<¬≡ eq ( ordtrans<-≤ (sc<sd (subst (λ k → supf mc << k ) (sym sd=d) (sc<<d {mc} asc spd)) )