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

comparison ordinal.agda @ 84:4b2aff372b7c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
omax ..
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 04 Jun 2019 23:58:58 +0900
parents 96c932d0145d
children 7494ae6b83c6
comparison
equal deleted inserted replaced
83:e013ccf00567 84:4b2aff372b7c
150 maxαd : {n : Level} → { lx : Nat } → OrdinalD {n} lx → OrdinalD lx → OrdinalD lx 150 maxαd : {n : Level} → { lx : Nat } → OrdinalD {n} lx → OrdinalD lx → OrdinalD lx
151 maxαd x y with triOrdd x y 151 maxαd x y with triOrdd x y
152 maxαd x y | tri< a ¬b ¬c = y 152 maxαd x y | tri< a ¬b ¬c = y
153 maxαd x y | tri≈ ¬a b ¬c = x 153 maxαd x y | tri≈ ¬a b ¬c = x
154 maxαd x y | tri> ¬a ¬b c = x 154 maxαd x y | tri> ¬a ¬b c = x
155
156 maxα : {n : Level} → Ordinal {n} → Ordinal → Ordinal
157 maxα x y with <-cmp (lv x) (lv y)
158 maxα x y | tri< a ¬b ¬c = x
159 maxα x y | tri> ¬a ¬b c = y
160 maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) }
161 155
162 _o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n) 156 _o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n)
163 a o≤ b = (a ≡ b) ∨ ( a o< b ) 157 a o≤ b = (a ≡ b) ∨ ( a o< b )
164 158
165 ordtrans : {n : Level} {x y z : Ordinal {n} } → x o< y → y o< z → x o< z 159 ordtrans : {n : Level} {x y z : Ordinal {n} } → x o< y → y o< z → x o< z
197 trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 refl lemma1 where 191 trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 refl lemma1 where
198 lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b) 192 lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b)
199 lemma1 (case1 x) = ¬a x 193 lemma1 (case1 x) = ¬a x
200 lemma1 (case2 x) = ≡→¬d< x 194 lemma1 (case2 x) = ≡→¬d< x
201 195
196 maxα : {n : Level} → Ordinal {n} → Ordinal → Ordinal
197 maxα x y with <-cmp (lv x) (lv y)
198 maxα x y | tri< a ¬b ¬c = x
199 maxα x y | tri> ¬a ¬b c = y
200 maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) }
201
202 omax : {n : Level} ( x y : Ordinal {suc n} ) → Ordinal {suc n}
203 omax {n} x y with <-cmp (lv x) (lv y)
204 omax {n} x y | tri< a ¬b ¬c = osuc y
205 omax {n} x y | tri> ¬a ¬b c = osuc x
206 omax {n} x y | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord y)
207 omax {n} x y | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = osuc y
208 omax {n} x y | tri≈ ¬a refl ¬c | tri≈ ¬a₁ b ¬c₁ = osuc x
209 omax {n} x y | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = osuc x
210
211 omax< : {n : Level} ( x y : Ordinal {suc n} ) → x o< y → osuc y ≡ omax x y
212 omax< {n} x y lt with <-cmp (lv x) (lv y)
213 omax< {n} x y lt | tri< a ¬b ¬c = refl
214 omax< {n} x y (case1 lt) | tri> ¬a ¬b c = ⊥-elim (¬a lt)
215 omax< {n} x y (case2 lt) | tri> ¬a ¬b c = ⊥-elim (¬b (d<→lv lt ))
216 omax< {n} x y (case1 lt) | tri≈ ¬a b ¬c = ⊥-elim (¬a lt)
217 omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord y)
218 omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = refl
219 omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( trio<≡ b lt )
220 omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim ( o<> (case2 lt) (case2 c) )
221
222 omaxx : {n : Level} ( x y : Ordinal {suc n} ) → x o< omax x y
223 omaxx {n} x y with trio< x y
224 omaxx {n} x y | tri< a ¬b ¬c = {!!}
225 omaxx {n} x y | tri> ¬a ¬b c = {!!}
226 omaxx {n} x y | tri≈ ¬a b ¬c = {!!}
227
202 OrdTrans : {n : Level} → Transitive {suc n} _o≤_ 228 OrdTrans : {n : Level} → Transitive {suc n} _o≤_
203 OrdTrans (case1 refl) (case1 refl) = case1 refl 229 OrdTrans (case1 refl) (case1 refl) = case1 refl
204 OrdTrans (case1 refl) (case2 lt2) = case2 lt2 230 OrdTrans (case1 refl) (case2 lt2) = case2 lt2
205 OrdTrans (case2 lt1) (case1 refl) = case2 lt1 231 OrdTrans (case2 lt1) (case1 refl) = case2 lt1
206 OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y) 232 OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y)