Nuprl - Pf formula rank wf 1 1 2

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

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

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

By: Analyze -1 THENL [Fold `fvar` 0 THEN Reduce 0;Analyze -1 THENL [Fold `fnot` 0 THEN Reduce 0;Analyze -1 THENL [Analyze -1 THEN Fold `fand` 0 THEN Reduce 0;Analyze -1 THENL [Analyze -1 THEN Fold `f_or` 0 THEN Reduce 0;Analyze -1 THEN Fold `fimp` 0 THEN Reduce 0]]]]

Generated subgoals:

1 3. x: Var
0

2 3. x: {f:Formula| Q(f) }
(x)+1

3 3. x1: {f:Formula| Q(f) }
4. x2: {f:Formula| Q(f) }
(x1)+(x2)+1

4 3. x1: {f:Formula| Q(f) }
4. x2: {f:Formula| Q(f) }
(x1)+(x2)+1

5 3. y2: {f:Formula| Q(f) }
4. y3: {f:Formula| Q(f) }
(y2)+(y3)+1

About:

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

1	3. `x:` `Var` `0`
2	3. `x:` `{f:Formula\| Q(f) }` `(x)+1`
3	3. `x1:` `{f:Formula\| Q(f) }` 4. `x2:` `{f:Formula\| Q(f) }` `(x1)+(x2)+1`
4	3. `x1:` `{f:Formula\| Q(f) }` 4. `x2:` `{f:Formula\| Q(f) }` `(x1)+(x2)+1`
5	3. `y2:` `{f:Formula\| Q(f) }` 4. `y3:` `{f:Formula\| Q(f) }` `(y2)+(y3)+1`