Nuprl - Proof: ma-compat-symmetry

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ma-compat-symmetry

A,B:MsgA. A ||+ B

B ||+ A

By:	Auto THEN ParallelOp -1 THEN Try (BackThru Thm* M1,M2:MsgA. M1 \|\| M2 M2 \|\| M1) THEN AllHyps (h. (ParallelOp h THEN ParallelOp h THEN Analyze -1 THEN Analyze 0 THEN Try Trivial) THEN AllHyps (h. (ParallelOp h THEN ParallelOp h THEN ParallelLast THEN Analyze -1 THEN Analyze 0 (THEN (Try Trivial)

Generated subgoals:

None

About:

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