script.kps 906 Bytes
Newer Older
1
// This file is not written yet!!
Sarah Grebing's avatar
Sarah Grebing committed
2

3
script main() {
Sarah Grebing's avatar
Sarah Grebing committed
4 5 6 7 8 9 10 11 12 13 14 15
    feqff : TERM := `f(c) = f(f(c))`;
    ffeqf : TERM := `f(f(c)) = f(c)`;
    feqfff: TERM :=  `f(c) = f(f(f(c)))`;

    impRight;
    instantiate var=`x` with=`c`;
    applyEq on=`f(f(c))` formula=feqfff;
    eqSymm on=feqff;
    close;
}

script main1() {
16
    impRight;
17 18 19

    //instantiate var=`x` with=`c`;
    //allLeft formula=`\forall` with=`a`;
Sarah Grebing's avatar
Sarah Grebing committed
20
    //allLeft on=`\forall s x; f(f(x)) = f(x)` inst_t=`c`;
21

Sarah Grebing's avatar
interim  
Sarah Grebing committed
22 23 24 25 26
}

script proj() {
impRight;
eqSymm formula = `f(c) = f(f(f(c)))`;
Sarah Grebing's avatar
interim  
Sarah Grebing committed
27 28
instantiate var=`x` with=`f(f(c))`;
//allLeft on =`\forall s x; f(f(x)) = f(x)` inst_t=`f(f(c))`;
Sarah Grebing's avatar
interim  
Sarah Grebing committed
29 30 31 32 33 34 35
allLeft on =`\forall s x; f(f(x)) = f(x)` inst_t=`c`;
//applyEqRigid;
//applyEq formula=`f(f(f(c))) = f(c)` occ=`f(f(c))`;
//applyEq formula=`f(f(f(c))) = f(c)` occ=4;
applyEq on=`f(f(c))` formula=`f(f(f(c))) = f(c)` ;
close;
//close formula=`f(f(c))=f(c)`;
36
}