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

comparison ordinal.agda @ 129:2a5519dcc167

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ord power set
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 02 Jul 2019 09:28:26 +0900
parents 870fe02c7a07
children c30bc9f5bd0d
comparison
equal deleted inserted replaced
128:69a845b82854 129:2a5519dcc167
214 trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 refl lemma1 where 214 trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 refl lemma1 where
215 lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b) 215 lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b)
216 lemma1 (case1 x) = ¬a x 216 lemma1 (case1 x) = ¬a x
217 lemma1 (case2 x) = ≡→¬d< x 217 lemma1 (case2 x) = ≡→¬d< x
218 218
219 maxα : {n : Level} → Ordinal {n} → Ordinal → Ordinal 219 maxα : {n : Level} → Ordinal {suc n} → Ordinal → Ordinal
220 maxα x y with <-cmp (lv x) (lv y) 220 maxα x y with trio< x y
221 maxα x y | tri< a ¬b ¬c = y 221 maxα x y | tri< a ¬b ¬c = y
222 maxα x y | tri> ¬a ¬b c = x 222 maxα x y | tri> ¬a ¬b c = x
223 maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) } 223 maxα x y | tri≈ ¬a refl ¬c = x
224 224
225 minα : {n : Level} → Ordinal {n} → Ordinal → Ordinal 225 minα : {n : Level} → Ordinal {suc n} → Ordinal → Ordinal
226 minα x y with <-cmp (lv x) (lv y) 226 minα {n} x y with trio< {n} x y
227 minα x y | tri< a ¬b ¬c = x 227 minα x y | tri< a ¬b ¬c = x
228 minα x y | tri> ¬a ¬b c = y 228 minα x y | tri> ¬a ¬b c = y
229 minα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = minαd (ord x) (ord y) } 229 minα x y | tri≈ ¬a refl ¬c = x
230
231 min1 : {n : Level} → {x y z : Ordinal {suc n} } → z o< x → z o< y → z o< minα x y
232 min1 {n} {x} {y} {z} z<x z<y with trio< {n} x y
233 min1 {n} {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
234 min1 {n} {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x
235 min1 {n} {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y
236
230 -- 237 --
231 -- max ( osuc x , osuc y ) 238 -- max ( osuc x , osuc y )
232 -- 239 --
233 240
234 omax : {n : Level} ( x y : Ordinal {suc n} ) → Ordinal {suc n} 241 omax : {n : Level} ( x y : Ordinal {suc n} ) → Ordinal {suc n}