| 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  • (∀ x y• x << n ∧ y << n ∧ x < y ∧ p y ⇒ p x) ⇒ (∀ x • x << n ⇒ (p x ⇔ x < IC p n) ∧ (¬ p x ⇔ IC p n < x)) ∧ (∀ q • (∀ x• x << n ⇒ (p x ⇔ q x)) ⇔ IC p n = IC q n)
|
|
SIndAx
|
⊢ well_founded $<< |
|
SInfAx
|
⊢ ∀ p • ∃ q • p << q ∧ (∀ x • x << q ⇒ (∃ y $e • y << q ∧ (∀ Z • ∃ u • u << y ∧ (∀ v • v << x ⇒ (v e u ⇔ Z v)))) ∧ (∀ G • (∀ u• u << x ⇒ G u << q) ⇒ (∃ y • y << q ∧ (∀ u• u << x ⇒ G u << y))))
|
| Definitions |
|
rank
|
⊢ ∀ n• rank n = IC (λ x• T) n |
|
<<
|
⊢ ∀ n m• n << m ⇔ rank n < rank m |
