Example: Copy the following term into the tactic slot of the proof below: Analyze5

To do this copying, place the point on the TACTIC slot with `(mouseleft)', then place the point on the above term, then use `(c-c)'.

Then, assuming the point is somewhere within the proof term, use `(c-z)'. This should "analyze" the 5th hypothesis into its two conjuncts, adding them as new assumptions in the subgoal.

Now, delete the tactic code and copy this into the slot: BackThru: Hyp:4

Use `(c-z)' notice that now there are two subgoals that result from "backchaining" through hpothesis Hyp:4, namely the Propositions, A and B, that hyp Hyp:4 says are sufficient for showing C.

Execute `(c-z)' again and note that Auto knocks off these subgoals, since they are explicitly assumed at Hyp:6 and Hyp:7.

top 1 1 1 11" A : Prop2" B : Prop3" C : Prop4" A B C5" A & B6. A7. B" C by <Unproved PREMISE><subgoals>

QUIT

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