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

comparison src/zorn.agda @ 777:fa765e37d7f9

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 Thu, 28 Jul 2022 09:10:36 +0900
parents 13d50db96684
children 6aafa22c951a
comparison
equal deleted inserted replaced
776:13d50db96684 777:fa765e37d7f9
762 psupf z with trio< z x 762 psupf z with trio< z x
763 ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z 763 ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
764 ... | tri≈ ¬a b ¬c = spu -- ^^ this z dependcy have to be removed 764 ... | tri≈ ¬a b ¬c = spu -- ^^ this z dependcy have to be removed
765 ... | tri> ¬a ¬b c = spu ---- ∀ z o< x , max (supf (pzc (osuc z) (ob<x lim a))) 765 ... | tri> ¬a ¬b c = spu ---- ∀ z o< x , max (supf (pzc (osuc z) (ob<x lim a)))
766 766
767 record Usupf ( w : Ordinal ) : Set n where
768 field
769 uniq-supf : {z : Ordinal } → (z<w : z o< w) → (w<x : w o< x)
770 → ZChain.supf (pzc (osuc z) (ob<x lim (ordtrans z<w w<x))) z
771 ≡ ZChain.supf (pzc (osuc w) (ob<x lim w<x)) z
772
773 US : (w1 : Ordinal) → w1 o< x → Usupf w1
774 US w1 w1<x = TransFinite0 uind w1 where
775 uind : (w : Ordinal) → ((z : Ordinal) → z o< w → Usupf z ) → Usupf w
776 uind w uprev = record { uniq-supf = u00 } where
777 u01 : {z w : Ordinal } → (z<w : z o< w) → (w<x : w o< x)
778 → ZChain.supf (pzc w ?) z
779 ≡ ZChain.supf (pzc (osuc w) (ob<x lim w<x)) z
780 u01 = ?
781 u00 : {z : Ordinal } → (z<w : z o< w) → (w<x : w o< x)
782 → ZChain.supf (pzc (osuc z) (ob<x lim (ordtrans z<w w<x))) z
783 ≡ ZChain.supf (pzc (osuc w) (ob<x lim w<x)) z
784 u00 {z} z<w w<x with Oprev-p w
785 ... | yes op with osuc-≡< ( subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<w )
786 ... | case1 z=pw = ?
787 ... | case2 z<pw = ?
788 u00 {z} z<w w<x | no lim = ? where -- trans (Usupf.uniq-supf (uprev _ ?) ? ? ) (u01 ? ?) where
789 us : {z : Ordinal } → z o< w → (w<x : w o< x) → ?
790 us {z} z<w w<x with trio< z w
791 ... | tri< a ¬b ¬c = ?
792 ... | tri≈ ¬a b ¬c = ?
793 ... | tri> ¬a ¬b c = ?
794
767 psupf<z : {z : Ordinal } → ( a : z o< x ) → psupf z ≡ ZChain.supf (pzc (osuc z) (ob<x lim a)) z 795 psupf<z : {z : Ordinal } → ( a : z o< x ) → psupf z ≡ ZChain.supf (pzc (osuc z) (ob<x lim a)) z
768 psupf<z {z} z<x with trio< z x 796 psupf<z {z} z<x with trio< z x
769 ... | tri< a ¬b ¬c = cong (λ k → ZChain.supf (pzc (osuc z) (ob<x lim k)) z) ( o<-irr _ _ ) 797 ... | tri< a ¬b ¬c = cong (λ k → ZChain.supf (pzc (osuc z) (ob<x lim k)) z) ( o<-irr _ _ )
770 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a z<x) 798 ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a z<x)
771 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a z<x) 799 ... | tri> ¬a ¬b c = ⊥-elim ( ¬a z<x)