Nuprl - Proof: atomic char 1 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: atomic char 1 1 1 1 1

1. a :

a = 0
3.

(a ~ 1)
4. b :

5. c :

6. a = b

c
7.

(b ~ 1)
8.

(b ~ a)
9.

c = 0
10.

b = 0
11.

c = 0

(c ~ 1)

By:	(HypSubst 6 8) THEN (Analyze 0)

Generated subgoal:

1 8. (b ~ (bc))
9. bc = 0
10. b = 0
11. c = 0
12. c ~ 1
False
2 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html