copy(A, B, Proof) :- 				%If all true, copy rule is true.
    A < B, 							%Row copied to is higher than row copied from.

    get_rule(B, Proof, Rule), 		%Get rule of row copied to.
    Rule = copy(A),					%Check that the rule is equal to copy of row A.

    get_prop(A, Proof, PropA), 		%Get proposition of row being copied from.
    get_prop(B, Proof, PropB), 		%Get proposition of row being copied to.

    PropA = PropB.					%Are the proposition of the rows equal to each other.
									%__ADD FUNCTIONALLITY OF BOXES__

andint(A, B, C, Proof) :-			%If all true, copy rule is true.
    A < C, 							%Left conjunction cannot be on a row after the row with the andint rule.
    B < C,							%Right conjunction cannot be on a row after the row with the andint rule.

    get_rule(C, Proof, Rule),		%Get rule of row being introducted an and.
    Rule = andint(A, B),			%Check that the rule is equal to andint of row A and B.

    get_prop(A, Proof, PropA),		%Get proposition of row being andint:ed from on the left conjunction.
    get_prop(B, Proof, PropB),		%Get proposition of row being andint:ed from on the right conjunction.
	get_prop(C, Proof, PropC),		%Get proposition of row being andint:ed to.

    and(PropA, PropB) = PropC.		%Check that the and of PropA and PropB is the same as PropC.

andel1(A, B, Proof) :-				%If all true, andel1 rule is true.
    A < B,							%Row copied to is higher than row copied from.

    get_rule(B, Proof, Rule),		%Get rule of row copied to.
    Rule = andel1(A),				%Check that the rule is equal to andel1 of row A.

    get_prop(A, Proof, PropA), 		%Get proposition of row being copied from.
    get_prop(B, Proof, PropB), 		%Get proposition of row being copied to.

    get_pred_of_prop(PropA, PredA), %Get predicate of row being andel1:ed from.
    get_pred_l(PredA, PredLeftA),	%Get the left conjunction of the predicate (left predicate).

    PredLeftA = PropB.				%Check that the left predicate of the conjunction is the same as the prop of PropB

andel2(A, B, Proof) :-				%If all true, andel2 rule is true.
    A < B,							%Row copied to is higher than row copied from.

    get_rule(B, Proof, Rule),		%Get rule of row copied to.
    Rule = andel2(A),				%Check that the rule is equal to andel2 of row A.

    get_prop(A, Proof, PropA), 		%Get proposition of row being copied from.
    get_prop(B, Proof, PropB), 		%Get proposition of row being copied to.

    get_pred_of_prop(PropA, PredA), %Get predicate of row being andel1:ed from.
    get_pred_r(PredA, PredRightA),	%Get the right conjunction of the predicate (right predicate).

    PredRightA = PropB.				%Check that the right predicate of the conjunction is the same as the prop of PropB

orint1(A, B, C, Proof) :-			%If all true, andel2 rule is true.
    A < C,							%Row copied to is higher than row copied from.
    B < C,

    get_rule(C, Proof, Rule),		%Get rule of row copied to.
    Rule = orint1(A, B), 			%Check that the rule is equal to or of row A.

    get_prop(A, Proof, PropA), 		%Get proposition of row being copied from.
    get_prop(C, Proof, PropC), 		%Get proposition of row being copied to.

    get_pred_of_prop(PropC, PredC), %Get predicate of row being orint1:ed from.
    get_pred_l(PredC, PredLeftC),	%Get the left conjunction of the predicate (right predicate).

    PredLeftC = PropA.				%Check that the right predicate of the conjunction is the same as the prop of PropB

orint2(A, B, C, Proof) :-			%If all true, andel2 rule is true.
    A < C,
    B < C,
    %Row copied to is higher than row copied from.

    get_rule(C, Proof, Rule),		%Get rule of row copied to.
    Rule = orint2(A, B), 			%Check that the rule is equal to or of row A.

    get_prop(B, Proof, PropB), 		%Get proposition of row being copied from.
    get_prop(C, Proof, PropC), 		%Get proposition of row being copied to.

    get_pred_of_prop(PropC, PredC), %Get predicate of row being orint1:ed from.
    get_pred_r(PredC, PredRightC),	%Get the left conjunction of the predicate (right predicate).

    PredRightC = PropB.				%Check that the right predicate of the conjunction is the same as the prop of PropB

