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

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

At: formula rank wf 1 1 2 3 1 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);

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

By: GenConcl (case x2:x 0;p ((p)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);pq ((p)+(q)+1); = n2) THEN GenConcl (case x1:x 0;p ((p)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);pq ((p)+(q)+1); = n1)

Generated subgoals:

None

About:

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