Nuprl - Pf zero_rank_all_vars 1 1 1 1 1 1 1 2 1

PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

At: zero rank all vars 1 1 1 1 1 1 1 2 1

1. z: Formula

(z) = 0 (v:Var. z = v)

By: FormulaCases 1 THEN AbReduce 0

Generated subgoals:

1 2. x: Var
0 = 0 (v:Var. x = v)

2 2. x: Formula
(x)+1 = 0 (v:Var. x = v)

3 2. x1: Formula
3. x2: Formula
(x1)+(x2)+1 = 0 (v:Var. x1x2 = v)

4 2. x1: Formula
3. x2: Formula
(x1)+(x2)+1 = 0 (v:Var. x1x2 = v)

5 2. y1: Formula
3. y2: Formula
(y1)+(y2)+1 = 0 (v:Var. y1y2 = v)

About:

1	2. `x:` `Var` `0 = 0 (v:Var. x = v)`
2	2. `x:` `Formula` `(x)+1 = 0 (v:Var. x = v)`
3	2. `x1:` `Formula` 3. `x2:` `Formula` `(x1)+(x2)+1 = 0 (v:Var. x1x2 = v)`
4	2. `x1:` `Formula` 3. `x2:` `Formula` `(x1)+(x2)+1 = 0 (v:Var. x1x2 = v)`
5	2. `y1:` `Formula` 3. `y2:` `Formula` `(y1)+(y2)+1 = 0 (v:Var. y1y2 = v)`