The Theory surreal
Parents
wf_relp gst-misc
Constants
s
No
<s
No → No → BOOL
IC
(No → BOOL) → No → No
rank
No → No
$<<
No → No → BOOL
Aliases
s : No
<
<s : No → No → BOOL
Types
No
Fixity
Right Infix 240:
e <<
Axioms
SZeroAx
⊢ ∀ x• rank x = ∅ ⇔ x = ∅
SCutAx
⊢ ∀ p n
fill• (∀ x y• x << n ∧ y << n ∧ x < y ∧ p y ⇒ p x)
fill⇒ (∀ x
fill• x << n
fill⇒ (p x ⇔ x < IC p n)
fill∧ (¬ p x ⇔ IC p n < x))
fill∧ (∀ q
fill• (∀ x• x << n ⇒ (p x ⇔ q x))
fill⇔ IC p n = IC q n)
SIndAx
⊢ well_founded $<<
SInfAx
⊢ ∀ p
fill• ∃ q
fill• p << q
fill∧ (∀ x
fill• x << q
fill⇒ (∃ y $e
fill• y << q
fill∧ (∀ Z
fill• ∃ u
fill• u << y
fill∧ (∀ v
fill• v << x ⇒ (v e u ⇔ Z v))))
fill∧ (∀ G
fill• (∀ u• u << x ⇒ G u << q)
fill⇒ (∃ y
fill• y << q
fill∧ (∀ u• u << x ⇒ G u << y))))
Definitions
rank
⊢ ∀ n• rank n = IC (λ x• T) n
<<
⊢ ∀ n m• n << m ⇔ rank n < rank m

up quick index

privacy policy

Created:

V