use(beta).
use(pbeta).

% Proof by induction over beta:
% beta ist Teilmenge von pbeta

beta(app(abs(s),t),subst(s,0,t)) => pbeta(app(abs(s),t),subst(s,0,t)),

((beta(s,t) and pbeta(s,t)) => (pbeta(app(u,s),app(u,t)) and
                                pbeta(app(s,u),app(t,u)))),

((beta(s,t) and pbeta(s,t)) => pbeta(abs(s),abs(t))) -> [].

option([var_overlaps(off),search_depth(0)]).
:-sarp(+[15]),saci([2]).


/*
Proof:
======

   1 : beta(app(abs(A),B),subst(A,0,B))                                 [input]
   9 : pbeta(A,B) -> pbeta(abs(A),abs(B))                               [input]
  10 : pbeta(A,B) -> pbeta(C,D)=>pbeta(app(A,C),app(B,D))               [input]
  11 : pbeta(A,B) -> pbeta(C,D)=>pbeta(app(abs(A),C),subst(B,0,D))      [input]
  12 : pbeta(A,A)                                                       [input]
  13 : beta(app(abs(s),t),subst(s,0,t))=>pbeta(app(abs(s),t),subst(s,0,t)),beta(s,t)and pbeta(s,t)=>pbeta(app(u,s),app(u,t))and pbeta(app(s,u),app(t,u)),beta(s,t)and pbeta(s,t)=>pbeta(abs(s),abs(t)) ->  [input]
  15 : pbeta(A,B),pbeta(C,D) -> pbeta(app(A,C),app(B,D))    [expansion from 10]
  16 : pbeta(A,B),pbeta(C,D) -> pbeta(app(abs(A),C),subst(B,0,D)) [expansion from 11]
  17 : beta(s,t)and pbeta(s,t)=>pbeta(abs(s),abs(t)),beta(s,t)and pbeta(s,t)=>pbeta(app(u,s),app(u,t))and pbeta(app(s,u),app(t,u)) ->  [reduction of 13 by [16,12,12,1,L]]
  18 : p$199,beta(s,t)and pbeta(s,t)=>pbeta(app(u,s),app(u,t))and pbeta(app(s,u),app(t,u)) ->  [expansion from 17]
  19 : p$199,beta(s,t)and pbeta(s,t)                        [expansion from 17]
  20 : pbeta(abs(s),abs(t)) -> p$199                        [expansion from 17]
  21 : p$198,p$199 ->                                       [expansion from 18]
  22 : p$198,beta(s,t)and pbeta(s,t)                        [expansion from 18]
  23 : pbeta(app(u,s),app(u,t))and pbeta(app(s,u),app(t,u)) -> p$198 [expansion from 18]
  24 : beta(s,t)and pbeta(s,t)                   [reduction of 22 by [21,19,L]]
  25 : pbeta(app(u,s),app(u,t)),pbeta(app(s,u),app(t,u)) -> p$198 [expansion from 23]
  27 : pbeta(s,t)                                           [expansion from 24]
  28 : pbeta(s,t) -> p$199                     [negative chaining of 9 from 20]
  29 : p$199                                          [reduction of 28 by [27]]
  30 : p$198 ->                                       [reduction of 21 by [29]]
  31 : false                      [reduction of 25 by [15,27,12,15,12,27,30,L]]

Length = 22, Depth = 10



Total time: 3880 milliseconds

Number of forward inferences: 1
Number of tableau inferences: 8
Number of kept clauses: 24
*/