Nuprl - Proof: assert-w-match 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: assert-w-match 2

1. the_w : World
2. l : IdLnk
3. t :

4. t' :

5. ||onlnk(l;m(source(l);t))||

((||snds(l;t)||

||rcvs(l;t')||)

((||rcvs(l;t')||<

||snds(l;t)||+||onlnk(l;m(source(l);t))||))

||snds(l;t)||

||rcvs(l;t')||

& ||rcvs(l;t')||<||snds(l;t)||+||onlnk(l;m(source(l);t))||

By:	RW assert_pushdownC 0

Generated subgoals:

None

About:

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