Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate OrdUtil.agda @ 423:9984cdd88da3
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 01 Aug 2020 18:05:23 +0900 |
| parents | Ordinals.agda@53422a8ea836 |
| children | 94392feeebc5 |
| rev | line source |
|---|---|
| 16 | 1 open import Level |
| 423 | 2 open import Ordinals |
| 3 module OrdUtil {n : Level} (O : Ordinals {n} ) where | |
| 3 | 4 |
| 423 | 5 open import logic |
| 6 open import nat | |
| 23 | 7 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) |
| 75 | 8 open import Data.Empty |
| 423 | 9 open import Relation.Binary.PropositionalEquality |
|
220
95a26d1698f4
try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
218
diff
changeset
|
10 open import Relation.Nullary |
|
95a26d1698f4
try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
218
diff
changeset
|
11 open import Relation.Binary |
| 3 | 12 |
| 423 | 13 open Ordinals.Ordinals O |
| 14 open Ordinals.IsOrdinals isOrdinal | |
| 15 open Ordinals.IsNext isNext | |
| 414 | 16 |
| 423 | 17 o<-dom : { x y : Ordinal } → x o< y → Ordinal |
| 18 o<-dom {x} _ = x | |
| 16 | 19 |
| 423 | 20 o<-cod : { x y : Ordinal } → x o< y → Ordinal |
| 21 o<-cod {_} {y} _ = y | |
|
222
59771eb07df0
TransFinite induction fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
221
diff
changeset
|
22 |
| 423 | 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 | |
| 221 | 25 |
| 423 | 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 | |
|
43
0d9b9db14361
equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
41
diff
changeset
|
31 |
| 423 | 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 | |
|
348
08d94fec239c
Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
347
diff
changeset
|
37 |
| 423 | 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 | |
| 94 | 42 |
| 423 | 43 osucc : {ox oy : Ordinal } → oy o< ox → osuc oy o< osuc ox |
| 44 ---- y < osuc y < x < osuc x | |
| 45 ---- y < osuc y = x < osuc x | |
| 46 ---- y < osuc y > x < osuc x -> y = x ∨ x < y → ⊥ | |
| 47 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox | |
| 48 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc | |
| 49 osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc | |
| 50 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c with osuc-≡< c | |
| 51 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy<ox) | |
| 52 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy<ox) | |
| 23 | 53 |
| 423 | 54 osucprev : {ox oy : Ordinal } → osuc oy o< osuc ox → oy o< ox |
| 55 osucprev {ox} {oy} oy<ox with trio< oy ox | |
| 56 osucprev {ox} {oy} oy<ox | tri< a ¬b ¬c = a | |
| 57 osucprev {ox} {oy} oy<ox | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (cong (λ k → osuc k) b) oy<ox ) | |
| 58 osucprev {ox} {oy} oy<ox | tri> ¬a ¬b c = ⊥-elim (o<> (osucc c) oy<ox ) | |
| 180 | 59 |
| 423 | 60 open _∧_ |
| 221 | 61 |
| 423 | 62 osuc2 : ( x y : Ordinal ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y) |
| 63 proj2 (osuc2 x y) lt = osucc lt | |
| 64 proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy | |
| 65 proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy | |
| 66 proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy | |
| 84 | 67 |
| 423 | 68 _o≤_ : Ordinal → Ordinal → Set n |
| 69 a o≤ b = a o< osuc b -- (a ≡ b) ∨ ( a o< b ) | |
| 221 | 70 |
| 129 | 71 |
| 423 | 72 xo<ab : {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa → ox o< ob ) → oa o< osuc ob |
| 73 xo<ab {oa} {ob} a→b with trio< oa ob | |
| 74 xo<ab {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc | |
| 75 xo<ab {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc | |
| 76 xo<ab {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c ) ) | |
| 88 | 77 |
| 423 | 78 maxα : Ordinal → Ordinal → Ordinal |
| 79 maxα x y with trio< x y | |
| 80 maxα x y | tri< a ¬b ¬c = y | |
| 81 maxα x y | tri> ¬a ¬b c = x | |
| 82 maxα x y | tri≈ ¬a refl ¬c = x | |
| 84 | 83 |
| 423 | 84 omin : Ordinal → Ordinal → Ordinal |
| 85 omin x y with trio< x y | |
| 86 omin x y | tri< a ¬b ¬c = x | |
| 87 omin x y | tri> ¬a ¬b c = y | |
| 88 omin x y | tri≈ ¬a refl ¬c = x | |
| 88 | 89 |
| 423 | 90 min1 : {x y z : Ordinal } → z o< x → z o< y → z o< omin x y |
| 91 min1 {x} {y} {z} z<x z<y with trio< x y | |
| 92 min1 {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x | |
| 93 min1 {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x | |
| 94 min1 {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y | |
| 84 | 95 |
| 423 | 96 -- |
| 97 -- max ( osuc x , osuc y ) | |
| 98 -- | |
| 221 | 99 |
| 423 | 100 omax : ( x y : Ordinal ) → Ordinal |
| 101 omax x y with trio< x y | |
| 102 omax x y | tri< a ¬b ¬c = osuc y | |
| 103 omax x y | tri> ¬a ¬b c = osuc x | |
| 104 omax x y | tri≈ ¬a refl ¬c = osuc x | |
| 86 | 105 |
| 423 | 106 omax< : ( x y : Ordinal ) → x o< y → osuc y ≡ omax x y |
| 107 omax< x y lt with trio< x y | |
| 108 omax< x y lt | tri< a ¬b ¬c = refl | |
| 109 omax< x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt ) | |
| 110 omax< x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt ) | |
| 86 | 111 |
| 423 | 112 omax≤ : ( x y : Ordinal ) → x o≤ y → osuc y ≡ omax x y |
| 113 omax≤ x y le with trio< x y | |
| 114 omax≤ x y le | tri< a ¬b ¬c = refl | |
| 115 omax≤ x y le | tri≈ ¬a refl ¬c = refl | |
| 116 omax≤ x y le | tri> ¬a ¬b c with osuc-≡< le | |
| 117 omax≤ x y le | tri> ¬a ¬b c | case1 eq = ⊥-elim (¬b eq) | |
| 118 omax≤ x y le | tri> ¬a ¬b c | case2 x<y = ⊥-elim (¬a x<y) | |
| 411 | 119 |
| 423 | 120 omax≡ : ( x y : Ordinal ) → x ≡ y → osuc y ≡ omax x y |
| 121 omax≡ x y eq with trio< x y | |
| 122 omax≡ x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq ) | |
| 123 omax≡ x y eq | tri≈ ¬a refl ¬c = refl | |
| 124 omax≡ x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq ) | |
| 91 | 125 |
| 423 | 126 omax-x : ( x y : Ordinal ) → x o< omax x y |
| 127 omax-x x y with trio< x y | |
| 128 omax-x x y | tri< a ¬b ¬c = ordtrans a <-osuc | |
| 129 omax-x x y | tri> ¬a ¬b c = <-osuc | |
| 130 omax-x x y | tri≈ ¬a refl ¬c = <-osuc | |
| 16 | 131 |
| 423 | 132 omax-y : ( x y : Ordinal ) → y o< omax x y |
| 133 omax-y x y with trio< x y | |
| 134 omax-y x y | tri< a ¬b ¬c = <-osuc | |
| 135 omax-y x y | tri> ¬a ¬b c = ordtrans c <-osuc | |
| 136 omax-y x y | tri≈ ¬a refl ¬c = <-osuc | |
| 221 | 137 |
| 423 | 138 omxx : ( x : Ordinal ) → omax x x ≡ osuc x |
| 139 omxx x with trio< x x | |
| 140 omxx x | tri< a ¬b ¬c = ⊥-elim (¬b refl ) | |
| 141 omxx x | tri> ¬a ¬b c = ⊥-elim (¬b refl ) | |
| 142 omxx x | tri≈ ¬a refl ¬c = refl | |
| 221 | 143 |
| 423 | 144 omxxx : ( x : Ordinal ) → omax x (omax x x ) ≡ osuc (osuc x) |
| 145 omxxx x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc )) | |
| 221 | 146 |
| 423 | 147 open _∧_ |
| 16 | 148 |
| 423 | 149 o≤-refl : { i j : Ordinal } → i ≡ j → i o≤ j |
| 150 o≤-refl {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc | |
| 151 OrdTrans : Transitive _o≤_ | |
| 152 OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c | |
| 153 OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc | |
| 154 OrdTrans a≤b b≤c | case1 refl | case2 a≤c = ordtrans a≤c <-osuc | |
| 155 OrdTrans a≤b b≤c | case2 a≤c | case1 refl = ordtrans a≤c <-osuc | |
| 156 OrdTrans a≤b b≤c | case2 a<b | case2 b<c = ordtrans (ordtrans a<b b<c) <-osuc | |
|
97
f2b579106770
power set using sup on Def
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
94
diff
changeset
|
157 |
| 423 | 158 OrdPreorder : Preorder n n n |
| 159 OrdPreorder = record { Carrier = Ordinal | |
| 160 ; _≈_ = _≡_ | |
| 161 ; _∼_ = _o≤_ | |
| 162 ; isPreorder = record { | |
| 163 isEquivalence = record { refl = refl ; sym = sym ; trans = trans } | |
| 164 ; reflexive = o≤-refl | |
| 165 ; trans = OrdTrans | |
| 166 } | |
| 167 } | |
| 165 | 168 |
| 423 | 169 FExists : {m l : Level} → ( ψ : Ordinal → Set m ) |
| 170 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p ) | |
| 171 → (exists : ¬ (∀ y → ¬ ( ψ y ) )) | |
| 172 → ¬ p | |
| 173 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) | |
| 221 | 174 |
| 423 | 175 nexto∅ : {x : Ordinal} → o∅ o< next x |
| 176 nexto∅ {x} with trio< o∅ x | |
| 177 nexto∅ {x} | tri< a ¬b ¬c = ordtrans a x<nx | |
| 178 nexto∅ {x} | tri≈ ¬a b ¬c = subst (λ k → k o< next x) (sym b) x<nx | |
| 179 nexto∅ {x} | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) | |
| 393 | 180 |
| 423 | 181 next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z |
| 182 next< {x} {y} {z} x<nz y<nx with trio< y (next z) | |
| 183 next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a | |
| 184 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) | |
| 185 (λ 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) )))) | |
| 186 next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (¬nx<nx x<nz (ordtrans c y<nx ) | |
| 187 (λ w nz=ow → o<¬≡ (sym nz=ow) (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc )))) | |
| 339 | 188 |
| 423 | 189 osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y |
| 190 osuc< {x} {y} refl = <-osuc | |
| 342 | 191 |
| 423 | 192 nexto=n : {x y : Ordinal} → x o< next (osuc y) → x o< next y |
| 193 nexto=n {x} {y} x<noy = next< (osuc<nx x<nx) x<noy | |
| 340 | 194 |
| 423 | 195 nexto≡ : {x : Ordinal} → next x ≡ next (osuc x) |
| 196 nexto≡ {x} with trio< (next x) (next (osuc x) ) | |
| 197 -- 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 | |
| 198 nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx<nx (osuc<nx x<nx ) a | |
| 199 (λ z eq → o<¬≡ (sym eq) (osuc<nx (osuc< (sym eq))))) | |
| 200 nexto≡ {x} | tri≈ ¬a b ¬c = b | |
| 201 -- 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) ... | |
| 202 nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c | |
| 203 (λ z eq → o<¬≡ (sym eq) (osuc<nx (osuc< (sym eq))))) | |
| 346 | 204 |
| 423 | 205 next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y) |
| 206 next-is-limit {x} {y} eq = o<¬≡ (sym eq) (osuc<nx y<nx) where | |
| 207 y<nx : y o< next x | |
| 208 y<nx = osuc< (sym eq) | |
| 352 | 209 |
| 423 | 210 omax<next : {x y : Ordinal} → x o< y → omax x y o< next y |
| 211 omax<next {x} {y} x<y = subst (λ k → k o< next y ) (omax< _ _ x<y ) (osuc<nx x<nx) | |
| 393 | 212 |
| 423 | 213 x<ny→≡next : {x y : Ordinal} → x o< y → y o< next x → next x ≡ next y |
| 214 x<ny→≡next {x} {y} x<y y<nx with trio< (next x) (next y) | |
| 215 x<ny→≡next {x} {y} x<y y<nx | tri< a ¬b ¬c = -- x < y < next x < next y ∧ next x = osuc z | |
| 216 ⊥-elim ( ¬nx<nx y<nx a (λ z eq → o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc )))) | |
| 217 x<ny→≡next {x} {y} x<y y<nx | tri≈ ¬a b ¬c = b | |
| 218 x<ny→≡next {x} {y} x<y y<nx | tri> ¬a ¬b c = -- x < y < next y < next x | |
| 219 ⊥-elim ( ¬nx<nx (ordtrans x<y x<nx) c (λ z eq → o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc )))) | |
| 410 | 220 |
| 423 | 221 ≤next : {x y : Ordinal} → x o≤ y → next x o≤ next y |
| 222 ≤next {x} {y} x≤y with trio< (next x) y | |
| 223 ≤next {x} {y} x≤y | tri< a ¬b ¬c = ordtrans a (ordtrans x<nx <-osuc ) | |
| 224 ≤next {x} {y} x≤y | tri≈ ¬a refl ¬c = (ordtrans x<nx <-osuc ) | |
| 225 ≤next {x} {y} x≤y | tri> ¬a ¬b c with osuc-≡< x≤y | |
| 226 ≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl refl -- x = y < next x | |
| 227 ≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl (x<ny→≡next x<y c) -- x ≤ y < next x | |
| 410 | 228 |
| 423 | 229 x<ny→≤next : {x y : Ordinal} → x o< next y → next x o≤ next y |
| 230 x<ny→≤next {x} {y} x<ny with trio< x y | |
| 231 x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c = ≤next (ordtrans a <-osuc ) | |
| 232 x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c = o≤-refl refl | |
| 233 x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl (sym ( x<ny→≡next c x<ny )) | |
| 410 | 234 |
| 423 | 235 omax<nomax : {x y : Ordinal} → omax x y o< next (omax x y ) |
| 236 omax<nomax {x} {y} with trio< x y | |
| 237 omax<nomax {x} {y} | tri< a ¬b ¬c = subst (λ k → osuc y o< k ) nexto≡ (osuc<nx x<nx ) | |
| 238 omax<nomax {x} {y} | tri≈ ¬a refl ¬c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx ) | |
| 239 omax<nomax {x} {y} | tri> ¬a ¬b c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx ) | |
| 410 | 240 |
| 423 | 241 omax<nx : {x y z : Ordinal} → x o< next z → y o< next z → omax x y o< next z |
| 242 omax<nx {x} {y} {z} x<nz y<nz with trio< x y | |
| 243 omax<nx {x} {y} {z} x<nz y<nz | tri< a ¬b ¬c = osuc<nx y<nz | |
| 244 omax<nx {x} {y} {z} x<nz y<nz | tri≈ ¬a refl ¬c = osuc<nx y<nz | |
| 245 omax<nx {x} {y} {z} x<nz y<nz | tri> ¬a ¬b c = osuc<nx x<nz | |
| 410 | 246 |
| 423 | 247 nn<omax : {x nx ny : Ordinal} → x o< next nx → x o< next ny → x o< next (omax nx ny) |
| 248 nn<omax {x} {nx} {ny} xnx xny with trio< nx ny | |
| 249 nn<omax {x} {nx} {ny} xnx xny | tri< a ¬b ¬c = subst (λ k → x o< k ) nexto≡ xny | |
| 250 nn<omax {x} {nx} {ny} xnx xny | tri≈ ¬a refl ¬c = subst (λ k → x o< k ) nexto≡ xny | |
| 251 nn<omax {x} {nx} {ny} xnx xny | tri> ¬a ¬b c = subst (λ k → x o< k ) nexto≡ xnx | |
| 420 | 252 |
| 423 | 253 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where |
| 254 field | |
| 255 os→ : (x : Ordinal) → x o< maxordinal → Ordinal | |
| 256 os← : Ordinal → Ordinal | |
| 257 os←limit : (x : Ordinal) → os← x o< maxordinal | |
| 258 os-iso← : {x : Ordinal} → os→ (os← x) (os←limit x) ≡ x | |
| 259 os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) → os← (os→ x lt) ≡ x | |
| 309 | 260 |
| 423 | 261 module o≤-Reasoning {n : Level} (O : Ordinals {n} ) where |
| 361 | 262 |
| 423 | 263 -- open inOrdinal O |
| 361 | 264 |
| 423 | 265 resp-o< : _o<_ Respects₂ _≡_ |
| 266 resp-o< = resp₂ _o<_ | |
| 361 | 267 |
| 423 | 268 trans1 : {i j k : Ordinal} → i o< j → j o< osuc k → i o< k |
| 269 trans1 {i} {j} {k} i<j j<ok with osuc-≡< j<ok | |
| 270 trans1 {i} {j} {k} i<j j<ok | case1 refl = i<j | |
| 271 trans1 {i} {j} {k} i<j j<ok | case2 j<k = ordtrans i<j j<k | |
| 361 | 272 |
| 423 | 273 trans2 : {i j k : Ordinal} → i o< osuc j → j o< k → i o< k |
| 274 trans2 {i} {j} {k} i<oj j<k with osuc-≡< i<oj | |
| 275 trans2 {i} {j} {k} i<oj j<k | case1 refl = j<k | |
| 276 trans2 {i} {j} {k} i<oj j<k | case2 i<j = ordtrans i<j j<k | |
| 361 | 277 |
| 423 | 278 open import Relation.Binary.Reasoning.Base.Triple |
| 279 (Preorder.isPreorder OrdPreorder) | |
| 280 ordtrans --<-trans | |
| 281 (resp₂ _o<_) --(resp₂ _<_) | |
| 282 (λ x → ordtrans x <-osuc ) --<⇒≤ | |
| 283 trans1 --<-transˡ | |
| 284 trans2 --<-transʳ | |
| 285 public | |
| 286 hiding (_≈⟨_⟩_) | |
| 361 | 287 |