// Adapted from Nguyen Huu Hai's example
// Must be executed on non-empty list
// If a is already stored, ignore.

void insert(node2 x, int a)
{
  // <0> 
  if (a < x->val) { 
    //if a is lower, we go down in the left subtree
    // <1>
    if (x->left == NULL) {
      // <2> 
      x = x->left = new node2(a,NULL,NULL);
    } else {
      // <3> 
      insert(x->left,a); // x = x->left; goto <0>
    }
  } else if (a > x->val) {
    //if a is bigger, we go down on the right subtree
    // <4>
    if (x->right == NULL) {
      // <5>
      x = x->right = new node2(a,NULL,NULL);
    } else {
      // <6>
      insert(x->right,a); // x = x->right; goto <0>
    }
  } // if a == x->val, do nothing
  // <7>
}


CLP Specification:
==================

path(H,X,X,E,{X}).
path(H,X,Y,E,S) :-
    T * {X} = S, H[X+1]!=null, E<H[X], path(H,H[X+1],Y,E,T).
path(H,X,Y,E,S) :-
    T * {X} = S, H[X+2]!=null, E>H[X], path(H,H[X+2],Y,E,T).

bst(H,X,{X}) :-
    H[X+1]=null, H[X+2]=null.
bst(H,X,S) :-
    H[X+1]!=null, H[X]>max(H[SL]), bst(H,H[X+1],SL),
    H[X+2]!=null, H[X]<min(H[SR]), bst(H,H[X+2],SR),
    SL * SR * {X} = S.
bst(H,X,S) :-
    H[X+1]!=null, H[X]>max(H[SL]), bst(H,H[X+1],SL),
    H[X+2]=null,
    SL * {X} = S.
bst(H,X,S) :-
    H[X+1]=null, 
    H[X+2]!=null, H[X]<min(H[SR]), bst(H,H[X+2],SR),
    SR * {X} = S.

-------------------------------------------------------------------------------

Assertion:
==========

N0:
p(0,H,X,A,Hf,Xf), X0=X, X!=null, bst(H,X0,S)
|= bst(Hf,X0,?U), max(H[?U])=max(cup({A},H[S])), min(H[?U])=min(cup({A},H[S]))

N0': LEFT GENERALIZE N0 (Yet to be proved)
p(0,H,X,A,Hf,Xf), path(H,X0,X,A,T), bst(H,X0,S), in(X,S)
|= bst(Hf,X0,?U), max(H[?U])=max(cup({A},H[S])), min(H[?U])=min(cup({A},H[S]))

N1a: LEFT UNFOLD N0'
p(7,H,X,A,Hf,Xf), path(H,X0,X,A,T), bst(H,X0,S), in(X,S), H[X]=A
|= bst(Hf,X0,?U), max(H[?U])=max(cup({A},H[S])), min(H[?U])=min(cup({A},H[S]))

N1b: LEFT UNFOLD N0'
p(1,H,X,A,Hf,Xf), path(H,X0,X,A,T), bst(H,X0,S), in(X,S), A<H[X]
|= bst(Hf,X0,?U), max(H[?U])=max(cup({A},H[S])), min(H[?U])=min(cup({A},H[S]))

N2: LEFT UNFOLD N1a
path(Hf,X0,Xf,A,T), bst(Hf,X0,S), in(Xf,S), Hf[Xf]=A
|= bst(Hf,X0,?U), max(H[?U])=max(cup({A},H[S])), min(H[?U])=min(cup({A},H[S]))

N2.1: ?U->S
path(Hf,X0,Xf,A,T), bst(Hf,X0,S), in(Xf,S), Hf[Xf]=A
|= bst(Hf,X0,S), max(H[S])=max(cup({A},H[S])), min(H[S])=min(cup({A},H[S]))
STOP: DIRECT PROOF (cup({A},H[S]) = H[S] since in(Xf,S))

= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =

N4: LEFT UNFOLD N1b
p(2,H,X,A,Hf,Xf), path(H,X0,X,A,T), bst(H,X0,S), in(X,S), A<H[X], H[X+1]=null
|= bst(Hf,X0,?U), max(H[?U])=max(cup({A},H[S])), min(H[?U])=min(cup({A},H[S]))

N5: LEFT UNFOLD N4
p(7,H',X',A,Hf,Xf), path(H,X0,X,A,T), bst(H,X0,S),
in(X,S), A<H[X], H[X+1]=null, {New} * S,
H'=<H,X+1,New>, New!=null, H[New]=A, H[New+1]=null, H[New+2]=null, X'=H'[X+1]
|= bst(Hf,X0,?U), max(H[?U])=max(cup({A},H[S])), min(H[?U])=min(cup({A},H[S]))

N6: LEFT UNFOLD N5
path(H,X0,X,A,T), bst(H,X0,S), in(X,S), A<H[X], H[X+1]=null, {New} * S,
Hf=<H,X+1,New>, New!=null, H[New]=A, H[New+1]=null, H[New+2]=null, Xf=Hf[X+1]
|= bst(Hf,X0,?U), max(H[?U])=max(cup({A},H[S])), min(H[?U])=min(cup({A},H[S]))

N7: REMOVE Hf, Xf
path(H,X0,X,A,T),
bst(H,X0,S), in(X,S), A<H[X], H[X+1]=null, {New} * S,
New!=null, H[New]=A, H[New+1]=null, H[New+2]=null, Xf=Hf[X+1]
|=
bst(<H,X+1,New>,X0,?U),
max(H[?U])=max(cup({A},H[S])), min(H[?U])=min(cup({A},H[S]))

N8a: LEFT UNFOLD N7 path (rule 1)
bst(H,X,S), in(X,S), A<H[X], H[X+1]=null, {New} * S,
New!=null, H[New]=A, H[New+1]=null, H[New+2]=null, Xf=Hf[X+1]
|=
bst(<H,X+1,New>,X,?U),
max(H[?U])=max(cup({A},H[S])), min(H[?U])=min(cup({A},H[S]))

= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = 

N9a: LEFT UNFOLD N8a (bst rule 1)
H[X+1]=null,
H[X+2]=null,
in(X,{X}),
A<H[X],
{New} * {X},
New!=null,
H[New]=A,
H[New+1]=null,
H[New+2]=null,
Xf=Hf[X+1]
|=
bst(<H,X+1,New>,X,?U),
max(H[?U])=max(cup({A},H[{X}])),
min(H[?U])=min(cup({A},H[{X}]))

N11: RIGHT UNFOLD N9a (3rd rule of bst)
H[X+1]=null,
H[X+2]=null,
in(X,{X}),
A<H[X],
{New} * {X},
New!=null,
H[New]=A,
H[New+1]=null,
H[New+2]=null,
Xf=Hf[X+1]
|=
max(H[?U])=max(cup({A},H[{X}])),
min(H[?U])=min(cup({A},H[{X}])),
<H,X+1,New>[X+1]!=null,
<H,X+1,New>[X] > max(<H,X+1,New>[?SL]),
bst(<H,X+1,New>,<H,X+1,New>[X+1],?SL),
<H,X+1,New>[X+2]=null,
?SL * {X} = ?U.

N13: RIGHT UNFOLD N11 (bst 1st rule)
H[X+1]=null,
H[X+2]=null,
in(X,{X}),
A<H[X],
{New} * {X},
New!=null,
H[New]=A,
H[New+1]=null,
H[New+2]=null,
Xf=Hf[X+1]
|=
max(H[{New} * {X}])=max(cup({A},H[{X}])),
min(H[{New} * {X}])=min(cup({A},H[{X}])),
H[X] > max(<H,X+1,New>[{New}]),
<H,X+1,New>[New+1]=null,
<H,X+1,New>[New+2]=null,
<H,X+1,New>[X+1]!=null
<H,X+1,New>[X+2]=null

N14: RIGHT SIMPLIFY N13 (AIP)
H[X]>max(<H,X+1,New>[{New}]) == H[X]>A           (X+1 != New, H[New]=A)
<H,X+1,New>[New+1]=null == H[New+1]=null         (X+1 != New)
<H,X+2,New>[New+1]=null == H[New+2]=null         (X+2 != New)
<H,X+1,New>[X+1]!=null == New!=null
<H,X+1,New>[X+2]=null  == H[X+2]=null

H[X+1]=null,
H[X+2]=null,
in(X,{X}),
A<H[X],
{New} * {X},
New!=null,
H[New]=A,
H[New+1]=null,
H[New+2]=null,
Xf=Hf[X+1]
|=
max(H[{New} * {X}])=max(cup({A},H[{X}])),
min(H[{New} * {X}])=min(cup({A},H[{X}])),
H[X] > A,
H[New+1]=null,
H[New+2]=null,
New!=null, 
H[X+2]=null.
DP

--------------------------------------------------------------------------------

N9b: LEFT UNFOLD N8a (4th rule of bst)
H[X+2]!=null,
H[X]<min(H[SR]),
bst(H,H[X+2],SR),
in(X,SR * {X}),
A<H[X],
H[X+1]=null,
{New} * SR * {X},
New!=null,
H[New]=A,
H[New+1]=null,
H[New+2]=null,
Xf=Hf[X+1]
|=
bst(<H,X+1,New>,X,?U),
max(H[?U])=max(cup({A},H[SR * {X}])),
min(H[?U])=min(cup({A},H[SR * {X}]))

N15: RIGHT UNFOLD N9b (2nd rule of bst)
H[X+2]!=null,
H[X]<min(H[SR]),
bst(H,H[X+2],SR),
in(X,SR * {X}),
A<H[X],
H[X+1]=null,
{New} * SR * {X},
New!=null,
H[New]=A,
H[New+1]=null,
H[New+2]=null,
Xf=Hf[X+1]
|=
<H,X+1,New>[X+1]!=null, 
<H,X+1,New>[X]>max(<H,X+1,New>[?SL]),
bst(<H,X+1,New>,<H,X+1,New>[X+1],?SL),
<H,X+1,New>[X+2]!=null, 
<H,X+1,New>[X]<min(<H,X+1,New>[?SR1]),
bst(<H,X+1,New>,<H,X+1,New>[X+2],?SR1),
max(H[?SL * ?SR1 * {X}])=max(cup({A},H[SR * {X}])),
min(H[?SL * ?SR1 * {X}])=min(cup({A},H[SR * {X}]))

N16: RU N15 (bst rule 1)
H[X+2]!=null,
H[X]<min(H[SR]),
bst(H,H[X+2],SR),
in(X,SR * {X}),
A<H[X],
H[X+1]=null,
{New} * SR * {X},
New!=null,
H[New]=A,
H[New+1]=null,
H[New+2]=null,
Xf=Hf[X+1]
|=
<H,X+1,New>[X+1]!=null, 
<H,X+1,New>[X]>max(<H,X+1,New>[<H,X+1,New>[X+1]]),
<H,X+1,New>[<H,X+1,New>[X+1]+1]=null,
<H,X+1,New>[<H,X+1,New>[X+1]+2]=null.
<H,X+1,New>[X+2]!=null, 
<H,X+1,New>[X]<min(<H,X+1,New>[?SR1]),
bst(<H,X+1,New>,<H,X+1,New>[X+2],?SR1),
max(H[{<H,X+1,New>[X+1]} * ?SR1 * {X}])=max(cup({A},H[SR * {X}])),
min(H[{<H,X+1,New>[X+1]} * ?SR1 * {X}])=min(cup({A},H[SR * {X}]))

