(sequent hyp ()
______________
P >> P;)
(sequent vr1 ()
P;
______________
[P v Q];)
(sequent vr2 ()
Q;
______________
[P v Q];)
(sequent vl ()
Q >> P;
R >> P;
______________
[Q v R] >> P;)
(sequent &r ()
P; Q;
_____
[P & Q];)
(sequent &l ()
P, Q >> R;
__________
[P & Q] >> R;)
(sequent =>r ()
P >> Q;
_______
[P => Q];)
(sequent =>l ()
[P => Q] >> P;
______________
[P => Q] >> Q;)
(sequent <=>r ()
[[P => Q] & [Q => P]];
______________________
[P <=> Q];)
(sequent <=>l ()
[[P => Q] & [Q => P]] >> R;
______________________
[P <=> Q] >> R;)
(sequent ~r ()
[P => falsum];
______________
[~ P];)
(sequent ~l ()
[P => falsum] >> Q;
______________
[~ P] >> Q;)
(sequent lemma (Q : prop)
Q;
Q >> P;
_______
P;)
(sequent lem (P : prop)
[P v [~ P]] >> Q;
_________________
Q;)
(sequent exp ()
falsum;
_______
P;)
(define remove-nth
{number --> (list A) --> (list A)}
1 [_ | Y] -> Y
N [X | Y] -> [X | (remove-nth (- N 1) Y)])
(sequent thin (N : number)
let Hypotheses (remove-nth N Hypotheses)
P;
_________________________________________
P;)
(define exchange
{number --> number --> (list A) --> (list A)}
M N X -> X where (or (= M 0) (= N 0))
1 N [X | Y] -> (let Z (nth N [X | Y])
[Z | (insert-nth X (- N 1) Y)])
M 1 [X | Y] -> (let Z (nth M [X | Y])
[Z | (insert-nth X (- M 1) Y)])
M N [X | Y] -> [X | (exchange (- M 1) (- N 1) Y)])
(define insert-nth
{A --> number --> (list A) --> (list A)}
X 1 [_ | Y] -> [X | Y]
X N [Y | Z] -> [Y | (insert-nth X (- N 1) Z)])
(sequent swap (M : number N : number)
let Hypotheses (exchange M N Hypotheses)
P;
_________________________________________
P;)
(sequent =r ()
_______
[X = X];)
(define replace
{term --> term --> prop --> prop}
Tm _ [all V P] -> [all V P] where (== Tm V)
Tm _ [exists V P] -> [exists V P] where (== Tm V)
Tm V [all X Y] -> [all X (replace Tm V Y)]
Tm V [exists X Y] -> [exists X (replace Tm V Y)]
Tm V [P v Q] -> [(replace Tm V P) v (replace Tm V Q)]
Tm V [P & Q] -> [(replace Tm V P) & (replace Tm V Q)]
Tm V [P => Q] -> [(replace Tm V P) => (replace Tm V Q)]
Tm V [P <=> Q] -> [(replace Tm V P) <=> (replace Tm V Q)]
Tm V [~ P] -> [~ (replace Tm V P)]
Tm V [X = Y] -> [(replace* Tm V X) = (replace* Tm V Y)]
Tm V [F | Terms] -> [F | (map (/. Term (replace* Tm V Term)) Terms)] where (atomic? [F | Terms])
_ _ P -> P)
(define replace*
{term --> term --> term --> term}
Tm V V -> Tm
Tm V [Func | Tms] -> [Func | (map (/. Term (replace* Tm V Term)) Tms)]
_ _ Term -> Term)
(sequent =l ()
let PX/Y (replace X Y P)
[X = Y] >> PX/Y;
________________________
[X = Y] >> P;)
(sequent alll (T : term)
let PX/T (replace X T P)
PX/T, [all X P] >> Q;
________________________
[all X P] >> Q;)
(sequent allr (T : term)
if (= (occurrences T Hypotheses) 0)
let PX/T (replace X T P)
PX/T;
________________________
[all X P];)