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

comparison ordinal.agda @ 30:3b0fdb95618e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
problem on Ordinal ( OSuc ℵ )
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 21 May 2019 00:30:01 +0900
parents fce60b99dc55
children 97ff3f7933fe 2b853472cb24
comparison
equal deleted inserted replaced
29:fce60b99dc55 30:3b0fdb95618e
28 _o<_ : {n : Level} ( x y : Ordinal ) → Set n 28 _o<_ : {n : Level} ( x y : Ordinal ) → Set n
29 _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y ) 29 _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y )
30 30
31 open import Data.Nat.Properties 31 open import Data.Nat.Properties
32 open import Data.Empty 32 open import Data.Empty
33 open import Data.Unit using ( ⊤ )
33 open import Relation.Nullary 34 open import Relation.Nullary
34 35
35 open import Relation.Binary 36 open import Relation.Binary
36 open import Relation.Binary.Core 37 open import Relation.Binary.Core
38
39 ¬ℵ : {n : Level} {lx : Nat } ( x : OrdinalD {n} lx ) → Set
40 ¬ℵ (Φ lv₁) = ⊤
41 ¬ℵ (OSuc lv₁ x) = ¬ℵ x
42 ¬ℵ (ℵ lv₁) = ⊥
43
44 s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → ¬ℵ x → x d< OSuc lx x
45 s<refl {n} {.lv₁} {Φ lv₁} t = Φ<
46 s<refl {n} {.lv₁} {OSuc lv₁ x} t = s< (s<refl t)
47 s<refl {n} {.(Suc lv₁)} {ℵ lv₁} ()
37 48
38 o∅ : {n : Level} → Ordinal {n} 49 o∅ : {n : Level} → Ordinal {n}
39 o∅ = record { lv = Zero ; ord = Φ Zero } 50 o∅ = record { lv = Zero ; ord = Φ Zero }
40 51
41 52
165 ; reflexive = case1 176 ; reflexive = case1
166 ; trans = OrdTrans 177 ; trans = OrdTrans
167 } 178 }
168 } 179 }
169 180
170 TransFinite : {n : Level} → ( ψ : Ordinal {n} → Set n ) 181 TransFinite : {n : Level} → { ψ : Ordinal {n} → Set n }
171 → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } )) 182 → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } ))
172 → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) ) 183 → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
173 → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) ) 184 → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
174 → ∀ (x : Ordinal) → ψ x 185 → ∀ (x : Ordinal) → ψ x
175 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = caseΦ lv 186 TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = caseΦ lv
176 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = caseOSuc lv ord₁ 187 TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = caseOSuc lv ord₁
177 ( TransFinite ψ caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } )) 188 ( TransFinite caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
178 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁ 189 TransFinite caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁
179 190