Nuprl - Pf formula rank wf 1 1 2 2 1 1

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

At: formula rank wf 1 1 2 2 1 1

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

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

By: GenConcl (case x:x 0;p ((p)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);pq ((p)+(q)+1); = n)

Generated subgoals:

None

About:

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