(*
 * Vericert: Verified high-level synthesis.
 * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
 *
 * This program is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program.  If not, see <https://www.gnu.org/licenses/>.
 *)

From compcert Require Import Smallstep Linking Integers Globalenvs.
From vericert Require HTL.
From vericert Require Import Vericertlib Veriloggen Verilog ValueInt AssocMap.
Require Import Lia.

Local Open Scope assocmap.

Definition match_prog (prog : HTL.program) (tprog : Verilog.program) :=
  match_program (fun cu f tf => tf = transl_fundef f) eq prog tprog.


forall prog : HTL.program, match_prog prog (transl_program prog)

forall prog : HTL.program, match_prog prog (transl_program prog)
prog:HTL.program

match_prog prog (transl_program prog)
prog:HTL.program

forall f : AST.fundef HTL.module, transl_fundef f = transl_fundef f
auto. Qed. Inductive match_stacks : list HTL.stackframe -> list stackframe -> Prop := | match_stack : forall res m pc reg_assoc arr_assoc hstk vstk, match_stacks hstk vstk -> match_stacks (HTL.Stackframe res m pc reg_assoc arr_assoc :: hstk) (Stackframe res (transl_module m) pc reg_assoc arr_assoc :: vstk) | match_stack_nil : match_stacks nil nil. Inductive match_states : HTL.state -> state -> Prop := | match_state : forall m st reg_assoc arr_assoc hstk vstk, match_stacks hstk vstk -> match_states (HTL.State hstk m st reg_assoc arr_assoc) (State vstk (transl_module m) st reg_assoc arr_assoc) | match_returnstate : forall v hstk vstk, match_stacks hstk vstk -> match_states (HTL.Returnstate hstk v) (Returnstate vstk v) | match_initial_call : forall m, match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil).

forall a b : value, Vlit a = Vlit b -> a = b

forall a b : value, Vlit a = Vlit b -> a = b
a, b:value
H:Vlit a = Vlit b
H1:a = b

b = b
trivial. Qed.

forall a b : positive, 0 <= Z.pos a <= Int.max_unsigned -> 0 <= Z.pos b <= Int.max_unsigned -> posToValue a = posToValue b -> a = b

forall a b : positive, 0 <= Z.pos a <= Int.max_unsigned -> 0 <= Z.pos b <= Int.max_unsigned -> posToValue a = posToValue b -> a = b
a, b:positive
H:0 <= Z.pos a <= Int.max_unsigned
H0:0 <= Z.pos b <= Int.max_unsigned
H1:posToValue a = posToValue b

a = b
a, b:positive
H:0 <= Z.pos a <= Int.max_unsigned
H0:0 <= Z.pos b <= Int.max_unsigned
H1:posToValue a = posToValue b

Z.to_pos (Z.pos a) = b
a, b:positive
H:0 <= Z.pos a <= Int.max_unsigned
H0:0 <= Z.pos b <= Int.max_unsigned
H1:posToValue a = posToValue b

Z.to_pos (Z.pos a) = Z.to_pos (Z.pos b)
a, b:positive
H:0 <= Z.pos a <= Int.max_unsigned
H0:0 <= Z.pos b <= Int.max_unsigned
H1:posToValue a = posToValue b

Z.to_pos (Int.unsigned (Int.repr (Z.pos a))) = Z.to_pos (Z.pos b)
a, b:positive
H:0 <= Z.pos a <= Int.max_unsigned
H0:0 <= Z.pos b <= Int.max_unsigned
H1:posToValue a = posToValue b

Z.to_pos (Z.pos b) = Z.to_pos (Int.unsigned (Int.repr (Z.pos a)))
a, b:positive
H:0 <= Z.pos a <= Int.max_unsigned
H0:0 <= Z.pos b <= Int.max_unsigned
H1:posToValue a = posToValue b

Z.to_pos (Int.unsigned (Int.repr (Z.pos b))) = Z.to_pos (Int.unsigned (Int.repr (Z.pos a)))
a, b:positive
H:0 <= Z.pos a <= Int.max_unsigned
H0:0 <= Z.pos b <= Int.max_unsigned
H1:Int.repr (Z.pos a) = Int.repr (Z.pos b)

Z.to_pos (Int.unsigned (Int.repr (Z.pos b))) = Z.to_pos (Int.unsigned (Int.repr (Z.pos a)))
rewrite H1; auto. Qed.

forall a b : int, 0 < Int.unsigned a -> 0 < Int.unsigned b -> valueToPos a = valueToPos b -> a = b

forall a b : int, 0 < Int.unsigned a -> 0 < Int.unsigned b -> valueToPos a = valueToPos b -> a = b
a, b:int
H:0 < Int.unsigned a
H0:0 < Int.unsigned b
H1:valueToPos a = valueToPos b

a = b
a, b:int
H:0 < Int.unsigned a
H0:0 < Int.unsigned b
H1:Z.to_pos (Int.unsigned a) = Z.to_pos (Int.unsigned b)

a = b
a, b:int
H:0 < Int.unsigned a
H0:0 < Int.unsigned b
H1:Z.to_pos (Int.unsigned a) = Z.to_pos (Int.unsigned b)

Int.repr (Int.unsigned a) = b
a, b:int
H:0 < Int.unsigned a
H0:0 < Int.unsigned b
H1:Z.to_pos (Int.unsigned a) = Z.to_pos (Int.unsigned b)

Int.repr (Int.unsigned a) = Int.repr (Int.unsigned b)
a, b:int
H:0 < Int.unsigned a
H0:0 < Int.unsigned b
H1:Z.pos (Z.to_pos (Int.unsigned a)) = Z.pos (Z.to_pos (Int.unsigned b))

Int.repr (Int.unsigned a) = Int.repr (Int.unsigned b)
a, b:int
H:0 < Int.unsigned a
H0:0 < Int.unsigned b
H1:Int.unsigned a = Z.pos (Z.to_pos (Int.unsigned b))

Int.repr (Int.unsigned a) = Int.repr (Int.unsigned b)
a, b:int
H:0 < Int.unsigned a
H0:0 < Int.unsigned b
H1:Int.unsigned a = Int.unsigned b

Int.repr (Int.unsigned a) = Int.repr (Int.unsigned b)
a, b:int
H:0 < Int.unsigned a
H0:0 < Int.unsigned b
H1:Int.unsigned a = Int.unsigned b

Int.repr (Int.unsigned b) = Int.repr (Int.unsigned b)
auto. Qed.

forall p : positive, Z.pos p <= Int.max_unsigned -> 0 < Int.unsigned (posToValue p)

forall p : positive, Z.pos p <= Int.max_unsigned -> 0 < Int.unsigned (posToValue p)
p:positive
H:Z.pos p <= Int.max_unsigned

0 < Int.unsigned (posToValue p)
p:positive
H:Z.pos p <= Int.max_unsigned

0 < Int.unsigned (Int.repr (Z.pos p))
rewrite Int.unsigned_repr; lia. Qed.

forall (p1 p2 : positive) (a b : stmnt), 0 <= Z.pos p1 <= Int.max_unsigned -> 0 <= Z.pos p2 <= Int.max_unsigned -> transl_list_fun (p1, a) = transl_list_fun (p2, b) -> (p1, a) = (p2, b)

forall (p1 p2 : positive) (a b : stmnt), 0 <= Z.pos p1 <= Int.max_unsigned -> 0 <= Z.pos p2 <= Int.max_unsigned -> transl_list_fun (p1, a) = transl_list_fun (p2, b) -> (p1, a) = (p2, b)
p1, p2:positive
a, b:stmnt
H:0 <= Z.pos p1 <= Int.max_unsigned
H0:0 <= Z.pos p2 <= Int.max_unsigned
H1:transl_list_fun (p1, a) = transl_list_fun (p2, b)

(p1, a) = (p2, b)
p1, p2:positive
a, b:stmnt
H:0 <= Z.pos p1 <= Int.max_unsigned
H0:0 <= Z.pos p2 <= Int.max_unsigned
H1:(Vlit (posToValue p1), a) = (Vlit (posToValue p2), b)