N17: ?SR1 -> SR
H[X+2]!=null,
H[X]<min(H[SR]),
bst(H,H[X+2],SR),
in(X,SR * {X}),
A<H[X],
H[X+1]=null,
{New} * SR * {X},
New!=null,
H[New]=A,
H[New+1]=null,
H[New+2]=null,
Xf=Hf[X+1]
|=
<H,X+1,New>[X+1]!=null, 
<H,X+1,New>[X]>max(<H,X+1,New>[<H,X+1,New>[X+1]]),
<H,X+1,New>[<H,X+1,New>[X+1]+1]=null,
<H,X+1,New>[<H,X+1,New>[X+1]+2]=null,
<H,X+1,New>[X+2]!=null, 
<H,X+1,New>[X]<min(<H,X+1,New>[SR]),
bst(<H,X+1,New>,<H,X+1,New>[X+2],SR),
max(H[{<H,X+1,New>[X+1]} * SR * {X}])=max(cup({A},H[SR * {X}])),
min(H[{<H,X+1,New>[X+1]} * SR * {X}])=min(cup({A},H[SR * {X}]))

N18: SIMPLIFY N17
         <H,X+1,New>[X]     == H[X]                       X != X+1
         <H,X+1,New>[X+1]   == New                        X+1 = X+1
         <H,X+1,New>[X+2]   == H[X+2]                     X+1 != X+2
         <H,X+1,New>[New]   == H[New]                     {New} * SR * X
         <H,X+1,New>[New+1] == H[New+1]                   {New} * SR * X
         <H,X+1,New>[New+2] == H[New+2]                   {New} * SR * X
         <H,X+1,New>[SR]    == H[SR]                      {New} * SR * X
         bst(<H,X+1,New>,H[X+2],SR) == bst(H,H[X+2],SR)   {New} * SR * X

H[X+2]!=null,
H[X]<min(H[SR]),
bst(H,H[X+2],SR),
in(X,SR * {X}),
A<H[X],
H[X+1]=null,
{New} * SR * {X},
New!=null,
H[New]=A,
H[New+1]=null,
H[New+2]=null,
Xf=Hf[X+1]
|=
New!=null, 
H[X]>max(H[New]),
H[New+1]=null,
H[New+2]=null,
H[X+2]!=null, 
H[X]<min(<H,X+1,New>[SR]),
bst(H,H[X+2],SR),
max(H[{New} * SR * {X}])=max(cup({A},H[SR * {X}])),
min(H[{New} * SR * {X}])=min(cup({A},H[SR * {X}]))
DP

-------------------------------------------------------------------------------

N8b: LEFT UNFOLD N7 (path 2nd rule)
path(H,H[X0+1],X,A,T1),
bst(H,X0,S),
T1 * {X0} = T,
H[X0+1]!=null,
A<H[X0],
in(X,S),
A<H[X],
H[X+1]=null,
{New} * S,
New!=null,
H[New]=A,
H[New+1]=null,
H[New+2]=null,
Xf=Hf[X+1]
|=
bst(<H,X+1,New>,X0,?U),
max(H[?U])=max(cup({A},H[S])),
min(H[?U])=min(cup({A},H[S]))

N21: LEFT UNFOLD N8b (bst 2nd rule)
path(H,H[X0+1],X,A,T1),
bst(H,H[X0+1],SL),
bst(H,H[X0+2],SR),
T1 * {X0} = T,
SL * SR * {X0} = S,
in(X,S),
A<H[X],
H[X+1]=null,
{New} * S,
New!=null,
H[New]=A,
H[New+1]=null,
H[New+2]=null,
Xf=Hf[X+1],
H[X0+1]!=null,
H[X0+2]!=null,
A<H[X0], 
H[X0]>max(H[SL]),
H[X0]<min(H[SR]),
|=
bst(<H,X+1,New>,X0,?U),
max(H[?U])=max(cup({A},H[S])),
min(H[?U])=min(cup({A},H[S]))


N22: AP N21,N7
path(H,H[X0+1],X,A,T1),
bst(H,H[X0+1],SR),
SL * SR * {X0} = S,
in(X,S),
A<H[X],
H[X+1]=null,
{New} * S,
New!=null,
H[New]=A,
H[New+1]=null,
H[New+2]=null,
Xf=Hf[X+1],
bst(<H,X+1,New>,H[X0+1],U1),
max(H[U1])=max(cup({A},H[SR])),
min(H[U1])=min(cup({A},H[SR])),
T1 * {X0} = T,
H[X0+1]!=null,
A<H[X0], 
H[X0]>max(H[SL]),
bst(H,H[X0+1],SL),
H[X0+2]!=null,
H[X0]<min(H[SR]),
bst(H,H[X0+1],SR)
|=
bst(<H,X+1,New>,X0,?U),
max(H[?U])=max(cup({A},H[S])), min(H[?U])=min(cup({A},H[S]))


N23: RIGHT UNFOLD N22 (bst rule 2)
path(H,H[X0+1],X,A,T1),
bst(H,H[X0+1],SR),
SL * SR * {X0} = S,
in(X,S),
A<H[X],
H[X+1]=null,
{New} * S,
New!=null,
H[New]=A,
H[New+1]=null,
H[New+2]=null,
Xf=Hf[X+1],
bst(<H,X+1,New>,H[X0+1],U1),
max(H[U1])=max(cup({A},H[SR])),
min(H[U1])=min(cup({A},H[SR])),
T1 * {X0} = T,
H[X0+1]!=null,
A<H[X0], 
H[X0]>max(H[SL]),
bst(H,H[X0+1],SL),
H[X0+2]!=null,
H[X0]<min(H[SR]),
bst(H,H[X0+1],SR)
|=
<H,X+1,New>[X0+1]!=null, <H,X+1,New>[X0]>max(H[?SL1]),
bst(<H,X+1,New>,<H,X+1,New>[X0+1],?SL1),
<H,X+1,New>[X0+2]!=null, <H,X+1,New>[X0]<min(H[?SR1]),
bst(<H,X+1,New>,<H,X+1,New>[X0+1],?SR1),
?SL1 * ?SR1 * {X0} = ?U,
max(H[?U])=max(cup({A},H[S])), min(H[?U])=min(cup({A},H[S]))


