test.key 856 Bytes
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
// This file is part of KeY - Integrated Deductive Software Design
//
// Copyright (C) 2001-2011 Universitaet Karlsruhe (TH), Germany
//                         Universitaet Koblenz-Landau, Germany
//                         Chalmers University of Technology, Sweden
// Copyright (C) 2011-2013 Karlsruhe Institute of Technology, Germany
//                         Technical University Darmstadt, Germany
//                         Chalmers University of Technology, Sweden
//
// The KeY system is protected by the GNU General
// Public License. See LICENSE.TXT for details.
//

// Input file for KeY standalone prover version 0.497
\sorts {
Alexander Weigl's avatar
Alexander Weigl committed
16
17
18
19
20
	S;
}

\functions {
   S a; S b; S c;
21
   int i; int j;
Alexander Weigl's avatar
Alexander Weigl committed
22
23
24
   S f(S);
   S g(S);
   S h(S, S);
25
26

   int fint(int);
27
28
29
30
31
}

\predicates {
	p;
	q;
32
33
	pred(S);
	qpred(S, S);
34
	intPred(int);
35
36
37
38
39
}

\problem {
    (p -> q) -> !q -> !p
}