(p1, a) = (p2, b)
p1, p2:positive
a, b:stmnt
H:0 <= Z.pos p1 <= Int.max_unsigned
H0:0 <= Z.pos p2 <= Int.max_unsigned
H1:Vlit (posToValue p1) = Vlit (posToValue p2) /\ a = b

(p1, a) = (p2, b)
p1, p2:positive
a, b:stmnt
H:0 <= Z.pos p1 <= Int.max_unsigned
H0:0 <= Z.pos p2 <= Int.max_unsigned
H1:Vlit (posToValue p1) = Vlit (posToValue p2)
H2:a = b

(p1, a) = (p2, b)
p1, p2:positive
a, b:stmnt
H:0 <= Z.pos p1 <= Int.max_unsigned
H0:0 <= Z.pos p2 <= Int.max_unsigned
H1:Vlit (posToValue p1) = Vlit (posToValue p2)
H2:a = b

(p1, b) = (p2, b)
p1, p2:positive
a, b:stmnt
H:0 <= Z.pos p1 <= Int.max_unsigned
H0:0 <= Z.pos p2 <= Int.max_unsigned
H1:posToValue p1 = posToValue p2
H2:a = b

(p1, b) = (p2, b)
p1, p2:positive
a, b:stmnt
H:0 <= Z.pos p1 <= Int.max_unsigned
H0:0 <= Z.pos p2 <= Int.max_unsigned
H1:p1 = p2
H2:a = b

(p1, b) = (p2, b)
rewrite H1; auto. Qed.

forall p q r : Z, p < q <= r -> p <= q <= r

forall p q r : Z, p < q <= r -> p <= q <= r
lia. Qed. Hint Resolve Zle_relax : verilogproof.

forall (l : list (positive * stmnt)) (p : positive), 0 <= Z.pos p <= Int.max_unsigned -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)

forall (l : list (positive * stmnt)) (p : positive), 0 <= Z.pos p <= Int.max_unsigned -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)

forall p : positive, 0 <= Z.pos p <= Int.max_unsigned -> (forall p0 : positive, In p0 (map fst nil) -> 0 < Z.pos p0 <= Int.max_unsigned) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun nil)) -> In p (map fst nil)
a:(positive * stmnt)%type
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= Int.max_unsigned -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)
forall p : positive, 0 <= Z.pos p <= Int.max_unsigned -> (forall p0 : positive, In p0 (map fst (a :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun (a :: l))) -> In p (map fst (a :: l))

forall p : positive, 0 <= Z.pos p <= Int.max_unsigned -> (forall p0 : positive, In p0 (map fst nil) -> 0 < Z.pos p0 <= Int.max_unsigned) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun nil)) -> In p (map fst nil)
p:positive
H0:forall p0 : positive, False -> 0 < Z.pos p0 <= 4294967295
H1:False
H2:0 <= Z.pos p
H3:Z.pos p <= 4294967295

False
auto.
a:(positive * stmnt)%type
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= Int.max_unsigned -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)

