Nuprl - Proof: ma-join-list-property 1

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ma-join-list-property 1

1. MsgA List

(

A,B

nil.A ||+ B)

(nil)

MsgA & (

M:MsgA. (

nil.M ||+ B)

M ||+

(nil))

By:	Unfolds [`pairwise`;`ma-join-list`] 0 THEN Reduce 0 THEN Unfold `ma-compat` 0 THEN Try (BackThru Thm* A:MsgA. A \|\| ) THEN Try (BackThru Thm* A:MsgA. ma-frame-compatible(A; )) THEN Try (BackThru Thm* A:MsgA. ma-sframe-compatible(A; ))

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html