--------------------------------------------------------------------------------

path(H,X,X,E,{X}).
path(H,X,Y,E,S) :-
    T * {X} = S, H[X+1]!=null, E<H[X], path(H,H[X+1],Y,E,T).
path(H,X,Y,E,S) :-
    T * {X} = S, H[X+2]!=null, E>H[X], path(H,H[X+2],Y,E,T).

bst(H,X,{X}) :-
    H[X+1]=null, H[X+2]=null.
bst(H,X,S) :-
    H[X+1]!=null, H[X]>max(H[SL]), bst(H,H[X+1],SL),
    H[X+2]!=null, H[X]<min(H[SR]), bst(H,H[X+2],SR),
    SL * SR * {X} = S.
bst(H,X,S) :-
    H[X+1]!=null, H[X]>max(H[SL]), bst(H,H[X+1],SL),
    H[X+2]=null,
    SL * {X} = S.
bst(H,X,S) :-
    H[X+1]=null, 
    H[X+2]!=null, H[X]<min(H[SR]), bst(H,H[X+2],SR),
    SR * {X} = S.







N22: COINDUCTION USING N7
bst(<H,X+1,New>,H[X0+1],min(A,Min),max(A,MaxL)),
A<H[X0], 
H[X0+1]!=null, H[X0]>MaxL, 
H[X0+2]!=null, H[X0]<MinR, bst(H,H[X0+2],MinR,Max),
no_visit(H,X0,H[X0+1],X,A),
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+1],H[X0+2])
|= bst(<H,X+1,New>,X0,min(A,Min),max(A,Max))

N23: RIGHT UNFOLD N22 (bst rule 2)
bst(<H,X+1,New>,H[X0+1],min(A,Min),max(A,MaxL)), A<H[X0], 
H[X0+1]!=null, H[X0]>MaxL, 
H[X0+2]!=null, H[X0]<MinR, bst(H,H[X0+2],MinR,Max),
no_visit(H,X0,H[X0+1],X,A),
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+1],H[X0+2])
|= 
<H,X+1,New>[X0+1]!=null, <H,X+1,New>[X0]>?MaxL1,
bst(<H,X+1,New>,<H,X+1,New>[X0+1],min(A,Min),?MaxL1),
<H,X+1,New>[X0+2]!=null, <H,X+1,New>[X0]<?MinR1,
bst(<H,X+1,New>,<H,X+1,New>[X0+2],?MinR1,max(A,Max)),
no_reach(<H,X+1,New>,X0,<H,X+1,New>[X0+1]),
no_reach(<H,X+1,New>,X0,<H,X+1,New>[X0+2]),
no_share(<H,X+1,New>,<H,X+1,New>[X0+1],<H,X+1,New>[X0+2])

N24: RIGHT SIMPLIFY N23 (NOTE: X0!=X DUE TO no_visit(H,X0,H[X0+1],X,A))
A<H[X0], 
H[X0+1]!=null, H[X0]>MaxL, bst(<H,X+1,New>,H[X0+1],min(A,Min),max(A,MaxL)),
H[X0+2]!=null, H[X0]<MinR, bst(H,H[X0+2],MinR,Max),
no_visit(H,X0,H[X0+1],X,A),
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+1],H[X0+2])
|= 
H[X0+1]!=null, H[X0]>?MaxL1, bst(<H,X+1,New>,H[X0+1],min(A,MinL),?MaxL1),
H[X0+2]!=null, H[X0]<?MinR1, bst(H,H[X0+2],?MinR1,max(A,Max)),
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+1],H[X0+2])

N25: RIGHT SPECIALIZE MaxL1 = max(A,MaxL), MinR1 = MinR
A<H[X0], 
H[X0+1]!=null, H[X0]>MaxL, bst(<H,X+1,New>,H[X0+1],min(A,Min),max(A,MaxL)),
H[X0+2]!=null, H[X0]<MinR, bst(H,H[X0+2],MinR,Max),
no_visit(H,X0,H[X0+1],X,A),
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+1],H[X0+2])
|= 
H[X0+1]!=null, H[X0]>max(A,MaxL),
bst(<H,X+1,New>,H[X0+1],min(A,MinL),max(A,MaxL)),
H[X0+2]!=null, H[X0]<MinR, bst(H,H[X0+2],MinR,max(A,Max)),
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+1],H[X0+2])
STOP: DIRECT PROOF

-------------------------------------------------------------------------------

N26: LEFT UNFOLD N20 USING bst (3rd rule)
path(H,H[X0+1],X,A), bst(H,H[X0+1],Min,MaxL), A<H[X], H[X+1]=null, 
New!=null, H[New]=A, H[New+1]=null, H[New+2]=null,
A<H[X0], H[X0+1]!=null, Max = H[X0], H[X0]>MaxL, H[X0+2]=null,
no_visit(H,X0,H[X0+1],X,A),
no_reach(H,X0,H[X0+1])
|= bst(<H,X+1,New>,X0,min(A,Min),max(A,Max))

N27: COINDUCTION USING N7
bst(<H,X+1,New>,H[X0+1],min(A,Min),max(A,MaxL)),
A<H[X0], H[X0+1]!=null, Max = H[X0], H[X0]>MaxL, H[X0+2]=null,
no_visit(H,X0,H[X0+1],X,A),
no_reach(H,X0,H[X0+1])
|= bst(<H,X+1,New>,X0,min(A,Min),max(A,Max))

