(18steps)
PrintForm
Definitions
formula
rank
Sections
ClassicalProps(jlc)
Doc
At:
formula
rank
wf
Formula
By:
RWH (AllC [UnfoldC `formula_rank`;letrec_unrollC;FoldC `formula_rank`]) 0
Generated subgoal:
1
(
f.case f:
x
0;
p
(
(p)+1);p
q
(
(p)+
(q)+1);p
q
(
(p)+
(q)+1);p
q
(
(p)+
(q)+1);)
Formula
About:
(18steps)
PrintForm
Definitions
formula
rank
Sections
ClassicalProps(jlc)
Doc
(
f.case f:
x
0;
p (
(p)+1);p
q ((p)+(q)+1);p
q ((p)+(q)+1);p
q ((p)+(q)+1);) 
Formula
Formula
(f.case f:x 0;p ((p)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);) Formula
