PrintForm
Definitions
action
sets
Sections
AutomataTheory
Doc
At:
factorial
wf
1
2
2
1.
n:
2.
0 < n
3.
(n-1)!
4.
n = 0
0
n
(n-1)!
By:
Inst
Thm*
a,b:
, n:
. a
b
n
a
n
b [0;n;(n-1)! ]
Generated subgoals:
1
0
n
2
5.
(n-1)!
0
(n-1)!
n
0
n
(n-1)!
About:
0
n
0(n-1)! n 0n(n-1)! 
n = 0 0n(n-1)! 
a,b:, n:. ab 
nanb
[0;n;(n-1)! ] 0n0(n-1)! n 0n(n-1)! 