N28: RIGHT UNFOLD N27 (3rd rule)
bst(<H,X+1,New>,H[X0+1],min(A,Min),max(A,MaxL)),
A<H[X0], H[X0+1]!=null, Max = H[X0], H[X0]>MaxL, H[X0+2]=null,
no_visit(H,X0,H[X0+1],X,A),
no_reach(H,X0,H[X0+1])
|= 
<H,X+1,New>[X0+1]!=null, <H,X+1,New>[X0]>?MaxL1, max(A,Max)=H[X0],
bst(<H,X+1,New>,<H,X+1,New>[X0+1],min(A,Min),?MaxL1),
<H,X+1,New>[X0+2]=null,
no_reach(<H,X+1,New>,X0,<H,X+1,New>[X0+1])

N29: SIMPLIFY N28 (X!=X0 DUE TO no_visit(H,X0,H[X0+1],X,A))
bst(<H,X+1,New>,H[X0+1],min(A,Min),max(A,MaxL)),
A<H[X0], H[X0+1]!=null, Max = H[X0], H[X0]>MaxL, H[X0+2]=null
no_visit(H,X0,H[X0+1],X,A),
no_reach(H,X0,H[X0+1])
|= 
H[X0+1]!=null, H[X0]>?MaxL1, max(A,Max)=H[X0],
bst(<H,X+1,New>,H[X0+1],min(A,Min),?MaxL1), H[X0+2]=null,
no_reach(H,X0,H[X0+1])

N30: RIGHT SPECIALIZE N29 WITH MaxL1=max(A,Max)
bst(<H,X+1,New>,H[X0+1],min(A,Min),max(A,MaxL)),
A<H[X0], H[X0+1]!=null, Max = H[X0], H[X0]>MaxL, H[X0+2]=null,
no_visit(H,X0,H[X0+1],X,A),
no_reach(H,X0,H[X0+1])
|= 
H[X0+1]!=null, H[X0]>max(A,MaxL), max(A,Max)=H[X0],
bst(<H,X+1,New>,H[X0+1],min(A,Min),max(A,MaxL)), H[X0+2]=null,
no_reach(H,X0,H[X0+1])
STOP: DIRECT PROOF

-------------------------------------------------------------------------------

N31: LEFT UNFOLD N7 (path 3rd rule)
path(H,H[X0+2],X,A), bst(H,X0,Min,Max), 
H[X0+2]!=null, A>H[X0], A<H[X], H[X+1]=null,
New!=null, H[New]=A, H[New+1]=null, H[New+2]=null,
no_visit(H,X0,H[X0+2],X,A)
|= bst(<H,X+1,New>,X0,min(A,Min),max(A,Max))

N32: LEFT UNFOLD N31 (bst 2nd rule)
path(H,H[X0+2],X,A), bst(H,H[X0+2],MinR,Max), A<H[X], H[X+1]=null,
New!=null, H[New]=A, H[New+1]=null, H[New+2]=null,
H[X0+1]!=null, H[X0]>MaxL, bst(H,H[X0+1],Min,MaxL),
H[X0+2]!=null, H[X0]<MinR, A>H[X0],
no_visit(H,X0,H[X0+2],X,A),
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+1],H[X0+2])
|= bst(<H,X+1,New>,X0,min(A,Min),max(A,Max))

N33: COINDUCTION ON N32 USING N7
A>H[X0],
H[X0+1]!=null, H[X0]>MaxL, bst(H,H[X0+1],Min,MaxL),
H[X0+2]!=null, H[X0]<MinR, bst(<H,X+1,New>,H[X0+2],min(A,MinR),max(A,Max)),
no_visit(H,X0,H[X0+2],X,A),
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+1],H[X0+2])
|= bst(<H,X+1,New>,X0,min(A,Min),max(A,Max))

N34: RIGHT UNFOLD N33 (bst 2nd rule)
A>H[X0],
H[X0+1]!=null, H[X0]>MaxL, bst(H,H[X0+1],Min,MaxL),
H[X0+2]!=null, H[X0]<MinR, bst(<H,X+1,New>,H[X0+2],min(A,MinR),max(A,Max)),
no_visit(H,X0,H[X0+2],X,A),
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+1],H[X0+2])
|=
<H,X+1,New>[X0+1]!=null, <H,X+1,New>[X0]>?MaxL1,
bst(<H,X+1,New>,<H,X+1,New>[X0+1],min(A,Min),?MaxL1),
<H,X+1,New>[X0+2]!=null, <H,X+1,New>[X0]<?MinR1,
bst(<H,X+1,New>,<H,X+1,New>[X0+2],?MinR1,max(A,Max)),
no_reach(<H,X+1,New>,X0,<H,X+1,New>[X0+1]),
no_reach(<H,X+1,New>,X0,<H,X+1,New>[X0+2]),
no_share(<H,X+1,New>,<H,X+1,New>[X0+1],<H,X+1,New>[X0+2])

N35: RIGHT SIMPLIFY
     X0!=X due to no_visit(H,X0,H[X0+2],X).
A>H[X0],
H[X0+1]!=null, H[X0]>MaxL, bst(H,H[X0+1],Min,MaxL),
H[X0+2]!=null, H[X0]<MinR, bst(<H,X+1,New>,H[X0+2],min(A,MinR),max(A,Max)),
no_visit(H,X0,H[X0+2],X,A),
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+1],H[X0+2])
|=
H[X0+1]!=null, H[X0]>?MaxL1, bst(H,H[X0+1],Min,?MaxL1),
H[X0+2]!=null, H[X0]<?MinR1, bst(<H,X+1,New>,H[X0+2],?MinR1,max(A,Max)),
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+1],H[X0+2])

N36: RIGHT SPECIALIZE WITH MinR1=min(A,MinR), MaxL1=MaxL
A>H[X0],
H[X0+1]!=null, H[X0]>MaxL, bst(H,H[X0+1],Min,MaxL),
H[X0+2]!=null, H[X0]<MinR, bst(<H,X+1,New>,H[X0+2],min(A,MinR),max(A,Max)),
no_visit(H,X0,H[X0+2],X,A),
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+1],H[X0+2])
|=
H[X0+1]!=null, H[X0]>MaxL, bst(H,H[X0+1],Min,MaxL),
H[X0+2]!=null, H[X0]<min(A,MinR),
bst(<H,X+1,New>,H[X0+2],min(A,MinR),max(A,Max)),
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+1],H[X0+2])
STOP: DIRECT PROOF

