Nuprl - Pf formula rank wf 1 1 2 5 1

(18steps) PrintForm Definitions formula rank Sections ClassicalProps(jlc) Doc

At: formula rank wf 1 1 2 5 1

1. Q: FormulaProp
2. y2: {f:Formula| Q(f) }
3. y3: {f:Formula| Q(f) }
4. case y2:x 0;p ((p)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);
5. case y3:x 0;p ((p)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);

(y2)+(y3)+1

By: RWH (AllC [UnfoldC `formula_rank`;letrec_unrollC;FoldC `formula_rank`]) 0

Generated subgoal:

1 case y2:x 0;p ((p)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);+case y3:x 0;p ((p)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);+1

About:

(18steps) PrintForm Definitions formula rank Sections ClassicalProps(jlc) Doc