Nuprl - Proof: decidable cand 1

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

1. P : Prop
2. Q : Prop(given P)
3. Dec(P)
4. P

Dec(Q)

Dec(P & Q)

By:

Analyze-2

Generated subgoals:

1 3. P
4. P  Dec(Q)
  Dec(P & Q)
4 steps

2 3. P
4. P  Dec(Q)
  Dec(P & Q)
3 steps

About:

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

1	3. P 4. P Dec(Q) Dec(P & Q)	4 steps
2	3. P 4. P Dec(Q) Dec(P & Q)	3 steps