Thms
action
sets
Sections
AutomataTheory
Doc
factorial
Def
(n)! == if n=
0
1 else n
(n-1)! fi (recursive)
Thm*
n:
. (n)!
eq_int
Def
i=
j == if i=j
true
; false
fi
Thm*
i,j:
. i=
j
About:
0
1 else n
(n-1)! fi (recursive)
n:
. (n)! 
j == if i=j true ; false fi
i,j:
. i=j 
0 1 else n(n-1)! fi (recursive)
j == if i=j true ; false fi
