Nuprl - Proof: assert-ma-join-list-is-empty 2

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

1. MsgA List
2. u : MsgA
3. v : MsgA List
4. reduce(

M,x. ma-is-empty(M)

x;true

;v)
4.

4. reduce(

M,x. ma-is-empty(M) & x;True;v)

(ma-is-empty(u)

reduce(

M,x. ma-is-empty(M)

x;true

;v))

ma-is-empty(u) & reduce(

M,x. ma-is-empty(M) & x;True;v)

By:	RW assert_pushdownC 0 THEN BackThruSomeHyp

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