Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 778:6aafa22c951a
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 28 Jul 2022 10:01:43 +0900 |
parents | fa765e37d7f9 |
children | 9e34893d9a03 |
files | src/zorn.agda |
diffstat | 1 files changed, 44 insertions(+), 28 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Thu Jul 28 09:10:36 2022 +0900 +++ b/src/zorn.agda Thu Jul 28 10:01:43 2022 +0900 @@ -758,40 +758,56 @@ usup = supP pchain0 (λ lt → proj1 lt) ptotal0 spu = & (SUP.sup usup) + record Usupf ( w : Ordinal ) : Set n where + field + supf : Ordinal → Ordinal + uniq-supf : {z w1 : Ordinal } → z o< w1 → (w<x : w o< x) → (w1<w : w1 o< w) + → supf z ≡ ZChain.supf (prev w1 (ordtrans w1<w w<x )) z + + US : (w1 : Ordinal) → w1 o< x → Usupf w1 + US w1 w1<x = TransFinite0 uind w1 where + uind : (w : Ordinal) → ((z : Ordinal) → z o< w → Usupf z ) → Usupf w + uind w uprev with Oprev-p x + ... | yes op = record { supf = ? ; uniq-supf = ? } where + px = Oprev.oprev op + zc : ZChain A f mf ay (Oprev.oprev op) + zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) + supf : Ordinal → Ordinal + supf z with trio< z w + ... | tri< a ¬b ¬c = ZChain.supf (prev _ ?) z + ... | tri≈ ¬a b ¬c = ZChain.supf zc z + ... | tri> ¬a ¬b c = ZChain.supf zc z + us : {z : Ordinal } → z o< w → (w<x : w o< x) → supf z ≡ ZChain.supf (prev _ w<x) z + us {z} z<w w<x with trio< z w + ... | tri< a ¬b ¬c = u01 where + u02 : ? ≡ Usupf.supf (uprev z a) z + u02 = ? + u01 : ZChain.supf (prev ? ?) z ≡ ZChain.supf (prev w w<x) z + u01 = ? -- subst (λ k → k ≡ _ ) ? ( Usupf.uniq-supf (uprev _ ?) ? ? ) + ... | tri≈ ¬a b ¬c = ? + ... | tri> ¬a ¬b c = ? + ... | no wlim = record { supf = supf ; uniq-supf = ? } where + supf : Ordinal → Ordinal + supf z with trio< (osuc z) w + ... | tri< a ¬b ¬c = Usupf.supf ( uprev (osuc z) a ) z + ... | tri≈ ¬a b ¬c = spu + ... | tri> ¬a ¬b c = spu + us : {z : Ordinal} {w2 : Ordinal} → z o< w2 + → (w<x : w o< x) (w2<w : w2 o< w) → supf z ≡ ZChain.supf (prev w2 (ordtrans w2<w w<x)) z + us {z} {w2} z<w2 w<x w2<w with trio< (osuc z) w + ... | tri< a ¬b ¬c = ? where + u00 = Usupf.uniq-supf (uprev (osuc z) ?) ? ? ? + u01 = Usupf.uniq-supf (uprev w2 ?) ? ? ? + ... | tri≈ ¬a b ¬c = ? + ... | tri> ¬a ¬b c = ? + + psupf : Ordinal → Ordinal psupf z with trio< z x ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z ... | tri≈ ¬a b ¬c = spu -- ^^ this z dependcy have to be removed ... | tri> ¬a ¬b c = spu ---- ∀ z o< x , max (supf (pzc (osuc z) (ob<x lim a))) - record Usupf ( w : Ordinal ) : Set n where - field - uniq-supf : {z : Ordinal } → (z<w : z o< w) → (w<x : w o< x) - → ZChain.supf (pzc (osuc z) (ob<x lim (ordtrans z<w w<x))) z - ≡ ZChain.supf (pzc (osuc w) (ob<x lim w<x)) z - - US : (w1 : Ordinal) → w1 o< x → Usupf w1 - US w1 w1<x = TransFinite0 uind w1 where - uind : (w : Ordinal) → ((z : Ordinal) → z o< w → Usupf z ) → Usupf w - uind w uprev = record { uniq-supf = u00 } where - u01 : {z w : Ordinal } → (z<w : z o< w) → (w<x : w o< x) - → ZChain.supf (pzc w ?) z - ≡ ZChain.supf (pzc (osuc w) (ob<x lim w<x)) z - u01 = ? - u00 : {z : Ordinal } → (z<w : z o< w) → (w<x : w o< x) - → ZChain.supf (pzc (osuc z) (ob<x lim (ordtrans z<w w<x))) z - ≡ ZChain.supf (pzc (osuc w) (ob<x lim w<x)) z - u00 {z} z<w w<x with Oprev-p w - ... | yes op with osuc-≡< ( subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<w ) - ... | case1 z=pw = ? - ... | case2 z<pw = ? - u00 {z} z<w w<x | no lim = ? where -- trans (Usupf.uniq-supf (uprev _ ?) ? ? ) (u01 ? ?) where - us : {z : Ordinal } → z o< w → (w<x : w o< x) → ? - us {z} z<w w<x with trio< z w - ... | tri< a ¬b ¬c = ? - ... | tri≈ ¬a b ¬c = ? - ... | tri> ¬a ¬b c = ? - psupf<z : {z : Ordinal } → ( a : z o< x ) → psupf z ≡ ZChain.supf (pzc (osuc z) (ob<x lim a)) z psupf<z {z} z<x with trio< z x ... | tri< a ¬b ¬c = cong (λ k → ZChain.supf (pzc (osuc z) (ob<x lim k)) z) ( o<-irr _ _ )