Nuprl - Proof: atomic char 1 1 1

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

1. a :

a = 0
3.

(a ~ 1)
4. b :

5. c :

6. a = b

c
7.

(b ~ 1)
8.

(b ~ a)

b,c:

(b ~ 1) &

(c ~ 1) & a = b

By:	(CopyToEnd 2) THEN (HypSubst 6 -1) THEN (Simple (FwdThru Thm* a,b:. ab = 0 a = 0 & b = 0 [-1])) THEN (Analyze -1)

Generated subgoal:

1 9. bc = 0
10. b = 0
11. c = 0
b,c:. (b ~ 1) & (c ~ 1) & a = bc
4 steps

About:

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