script.kps

// Please select one of the following scripts.
//

script test1234(){
    impRight;
    //auto;
}

script test23(){
impRight;
x:term := find(match `?rt ==>`);
impLeft formula=x;


cases{
    case match `q==>`:
      impRight;
      notRight;

    case match `==>`:
      impRight;
      notRight;
      close;
    }

        auto;

}


script test(){

}

script test1(){
  impRight;
  impRight;
}

script test_2(){
impRight;
impLeft;
cases{
    case match `q ==> ?X -> ?Y`:
      impRight;

}
}

script test2(){
impRight;
impLeft;
cases{
    case match `?X -> ?Y ==> not(?Z)`:
      notLeft;
    default:
      notRight;
}

}
script cpClosable(){
    impRight;
    impRight;
    cases{

       case match `?X -> ?Y ==> not(?Z)`:
            notLeft;

        try:
            notLeft;
            notRight;
            replace_known_left occ='2';
            concrete_impl_1;
            close;

        default:
            auto;

    }
}