pop2push2 :  

  |-------
{1}   FORALL (s: stack, x, y: t): pop(pop(push(x, push(y, s)))) = s

Rule? (skolem!)
Skolemizing,
this simplifies to: 
pop2push2 :  

  |-------
{1}   pop(pop(push(x!1, push(y!1, s!1)))) = s!1

Rule? (replace 1)
No change on: (REPLACE 1)
pop2push2 :  

  |-------
{1}   pop(pop(push(x!1, push(y!1, s!1)))) = s!1

Rule? (replace "po_push")
No sequent formula corresponding to po_push,

No change on: (REPLACE "po_push")
pop2push2 :  

  |-------
{1}   pop(pop(push(x!1, push(y!1, s!1)))) = s!1

Rule? (replace "pop_push")
No sequent formula corresponding to pop_push,

No change on: (REPLACE "pop_push")
pop2push2 :  

  |-------
{1}   pop(pop(push(x!1, push(y!1, s!1)))) = s!1

Rule? (rewrite "pop_push" 1)
Found matching substitution:
s: stack gets push(y!1, s!1),
x: t gets x!1,
Rewriting using pop_push, matching in 1,
this simplifies to: 
pop2push2 :  

  |-------
{1}   pop(push(y!1, s!1)) = s!1

Rule? (rewrite "pop_push" 1)
Found matching substitution:
s: stack gets s!1,
x: t gets y!1,
Rewriting using pop_push, matching in 1,
Q.E.D.



Run time  = 0.53 secs.
Real time = 1037.54 secs.



NIL
PVS(25): 
