1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
(* This file was originally generated by why.
It can be modified; only the generated parts will be overwritten. *)
Require Export max_spec_why.
(* Why obligation from file "/home/cmarche/recherche/why/examples-c/tutorial/max.c", line 2, characters 4-87: *)
(*Why goal*) Lemma max_impl_po_1 :
forall (x: Z),
forall (y: Z),
forall (HW_1: x > y),
(* CADUCEUS_1 *) ((x >= x /\ x >= y) /\
(forall (z:Z), (z >= x /\ z >= y -> z >= x))).
Proof.
intuition.
(* FILL PROOF HERE *)
Save.
(* Why obligation from file "/home/cmarche/recherche/why/examples-c/tutorial/max.c", line 2, characters 4-87: *)
(*Why goal*) Lemma max_impl_po_2 :
forall (x: Z),
forall (y: Z),
forall (HW_2: x <= y),
(* CADUCEUS_1 *) ((y >= x /\ y >= y) /\
(forall (z:Z), (z >= x /\ z >= y -> z >= y))).
Proof.
intuition.
(* FILL PROOF HERE *)
Save.
|
