script.kps 375 Bytes
Newer Older
Sarah Grebing's avatar
Sarah Grebing committed
1
script split_from_quicksort() {
Sarah Grebing's avatar
Sarah Grebing committed
2 3 4 5 6 7 8 9 10 11 12 13 14 15
  autopilot_prep;
  foreach{
    tryclose;
  }
  foreach{
    simp_upd;
    seqPermFromSwap;
    andRight;
  }


  cases{
    case match `==> seqDef(_,_,_) = seqDef(_, _, _)`:
        auto;
16
    case match `==> (\exists ?X (\exists ?Y _))`:
Sarah Grebing's avatar
Sarah Grebing committed
17 18
        instantiate  var=X with=`i_0`;
        instantiate  var=Y with=`j_0`;
Sarah Grebing's avatar
Sarah Grebing committed
19 20 21 22
        auto;
  }
}