verify(InputFileName) :- see(InputFileName),
read(Prems), read(Goal), read(Proof),
seen,
valid_proof(Prems, Goal, Proof).

valid_proof([H|T], G, [H2|T2]) :- findlast([H2|T2], _, [_|[G|_]]), check_rules([H|T], [H2|T2], [H2|T2], 1).

findlast([X], [], X).
findlast([H | T], [H | N], X) :- findlast(T, N, X).

check_rules([_|_], [[]], _, _).
check_rules([_|_], [], _, _).
check_rules([H|T], [[_|[T1|_]]|T2], Proof, Count) :- get_rule(Proof, Count, [R|_]), (R == premise, get_prop(Proof, Count, Prop), check_premise(Prop, [H|T]) ;
                                              R == assumption, check_assumption(Proof, Count) ;
                                              R = copy(_), get_pred_of_prop(R, [_|[Num|_]]), copy(Num, Count, Proof) ;
                                              R = andint(_, _), get_pred_of_prop(R, [_|[A|[B|_]]]), andint(A, B, Count, Proof) ;
                                              R = andel1(_), get_pred_of_prop(R, [_|[Num|_]]), andel1(Num, Count, Proof) ;
                                              R = andel2(_), get_pred_of_prop(R, [_|[Num|_]]), andel2(Num, Count, Proof) ;
                                              R = orint1(_), get_pred_of_prop(R, [_|[Num|_]]), orint1(Num, Count, Proof) ;
                                              R = orint2(_), get_pred_of_prop(R, [_|[Num|_]]), orint2(Num, Count, Proof) ;
                                              R = impel(_, _), get_pred_of_prop(R, [_|[A|[B|_]]]), impel(A, B, Count, Proof) ;
                                              R = negint(_, _), get_pred_of_prop(R, [_|[A|[B|_]]]), negint(A, B, Count, Proof)),
                                              C1 is Count + 1,
    										  (not(is_list(T1)), check_rules([H|T], T2, Proof, C1) ; check_rules([H|T], [T1|T2], Proof, C1)).

check_assumption(Proof, Num) :- row_depth(Proof, Num, Depth), is_list(Depth), findlast(Depth, [_|_], 1).

check_premise(Result, H) :- Result == H.
check_premise(Result, [H|T]) :- Result == H ; check_premise(Result, T).


find_row([[[[H|T]|_]|_]|_], H, [H|T]).
find_row([[[H|T]|_]|_], H, [H|T]).
find_row([[H|T]|_], H, [H|T]).
find_row([[[Hf|Tf]|T2]|[[H|T3]|T4]], Num, Result) :- less_than(H, Num), find_row([[H|T3]|T4], Num, Result) ; find_row([[Hf|Tf]|T2], Num, Result).
find_row([[_|[T1|_]]|T2], Num, Result) :- (not(is_list(T1)), find_row(T2, Num, Result) ; find_row([T1|T2], Num, Result)).

less_than(H, Num) :- is_list(H), get_list_head(H, P), less_than(P, Num) ; not(is_list(H)), H =< Num.
get_list_head([H|_], H).

depth(X, [X|_], [C], C).
depth(X, [H|_], [C|D], C) :- depth(X, H, D, 1).
depth(X, [_|T], D, C) :- C1 is C+1, depth(X, T, D, C1).

row_depth(Proof, Row, Depth) :- find_row(Proof, Row, FullRow), depth(FullRow, Proof, Depth, 1).

find_row_and_depth(Proof, Num, Row, Depth) :- find_row(Proof, Num, Row), row_depth(Row, Proof, Depth).

get_prop(Proof, Num, Prop) :- find_row(Proof, Num, [_|[Prop|_]]).

get_rule(Proof, Num, Rule) :- find_row(Proof, Num, [_|[_|Rule]]).

get_pred_of_prop(L, List) :- L =.. List.

lesser_depth([_], _).
lesser_depth([Ha|Ta], [Hb|Tb]) :- Ha is Hb, lesser_depth(Ta, Tb).

valid_depth(Proof, RowA, RowB) :- row_depth(Proof, RowA, DepthA), row_depth(Proof, RowB, DepthB),
                            lesser_depth(DepthA, DepthB).
valid_depth_box(Proof, RowBox, RowB) :- depth(RowBox, Proof, DepthBox, 1), row_depth(Proof, RowB, DepthB),
                            lesser_depth(DepthBox, DepthB).

check_box(Proof, Start, End, R) :- Start < End, row_depth(Proof, Start, [Hs|Ts]), row_depth(Proof, End, [Hs|Ts]), C1 is End+1, row_depth(Proof, C1, [H|T]), not(H is Hs), not(T is Ts), findlast(Ts, R, _).

copy(A, B, Proof) :-
    A < B,
    get_prop(Proof, A, PropA),
    get_prop(Proof, B, PropB),
    PropA==PropB, valid_depth(Proof, A, B).

andint(A, B, C, Proof) :-
    A < C,
    B < C,
    get_prop(Proof, A, PropA),
    get_prop(Proof, B, PropB),
    get_prop(Proof, C, PropC),

    and(PropA, PropB) = PropC,
    valid_depth(Proof, A, C), valid_depth(Proof, B, C).

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

    get_rule(Proof, B, [Rule|_]),
    Rule = andel1(A),

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

    get_pred_of_prop(PropA, [_ | [PredLeftA | _]]),

    PredLeftA = PropB,
    valid_depth(Proof, A, B).

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

    get_rule(Proof, B, [Rule|_]),
    Rule = andel2(A),

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

    get_pred_of_prop(PropA, [_ | [_ | [PredRightA | _]]]),

    PredRightA = PropB,
    valid_depth(Proof, A, B).

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

    get_rule(Proof, B, [Rule|_]),
    Rule = orint1(A),

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

    get_pred_of_prop(PropB, [_ | [PredLeftB | _]]),

    PredLeftB = PropA,
    valid_depth(Proof, A, B).

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

    get_rule(Proof, B, [Rule|_]),
    Rule = orint2(A),

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

    get_pred_of_prop(PropB, [_ | [_ | [PredRightB | _]]]),

    PredRightB = PropA,
    valid_depth(Proof, A, B).

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

    get_rule(Proof, C, [Rule|_]),
    Rule = impel(A, B),

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

    ((get_pred_of_prop(PropB, [_ | [PredLeftB | [PredRightB | _]]]),
    PropA = PredLeftB,
    PropC = PredRightB) ;
    (get_pred_of_prop(PropA, [_ | [PredLeftA | [PredRightA | _]]]),
    PropB = PredLeftA,
    PropC = PredRightA)),

    valid_depth(Proof, A, C), valid_depth(Proof, B, C).

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

      check_box(Proof, A, B, Indexlist),
      valid_depth_box(Proof, Indexlist, 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.