orel(X, A, B, C, D, E, Proof) :-
    A < B,
    C < D,
    B < E,
    D < E,
    X < E,

    get_rule(E, Proof, Rule),
    Rule = orel(X, A, B, C, D),

    get_prop(B, Proof, PropB),
    get_prop(D, Proof, PropD),

    PropB = PropD.
										%__ADD FUNCTIONALLITY OF BOXES__

impint(A, B, C, Proof) :-
    A < B,
    A < C,
    B < C,

    get_rule(C, Proof, Rule),
    Rule = impint(A, B),

    get_prop(A, Proof, PropA),
    get_prop(B, Proof, PropB),
    get_prop(C, Proof, PropC),

    get_pred_of_prop(PropC, PredC),
    get_pred_l(PredC, PredLeftC),
    get_pred_r(PredC, PredRightC),

    PropA = PredLeftC,
    PropB = PredRightC.


impel(A, B, C, Proof) :-
    A < C,
    B < C,

    get_rule(C, Proof, Rule),
    Rule = impel(A, B),

    get_prop(A, Proof, PropA),
    get_prop(B, Proof, PropB),
    get_prop(C, Proof, PropC),

    get_pred_of_prop(PropB, PredB),
    get_pred_l(PredB, PredLeftB),
    get_pred_r(PredB, PredRightB),

    PropA = PredLeftB,
    PropC = PredRightB.

negint(A, B, C, Proof) :-
    A < B,
    A < C,
    B < C,

    get_rule(C, Proof, Rule),
    Rule = negint(A, B),

    get_prop(A, Proof, PropA),
    get_prop(B, Proof, PropB),
    get_prop(C, Proof, PropC),

    get_pred_of_prop(PropC, PredC),
    get_pred_l(PredC, PredLeftC),

    PropA = PredLeftC,
    PropB = cont.


negel(A, B, C, Proof) :-
    A < C,
    B < C,

    get_rule(C, Proof, Rule),
    Rule = negel(A, B),

    get_prop(A, Proof, PropA),
    get_prop(B, Proof, PropB),
    get_prop(C, Proof, PropC),

    get_pred_of_prop(PropB, PredB),
    get_pred_l(PredB, PredLeftB),

    PropA = PredLeftB,
    PropC = cont.

contel(A, B, Proof) :-
    A < B,

    get_rule(B, Proof, Rule),
    Rule = contel(A),

    get_prop(A, Proof, PropA),

    PropA = cont.

negnegint(A, B, Proof) :-
    A < B,

    get_rule(B, Proof, Rule),
    Rule = negnegint(A),

    get_prop(A, Proof, PropA),
    get_prop(B, Proof, PropB),

    get_pred_of_prop(PropB, PredB),
    get_pred_l(PredB, PredLeftB),
    get_pred_of_prop(PredLeftB, PredBB),
    get_pred_l(PredBB, PredLeftBB),

    PropA = PredLeftBB.

negnegel(A, B, Proof) :-
    A < B,

    get_rule(B, Proof, Rule),
    Rule = negnegel(A),

    get_prop(A, Proof, PropA),
    get_prop(B, Proof, PropB),

    get_pred_of_prop(PropA, PredA),
    get_pred_l(PredA, PredLeftA),
    get_pred_of_prop(PredLeftA, PredAA),
    get_pred_l(PredAA, PredLeftAA),

    PropB = PredLeftAA.

mt(A, B, C, Proof) :-
    A < C,
    B < C,

    get_rule(C, Proof, Rule),
    Rule = mt(A, B),

    get_prop(A, Proof, PropA),
    get_prop(B, Proof, PropB),
    get_prop(C, Proof, PropC),

    get_pred_of_prop(PropA, PredA),
    get_pred_l(PredA, PredLeftA),
    get_pred_r(PredA, PredRightA),

    neg(PredLeftA) = PropC,
    neg(PredRightA) = PropB.

pbc(A, B, C, Proof) :-
    A < B,
    B < C,

    get_rule(C, Proof, Rule),
    Rule = pcb(A, B),

    get_prop(A, Proof, PropA),
    get_prop(B, Proof, PropB),
    get_prop(C, Proof, PropC),

    get_pred_of_prop(PropA, PredA),
    get_pred_l(PredA, PredLeftA),


    neg(PredLeftA) = PropC,
    cont = PropB.

lem(A, Proof) :-
    get_rule(A, Proof, Rule),
    Rule = lem,

    get_prop(A, Proof, PropA),

    get_pred_of_prop(PropA, PredA),
    get_pred_l(PredA, PredLeftA),
    get_pred_r(PredA, PredRightA),

    neg(PredLeftA) = PredRightA,
	PropA = and(PredLeftA, PredRightA).