Nuprl - Proof: atomic char 1 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

1. a :

a = 0
3.

(a ~ 1)
4. b :

5. c :

6. a = b

c
7.

(b ~ 1)
8.

(b ~ (b

c))
9.

c = 0
10.

b = 0
11.

c = 0
12. c ~ 1

False

By:	(RWH (HypC 12) 8) THEN (Analyze 8) THEN (ArithSimp 0)

Generated subgoal:

1 8. bc = 0
9. b = 0
10. c = 0
11. c ~ 1
b ~ b
1 step

About:

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