-------------------------------------------------------------------------------


N37: LEFT UNFOLD N31 (bst 4th rule)
path(H,H[X0+2],X,A), bst(H,H[X0+2],MinR,Max), A<H[X], H[X+1]=null,
New!=null, H[New]=A, H[New+1]=null, H[New+2]=null,
H[X0+1]=null, H[X0]<MinR, H[X0+2]!=null, A>H[X0],
no_visit(H,X0,H[X0+2],X,A),
no_reach(H,X0,H[X0+2])
|= bst(<H,X+1,New>,X0,H[X0],max(A,Max))

N38: COINDUCTION USING N7
bst(<H,X+1,New>,H[X0+2],min(A,MinR),max(A,Max)),
H[X0+1]=null, H[X0]<MinR, H[X0+2]!=null, A>H[X0]
no_visit(H,X0,H[X0+2],X,A),
no_reach(H,X0,H[X0+2])
|= bst(<H,X+1,New>,X0,H[X0],max(A,Max))

N39: RIGHT UNFOLD N38 (bst 4th rule)
bst(<H,X+1,New>,H[X0+2],min(A,MinR),max(A,Max)),
H[X0+1]=null, H[X0]<MinR, H[X0+2]!=null, A>H[X0]
no_visit(H,X0,H[X0+2],X,A),
no_reach(H,X0,H[X0+2])
|=
<H,X+1,New>[X0]=H[X0], <H,X+1,New>[X0+1]=null,
<H,X+1,New>[X0+2]!=null, <H,X+1,New>[X0]<?MinR1, 
bst(<H,X+1,New>,<H,X+1,New>[X0+2],?MinR1,max(A,Max)),
no_reach(<H,X+1,New>,X0,<H,X+1,New>[X0+2])

N40: RIGHT SIMPLIFY N39 USING "NO SHARING"
     X0!=X due to no_visit(H,X0,H[X0+2],X,A)
bst(<H,X+1,New>,H[X0+2],min(A,MinR),max(A,Max)),
H[X0+1]=null, H[X0]<MinR, H[X0+2]!=null, A>H[X0]
no_visit(H,X0,H[X0+2],X,A),
no_reach(H,X0,H[X0+2])
|=
H[X0+1]=null, H[X0+2]!=null, H[X0]<?MinR1, 
bst(<H,X+1,New>,H[X0+2],?MinR1,max(A,Max)),
no_reach(H,X0,H[X0+2])

N41: RIGHT SPECIALIZE WITH MinR1=min(A,MinR)
bst(<H,X+1,New>,H[X0+2],min(A,MinR),max(A,Max)),
H[X0+1]=null, H[X0]<MinR, H[X0+2]!=null, A>H[X0]
no_visit(H,X0,H[X0+2],X,A),
no_reach(H,X0,H[X0+2])
|=
H[X0+1]=null, H[X0+2]!=null, H[X0]<min(A,MinR), 
bst(<H,X+1,New>,H[X0+2],min(A,MinR),max(A,Max)),
no_reach(H,X0,H[X0+2])
STOP: DIRECT PROOF

-------------------------------------------------------------------------------

N42: LEFT UNFOLD N3 (p)
p(3,H,X,A,Hf,Xf), path(H,X0,X,A), bst(H,X0,Min,Max), A<H[X], H[X+1]!=null,
|= bst(Hf,X0,min(A,Min),max(A,Max))

N43: LEFT UNFOLD N42 (p)
p(0,H,X',A,Hf,Xf), path(H,X0,X,A), bst(H,X0,Min,Max),
A<H[X], H[X+1]!=null, X'=H[X+1]
|= bst(Hf,X0,min(A,Min),max(A,Max))
STOP: LHS SUBSUMED BY N0a

===============================================================================

PROOF OF SUBSUMPTION:

S0:
path(H,X0,X,A), A<H[X], H[X+1]!=null, bst(H,X0,Min,Max)
|= path(H,X0,H[X+1],A)

S1: LEFT UNFOLD S0 (path rule 1)
A<H[X], H[X+1]!=null, bst(H,X,Min,Max) |= path(H,X,H[X+1],A)

S2: RIGHT UNFOLD S1 (path rule 2)
A<H[X], H[X+1]!=null, bst(H,X,Min,Max)
|=
H[X+1]!=null, A<H[X], path(H,H[X+1],H[X+1],A),
no_visit(H,X,H[X+1],H[X+1],A)

S3: RIGHT UNFOLD S2 (path rule 1)
A<H[X], H[X+1]!=null, bst(H,X,Min,Max)
|=
H[X+1]!=null, A<H[X],
no_visit(H,X,H[X+1],H[X+1],A)

S4: LEFT UNFOLD S3 (bst rule 2)
A<H[X],
H[X+1]!=null, H[X]>MaxL, bst(H,H[X+1],Min,MaxL),
H[X+2]!=null, H[X]<MinR, bst(H,H[X+2],MinR,Max),
no_reach(H,X,H[X+1]),
no_reach(H,X,H[X+2]),
no_share(H,H[X+1],H[X+2])
|=
H[X+1]!=null, A<H[X],
no_visit(H,X,H[X+1],H[X+1],A)

S5: SIMPLIFY no_visit(H,X,H[X+1],H[X+1],A)=true DUE TO no_reach(H,X,H[X+1])
A<H[X],
H[X+1]!=null, H[X]>MaxL, bst(H,H[X+1],Min,MaxL),
H[X+2]!=null, H[X]<MinR, bst(H,H[X+2],MinR,Max),
no_reach(H,X,H[X+1]),
no_reach(H,X,H[X+2]),
no_share(H,H[X+1],H[X+2])
|=
H[X+1]!=null, A<H[X]
STOP: DIRECT PROOF

-------------------------------------------------------------------------------

S7: LEFT UNFOLD S3 (bst rule 3)
A<H[X],
H[X+1]!=null, Max=H[X], H[X]>MaxL, bst(H,H[X+1],Min,MaxL),
H[X+2]=null, no_reach(H,X,H[X+1])
|=
H[X+1]!=null, A<H[X], no_visit(H,X,H[X+1],H[X+1],A)

S8: SIMPLIFY S7 (no_visit(H,X,H[X+1],H[X+1],A)=true) DUE TO 
    no_reach(H,X,H[X+1])
A<H[X],
H[X+1]!=null, Max=H[X], H[X]>MaxL, bst(H,H[X+1],Min,MaxL),
H[X+2]=null, no_reach(H,X,H[X+1])
|=
H[X+1]!=null, A<H[X]
STOP: DIRECT PROOF

-------------------------------------------------------------------------------

S9: LEFT UNFOLD S0 (path rule 2)
H[X0+1]!=null, A<H[X0], path(H,H[X0+1],X,A),
no_visit(H,X0,H[X0+1],X,A),
A<H[X], H[X+1]!=null, bst(H,X0,Min,Max)
|= path(H,X0,H[X+1],A)

S10: LEFT UNFOLD S9 (bst rule 2)
path(H,H[X0+1],X,A), A<H[X], H[X+1]!=null, bst(H,H[X0+1],Min,MaxL),
A<H[X0], 
H[X0+1]!=null, H[X0]>MaxL, 
H[X0+2]!=null, H[X0]<MinR, bst(H,H[X0+2],MinR,Max),
no_visit(H,X0,H[X0+1],X,A),
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+1],H[X0+2])
|= path(H,X0,H[X+1],A)

