Squirrel Prover - Squirrel Prover

hash H.

RUNNING EXAMPLE

This protocol is a variant of the OSK protocol described in: M. Ohkubo, K. Suzuki, S. Kinoshita et al., “Cryptographic approach to “privacy-friendly” tags,” RFID privacy workshop, vol. 82. Cambridge, USA, 2003.

Each tag is associated to a mutable state sT initialized with s0. Readers have access to a database containing an entry sR for each authorized tag.

sT := H(sT,k) T -> R : G(sT,k’)

input x; sR := H(sR,k) if x = G(H(sR,k),k’) with sR in DB R -> T : ok

COMMENTS - In this model we add in parallel a process in order to provide the attacker the ability to compute hashes with their respective keys (without knowing these keys). - The reader process is not modelled here, this is left for future work.

HELPING LEMMAS - last update - disjoint chains - monotonic chain

SECURITY PROPERTIES - strong secrecy ******************************************************************************

hash G.
name k : message.
name k' : message.
name s0 : index->message.
mutable s (i:index) : message = s0(i).

channel o.
channel c.

system (
(O: !_j in(o,x); out(o,<H(x,k),G(x,k')>)) |
(A: !_i !_j s(i):=H(s(i),k); out(o,G(s(i),k')))
). System before processing:

(O: !_j in(o,x); out(o,pair(H(x,k),G(x,k'))); null) |
(A: !_i !_j s(i) := H(s(i),k); out(o,G(s(i),k')); null)

System after processing:

(!_j in(o,x); O: out(o,pair(H(x,k),G(x,k'))); null) |
(!_i !_j s(i) := H(s(i),k); A: out(o,G(s(i),k')); null)

System default registered with actions (init,O,A).

include Basic. Goal eq_sym :
(x = y) = (y = x)
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x,y:'a
----------------------------------------
(x = y) = (y = x)

[> Line 11: by (rewrite ...)
[goal> Goal eq_sym is proved
Exiting proof mode.

Goal neq_sym :
(x <> y) = (y <> x)
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x,y:'a
----------------------------------------
(x <> y) = (y <> x)

[> Line 14: by (rewrite ...)
[goal> Goal neq_sym is proved
Exiting proof mode.

Goal eq_refl :
(x = x) = true
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x:'a
----------------------------------------
(x = x) = true

[> Line 18: by (rewrite ...)
[goal> Goal eq_refl is proved
Exiting proof mode.

Goal false_true :
(false = true) = false
[goal> Focused goal (1/1):
System: any
----------------------------------------
(false = true) = false

[> Line 30: by (rewrite ...)
[goal> Goal false_true is proved
Exiting proof mode.

Goal eq_true :
(b = true) = b
[goal> Focused goal (1/1):
System: any
Variables: b:bool
----------------------------------------
(b = true) = b

[> Line 35: by (case b)
[goal> Goal eq_true is proved
Exiting proof mode.

Goal eq_true2 :
(true = b) = b
[goal> Focused goal (1/1):
System: any
Variables: b:bool
----------------------------------------
(true = b) = b

[> Line 39: by (case b)
[goal> Goal eq_true2 is proved
Exiting proof mode.

Goal not_not :
not(not(b)) = b
[goal> Focused goal (1/1):
System: any
Variables: b:bool
----------------------------------------
not(not(b)) = b

[> Line 54: by (case b)
[goal> Goal not_not is proved
Exiting proof mode.

Goal not_eq :
not(x = y) = (x <> y)
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x,y:'a
----------------------------------------
not(x = y) = (x <> y)

[> Line 60: by (rewrite ...)
[goal> Goal not_eq is proved
Exiting proof mode.

Goal not_neq :
not(x <> y) = (x = y)
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x,y:'a
----------------------------------------
not(x <> y) = (x = y)

[> Line 66: by (rewrite ...)
[goal> Goal not_neq is proved
Exiting proof mode.

Goal not_eqfalse :
(b = false) = not(b)
[goal> Focused goal (1/1):
System: any
Variables: b:bool
----------------------------------------
(b = false) = not(b)

[> Line 72: by (case b)
[goal> Goal not_eqfalse is proved
Exiting proof mode.

Goal eq_false :
((x = y) = false) = (x <> y)
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x,y:'a
----------------------------------------
((x = y) = false) = (x <> y)

[> Line 80: (rewrite ...)
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x,y:'a
----------------------------------------
((x = y) = false) = not(x = y)

[> Line 80: ((case (x = y));(intro _))
[goal> Focused goal (1/2):
System: any
Type variables: 'a
Variables: x,y:'a
_: x = y
----------------------------------------
(true = false) = not(true)

[> Line 80: simpl
[goal> Focused goal (1/2):
System: any
Type variables: 'a
Variables: x,y:'a
_: x = y
----------------------------------------
true

[> Line 80: auto
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x,y:'a
_: not(x = y)
----------------------------------------
(false = false) = not(false)

[> Line 81: by (rewrite ...)
[goal> Goal eq_false is proved
Exiting proof mode.

Goal and_true_r :
(b && true) = b
[goal> Focused goal (1/1):
System: any
Variables: b:bool
----------------------------------------
(b && true) = b

[> Line 94: by (rewrite ... ...)
[goal> Goal and_true_r is proved
Exiting proof mode.

Goal and_false_r :
(b && false) = false
[goal> Focused goal (1/1):
System: any
Variables: b:bool
----------------------------------------
(b && false) = false

[> Line 101: by (rewrite ... ...)
[goal> Goal and_false_r is proved
Exiting proof mode.

Goal or_false_r :
(b || false) = b
[goal> Focused goal (1/1):
System: any
Variables: b:bool
----------------------------------------
(b || false) = b

[> Line 112: by (rewrite ... ...)
[goal> Goal or_false_r is proved
Exiting proof mode.

Goal or_true_r :
(b || true) = true
[goal> Focused goal (1/1):
System: any
Variables: b:bool
----------------------------------------
(b || true) = true

[> Line 119: by (rewrite ... ...)
[goal> Goal or_true_r is proved
Exiting proof mode.

Goal not_and :
not((a && b)) = (not(a) || not(b))
[goal> Focused goal (1/1):
System: any
Variables: a,b:bool
----------------------------------------
not((a && b)) = (not(a) || not(b))

[> Line 128: (rewrite ...)
[goal> Focused goal (1/1):
System: any
Variables: a,b:bool
----------------------------------------
not((a && b)) <=> not(a) || not(b)

[> Line 129: (((case a);(case b));(intro //=))
[goal> Goal not_and is proved
Exiting proof mode.

Goal not_or :
not((a || b)) = (not(a) && not(b))
[goal> Focused goal (1/1):
System: any
Variables: a,b:bool
----------------------------------------
not((a || b)) = (not(a) && not(b))

[> Line 134: (rewrite ...)
[goal> Focused goal (1/1):
System: any
Variables: a,b:bool
----------------------------------------
not((a || b)) <=> not(a) && not(b)

[> Line 135: (((case a);(case b));(intro //=))
[goal> Goal not_or is proved
Exiting proof mode.

Goal if_true :
b => if b then x else y = x
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b:bool,x,y:'a
----------------------------------------
b => if b then x else y = x

[> Line 144: (intro *)
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b:bool,x,y:'a
H: b
----------------------------------------
if b then x else y = x

[> Line 145: (case if b then x else y)
[goal> Focused goal (1/2):
System: any
Type variables: 'a
Variables: b:bool,x,y:'a
H: b
----------------------------------------
b && if b then x else y = x => x = x

[> Line 146: auto
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b:bool,x,y:'a
H: b
----------------------------------------
not(b) && if b then x else y = y => y = x

[> Line 147: (intro [HH _])
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b:bool,x,y:'a
H: b
HH: not(b)
_: if b then x else y = y
----------------------------------------
y = x

[> Line 147: by (have ... as )
[goal> Goal if_true is proved
Exiting proof mode.

Goal if_true0 :
if true then x else y = x
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x,y:'a
----------------------------------------
if true then x else y = x

[> Line 153: by (rewrite ...)
[goal> Goal if_true0 is proved
Exiting proof mode.

Goal if_false :
not(b) => if b then x else y = y
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b:bool,x,y:'a
----------------------------------------
not(b) => if b then x else y = y

[> Line 160: ((intro *);(case if b then x else y))
[goal> Focused goal (1/2):
System: any
Type variables: 'a
Variables: b:bool,x,y:'a
H: not(b)
----------------------------------------
b && if b then x else y = x => x = y

[> Line 161: (intro [HH _])
[goal> Focused goal (1/2):
System: any
Type variables: 'a
Variables: b:bool,x,y:'a
H: not(b)
HH: b
_: if b then x else y = x
----------------------------------------
x = y

[> Line 161: by (have ... as )
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b:bool,x,y:'a
H: not(b)
----------------------------------------
not(b) && if b then x else y = y => y = y

[> Line 162: auto
[goal> Goal if_false is proved
Exiting proof mode.

Goal if_false0 :
if false then x else y = y
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x,y:'a
----------------------------------------
if false then x else y = y

[> Line 168: by (rewrite ...)
[goal> Goal if_false0 is proved
Exiting proof mode.

Goal if_then_then :
if b then if b' then x else y else y = if (b && b') then x else y
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b,b':bool,x,y:'a
----------------------------------------
if b then if b' then x else y else y = if (b && b') then x else y

[> Line 175: by ((case b);(case b'))
[goal> Goal if_then_then is proved
Exiting proof mode.

Goal if_then_implies :
if b then if b' then x else y else z =
if b then if (b => b') then x else y else z
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b,b':bool,x,y,z:'a
----------------------------------------
if b then if b' then x else y else z =
if b then if (b => b') then x else y else z

[> Line 182: ((case b);
((intro H);((case b');((intro H');(simpl;(try auto))))))

[goal> Focused goal (1/2):
System: any
Type variables: 'a
Variables: b,b':bool,x,y,z:'a
H: b
H': b'
----------------------------------------
x = if (true => true) then x else y

[> Line 183: by (rewrite ...)
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b,b':bool,x,y,z:'a
H: b
H': not(b')
----------------------------------------
y = if (true => false) then x else y

[> Line 184: (rewrite ...)
[goal> Focused goal (1/2):
System: any
Type variables: 'a
Variables: b,b':bool,x,y,z:'a
H: b
H': not(b')
----------------------------------------
not((true => false))

[> Line 185: ((intro Habs);by (have ... as ))
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b,b':bool,x,y,z:'a
H: b
H': not(b')
----------------------------------------
y = y

[> Line 186: auto
[goal> Goal if_then_implies is proved
Exiting proof mode.

Goal if_same :
if b then x else x = x
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b:bool,x:'a
----------------------------------------
if b then x else x = x

[> Line 192: by (case b)
[goal> Goal if_same is proved
Exiting proof mode.

Goal if_then :
b = b' => if b then if b' then x else y else z = if b then x else z
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b,b':bool,x,y,z:'a
----------------------------------------
b = b' => if b then if b' then x else y else z = if b then x else z

[> Line 201: by ((intro ->);(case b'))
[goal> Goal if_then is proved
Exiting proof mode.

Goal if_else :
b = b' => if b then x else if b' then y else z = if b then x else z
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b,b':bool,x,y,z:'a
----------------------------------------
b = b' => if b then x else if b' then y else z = if b then x else z

[> Line 210: by ((intro ->);(case b'))
[goal> Goal if_else is proved
Exiting proof mode.

Goal if_then_not :
b = not(b') => if b then if b' then x else y else z = if b then y else z
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b,b':bool,x,y,z:'a
----------------------------------------
b = not(b') => if b then if b' then x else y else z = if b then y else z

[> Line 219: by ((intro ->);(case b'))
[goal> Goal if_then_not is proved
Exiting proof mode.

Goal if_else_not :
b = not(b') => if b then x else if b' then y else z = if b then x else y
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b,b':bool,x,y,z:'a
----------------------------------------
b = not(b') => if b then x else if b' then y else z = if b then x else y

[> Line 228: by ((intro ->);(case b'))
[goal> Goal if_else_not is proved
Exiting proof mode.

Goal fst_pair :
fst(<x,y>) = x
[goal> Focused goal (1/1):
System: any
Variables: x,y:message
----------------------------------------
fst(<x,y>) = x

[> Line 236: auto
[goal> Goal fst_pair is proved
Exiting proof mode.

Goal snd_pair :
snd(<x,y>) = y
[goal> Focused goal (1/1):
System: any
Variables: x,y:message
----------------------------------------
snd(<x,y>) = y

[> Line 240: auto
[goal> Goal snd_pair is proved
Exiting proof mode.

Goal iff_refl :
(x <=> x) = true
[goal> Focused goal (1/1):
System: any
Variables: x:bool
----------------------------------------
(x <=> x) = true

[> Line 248: by (rewrite ...)
[goal> Goal iff_refl is proved
Exiting proof mode.

Goal iff_sym :
(x <=> y) = (y <=> x)
[goal> Focused goal (1/1):
System: any
Variables: x,y:bool
----------------------------------------
(x <=> y) = (y <=> x)

[> Line 254: by (rewrite ...)
[goal> Goal iff_sym is proved
Exiting proof mode.

Goal true_iff_false :
(true <=> false) = false
[goal> Focused goal (1/1):
System: any
----------------------------------------
(true <=> false) = false

[> Line 259: by (rewrite ...)
[goal> Goal true_iff_false is proved
Exiting proof mode.

Goal false_iff_true :
(false <=> true) = false
[goal> Focused goal (1/1):
System: any
----------------------------------------
(false <=> true) = false

[> Line 265: by (rewrite ...)
[goal> Goal false_iff_true is proved
Exiting proof mode.

Goal exists_false1 :
(exists (a:'a), false) = false
[goal> Focused goal (1/1):
System: any
Type variables: 'a
----------------------------------------
(exists (a:'a), false) = false

[> Line 277: by (rewrite ...)
[goal> Goal exists_false1 is proved
Exiting proof mode.

Goal exists_false2 :
(exists (a:'a,b:'b), false) = false
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b
----------------------------------------
(exists (a:'a,b:'b), false) = false

[> Line 281: by (rewrite ...)
[goal> Goal exists_false2 is proved
Exiting proof mode.

Goal exists_false3 :
(exists (a:'a,b:'b,c:'c), false) = false
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b, 'c
----------------------------------------
(exists (a:'a,b:'b,c:'c), false) = false

[> Line 285: by (rewrite ...)
[goal> Goal exists_false3 is proved
Exiting proof mode.

Goal exists_false4 :
(exists (a:'a,b:'b,c:'c,d:'d), false) = false
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b, 'c, 'd
----------------------------------------
(exists (a:'a,b:'b,c:'c,d:'d), false) = false

[> Line 289: by (rewrite ...)
[goal> Goal exists_false4 is proved
Exiting proof mode.

Goal exists_false5 :
(exists (a:'a,b:'b,c:'c,d:'d,e:'e), false) = false
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b, 'c, 'd, 'e
----------------------------------------
(exists (a:'a,b:'b,c:'c,d:'d,e:'e), false) = false

[> Line 293: by (rewrite ...)
[goal> Goal exists_false5 is proved
Exiting proof mode.

Goal exists_false6 :
(exists (a:'a,b:'b,c:'c,d:'d,e:'e,f:'f), false) = false
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b, 'c, 'd, 'e, 'f
----------------------------------------
(exists (a:'a,b:'b,c:'c,d:'d,e:'e,f:'f), false) = false

[> Line 297: by (rewrite ...)
[goal> Goal exists_false6 is proved
Exiting proof mode.

Goal forall_true1 :
(forall (a:'a), true) = true
[goal> Focused goal (1/1):
System: any
Type variables: 'a
----------------------------------------
(forall (a:'a), true) = true

[> Line 307: auto
[goal> Goal forall_true1 is proved
Exiting proof mode.

Goal forall_true2 :
(forall (a:'a,b:'b), true) = true
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b
----------------------------------------
(forall (a:'a,b:'b), true) = true

[> Line 311: auto
[goal> Goal forall_true2 is proved
Exiting proof mode.

Goal forall_true3 :
(forall (a:'a,b:'b,c:'c), true) = true
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b, 'c
----------------------------------------
(forall (a:'a,b:'b,c:'c), true) = true

[> Line 315: auto
[goal> Goal forall_true3 is proved
Exiting proof mode.

Goal forall_true4 :
(forall (a:'a,b:'b,c:'c,d:'d), true) = true
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b, 'c, 'd
----------------------------------------
(forall (a:'a,b:'b,c:'c,d:'d), true) = true

[> Line 319: auto
[goal> Goal forall_true4 is proved
Exiting proof mode.

Goal forall_true5 :
(forall (a:'a,b:'b,c:'c,d:'d,e:'e), true) = true
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b, 'c, 'd, 'e
----------------------------------------
(forall (a:'a,b:'b,c:'c,d:'d,e:'e), true) = true

[> Line 323: auto
[goal> Goal forall_true5 is proved
Exiting proof mode.

Goal forall_true6 :
(forall (a:'a,b:'b,c:'c,d:'d,e:'e,f:'f), true) = true
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b, 'c, 'd, 'e, 'f
----------------------------------------
(forall (a:'a,b:'b,c:'c,d:'d,e:'e,f:'f), true) = true

[> Line 327: auto
[goal> Goal forall_true6 is proved
Exiting proof mode.

[warning> loaded: Basic.sp <]

(* AXIOMS *)

(* We assume that the attacker never repeats a query to the oracle. *)

axiom unique_queries : forall (i,j:index) i <> j => input@O(i) <> input@O(j).

(* HELPING LEMMAS *)

(* See `running-ex.sp` for more details about lastupdate_XXX lemmas. *)

goal lastupdate_pure : forall (i:index,tau:timestamp), happens(tau) => (
(forall j:index, happens(A(i,j)) => A(i,j)>tau) ||
(exists j:index, happens(A(i,j)) && A(i,j)<=tau
&& forall jj:index, happens(A(i,jj)) && A(i,jj)<=tau => A(i,jj)<=A(i,j))). Goal lastupdate_pure :
forall (i:index,tau:timestamp),
happens(tau) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)

Proof. [goal> Focused goal (1/1):
System: left:default/left, right:default/right
----------------------------------------
forall (i:index,tau:timestamp),
happens(tau) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)

intro i. [> Line 66: (intro i)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i:index
----------------------------------------
forall (tau:timestamp),
happens(tau) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)

induction => tau IH Hp. [> Line 67: (induction;(intro tau IH Hp))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i:index,tau:timestamp
Hp: happens(tau)
IH: forall (tau0:timestamp),
tau0 < tau =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
----------------------------------------
(forall (j:index), happens(A(i,j)) => A(i,j) > tau) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau &&
forall (jj:index), happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)

case tau. [> Line 68: (case tau)
[goal> Focused goal (1/3):
System: left:default/left, right:default/right
Variables: i:index,tau:timestamp
Hp: happens(tau)
IH: forall (tau0:timestamp),
tau0 < tau =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
----------------------------------------
tau = init =>
(forall (j:index), happens(A(i,j)) => A(i,j) > init) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= init &&
forall (jj:index), happens(A(i,jj)) && A(i,jj) <= init => A(i,jj) <= A(i,j)

+ (* init *)
intro Eq; left; intro j HpA; by auto. [> Line 71: ((intro Eq);(left;((intro j HpA);by auto)))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i:index,tau:timestamp
Hp: happens(tau)
IH: forall (tau0:timestamp),
tau0 < tau =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
----------------------------------------
(exists (j:index), tau = O(j)) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau &&
forall (jj:index), happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)

+ (* O(i) *)
intro [j Eq]; subst tau, O(j). [> Line 74: ((intro [j Eq]);(subst tau, O(j)))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j:index
Hp: happens(O(j))
IH: forall (tau0:timestamp),
tau0 < O(j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
----------------------------------------
(forall (j0:index), happens(A(i,j0)) => A(i,j0) > O(j)) ||
exists (j0:index),
happens(A(i,j0)) &&
A(i,j0) <= O(j) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= O(j) => A(i,jj) <= A(i,j0)

use IH with pred(O(j)) => //. [> Line 75: ((have ... as );(intro //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j:index
H: (forall (j0:index), happens(A(i,j0)) => A(i,j0) > pred(O(j))) ||
exists (j0:index),
happens(A(i,j0)) &&
A(i,j0) <= pred(O(j)) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(O(j)) => A(i,jj) <= A(i,j0)
Hp: happens(O(j))
IH: forall (tau0:timestamp),
tau0 < O(j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
----------------------------------------
(forall (j0:index), happens(A(i,j0)) => A(i,j0) > O(j)) ||
exists (j0:index),
happens(A(i,j0)) &&
A(i,j0) <= O(j) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= O(j) => A(i,jj) <= A(i,j0)

destruct H as [H1 | [j0 H2]]. [> Line 76: (destruct H, [H1|[j0 H2]])
[goal> Focused goal (1/3):
System: left:default/left, right:default/right
Variables: i,j:index
H1: forall (j0:index), happens(A(i,j0)) => A(i,j0) > pred(O(j))
Hp: happens(O(j))
IH: forall (tau0:timestamp),
tau0 < O(j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
----------------------------------------
(forall (j0:index), happens(A(i,j0)) => A(i,j0) > O(j)) ||
exists (j0:index),
happens(A(i,j0)) &&
A(i,j0) <= O(j) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= O(j) => A(i,jj) <= A(i,j0)

- left; intro j0 HpA; by use H1 with j0. [> Line 77: (left;((intro j0 HpA);by (have ... as )))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0:index
H2: happens(A(i,j0)) &&
A(i,j0) <= pred(O(j)) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(O(j)) => A(i,jj) <= A(i,j0)
Hp: happens(O(j))
IH: forall (tau0:timestamp),
tau0 < O(j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
----------------------------------------
(forall (j0:index), happens(A(i,j0)) => A(i,j0) > O(j)) ||
exists (j0:index),
happens(A(i,j0)) &&
A(i,j0) <= O(j) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= O(j) => A(i,jj) <= A(i,j0)

- right. [> Line 78: right
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0:index
H2: happens(A(i,j0)) &&
A(i,j0) <= pred(O(j)) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(O(j)) => A(i,jj) <= A(i,j0)
Hp: happens(O(j))
IH: forall (tau0:timestamp),
tau0 < O(j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
----------------------------------------
exists (j0:index),
happens(A(i,j0)) &&
A(i,j0) <= O(j) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= O(j) => A(i,jj) <= A(i,j0)

destruct H2 as [_ _ H2]. [> Line 78: (destruct H2, [_ _ H2])
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0:index
H2: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(O(j)) => A(i,jj) <= A(i,j0)
Hp: happens(O(j))
IH: forall (tau0:timestamp),
tau0 < O(j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
_: A(i,j0) <= pred(O(j))
_: happens(A(i,j0))
----------------------------------------
exists (j0:index),
happens(A(i,j0)) &&
A(i,j0) <= O(j) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= O(j) => A(i,jj) <= A(i,j0)

exists j0. [> Line 79: (exists j0)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0:index
H2: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(O(j)) => A(i,jj) <= A(i,j0)
Hp: happens(O(j))
IH: forall (tau0:timestamp),
tau0 < O(j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
_: A(i,j0) <= pred(O(j))
_: happens(A(i,j0))
----------------------------------------
happens(A(i,j0)) &&
A(i,j0) <= O(j) &&
forall (jj:index), happens(A(i,jj)) && A(i,jj) <= O(j) => A(i,jj) <= A(i,j0)

intro /= jj Hyp. [> Line 80: (intro /= jj Hyp)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0,jj:index
H2: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(O(j)) => A(i,jj) <= A(i,j0)
Hp: happens(O(j))
Hyp: happens(A(i,jj)) && A(i,jj) <= O(j)
IH: forall (tau0:timestamp),
tau0 < O(j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
_: A(i,j0) <= pred(O(j))
_: happens(A(i,j0))
----------------------------------------
A(i,jj) <= A(i,j0)

by apply H2. [> Line 81: by (apply ... )
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i:index,tau:timestamp
Hp: happens(tau)
IH: forall (tau0:timestamp),
tau0 < tau =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
----------------------------------------
(exists (i0,j:index), tau = A(i0,j)) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau &&
forall (jj:index), happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)

+ (* A(i0,j) *)
intro [i0 j Eq]; subst tau, A(i0,j). [> Line 84: ((intro [i0 j Eq]);(subst tau, A(i0,j)))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j:index
Hp: happens(A(i0,j))
IH: forall (tau0:timestamp),
tau0 < A(i0,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
----------------------------------------
(forall (j0:index), happens(A(i,j0)) => A(i,j0) > A(i0,j)) ||
exists (j0:index),
happens(A(i,j0)) &&
A(i,j0) <= A(i0,j) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i0,j) => A(i,jj) <= A(i,j0)

case (i<>i0) => //. [> Line 85: ((case (i <> i0));(intro //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,i0,j:index
Hp: happens(A(i0,j))
IH: forall (tau0:timestamp),
tau0 < A(i0,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
----------------------------------------
i <> i0 =>
(forall (j0:index), happens(A(i,j0)) => A(i,j0) > A(i0,j)) ||
exists (j0:index),
happens(A(i,j0)) &&
A(i,j0) <= A(i0,j) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i0,j) => A(i,jj) <= A(i,j0)

- (* 1st case: i<>i0 *)
intro Neq. [> Line 87: (intro Neq)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,i0,j:index
Hp: happens(A(i0,j))
IH: forall (tau0:timestamp),
tau0 < A(i0,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
Neq: i <> i0
----------------------------------------
(forall (j0:index), happens(A(i,j0)) => A(i,j0) > A(i0,j)) ||
exists (j0:index),
happens(A(i,j0)) &&
A(i,j0) <= A(i0,j) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i0,j) => A(i,jj) <= A(i,j0)

use IH with pred(A(i0,j)) => //. [> Line 88: ((have ... as );(intro //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,i0,j:index
H: (forall (j0:index), happens(A(i,j0)) => A(i,j0) > pred(A(i0,j))) ||
exists (j0:index),
happens(A(i,j0)) &&
A(i,j0) <= pred(A(i0,j)) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(A(i0,j)) => A(i,jj) <= A(i,j0)
Hp: happens(A(i0,j))
IH: forall (tau0:timestamp),
tau0 < A(i0,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
Neq: i <> i0
----------------------------------------
(forall (j0:index), happens(A(i,j0)) => A(i,j0) > A(i0,j)) ||
exists (j0:index),
happens(A(i,j0)) &&
A(i,j0) <= A(i0,j) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i0,j) => A(i,jj) <= A(i,j0)

destruct H as [H1 | [j0 H2]]. [> Line 89: (destruct H, [H1|[j0 H2]])
[goal> Focused goal (1/3):
System: left:default/left, right:default/right
Variables: i,i0,j:index
H1: forall (j0:index), happens(A(i,j0)) => A(i,j0) > pred(A(i0,j))
Hp: happens(A(i0,j))
IH: forall (tau0:timestamp),
tau0 < A(i0,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
Neq: i <> i0
----------------------------------------
(forall (j0:index), happens(A(i,j0)) => A(i,j0) > A(i0,j)) ||
exists (j0:index),
happens(A(i,j0)) &&
A(i,j0) <= A(i0,j) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i0,j) => A(i,jj) <= A(i,j0)

* left; intro j0 HpA; by use H1 with j0. [> Line 90: (left;((intro j0 HpA);by (have ... as )))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,i0,j,j0:index
H2: happens(A(i,j0)) &&
A(i,j0) <= pred(A(i0,j)) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(A(i0,j)) => A(i,jj) <= A(i,j0)
Hp: happens(A(i0,j))
IH: forall (tau0:timestamp),
tau0 < A(i0,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
Neq: i <> i0
----------------------------------------
(forall (j0:index), happens(A(i,j0)) => A(i,j0) > A(i0,j)) ||
exists (j0:index),
happens(A(i,j0)) &&
A(i,j0) <= A(i0,j) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i0,j) => A(i,jj) <= A(i,j0)

* right; destruct H2 as [_ _ H2]; exists j0. [> Line 91: (right;((destruct H2, [_ _ H2]);(exists j0)))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,i0,j,j0:index
H2: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(A(i0,j)) => A(i,jj) <= A(i,j0)
Hp: happens(A(i0,j))
IH: forall (tau0:timestamp),
tau0 < A(i0,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
Neq: i <> i0
_: A(i,j0) <= pred(A(i0,j))
_: happens(A(i,j0))
----------------------------------------
happens(A(i,j0)) &&
A(i,j0) <= A(i0,j) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i0,j) => A(i,jj) <= A(i,j0)

intro /= jj Hyp. [> Line 92: (intro /= jj Hyp)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,i0,j,j0,jj:index
H2: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(A(i0,j)) => A(i,jj) <= A(i,j0)
Hp: happens(A(i0,j))
Hyp: happens(A(i,jj)) && A(i,jj) <= A(i0,j)
IH: forall (tau0:timestamp),
tau0 < A(i0,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
Neq: i <> i0
_: A(i,j0) <= pred(A(i0,j))
_: happens(A(i,j0))
----------------------------------------
A(i,jj) <= A(i,j0)

by apply H2. [> Line 93: by (apply ... )
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j:index
Hp: happens(A(i0,j))
IH: forall (tau0:timestamp),
tau0 < A(i0,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
----------------------------------------
not(i <> i0) =>
(forall (j0:index), happens(A(i,j0)) => A(i,j0) > A(i0,j)) ||
exists (j0:index),
happens(A(i,j0)) &&
A(i,j0) <= A(i0,j) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i0,j) => A(i,jj) <= A(i,j0)

- (* 2nd case: i<>i0 *)
intro Eq; subst i0, i. [> Line 96: ((intro Eq);(subst i0, i))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j:index
Eq: not(i <> i)
Hp: happens(A(i,j))
IH: forall (tau0:timestamp),
tau0 < A(i,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) ||
exists (j:index),
happens(A(i,j)) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j)
----------------------------------------
(forall (j0:index), happens(A(i,j0)) => A(i,j0) > A(i,j)) ||
exists (j0:index),
happens(A(i,j0)) &&
A(i,j0) <= A(i,j) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i,j) => A(i,jj) <= A(i,j0)

by right; exists j. [> Line 97: by (right;(exists j))
[goal> Goal lastupdate_pure is proved

Qed. Exiting proof mode.

goal lastupdate_init : forall (i:index,tau:timestamp), happens(tau) => (
(forall j:index, happens(A(i,j)) => A(i,j)>tau))
=> s(i)@tau = s(i)@init. Goal lastupdate_init :
forall (i:index,tau:timestamp),
happens(tau) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau) =>
s(i)@tau = s(i)@init

Proof. [goal> Focused goal (1/1):
System: left:default/left, right:default/right
----------------------------------------
forall (i:index,tau:timestamp),
happens(tau) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau) => s(i)@tau = s(i)@init

intro i. [> Line 105: (intro i)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i:index
----------------------------------------
forall (tau:timestamp),
happens(tau) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau) => s(i)@tau = s(i)@init

induction => tau IH Htau. [> Line 106: (induction;(intro tau IH Htau))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i:index,tau:timestamp
Htau: happens(tau)
IH: forall (tau0:timestamp),
tau0 < tau =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) =>
s(i)@tau0 = s(i)@init
----------------------------------------
(forall (j:index), happens(A(i,j)) => A(i,j) > tau) => s(i)@tau = s(i)@init

case tau. [> Line 107: (case tau)
[goal> Focused goal (1/3):
System: left:default/left, right:default/right
Variables: i:index,tau:timestamp
Htau: happens(tau)
IH: forall (tau0:timestamp),
tau0 < tau =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) =>
s(i)@tau0 = s(i)@init
----------------------------------------
tau = init =>
(forall (j:index), happens(A(i,j)) => A(i,j) > init) => s(i)@init = s(i)@init

+ (* init *)
by auto. [> Line 110: by auto
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i:index,tau:timestamp
Htau: happens(tau)
IH: forall (tau0:timestamp),
tau0 < tau =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) =>
s(i)@tau0 = s(i)@init
----------------------------------------
(exists (j:index), tau = O(j)) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau) => s(i)@tau = s(i)@init

+ (* O(j) *)
intro [j Hj]; rewrite Hj in *. [> Line 113: ((intro [j Hj]);(rewrite ... in *))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j:index,tau:timestamp
Hj: tau = O(j)
Htau: happens(O(j))
IH: forall (tau0:timestamp),
tau0 < O(j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) =>
s(i)@tau0 = s(i)@init
----------------------------------------
(forall (j0:index), happens(A(i,j0)) => A(i,j0) > O(j)) =>
s(i)@O(j) = s(i)@init

expand s(i)@O(j). [> Line 114: (expand s(i)@O(j))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j:index,tau:timestamp
Hj: tau = O(j)
Htau: happens(O(j))
IH: forall (tau0:timestamp),
tau0 < O(j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) =>
s(i)@tau0 = s(i)@init
----------------------------------------
(forall (j0:index), happens(A(i,j0)) => A(i,j0) > O(j)) =>
s(i)@pred(O(j)) = s(i)@init

intro Hyp. [> Line 115: (intro Hyp)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j:index,tau:timestamp
Hj: tau = O(j)
Htau: happens(O(j))
Hyp: forall (j0:index), happens(A(i,j0)) => A(i,j0) > O(j)
IH: forall (tau0:timestamp),
tau0 < O(j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) =>
s(i)@tau0 = s(i)@init
----------------------------------------
s(i)@pred(O(j)) = s(i)@init

use IH with pred(O(j)) => //. [> Line 116: ((have ... as );(intro //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j:index,tau:timestamp
Hj: tau = O(j)
Htau: happens(O(j))
Hyp: forall (j0:index), happens(A(i,j0)) => A(i,j0) > O(j)
IH: forall (tau0:timestamp),
tau0 < O(j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) =>
s(i)@tau0 = s(i)@init
----------------------------------------
forall (j0:index), happens(A(i,j0)) => A(i,j0) > pred(O(j))

intro j0 HpA. [> Line 117: (intro j0 HpA)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0:index,tau:timestamp
Hj: tau = O(j)
HpA: happens(A(i,j0))
Htau: happens(O(j))
Hyp: forall (j0:index), happens(A(i,j0)) => A(i,j0) > O(j)
IH: forall (tau0:timestamp),
tau0 < O(j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) =>
s(i)@tau0 = s(i)@init
----------------------------------------
A(i,j0) > pred(O(j))

by use Hyp with j0. [> Line 118: by (have ... as )
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i:index,tau:timestamp
Htau: happens(tau)
IH: forall (tau0:timestamp),
tau0 < tau =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) =>
s(i)@tau0 = s(i)@init
----------------------------------------
(exists (i0,j:index), tau = A(i0,j)) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau) => s(i)@tau = s(i)@init

+ (* A(i0,j) *)
intro [i0 j HA]; rewrite HA in *. [> Line 121: ((intro [i0 j HA]);(rewrite ... in *))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j:index,tau:timestamp
HA: tau = A(i0,j)
Htau: happens(A(i0,j))
IH: forall (tau0:timestamp),
tau0 < A(i0,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) =>
s(i)@tau0 = s(i)@init
----------------------------------------
(forall (j0:index), happens(A(i,j0)) => A(i,j0) > A(i0,j)) =>
s(i)@A(i0,j) = s(i)@init

case (i = i0) => //. [> Line 122: ((case (i = i0));(intro //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,i0,j:index,tau:timestamp
HA: tau = A(i0,j)
Htau: happens(A(i0,j))
IH: forall (tau0:timestamp),
tau0 < A(i0,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) =>
s(i)@tau0 = s(i)@init
----------------------------------------
i = i0 =>
(forall (j0:index), happens(A(i,j0)) => A(i,j0) > A(i0,j)) =>
s(i)@A(i0,j) = s(i)@init

- intro Eq H0. [> Line 123: (intro Eq H0)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j:index,tau:timestamp
H0: forall (j0:index), happens(A(i,j0)) => A(i,j0) > A(i,j)
HA: tau = A(i,j)
Htau: happens(A(i,j))
IH: forall (tau0:timestamp),
tau0 < A(i,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) =>
s(i)@tau0 = s(i)@init
----------------------------------------
s(i)@A(i,j) = s(i)@init

use H0 with j => //. [> Line 124: ((have ... as );(intro //))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j:index,tau:timestamp
HA: tau = A(i0,j)
Htau: happens(A(i0,j))
IH: forall (tau0:timestamp),
tau0 < A(i0,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) =>
s(i)@tau0 = s(i)@init
----------------------------------------
not(i = i0) =>
(forall (j0:index), happens(A(i,j0)) => A(i,j0) > A(i0,j)) =>
s(i)@A(i0,j) = s(i)@init

- intro Neq H0. [> Line 126: (intro Neq H0)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j:index,tau:timestamp
H0: forall (j0:index), happens(A(i,j0)) => A(i,j0) > A(i0,j)
HA: tau = A(i0,j)
Htau: happens(A(i0,j))
IH: forall (tau0:timestamp),
tau0 < A(i0,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) =>
s(i)@tau0 = s(i)@init
Neq: not(i = i0)
----------------------------------------
s(i)@A(i0,j) = s(i)@init

use IH with pred(A(i0,j)) => //. [> Line 127: ((have ... as );(intro //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,i0,j:index,tau:timestamp
H0: forall (j0:index), happens(A(i,j0)) => A(i,j0) > A(i0,j)
HA: tau = A(i0,j)
Htau: happens(A(i0,j))
IH: forall (tau0:timestamp),
tau0 < A(i0,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) =>
s(i)@tau0 = s(i)@init
Meq: s(i)@pred(A(i0,j)) = s(i)@init
Neq: not(i = i0)
----------------------------------------
s(i)@A(i0,j) = s(i)@init

* expand s(i)@A(i0,j). [> Line 128: (expand s(i)@A(i0,j))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,i0,j:index,tau:timestamp
H0: forall (j0:index), happens(A(i,j0)) => A(i,j0) > A(i0,j)
HA: tau = A(i0,j)
Htau: happens(A(i0,j))
IH: forall (tau0:timestamp),
tau0 < A(i0,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) =>
s(i)@tau0 = s(i)@init
Meq: s(i)@pred(A(i0,j)) = s(i)@init
Neq: not(i = i0)
----------------------------------------
if (i = i0) then H(s(i0)@pred(A(i0,j)),k) else s(i)@pred(A(i0,j)) = s(i)@init

rewrite if_false => //. [> Line 129: ((rewrite ...);(intro //))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j:index,tau:timestamp
H0: forall (j0:index), happens(A(i,j0)) => A(i,j0) > A(i0,j)
HA: tau = A(i0,j)
Htau: happens(A(i0,j))
IH: forall (tau0:timestamp),
tau0 < A(i0,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) =>
s(i)@tau0 = s(i)@init
Neq: not(i = i0)
----------------------------------------
forall (j0:index), happens(A(i,j0)) => A(i,j0) > pred(A(i0,j))

* intro j0 Hp. [> Line 130: (intro j0 Hp)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j,j0:index,tau:timestamp
H0: forall (j0:index), happens(A(i,j0)) => A(i,j0) > A(i0,j)
HA: tau = A(i0,j)
Hp: happens(A(i,j0))
Htau: happens(A(i0,j))
IH: forall (tau0:timestamp),
tau0 < A(i0,j) =>
happens(tau0) =>
(forall (j:index), happens(A(i,j)) => A(i,j) > tau0) =>
s(i)@tau0 = s(i)@init
Neq: not(i = i0)
----------------------------------------
A(i,j0) > pred(A(i0,j))

use H0 with j0 => //. [> Line 131: ((have ... as );(intro //))
[goal> Goal lastupdate_init is proved

Qed. Exiting proof mode.

goal lastupdate_A: forall (i:index, j:index, tau:timestamp),
(happens(tau) &&
A(i,j)<=tau &&
forall jj:index, happens(A(i,jj)) && A(i,jj)<=tau => A(i,jj)<=A(i,j))
=> s(i)@tau = s(i)@A(i,j). Goal lastupdate_A :
forall (i,j:index,tau:timestamp),
happens(tau) &&
A(i,j) <= tau &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j) =>
s(i)@tau = s(i)@A(i,j)

Proof. [goal> Focused goal (1/1):
System: left:default/left, right:default/right
----------------------------------------
forall (i,j:index,tau:timestamp),
happens(tau) &&
A(i,j) <= tau &&
forall (jj:index), happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j) =>
s(i)@tau = s(i)@A(i,j)

intro i j. [> Line 141: (intro i j)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j:index
----------------------------------------
forall (tau:timestamp),
happens(tau) &&
A(i,j) <= tau &&
forall (jj:index), happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j) =>
s(i)@tau = s(i)@A(i,j)

induction => tau IH [Hp Ord Hyp]. [> Line 142: (induction;(intro tau IH [Hp Ord Hyp]))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j:index,tau:timestamp
Hp: happens(tau)
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < tau =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Ord: A(i,j) <= tau
----------------------------------------
s(i)@tau = s(i)@A(i,j)

case tau. [> Line 143: (case tau)
[goal> Focused goal (1/3):
System: left:default/left, right:default/right
Variables: i,j:index,tau:timestamp
Hp: happens(tau)
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < tau =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Ord: A(i,j) <= tau
----------------------------------------
tau = init => s(i)@init = s(i)@A(i,j)

+ (* init *)
by auto. [> Line 146: by auto
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j:index,tau:timestamp
Hp: happens(tau)
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < tau =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Ord: A(i,j) <= tau
----------------------------------------
(exists (j0:index), tau = O(j0)) => s(i)@tau = s(i)@A(i,j)

+ (* O(j0 *)
intro [j0 Hj]; rewrite Hj in *. [> Line 149: ((intro [j0 Hj]);(rewrite ... in *))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0:index,tau:timestamp
Hj: tau = O(j0)
Hp: happens(O(j0))
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= O(j0) => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < O(j0) =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Ord: A(i,j) <= O(j0)
----------------------------------------
s(i)@O(j0) = s(i)@A(i,j)

expand s(i)@O(j0). [> Line 150: (expand s(i)@O(j0))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0:index,tau:timestamp
Hj: tau = O(j0)
Hp: happens(O(j0))
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= O(j0) => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < O(j0) =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Ord: A(i,j) <= O(j0)
----------------------------------------
s(i)@pred(O(j0)) = s(i)@A(i,j)

use IH with pred(O(j0)) => //. [> Line 151: ((have ... as );(intro //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0:index,tau:timestamp
Hj: tau = O(j0)
Hp: happens(O(j0))
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= O(j0) => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < O(j0) =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Ord: A(i,j) <= O(j0)
----------------------------------------
happens(pred(O(j0))) &&
A(i,j) <= pred(O(j0)) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(O(j0)) => A(i,jj) <= A(i,j)

repeat split => //. [> Line 152: ((repeat split);(intro //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0:index,tau:timestamp
Hj: tau = O(j0)
Hp: happens(O(j0))
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= O(j0) => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < O(j0) =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Ord: A(i,j) <= O(j0)
----------------------------------------
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(O(j0)) => A(i,jj) <= A(i,j)

intro jj H. [> Line 153: (intro jj H)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0,jj:index,tau:timestamp
H: happens(A(i,jj)) && A(i,jj) <= pred(O(j0))
Hj: tau = O(j0)
Hp: happens(O(j0))
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= O(j0) => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < O(j0) =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Ord: A(i,j) <= O(j0)
----------------------------------------
A(i,jj) <= A(i,j)

use Hyp with jj => //. [> Line 154: ((have ... as );(intro //))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j:index,tau:timestamp
Hp: happens(tau)
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < tau =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Ord: A(i,j) <= tau
----------------------------------------
(exists (i0,j0:index), tau = A(i0,j0)) => s(i)@tau = s(i)@A(i,j)

+ (* A(i0,j0) *)
intro [i0 j0 H]; rewrite H in *. [> Line 157: ((intro [i0 j0 H]);(rewrite ... in *))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j,j0:index,tau:timestamp
H: tau = A(i0,j0)
Hp: happens(A(i0,j0))
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i0,j0) => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < A(i0,j0) =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Ord: A(i,j) <= A(i0,j0)
----------------------------------------
s(i)@A(i0,j0) = s(i)@A(i,j)

case (i=i0) => //. [> Line 158: ((case (i = i0));(intro //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,i0,j,j0:index,tau:timestamp
H: tau = A(i0,j0)
Hp: happens(A(i0,j0))
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i0,j0) => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < A(i0,j0) =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Ord: A(i,j) <= A(i0,j0)
----------------------------------------
i = i0 => s(i)@A(i0,j0) = s(i)@A(i,j)

- intro Eqi. [> Line 159: (intro Eqi)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0:index,tau:timestamp
H: tau = A(i,j0)
Hp: happens(A(i,j0))
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i,j0) => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < A(i,j0) =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Ord: A(i,j) <= A(i,j0)
----------------------------------------
s(i)@A(i,j0) = s(i)@A(i,j)

use Hyp with j0. [> Line 160: (have ... as )
[goal> Focused goal (1/3):
System: left:default/left, right:default/right
Variables: i,j,j0:index,tau:timestamp
Cle: A(i,j0) <= A(i,j)
H: tau = A(i,j0)
Hp: happens(A(i,j0))
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i,j0) => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < A(i,j0) =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Ord: A(i,j) <= A(i,j0)
----------------------------------------
s(i)@A(i,j0) = s(i)@A(i,j)

* case (j=j0) => //. [> Line 161: ((case (j = j0));(intro //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0:index,tau:timestamp
H: tau = A(i,j0)
Hp: happens(A(i,j0))
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i,j0) => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < A(i,j0) =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Ord: A(i,j) <= A(i,j0)
----------------------------------------
happens(A(i,j0)) && A(i,j0) <= A(i,j0)

* auto. [> Line 162: auto
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j,j0:index,tau:timestamp
H: tau = A(i0,j0)
Hp: happens(A(i0,j0))
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i0,j0) => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < A(i0,j0) =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Ord: A(i,j) <= A(i0,j0)
----------------------------------------
not(i = i0) => s(i)@A(i0,j0) = s(i)@A(i,j)

- intro Neqi. [> Line 163: (intro Neqi)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j,j0:index,tau:timestamp
H: tau = A(i0,j0)
Hp: happens(A(i0,j0))
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i0,j0) => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < A(i0,j0) =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Neqi: not(i = i0)
Ord: A(i,j) <= A(i0,j0)
----------------------------------------
s(i)@A(i0,j0) = s(i)@A(i,j)

expand s(i)@A(i0,j0). [> Line 164: (expand s(i)@A(i0,j0))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j,j0:index,tau:timestamp
H: tau = A(i0,j0)
Hp: happens(A(i0,j0))
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i0,j0) => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < A(i0,j0) =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Neqi: not(i = i0)
Ord: A(i,j) <= A(i0,j0)
----------------------------------------
if (i = i0) then H(s(i0)@pred(A(i0,j0)),k) else s(i)@pred(A(i0,j0)) =
s(i)@A(i,j)

rewrite if_false. [> Line 165: (rewrite ...)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,i0,j,j0:index,tau:timestamp
H: tau = A(i0,j0)
Hp: happens(A(i0,j0))
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i0,j0) => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < A(i0,j0) =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Neqi: not(i = i0)
Ord: A(i,j) <= A(i0,j0)
----------------------------------------
not(i = i0)

* auto. [> Line 166: auto
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j,j0:index,tau:timestamp
H: tau = A(i0,j0)
Hp: happens(A(i0,j0))
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i0,j0) => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < A(i0,j0) =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Neqi: not(i = i0)
Ord: A(i,j) <= A(i0,j0)
----------------------------------------
s(i)@pred(A(i0,j0)) = s(i)@A(i,j)

* use IH with pred(A(i0,j0)) => //. [> Line 167: ((have ... as );(intro //))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j,j0:index,tau:timestamp
H: tau = A(i0,j0)
Hp: happens(A(i0,j0))
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i0,j0) => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < A(i0,j0) =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Neqi: not(i = i0)
Ord: A(i,j) <= A(i0,j0)
----------------------------------------
happens(pred(A(i0,j0))) &&
A(i,j) <= pred(A(i0,j0)) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(A(i0,j0)) => A(i,jj) <= A(i,j)

repeat split => //. [> Line 168: ((repeat split);(intro //))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j,j0:index,tau:timestamp
H: tau = A(i0,j0)
Hp: happens(A(i0,j0))
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i0,j0) => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < A(i0,j0) =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Neqi: not(i = i0)
Ord: A(i,j) <= A(i0,j0)
----------------------------------------
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(A(i0,j0)) => A(i,jj) <= A(i,j)

intro jj H0. [> Line 169: (intro jj H0)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j,j0,jj:index,tau:timestamp
H: tau = A(i0,j0)
H0: happens(A(i,jj)) && A(i,jj) <= pred(A(i0,j0))
Hp: happens(A(i0,j0))
Hyp: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= A(i0,j0) => A(i,jj) <= A(i,j)
IH: forall (tau0:timestamp),
tau0 < A(i0,j0) =>
happens(tau0) &&
A(i,j) <= tau0 &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau0 => A(i,jj) <= A(i,j) =>
s(i)@tau0 = s(i)@A(i,j)
Neqi: not(i = i0)
Ord: A(i,j) <= A(i0,j0)
----------------------------------------
A(i,jj) <= A(i,j)

use Hyp with jj => //. [> Line 170: ((have ... as );(intro //))
[goal> Goal lastupdate_A is proved

Qed. Exiting proof mode.

goal lastupdate : forall (i:index,tau:timestamp), happens(tau) => (
(s(i)@tau = s(i)@init && forall j:index, happens(A(i,j)) => A(i,j)>tau) ||
(exists j:index,
s(i)@tau = s(i)@A(i,j) && A(i,j)<=tau
&& forall jj:index, happens(A(i,jj)) && A(i,jj)<=tau => A(i,jj)<=A(i,j))). Goal lastupdate :
forall (i:index,tau:timestamp),
happens(tau) =>
s(i)@tau = s(i)@init && forall (j:index), happens(A(i,j)) => A(i,j) > tau ||
exists (j:index),
s(i)@tau = s(i)@A(i,j) &&
A(i,j) <= tau &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)

Proof. [goal> Focused goal (1/1):
System: left:default/left, right:default/right
----------------------------------------
forall (i:index,tau:timestamp),
happens(tau) =>
s(i)@tau = s(i)@init && forall (j:index), happens(A(i,j)) => A(i,j) > tau ||
exists (j:index),
s(i)@tau = s(i)@A(i,j) &&
A(i,j) <= tau &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)

intro i tau Htau. [> Line 180: (intro i tau Htau)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i:index,tau:timestamp
Htau: happens(tau)
----------------------------------------
s(i)@tau = s(i)@init && forall (j:index), happens(A(i,j)) => A(i,j) > tau ||
exists (j:index),
s(i)@tau = s(i)@A(i,j) &&
A(i,j) <= tau &&
forall (jj:index), happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)

use lastupdate_pure with i, tau as [Hinit | [j [HAj1 HAj2 HAj3]]] => //. [> Line 181: ((have ... as [Hinit|[j [HAj1 HAj2 HAj3]]]);(intro //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i:index,tau:timestamp
Hinit: forall (j:index), happens(A(i,j)) => A(i,j) > tau
Htau: happens(tau)
----------------------------------------
s(i)@tau = s(i)@init && forall (j:index), happens(A(i,j)) => A(i,j) > tau ||
exists (j:index),
s(i)@tau = s(i)@A(i,j) &&
A(i,j) <= tau &&
forall (jj:index), happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)

+ left. [> Line 182: left
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i:index,tau:timestamp
Hinit: forall (j:index), happens(A(i,j)) => A(i,j) > tau
Htau: happens(tau)
----------------------------------------
s(i)@tau = s(i)@init && forall (j:index), happens(A(i,j)) => A(i,j) > tau

split => //. [> Line 183: (split;(intro //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i:index,tau:timestamp
Hinit: forall (j:index), happens(A(i,j)) => A(i,j) > tau
Htau: happens(tau)
----------------------------------------
s(i)@tau = s(i)@init

by apply lastupdate_init. [> Line 184: by (apply ... )
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j:index,tau:timestamp
HAj1: happens(A(i,j))
HAj2: A(i,j) <= tau
HAj3: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)
Htau: happens(tau)
----------------------------------------
s(i)@tau = s(i)@init && forall (j:index), happens(A(i,j)) => A(i,j) > tau ||
exists (j:index),
s(i)@tau = s(i)@A(i,j) &&
A(i,j) <= tau &&
forall (jj:index), happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)

+ right. [> Line 185: right
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j:index,tau:timestamp
HAj1: happens(A(i,j))
HAj2: A(i,j) <= tau
HAj3: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)
Htau: happens(tau)
----------------------------------------
exists (j:index),
s(i)@tau = s(i)@A(i,j) &&
A(i,j) <= tau &&
forall (jj:index), happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)

exists j. [> Line 186: (exists j)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j:index,tau:timestamp
HAj1: happens(A(i,j))
HAj2: A(i,j) <= tau
HAj3: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)
Htau: happens(tau)
----------------------------------------
s(i)@tau = s(i)@A(i,j) &&
A(i,j) <= tau &&
forall (jj:index), happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)

repeat split => //. [> Line 187: ((repeat split);(intro //))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j:index,tau:timestamp
HAj1: happens(A(i,j))
HAj2: A(i,j) <= tau
HAj3: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)
Htau: happens(tau)
----------------------------------------
s(i)@tau = s(i)@A(i,j)

use lastupdate_A with i, j, tau => //. [> Line 188: ((have ... as );(intro //))
[goal> Goal lastupdate is proved

Qed. Exiting proof mode.

goal disjoint_chains :
forall (tau',tau:timestamp,i',i:index) happens(tau',tau) =>
i<>i' =>
s(i)@tau <> s(i')@tau'. Goal disjoint_chains :
forall (tau',tau:timestamp,i',i:index),
happens(tau, tau') => i <> i' => s(i)@tau <> s(i')@tau'

The contents of distinct memory cells never coincide.

Proof. [goal> Focused goal (1/1):
System: left:default/left, right:default/right
----------------------------------------
forall (tau',tau:timestamp,i',i:index),
happens(tau, tau') => i <> i' => s(i)@tau <> s(i')@tau'

induction => tau' IH tau i' i D E Meq. [> Line 198: (induction;(intro tau' IH tau i' i D E Meq))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i':index,tau,tau':timestamp
D: happens(tau, tau')
E: i <> i'
IH: forall (tau'0,tau:timestamp,i',i:index),
tau'0 < tau' =>
happens(tau, tau'0) => i <> i' => s(i)@tau <> s(i')@tau'0
Meq: s(i)@tau = s(i')@tau'
----------------------------------------
false

use lastupdate with i,tau as [[A0 Hinit] | [j [A0 A1 Hsup]]] => //;
use lastupdate with i',tau' as [[A Hinit'] | [j' [B C Hsup']]] => //. [> Line 200: ((((have ... as [[A0 Hinit]|[j [A0 A1 Hsup]]]);(intro //));
(have ... as [[A Hinit']|[j' [B C Hsup']]]));
(intro //))

[goal> Focused goal (1/3):
System: left:default/left, right:default/right
Variables: i,i',j':index,tau,tau':timestamp
A0: s(i)@tau = s(i)@init
B: s(i')@tau' = s(i')@A(i',j')
C: A(i',j') <= tau'
D: happens(tau, tau')
E: i <> i'
Hinit: forall (j:index), happens(A(i,j)) => A(i,j) > tau
Hsup': forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= tau' => A(i',jj) <= A(i',j')
IH: forall (tau'0,tau:timestamp,i',i:index),
tau'0 < tau' =>
happens(tau, tau'0) => i <> i' => s(i)@tau <> s(i')@tau'0
Meq: s(i)@tau = s(i')@tau'
----------------------------------------
false

+ rewrite -Meq A0 /s in B. [> Line 202: (rewrite ... ... ... in B)
[goal> Focused goal (1/3):
System: left:default/left, right:default/right
Variables: i,i',j':index,tau,tau':timestamp
A0: s(i)@tau = s(i)@init
B: s0(i) = H(s(i')@pred(A(i',j')),k)
C: A(i',j') <= tau'
D: happens(tau, tau')
E: i <> i'
Hinit: forall (j:index), happens(A(i,j)) => A(i,j) > tau
Hsup': forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= tau' => A(i',jj) <= A(i',j')
IH: forall (tau'0,tau:timestamp,i',i:index),
tau'0 < tau' =>
happens(tau, tau'0) => i <> i' => s(i)@tau <> s(i')@tau'0
Meq: s(i)@tau = s(i')@tau'
----------------------------------------
false

by fresh B. [> Line 203: by (fresh B)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,i',j:index,tau,tau':timestamp
A: s(i')@tau' = s(i')@init
A0: s(i)@tau = s(i)@A(i,j)
A1: A(i,j) <= tau
D: happens(tau, tau')
E: i <> i'
Hinit': forall (j:index), happens(A(i',j)) => A(i',j) > tau'
Hsup: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)
IH: forall (tau'0,tau:timestamp,i',i:index),
tau'0 < tau' =>
happens(tau, tau'0) => i <> i' => s(i)@tau <> s(i')@tau'0
Meq: s(i)@tau = s(i')@tau'
----------------------------------------
false

+ rewrite Meq A /s in A0. [> Line 205: (rewrite ... ... ... in A0)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,i',j:index,tau,tau':timestamp
A: s(i')@tau' = s(i')@init
A0: s0(i') = H(s(i)@pred(A(i,j)),k)
A1: A(i,j) <= tau
D: happens(tau, tau')
E: i <> i'
Hinit': forall (j:index), happens(A(i',j)) => A(i',j) > tau'
Hsup: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)
IH: forall (tau'0,tau:timestamp,i',i:index),
tau'0 < tau' =>
happens(tau, tau'0) => i <> i' => s(i)@tau <> s(i')@tau'0
Meq: s(i)@tau = s(i')@tau'
----------------------------------------
false

by fresh A0. [> Line 206: by (fresh A0)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i',j,j':index,tau,tau':timestamp
A0: s(i)@tau = s(i)@A(i,j)
A1: A(i,j) <= tau
B: s(i')@tau' = s(i')@A(i',j')
C: A(i',j') <= tau'
D: happens(tau, tau')
E: i <> i'
Hsup: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)
Hsup': forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= tau' => A(i',jj) <= A(i',j')
IH: forall (tau'0,tau:timestamp,i',i:index),
tau'0 < tau' =>
happens(tau, tau'0) => i <> i' => s(i)@tau <> s(i')@tau'0
Meq: s(i)@tau = s(i')@tau'
----------------------------------------
false

+ rewrite Meq B /s in A0. [> Line 208: (rewrite ... ... ... in A0)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i',j,j':index,tau,tau':timestamp
A0: H(s(i')@pred(A(i',j')),k) = H(s(i)@pred(A(i,j)),k)
A1: A(i,j) <= tau
B: s(i')@tau' = s(i')@A(i',j')
C: A(i',j') <= tau'
D: happens(tau, tau')
E: i <> i'
Hsup: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)
Hsup': forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= tau' => A(i',jj) <= A(i',j')
IH: forall (tau'0,tau:timestamp,i',i:index),
tau'0 < tau' =>
happens(tau, tau'0) => i <> i' => s(i)@tau <> s(i')@tau'0
Meq: s(i)@tau = s(i')@tau'
----------------------------------------
false

collision A0 => H. [> Line 209: ((collision A0);(intro H))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i',j,j':index,tau,tau':timestamp
A0: H(s(i')@pred(A(i',j')),k) = H(s(i)@pred(A(i,j)),k)
A1: A(i,j) <= tau
B: s(i')@tau' = s(i')@A(i',j')
C: A(i',j') <= tau'
D: happens(tau, tau')
E: i <> i'
H: s(i')@pred(A(i',j')) = s(i)@pred(A(i,j))
Hsup: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= tau => A(i,jj) <= A(i,j)
Hsup': forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= tau' => A(i',jj) <= A(i',j')
IH: forall (tau'0,tau:timestamp,i',i:index),
tau'0 < tau' =>
happens(tau, tau'0) => i <> i' => s(i)@tau <> s(i')@tau'0
Meq: s(i)@tau = s(i')@tau'
----------------------------------------
false

use IH with pred(A(i',j')),pred(A(i,j)),i',i => //. [> Line 210: ((have ... as );(intro //))
[goal> Goal disjoint_chains is proved

Qed. Exiting proof mode.

goal monotonic_chain :
forall (tau,tau':timestamp,i,j:index) happens(tau,A(i,j)) => (
(s(i)@tau = s(i)@A(i,j) && tau' < A(i,j) && A(i,j) <= tau)
=> s(i)@tau' <> s(i)@tau). Goal monotonic_chain :
forall (tau,tau':timestamp,i,j:index),
happens(A(i,j), tau) =>
s(i)@tau = s(i)@A(i,j) && tau' < A(i,j) && A(i,j) <= tau =>
s(i)@tau' <> s(i)@tau

Values do not repeat inside the same chain of hashes.

Proof. [goal> Focused goal (1/1):
System: left:default/left, right:default/right
----------------------------------------
forall (tau,tau':timestamp,i,j:index),
happens(A(i,j), tau) =>
s(i)@tau = s(i)@A(i,j) && tau' < A(i,j) && A(i,j) <= tau =>
s(i)@tau' <> s(i)@tau

induction => tau IH tau' i j Hap [H1 H2 H3] Meq. [> Line 220: (induction;(intro tau IH tau' i j Hap [H1 H2 H3] Meq))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j:index,tau,tau':timestamp
H1: s(i)@tau = s(i)@A(i,j)
H2: tau' < A(i,j)
H3: A(i,j) <= tau
Hap: happens(A(i,j), tau)
IH: forall (tau0,tau':timestamp,i,j:index),
tau0 < tau =>
happens(A(i,j), tau0) =>
s(i)@tau0 = s(i)@A(i,j) && tau' < A(i,j) && A(i,j) <= tau0 =>
s(i)@tau' <> s(i)@tau0
Meq: s(i)@tau' = s(i)@tau
----------------------------------------
false

assert s(i)@tau' = s(i)@A(i,j) as Meq' by auto. [> Line 221: ((have (s(i)@tau' = s(i)@A(i,j)), Meq'); 1: by auto)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j:index,tau,tau':timestamp
H1: s(i)@tau = s(i)@A(i,j)
H2: tau' < A(i,j)
H3: A(i,j) <= tau
Hap: happens(A(i,j), tau)
IH: forall (tau0,tau':timestamp,i,j:index),
tau0 < tau =>
happens(A(i,j), tau0) =>
s(i)@tau0 = s(i)@A(i,j) && tau' < A(i,j) && A(i,j) <= tau0 =>
s(i)@tau' <> s(i)@tau0
Meq: s(i)@tau' = s(i)@tau
Meq': s(i)@tau' = s(i)@A(i,j)
----------------------------------------
false

expand s(i)@A(i,j). [> Line 222: (expand s(i)@A(i,j))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j:index,tau,tau':timestamp
H1: s(i)@tau = H(s(i)@pred(A(i,j)),k)
H2: tau' < A(i,j)
H3: A(i,j) <= tau
Hap: happens(A(i,j), tau)
IH: forall (tau0,tau':timestamp,i,j:index),
tau0 < tau =>
happens(A(i,j), tau0) =>
s(i)@tau0 = s(i)@A(i,j) && tau' < A(i,j) && A(i,j) <= tau0 =>
s(i)@tau' <> s(i)@tau0
Meq: s(i)@tau' = s(i)@tau
Meq': s(i)@tau' = H(s(i)@pred(A(i,j)),k)
----------------------------------------
false

euf Meq'. [> Line 223: (euf Meq')
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j,j0:index,tau,tau':timestamp
H1: s(i)@tau = H(s(i)@pred(A(i,j)),k)
H2: tau' < A(i,j)
H3: A(i,j) <= tau
Hap: happens(A(i,j), tau)
IH: forall (tau0,tau':timestamp,i,j:index),
tau0 < tau =>
happens(A(i,j), tau0) =>
s(i)@tau0 = s(i)@A(i,j) && tau' < A(i,j) && A(i,j) <= tau0 =>
s(i)@tau' <> s(i)@tau0
Meq: s(i)@tau' = s(i)@tau
Meq': s(i)@tau' = H(s(i)@pred(A(i,j)),k)
----------------------------------------
A(i0,j0) <= tau' || A(i0,j0) < A(i,j) =>
s(i0)@pred(A(i0,j0)) = s(i)@pred(A(i,j)) => false

intro Heuf Meuf *. [> Line 224: (intro Heuf Meuf *)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j,j0:index,tau,tau':timestamp
H1: s(i)@tau = H(s(i)@pred(A(i,j)),k)
H2: tau' < A(i,j)
H3: A(i,j) <= tau
Hap: happens(A(i,j), tau)
Heuf: A(i0,j0) <= tau' || A(i0,j0) < A(i,j)
IH: forall (tau0,tau':timestamp,i,j:index),
tau0 < tau =>
happens(A(i,j), tau0) =>
s(i)@tau0 = s(i)@A(i,j) && tau' < A(i,j) && A(i,j) <= tau0 =>
s(i)@tau' <> s(i)@tau0
Meq: s(i)@tau' = s(i)@tau
Meq': s(i)@tau' = H(s(i)@pred(A(i,j)),k)
Meuf: s(i0)@pred(A(i0,j0)) = s(i)@pred(A(i,j))
----------------------------------------
false

assert i=i0 || i<>i0 as [H0|H0] by auto. [> Line 225: ((have ((i = i0) || (i <> i0)), [H0|H0]); 1: by auto)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0:index,tau,tau':timestamp
H1: s(i)@tau = H(s(i)@pred(A(i,j)),k)
H2: tau' < A(i,j)
H3: A(i,j) <= tau
Hap: happens(A(i,j), tau)
Heuf: A(i,j0) <= tau' || A(i,j0) < A(i,j)
IH: forall (tau0,tau':timestamp,i,j:index),
tau0 < tau =>
happens(A(i,j), tau0) =>
s(i)@tau0 = s(i)@A(i,j) && tau' < A(i,j) && A(i,j) <= tau0 =>
s(i)@tau' <> s(i)@tau0
Meq: s(i)@tau' = s(i)@tau
Meq': s(i)@tau' = H(s(i)@pred(A(i,j)),k)
Meuf: s(i)@pred(A(i,j0)) = s(i)@pred(A(i,j))
----------------------------------------
false

+ (* i = i0 *)
use lastupdate with i,pred(A(i,j)) as H4; 2: by auto. [> Line 227: ((have ... as H4); 2: by auto)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0:index,tau,tau':timestamp
H1: s(i)@tau = H(s(i)@pred(A(i,j)),k)
H2: tau' < A(i,j)
H3: A(i,j) <= tau
H4: s(i)@pred(A(i,j)) = s(i)@init &&
forall (j0:index), happens(A(i,j0)) => A(i,j0) > pred(A(i,j)) ||
exists (j0:index),
s(i)@pred(A(i,j)) = s(i)@A(i,j0) &&
A(i,j0) <= pred(A(i,j)) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(A(i,j)) => A(i,jj) <= A(i,j0)
Hap: happens(A(i,j), tau)
Heuf: A(i,j0) <= tau' || A(i,j0) < A(i,j)
IH: forall (tau0,tau':timestamp,i,j:index),
tau0 < tau =>
happens(A(i,j), tau0) =>
s(i)@tau0 = s(i)@A(i,j) && tau' < A(i,j) && A(i,j) <= tau0 =>
s(i)@tau' <> s(i)@tau0
Meq: s(i)@tau' = s(i)@tau
Meq': s(i)@tau' = H(s(i)@pred(A(i,j)),k)
Meuf: s(i)@pred(A(i,j0)) = s(i)@pred(A(i,j))
----------------------------------------
false

case H4. [> Line 228: (case H4)
[goal> Focused goal (1/3):
System: left:default/left, right:default/right
Variables: i,j,j0:index,tau,tau':timestamp
H1: s(i)@tau = H(s(i)@pred(A(i,j)),k)
H2: tau' < A(i,j)
H3: A(i,j) <= tau
H4: s(i)@pred(A(i,j)) = s(i)@init &&
forall (j0:index), happens(A(i,j0)) => A(i,j0) > pred(A(i,j))
Hap: happens(A(i,j), tau)
Heuf: A(i,j0) <= tau' || A(i,j0) < A(i,j)
IH: forall (tau0,tau':timestamp,i,j:index),
tau0 < tau =>
happens(A(i,j), tau0) =>
s(i)@tau0 = s(i)@A(i,j) && tau' < A(i,j) && A(i,j) <= tau0 =>
s(i)@tau' <> s(i)@tau0
Meq: s(i)@tau' = s(i)@tau
Meq': s(i)@tau' = H(s(i)@pred(A(i,j)),k)
Meuf: s(i)@pred(A(i,j0)) = s(i)@pred(A(i,j))
----------------------------------------
false

- (* case H4 - init *)
destruct H4 as [H4 H4']. [> Line 230: (destruct H4, [H4 H4'])
[goal> Focused goal (1/3):
System: left:default/left, right:default/right
Variables: i,j,j0:index,tau,tau':timestamp
H1: s(i)@tau = H(s(i)@pred(A(i,j)),k)
H2: tau' < A(i,j)
H3: A(i,j) <= tau
H4: s(i)@pred(A(i,j)) = s(i)@init
H4': forall (j0:index), happens(A(i,j0)) => A(i,j0) > pred(A(i,j))
Hap: happens(A(i,j), tau)
Heuf: A(i,j0) <= tau' || A(i,j0) < A(i,j)
IH: forall (tau0,tau':timestamp,i,j:index),
tau0 < tau =>
happens(A(i,j), tau0) =>
s(i)@tau0 = s(i)@A(i,j) && tau' < A(i,j) && A(i,j) <= tau0 =>
s(i)@tau' <> s(i)@tau0
Meq: s(i)@tau' = s(i)@tau
Meq': s(i)@tau' = H(s(i)@pred(A(i,j)),k)
Meuf: s(i)@pred(A(i,j0)) = s(i)@pred(A(i,j))
----------------------------------------
false

use H4' with j0; 1,2: case Heuf; auto. [> Line 231: ((have ... as ); 1,2: ((case Heuf);auto))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0:index,tau,tau':timestamp
H1: s(i)@tau = H(s(i)@pred(A(i,j)),k)
H2: tau' < A(i,j)
H3: A(i,j) <= tau
H4: exists (j0:index),
s(i)@pred(A(i,j)) = s(i)@A(i,j0) &&
A(i,j0) <= pred(A(i,j)) &&
forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(A(i,j)) => A(i,jj) <= A(i,j0)
Hap: happens(A(i,j), tau)
Heuf: A(i,j0) <= tau' || A(i,j0) < A(i,j)
IH: forall (tau0,tau':timestamp,i,j:index),
tau0 < tau =>
happens(A(i,j), tau0) =>
s(i)@tau0 = s(i)@A(i,j) && tau' < A(i,j) && A(i,j) <= tau0 =>
s(i)@tau' <> s(i)@tau0
Meq: s(i)@tau' = s(i)@tau
Meq': s(i)@tau' = H(s(i)@pred(A(i,j)),k)
Meuf: s(i)@pred(A(i,j0)) = s(i)@pred(A(i,j))
----------------------------------------
false

- (* case H1 - general *)
destruct H4 as [j1 [Meq1 H4 H5]]. [> Line 233: (destruct H4, [j1 [Meq1 H4 H5]])
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0,j1:index,tau,tau':timestamp
H1: s(i)@tau = H(s(i)@pred(A(i,j)),k)
H2: tau' < A(i,j)
H3: A(i,j) <= tau
H4: A(i,j1) <= pred(A(i,j))
H5: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(A(i,j)) => A(i,jj) <= A(i,j1)
Hap: happens(A(i,j), tau)
Heuf: A(i,j0) <= tau' || A(i,j0) < A(i,j)
IH: forall (tau0,tau':timestamp,i,j:index),
tau0 < tau =>
happens(A(i,j), tau0) =>
s(i)@tau0 = s(i)@A(i,j) && tau' < A(i,j) && A(i,j) <= tau0 =>
s(i)@tau' <> s(i)@tau0
Meq: s(i)@tau' = s(i)@tau
Meq': s(i)@tau' = H(s(i)@pred(A(i,j)),k)
Meq1: s(i)@pred(A(i,j)) = s(i)@A(i,j1)
Meuf: s(i)@pred(A(i,j0)) = s(i)@pred(A(i,j))
----------------------------------------
false

use IH with pred(A(i,j)),pred(A(i,j0)),i,j1 as H; try auto. [> Line 234: ((have ... as H);(try auto))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0,j1:index,tau,tau':timestamp
H1: s(i)@tau = H(s(i)@pred(A(i,j)),k)
H2: tau' < A(i,j)
H3: A(i,j) <= tau
H4: A(i,j1) <= pred(A(i,j))
H5: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(A(i,j)) => A(i,jj) <= A(i,j1)
Hap: happens(A(i,j), tau)
Heuf: A(i,j0) <= tau' || A(i,j0) < A(i,j)
IH: forall (tau0,tau':timestamp,i,j:index),
tau0 < tau =>
happens(A(i,j), tau0) =>
s(i)@tau0 = s(i)@A(i,j) && tau' < A(i,j) && A(i,j) <= tau0 =>
s(i)@tau' <> s(i)@tau0
Meq: s(i)@tau' = s(i)@tau
Meq': s(i)@tau' = H(s(i)@pred(A(i,j)),k)
Meq1: s(i)@pred(A(i,j)) = s(i)@A(i,j1)
Meuf: s(i)@pred(A(i,j0)) = s(i)@pred(A(i,j))
----------------------------------------
s(i)@pred(A(i,j)) = s(i)@A(i,j1) &&
pred(A(i,j0)) < A(i,j1) && A(i,j1) <= pred(A(i,j))

repeat split => //. [> Line 235: ((repeat split);(intro //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0,j1:index,tau,tau':timestamp
H1: s(i)@tau = H(s(i)@pred(A(i,j)),k)
H2: tau' < A(i,j)
H3: A(i,j) <= tau
H4: A(i,j1) <= pred(A(i,j))
H5: forall (jj:index),
happens(A(i,jj)) && A(i,jj) <= pred(A(i,j)) => A(i,jj) <= A(i,j1)
Hap: happens(A(i,j), tau)
Heuf: A(i,j0) <= tau' || A(i,j0) < A(i,j)
IH: forall (tau0,tau':timestamp,i,j:index),
tau0 < tau =>
happens(A(i,j), tau0) =>
s(i)@tau0 = s(i)@A(i,j) && tau' < A(i,j) && A(i,j) <= tau0 =>
s(i)@tau' <> s(i)@tau0
Meq: s(i)@tau' = s(i)@tau
Meq': s(i)@tau' = H(s(i)@pred(A(i,j)),k)
Meq1: s(i)@pred(A(i,j)) = s(i)@A(i,j1)
Meuf: s(i)@pred(A(i,j0)) = s(i)@pred(A(i,j))
----------------------------------------
pred(A(i,j0)) < A(i,j1)

use H5 with j0; 1,2: case Heuf; auto. [> Line 236: ((have ... as ); 1,2: ((case Heuf);auto))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j,j0:index,tau,tau':timestamp
H0: i <> i0
H1: s(i)@tau = H(s(i)@pred(A(i,j)),k)
H2: tau' < A(i,j)
H3: A(i,j) <= tau
Hap: happens(A(i,j), tau)
Heuf: A(i0,j0) <= tau' || A(i0,j0) < A(i,j)
IH: forall (tau0,tau':timestamp,i,j:index),
tau0 < tau =>
happens(A(i,j), tau0) =>
s(i)@tau0 = s(i)@A(i,j) && tau' < A(i,j) && A(i,j) <= tau0 =>
s(i)@tau' <> s(i)@tau0
Meq: s(i)@tau' = s(i)@tau
Meq': s(i)@tau' = H(s(i)@pred(A(i,j)),k)
Meuf: s(i0)@pred(A(i0,j0)) = s(i)@pred(A(i,j))
----------------------------------------
false

+ (* case i<>i0 *)
use disjoint_chains with pred(A(i0,j0)),pred(A(i,j)),i0,i => //. [> Line 238: ((have ... as );(intro //))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j,j0:index,tau,tau':timestamp
H0: i <> i0
H1: s(i)@tau = H(s(i)@pred(A(i,j)),k)
H2: tau' < A(i,j)
H3: A(i,j) <= tau
Hap: happens(A(i,j), tau)
Heuf: A(i0,j0) <= tau' || A(i0,j0) < A(i,j)
IH: forall (tau0,tau':timestamp,i,j:index),
tau0 < tau =>
happens(A(i,j), tau0) =>
s(i)@tau0 = s(i)@A(i,j) && tau' < A(i,j) && A(i,j) <= tau0 =>
s(i)@tau' <> s(i)@tau0
Meq: s(i)@tau' = s(i)@tau
Meq': s(i)@tau' = H(s(i)@pred(A(i,j)),k)
Meuf: s(i0)@pred(A(i0,j0)) = s(i)@pred(A(i,j))
----------------------------------------
happens(pred(A(i,j)), pred(A(i0,j0)))

by case Heuf. [> Line 239: by (case Heuf)
[goal> Goal monotonic_chain is proved

Qed. Exiting proof mode.

(* SECURITY PROPERTIES *)

name m : message.

global goal [default/left,default/left]
strong_secrecy (tau:timestamp) : forall (i':index,tau':timestamp),
[happens(tau)] -> [happens(tau')] -> equiv(frame@tau, diff(s(i')@tau',m)). Goal strong_secrecy :
forall tau:timestamp,
Forall (i':index,tau':timestamp),
[happens(tau)] ->
[happens(tau')] -> equiv(frame@tau, diff(s(i')@tau', m))

Proof. [goal> Focused goal (1/1):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: tau:timestamp
----------------------------------------
Forall (i':index,tau':timestamp),
[happens(tau)] -> [happens(tau')] -> equiv(frame@tau, diff(s(i')@tau', m))

induction tau => i' tau' Htau Htau'. [> Line 251: ((induction tau);(intro i' tau' Htau Htau'))
[goal> Focused goal (1/3):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i':index,tau':timestamp
Htau: [happens(init)]
Htau': [happens(tau')]
----------------------------------------
0: frame@init
1: diff(s(i')@tau', m)

+ (* Init *)
expand frame@init. [> Line 254: (expand frame@init)
[goal> Focused goal (1/3):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i':index,tau':timestamp
Htau: [happens(init)]
Htau': [happens(tau')]
----------------------------------------
0: diff(s(i')@tau', m)

use lastupdate_pure with i',tau' as [Hinit | [j HA]]; try auto. [> Line 255: ((have ... as [Hinit|[j HA]]);(try auto))
[goal> Focused goal (1/4):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i':index,tau':timestamp
Hinit: [forall (j:index), happens(A(i',j)) => A(i',j) > tau']
Htau: [happens(init)]
Htau': [happens(tau')]
----------------------------------------
0: diff(s(i')@tau', m)

- use lastupdate_init with i',tau' as H; try auto. [> Line 257: ((have ... as H);(try auto))
[goal> Focused goal (1/4):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i':index,tau':timestamp
H: [s(i')@tau' = s(i')@init]
Hinit: [forall (j:index), happens(A(i',j)) => A(i',j) > tau']
Htau: [happens(init)]
Htau': [happens(tau')]
----------------------------------------
0: diff(s(i')@tau', m)

rewrite H; expand s(i')@init; fresh 0; auto. [> Line 258: ((rewrite ...);((expand s(i')@init);((fresh 0);auto)))
[goal> Focused goal (1/3):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i',j:index,tau':timestamp
HA: [happens(A(i',j)) &&
A(i',j) <= tau' &&
forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= tau' => A(i',jj) <= A(i',j)]
Htau: [happens(init)]
Htau': [happens(tau')]
----------------------------------------
0: diff(s(i')@tau', m)

- use lastupdate_A with i',j,tau' as H; try auto. [> Line 260: ((have ... as H);(try auto))
[goal> Focused goal (1/3):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i',j:index,tau':timestamp
H: [s(i')@tau' = s(i')@A(i',j)]
HA: [happens(A(i',j)) &&
A(i',j) <= tau' &&
forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= tau' => A(i',jj) <= A(i',j)]
Htau: [happens(init)]
Htau': [happens(tau')]
----------------------------------------
0: diff(s(i')@tau', m)

rewrite H in *; expand s(i')@A(i',j). [> Line 261: ((rewrite ... in *);(expand s(i')@A(i',j)))
[goal> Focused goal (1/3):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i',j:index,tau':timestamp
H: [s(i')@tau' = H(s(i')@pred(A(i',j)),k)]
HA: [happens(A(i',j)) &&
A(i',j) <= tau' &&
forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= tau' => A(i',jj) <= A(i',j)]
Htau: [happens(init)]
Htau': [happens(tau')]
----------------------------------------
0: diff(H(s(i')@pred(A(i',j)),k), m)

prf 0; rewrite if_true; [2: by fresh 0]. [> Line 262: ((prf 0);((rewrite ...); 2: by (fresh 0)))
[goal> Focused goal (1/3):
System: left:default/left
(equivalences: left:default/left, right:default/left)
Variables: i',j:index,tau':timestamp
H: [s(i')@tau' = H(s(i')@pred(A(i',j)),k)]
HA: [happens(A(i',j)) &&
A(i',j) <= tau' &&
forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= tau' => A(i',jj) <= A(i',j)]
Htau: [happens(init)]
Htau': [happens(tau')]
----------------------------------------
true &&
forall (j0:index),
A(i',j0) < A(i',j) => s(i')@pred(A(i',j)) <> s(i')@pred(A(i',j0))

simpl. [> Line 263: simpl
[goal> Focused goal (1/3):
System: left:default/left
(equivalences: left:default/left, right:default/left)
Variables: i',j:index,tau':timestamp
H: [s(i')@tau' = H(s(i')@pred(A(i',j)),k)]
HA: [happens(A(i',j)) &&
A(i',j) <= tau' &&
forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= tau' => A(i',jj) <= A(i',j)]
Htau: [happens(init)]
Htau': [happens(tau')]
----------------------------------------
forall (j0:index),
A(i',j0) < A(i',j) => s(i')@pred(A(i',j)) <> s(i')@pred(A(i',j0))

intro j0 HAi0. [> Line 263: (intro j0 HAi0)
[goal> Focused goal (1/3):
System: left:default/left
(equivalences: left:default/left, right:default/left)
Variables: i',j,j0:index,tau':timestamp
H: [s(i')@tau' = H(s(i')@pred(A(i',j)),k)]
HA: [happens(A(i',j)) &&
A(i',j) <= tau' &&
forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= tau' => A(i',jj) <= A(i',j)]
HAi0: A(i',j0) < A(i',j)
Htau: [happens(init)]
Htau': [happens(tau')]
----------------------------------------
s(i')@pred(A(i',j)) <> s(i')@pred(A(i',j0))

use lastupdate with i',pred(A(i',j)) as [[H1 H2] | H1]; try auto. [> Line 264: ((have ... as [[H1 H2]|H1]);(try auto))
[goal> Focused goal (1/4):
System: left:default/left
(equivalences: left:default/left, right:default/left)
Variables: i',j,j0:index,tau':timestamp
H: [s(i')@tau' = H(s(i')@pred(A(i',j)),k)]
H1: s(i')@pred(A(i',j)) = s(i')@init
H2: forall (j0:index), happens(A(i',j0)) => A(i',j0) > pred(A(i',j))
HA: [happens(A(i',j)) &&
A(i',j) <= tau' &&
forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= tau' => A(i',jj) <= A(i',j)]
HAi0: A(i',j0) < A(i',j)
Htau: [happens(init)]
Htau': [happens(tau')]
----------------------------------------
s(i')@pred(A(i',j)) <> s(i')@pred(A(i',j0))

* use H2 with j0 as H3; try auto. [> Line 265: ((have ... as H3);(try auto))
[goal> Focused goal (1/3):
System: left:default/left
(equivalences: left:default/left, right:default/left)
Variables: i',j,j0:index,tau':timestamp
H: [s(i')@tau' = H(s(i')@pred(A(i',j)),k)]
H1: exists (j0:index),
s(i')@pred(A(i',j)) = s(i')@A(i',j0) &&
A(i',j0) <= pred(A(i',j)) &&
forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= pred(A(i',j)) =>
A(i',jj) <= A(i',j0)
HA: [happens(A(i',j)) &&
A(i',j) <= tau' &&
forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= tau' => A(i',jj) <= A(i',j)]
HAi0: A(i',j0) < A(i',j)
Htau: [happens(init)]
Htau': [happens(tau')]
----------------------------------------
s(i')@pred(A(i',j)) <> s(i')@pred(A(i',j0))

* destruct H1 as [j1 [H1 H2 H3]]. [> Line 266: (destruct H1, [j1 [H1 H2 H3]])
[goal> Focused goal (1/3):
System: left:default/left
(equivalences: left:default/left, right:default/left)
Variables: i',j,j0,j1:index,tau':timestamp
H: [s(i')@tau' = H(s(i')@pred(A(i',j)),k)]
H1: s(i')@pred(A(i',j)) = s(i')@A(i',j1)
H2: A(i',j1) <= pred(A(i',j))
H3: forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= pred(A(i',j)) => A(i',jj) <= A(i',j1)
HA: [happens(A(i',j)) &&
A(i',j) <= tau' &&
forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= tau' => A(i',jj) <= A(i',j)]
HAi0: A(i',j0) < A(i',j)
Htau: [happens(init)]
Htau': [happens(tau')]
----------------------------------------
s(i')@pred(A(i',j)) <> s(i')@pred(A(i',j0))

use monotonic_chain with pred(A(i',j)),pred(A(i',j0)),i',j1 => //. [> Line 267: ((have ... as );(intro //))
[goal> Focused goal (1/3):
System: left:default/left
(equivalences: left:default/left, right:default/left)
Variables: i',j,j0,j1:index,tau':timestamp
H: [s(i')@tau' = H(s(i')@pred(A(i',j)),k)]
H1: s(i')@pred(A(i',j)) = s(i')@A(i',j1)
H2: A(i',j1) <= pred(A(i',j))
H3: forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= pred(A(i',j)) => A(i',jj) <= A(i',j1)
HA: [happens(A(i',j)) &&
A(i',j) <= tau' &&
forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= tau' => A(i',jj) <= A(i',j)]
HAi0: A(i',j0) < A(i',j)
Htau: [happens(init)]
Htau': [happens(tau')]
----------------------------------------
s(i')@pred(A(i',j)) = s(i')@A(i',j1) &&
pred(A(i',j0)) < A(i',j1) && A(i',j1) <= pred(A(i',j))

repeat split; try auto. [> Line 268: ((repeat split);(try auto))
[goal> Focused goal (1/3):
System: left:default/left
(equivalences: left:default/left, right:default/left)
Variables: i',j,j0,j1:index,tau':timestamp
H: [s(i')@tau' = H(s(i')@pred(A(i',j)),k)]
H1: s(i')@pred(A(i',j)) = s(i')@A(i',j1)
H2: A(i',j1) <= pred(A(i',j))
H3: forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= pred(A(i',j)) => A(i',jj) <= A(i',j1)
HA: [happens(A(i',j)) &&
A(i',j) <= tau' &&
forall (jj:index),
happens(A(i',jj)) && A(i',jj) <= tau' => A(i',jj) <= A(i',j)]
HAi0: A(i',j0) < A(i',j)
Htau: [happens(init)]
Htau': [happens(tau')]
----------------------------------------
pred(A(i',j0)) < A(i',j1)

use H3 with j0 as H4; try auto. [> Line 269: ((have ... as H4);(try auto))
[goal> Focused goal (1/2):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i',j:index,tau':timestamp
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
0: frame@O(j)
1: diff(s(i')@tau', m)

+ (* Oracle *)
expand frame, exec, cond, output. [> Line 272: (expand frame, exec, cond, output)
[goal> Focused goal (1/2):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i',j:index,tau':timestamp
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
0: <frame@pred(O(j)),
<of_bool(exec@pred(O(j)) && true),
if (exec@pred(O(j)) && true) then <H(input@O(j),k),G(input@O(j),k')>>>
1: diff(s(i')@tau', m)

fa !<_,_>, if _ then _, (_ && _), <_,_>. [> Line 273: (fa !pair(_,_) if _ then _ else zero (_ && _) pair(_,_))
[goal> Focused goal (1/2):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i',j:index,tau':timestamp
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
0: frame@pred(O(j))
1: H(input@O(j),k)
2: G(input@O(j),k')
3: diff(s(i')@tau', m)

prf 1; rewrite if_true; 2: fresh 1. [> Line 274: ((prf 1);((rewrite ...); 2: (fresh 1)))
[goal> Focused goal (1/3):
System: left:default/left, right:default/left (same for equivalences)
Variables: i',j:index,tau':timestamp
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
true &&
(forall (j0:index), O(j0) < O(j) => input@O(j) <> input@O(j0)) &&
forall (i,j0:index),
diff(A(i,j0) <= tau' || A(i,j0) < O(j) => input@O(j) <> s(i)@pred(A(i,j0)),
A(i,j0) < O(j) => input@O(j) <> s(i)@pred(A(i,j0)))

{
simpl; split. [> Line 275: (simpl;split)
[goal> Focused goal (1/4):
System: left:default/left, right:default/left (same for equivalences)
Variables: i',j:index,tau':timestamp
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
forall (j0:index), O(j0) < O(j) => input@O(j) <> input@O(j0)

* intro j0 H. [> Line 276: (intro j0 H)
[goal> Focused goal (1/4):
System: left:default/left, right:default/left (same for equivalences)
Variables: i',j,j0:index,tau':timestamp
H: O(j0) < O(j)
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
input@O(j) <> input@O(j0)

by apply unique_queries. [> Line 277: by (apply ... )
[goal> Focused goal (1/3):
System: left:default/left, right:default/left (same for equivalences)
Variables: i',j:index,tau':timestamp
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
forall (i,j0:index),
diff(A(i,j0) <= tau' || A(i,j0) < O(j) => input@O(j) <> s(i)@pred(A(i,j0)),
A(i,j0) < O(j) => input@O(j) <> s(i)@pred(A(i,j0)))

* intro i0 j0. [> Line 278: (intro i0 j0)
[goal> Focused goal (1/3):
System: left:default/left, right:default/left (same for equivalences)
Variables: i',i0,j,j0:index,tau':timestamp
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
diff(
A(i0,j0) <= tau' || A(i0,j0) < O(j) => input@O(j) <> s(i0)@pred(A(i0,j0)),
A(i0,j0) < O(j) => input@O(j) <> s(i0)@pred(A(i0,j0)))

project. [> Line 279: project
[goal> Focused goal (1/4):
System: left:default/left
(equivalences: left:default/left, right:default/left)
Variables: i',i0,j,j0:index,tau':timestamp
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
A(i0,j0) <= tau' || A(i0,j0) < O(j) => input@O(j) <> s(i0)@pred(A(i0,j0))

** intro H; destruct H as [H1|H2]. [> Line 280: ((intro H);(destruct H, [H1|H2]))
[goal> Focused goal (1/5):
System: left:default/left
(equivalences: left:default/left, right:default/left)
Variables: i',i0,j,j0:index,tau':timestamp
H1: A(i0,j0) <= tau'
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
input@O(j) <> s(i0)@pred(A(i0,j0))

*** rewrite equiv IH i0 (pred(A(i0,j0))) => // Hf; by fresh Hf. [> Line 281: (((rewrite equiv ...);(intro // Hf));by (fresh Hf))
[goal> Focused goal (1/4):
System: left:default/left
(equivalences: left:default/left, right:default/left)
Variables: i',i0,j,j0:index,tau':timestamp
H2: A(i0,j0) < O(j)
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
input@O(j) <> s(i0)@pred(A(i0,j0))

*** rewrite equiv IH i0 (pred(A(i0,j0))) => // Hf; by fresh Hf. [> Line 282: (((rewrite equiv ...);(intro // Hf));by (fresh Hf))
[goal> Focused goal (1/3):
System: right:default/left
(equivalences: left:default/left, right:default/left)
Variables: i',i0,j,j0:index,tau':timestamp
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
A(i0,j0) < O(j) => input@O(j) <> s(i0)@pred(A(i0,j0))

** intro H. [> Line 283: (intro H)
[goal> Focused goal (1/3):
System: right:default/left
(equivalences: left:default/left, right:default/left)
Variables: i',i0,j,j0:index,tau':timestamp
H: A(i0,j0) < O(j)
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
input@O(j) <> s(i0)@pred(A(i0,j0))

rewrite equiv IH i0 (pred(A(i0,j0))) => // Hf; by fresh Hf. [> Line 283: (((rewrite equiv ...);(intro // Hf));by (fresh Hf))
[goal> Focused goal (1/2):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i',j:index,tau':timestamp
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
0: frame@pred(O(j))
1: G(input@O(j),k')
2: diff(s(i')@tau', m)

}. [> Line 284: ??
[goal> Focused goal (1/2):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i',j:index,tau':timestamp
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
0: frame@pred(O(j))
1: G(input@O(j),k')
2: diff(s(i')@tau', m)

prf 1; rewrite if_true; 2: fresh 1; by apply IH. [> Line 285: ((prf 1);((rewrite ...); 2: ((fresh 1);by (apply ... ))))
[goal> Focused goal (1/2):
System: left:default/left, right:default/left (same for equivalences)
Variables: i',j:index,tau':timestamp
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
true &&
(forall (j0:index), O(j0) < O(j) => input@O(j) <> input@O(j0)) &&
forall (i,j0:index), A(i,j0) < O(j) => input@O(j) <> s(i)@A(i,j0)

simpl; split. [> Line 286: (simpl;split)
[goal> Focused goal (1/3):
System: left:default/left, right:default/left (same for equivalences)
Variables: i',j:index,tau':timestamp
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
forall (j0:index), O(j0) < O(j) => input@O(j) <> input@O(j0)

* intro j0 H. [> Line 287: (intro j0 H)
[goal> Focused goal (1/3):
System: left:default/left, right:default/left (same for equivalences)
Variables: i',j,j0:index,tau':timestamp
H: O(j0) < O(j)
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
input@O(j) <> input@O(j0)

apply unique_queries; auto. [> Line 288: ((apply ... );auto)
[goal> Focused goal (1/2):
System: left:default/left, right:default/left (same for equivalences)
Variables: i',j:index,tau':timestamp
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
forall (i,j0:index), A(i,j0) < O(j) => input@O(j) <> s(i)@A(i,j0)

* intro i0 j0 H. [> Line 289: (intro i0 j0 H)
[goal> Focused goal (1/2):
System: left:default/left, right:default/left (same for equivalences)
Variables: i',i0,j,j0:index,tau':timestamp
H: A(i0,j0) < O(j)
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
input@O(j) <> s(i0)@A(i0,j0)

rewrite equiv IH i0 (A(i0,j0)) => // Hf. [> Line 290: ((rewrite equiv ...);(intro // Hf))
[goal> Focused goal (1/2):
System: left:default/left, right:default/left (same for equivalences)
Variables: i',i0,j,j0:index,tau':timestamp
H: A(i0,j0) < O(j)
Hf: input@O(j) = m
Htau: [happens(O(j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(O(j)))] ->
[happens(tau')] -> equiv(frame@pred(O(j)), diff(s(i')@tau', m))
----------------------------------------
false

by fresh Hf. [> Line 291: by (fresh Hf)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i,i',j:index,tau':timestamp
Htau: [happens(A(i,j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(A(i,j)))] ->
[happens(tau')] -> equiv(frame@pred(A(i,j)), diff(s(i')@tau', m))
----------------------------------------
0: frame@A(i,j)
1: diff(s(i')@tau', m)

+ (* Tag *)
expand frame@A(i,j). [> Line 294: (expand frame@A(i,j))
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i,i',j:index,tau':timestamp
Htau: [happens(A(i,j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(A(i,j)))] ->
[happens(tau')] -> equiv(frame@pred(A(i,j)), diff(s(i')@tau', m))
----------------------------------------
0: <frame@pred(A(i,j)),
<of_bool(exec@A(i,j)),if exec@A(i,j) then output@A(i,j)>>
1: diff(s(i')@tau', m)

expand exec@A(i,j). [> Line 294: (expand exec@A(i,j))
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i,i',j:index,tau':timestamp
Htau: [happens(A(i,j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(A(i,j)))] ->
[happens(tau')] -> equiv(frame@pred(A(i,j)), diff(s(i')@tau', m))
----------------------------------------
0: <frame@pred(A(i,j)),
<of_bool(exec@pred(A(i,j)) && cond@A(i,j)),
if (exec@pred(A(i,j)) && cond@A(i,j)) then output@A(i,j)>>
1: diff(s(i')@tau', m)

expand cond@A(i,j). [> Line 294: (expand cond@A(i,j))
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i,i',j:index,tau':timestamp
Htau: [happens(A(i,j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(A(i,j)))] ->
[happens(tau')] -> equiv(frame@pred(A(i,j)), diff(s(i')@tau', m))
----------------------------------------
0: <frame@pred(A(i,j)),
<of_bool(exec@pred(A(i,j)) && true),
if (exec@pred(A(i,j)) && true) then output@A(i,j)>>
1: diff(s(i')@tau', m)

expand output@A(i,j). [> Line 294: (expand output@A(i,j))
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i,i',j:index,tau':timestamp
Htau: [happens(A(i,j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(A(i,j)))] ->
[happens(tau')] -> equiv(frame@pred(A(i,j)), diff(s(i')@tau', m))
----------------------------------------
0: <frame@pred(A(i,j)),
<of_bool(exec@pred(A(i,j)) && true),
if (exec@pred(A(i,j)) && true) then G(s(i)@A(i,j),k')>>
1: diff(s(i')@tau', m)

fa 0. [> Line 295: (fa 0)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i,i',j:index,tau':timestamp
Htau: [happens(A(i,j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(A(i,j)))] ->
[happens(tau')] -> equiv(frame@pred(A(i,j)), diff(s(i')@tau', m))
----------------------------------------
0: frame@pred(A(i,j))
1: <of_bool(exec@pred(A(i,j)) && true),
if (exec@pred(A(i,j)) && true) then G(s(i)@A(i,j),k')>
2: diff(s(i')@tau', m)

fa 1. [> Line 295: (fa 1)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i,i',j:index,tau':timestamp
Htau: [happens(A(i,j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(A(i,j)))] ->
[happens(tau')] -> equiv(frame@pred(A(i,j)), diff(s(i')@tau', m))
----------------------------------------
0: frame@pred(A(i,j))
1: if (exec@pred(A(i,j)) && true) then G(s(i)@A(i,j),k')
2: diff(s(i')@tau', m)

fa 1. [> Line 295: (fa 1)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/left (same for equivalences)
Variables: i,i',j:index,tau':timestamp
Htau: [happens(A(i,j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(A(i,j)))] ->
[happens(tau')] -> equiv(frame@pred(A(i,j)), diff(s(i')@tau', m))
----------------------------------------
0: frame@pred(A(i,j))
1: G(s(i)@A(i,j),k')
2: diff(s(i')@tau', m)

prf 1; rewrite if_true; 2: fresh 1; by apply IH. [> Line 296: ((prf 1);((rewrite ...); 2: ((fresh 1);by (apply ... ))))
[goal> Focused goal (1/1):
System: left:default/left, right:default/left (same for equivalences)
Variables: i,i',j:index,tau':timestamp
Htau: [happens(A(i,j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(A(i,j)))] ->
[happens(tau')] -> equiv(frame@pred(A(i,j)), diff(s(i')@tau', m))
----------------------------------------
true &&
(forall (j0:index), O(j0) < A(i,j) => s(i)@A(i,j) <> input@O(j0)) &&
forall (i0,j0:index), A(i0,j0) < A(i,j) => s(i)@A(i,j) <> s(i0)@A(i0,j0)

simpl; split. [> Line 297: (simpl;split)
[goal> Focused goal (1/2):
System: left:default/left, right:default/left (same for equivalences)
Variables: i,i',j:index,tau':timestamp
Htau: [happens(A(i,j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(A(i,j)))] ->
[happens(tau')] -> equiv(frame@pred(A(i,j)), diff(s(i')@tau', m))
----------------------------------------
forall (j0:index), O(j0) < A(i,j) => s(i)@A(i,j) <> input@O(j0)

- intro j0 H. [> Line 298: (intro j0 H)
[goal> Focused goal (1/2):
System: left:default/left, right:default/left (same for equivalences)
Variables: i,i',j,j0:index,tau':timestamp
H: O(j0) < A(i,j)
Htau: [happens(A(i,j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(A(i,j)))] ->
[happens(tau')] -> equiv(frame@pred(A(i,j)), diff(s(i')@tau', m))
----------------------------------------
s(i)@A(i,j) <> input@O(j0)

rewrite equiv IH i (A(i,j)) => // Hf; by fresh Hf. [> Line 299: (((rewrite equiv ...);(intro // Hf));by (fresh Hf))
[goal> Focused goal (1/1):
System: left:default/left, right:default/left (same for equivalences)
Variables: i,i',j:index,tau':timestamp
Htau: [happens(A(i,j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(A(i,j)))] ->
[happens(tau')] -> equiv(frame@pred(A(i,j)), diff(s(i')@tau', m))
----------------------------------------
forall (i0,j0:index), A(i0,j0) < A(i,j) => s(i)@A(i,j) <> s(i0)@A(i0,j0)

- intro i0 j0 H. [> Line 300: (intro i0 j0 H)
[goal> Focused goal (1/1):
System: left:default/left, right:default/left (same for equivalences)
Variables: i,i',i0,j,j0:index,tau':timestamp
H: A(i0,j0) < A(i,j)
Htau: [happens(A(i,j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(A(i,j)))] ->
[happens(tau')] -> equiv(frame@pred(A(i,j)), diff(s(i')@tau', m))
----------------------------------------
s(i)@A(i,j) <> s(i0)@A(i0,j0)

assert i=i0 || i<>i0; try auto. [> Line 301: ((have ((i = i0) || (i <> i0)));(try auto))
[goal> Focused goal (1/1):
System: left:default/left, right:default/left (same for equivalences)
Variables: i,i',i0,j,j0:index,tau':timestamp
H: A(i0,j0) < A(i,j)
H0: i = i0 || i <> i0
Htau: [happens(A(i,j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(A(i,j)))] ->
[happens(tau')] -> equiv(frame@pred(A(i,j)), diff(s(i')@tau', m))
----------------------------------------
s(i)@A(i,j) <> s(i0)@A(i0,j0)

case H0. [> Line 302: (case H0)
[goal> Focused goal (1/2):
System: left:default/left, right:default/left (same for equivalences)
Variables: i,i',j,j0:index,tau':timestamp
H: A(i,j0) < A(i,j)
Htau: [happens(A(i,j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(A(i,j)))] ->
[happens(tau')] -> equiv(frame@pred(A(i,j)), diff(s(i')@tau', m))
----------------------------------------
s(i)@A(i,j) <> s(i)@A(i,j0)

* by use monotonic_chain with A(i,j),A(i,j0),i,j => //. [> Line 303: (by (have ... as );(intro //))
[goal> Focused goal (1/1):
System: left:default/left, right:default/left (same for equivalences)
Variables: i,i',i0,j,j0:index,tau':timestamp
H: A(i0,j0) < A(i,j)
H0: i <> i0
Htau: [happens(A(i,j))]
Htau': [happens(tau')]
IH: Forall (i':index,tau':timestamp),
[happens(pred(A(i,j)))] ->
[happens(tau')] -> equiv(frame@pred(A(i,j)), diff(s(i')@tau', m))
----------------------------------------
s(i)@A(i,j) <> s(i0)@A(i0,j0)

* by use disjoint_chains with A(i,j),A(i0,j0),i,i0. [> Line 304: by (have ... as )
[goal> Goal strong_secrecy is proved

Qed. Exiting proof mode.

Press the left and right arrows to do and undo an instruction.

Alternatively, you can double-click on an instruction.

This zone shows a Squirrel file. You can double-click on a comment to collapse it for better readabilility.

This zone shows the output given by Squirrel.

This zone shows the output of the previous instruction, to help identifying the change caused by the instruction.

Previously: