Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / oversampling / out / typed / Globals.v @ 6a93d814

History | View | Annotate | Download (986 Bytes)

1
(* ---------------------------------------------------------- *)
2
(* --- Global Variables                                   --- *)
3
(* ---------------------------------------------------------- *)
4

    
5
Require Import ZArith.
6
Require Import Reals.
7
Require Import BuiltIn.
8
Require Import bool.Bool.
9
Require Import int.Int.
10
Require Import int.Abs.
11
Require Import int.ComputerDivision.
12
Require Import real.Real.
13
Require Import real.RealInfix.
14
Require Import real.FromInt.
15
Require Import map.Map.
16
Require Import Qedlib.
17
Require Import Qed.
18

    
19
Definition L_last_y_459 : Z := (460)%Z.
20

    
21
Definition L_cpt_458 : Z := (459)%Z.
22
Require Import Memory.
23

    
24
Hypothesis Q_L_last_y_459_linked: forall (t : array Z), ((linked t)) ->
25
  ((4 = (t.[ (L_last_y_459)%Z ]))%Z).
26

    
27
Hypothesis Q_L_last_y_459_region: (2 = ((region (L_last_y_459)%Z)))%Z.
28

    
29
Hypothesis Q_L_cpt_458_linked: forall (t : array Z), ((linked t)) ->
30
  ((4 = (t.[ (L_cpt_458)%Z ]))%Z).
31

    
32
Hypothesis Q_L_cpt_458_region: (2 = ((region (L_cpt_458)%Z)))%Z.
33