|
wneuper@4885
|
1 |
package isac.gui.mawen.scalaterm
|
|
wneuper@4885
|
2 |
|
|
wneuper@4885
|
3 |
import edu.tum.cs.isabelle.pure._
|
|
wneuper@4885
|
4 |
|
|
wneuper@4885
|
5 |
object TestsDATA {
|
|
wneuper@4885
|
6 |
|
|
wneuper@4885
|
7 |
//---------------------------- for <code>MockCalcTreeSIMPLIFY</code>
|
|
wneuper@4885
|
8 |
/* copied from ScalaTermFromString.testExampleForRef1
|
|
wneuper@4885
|
9 |
1 App(Const(Simplify.Simplify,Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))),App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(1,Type(Real.real,List()))),App(App(Const(Fields.inverse_class.divide,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(2,Type(Real.real,List()))),Free(x,Type(Real.real,List())))),App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(y,Type(Real.real,List()))),Free(3,Type(Real.real,List()))))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(4,Type(Real.real,List()))),Free(z,Type(Real.real,List())))),App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(y,Type(Real.real,List()))),Free(3,Type(Real.real,List()))))))),Free(5,Type(Real.real,List()))))
|
|
wneuper@4885
|
10 |
2 App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(1,Type(Real.real,List()))),App(App(Const(Fields.inverse_class.divide,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(2,Type(Real.real,List()))),Free(x,Type(Real.real,List())))),App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(y,Type(Real.real,List()))),Free(3,Type(Real.real,List()))))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(4,Type(Real.real,List()))),Free(z,Type(Real.real,List())))),App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(y,Type(Real.real,List()))),Free(3,Type(Real.real,List()))))))),Free(5,Type(Real.real,List())))
|
|
wneuper@4885
|
11 |
3 App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(1,Type(Real.real,List()))),App(App(Const(Fields.inverse_class.divide,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(2,Type(Real.real,List()))),Free(x,Type(Real.real,List())))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(4,Type(Real.real,List()))),Free(z,Type(Real.real,List())))))),Free(5,Type(Real.real,List())))
|
|
wneuper@4885
|
12 |
4 App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(1,Type(Real.real,List()))),App(App(Const(Fields.inverse_class.divide,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(x,Type(Real.real,List()))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(2,Type(Real.real,List()))),Free(z,Type(Real.real,List())))))),Free(5,Type(Real.real,List())))
|
|
wneuper@4885
|
13 |
5 App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(6,Type(Real.real,List()))),App(App(Const(Fields.inverse_class.divide,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(x,Type(Real.real,List()))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(2,Type(Real.real,List()))),Free(z,Type(Real.real,List())))))
|
|
wneuper@4885
|
14 |
*/
|
|
wneuper@4885
|
15 |
// below <REPLACE ALL> fun WITH "fun", etc (in a separate file in order to preserve the above copies)
|
|
wneuper@4885
|
16 |
// "Simplify ((1 + (2 * x * (y + 3)) / (4 * z * (y + 3))) + 5::real)";
|
|
wneuper@4885
|
17 |
def tt1 (): Term = App(Const("Simplify.Simplify",Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))))),Free("5",Type("Real.real",List()))))
|
|
wneuper@4885
|
18 |
// "(1 + (2 * x * (y + 3)) / (4 * z * (y + 3))) + 5::real";
|
|
wneuper@4885
|
19 |
def tt3 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))))),Free("5",Type("Real.real",List())))
|
|
wneuper@4885
|
20 |
// "(1 + (2 * x) / (4 * z)) + 5::real";
|
|
wneuper@4885
|
21 |
def tt4 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))))),Free("5",Type("Real.real",List())))
|
|
wneuper@4885
|
22 |
// "6 + (2 * x) / (4 * z::real)";
|
|
wneuper@4885
|
23 |
def tt5 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("x",Type("Real.real",List()))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("z",Type("Real.real",List())))))),Free("5",Type("Real.real",List())))
|
|
wneuper@4885
|
24 |
|
|
wneuper@4885
|
25 |
def tt6 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("6",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("x",Type("Real.real",List()))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("z",Type("Real.real",List())))))
|
|
S1420454023@4922
|
26 |
|
|
S1420454023@4922
|
27 |
def tt3_math(): String =
|
|
S1420454023@4922
|
28 |
"<math xmlns="+"\"&mathml;\""+">"+
|
|
S1420454023@4922
|
29 |
"<mrow>"+
|
|
S1420454023@4922
|
30 |
"<mn>1</mn>"+
|
|
S1420454023@4922
|
31 |
"<mo> + </mo>"+
|
|
S1420454023@4922
|
32 |
"<mfrac>"+
|
|
S1420454023@4922
|
33 |
"<mrow>"+
|
|
S1420454023@4922
|
34 |
"<mn>2</mn><mo> * </mo><mi>x</mi>"+
|
|
S1420454023@4922
|
35 |
"<mo> * </mo>"+
|
|
S1420454023@4922
|
36 |
"<mfenced separators=\'\'>"+
|
|
S1420454023@4922
|
37 |
"<mi>y</mi><mo> + </mo><mn>3</mn>"+
|
|
S1420454023@4922
|
38 |
"</mfenced>"+
|
|
S1420454023@4922
|
39 |
"</mrow>"+
|
|
S1420454023@4922
|
40 |
"<mrow>"+
|
|
S1420454023@4922
|
41 |
"<mn>4</mn><mo> * </mo><mi>z</mi>"+
|
|
S1420454023@4922
|
42 |
"<mo> * </mo>"+
|
|
S1420454023@4922
|
43 |
"<mfenced separators=\'\'>"+
|
|
S1420454023@4922
|
44 |
"<mi>y</mi><mo> + </mo><mn>3</mn>"+
|
|
S1420454023@4922
|
45 |
"</mfenced>"+
|
|
S1420454023@4922
|
46 |
"</mrow>"+
|
|
S1420454023@4922
|
47 |
"</mfrac>"+
|
|
S1420454023@4922
|
48 |
"<mo> + </mo>"+
|
|
S1420454023@4922
|
49 |
"<mn>5</mn>"+
|
|
S1420454023@4922
|
50 |
"</mrow>" +
|
|
S1420454023@4922
|
51 |
"</math>";
|
|
wneuper@4962
|
52 |
//scenario 1: http://www.ist.tugraz.at/projects/isac/publ/Masterthesis_NatalieKarl.pdf p.47
|
|
S1420454023@4952
|
53 |
def tt_me1_1 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Atools.pow",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Nat.nat",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("2",Type("Nat.nat",List())))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("6",Type("Real.real",List()))),Free("y",Type("Real.real",List()))))),Free("9",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))))),Free("5",Type("Real.real",List())))
|
|
S1420454023@4952
|
54 |
def tt_me1_2 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Atools.pow",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Nat.nat",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List())))),Free("2",Type("Nat.nat",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))))),Free("5",Type("Real.real",List())))
|
|
S1420454023@4952
|
55 |
def tt_me1_3 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("6",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("x",Type("Real.real",List()))),Free("1",Type("Real.real",List()))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))))
|
|
wneuper@4962
|
56 |
//scenario 4: http://www.ist.tugraz.at/projects/isac/publ/Masterthesis_NatalieKarl.pdf p.50
|
|
S1420454023@4952
|
57 |
def tt_me4_1 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("6",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("3",Type("Real.real",List()))),Free("b",Type("Real.real",List()))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("a",Type("Real.real",List()))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("c",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("a",Type("Real.real",List()))))))
|
|
S1420454023@4952
|
58 |
def tt_me4_2 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("6",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Atools.pow",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Nat.nat",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("a",Type("Real.real",List())))),Free("2",Type("Nat.nat",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("a",Type("Real.real",List()))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("3",Type("Real.real",List()))),Free("b",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("a",Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("c",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("a",Type("Real.real",List()))))))
|
|
S1420454023@4952
|
59 |
def tt_me4_3 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("5",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("a",Type("Real.real",List()))))),App(App(Const("Atools.pow",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Nat.nat",List()), Type("Real.real",List())))))),Free("a",Type("Real.real",List()))),Free("2",Type("Nat.nat",List()))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("a",Type("Real.real",List()))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("3",Type("Real.real",List()))),Free("b",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("a",Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("c",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("a",Type("Real.real",List()))))))),Free("1",Type("Real.real",List())))
|
|
wneuper@4962
|
60 |
//scenario 5: http://www.ist.tugraz.at/projects/isac/publ/Masterthesis_NatalieKarl.pdf p.51
|
|
S1420454023@4952
|
61 |
def tt_me5_1 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Atools.pow",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Nat.nat",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("2",Type("Nat.nat",List())))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("6",Type("Real.real",List()))),Free("y",Type("Real.real",List()))))),Free("9",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))))),Free("5",Type("Real.real",List())))
|
|
S1420454023@4952
|
62 |
def tt_me5_2 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Atools.pow",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Nat.nat",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List())))),Free("2",Type("Nat.nat",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))))),Free("5",Type("Real.real",List())))
|
|
S1420454023@4952
|
63 |
def tt_me5_3 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))))),Free("5",Type("Real.real",List())))
|
|
S1420454023@4952
|
64 |
def tt_me5_4 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),Free("1",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))))),Free("5",Type("Real.real",List())))
|
|
S1420454023@4952
|
65 |
def tt_me5_5 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),Free("1",Type("Real.real",List())))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))))),Free("5",Type("Real.real",List())))
|
|
S1420454023@4952
|
66 |
def tt_me5_6 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("6",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),Free("1",Type("Real.real",List())))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))))
|
|
S1420454023@4952
|
67 |
|
|
wneuper@4885
|
68 |
} |