(11steps total)
PrintForm
Definitions
LogicSupplement
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
xor
vs
neg
n
dec
1
2
1.
P
: Prop
2.
Q
: Prop
3. (
Q
P
) & Dec(
P
)
P
XOR
Q
By:
Guarding (<prop>
<prop>) Def THEN Rewrite by
Q
P
Generated subgoals:
1
3.
Q
P
4.
Q
(
P
)
5. Dec(
P
)
P
P
1
step
2
3.
Q
P
4.
Q
(
P
)
5. Dec(
P
)
(
P
&
P
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(11steps total)
PrintForm
Definitions
LogicSupplement
Sections
DiscrMathExt
Doc
P) & Dec(P)
P XOR Q P) & Dec(P)
P XOR Q <prop>) Def THEN Rewrite by Q P
P
(P)
P 
P
P
(P)
(P & P)