S11: COINDUCTION TO S0
path(H,H[X0+1],H[X+1],A), A<H[X0], 
H[X0+1]!=null, H[X0]>MaxL, 
H[X0+2]!=null, H[X0]<MinR, bst(H,H[X0+2],MinR,Max),
no_visit(H,X0,H[X0+1],X,A),
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+1],H[X0+2])
|= path(H,X0,H[X+1],A)

S12: RIGHT UNFOLD S11 (path rule 2)
path(H,H[X0+1],H[X+1],A), A<H[X0], 
H[X0+1]!=null, H[X0]>MaxL, 
H[X0+2]!=null, H[X0]<MinR, bst(H,H[X0+2],MinR,Max),
no_visit(H,X0,H[X0+1],X,A),
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+1],H[X0+2])
|=
H[X0+1]!=null, A<H[X0], path(H,H[X0+1],H[X+1],A),
no_visit(H,X0,H[X0+1],H[X+1],A)

S13: SIMPLIFY S12 no_visit(H,X0,H[X0+1],H[X+1],A)=true DUE TO
     no_reach(H,X0,H[X0+1])
path(H,H[X0+1],H[X+1],A), A<H[X0], 
H[X0+1]!=null, H[X0]>MaxL, 
H[X0+2]!=null, H[X0]<MinR, bst(H,H[X0+2],MinR,Max),
no_visit(H,X0,H[X0+1],X,A),
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+1],H[X0+2])
|=
H[X0+1]!=null, A<H[X0], path(H,H[X0+1],H[X+1],A)
STOP: DIRECT PROOF

-------------------------------------------------------------------------------

S14: LEFT UNFOLD S9 (bst rule 3)
path(H,H[X0+1],X,A), A<H[X], H[X+1]!=null, bst(H,H[X0+1],Min,MaxL),
H[X0+1]!=null, A<H[X0], H[X0+2]=null, H[X0]>MaxL, 
no_visit(H,X0,H[X0+1],X,A),
no_reach(H,X0,H[X0+1])
|= path(H,X0,H[X+1],A)

S15: COINDUCTION OF S14 USING S0
H[X0+1]!=null, A<H[X0], H[X0+2]=null, H[X0]>MaxL, 
path(H,H[X0+1],H[X+1],A),
no_visit(H,X0,H[X0+1],X,A),
no_reach(H,X0,H[X0+1])
|= path(H,X0,H[X+1],A)

S16: RIGHT UNFOLD S15 (path rule 2)
H[X0+1]!=null, A<H[X0], H[X0+2]=null, H[X0]>MaxL, 
path(H,H[X0+1],H[X+1],A),
no_visit(H,X0,H[X0+1],X,A),
no_reach(H,X0,H[X0+1])
|= 
H[X0+1]!=null, A<H[X0], path(H,H[X0+1],H[X+1],A),
no_visit(H,X0,H[X0+1],H[X+1],A)

S17: no_visit(H,X0,H[X0+1],H[X+1],A)=true DUE TO 
     no_reach(H,X0,H[X0+1])
H[X0+1]!=null, A<H[X0], H[X0+2]=null, H[X0]>MaxL, 
path(H,H[X0+1],H[X+1],A),
no_visit(H,X0,H[X0+1],X,A),
no_reach(H,X0,H[X0+1])
|= 
H[X0+1]!=null, A<H[X0], path(H,H[X0+1],H[X+1],A),
STOP: DIRECT PROOF

-------------------------------------------------------------------------------

S18: LEFT UNFOLD S0 (path rule 3)
H[X0+2]!=null, A>H[X0], path(H,H[X0+2],X,A),
A<H[X], H[X+1]!=null, bst(H,X0,Min,Max),
no_visit(H,X0,H[X0+2],X,A)
|= path(H,X0,H[X+1],A)

