Nuprl - Pf formula rank wf 1 1 2 3 1

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

At: formula rank wf 1 1 2 3 1

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

(x1)+(x2)+1

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

Generated subgoal:

1 case x1:x 0;p ((p)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);+case x2: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