File: los_problem.why

package info (click to toggle)
why3 1.8.2-3
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid
  • size: 45,028 kB
  • sloc: xml: 185,443; ml: 111,224; ansic: 3,998; sh: 2,578; makefile: 2,568; java: 865; python: 720; javascript: 290; lisp: 205; pascal: 173
file content (23 lines) | stat: -rw-r--r-- 494 bytes parent folder | download | duplicates (6) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
 

(* Los problem *)

theory LosProblem

  type t
  predicate p t t
  predicate q t t

  (* p and q are transitive *)
  axiom p_trans: forall x y z: t. p x y -> p y z -> p x z
  axiom q_trans: forall x y z: t. q x y -> q y z -> q x z

  (* q is symmetric *)
  axiom q_sym: forall x y: t. q x y -> q y x

  (* p\/q is universal *)
  axiom p_or_q: forall x y: t. p x y \/ q x y

  (* show that either p or q is universal *)
  goal los_problem: (forall x y: t. p x y) \/ (forall x y: t. q x y)

end