Nuprl - Proof: atomic imp prime 1

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

1. a :

2. atomic(a)
3.

(a ~ 1) & (

. b | a

(b ~ 1)

(b ~ a))

prime(a)

By:	Unfold `prime` 0 THEN Unfold `atomic` 2 THEN GenUnivCD THEN (Complete Auto ORELSE Thin 2)

Generated subgoal:

1 2. (a ~ 1) & (b:. b | a (b ~ 1) (b ~ a))
3. b :
4. c :
5. a | bc
a | b a | c
11 steps

About:

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