forall p : positive, 0 <= Z.pos p <= Int.max_unsigned -> (forall p0 : positive, In p0 (map fst (a :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun (a :: l))) -> In p (map fst (a :: l))
a:(positive * stmnt)%type
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= Int.max_unsigned -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)
p:positive
H:0 <= Z.pos p <= Int.max_unsigned
H0:forall p0 : positive, In p0 (map fst (a :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H1:In (Vlit (posToValue p)) (map fst (map transl_list_fun (a :: l)))

In p (map fst (a :: l))
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= Int.max_unsigned -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)
p:positive
H:0 <= Z.pos p <= Int.max_unsigned
H0:forall p1 : positive, In p1 (map fst ((p0, s) :: l)) -> 0 < Z.pos p1 <= Int.max_unsigned
H1:In (Vlit (posToValue p)) (map fst (map transl_list_fun ((p0, s) :: l)))

In p (map fst ((p0, s) :: l))
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:Vlit (posToValue p0) = Vlit (posToValue p) \/ In (Vlit (posToValue p)) (map fst (map transl_list_fun l))
H2:0 <= Z.pos p
H3:Z.pos p <= 4294967295

p0 = p \/ In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:Vlit (posToValue p0) = Vlit (posToValue p) \/ In (Vlit (posToValue p)) (map fst (map transl_list_fun l))
H2:0 <= Z.pos p
H3:Z.pos p <= 4294967295
n:p0 <> p

p0 = p \/ In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:Vlit (posToValue p0) = Vlit (posToValue p) \/ In (Vlit (posToValue p)) (map fst (map transl_list_fun l))
H2:0 <= Z.pos p
H3:Z.pos p <= 4294967295
n:p0 <> p

In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H2:0 <= Z.pos p
H3:Z.pos p <= 4294967295
n:p0 <> p
H:Vlit (posToValue p0) = Vlit (posToValue p)

In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H2:0 <= Z.pos p
H3:Z.pos p <= 4294967295
n:p0 <> p
H:In (Vlit (posToValue p)) (map fst (map transl_list_fun l))
In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H2:0 <= Z.pos p
H3:Z.pos p <= 4294967295
n:p0 <> p
H:posToValue p0 = posToValue p

In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H2:0 <= Z.pos p
H3:Z.pos p <= 4294967295
n:p0 <> p
H:In (Vlit (posToValue p)) (map fst (map transl_list_fun l))
In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H2:0 <= Z.pos p
H3:Z.pos p <= 4294967295
n:p0 <> p
H:p0 = p

In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H2:0 <= Z.pos p
H3:Z.pos p <= 4294967295
n:p0 <> p
H:posToValue p0 = posToValue p
0 <= Z.pos p0 <= Int.max_unsigned
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H2:0 <= Z.pos p
H3:Z.pos p <= 4294967295
n:p0 <> p
H:In (Vlit (posToValue p)) (map fst (map transl_list_fun l))
In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H2:0 <= Z.pos p
H3:Z.pos p <= 4294967295
n:p0 <> p
H:posToValue p0 = posToValue p

0 <= Z.pos p0 <= Int.max_unsigned
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H2:0 <= Z.pos p
H3:Z.pos p <= 4294967295
n:p0 <> p
H:In (Vlit (posToValue p)) (map fst (map transl_list_fun l))
In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> In p (map fst l)
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H2:0 <= Z.pos p
H3:Z.pos p <= 4294967295
n:p0 <> p
H:In (Vlit (posToValue p)) (map fst (map transl_list_fun l))

In p (map fst l)
apply IHl; auto. Qed.

forall (l : list (positive * stmnt)) (p : positive), 0 <= Z.pos p <= Int.max_unsigned -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> ~ In p (map fst l) -> ~ In (Vlit (posToValue p)) (map fst (transl_list l))

forall (l : list (positive * stmnt)) (p : positive), 0 <= Z.pos p <= Int.max_unsigned -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> ~ In p (map fst l) -> ~ In (Vlit (posToValue p)) (map fst (transl_list l))
a:(positive * stmnt)%type
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= Int.max_unsigned -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> ~ In p (map fst l) -> ~ In (Vlit (posToValue p)) (map fst (transl_list l))

forall p : positive, 0 <= Z.pos p <= Int.max_unsigned -> (forall p0 : positive, In p0 (map fst (a :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned) -> ~ In p (map fst (a :: l)) -> ~ In (Vlit (posToValue p)) (map fst (transl_list (a :: l)))
a:(positive * stmnt)%type
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= Int.max_unsigned -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> ~ In p (map fst l) -> ~ In (Vlit (posToValue p)) (map fst (transl_list l))
p:positive
H:0 <= Z.pos p <= Int.max_unsigned
H0:forall p0 : positive, In p0 (map fst (a :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H1:~ In p (map fst (a :: l))

~ In (Vlit (posToValue p)) (map fst (transl_list (a :: l)))
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= Int.max_unsigned -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> ~ In p (map fst l) -> ~ In (Vlit (posToValue p)) (map fst (transl_list l))
p:positive
H:0 <= Z.pos p <= Int.max_unsigned
H0:forall p1 : positive, In p1 (map fst ((p0, s) :: l)) -> 0 < Z.pos p1 <= Int.max_unsigned
H1:~ In p (map fst ((p0, s) :: l))

~ In (Vlit (posToValue p)) (map fst (transl_list ((p0, s) :: l)))
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= Int.max_unsigned -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (transl_list l)) -> False
p:positive
H:0 <= Z.pos p <= Int.max_unsigned
H0:forall p1 : positive, In p1 (map fst ((p0, s) :: l)) -> 0 < Z.pos p1 <= Int.max_unsigned
H1:In p (map fst ((p0, s) :: l)) -> False

In (Vlit (posToValue p)) (map fst (transl_list ((p0, s) :: l))) -> False
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= Int.max_unsigned -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (transl_list l)) -> False
p:positive
H:0 <= Z.pos p <= Int.max_unsigned
H0:forall p1 : positive, In p1 (map fst ((p0, s) :: l)) -> 0 < Z.pos p1 <= Int.max_unsigned
H1:In p (map fst ((p0, s) :: l)) -> False
H2:In (Vlit (posToValue p)) (map fst (transl_list ((p0, s) :: l)))

False
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (transl_list l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H2:Vlit (posToValue p0) = Vlit (posToValue p) \/ In (Vlit (posToValue p)) (map fst (transl_list l))
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295

False
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (transl_list l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H2:Vlit (posToValue p0) = Vlit (posToValue p) \/ In (Vlit (posToValue p)) (map fst (transl_list l))
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
e:p0 = p

False
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (transl_list l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H2:Vlit (posToValue p0) = Vlit (posToValue p) \/ In (Vlit (posToValue p)) (map fst (transl_list l))
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p
False
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (transl_list l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H2:Vlit (posToValue p0) = Vlit (posToValue p) \/ In (Vlit (posToValue p)) (map fst (transl_list l))
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
e:p0 = p

p0 = p \/ In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (transl_list l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H2:Vlit (posToValue p0) = Vlit (posToValue p) \/ In (Vlit (posToValue p)) (map fst (transl_list l))
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p
False
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (transl_list l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H2:Vlit (posToValue p0) = Vlit (posToValue p) \/ In (Vlit (posToValue p)) (map fst (transl_list l))
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p

False
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (transl_list l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H2:Vlit (posToValue p0) = Vlit (posToValue p) \/ In (Vlit (posToValue p)) (map fst (transl_list l))
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p

p0 = p \/ In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H2:Vlit (posToValue p0) = Vlit (posToValue p) \/ In (Vlit (posToValue p)) (map fst (map transl_list_fun l))
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p

p0 = p \/ In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p
H:Vlit (posToValue p0) = Vlit (posToValue p)

p0 = p \/ In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p
H:In (Vlit (posToValue p)) (map fst (map transl_list_fun l))
p0 = p \/ In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p
H:posToValue p0 = posToValue p

p0 = p \/ In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p
H:In (Vlit (posToValue p)) (map fst (map transl_list_fun l))
p0 = p \/ In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p
H:p0 = p

p0 = p \/ In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p
H:posToValue p0 = posToValue p
0 <= Z.pos p0 <= Int.max_unsigned
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p
H:posToValue p0 = posToValue p
0 <= Z.pos p <= Int.max_unsigned
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p
H:In (Vlit (posToValue p)) (map fst (map transl_list_fun l))
p0 = p \/ In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p
H:posToValue p0 = posToValue p

0 <= Z.pos p0 <= Int.max_unsigned
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p
H:posToValue p0 = posToValue p
0 <= Z.pos p <= Int.max_unsigned
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p
H:In (Vlit (posToValue p)) (map fst (map transl_list_fun l))
p0 = p \/ In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p
H:posToValue p0 = posToValue p

0 <= Z.pos p <= Int.max_unsigned
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p
H:In (Vlit (posToValue p)) (map fst (map transl_list_fun l))
p0 = p \/ In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p
H:In (Vlit (posToValue p)) (map fst (map transl_list_fun l))

p0 = p \/ In p (map fst l)
p0:positive
s:stmnt
l:list (positive * stmnt)
IHl:forall p : positive, 0 <= Z.pos p <= 4294967295 -> (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> (In p (map fst l) -> False) -> In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> False
p:positive
H0:forall p1 : positive, p0 = p1 \/ In p1 (map fst l) -> 0 < Z.pos p1 <= 4294967295
H1:p0 = p \/ In p (map fst l) -> False
H3:0 <= Z.pos p
H4:Z.pos p <= 4294967295
n:p0 <> p
H:In (Vlit (posToValue p)) (map fst (map transl_list_fun l))

In p (map fst l)
apply transl_in; auto. Qed.

forall l : list (positive * stmnt), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))

forall l : list (positive * stmnt), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))

(forall p0 : positive, In p0 (map fst nil) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst nil) -> list_norepet (map fst (transl_list nil))
a:(positive * stmnt)%type
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
(forall p0 : positive, In p0 (map fst (a :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst (a :: l)) -> list_norepet (map fst (transl_list (a :: l)))

(forall p0 : positive, In p0 (map fst nil) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst nil) -> list_norepet (map fst (transl_list nil))
H:forall p0 : positive, In p0 (map fst nil) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst nil)

list_norepet (map fst (transl_list nil))
H:forall p0 : positive, In p0 (map fst nil) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst nil)

list_norepet nil
apply list_norepet_nil.
a:(positive * stmnt)%type
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))

(forall p0 : positive, In p0 (map fst (a :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst (a :: l)) -> list_norepet (map fst (transl_list (a :: l)))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))

(forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst ((p, s) :: l)) -> list_norepet (map fst (transl_list ((p, s) :: l)))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))

list_norepet (map fst (transl_list ((p, s) :: l)))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))

list_norepet (Vlit (posToValue p) :: map fst (transl_list l))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))

~ In (Vlit (posToValue p)) (map fst (transl_list l))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))
list_norepet (map fst (transl_list l))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H3:~ In p (map fst l)
H4:list_norepet (map fst l)

~ In (Vlit (posToValue p)) (map fst (transl_list l))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))
list_norepet (map fst (transl_list l))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H3:~ In p (map fst l)
H4:list_norepet (map fst l)

0 <= Z.pos p <= Int.max_unsigned
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H3:~ In p (map fst l)
H4:list_norepet (map fst l)
forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H3:~ In p (map fst l)
H4:list_norepet (map fst l)
~ In p (map fst l)
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))
list_norepet (map fst (transl_list l))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H3:~ In p (map fst l)
H4:list_norepet (map fst l)

0 < Z.pos p <= Int.max_unsigned
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H3:~ In p (map fst l)
H4:list_norepet (map fst l)
forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H3:~ In p (map fst l)
H4:list_norepet (map fst l)
~ In p (map fst l)
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))
list_norepet (map fst (transl_list l))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H3:~ In p (map fst l)
H4:list_norepet (map fst l)

In p (map fst ((p, s) :: l))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H3:~ In p (map fst l)
H4:list_norepet (map fst l)
forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H3:~ In p (map fst l)
H4:list_norepet (map fst l)
~ In p (map fst l)
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))
list_norepet (map fst (transl_list l))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H3:~ In p (map fst l)
H4:list_norepet (map fst l)

forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H3:~ In p (map fst l)
H4:list_norepet (map fst l)
~ In p (map fst l)
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))
list_norepet (map fst (transl_list l))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H3:~ In p (map fst l)
H4:list_norepet (map fst l)
p0:positive
H0:In p0 (map fst l)

0 < Z.pos p0 <= Int.max_unsigned
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H3:~ In p (map fst l)
H4:list_norepet (map fst l)
~ In p (map fst l)
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))
list_norepet (map fst (transl_list l))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H3:~ In p (map fst l)
H4:list_norepet (map fst l)
p0:positive
H0:In p0 (map fst l)

In p0 (map fst ((p, s) :: l))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H3:~ In p (map fst l)
H4:list_norepet (map fst l)
~ In p (map fst l)
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))
list_norepet (map fst (transl_list l))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H3:~ In p (map fst l)
H4:list_norepet (map fst l)

~ In p (map fst l)
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))
list_norepet (map fst (transl_list l))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))

list_norepet (map fst (transl_list l))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))

forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))
list_norepet (map fst l)
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))
p0:positive
H1:In p0 (map fst l)

0 < Z.pos p0 <= Int.max_unsigned
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))
list_norepet (map fst l)
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))
p0:positive
H1:In p0 (map fst l)

In p0 (map fst ((p, s) :: l))
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))
list_norepet (map fst l)
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, In p0 (map fst ((p, s) :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
H0:list_norepet (map fst ((p, s) :: l))

list_norepet (map fst l)
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, p = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
H0:list_norepet (p :: map fst l)

list_norepet (map fst l)
p:positive
s:stmnt
l:list (positive * stmnt)
IHl:(forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> list_norepet (map fst (transl_list l))
H:forall p0 : positive, p = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
H3:~ In p (map fst l)
H4:list_norepet (map fst l)

list_norepet (map fst l)
assumption. Qed.

forall (l : list (positive * stmnt)) (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}

forall (l : list (positive * stmnt)) (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}

forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst nil) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst nil) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) nil -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list nil) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
a:(positive * stmnt)%type
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst (a :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst (a :: l)) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) (a :: l) -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list (a :: l)) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}

forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst nil) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst nil) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) nil -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list nil) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
contradiction.
a:(positive * stmnt)%type
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}

forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst (a :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst (a :: l)) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) (a :: l) -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list (a :: l)) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
a:(positive * stmnt)%type
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
v:value
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, In p0 (map fst (a :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
NOREP:list_norepet (map fst (a :: l))
ASSOC:asr ! ev = Some v
p:positive
s:stmnt
IN:In (p, s) (a :: l)
EQ:v = posToValue p
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}

stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list (a :: l)) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
v:value
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, In p0 (map fst ((p', s') :: l)) -> 0 < Z.pos p0 <= Int.max_unsigned
NOREP:list_norepet (map fst ((p', s') :: l))
ASSOC:asr ! ev = Some v
p:positive
s:stmnt
IN:In (p, s) ((p', s') :: l)
EQ:v = posToValue p
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}

stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list ((p', s') :: l)) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
v:value
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
ASSOC:asr ! ev = Some v
p:positive
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
EQ:v = posToValue p
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}

stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) ((Vlit (posToValue p'), s') :: transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
ASSOC:asr ! ev = Some (posToValue p')
s:stmnt
IN:(p', s') = (p', s) \/ In (p', s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}

stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) ((Vlit (posToValue p'), s') :: transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) ((Vlit (posToValue p'), s') :: transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
eapply stmnt_runp_Vcase_match. constructor. simplify. unfold AssocMap.find_assocmap, AssocMapExt.get_default. rewrite ASSOC. trivial.
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
ASSOC:asr ! ev = Some (posToValue p')
s:stmnt
IN:(p', s') = (p', s) \/ In (p', s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}

posToValue p' = posToValue p'
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
ASSOC:asr ! ev = Some (posToValue p')
s:stmnt
IN:(p', s') = (p', s) \/ In (p', s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s' {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) ((Vlit (posToValue p'), s') :: transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
ASSOC:asr ! ev = Some (posToValue p')
s:stmnt
IN:(p', s') = (p', s) \/ In (p', s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}

stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s' {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) ((Vlit (posToValue p'), s') :: transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
ASSOC:asr ! ev = Some (posToValue p')
s:stmnt
IN:(p', s') = (p', s) \/ In (p', s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
INV:(p', s') = (p', s)

stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s' {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
ASSOC:asr ! ev = Some (posToValue p')
s:stmnt
IN:(p', s') = (p', s) \/ In (p', s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
INV:In (p', s) l
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s' {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) ((Vlit (posToValue p'), s') :: transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
ASSOC:asr ! ev = Some (posToValue p')
s:stmnt
IN:(p', s) = (p', s) \/ In (p', s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
INV:(p', s) = (p', s)

stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
ASSOC:asr ! ev = Some (posToValue p')
s:stmnt
IN:(p', s') = (p', s) \/ In (p', s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
INV:In (p', s) l
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s' {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) ((Vlit (posToValue p'), s') :: transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
ASSOC:asr ! ev = Some (posToValue p')
s:stmnt
IN:(p', s') = (p', s) \/ In (p', s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
INV:In (p', s) l

stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s' {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) ((Vlit (posToValue p'), s') :: transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
ASSOC:asr ! ev = Some (posToValue p')
s:stmnt
IN:(p', s') = (p', s) \/ In (p', s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
INV:In (p', s) l
H1:~ In p' (map fst l)
H2:list_norepet (map fst l)

stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s' {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) ((Vlit (posToValue p'), s') :: transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
ASSOC:asr ! ev = Some (posToValue p')
s:stmnt
IN:(p', s') = (p', s) \/ In (p', s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
INV:In (fst (p', s)) (map fst l)
H1:~ In p' (map fst l)
H2:list_norepet (map fst l)

stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s' {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) ((Vlit (posToValue p'), s') :: transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'

stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) ((Vlit (posToValue p'), s') :: transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
eapply stmnt_runp_Vcase_nomatch. constructor. simplify. unfold AssocMap.find_assocmap, AssocMapExt.get_default. rewrite ASSOC. trivial.
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'

posToValue p' <> posToValue p
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'

posToValue p' = posToValue p -> False
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p

False
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p

p = p'
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p

0 <= Z.pos p <= Int.max_unsigned
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
0 <= Z.pos p' <= Int.max_unsigned
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
posToValue p = posToValue p'
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p

0 < Z.pos p <= Int.max_unsigned
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
0 <= Z.pos p' <= Int.max_unsigned
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
posToValue p = posToValue p'
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p

p' = p \/ In p (map fst l)
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
0 <= Z.pos p' <= Int.max_unsigned
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
posToValue p = posToValue p'
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p

In p (map fst l)
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
0 <= Z.pos p' <= Int.max_unsigned
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
posToValue p = posToValue p'
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
H0:(p', s') = (p, s)

In p (map fst l)
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
H0:In (p, s) l
In p (map fst l)
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
0 <= Z.pos p' <= Int.max_unsigned
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
posToValue p = posToValue p'
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
H0:In (p, s) l

In p (map fst l)
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
0 <= Z.pos p' <= Int.max_unsigned
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
posToValue p = posToValue p'
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
H0:In (fst (p, s)) (map fst l)

In p (map fst l)
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
0 <= Z.pos p' <= Int.max_unsigned
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
posToValue p = posToValue p'
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p

0 <= Z.pos p' <= Int.max_unsigned
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
posToValue p = posToValue p'
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p

0 < Z.pos p' <= Int.max_unsigned
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p
posToValue p = posToValue p'
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
H:posToValue p' = posToValue p

posToValue p = posToValue p'
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'

stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction.
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'

posToValue p = posToValue p
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'
stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
p':positive
s':stmnt
l:list (positive * stmnt)
IHl:forall (v : value) (ev : positive) (f : fext) (asr : AssocMap.t value) (asa : AssocMap.t arr) (asrn : AssocMap.t value) (asan : AssocMap.t arr) (asr' : AssocMap.t value) (asa' : AssocMap.t arr) (asrn' : AssocMap.t value) (asan' : AssocMap.t arr), (forall p0 : positive, In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295) -> list_norepet (map fst l) -> asr ! ev = Some v -> forall (p : positive) (s : stmnt), In (p, s) l -> v = posToValue p -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} (Vcase (Vvar ev) (transl_list l) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
ev:positive
f:fext
asr:AssocMap.t value
asa:AssocMap.t arr
asrn:AssocMap.t value
asan:AssocMap.t arr
asr':AssocMap.t value
asa':AssocMap.t arr
asrn':AssocMap.t value
asan':AssocMap.t arr
BOUND:forall p0 : positive, p' = p0 \/ In p0 (map fst l) -> 0 < Z.pos p0 <= 4294967295
NOREP:list_norepet (p' :: map fst l)
p:positive
ASSOC:asr ! ev = Some (posToValue p)
s:stmnt
IN:(p', s') = (p, s) \/ In (p, s) l
SRUN:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
n:p <> p'

stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} s {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}
assumption. Qed. Hint Resolve transl_list_correct : verilogproof.

forall (A : Type) (m : AssocMap.t A) (p : positive) (v : A), (forall p0 : positive, In p0 (map fst (AssocMap.elements m)) -> 0 < Z.pos p0 <= Int.max_unsigned) -> m ! p = Some v -> 0 <= Z.pos p <= Int.max_unsigned

forall (A : Type) (m : AssocMap.t A) (p : positive) (v : A), (forall p0 : positive, In p0 (map fst (AssocMap.elements m)) -> 0 < Z.pos p0 <= Int.max_unsigned) -> m ! p = Some v -> 0 <= Z.pos p <= Int.max_unsigned
A:Type
m:AssocMap.t A
p:positive
v:A
LT:forall p0 : positive, In p0 (map fst (AssocMap.elements m)) -> 0 < Z.pos p0 <= Int.max_unsigned
S:m ! p = Some v

0 <= Z.pos p <= Int.max_unsigned
A:Type
m:AssocMap.t A
p:positive
v:A
LT:forall p0 : positive, In p0 (map fst (AssocMap.elements m)) -> 0 < Z.pos p0 <= Int.max_unsigned
S:m ! p = Some v

0 < Z.pos p <= Int.max_unsigned
A:Type
m:AssocMap.t A
p:positive
v:A
LT:forall p0 : positive, In p0 (map fst (AssocMap.elements m)) -> 0 < Z.pos p0 <= Int.max_unsigned
S:m ! p = Some v

In p (map fst (AssocMap.elements m))
A:Type
m:AssocMap.t A
p:positive
v:A
LT:forall p0 : positive, In p0 (map fst (AssocMap.elements m)) -> 0 < Z.pos p0 <= Int.max_unsigned
S:In (p, v) (AssocMap.elements m)

In p (map fst (AssocMap.elements m))
A:Type
m:AssocMap.t A
p:positive
v:A
LT:forall p0 : positive, In p0 (map fst (AssocMap.elements m)) -> 0 < Z.pos p0 <= Int.max_unsigned
x:(positive * A)%type
Heqx:x = (p, v)
S:In x (AssocMap.elements m)

In p (map fst (AssocMap.elements m))
exploit in_map. apply S.
A:Type
m:AssocMap.t A
p:positive
v:A
LT:forall p0 : positive, In p0 (map fst (AssocMap.elements m)) -> 0 < Z.pos p0 <= Int.max_unsigned
x:(positive * A)%type
Heqx:x = (p, v)
S:In x (AssocMap.elements m)

In (fst x) (map fst (AssocMap.elements m)) -> In p (map fst (AssocMap.elements m))
A:Type
m:AssocMap.t A
p:positive
v:A
LT:forall p0 : positive, In p0 (map fst (AssocMap.elements m)) -> 0 < Z.pos p0 <= Int.max_unsigned
S:In (p, v) (AssocMap.elements m)

In (fst (p, v)) (map fst (AssocMap.elements m)) -> In p (map fst (AssocMap.elements m))
A:Type
m:AssocMap.t A
p:positive
v:A
LT:forall p0 : positive, In p0 (map fst (AssocMap.elements m)) -> 0 < Z.pos p0 <= 4294967295
S:In (p, v) (AssocMap.elements m)
H:In p (map fst (AssocMap.elements m))

In p (map fst (AssocMap.elements m))
auto. Qed.

forall (l : list declaration) (asr : reg_associations) (asa : arr_associations) (f : fext), mis_stepp f asr asa (map Vdeclaration l) asr asa

forall (l : list declaration) (asr : reg_associations) (asa : arr_associations) (f : fext), mis_stepp f asr asa (map Vdeclaration l) asr asa

forall (asr : reg_associations) (asa : arr_associations) (f : fext), mis_stepp f asr asa (map Vdeclaration nil) asr asa
a:declaration
l:list declaration
IHl:forall (asr : reg_associations) (asa : arr_associations) (f : fext), mis_stepp f asr asa (map Vdeclaration l) asr asa
forall (asr : reg_associations) (asa : arr_associations) (f : fext), mis_stepp f asr asa (map Vdeclaration (a :: l)) asr asa

forall (asr : reg_associations) (asa : arr_associations) (f : fext), mis_stepp f asr asa (map Vdeclaration nil) asr asa
asr:reg_associations
asa:arr_associations
f:fext

mis_stepp f asr asa (map Vdeclaration nil) asr asa
constructor.
a:declaration
l:list declaration
IHl:forall (asr : reg_associations) (asa : arr_associations) (f : fext), mis_stepp f asr asa (map Vdeclaration l) asr asa

forall (asr : reg_associations) (asa : arr_associations) (f : fext), mis_stepp f asr asa (map Vdeclaration (a :: l)) asr asa
a:declaration
l:list declaration
IHl:forall (asr : reg_associations) (asa : arr_associations) (f : fext), mis_stepp f asr asa (map Vdeclaration l) asr asa
asr:reg_associations
asa:arr_associations
f:fext

mis_stepp f asr asa (map Vdeclaration (a :: l)) asr asa
a:declaration
l:list declaration
IHl:forall (asr : reg_associations) (asa : arr_associations) (f : fext), mis_stepp f asr asa (map Vdeclaration l) asr asa
asr:reg_associations
asa:arr_associations
f:fext

mis_stepp f asr asa (Vdeclaration a :: map Vdeclaration l) asr asa
econstructor.
a:declaration
l:list declaration
IHl:forall (asr : reg_associations) (asa : arr_associations) (f : fext), mis_stepp f asr asa (map Vdeclaration l) asr asa
asr:reg_associations
asa:arr_associations
f:fext

mis_stepp f asr asa (map Vdeclaration l) asr asa
auto. Qed. Hint Resolve mis_stepp_decl : verilogproof. Section CORRECTNESS. Variable prog: HTL.program. Variable tprog: program. Hypothesis TRANSL : match_prog prog tprog. Let ge : HTL.genv := Globalenvs.Genv.globalenv prog. Let tge : genv := Globalenvs.Genv.globalenv tprog.
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv

forall s : AST.ident, Genv.find_symbol tge s = Genv.find_symbol ge s
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv

forall s : AST.ident, Genv.find_symbol tge s = Genv.find_symbol ge s
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv
s:AST.ident

Genv.find_symbol tge s = Genv.find_symbol ge s
eapply (Genv.find_symbol_match TRANSL). Qed. Hint Resolve symbols_preserved : verilogproof.
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv

forall (b : Values.block) (f : HTL.fundef), Genv.find_funct_ptr ge b = Some f -> exists tf : fundef, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = tf
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv

forall (b : Values.block) (f : HTL.fundef), Genv.find_funct_ptr ge b = Some f -> exists tf : fundef, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = tf
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv
b:Values.block
f:HTL.fundef
H:Genv.find_funct_ptr ge b = Some f

exists tf : fundef, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = tf
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv
b:Values.block
f:HTL.fundef
H:Genv.find_funct_ptr ge b = Some f

(exists (cunit : AST.program (AST.fundef HTL.module) unit) (tf : AST.fundef module), Genv.find_funct_ptr (Genv.globalenv tprog) b = Some tf /\ tf = transl_fundef f /\ linkorder cunit prog) -> exists tf : fundef, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = tf
intros (cu & tf & P & Q & R); exists tf; auto. Qed. Hint Resolve function_ptr_translated : verilogproof.
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv

forall (v : Values.val) (f : HTL.fundef), Genv.find_funct ge v = Some f -> exists tf : fundef, Genv.find_funct tge v = Some tf /\ transl_fundef f = tf
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv

forall (v : Values.val) (f : HTL.fundef), Genv.find_funct ge v = Some f -> exists tf : fundef, Genv.find_funct tge v = Some tf /\ transl_fundef f = tf
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv
v:Values.val
f:HTL.fundef
H:Genv.find_funct ge v = Some f

exists tf : fundef, Genv.find_funct tge v = Some tf /\ transl_fundef f = tf
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv
v:Values.val
f:HTL.fundef
H:Genv.find_funct ge v = Some f

(exists (cunit : AST.program (AST.fundef HTL.module) unit) (tf : AST.fundef module), Genv.find_funct (Genv.globalenv tprog) v = Some tf /\ tf = transl_fundef f /\ linkorder cunit prog) -> exists tf : fundef, Genv.find_funct tge v = Some tf /\ transl_fundef f = tf
intros (cu & tf & P & Q & R); exists tf; auto. Qed. Hint Resolve functions_translated : verilogproof.
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv

Senv.equiv ge tge
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv

Senv.equiv ge tge
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv

Senv.equiv ge tge
eapply (Genv.senv_match TRANSL). Qed. Hint Resolve senv_preserved : verilogproof.
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv

forall (S1 : HTL.state) (t : Events.trace) (S2 : HTL.state), HTL.step ge S1 t S2 -> forall R1 : state, match_states S1 R1 -> exists R2 : state, plus step tge R1 t R2 /\ match_states S2 R2
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv

forall (S1 : HTL.state) (t : Events.trace) (S2 : HTL.state), HTL.step ge S1 t S2 -> forall R1 : state, match_states S1 R1 -> exists R2 : state, plus step tge R1 t R2 /\ match_states S2 R2
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
tge:=Genv.globalenv tprog:genv
g:HTL.genv
m:HTL.module
st:positive
sf:list HTL.stackframe
ctrl, data:stmnt
asr:AssocMap.t value
asa:AssocMap.t arr
basr1:AssocMap.t value
basa1:AssocMap.t arr
nasr1:AssocMap.t value
nasa1:AssocMap.t arr
basr2:AssocMap.t value
basa2:AssocMap.t arr
nasr2:AssocMap.t value
nasa2:AssocMap.t arr
f:fext
pstval:positive
H:asr ! (HTL.mod_reset m) = Some (ZToValue 0)
H0:asr ! (HTL.mod_finish m) = Some (ZToValue 0)
H1:asr ! (HTL.mod_st m) = Some (posToValue st)
H2:(HTL.mod_controllogic m) ! st = Some ctrl
H3:(HTL.mod_datapath m) ! st = Some data
H4:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := empty_assocmap |} {| assoc_blocking := asa; assoc_nonblocking := HTL.empty_stack m |} ctrl {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |} {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |}
H5:basr1 ! (HTL.mod_st m) = Some (posToValue st)
H6:stmnt_runp f {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |} {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |} data {| assoc_blocking := basr2; assoc_nonblocking := nasr2 |} {| assoc_blocking := basa2; assoc_nonblocking := nasa2 |}
H9:(merge_regs nasr2 basr2) ! (HTL.mod_st m) = Some (posToValue pstval)
H10:Z.pos pstval <= Int.max_unsigned
vstk:list stackframe
H17:match_stacks sf vstk

exists R2 : state, plus step tge (State vstk (transl_module m) st asr asa) Events.E0 R2 /\ match_states (HTL.State sf m pstval (merge_regs nasr2 basr2) (merge_arrs nasa2 basa2)) R2
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
tge:=Genv.globalenv tprog:genv
g:HTL.genv
m:HTL.module
st:HTL.node
asr:AssocMap.t value
asa:assocmap_arr
retval:value
sf:list HTL.stackframe
H:asr ! (HTL.mod_finish m) = Some (ZToValue 1)
H0:asr ! (HTL.mod_return m) = Some retval
vstk:list stackframe
H7:match_stacks sf vstk
exists R2 : state, plus step tge (State vstk (transl_module m) st asr asa) Events.E0 R2 /\ match_states (HTL.Returnstate sf retval) R2
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
tge:=Genv.globalenv tprog:genv
g:HTL.genv
m:HTL.module
exists R2 : state, plus step tge (Callstate nil (transl_module m) nil) Events.E0 R2 /\ match_states (HTL.State nil m (HTL.mod_entrypoint m) (((HTL.init_regs nil (HTL.mod_params m)) # (HTL.mod_st m) <- (posToValue (HTL.mod_entrypoint m))) # (HTL.mod_finish m) <- (ZToValue 0)) # (HTL.mod_reset m) <- (ZToValue 0) (HTL.empty_stack m)) R2
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
tge:=Genv.globalenv tprog:genv
g:HTL.genv
m:HTL.module
asr:assocmap_reg
asa:assocmap_arr
i:value
r:HTL.reg
sf:list HTL.stackframe
pc:HTL.node
vstk:list stackframe
H3:match_stacks (HTL.Stackframe r m pc asr asa :: sf) vstk
exists R2 : state, plus step tge (Returnstate vstk i) Events.E0 R2 /\ match_states (HTL.State sf m pc (asr # (HTL.mod_st m) <- (posToValue pc)) # r <- i asa) R2
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
tge:=Genv.globalenv tprog:genv
g:HTL.genv
m:HTL.module
st:positive
sf:list HTL.stackframe
ctrl, data:stmnt
asr:AssocMap.t value
asa:AssocMap.t arr
basr1:AssocMap.t value
basa1:AssocMap.t arr
nasr1:AssocMap.t value
nasa1:AssocMap.t arr
basr2:AssocMap.t value
basa2:AssocMap.t arr
nasr2:AssocMap.t value
nasa2:AssocMap.t arr
f:fext
pstval:positive
H:asr ! (HTL.mod_reset m) = Some (ZToValue 0)
H0:asr ! (HTL.mod_finish m) = Some (ZToValue 0)
H1:asr ! (HTL.mod_st m) = Some (posToValue st)
H2:(HTL.mod_controllogic m) ! st = Some ctrl
H3:(HTL.mod_datapath m) ! st = Some data
H4:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := empty_assocmap |} {| assoc_blocking := asa; assoc_nonblocking := HTL.empty_stack m |} ctrl {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |} {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |}
H5:basr1 ! (HTL.mod_st m) = Some (posToValue st)
H6:stmnt_runp f {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |} {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |} data {| assoc_blocking := basr2; assoc_nonblocking := nasr2 |} {| assoc_blocking := basa2; assoc_nonblocking := nasa2 |}
H9:(merge_regs nasr2 basr2) ! (HTL.mod_st m) = Some (posToValue pstval)
H10:Z.pos pstval <= Int.max_unsigned
vstk:list stackframe
H17:match_stacks sf vstk

exists R2 : state, plus step tge (State vstk (transl_module m) st asr asa) Events.E0 R2 /\ match_states (HTL.State sf m pstval (merge_regs nasr2 basr2) (merge_arrs nasa2 basa2)) R2
econstructor; split. apply Smallstep.plus_one. econstructor. assumption. assumption. eassumption. apply valueToPos_posToValue. split. lia. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. split. lia. apply HP. eassumption. eassumption. econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor. simpl. unfold find_assocmap. unfold AssocMapExt.get_default. rewrite H. trivial. econstructor. simpl. auto. auto. eapply transl_list_correct. intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. auto. apply Maps.PTree.elements_keys_norepet. eassumption. 2: { apply valueToPos_inj. apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. split. lia. apply HP. eassumption. eassumption. apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. split. lia. apply HP. eassumption. eassumption. trivial. } apply Maps.PTree.elements_correct. eassumption. eassumption. econstructor. econstructor. eapply transl_list_correct. intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto. apply Maps.PTree.elements_keys_norepet. eassumption. 2: { apply valueToPos_inj. apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. split. lia. apply HP. eassumption. eassumption. apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. split. lia. apply HP. eassumption. eassumption. trivial. } apply Maps.PTree.elements_correct. eassumption. eassumption. apply mis_stepp_decl. trivial. trivial. simpl. eassumption.
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
tge:=Genv.globalenv tprog:genv
g:HTL.genv
m:HTL.module
st:positive
sf:list HTL.stackframe
ctrl, data:stmnt
asr:AssocMap.t value
asa:AssocMap.t arr
basr1:AssocMap.t value
basa1:AssocMap.t arr
nasr1:AssocMap.t value
nasa1:AssocMap.t arr
basr2:AssocMap.t value
basa2:AssocMap.t arr
nasr2:AssocMap.t value
nasa2:AssocMap.t arr
f:fext
pstval:positive
H:asr ! (HTL.mod_reset m) = Some (ZToValue 0)
H0:asr ! (HTL.mod_finish m) = Some (ZToValue 0)
H1:asr ! (HTL.mod_st m) = Some (posToValue st)
H2:(HTL.mod_controllogic m) ! st = Some ctrl
H3:(HTL.mod_datapath m) ! st = Some data
H4:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := empty_assocmap |} {| assoc_blocking := asa; assoc_nonblocking := HTL.empty_stack m |} ctrl {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |} {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |}
H5:basr1 ! (HTL.mod_st m) = Some (posToValue st)
H6:stmnt_runp f {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |} {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |} data {| assoc_blocking := basr2; assoc_nonblocking := nasr2 |} {| assoc_blocking := basa2; assoc_nonblocking := nasa2 |}
H9:(merge_regs nasr2 basr2) ! (HTL.mod_st m) = Some (posToValue pstval)
H10:Z.pos pstval <= Int.max_unsigned
vstk:list stackframe
H17:match_stacks sf vstk

match_states (HTL.State sf m pstval (merge_regs nasr2 basr2) (merge_arrs nasa2 basa2)) (State vstk (transl_module m) (valueToPos (posToValue pstval)) (merge_regs nasr2 basr2) (merge_arrs nasa2 basa2))
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
tge:=Genv.globalenv tprog:genv
g:HTL.genv
m:HTL.module
st:positive
sf:list HTL.stackframe
ctrl, data:stmnt
asr:AssocMap.t value
asa:AssocMap.t arr
basr1:AssocMap.t value
basa1:AssocMap.t arr
nasr1:AssocMap.t value
nasa1:AssocMap.t arr
basr2:AssocMap.t value
basa2:AssocMap.t arr
nasr2:AssocMap.t value
nasa2:AssocMap.t arr
f:fext
pstval:positive
H:asr ! (HTL.mod_reset m) = Some (ZToValue 0)
H0:asr ! (HTL.mod_finish m) = Some (ZToValue 0)
H1:asr ! (HTL.mod_st m) = Some (posToValue st)
H2:(HTL.mod_controllogic m) ! st = Some ctrl
H3:(HTL.mod_datapath m) ! st = Some data
H4:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := empty_assocmap |} {| assoc_blocking := asa; assoc_nonblocking := HTL.empty_stack m |} ctrl {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |} {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |}
H5:basr1 ! (HTL.mod_st m) = Some (posToValue st)
H6:stmnt_runp f {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |} {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |} data {| assoc_blocking := basr2; assoc_nonblocking := nasr2 |} {| assoc_blocking := basa2; assoc_nonblocking := nasa2 |}
H9:(merge_regs nasr2 basr2) ! (HTL.mod_st m) = Some (posToValue pstval)
H10:Z.pos pstval <= Int.max_unsigned
vstk:list stackframe
H17:match_stacks sf vstk

match_states (HTL.State sf m pstval (merge_regs nasr2 basr2) (merge_arrs nasa2 basa2)) (State vstk (transl_module m) pstval (merge_regs nasr2 basr2) (merge_arrs nasa2 basa2))
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
tge:=Genv.globalenv tprog:genv
g:HTL.genv
m:HTL.module
st:positive
sf:list HTL.stackframe
ctrl, data:stmnt
asr:AssocMap.t value
asa:AssocMap.t arr
basr1:AssocMap.t value
basa1:AssocMap.t arr
nasr1:AssocMap.t value
nasa1:AssocMap.t arr
basr2:AssocMap.t value
basa2:AssocMap.t arr
nasr2:AssocMap.t value
nasa2:AssocMap.t arr
f:fext
pstval:positive
H:asr ! (HTL.mod_reset m) = Some (ZToValue 0)
H0:asr ! (HTL.mod_finish m) = Some (ZToValue 0)
H1:asr ! (HTL.mod_st m) = Some (posToValue st)
H2:(HTL.mod_controllogic m) ! st = Some ctrl
H3:(HTL.mod_datapath m) ! st = Some data
H4:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := empty_assocmap |} {| assoc_blocking := asa; assoc_nonblocking := HTL.empty_stack m |} ctrl {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |} {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |}
H5:basr1 ! (HTL.mod_st m) = Some (posToValue st)
H6:stmnt_runp f {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |} {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |} data {| assoc_blocking := basr2; assoc_nonblocking := nasr2 |} {| assoc_blocking := basa2; assoc_nonblocking := nasa2 |}
H9:(merge_regs nasr2 basr2) ! (HTL.mod_st m) = Some (posToValue pstval)
H10:Z.pos pstval <= Int.max_unsigned
vstk:list stackframe
H17:match_stacks sf vstk
0 <= Z.pos pstval <= Int.max_unsigned
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
tge:=Genv.globalenv tprog:genv
g:HTL.genv
m:HTL.module
st:positive
sf:list HTL.stackframe
ctrl, data:stmnt
asr:AssocMap.t value
asa:AssocMap.t arr
basr1:AssocMap.t value
basa1:AssocMap.t arr
nasr1:AssocMap.t value
nasa1:AssocMap.t arr
basr2:AssocMap.t value
basa2:AssocMap.t arr
nasr2:AssocMap.t value
nasa2:AssocMap.t arr
f:fext
pstval:positive
H:asr ! (HTL.mod_reset m) = Some (ZToValue 0)
H0:asr ! (HTL.mod_finish m) = Some (ZToValue 0)
H1:asr ! (HTL.mod_st m) = Some (posToValue st)
H2:(HTL.mod_controllogic m) ! st = Some ctrl
H3:(HTL.mod_datapath m) ! st = Some data
H4:stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := empty_assocmap |} {| assoc_blocking := asa; assoc_nonblocking := HTL.empty_stack m |} ctrl {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |} {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |}
H5:basr1 ! (HTL.mod_st m) = Some (posToValue st)
H6:stmnt_runp f {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |} {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |} data {| assoc_blocking := basr2; assoc_nonblocking := nasr2 |} {| assoc_blocking := basa2; assoc_nonblocking := nasa2 |}
H9:(merge_regs nasr2 basr2) ! (HTL.mod_st m) = Some (posToValue pstval)
H10:Z.pos pstval <= Int.max_unsigned
vstk:list stackframe
H17:match_stacks sf vstk

0 <= Z.pos pstval <= Int.max_unsigned
lia.
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
tge:=Genv.globalenv tprog:genv
g:HTL.genv
m:HTL.module
st:HTL.node
asr:AssocMap.t value
asa:assocmap_arr
retval:value
sf:list HTL.stackframe
H:asr ! (HTL.mod_finish m) = Some (ZToValue 1)
H0:asr ! (HTL.mod_return m) = Some retval
vstk:list stackframe
H7:match_stacks sf vstk

exists R2 : state, plus step tge (State vstk (transl_module m) st asr asa) Events.E0 R2 /\ match_states (HTL.Returnstate sf retval) R2
econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption.
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
tge:=Genv.globalenv tprog:genv
g:HTL.genv
m:HTL.module
st:HTL.node
asr:AssocMap.t value
asa:assocmap_arr
retval:value
sf:list HTL.stackframe
H:asr ! (HTL.mod_finish m) = Some (ZToValue 1)
H0:asr ! (HTL.mod_return m) = Some retval
vstk:list stackframe
H7:match_stacks sf vstk

match_states (HTL.Returnstate sf retval) (Returnstate vstk retval)
constructor; assumption.
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
tge:=Genv.globalenv tprog:genv
g:HTL.genv
m:HTL.module

exists R2 : state, plus step tge (Callstate nil (transl_module m) nil) Events.E0 R2 /\ match_states (HTL.State nil m (HTL.mod_entrypoint m) (((HTL.init_regs nil (HTL.mod_params m)) # (HTL.mod_st m) <- (posToValue (HTL.mod_entrypoint m))) # (HTL.mod_finish m) <- (ZToValue 0)) # (HTL.mod_reset m) <- (ZToValue 0) (HTL.empty_stack m)) R2
econstructor; split. apply Smallstep.plus_one.
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
tge:=Genv.globalenv tprog:genv
g:HTL.genv
m:HTL.module

match_states (HTL.State nil m (HTL.mod_entrypoint m) (((HTL.init_regs nil (HTL.mod_params m)) # (HTL.mod_st m) <- (posToValue (HTL.mod_entrypoint m))) # (HTL.mod_finish m) <- (ZToValue 0)) # (HTL.mod_reset m) <- (ZToValue 0) (HTL.empty_stack m)) (State nil (transl_module m) (mod_entrypoint (transl_module m)) (((init_params nil (mod_args (transl_module m))) # (mod_st (transl_module m)) <- (posToValue (mod_entrypoint (transl_module m)))) # (mod_finish (transl_module m)) <- (ZToValue 0)) # (mod_reset (transl_module m)) <- (ZToValue 0) (empty_stack (transl_module m)))
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
tge:=Genv.globalenv tprog:genv
g:HTL.genv
m:HTL.module

match_stacks nil nil
constructor.
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
tge:=Genv.globalenv tprog:genv
g:HTL.genv
m:HTL.module
asr:assocmap_reg
asa:assocmap_arr
i:value
r:HTL.reg
sf:list HTL.stackframe
pc:HTL.node
vstk:list stackframe
H3:match_stacks (HTL.Stackframe r m pc asr asa :: sf) vstk

exists R2 : state, plus step tge (Returnstate vstk i) Events.E0 R2 /\ match_states (HTL.State sf m pc (asr # (HTL.mod_st m) <- (posToValue pc)) # r <- i asa) R2
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
tge:=Genv.globalenv tprog:genv
g:HTL.genv
m:HTL.module
asr:assocmap_reg
asa:assocmap_arr
i:value
r:HTL.reg
sf:list HTL.stackframe
pc:HTL.node
vstk0:list stackframe
H7:match_stacks sf vstk0

exists R2 : state, plus step tge (Returnstate (Stackframe r (transl_module m) pc asr asa :: vstk0) i) Events.E0 R2 /\ match_states (HTL.State sf m pc (asr # (HTL.mod_st m) <- (posToValue pc)) # r <- i asa) R2
econstructor; split. apply Smallstep.plus_one. constructor.
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
tge:=Genv.globalenv tprog:genv
g:HTL.genv
m:HTL.module
asr:assocmap_reg
asa:assocmap_arr
i:value
r:HTL.reg
sf:list HTL.stackframe
pc:HTL.node
vstk0:list stackframe
H7:match_stacks sf vstk0

match_states (HTL.State sf m pc (asr # (HTL.mod_st m) <- (posToValue pc)) # r <- i asa) (State vstk0 (transl_module m) pc (asr # (mod_st (transl_module m)) <- (posToValue pc)) # r <- i asa)
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
tge:=Genv.globalenv tprog:genv
g:HTL.genv
m:HTL.module
asr:assocmap_reg
asa:assocmap_arr
i:value
r:HTL.reg
sf:list HTL.stackframe
pc:HTL.node
vstk0:list stackframe
H7:match_stacks sf vstk0

match_stacks sf vstk0
assumption. Qed. Hint Resolve transl_step_correct : verilogproof.
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv

forall s1 : Smallstep.state (HTL.semantics prog), Smallstep.initial_state (HTL.semantics prog) s1 -> exists s2 : Smallstep.state (semantics tprog), Smallstep.initial_state (semantics tprog) s2 /\ match_states s1 s2
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv

forall s1 : Smallstep.state (HTL.semantics prog), Smallstep.initial_state (HTL.semantics prog) s1 -> exists s2 : Smallstep.state (semantics tprog), Smallstep.initial_state (semantics tprog) s2 /\ match_states s1 s2
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv
b:Values.block
m0:Memory.Mem.mem
m:HTL.module
ge0:=Genv.globalenv prog:Genv.t HTL.fundef unit
H:Genv.init_mem prog = Some m0
H0:Genv.find_symbol ge0 (AST.prog_main prog) = Some b
H1:Genv.find_funct_ptr ge0 b = Some (AST.Internal m)

exists s2 : Smallstep.state (semantics tprog), Smallstep.initial_state (semantics tprog) s2 /\ match_states (HTL.Callstate nil m nil) s2
econstructor; split. econstructor. apply (Genv.init_mem_transf TRANSL); eauto. rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog); eauto. symmetry; eapply Linking.match_program_main; eauto. exploit function_ptr_translated; eauto. intros [tf [A B]]. inv B.
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv
b:Values.block
m0:Memory.Mem.mem
m:HTL.module
ge0:=Genv.globalenv prog:Genv.t HTL.fundef unit
H:Genv.init_mem prog = Some m0
H0:Genv.find_symbol ge0 (AST.prog_main prog) = Some b
H1:Genv.find_funct_ptr ge0 b = Some (AST.Internal m)

match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil)
constructor. Qed. Hint Resolve transl_initial_states : verilogproof.
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv

forall (s1 : Smallstep.state (HTL.semantics prog)) (s2 : Smallstep.state (semantics tprog)) (r : int), match_states s1 s2 -> Smallstep.final_state (HTL.semantics prog) s1 r -> Smallstep.final_state (semantics tprog) s2 r
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv

forall (s1 : Smallstep.state (HTL.semantics prog)) (s2 : Smallstep.state (semantics tprog)) (r : int), match_states s1 s2 -> Smallstep.final_state (HTL.semantics prog) s1 r -> Smallstep.final_state (semantics tprog) s2 r
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv
s1:Smallstep.state (HTL.semantics prog)
s2:Smallstep.state (semantics tprog)
r:int
H:match_states s1 s2
H0:Smallstep.final_state (HTL.semantics prog) s1 r

Smallstep.final_state (semantics tprog) s2 r
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv
s2:Smallstep.state (semantics tprog)
retval:value
H:match_states (HTL.Returnstate nil retval) s2

Smallstep.final_state (semantics tprog) s2 (valueToInt retval)
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv
retval:value
vstk:list stackframe
H3:match_stacks nil vstk

Smallstep.final_state (semantics tprog) (Returnstate vstk retval) (valueToInt retval)
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv
retval:value

Smallstep.final_state (semantics tprog) (Returnstate nil retval) (valueToInt retval)
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv
retval:value

valueToInt retval = valueToInt retval
reflexivity. Qed. Hint Resolve transl_final_states : verilogproof.
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv

forward_simulation (HTL.semantics prog) (semantics tprog)
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv

forward_simulation (HTL.semantics prog) (semantics tprog)
prog:HTL.program
tprog:program
TRANSL:match_prog prog tprog
ge:=Genv.globalenv prog:HTL.genv
tge:=Genv.globalenv tprog:genv

forall id : AST.ident, Senv.public_symbol (symbolenv (semantics tprog)) id = Senv.public_symbol (symbolenv (HTL.semantics prog)) id
apply senv_preserved. Qed. End CORRECTNESS.