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

comparison src/zorn1.agda @ 933:409ac0af7b3b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 24 Oct 2022 09:15:49 +0900
parents b1899e33e2c7
children
comparison
equal deleted inserted replaced
932:b1899e33e2c7 933:409ac0af7b3b
733 -- z25 (fsuc x lt) = ? -- cf (sup c) 733 -- z25 (fsuc x lt) = ? -- cf (sup c)
734 734
735 sd=d : supf d ≡ d 735 sd=d : supf d ≡ d
736 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫ 736 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫
737 737
738 sc<<sd : supf mc << supf d 738 sc<<d : {mc : Ordinal } → {asc : odef A (supf mc)} → (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ))
739 sc<<sd = ? 739 → supf mc << MinSUP.sup spd
740 sc<<d {mc} {asc} spd = z25 where
741 d1 : Ordinal
742 d1 = MinSUP.sup spd
743 z24 : (supf mc ≡ d1) ∨ ( supf mc << d1 )
744 z24 = MinSUP.x<sup spd (init asc refl)
745 z25 : supf mc << d1
746 z25 with z24
747 ... | case2 lt = lt
748 ... | case1 eq = ?
740 749
741 sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d 750 sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d
742 sc<sd {mc} {d} sc<<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) ) 751 sc<sd {mc} {d} sc<<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) )
743 ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) (sym eq) )) sc<<sd ) 752 ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) (sym eq) )) sc<<sd )
744 ... | case2 lt = lt 753 ... | case2 lt = lt
745 754
746 sms<sa : supf mc o< supf (& A) 755 sms<sa : supf mc o< supf (& A)
747 sms<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫) )) 756 sms<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫) ))
748 ... | case2 lt = lt 757 ... | case2 lt = lt
749 ... | case1 eq = ⊥-elim ( o<¬≡ eq ( ordtrans<-≤ (sc<sd sc<<sd ) ( ZChain.supf-mono zc (o<→≤ d<A )))) 758 ... | case1 eq = ⊥-elim ( o<¬≡ eq ( ordtrans<-≤ (sc<sd (subst (λ k → supf mc << k ) (sym sd=d) (sc<<d {mc} {asc} spd)) )
759 ( ZChain.supf-mono zc (o<→≤ d<A ))))
750 760
751 ss<sa : supf c o< supf (& A) 761 ss<sa : supf c o< supf (& A)
752 ss<sa = subst (λ k → supf k o< supf (& A)) (sym c=mc) sms<sa 762 ss<sa = subst (λ k → supf k o< supf (& A)) (sym c=mc) sms<sa
753 763
754 zorn00 : Maximal A 764 zorn00 : Maximal A