set postQuantumSound=true.

LAK WITH PAIRS AND TAGS

[D] Lucca Hirschi, David Baelde, and Stéphanie Delaune. A method for unbounded verification of privacy-type properties. Journal of Computer Security, 27(3):277–342, 2019.

R –> T : nR T –> R : <nT,h(<<nR,nT>,tag1>,k)> R –> T : h(<<h(<<nR,nT>,tag1>,k),nR>,tag2>,k)

We consider tags in the messages (tag1 and tag2) to ease the proof.

This is a “light” model without the last check of T. ******************************************************************************

hash h

abstract ok : message
abstract ko : message

abstract tag1 : message
abstract tag2 : message

name key : index->message
name key': index->index->message

channel cT
channel cR

process tag(i,j:index) =
new nT;
in(cR,nR);
let m2 = h(<<nR,nT>,tag1>,diff(key(i),key'(i,j))) in
out(cT,<nT,m2>)

process reader =
new nR;
out(cR,nR);
in(cT,x);
if exists (i,k:index),
snd(x) = h(<<nR,fst(x)>,tag1>,diff(key(i),key'(i,k)))
then
out(cR, try find i,k such that
snd(x) = h(<<nR,fst(x)>,tag1>,diff(key(i),key'(i,k)))
in
h(<<snd(x),nR>,tag2>,diff(key(i),key'(i,k))))
else
out(cR,ko)

system ((!_k R: reader) | (!_i !_j T: tag(i,j))). System before processing:

(!_k R: reader ) | (!_i !_j T: tag i j)

System after processing:

(!_k
R:
out(cR,nR(k));
in(cT,x);
if exists (i,k:index),
(snd(x) = h(pair(pair(nR(k),fst(x)),tag1),diff(key(i),key'(i,k)))) then
R1:
out(cR,
try find i,k:index such that
(snd(x) = h(pair(pair(nR(k),fst(x)),tag1),diff(key(i),key'(i,k)))) in
h(pair(pair(snd(x),nR(k)),tag2),diff(key(i),key'(i,k))) else zero);
null else R2: out(cR,ko); null) |
(!_i
!_j
in(cR,nR);
let m2 = h(pair(pair(nR,nT(i,j)),tag1),diff(key(i),key'(i,j))) in
T: out(cT,pair(nT(i,j),m2(i,j))); null)

System default registered with actions (init,R,R1,R2,T).

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 <]

axiom tags_neq : tag1 <> tag2.

goal wa_R1_R2 (tau:timestamp,k:index):
happens(tau) =>
(exists (i,j:index)
snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,diff(key(i),key'(i,j))))
=
(exists (i,j:index),
T(i,j) < tau && R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@tau) &&
fst(output@T(i,j)) = fst(input@tau) &&
input@T(i,j) = output@R(k)). Goal wa_R1_R2 :
happens(tau) =>
(exists (i,j:index),
snd(input@tau) =
h(<<nR(k),fst(input@tau)>,tag1>,diff(key(i), key'(i,j)))) =
exists (i,j:index),
T(i,j) < tau &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@tau) &&
fst(output@T(i,j)) = fst(input@tau) && input@T(i,j) = output@R(k)
Proof. [goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: k:index,tau:timestamp
----------------------------------------
happens(tau) =>
(exists (i,j:index),
snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,diff(key(i), key'(i,j)))) =
exists (i,j:index),
T(i,j) < tau &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@tau) &&
fst(output@T(i,j)) = fst(input@tau) && input@T(i,j) = output@R(k)
intro Hap. [> Line 70: (intro Hap)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: k:index,tau:timestamp
Hap: happens(tau)
----------------------------------------
(exists (i,j:index),
snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,diff(key(i), key'(i,j)))) =
exists (i,j:index),
T(i,j) < tau &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@tau) &&
fst(output@T(i,j)) = fst(input@tau) && input@T(i,j) = output@R(k)
rewrite eq_iff; split. [> Line 71: ((rewrite ...);split)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: k:index,tau:timestamp
Hap: happens(tau)
----------------------------------------
(exists (i,j:index),
snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,diff(key(i), key'(i,j)))) =>
exists (i,j:index),
T(i,j) < tau &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@tau) &&
fst(output@T(i,j)) = fst(input@tau) && input@T(i,j) = output@R(k)

(* COND => WA *)
+ intro [i j H]. [> Line 74: (intro [i j H])
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,k:index,tau:timestamp
H: snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,diff(key(i), key'(i,j)))
Hap: happens(tau)
----------------------------------------
exists (i,j:index),
T(i,j) < tau &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@tau) &&
fst(output@T(i,j)) = fst(input@tau) && input@T(i,j) = output@R(k)
use tags_neq; project. [> Line 75: ((have ... as );project)
[goal> Focused goal (1/3):
System: left:default/left
Variables: i,j,k:index,tau:timestamp
H: snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,key(i))
Hap: happens(tau)
Mneq: tag1 <> tag2
----------------------------------------
exists (i,j:index),
T(i,j) < tau &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@tau) &&
fst(output@T(i,j)) = fst(input@tau) && input@T(i,j) = output@R(k)

(* LEFT *)
- euf H => _ _ _ //. [> Line 78: ((euf H);(intro _ _ _ //))
[goal> Focused goal (1/3):
System: left:default/left
Variables: i,j,j0,k:index,tau:timestamp
H: snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,key(i))
Hap: happens(tau)
Mneq: tag1 <> tag2
_: <<input@T(i,j0),nT(i,j0)>,tag1> = <<nR(k),fst(input@tau)>,tag1>
_: T(i,j0) < tau
----------------------------------------
exists (i,j:index),
T(i,j) < tau &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@tau) &&
fst(output@T(i,j)) = fst(input@tau) && input@T(i,j) = output@R(k)
exists i,j0. [> Line 79: (exists i, j0)
[goal> Focused goal (1/3):
System: left:default/left
Variables: i,j,j0,k:index,tau:timestamp
H: snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,key(i))
Hap: happens(tau)
Mneq: tag1 <> tag2
_: <<input@T(i,j0),nT(i,j0)>,tag1> = <<nR(k),fst(input@tau)>,tag1>
_: T(i,j0) < tau
----------------------------------------
T(i,j0) < tau &&
R(k) < T(i,j0) &&
snd(output@T(i,j0)) = snd(input@tau) &&
fst(output@T(i,j0)) = fst(input@tau) && input@T(i,j0) = output@R(k)
assert input@T(i,j0)=nR(k) as Meq1 by auto. [> Line 80: ((have (input@T(i,j0) = nR(k)), Meq1); 1: by auto)
[goal> Focused goal (1/3):
System: left:default/left
Variables: i,j,j0,k:index,tau:timestamp
H: snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,key(i))
Hap: happens(tau)
Meq1: input@T(i,j0) = nR(k)
Mneq: tag1 <> tag2
_: <<input@T(i,j0),nT(i,j0)>,tag1> = <<nR(k),fst(input@tau)>,tag1>
_: T(i,j0) < tau
----------------------------------------
T(i,j0) < tau &&
R(k) < T(i,j0) &&
snd(output@T(i,j0)) = snd(input@tau) &&
fst(output@T(i,j0)) = fst(input@tau) && input@T(i,j0) = output@R(k)
fresh Meq1 => C /=. [> Line 81: ((fresh Meq1);(intro C /=))
[goal> Focused goal (1/3):
System: left:default/left
Variables: i,j,j0,k:index,tau:timestamp
C: R(k) < T(i,j0) || R1(k) < T(i,j0) || R2(k) < T(i,j0)
H: snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,key(i))
Hap: happens(tau)
Meq1: input@T(i,j0) = nR(k)
Mneq: tag1 <> tag2
_: <<input@T(i,j0),nT(i,j0)>,tag1> = <<nR(k),fst(input@tau)>,tag1>
_: T(i,j0) < tau
----------------------------------------
R(k) < T(i,j0) &&
m2(i,j0)@T(i,j0) = snd(input@tau) && input@T(i,j0) = output@R(k)
case C => //. [> Line 82: ((case C);(intro //))
[goal> Focused goal (1/4):
System: left:default/left
Variables: i,j,j0,k:index,tau:timestamp
C: R1(k) < T(i,j0)
H: snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,key(i))
Hap: happens(tau)
Meq1: input@T(i,j0) = nR(k)
Mneq: tag1 <> tag2
_: <<input@T(i,j0),nT(i,j0)>,tag1> = <<nR(k),fst(input@tau)>,tag1>
_: T(i,j0) < tau
----------------------------------------
R(k) < T(i,j0) &&
m2(i,j0)@T(i,j0) = snd(input@tau) && input@T(i,j0) = output@R(k)
* by depends R(k),R1(k). [> Line 83: by (depends R(k), R1(k))
[goal> Focused goal (1/3):
System: left:default/left
Variables: i,j,j0,k:index,tau:timestamp
C: R2(k) < T(i,j0)
H: snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,key(i))
Hap: happens(tau)
Meq1: input@T(i,j0) = nR(k)
Mneq: tag1 <> tag2
_: <<input@T(i,j0),nT(i,j0)>,tag1> = <<nR(k),fst(input@tau)>,tag1>
_: T(i,j0) < tau
----------------------------------------
R(k) < T(i,j0) &&
m2(i,j0)@T(i,j0) = snd(input@tau) && input@T(i,j0) = output@R(k)
* by depends R(k),R2(k). [> Line 84: by (depends R(k), R2(k))
[goal> Focused goal (1/2):
System: right:default/right
Variables: i,j,k:index,tau:timestamp
H: snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,key'(i,j))
Hap: happens(tau)
Mneq: tag1 <> tag2
----------------------------------------
exists (i,j:index),
T(i,j) < tau &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@tau) &&
fst(output@T(i,j)) = fst(input@tau) && input@T(i,j) = output@R(k)

(* RIGHT *)
- euf H => _ _ _ //. [> Line 87: ((euf H);(intro _ _ _ //))
[goal> Focused goal (1/2):
System: right:default/right
Variables: i,j,k:index,tau:timestamp
H: snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,key'(i,j))
Hap: happens(tau)
Mneq: tag1 <> tag2
_: i = i && j = j
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@tau)>,tag1>
_: T(i,j) < tau
----------------------------------------
exists (i,j:index),
T(i,j) < tau &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@tau) &&
fst(output@T(i,j)) = fst(input@tau) && input@T(i,j) = output@R(k)
exists i,j. [> Line 88: (exists i, j)
[goal> Focused goal (1/2):
System: right:default/right
Variables: i,j,k:index,tau:timestamp
H: snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,key'(i,j))
Hap: happens(tau)
Mneq: tag1 <> tag2
_: i = i && j = j
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@tau)>,tag1>
_: T(i,j) < tau
----------------------------------------
T(i,j) < tau &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@tau) &&
fst(output@T(i,j)) = fst(input@tau) && input@T(i,j) = output@R(k)
assert input@T(i,j)=nR(k) as Meq1 by auto. [> Line 89: ((have (input@T(i,j) = nR(k)), Meq1); 1: by auto)
[goal> Focused goal (1/2):
System: right:default/right
Variables: i,j,k:index,tau:timestamp
H: snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,key'(i,j))
Hap: happens(tau)
Meq1: input@T(i,j) = nR(k)
Mneq: tag1 <> tag2
_: i = i && j = j
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@tau)>,tag1>
_: T(i,j) < tau
----------------------------------------
T(i,j) < tau &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@tau) &&
fst(output@T(i,j)) = fst(input@tau) && input@T(i,j) = output@R(k)
fresh Meq1 => C /=. [> Line 90: ((fresh Meq1);(intro C /=))
[goal> Focused goal (1/2):
System: right:default/right
Variables: i,j,k:index,tau:timestamp
C: R(k) < T(i,j) || R1(k) < T(i,j) || R2(k) < T(i,j)
H: snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,key'(i,j))
Hap: happens(tau)
Meq1: input@T(i,j) = nR(k)
Mneq: tag1 <> tag2
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@tau)>,tag1>
_: T(i,j) < tau
----------------------------------------
R(k) < T(i,j) &&
m2(i,j)@T(i,j) = snd(input@tau) && input@T(i,j) = output@R(k)
case C => //. [> Line 91: ((case C);(intro //))
[goal> Focused goal (1/3):
System: right:default/right
Variables: i,j,k:index,tau:timestamp
C: R1(k) < T(i,j)
H: snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,key'(i,j))
Hap: happens(tau)
Meq1: input@T(i,j) = nR(k)
Mneq: tag1 <> tag2
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@tau)>,tag1>
_: T(i,j) < tau
----------------------------------------
R(k) < T(i,j) &&
m2(i,j)@T(i,j) = snd(input@tau) && input@T(i,j) = output@R(k)
* by depends R(k),R1(k). [> Line 92: by (depends R(k), R1(k))
[goal> Focused goal (1/2):
System: right:default/right
Variables: i,j,k:index,tau:timestamp
C: R2(k) < T(i,j)
H: snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,key'(i,j))
Hap: happens(tau)
Meq1: input@T(i,j) = nR(k)
Mneq: tag1 <> tag2
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@tau)>,tag1>
_: T(i,j) < tau
----------------------------------------
R(k) < T(i,j) &&
m2(i,j)@T(i,j) = snd(input@tau) && input@T(i,j) = output@R(k)
* by depends R(k),R2(k). [> Line 93: by (depends R(k), R2(k))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: k:index,tau:timestamp
Hap: happens(tau)
----------------------------------------
(exists (i,j:index),
T(i,j) < tau &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@tau) &&
fst(output@T(i,j)) = fst(input@tau) && input@T(i,j) = output@R(k)) =>
exists (i,j:index),
snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,diff(key(i), key'(i,j)))

(* WA => COND *)
+ intro [i j _]; exists i,j. [> Line 96: ((intro [i j _]);(exists i, j))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j,k:index,tau:timestamp
Hap: happens(tau)
_: T(i,j) < tau &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@tau) &&
fst(output@T(i,j)) = fst(input@tau) && input@T(i,j) = output@R(k)
----------------------------------------
snd(input@tau) = h(<<nR(k),fst(input@tau)>,tag1>,diff(key(i), key'(i,j)))
by expand output, m2. [> Line 97: by (expand output, m2)
[goal> Goal wa_R1_R2 is proved

Qed. Exiting proof mode.


 goal [default/left] wa_R1_left (i,k:index):
happens(R1(k)) =>
(snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key(i)))
=
(exists j:index,
T(i,j) < R1(k) && R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) &&
input@T(i,j) = output@R(k)). Goal wa_R1_left :
happens(R1(k)) =>
(snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key(i))) =
exists (j:index),
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k)

The next two lemmas are more precise variants of the previous one, specifically for R1. They are useful to simplify the try-find construct in the output of that action. Note that the proofs of the next two lemmas are almost identical, but their statements differ in the treatment of index k, and they deal with distinct systems.
Proof. [goal> Focused goal (1/1):
System: default/left
Variables: i,k:index
----------------------------------------
happens(R1(k)) =>
(snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key(i))) =
exists (j:index),
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k)
intro Hap. [> Line 116: (intro Hap)
[goal> Focused goal (1/1):
System: default/left
Variables: i,k:index
Hap: happens(R1(k))
----------------------------------------
(snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key(i))) =
exists (j:index),
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k)
rewrite eq_iff; split; 2: by intro [j _]; expand output, m2. [> Line 117: ((rewrite ...);
(split; 2: by ((intro [j _]);(expand output, m2))))

[goal> Focused goal (1/1):
System: default/left
Variables: i,k:index
Hap: happens(R1(k))
----------------------------------------
snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key(i)) =>
exists (j:index),
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k)

intro Meq. [> Line 119: (intro Meq)
[goal> Focused goal (1/1):
System: default/left
Variables: i,k:index
Hap: happens(R1(k))
Meq: snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key(i))
----------------------------------------
exists (j:index),
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k)
use tags_neq. [> Line 120: (have ... as )
[goal> Focused goal (1/1):
System: default/left
Variables: i,k:index
Hap: happens(R1(k))
Meq: snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key(i))
Mneq: tag1 <> tag2
----------------------------------------
exists (j:index),
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k)
euf Meq => _ _ _ //. [> Line 121: ((euf Meq);(intro _ _ _ //))
[goal> Focused goal (1/1):
System: default/left
Variables: i,j,k:index
Hap: happens(R1(k))
Meq: snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key(i))
Mneq: tag1 <> tag2
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@R1(k))>,tag1>
_: T(i,j) < R1(k)
----------------------------------------
exists (j:index),
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k)
exists j. [> Line 122: (exists j)
[goal> Focused goal (1/1):
System: default/left
Variables: i,j,k:index
Hap: happens(R1(k))
Meq: snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key(i))
Mneq: tag1 <> tag2
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@R1(k))>,tag1>
_: T(i,j) < R1(k)
----------------------------------------
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k)
assert input@T(i,j) = nR(k) as Meq1 by auto. [> Line 123: ((have (input@T(i,j) = nR(k)), Meq1); 1: by auto)
[goal> Focused goal (1/1):
System: default/left
Variables: i,j,k:index
Hap: happens(R1(k))
Meq: snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key(i))
Meq1: input@T(i,j) = nR(k)
Mneq: tag1 <> tag2
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@R1(k))>,tag1>
_: T(i,j) < R1(k)
----------------------------------------
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k)
fresh Meq1 => C /=. [> Line 124: ((fresh Meq1);(intro C /=))
[goal> Focused goal (1/1):
System: default/left
Variables: i,j,k:index
C: R(k) < T(i,j) || R1(k) < T(i,j) || R2(k) < T(i,j)
Hap: happens(R1(k))
Meq: snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key(i))
Meq1: input@T(i,j) = nR(k)
Mneq: tag1 <> tag2
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@R1(k))>,tag1>
_: T(i,j) < R1(k)
----------------------------------------
R(k) < T(i,j) &&
m2(i,j)@T(i,j) = snd(input@R1(k)) && input@T(i,j) = output@R(k)
case C => //. [> Line 125: ((case C);(intro //))
[goal> Focused goal (1/1):
System: default/left
Variables: i,j,k:index
C: R2(k) < T(i,j)
Hap: happens(R1(k))
Meq: snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key(i))
Meq1: input@T(i,j) = nR(k)
Mneq: tag1 <> tag2
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@R1(k))>,tag1>
_: T(i,j) < R1(k)
----------------------------------------
R(k) < T(i,j) &&
m2(i,j)@T(i,j) = snd(input@R1(k)) && input@T(i,j) = output@R(k)
by depends R(k),R2(k). [> Line 126: by (depends R(k), R2(k))
[goal> Goal wa_R1_left is proved

Qed. Exiting proof mode.

goal [default/right] wa_R1_right (i,j,k:index):
happens(R1(k)) =>
(snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key'(i,j)))
=
(T(i,j) < R1(k) && R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) &&
input@T(i,j) = output@R(k)). Goal wa_R1_right :
happens(R1(k)) =>
(snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key'(i,j))) =
(T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k))
Proof. [goal> Focused goal (1/1):
System: default/right
Variables: i,j,k:index
----------------------------------------
happens(R1(k)) =>
(snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key'(i,j))) =
(T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k))
intro Hap. [> Line 138: (intro Hap)
[goal> Focused goal (1/1):
System: default/right
Variables: i,j,k:index
Hap: happens(R1(k))
----------------------------------------
(snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key'(i,j))) =
(T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k))
rewrite eq_iff; split; 2: by intro [j _]; expand output, m2. [> Line 139: ((rewrite ...);
(split; 2: by ((intro [j _]);(expand output, m2))))

[goal> Focused goal (1/1):
System: default/right
Variables: i,j,k:index
Hap: happens(R1(k))
----------------------------------------
snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key'(i,j)) =>
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k)

intro Meq. [> Line 141: (intro Meq)
[goal> Focused goal (1/1):
System: default/right
Variables: i,j,k:index
Hap: happens(R1(k))
Meq: snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key'(i,j))
----------------------------------------
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k)
use tags_neq. [> Line 142: (have ... as )
[goal> Focused goal (1/1):
System: default/right
Variables: i,j,k:index
Hap: happens(R1(k))
Meq: snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key'(i,j))
Mneq: tag1 <> tag2
----------------------------------------
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k)
euf Meq => _ _ _ //. [> Line 143: ((euf Meq);(intro _ _ _ //))
[goal> Focused goal (1/1):
System: default/right
Variables: i,j,k:index
Hap: happens(R1(k))
Meq: snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key'(i,j))
Mneq: tag1 <> tag2
_: i = i && j = j
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@R1(k))>,tag1>
_: T(i,j) < R1(k)
----------------------------------------
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k)
assert input@T(i,j) = nR(k) as Meq1 by auto. [> Line 144: ((have (input@T(i,j) = nR(k)), Meq1); 1: by auto)
[goal> Focused goal (1/1):
System: default/right
Variables: i,j,k:index
Hap: happens(R1(k))
Meq: snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key'(i,j))
Meq1: input@T(i,j) = nR(k)
Mneq: tag1 <> tag2
_: i = i && j = j
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@R1(k))>,tag1>
_: T(i,j) < R1(k)
----------------------------------------
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k)
fresh Meq1 => C /=. [> Line 145: ((fresh Meq1);(intro C /=))
[goal> Focused goal (1/1):
System: default/right
Variables: i,j,k:index
C: R(k) < T(i,j) || R1(k) < T(i,j) || R2(k) < T(i,j)
Hap: happens(R1(k))
Meq: snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key'(i,j))
Meq1: input@T(i,j) = nR(k)
Mneq: tag1 <> tag2
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@R1(k))>,tag1>
_: T(i,j) < R1(k)
----------------------------------------
R(k) < T(i,j) &&
m2(i,j)@T(i,j) = snd(input@R1(k)) && input@T(i,j) = output@R(k)
case C => //. [> Line 146: ((case C);(intro //))
[goal> Focused goal (1/1):
System: default/right
Variables: i,j,k:index
C: R2(k) < T(i,j)
Hap: happens(R1(k))
Meq: snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key'(i,j))
Meq1: input@T(i,j) = nR(k)
Mneq: tag1 <> tag2
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@R1(k))>,tag1>
_: T(i,j) < R1(k)
----------------------------------------
R(k) < T(i,j) &&
m2(i,j)@T(i,j) = snd(input@R1(k)) && input@T(i,j) = output@R(k)
by depends R(k),R2(k). [> Line 147: by (depends R(k), R2(k))
[goal> Goal wa_R1_right is proved

Qed. Exiting proof mode.


 goal wa_R1_tryfind (k:index) : happens(R1(k)) =>
(if exec@pred(R1(k)) && cond@R1(k) then
try find i,j such that
snd(input@R1(k)) =
h(<<nR(k),fst(input@R1(k))>,tag1>,diff(key(i),key'(i,j)))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i),key'(i,j))))
=
(if exec@pred(R1(k)) && cond@R1(k) then
try find i,j such that
exec@pred(R1(k)) &&
(T(i,j) < R1(k) && R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) &&
input@T(i,j) = output@R(k))
in
h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i),key'(i,j)))). Goal wa_R1_tryfind :
happens(R1(k)) =>
if (exec@pred(R1(k)) && cond@R1(k)) then
try find i,j:index such that
(snd(input@R1(k)) =
h(<<nR(k),fst(input@R1(k))>,tag1>,diff(key(i), key'(i,j))))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,j))) =
if (exec@pred(R1(k)) && cond@R1(k)) then
try find i,j:index such that
(exec@pred(R1(k)) &&
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,j)))

Equality used to rewrite the try-find in R1 so that its condition can be discharged using fadup.
Proof. [goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: k:index
----------------------------------------
happens(R1(k)) =>
if (exec@pred(R1(k)) && cond@R1(k)) then
try find i,j:index such that
(snd(input@R1(k)) =
h(<<nR(k),fst(input@R1(k))>,tag1>,diff(key(i), key'(i,j))))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,j))) =
if (exec@pred(R1(k)) && cond@R1(k)) then
try find i,j:index such that
(exec@pred(R1(k)) &&
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,j)))
intro Hap. [> Line 169: (intro Hap)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: k:index
Hap: happens(R1(k))
----------------------------------------
if (exec@pred(R1(k)) && cond@R1(k)) then
try find i,j:index such that
(snd(input@R1(k)) =
h(<<nR(k),fst(input@R1(k))>,tag1>,diff(key(i), key'(i,j))))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,j))) =
if (exec@pred(R1(k)) && cond@R1(k)) then
try find i,j:index such that
(exec@pred(R1(k)) &&
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,j)))
case exec@pred(R1(k)) => Hexec; 2: auto. [> Line 170: (((case exec@pred(R1(k)));(intro Hexec)); 2: auto)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: k:index
Hap: happens(R1(k))
Hexec: exec@pred(R1(k))
----------------------------------------
if (true && cond@R1(k)) then
try find i,j:index such that
(snd(input@R1(k)) =
h(<<nR(k),fst(input@R1(k))>,tag1>,diff(key(i), key'(i,j))))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,j))) =
if (true && cond@R1(k)) then
try find i,j:index such that
(true &&
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,j)))
case cond@R1(k) => Hcond; 2: auto. [> Line 171: (((case cond@R1(k));(intro Hcond)); 2: auto)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: k:index
Hap: happens(R1(k))
Hcond: cond@R1(k)
Hexec: exec@pred(R1(k))
----------------------------------------
if (true && true) then
try find i,j:index such that
(snd(input@R1(k)) =
h(<<nR(k),fst(input@R1(k))>,tag1>,diff(key(i), key'(i,j))))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,j))) =
if (true && true) then
try find i,j:index such that
(true &&
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,j)))
simpl. [> Line 172: simpl
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: k:index
Hap: happens(R1(k))
Hcond: cond@R1(k)
Hexec: exec@pred(R1(k))
----------------------------------------
try find i,j:index such that
(snd(input@R1(k)) =
h(<<nR(k),fst(input@R1(k))>,tag1>,diff(key(i), key'(i,j))))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,j))) =
try find i,j:index such that
(T(i,j) < R1(k) &&
R(k) < T(i,j) &&
m2(i,j)@T(i,j) = snd(input@R1(k)) &&
nT(i,j) = fst(input@R1(k)) && input@T(i,j) = output@R(k))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,j)))
(* It is important to project before using "fa" on
the "try find" construct so that the redundant
index k on the left is treated smartly. *)
project. [> Line 176: project
[goal> Focused goal (1/2):
System: left:default/left
Variables: k:index
Hap: happens(R1(k))
Hcond: cond@R1(k)
Hexec: exec@pred(R1(k))
----------------------------------------
try find i,j:index such that
(snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key(i)))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,key(i)) =
try find i,j:index such that
(T(i,j) < R1(k) &&
R(k) < T(i,j) &&
m2(i,j)@T(i,j) = snd(input@R1(k)) &&
nT(i,j) = fst(input@R1(k)) && input@T(i,j) = output@R(k))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,key(i))
+ fa => // Heq. [> Line 177: (fa;(intro // Heq))
[goal> Focused goal (1/2):
System: left:default/left
Variables: i,j,k:index
Hap: happens(R1(k))
Hcond: cond@R1(k)
Heq: snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key(i))
Hexec: exec@pred(R1(k))
----------------------------------------
exists (j:index),
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
m2(i,j)@T(i,j) = snd(input@R1(k)) &&
nT(i,j) = fst(input@R1(k)) && input@T(i,j) = output@R(k)
by rewrite wa_R1_left in Heq. [> Line 178: by (rewrite ... in Heq)
[goal> Focused goal (1/1):
System: right:default/right
Variables: k:index
Hap: happens(R1(k))
Hcond: cond@R1(k)
Hexec: exec@pred(R1(k))
----------------------------------------
try find i,j:index such that
(snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key'(i,j)))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,key'(i,j)) =
try find i,j:index such that
(T(i,j) < R1(k) &&
R(k) < T(i,j) &&
m2(i,j)@T(i,j) = snd(input@R1(k)) &&
nT(i,j) = fst(input@R1(k)) && input@T(i,j) = output@R(k))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,key'(i,j))
+ fa => // Heq. [> Line 179: (fa;(intro // Heq))
[goal> Focused goal (1/1):
System: right:default/right
Variables: i,j,k:index
Hap: happens(R1(k))
Hcond: cond@R1(k)
Heq: snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key'(i,j))
Hexec: exec@pred(R1(k))
----------------------------------------
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
m2(i,j)@T(i,j) = snd(input@R1(k)) &&
nT(i,j) = fst(input@R1(k)) && input@T(i,j) = output@R(k)
by rewrite wa_R1_right in Heq. [> Line 180: by (rewrite ... in Heq)
[goal> Goal wa_R1_tryfind is proved

Qed. Exiting proof mode.

equiv unlinkability. Goal unlinkability :
forall t:timestamp, equiv(frame@t)
Proof. [goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: t:timestamp
H: [happens(t)]
----------------------------------------
0: frame@t
induction t. [> Line 185: (induction t)
[goal> Focused goal (1/5):
Systems: left:default/left, right:default/right (same for equivalences)
H: [happens(init)]
----------------------------------------
0: frame@init

(* Case init *)
+ auto. [> Line 188: auto
[goal> Focused goal (1/4):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: k:index
H: [happens(R(k))]
IH: equiv(frame@pred(R(k)))
----------------------------------------
0: frame@R(k)

(* Case R *)
+ expand frame, exec, cond, output. [> Line 191: (expand frame, exec, cond, output)
[goal> Focused goal (1/4):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: k:index
H: [happens(R(k))]
IH: equiv(frame@pred(R(k)))
----------------------------------------
0: <frame@pred(R(k)),
<of_bool(exec@pred(R(k)) && true),if (exec@pred(R(k)) && true) then nR(k)>>
fa !<_,_>, if _ then _. [> Line 192: (fa !pair(_,_) if _ then _ else zero)
[goal> Focused goal (1/4):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: k:index
H: [happens(R(k))]
IH: equiv(frame@pred(R(k)))
----------------------------------------
0: frame@pred(R(k))
1: nR(k)
fresh 1; rewrite if_true. [> Line 193: ((fresh 1);(rewrite ...))
[goal> Focused goal (1/5):
System: left:default/left, right:default/right (same for equivalences)
Variables: k:index
H: [happens(R(k))]
IH: equiv(frame@pred(R(k)))
----------------------------------------
(forall (k0:index), R2(k0) < R(k) => k0 <> k) &&
(forall (k0:index), R1(k0) < R(k) => k0 <> k) &&
forall (k0:index), R(k0) < R(k) => k0 <> k

 {
repeat split => // j0 H1. [> Line 194: ((repeat split);(intro // j0 H1))
[goal> Focused goal (1/6):
System: left:default/left, right:default/right (same for equivalences)
Variables: j0,k:index
H: [happens(R(k))]
H1: R2(j0) < R(k)
IH: equiv(frame@pred(R(k)))
----------------------------------------
j0 <> k
by depends R(j0),R2(j0). [> Line 195: by (depends R(j0), R2(j0))
[goal> Focused goal (1/5):
System: left:default/left, right:default/right (same for equivalences)
Variables: j0,k:index
H: [happens(R(k))]
H1: R1(j0) < R(k)
IH: equiv(frame@pred(R(k)))
----------------------------------------
j0 <> k
by depends R(j0),R1(j0). [> Line 196: by (depends R(j0), R1(j0))
[goal> Focused goal (1/4):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: k:index
H: [happens(R(k))]
IH: equiv(frame@pred(R(k)))
----------------------------------------
0: frame@pred(R(k))
}
auto. [> Line 198: auto
[goal> Focused goal (1/3):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: k:index
H: [happens(R1(k))]
IH: equiv(frame@pred(R1(k)))
----------------------------------------
0: frame@R1(k)

(* Case R1 *)
+ expand frame, exec, output. [> Line 201: (expand frame, exec, output)
[goal> Focused goal (1/3):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: k:index
H: [happens(R1(k))]
IH: equiv(frame@pred(R1(k)))
----------------------------------------
0: <frame@pred(R1(k)),
<of_bool(exec@pred(R1(k)) && cond@R1(k)),
if (exec@pred(R1(k)) && cond@R1(k)) then
try find i,k0:index such that
(snd(input@R1(k)) =
h(<<nR(k),fst(input@R1(k))>,tag1>,diff(key(i), key'(i,k0))))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,k0)))>>
fa !<_,_>. [> Line 202: (fa !pair(_,_))
[goal> Focused goal (1/3):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: k:index
H: [happens(R1(k))]
IH: equiv(frame@pred(R1(k)))
----------------------------------------
0: frame@pred(R1(k))
1: exec@pred(R1(k)) && cond@R1(k)
2: if (exec@pred(R1(k)) && cond@R1(k)) then
try find i,k0:index such that
(snd(input@R1(k)) =
h(<<nR(k),fst(input@R1(k))>,tag1>,diff(key(i), key'(i,k0))))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,k0)))
rewrite wa_R1_tryfind; 1: auto. [> Line 203: ((rewrite ...); 1: auto)
[goal> Focused goal (1/3):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: k:index
H: [happens(R1(k))]
IH: equiv(frame@pred(R1(k)))
----------------------------------------
0: frame@pred(R1(k))
1: exec@pred(R1(k)) && cond@R1(k)
2: if (exec@pred(R1(k)) && cond@R1(k)) then
try find i,j:index such that
(exec@pred(R1(k)) &&
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,j)))
expand cond; rewrite wa_R1_R2; 1: auto. [> Line 204: ((expand cond);((rewrite ...); 1: auto))
[goal> Focused goal (1/3):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: k:index
H: [happens(R1(k))]
IH: equiv(frame@pred(R1(k)))
----------------------------------------
0: frame@pred(R1(k))
1: exec@pred(R1(k)) &&
exists (i,j:index),
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k)
2: if (exec@pred(R1(k)) &&
exists (i,j:index),
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k))
then
try find i,j:index such that
(exec@pred(R1(k)) &&
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,j)))
fa 2; fadup 1. [> Line 205: ((fa 2);(fadup 1))
[goal> Focused goal (1/3):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: k:index
H: [happens(R1(k))]
IH: equiv(frame@pred(R1(k)))
----------------------------------------
0: frame@pred(R1(k))
1: try find i,j:index such that
(exec@pred(R1(k)) &&
T(i,j) < R1(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R1(k)) &&
fst(output@T(i,j)) = fst(input@R1(k)) && input@T(i,j) = output@R(k))
in h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,j)))
fa 1; fadup 1. [> Line 206: ((fa 1);(fadup 1))
[goal> Focused goal (1/3):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i,j,k:index
H: [happens(R1(k))]
IH: equiv(frame@pred(R1(k)))
----------------------------------------
0: frame@pred(R1(k))
1: h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,j)))
prf 1. [> Line 207: (prf 1)
[goal> Focused goal (1/3):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i,j,k:index
H: [happens(R1(k))]
IH: equiv(frame@pred(R1(k)))
----------------------------------------
0: frame@pred(R1(k))
1: if (true &&
diff(
forall (k0,i0:index),
R1(k0) < R1(k) =>
snd(input@R1(k0)) = h(<<nR(k0),fst(input@R1(k0))>,tag1>,key(i0)) &&
i = i0 =>
<<snd(input@R1(k)),nR(k)>,tag2> <>
<<snd(input@R1(k0)),nR(k0)>,tag2>,
forall (k0,i0,k1:index),
R1(k0) < R1(k) =>
snd(input@R1(k0)) =
h(<<nR(k0),fst(input@R1(k0))>,tag1>,key'(i0,k1)) &&
i = i0 && j = k1 =>
<<snd(input@R1(k)),nR(k)>,tag2> <>
<<snd(input@R1(k0)),nR(k0)>,tag2>) &&
diff(
(forall (k0,i0:index),
R1(k0) < R1(k) =>
i = i0 =>
<<snd(input@R1(k)),nR(k)>,tag2> <>
<<nR(k0),fst(input@R1(k0))>,tag1>) &&
(forall (k0,i0:index),
R2(k0) < R1(k) =>
i = i0 =>
<<snd(input@R1(k)),nR(k)>,tag2> <>
<<nR(k0),fst(input@R2(k0))>,tag1>) &&
forall (i0,j0:index),
T(i0,j0) < R1(k) =>
i = i0 =>
<<snd(input@R1(k)),nR(k)>,tag2> <>
<<input@T(i0,j0),nT(i0,j0)>,tag1>,
(forall (k0,i0,k1:index),
R1(k0) < R1(k) =>
i = i0 && j = k1 =>
<<snd(input@R1(k)),nR(k)>,tag2> <>
<<nR(k0),fst(input@R1(k0))>,tag1>) &&
(forall (k0,i0,k1:index),
R2(k0) < R1(k) =>
i = i0 && j = k1 =>
<<snd(input@R1(k)),nR(k)>,tag2> <>
<<nR(k0),fst(input@R2(k0))>,tag1>) &&
forall (i0,j0:index),
T(i0,j0) < R1(k) =>
i = i0 && j = j0 =>
<<snd(input@R1(k)),nR(k)>,tag2> <>
<<input@T(i0,j0),nT(i0,j0)>,tag1>)) then n_PRF
else h(<<snd(input@R1(k)),nR(k)>,tag2>,diff(key(i), key'(i,j)))
rewrite if_true. [> Line 208: (rewrite ...)
[goal> Focused goal (1/4):
System: left:default/left, right:default/right (same for equivalences)
Variables: i,j,k:index
H: [happens(R1(k))]
IH: equiv(frame@pred(R1(k)))
----------------------------------------
true &&
diff(
forall (k0,i0:index),
R1(k0) < R1(k) =>
snd(input@R1(k0)) = h(<<nR(k0),fst(input@R1(k0))>,tag1>,key(i0)) &&
i = i0 =>
<<snd(input@R1(k)),nR(k)>,tag2> <> <<snd(input@R1(k0)),nR(k0)>,tag2>,
forall (k0,i0,k1:index),
R1(k0) < R1(k) =>
snd(input@R1(k0)) = h(<<nR(k0),fst(input@R1(k0))>,tag1>,key'(i0,k1)) &&
i = i0 && j = k1 =>
<<snd(input@R1(k)),nR(k)>,tag2> <> <<snd(input@R1(k0)),nR(k0)>,tag2>) &&
diff(
(forall (k0,i0:index),
R1(k0) < R1(k) =>
i = i0 =>
<<snd(input@R1(k)),nR(k)>,tag2> <> <<nR(k0),fst(input@R1(k0))>,tag1>) &&
(forall (k0,i0:index),
R2(k0) < R1(k) =>
i = i0 =>
<<snd(input@R1(k)),nR(k)>,tag2> <> <<nR(k0),fst(input@R2(k0))>,tag1>) &&
forall (i0,j0:index),
T(i0,j0) < R1(k) =>
i = i0 =>
<<snd(input@R1(k)),nR(k)>,tag2> <> <<input@T(i0,j0),nT(i0,j0)>,tag1>,
(forall (k0,i0,k1:index),
R1(k0) < R1(k) =>
i = i0 && j = k1 =>
<<snd(input@R1(k)),nR(k)>,tag2> <> <<nR(k0),fst(input@R1(k0))>,tag1>) &&
(forall (k0,i0,k1:index),
R2(k0) < R1(k) =>
i = i0 && j = k1 =>
<<snd(input@R1(k)),nR(k)>,tag2> <> <<nR(k0),fst(input@R2(k0))>,tag1>) &&
forall (i0,j0:index),
T(i0,j0) < R1(k) =>
i = i0 && j = j0 =>
<<snd(input@R1(k)),nR(k)>,tag2> <> <<input@T(i0,j0),nT(i0,j0)>,tag1>)
by use tags_neq; project. [> Line 209: by ((have ... as );project)
[goal> Focused goal (1/3):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i,j,k:index
H: [happens(R1(k))]
IH: equiv(frame@pred(R1(k)))
----------------------------------------
0: frame@pred(R1(k))
1: n_PRF
by fresh 1. [> Line 210: by (fresh 1)
[goal> Focused goal (1/2):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: k:index
H: [happens(R2(k))]
IH: equiv(frame@pred(R2(k)))
----------------------------------------
0: frame@R2(k)

(* Case R2 *)
+ expand frame, exec, output. [> Line 213: (expand frame, exec, output)
[goal> Focused goal (1/2):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: k:index
H: [happens(R2(k))]
IH: equiv(frame@pred(R2(k)))
----------------------------------------
0: <frame@pred(R2(k)),
<of_bool(exec@pred(R2(k)) && cond@R2(k)),
if (exec@pred(R2(k)) && cond@R2(k)) then ko>>
fa !<_,_>. [> Line 214: (fa !pair(_,_))
[goal> Focused goal (1/2):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: k:index
H: [happens(R2(k))]
IH: equiv(frame@pred(R2(k)))
----------------------------------------
0: frame@pred(R2(k))
1: exec@pred(R2(k)) && cond@R2(k)
expand cond; rewrite wa_R1_R2; 1: auto. [> Line 215: ((expand cond);((rewrite ...); 1: auto))
[goal> Focused goal (1/2):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: k:index
H: [happens(R2(k))]
IH: equiv(frame@pred(R2(k)))
----------------------------------------
0: frame@pred(R2(k))
1: exec@pred(R2(k)) &&
not(exists (i,j:index),
T(i,j) < R2(k) &&
R(k) < T(i,j) &&
snd(output@T(i,j)) = snd(input@R2(k)) &&
fst(output@T(i,j)) = fst(input@R2(k)) && input@T(i,j) = output@R(k))
by fadup 1. [> Line 216: by (fadup 1)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i,j:index
H: [happens(T(i,j))]
IH: equiv(frame@pred(T(i,j)))
----------------------------------------
0: frame@T(i,j)

(* Case T *)
+ expand frame, exec, cond, output. [> Line 219: (expand frame, exec, cond, output)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i,j:index
H: [happens(T(i,j))]
IH: equiv(frame@pred(T(i,j)))
----------------------------------------
0: <frame@pred(T(i,j)),
<of_bool(exec@pred(T(i,j)) && true),
if (exec@pred(T(i,j)) && true) then <nT(i,j),m2(i,j)@T(i,j)>>>
expand m2(i,j)@T(i,j). [> Line 220: (expand m2(i,j)@T(i,j))
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i,j:index
H: [happens(T(i,j))]
IH: equiv(frame@pred(T(i,j)))
----------------------------------------
0: <frame@pred(T(i,j)),
<of_bool(exec@pred(T(i,j)) && true),
if (exec@pred(T(i,j)) && true) then
<nT(i,j),h(<<input@T(i,j),nT(i,j)>,tag1>,diff(key(i), key'(i,j)))>>>
fa !<_,_>, if _ then _, <_,_>. [> Line 221: (fa !pair(_,_) if _ then _ else zero pair(_,_))
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i,j:index
H: [happens(T(i,j))]
IH: equiv(frame@pred(T(i,j)))
----------------------------------------
0: frame@pred(T(i,j))
1: nT(i,j)
2: h(<<input@T(i,j),nT(i,j)>,tag1>,diff(key(i), key'(i,j)))
prf 2. [> Line 222: (prf 2)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i,j:index
H: [happens(T(i,j))]
IH: equiv(frame@pred(T(i,j)))
----------------------------------------
0: frame@pred(T(i,j))
1: nT(i,j)
2: if (true &&
diff(
forall (k,i0:index),
R1(k) < T(i,j) =>
snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key(i0)) &&
i = i0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<snd(input@R1(k)),nR(k)>,tag2>,
forall (k,i0,k0:index),
R1(k) < T(i,j) =>
snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key'(i0,k0)) &&
i = i0 && j = k0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<snd(input@R1(k)),nR(k)>,tag2>) &&
diff(
(forall (k,i0:index),
R1(k) < T(i,j) =>
i = i0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<nR(k),fst(input@R1(k))>,tag1>) &&
(forall (k,i0:index),
R2(k) < T(i,j) =>
i = i0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<nR(k),fst(input@R2(k))>,tag1>) &&
forall (i0,j0:index),
T(i0,j0) < T(i,j) =>
i = i0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<input@T(i0,j0),nT(i0,j0)>,tag1>,
(forall (k,i0,k0:index),
R1(k) < T(i,j) =>
i = i0 && j = k0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<nR(k),fst(input@R1(k))>,tag1>) &&
(forall (k,i0,k0:index),
R2(k) < T(i,j) =>
i = i0 && j = k0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<nR(k),fst(input@R2(k))>,tag1>) &&
forall (i0,j0:index),
T(i0,j0) < T(i,j) =>
i = i0 && j = j0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<input@T(i0,j0),nT(i0,j0)>,tag1>))
then n_PRF
else h(<<input@T(i,j),nT(i,j)>,tag1>,diff(key(i), key'(i,j)))
rewrite if_true. [> Line 223: (rewrite ...)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right (same for equivalences)
Variables: i,j:index
H: [happens(T(i,j))]
IH: equiv(frame@pred(T(i,j)))
----------------------------------------
true &&
diff(
forall (k,i0:index),
R1(k) < T(i,j) =>
snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key(i0)) && i = i0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<snd(input@R1(k)),nR(k)>,tag2>,
forall (k,i0,k0:index),
R1(k) < T(i,j) =>
snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key'(i0,k0)) &&
i = i0 && j = k0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<snd(input@R1(k)),nR(k)>,tag2>) &&
diff(
(forall (k,i0:index),
R1(k) < T(i,j) =>
i = i0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<nR(k),fst(input@R1(k))>,tag1>) &&
(forall (k,i0:index),
R2(k) < T(i,j) =>
i = i0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<nR(k),fst(input@R2(k))>,tag1>) &&
forall (i0,j0:index),
T(i0,j0) < T(i,j) =>
i = i0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<input@T(i0,j0),nT(i0,j0)>,tag1>,
(forall (k,i0,k0:index),
R1(k) < T(i,j) =>
i = i0 && j = k0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<nR(k),fst(input@R1(k))>,tag1>) &&
(forall (k,i0,k0:index),
R2(k) < T(i,j) =>
i = i0 && j = k0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<nR(k),fst(input@R2(k))>,tag1>) &&
forall (i0,j0:index),
T(i0,j0) < T(i,j) =>
i = i0 && j = j0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<input@T(i0,j0),nT(i0,j0)>,tag1>)

 {
simpl. [> Line 224: simpl
[goal> Focused goal (1/2):
System: left:default/left, right:default/right (same for equivalences)
Variables: i,j:index
H: [happens(T(i,j))]
IH: equiv(frame@pred(T(i,j)))
----------------------------------------
diff(
forall (k,i0:index),
R1(k) < T(i,j) =>
snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key(i0)) && i = i0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<snd(input@R1(k)),nR(k)>,tag2>,
forall (k,i0,k0:index),
R1(k) < T(i,j) =>
snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key'(i0,k0)) &&
i = i0 && j = k0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<snd(input@R1(k)),nR(k)>,tag2>) &&
diff(
(forall (k,i0:index),
R1(k) < T(i,j) =>
i = i0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<nR(k),fst(input@R1(k))>,tag1>) &&
(forall (k,i0:index),
R2(k) < T(i,j) =>
i = i0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<nR(k),fst(input@R2(k))>,tag1>) &&
forall (i0,j0:index),
T(i0,j0) < T(i,j) =>
i = i0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<input@T(i0,j0),nT(i0,j0)>,tag1>,
(forall (k,i0,k0:index),
R1(k) < T(i,j) =>
i = i0 && j = k0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<nR(k),fst(input@R1(k))>,tag1>) &&
(forall (k,i0,k0:index),
R2(k) < T(i,j) =>
i = i0 && j = k0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<nR(k),fst(input@R2(k))>,tag1>) &&
forall (i0,j0:index),
T(i0,j0) < T(i,j) =>
i = i0 && j = j0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<input@T(i0,j0),nT(i0,j0)>,tag1>)
use tags_neq. [> Line 225: (have ... as )
[goal> Focused goal (1/2):
System: left:default/left, right:default/right (same for equivalences)
Variables: i,j:index
H: [happens(T(i,j))]
IH: equiv(frame@pred(T(i,j)))
Mneq: tag1 <> tag2
----------------------------------------
diff(
forall (k,i0:index),
R1(k) < T(i,j) =>
snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key(i0)) && i = i0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<snd(input@R1(k)),nR(k)>,tag2>,
forall (k,i0,k0:index),
R1(k) < T(i,j) =>
snd(input@R1(k)) = h(<<nR(k),fst(input@R1(k))>,tag1>,key'(i0,k0)) &&
i = i0 && j = k0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<snd(input@R1(k)),nR(k)>,tag2>) &&
diff(
(forall (k,i0:index),
R1(k) < T(i,j) =>
i = i0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<nR(k),fst(input@R1(k))>,tag1>) &&
(forall (k,i0:index),
R2(k) < T(i,j) =>
i = i0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<nR(k),fst(input@R2(k))>,tag1>) &&
forall (i0,j0:index),
T(i0,j0) < T(i,j) =>
i = i0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<input@T(i0,j0),nT(i0,j0)>,tag1>,
(forall (k,i0,k0:index),
R1(k) < T(i,j) =>
i = i0 && j = k0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<nR(k),fst(input@R1(k))>,tag1>) &&
(forall (k,i0,k0:index),
R2(k) < T(i,j) =>
i = i0 && j = k0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<nR(k),fst(input@R2(k))>,tag1>) &&
forall (i0,j0:index),
T(i0,j0) < T(i,j) =>
i = i0 && j = j0 =>
<<input@T(i,j),nT(i,j)>,tag1> <> <<input@T(i0,j0),nT(i0,j0)>,tag1>)
by project; repeat split; intro > _ _ [[_ Meq] _]; fresh Meq. [> Line 226: by (project;
((repeat split);((intro > _ _ [[_ Meq] _]);(fresh Meq))))

[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i,j:index
H: [happens(T(i,j))]
IH: equiv(frame@pred(T(i,j)))
----------------------------------------
0: frame@pred(T(i,j))
1: nT(i,j)
2: n_PRF
}
fresh 2. [> Line 228: (fresh 2)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i,j:index
H: [happens(T(i,j))]
IH: equiv(frame@pred(T(i,j)))
----------------------------------------
0: frame@pred(T(i,j))
1: nT(i,j)
by fresh 1; rewrite if_true. [> Line 229: by ((fresh 1);(rewrite ...))
[goal> Goal unlinkability is proved

Qed. Exiting proof mode.

Squirrel Prover

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: