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

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

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

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

By: GenConcl (case y3:x 0;p ((p)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);pq ((p)+(q)+1); = n3) THEN GenConcl (case y2:x 0;p ((p)+1);pq ((p)+(q)+1);pq ((p)+(q)+1);pq ((p)+(q)+1); = n2)

Generated subgoals:

None

About:

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