Nuprl - Proof: decidable cand

(13steps total) PrintForm Definitions Lemmas LogicSupplement Sections DiscrMathExt Doc

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

P:Prop, Q:Prop(given P). Dec(P)

Dec(Q))

Dec(P & Q)

By:

UnivCD

Generated subgoals:

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

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

About:

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

(13steps total) PrintForm Definitions Lemmas LogicSupplement Sections DiscrMathExt Doc

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