Running Tactics 1

The proof-editor window should now look like:

$$\vdash \forall {\Bbb{P}} \forall {\Bbb{P}} \neg \wedge \Longleftrightarrow \neg \vee \neg$$ <refinement rule>

Click on <refinement rule>. selects it and opens up a term-editor window, which should look like:

The rule window is set up for entering a tactic. Initially the window contains an empty text string. Enter the tactic:

Here $\ulcorner$0$\urcorner$ is the number zero. The letter O in the typewriter font is $\ulcorner$O$\urcorner$.The $\langle$C-Z$\rangle$ closes the window and runs the tactic D 0 on the main goal, generating two subgoals:

$$\vdash \forall {\Bbb{P}} \forall {\Bbb{P}} \neg \wedge \Longleftrightarrow \neg \vee \neg$$ BY D 0

$${\Bbb{P}}$$

$$\vdash \forall {\Bbb{P}} \neg \wedge \Longleftrightarrow \neg \vee \neg$$

$$\vdash {\Bbb{P}} \in \Bbb{U}$$

The D tactic decomposes the outermost connective of either a hypothesis or the conclusion. The D tactic always takes an integer argument. To see this, click in the ML-Top-Loop window, and enter

You should see:

So the expression $\ulcorner$D 0$\urcorner$ has the ML type tactic. Enter

You should see: