FreeChief

This is the user page for the Programmer in Chief. Does it work? Programmer in Chief (talk) 07:38, 18 February 2011 (UTC)

$Axiom\quad {A\leftarrow A}$

$Cut\quad {C\leftarrow \Delta A\Delta '\qquad A\leftarrow \Gamma \over C\leftarrow \Delta \Gamma \Delta '}$

Introduction	Elimination
$\backslash In\quad {C\leftarrow \Delta B\Delta '\qquad A\leftarrow \Gamma \over C\leftarrow \Delta \Gamma (A\backslash B)\Delta '}$	$\backslash Out\quad {B\leftarrow A\Gamma \over A\backslash B\leftarrow \Gamma }$
$/In\quad {C\leftarrow \Delta B\Delta '\qquad A\leftarrow \Gamma \over C\leftarrow \Delta (B/A)\Gamma \Delta '}$	$/Out\quad {B\leftarrow \Gamma A \over B/A\leftarrow \Gamma }$
$\star In\quad {C\leftarrow \Delta AB\Delta ' \over C\leftarrow \Delta (A\star B)\Delta '}$	$\star Out\quad {A\leftarrow \Gamma \qquad B\leftarrow \Gamma ' \over A\star B\leftarrow \Gamma \Gamma '}$