i$
i
i
IND BOOL
suci
IND
| Parents |
| hol |
| Constants |
|
i |
IND |
|
$
i |
IND IND BOOL
|
|
suci
|
IND IND
|
| Aliases |
|
|
i : IND
|
|
|
$i : IND IND BOOL
|
|
suc
|
suci : IND IND
|
| Fixity |
| Right Infix 240: |
i |
| Axioms |
|
strong_infinity_axiom
|
   mk_var("i",  (IND IND BOOL) )
   p q p i q  ( x x i q  ( y y i q ( Z z z i y ( v v i z  v i x Z v))) ( f ( u u i x f u i q) ( y y i q ( u u i x f u i y))))
|
| Definitions |
|
i |
T
|
|
i |
p q p q ( x x q ( y y q ( Z z z y ( v v z v x Z v))) ( f ( u u x f u q) ( y y q ( u u x f u y))))
|
|
suci
|
or suc or = ( or' x x or  x = or x or')
|
