1072   Dyckhoff presents in \cite{Dyckhoff92} inference rules for a sequent

  1073   calculus, called G4ip, in which no contraction rule is needed in order to be

  1074   complete. As a result the rules applied in any order give a simple decision

  1075   procedure for propositional intuitionistic logic. His rules are

  1076 

  1077   \begin{center}

  1078   \def\arraystretch{2.3}

  1079   \begin{tabular}{cc}

  1080   \infer[Ax]{A,\varGamma \Rightarrow A}{} &

  1081   \infer[False]{False,\varGamma \Rightarrow G}{}\\

  1082 

  1083   \infer[\wedge_L]{A \wedge B, \varGamma \Rightarrow G}{A, B, \varGamma \Rightarrow G} &

  1084   \infer[\wedge_R]

  1085   {\varGamma \Rightarrow A\wedge B}{\varGamma \Rightarrow A & \varGamma \Rightarrow B}\\

  1087   \infer[\vee_L]

  1088   {A\vee B, \varGamma \Rightarrow G}{A,\varGamma \Rightarrow G & B,\varGamma \Rightarrow G} &

  1089   \infer[\vee_{R_1}]

  1090   {\varGamma \Rightarrow A \vee B}{\varGamma \Rightarrow A} \hspace{3mm}

  1091   \infer[\vee_{R_2}]

  1092   {\varGamma \Rightarrow A \vee B}{\varGamma \Rightarrow B}\\

  1093   

  1094   \infer[\longrightarrow_{L_1}]

  1095   {A\longrightarrow B, A, \varGamma \Rightarrow G}{B, A, \varGamma \Rightarrow G} &

  1096   \infer[\longrightarrow_R]

  1097   {\varGamma \Rightarrow A\longrightarrow B}{A,\varGamma \Rightarrow B}\\

  1098 

  1099   \infer[\longrightarrow_{L_2}]

  1100   {(C \wedge D)\longrightarrow B, \varGamma \Rightarrow G}

  1101   {C\longrightarrow (D \longrightarrow B), \varGamma \Rightarrow G} &

  1102   

  1103   \infer[\longrightarrow_{L_3}]

  1104   {(C \vee D)\longrightarrow B, \varGamma \Rightarrow G}

  1105   {C\longrightarrow B, D\longrightarrow B, \varGamma \Rightarrow G}\\

  1106 

  1107   \multicolumn{2}{c}{

  1108   \infer[\longrightarrow_{L_4}]

  1109   {(C \longrightarrow D)\longrightarrow B, \varGamma \Rightarrow G}

  1110   {D\longrightarrow B, \varGamma \Rightarrow C \longrightarrow D &

  1111   B, \varGamma \Rightarrow G}}\\

  1112   \end{tabular}

  1113   \end{center}

  1114 

  1115   Implement a tactic that explores all possibilites of applying these rules to

  1116   a propositional formula until a goal state is reached in which all subgoals

  1117   are discharged.  Note that in Isabelle the left-rules need to be implemented

  1118   as elimination rules. You need to prove separate lemmas corresponding to

  1119   $\longrightarrow_{L_{1..4}}$.  In order to explore all possibilities of applying 

  1120   the rules, use the tactic combinator @{ML [index] DEPTH_SOLVE}, which searches 

  1121   for a state in which all subgoals are solved. Add also rules for equality and

  1122   run your tactic on the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}.