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

comparison Ordinals.agda @ 387:8b0715e28b33

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 25 Jul 2020 09:09:00 +0900
parents 4cbcf71b09c4
children 19687f3304c9
comparison
equal deleted inserted replaced
386:24a66a246316 387:8b0715e28b33
22 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) 22 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a)
23 not-limit-p : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) )) 23 not-limit-p : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) ))
24 TransFinite : { ψ : ord → Set n } 24 TransFinite : { ψ : ord → Set n }
25 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) 25 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
26 → ∀ (x : ord) → ψ x 26 → ∀ (x : ord) → ψ x
27 TransFinite1 : { ψ : ord → Set (suc n) }
28 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
29 → ∀ (x : ord) → ψ x
30 27
31 record IsNext {n : Level } (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where 28 record IsNext {n : Level } (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
32 field 29 field
33 x<nx : { y : ord } → (y o< next y ) 30 x<nx : { y : ord } → (y o< next y )
34 osuc<nx : { x y : ord } → x o< next y → osuc x o< next y 31 osuc<nx : { x y : ord } → x o< next y → osuc x o< next y
63 60
64 ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O) 61 ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O)
65 osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O) 62 osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O)
66 <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O) 63 <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O)
67 TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O) 64 TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O)
68 TransFinite1 = IsOrdinals.TransFinite1 (Ordinals.isOrdinal O)
69 65
70 x<nx = IsNext.x<nx (Ordinals.isNext O) 66 x<nx = IsNext.x<nx (Ordinals.isNext O)
71 osuc<nx = IsNext.osuc<nx (Ordinals.isNext O) 67 osuc<nx = IsNext.osuc<nx (Ordinals.isNext O)
72 ¬nx<nx = IsNext.¬nx<nx (Ordinals.isNext O) 68 ¬nx<nx = IsNext.¬nx<nx (Ordinals.isNext O)
73 69