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

comparison src/Ordinals.agda @ 693:a3b7f1e0ca60

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
same problem again
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 11 Jul 2022 11:49:11 +0900
parents 099ca2fea51c
children 7c39cae23803
comparison
equal deleted inserted replaced
692:38103b4e6780 693:a3b7f1e0ca60
24 trio< : Trichotomous {n} _≡_ _o<_ 24 trio< : Trichotomous {n} _≡_ _o<_
25 ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) 25 ¬x<0 : { x : ord } → ¬ ( x o< o∅ )
26 <-osuc : { x : ord } → x o< osuc x 26 <-osuc : { x : ord } → x o< osuc x
27 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) 27 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a)
28 Oprev-p : ( x : ord ) → Dec ( Oprev ord osuc x ) 28 Oprev-p : ( x : ord ) → Dec ( Oprev ord osuc x )
29 o<-irr : { x y : ord } → { lt lt1 : x o< y } → lt ≡ lt1 29 o<-irr : { x y : ord } → ( lt lt1 : x o< y ) → lt ≡ lt1
30 TransFinite : { ψ : ord → Set (suc n) } 30 TransFinite : { ψ : ord → Set (suc n) }
31 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) 31 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
32 → ∀ (x : ord) → ψ x 32 → ∀ (x : ord) → ψ x
33 33
34 34