Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff cardinal.agda @ 227:a4cdfc84f65f
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 11 Aug 2019 18:37:33 +0900 |
parents | 176ff97547b4 |
children | 49736efc822b |
line wrap: on
line diff
--- a/cardinal.agda Sun Aug 11 13:05:17 2019 +0900 +++ b/cardinal.agda Sun Aug 11 18:37:33 2019 +0900 @@ -48,6 +48,34 @@ lemma y | case1 refl = _⊗_.π2 lt lemma y | case2 not = o∅ +-- contra position of sup-o< +-- + +record Sup ( ψ : Ordinal → Ordinal ) : Set n where + field + sup-x : Ordinal + sup-lb : {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ sup-x ) + +sup-o> : ( ψ : Ordinal → Ordinal ) → Sup ψ +sup-o> ψ = record { + sup-x = od→ord ( minimul (Ord (osuc (sup-o ψ))) lemma ) + ; sup-lb = λ {z} z<sψ → lemma1 z<sψ + } where + lemma0 : {x : Ordinal} → o∅ o< osuc x + lemma0 {x} with trio< o∅ (osuc x) + lemma0 {x} | tri< a ¬b ¬c = a + lemma0 {x} | tri≈ ¬a refl ¬c = ⊥-elim (¬x<0 <-osuc ) + lemma0 {x} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c) + lemma : ¬ (Ord (osuc (sup-o ψ)) == od∅) + lemma record { eq→ = eq→ ; eq← = eq← } = ¬x<0 {o∅} ( eq→ lemma0 ) + lemma1 : {z : Ordinal} → z o< sup-o ψ → z o< osuc (ψ (od→ord (minimul (Ord (osuc (sup-o ψ))) lemma))) + lemma1 {z} lt with trio< z (ψ (od→ord (minimul (Ord (osuc (sup-o ψ))) lemma))) + lemma1 {z} lt | tri< a ¬b ¬c = ordtrans a <-osuc + lemma1 {z} lt | tri≈ ¬a refl ¬c = <-osuc + lemma1 {z} lt | tri> ¬a ¬b c = ⊥-elim (o<> c lemma2 ) where + lemma2 : z o< ψ (od→ord (minimul (Ord (osuc (sup-o ψ))) lemma)) + lemma2 = ordtrans sup-o< ( o<-subst (x∋minimul (Ord (osuc (sup-o ψ))) lemma ) ? ?) + ------------ -- -- Onto map