script.kps 605 Bytes
Newer Older
1
2
3
// This file is not written yet!!
script main() {
    impRight;
4
5
6
7

    //instantiate var=`x` with=`c`;
    //allLeft formula=`\forall` with=`a`;
    allLeft on=`\forall s x; f(f(x)) = f(x)` inst_t=`c`;
8

Sarah Grebing's avatar
interim    
Sarah Grebing committed
9
10
11
12
13
14
15
16
17
18
19
20
21
}

script proj() {
impRight;
eqSymm formula = `f(c) = f(f(f(c)))`;
allLeft on =`\forall s x; f(f(x)) = f(x)` inst_t=`f(f(c))`;
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)`;
22
}