|
431
|
1 open import Level
|
|
|
2 open import Ordinals
|
|
|
3 module OrdUtil {n : Level} (O : Ordinals {n} ) where
|
|
|
4
|
|
|
5 open import logic
|
|
|
6 open import nat
|
|
|
7 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
|
|
|
8 open import Data.Empty
|
|
|
9 open import Relation.Binary.PropositionalEquality
|
|
|
10 open import Relation.Nullary
|
|
|
11 open import Relation.Binary hiding (_⇔_)
|
|
|
12
|
|
|
13 open Ordinals.Ordinals O
|
|
|
14 open Ordinals.IsOrdinals isOrdinal
|
|
|
15 open Ordinals.IsNext isNext
|
|
|
16
|
|
|
17 o<-dom : { x y : Ordinal } → x o< y → Ordinal
|
|
|
18 o<-dom {x} _ = x
|
|
|
19
|
|
|
20 o<-cod : { x y : Ordinal } → x o< y → Ordinal
|
|
|
21 o<-cod {_} {y} _ = y
|
|
|
22
|
|
|
23 o<-subst : {Z X z x : Ordinal } → Z o< X → Z ≡ z → X ≡ x → z o< x
|
|
|
24 o<-subst df refl refl = df
|
|
|
25
|
|
|
26 o<¬≡ : { ox oy : Ordinal } → ox ≡ oy → ox o< oy → ⊥
|
|
|
27 o<¬≡ {ox} {oy} eq lt with trio< ox oy
|
|
|
28 o<¬≡ {ox} {oy} eq lt | tri< a ¬b ¬c = ¬b eq
|
|
|
29 o<¬≡ {ox} {oy} eq lt | tri≈ ¬a b ¬c = ¬a lt
|
|
|
30 o<¬≡ {ox} {oy} eq lt | tri> ¬a ¬b c = ¬b eq
|
|
|
31
|
|
|
32 o<> : {x y : Ordinal } → y o< x → x o< y → ⊥
|
|
|
33 o<> {ox} {oy} lt tl with trio< ox oy
|
|
|
34 o<> {ox} {oy} lt tl | tri< a ¬b ¬c = ¬c lt
|
|
|
35 o<> {ox} {oy} lt tl | tri≈ ¬a b ¬c = ¬a tl
|
|
|
36 o<> {ox} {oy} lt tl | tri> ¬a ¬b c = ¬a tl
|
|
|
37
|
|
|
38 osuc-< : { x y : Ordinal } → y o< osuc x → x o< y → ⊥
|
|
|
39 osuc-< {x} {y} y<ox x<y with osuc-≡< y<ox
|
|
|
40 osuc-< {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y
|
|
|
41 osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x
|
|
|
42
|
|
712
|
43 open _∧_
|
|
|
44
|
|
|
45 ¬p<x<op : { p b : Ordinal } → ¬ ( (p o< b ) ∧ (b o< osuc p ) )
|
|
|
46 ¬p<x<op {p} {b} P with osuc-≡< (proj2 P)
|
|
|
47 ... | case1 eq = o<¬≡ (sym eq) (proj1 P)
|
|
|
48 ... | case2 lt = o<> lt (proj1 P)
|
|
|
49
|
|
431
|
50 osucc : {ox oy : Ordinal } → oy o< ox → osuc oy o< osuc ox
|
|
|
51 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox
|
|
|
52 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc
|
|
|
53 osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc
|
|
|
54 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c with osuc-≡< c
|
|
|
55 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy<ox)
|
|
|
56 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy<ox)
|
|
|
57
|
|
|
58 osucprev : {ox oy : Ordinal } → osuc oy o< osuc ox → oy o< ox
|
|
|
59 osucprev {ox} {oy} oy<ox with trio< oy ox
|
|
|
60 osucprev {ox} {oy} oy<ox | tri< a ¬b ¬c = a
|
|
|
61 osucprev {ox} {oy} oy<ox | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (cong (λ k → osuc k) b) oy<ox )
|
|
|
62 osucprev {ox} {oy} oy<ox | tri> ¬a ¬b c = ⊥-elim (o<> (osucc c) oy<ox )
|
|
|
63
|
|
653
|
64 ordtrans≤-< : {ox oy oz : Ordinal } → ox o< osuc oy → oy o< oz → ox o< oz
|
|
|
65 ordtrans≤-< {ox} {oy} {oz} x≤y y<z with osuc-≡< x≤y
|
|
|
66 ... | case1 x=y = subst ( λ k → k o< oz ) (sym x=y) y<z
|
|
|
67 ... | case2 x<y = ordtrans x<y y<z
|
|
|
68
|
|
431
|
69 open _∧_
|
|
|
70
|
|
|
71 osuc2 : ( x y : Ordinal ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
|
|
|
72 proj2 (osuc2 x y) lt = osucc lt
|
|
|
73 proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy
|
|
|
74 proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy
|
|
|
75 proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy
|
|
|
76
|
|
538
|
77 o≡? : (x y : Ordinal) → Dec ( x ≡ y )
|
|
|
78 o≡? x y with trio< x y
|
|
|
79 ... | tri< a ¬b ¬c = no ¬b
|
|
|
80 ... | tri≈ ¬a b ¬c = yes b
|
|
|
81 ... | tri> ¬a ¬b c = no ¬b
|
|
|
82
|
|
431
|
83 _o≤_ : Ordinal → Ordinal → Set n
|
|
|
84 a o≤ b = a o< osuc b -- (a ≡ b) ∨ ( a o< b )
|
|
|
85
|
|
653
|
86 o<→≤ : {a b : Ordinal} → a o< b → a o≤ b
|
|
|
87 o<→≤ {a} {b} lt with trio< a (osuc b)
|
|
|
88 ... | tri< a₁ ¬b ¬c = a₁
|
|
|
89 ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a (ordtrans lt <-osuc ) )
|
|
|
90 ... | tri> ¬a ¬b c = ⊥-elim (¬a (ordtrans lt <-osuc ) )
|
|
|
91
|
|
611
|
92 -- o<-irr : { x y : Ordinal } → { lt lt1 : x o< y } → lt ≡ lt1
|
|
431
|
93
|
|
|
94 xo<ab : {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa → ox o< ob ) → oa o< osuc ob
|
|
|
95 xo<ab {oa} {ob} a→b with trio< oa ob
|
|
|
96 xo<ab {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc
|
|
|
97 xo<ab {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc
|
|
|
98 xo<ab {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c ) )
|
|
|
99
|
|
|
100 maxα : Ordinal → Ordinal → Ordinal
|
|
|
101 maxα x y with trio< x y
|
|
|
102 maxα x y | tri< a ¬b ¬c = y
|
|
|
103 maxα x y | tri> ¬a ¬b c = x
|
|
|
104 maxα x y | tri≈ ¬a refl ¬c = x
|
|
|
105
|
|
|
106 omin : Ordinal → Ordinal → Ordinal
|
|
|
107 omin x y with trio< x y
|
|
|
108 omin x y | tri< a ¬b ¬c = x
|
|
|
109 omin x y | tri> ¬a ¬b c = y
|
|
|
110 omin x y | tri≈ ¬a refl ¬c = x
|
|
|
111
|
|
|
112 min1 : {x y z : Ordinal } → z o< x → z o< y → z o< omin x y
|
|
|
113 min1 {x} {y} {z} z<x z<y with trio< x y
|
|
|
114 min1 {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
|
|
|
115 min1 {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x
|
|
|
116 min1 {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y
|
|
|
117
|
|
|
118 --
|
|
|
119 -- max ( osuc x , osuc y )
|
|
|
120 --
|
|
|
121
|
|
|
122 omax : ( x y : Ordinal ) → Ordinal
|
|
|
123 omax x y with trio< x y
|
|
|
124 omax x y | tri< a ¬b ¬c = osuc y
|
|
|
125 omax x y | tri> ¬a ¬b c = osuc x
|
|
|
126 omax x y | tri≈ ¬a refl ¬c = osuc x
|
|
|
127
|
|
|
128 omax< : ( x y : Ordinal ) → x o< y → osuc y ≡ omax x y
|
|
|
129 omax< x y lt with trio< x y
|
|
|
130 omax< x y lt | tri< a ¬b ¬c = refl
|
|
|
131 omax< x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt )
|
|
|
132 omax< x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt )
|
|
|
133
|
|
|
134 omax≤ : ( x y : Ordinal ) → x o≤ y → osuc y ≡ omax x y
|
|
|
135 omax≤ x y le with trio< x y
|
|
|
136 omax≤ x y le | tri< a ¬b ¬c = refl
|
|
|
137 omax≤ x y le | tri≈ ¬a refl ¬c = refl
|
|
|
138 omax≤ x y le | tri> ¬a ¬b c with osuc-≡< le
|
|
|
139 omax≤ x y le | tri> ¬a ¬b c | case1 eq = ⊥-elim (¬b eq)
|
|
|
140 omax≤ x y le | tri> ¬a ¬b c | case2 x<y = ⊥-elim (¬a x<y)
|
|
|
141
|
|
|
142 omax≡ : ( x y : Ordinal ) → x ≡ y → osuc y ≡ omax x y
|
|
|
143 omax≡ x y eq with trio< x y
|
|
|
144 omax≡ x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq )
|
|
|
145 omax≡ x y eq | tri≈ ¬a refl ¬c = refl
|
|
|
146 omax≡ x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq )
|
|
|
147
|
|
|
148 omax-x : ( x y : Ordinal ) → x o< omax x y
|
|
|
149 omax-x x y with trio< x y
|
|
|
150 omax-x x y | tri< a ¬b ¬c = ordtrans a <-osuc
|
|
|
151 omax-x x y | tri> ¬a ¬b c = <-osuc
|
|
|
152 omax-x x y | tri≈ ¬a refl ¬c = <-osuc
|
|
|
153
|
|
|
154 omax-y : ( x y : Ordinal ) → y o< omax x y
|
|
|
155 omax-y x y with trio< x y
|
|
|
156 omax-y x y | tri< a ¬b ¬c = <-osuc
|
|
|
157 omax-y x y | tri> ¬a ¬b c = ordtrans c <-osuc
|
|
|
158 omax-y x y | tri≈ ¬a refl ¬c = <-osuc
|
|
|
159
|
|
|
160 omxx : ( x : Ordinal ) → omax x x ≡ osuc x
|
|
|
161 omxx x with trio< x x
|
|
|
162 omxx x | tri< a ¬b ¬c = ⊥-elim (¬b refl )
|
|
|
163 omxx x | tri> ¬a ¬b c = ⊥-elim (¬b refl )
|
|
|
164 omxx x | tri≈ ¬a refl ¬c = refl
|
|
|
165
|
|
|
166 omxxx : ( x : Ordinal ) → omax x (omax x x ) ≡ osuc (osuc x)
|
|
|
167 omxxx x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc ))
|
|
|
168
|
|
|
169 open _∧_
|
|
|
170
|
|
625
|
171 o≤-refl0 : { i j : Ordinal } → i ≡ j → i o≤ j
|
|
|
172 o≤-refl0 {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc
|
|
|
173
|
|
|
174 o≤-refl : { i : Ordinal } → i o≤ i
|
|
|
175 o≤-refl {i} = subst (λ k → i o< osuc k ) refl <-osuc
|
|
|
176
|
|
674
|
177 o≤? : (x y : Ordinal) → Dec ( x o≤ y )
|
|
|
178 o≤? x y with trio< x y
|
|
|
179 ... | tri< a ¬b ¬c = yes (ordtrans a <-osuc)
|
|
|
180 ... | tri≈ ¬a b ¬c = yes (o≤-refl0 b)
|
|
|
181 ... | tri> ¬a ¬b c = no (λ n → osuc-< n c )
|
|
|
182
|
|
683
|
183 o¬≤→< : {x z : Ordinal} → ¬ (x o< osuc z) → z o< x
|
|
|
184 o¬≤→< {x} {z} not with trio< z x
|
|
|
185 ... | tri< a ¬b ¬c = a
|
|
|
186 ... | tri≈ ¬a b ¬c = ⊥-elim (not (o≤-refl0 (sym b)))
|
|
|
187 ... | tri> ¬a ¬b c = ⊥-elim (not (o<→≤ c ))
|
|
|
188
|
|
431
|
189 OrdTrans : Transitive _o≤_
|
|
|
190 OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c
|
|
|
191 OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc
|
|
|
192 OrdTrans a≤b b≤c | case1 refl | case2 a≤c = ordtrans a≤c <-osuc
|
|
|
193 OrdTrans a≤b b≤c | case2 a≤c | case1 refl = ordtrans a≤c <-osuc
|
|
|
194 OrdTrans a≤b b≤c | case2 a<b | case2 b<c = ordtrans (ordtrans a<b b<c) <-osuc
|
|
|
195
|
|
|
196 OrdPreorder : Preorder n n n
|
|
|
197 OrdPreorder = record { Carrier = Ordinal
|
|
|
198 ; _≈_ = _≡_
|
|
|
199 ; _∼_ = _o≤_
|
|
|
200 ; isPreorder = record {
|
|
|
201 isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
|
|
625
|
202 ; reflexive = o≤-refl0
|
|
431
|
203 ; trans = OrdTrans
|
|
|
204 }
|
|
|
205 }
|
|
|
206
|
|
|
207 FExists : {m l : Level} → ( ψ : Ordinal → Set m )
|
|
|
208 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p )
|
|
|
209 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
|
|
|
210 → ¬ p
|
|
|
211 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
|
|
|
212
|
|
|
213 nexto∅ : {x : Ordinal} → o∅ o< next x
|
|
|
214 nexto∅ {x} with trio< o∅ x
|
|
|
215 nexto∅ {x} | tri< a ¬b ¬c = ordtrans a x<nx
|
|
|
216 nexto∅ {x} | tri≈ ¬a b ¬c = subst (λ k → k o< next x) (sym b) x<nx
|
|
|
217 nexto∅ {x} | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
|
|
|
218
|
|
|
219 next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z
|
|
|
220 next< {x} {y} {z} x<nz y<nx with trio< y (next z)
|
|
|
221 next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a
|
|
|
222 next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim (¬nx<nx x<nz (subst (λ k → k o< next x) b y<nx)
|
|
|
223 (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc) ))))
|
|
|
224 next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (¬nx<nx x<nz (ordtrans c y<nx )
|
|
|
225 (λ w nz=ow → o<¬≡ (sym nz=ow) (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))
|
|
|
226
|
|
|
227 osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y
|
|
|
228 osuc< {x} {y} refl = <-osuc
|
|
|
229
|
|
|
230 nexto=n : {x y : Ordinal} → x o< next (osuc y) → x o< next y
|
|
|
231 nexto=n {x} {y} x<noy = next< (osuc<nx x<nx) x<noy
|
|
|
232
|
|
|
233 nexto≡ : {x : Ordinal} → next x ≡ next (osuc x)
|
|
|
234 nexto≡ {x} with trio< (next x) (next (osuc x) )
|
|
|
235 -- next x o< next (osuc x ) -> osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x
|
|
|
236 nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx<nx (osuc<nx x<nx ) a
|
|
|
237 (λ z eq → o<¬≡ (sym eq) (osuc<nx (osuc< (sym eq)))))
|
|
|
238 nexto≡ {x} | tri≈ ¬a b ¬c = b
|
|
|
239 -- next (osuc x) o< next x -> osuc x o< next (osuc x) o< next x -> next (osuc x) ≡ osuc z -> z o o< next (osuc x) ...
|
|
|
240 nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c
|
|
|
241 (λ z eq → o<¬≡ (sym eq) (osuc<nx (osuc< (sym eq)))))
|
|
|
242
|
|
|
243 next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y)
|
|
|
244 next-is-limit {x} {y} eq = o<¬≡ (sym eq) (osuc<nx y<nx) where
|
|
|
245 y<nx : y o< next x
|
|
|
246 y<nx = osuc< (sym eq)
|
|
|
247
|
|
|
248 omax<next : {x y : Ordinal} → x o< y → omax x y o< next y
|
|
|
249 omax<next {x} {y} x<y = subst (λ k → k o< next y ) (omax< _ _ x<y ) (osuc<nx x<nx)
|
|
|
250
|
|
|
251 x<ny→≡next : {x y : Ordinal} → x o< y → y o< next x → next x ≡ next y
|
|
|
252 x<ny→≡next {x} {y} x<y y<nx with trio< (next x) (next y)
|
|
|
253 x<ny→≡next {x} {y} x<y y<nx | tri< a ¬b ¬c = -- x < y < next x < next y ∧ next x = osuc z
|
|
|
254 ⊥-elim ( ¬nx<nx y<nx a (λ z eq → o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc ))))
|
|
|
255 x<ny→≡next {x} {y} x<y y<nx | tri≈ ¬a b ¬c = b
|
|
|
256 x<ny→≡next {x} {y} x<y y<nx | tri> ¬a ¬b c = -- x < y < next y < next x
|
|
|
257 ⊥-elim ( ¬nx<nx (ordtrans x<y x<nx) c (λ z eq → o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc ))))
|
|
|
258
|
|
|
259 ≤next : {x y : Ordinal} → x o≤ y → next x o≤ next y
|
|
|
260 ≤next {x} {y} x≤y with trio< (next x) y
|
|
|
261 ≤next {x} {y} x≤y | tri< a ¬b ¬c = ordtrans a (ordtrans x<nx <-osuc )
|
|
|
262 ≤next {x} {y} x≤y | tri≈ ¬a refl ¬c = (ordtrans x<nx <-osuc )
|
|
|
263 ≤next {x} {y} x≤y | tri> ¬a ¬b c with osuc-≡< x≤y
|
|
625
|
264 ≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl -- x = y < next x
|
|
|
265 ≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl0 (x<ny→≡next x<y c) -- x ≤ y < next x
|
|
431
|
266
|
|
|
267 x<ny→≤next : {x y : Ordinal} → x o< next y → next x o≤ next y
|
|
|
268 x<ny→≤next {x} {y} x<ny with trio< x y
|
|
|
269 x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c = ≤next (ordtrans a <-osuc )
|
|
625
|
270 x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c = o≤-refl
|
|
|
271 x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl0 (sym ( x<ny→≡next c x<ny ))
|
|
431
|
272
|
|
|
273 omax<nomax : {x y : Ordinal} → omax x y o< next (omax x y )
|
|
|
274 omax<nomax {x} {y} with trio< x y
|
|
|
275 omax<nomax {x} {y} | tri< a ¬b ¬c = subst (λ k → osuc y o< k ) nexto≡ (osuc<nx x<nx )
|
|
|
276 omax<nomax {x} {y} | tri≈ ¬a refl ¬c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
|
|
|
277 omax<nomax {x} {y} | tri> ¬a ¬b c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
|
|
|
278
|
|
|
279 omax<nx : {x y z : Ordinal} → x o< next z → y o< next z → omax x y o< next z
|
|
|
280 omax<nx {x} {y} {z} x<nz y<nz with trio< x y
|
|
|
281 omax<nx {x} {y} {z} x<nz y<nz | tri< a ¬b ¬c = osuc<nx y<nz
|
|
|
282 omax<nx {x} {y} {z} x<nz y<nz | tri≈ ¬a refl ¬c = osuc<nx y<nz
|
|
|
283 omax<nx {x} {y} {z} x<nz y<nz | tri> ¬a ¬b c = osuc<nx x<nz
|
|
|
284
|
|
|
285 nn<omax : {x nx ny : Ordinal} → x o< next nx → x o< next ny → x o< next (omax nx ny)
|
|
|
286 nn<omax {x} {nx} {ny} xnx xny with trio< nx ny
|
|
|
287 nn<omax {x} {nx} {ny} xnx xny | tri< a ¬b ¬c = subst (λ k → x o< k ) nexto≡ xny
|
|
|
288 nn<omax {x} {nx} {ny} xnx xny | tri≈ ¬a refl ¬c = subst (λ k → x o< k ) nexto≡ xny
|
|
|
289 nn<omax {x} {nx} {ny} xnx xny | tri> ¬a ¬b c = subst (λ k → x o< k ) nexto≡ xnx
|
|
|
290
|
|
|
291 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
|
|
|
292 field
|
|
|
293 os→ : (x : Ordinal) → x o< maxordinal → Ordinal
|
|
|
294 os← : Ordinal → Ordinal
|
|
|
295 os←limit : (x : Ordinal) → os← x o< maxordinal
|
|
|
296 os-iso← : {x : Ordinal} → os→ (os← x) (os←limit x) ≡ x
|
|
|
297 os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) → os← (os→ x lt) ≡ x
|
|
|
298
|
|
|
299 module o≤-Reasoning {n : Level} (O : Ordinals {n} ) where
|
|
|
300
|
|
|
301 -- open inOrdinal O
|
|
|
302
|
|
|
303 resp-o< : _o<_ Respects₂ _≡_
|
|
|
304 resp-o< = resp₂ _o<_
|
|
|
305
|
|
|
306 trans1 : {i j k : Ordinal} → i o< j → j o< osuc k → i o< k
|
|
|
307 trans1 {i} {j} {k} i<j j<ok with osuc-≡< j<ok
|
|
|
308 trans1 {i} {j} {k} i<j j<ok | case1 refl = i<j
|
|
|
309 trans1 {i} {j} {k} i<j j<ok | case2 j<k = ordtrans i<j j<k
|
|
|
310
|
|
|
311 trans2 : {i j k : Ordinal} → i o< osuc j → j o< k → i o< k
|
|
|
312 trans2 {i} {j} {k} i<oj j<k with osuc-≡< i<oj
|
|
|
313 trans2 {i} {j} {k} i<oj j<k | case1 refl = j<k
|
|
|
314 trans2 {i} {j} {k} i<oj j<k | case2 i<j = ordtrans i<j j<k
|
|
|
315
|
|
|
316 open import Relation.Binary.Reasoning.Base.Triple
|
|
|
317 (Preorder.isPreorder OrdPreorder)
|
|
|
318 ordtrans --<-trans
|
|
|
319 (resp₂ _o<_) --(resp₂ _<_)
|
|
|
320 (λ x → ordtrans x <-osuc ) --<⇒≤
|
|
|
321 trans1 --<-transˡ
|
|
|
322 trans2 --<-transʳ
|
|
|
323 public
|
|
|
324 -- hiding (_≈⟨_⟩_)
|
|
|
325
|