S19: LEFT UNFOLD S18 (bst rule 2)
path(H,H[X0+2],X,A), A<H[X], H[X+1]!=null, bst(H,H[X0+2],MinR,Max),
H[X0+1]!=null, H[X0+2]!=null, A>H[X0], 
H[X0]>MaxL, bst(H,H[X0+1],Min,MaxL),
H[X0]<MinR, 
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+2],H[X0+2]),
no_visit(H,X0,H[X0+2],X,A)
|= path(H,X0,H[X+1],A)

S20: COINDUCTION OF S19 TO S0
path(H,H[X0+2],H[X+1],A),
H[X0+1]!=null, H[X0+2]!=null, A>H[X0], 
H[X0]>MaxL, bst(H,H[X0+1],Min,MaxL),
H[X0]<MinR, 
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+2],H[X0+2]),
no_visit(H,X0,H[X0+2],X,A)
|= path(H,X0,H[X+1],A)

S21: RIGHT UNFOLD S20 (path rule 3)
path(H,H[X0+2],H[X+1],A),
H[X0+1]!=null, H[X0+2]!=null, A>H[X0], 
H[X0]>MaxL, bst(H,H[X0+1],Min,MaxL),
H[X0]<MinR, 
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+2],H[X0+2]),
no_visit(H,X0,H[X0+2],X,A)
|=
H[X0+2]!=null, A>H[X0], path(H,H[X0+2],H[X+1],A),
no_visit(H,X0,H[X0+2],H[X+1],A)

S22: SIMPLIFY S21
     no_visit(H,X0,H[X0+2],H[X+1],A)=true
     DUE TO no_reach(H,X0,H[X0+2])
path(H,H[X0+2],H[X+1],A),
H[X0+1]!=null, H[X0+2]!=null, A>H[X0], 
H[X0]>MaxL, bst(H,H[X0+1],Min,MaxL),
H[X0]<MinR, 
no_reach(H,X0,H[X0+1]),
no_reach(H,X0,H[X0+2]),
no_share(H,H[X0+2],H[X0+2]),
no_visit(H,X0,H[X0+2],X,A)
|=
H[X0+2]!=null, A>H[X0], path(H,H[X0+2],H[X+1],A),
STOP: DIRECT PROOF

-------------------------------------------------------------------------------

S24: LEFT UNFOLD S18 (bst rule 4)
path(H,H[X0+2],X,A), A<H[X], H[X+1]!=null, bst(H,H[X0+2],MinR,Max),
H[X0+2]!=null, A>H[X0], Min=H[X0], H[X0+1]=null, H[X0]<MinR, 
no_reach(H,X0,H[X0+2]),
no_visit(H,X0,H[X0+2],X,A)
|= path(H,X0,H[X+1],A)

S25: COINDUCTION TO S0
path(H,H[X0+2],H[X+1],A),
H[X0+2]!=null, A>H[X0], Min=H[X0], H[X0+1]=null, H[X0]<MinR, 
no_reach(H,X0,H[X0+2]), no_visit(H,X0,H[X0+2],X,A)
|= path(H,X0,H[X+1],A)

S26: RIGHT UNFOLD S25
path(H,H[X0+2],H[X+1],A),
H[X0+2]!=null, A>H[X0], Min=H[X0], H[X0+1]=null, H[X0]<MinR, 
no_reach(H,X0,H[X0+2]), no_visit(H,X0,H[X0+2],X,A)
|= 
H[X0+2]!=null, A>H[X0], path(H,H[X0+2],H[X+1],A),
no_visit(H,X0,H[X0+2],H[X+1],A)

S27: SIMPLIFY S26
     no_visit(H,X0,H[X0+2],H[X+1],A)=true
     DUE TO no_reach(H,X0,H[X0+2])
path(H,H[X0+2],H[X+1],A),
H[X0+2]!=null, A>H[X0], Min=H[X0], H[X0+1]=null, H[X0]<MinR, 
no_reach(H,X0,H[X0+2]), no_visit(H,X0,H[X0+2],X,A)
|= 
H[X0+2]!=null, A>H[X0], path(H,H[X0+2],H[X+1],A),
STOP: DIRECT PROOF

===============================================================================

N44: LEFT UNFOLD N0a
p(4,H,X,A,Hf,Xf), path(H,X0,X,A), bst(H,X0,Min,Max), A>H[X]
|= bst(Hf,X0,min(A,Min),max(A,Max))
STOP: SYMMETRIC TO N3

-------------------------------------------------------------------------------

B0: bst(H,X,Min,Max) |= Min <= Max

B1: LEFT UNFOLD B0
Min=Max=H[X], H[X+1]=null, H[X+2]=null |= Min <= Max
STOP: DIRECT PROOF

B2: LEFT UNFOLD B0
H[X+1]!=null, H[X]>MaxL, bst(H,H[X+1],Min,MaxL),
H[X+2]!=null, H[X]<MinR, bst(H,H[X+2],MinR,Max) |= Min <= Max

B3: COINDUCTION USING B0
H[X+1]!=null, H[X]>MaxL, Min <= MaxL,
H[X+2]!=null, H[X]<MinR, MinR <= Max |= Min <= Max
STOP: DIRECT PROOF

B4: LEFT UNFOLD B0
H[X+1]!=null, H[X]>MaxL, bst(H,H[X+1],Min,MaxL), H[X+2]=null
|= Min <= Max

B5: COINDUCTION USING B0
H[X+1]!=null, H[X]>MaxL, Min <= MaxL, H[X+2]=null, Max=H[X]
|= Min <= Max
STOP: DIRECT PROOF

B6: LEFT UNFOLD B0
H[X+1]=null, Min=H[X],
H[X+2]!=null, H[X]<MinR, bst(H,H[X+2],MinR,Max)
|= Min <= Max

B7: COINDUCTION USING B0
H[X+1]=null, Min=H[X], H[X+2]!=null, H[X]<MinR, MinR <= Max
|= Min <= Max
STOP: DIRECT PROOF