[STATEMENT]
lemma transfer_val2:
  assumes "transfer ads addr val acc = Some acc'"
      and "ads \<noteq> addr"
    shows "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc addr) + ReadL\<^sub>i\<^sub>n\<^sub>t val < 2^256"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>accessBalance acc addr\<rceil> + \<lceil>val\<rceil> < 2 ^ 256
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lceil>accessBalance acc addr\<rceil> + \<lceil>val\<rceil> < 2 ^ 256
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
transfer ads addr val acc = Some acc'
[PROOF STEP]
obtain acc''
    where *: "subBalance ads val acc = Some acc''"
      and **: "addBalance addr val acc'' = Some acc'"
[PROOF STATE]
proof (prove)
using this:
transfer ads addr val acc = Some acc'

goal (1 subgoal):
 1. (\<And>acc''. \<lbrakk>subBalance ads val acc = Some acc''; addBalance addr val acc'' = Some acc'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp split:if_split_asm)
[PROOF STATE]
proof (state)
this:
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'

goal (1 subgoal):
 1. \<lceil>accessBalance acc addr\<rceil> + \<lceil>val\<rceil> < 2 ^ 256
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'
[PROOF STEP]
have "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc'' addr) + ReadL\<^sub>i\<^sub>n\<^sub>t val < 2^256"
[PROOF STATE]
proof (prove)
using this:
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'

goal (1 subgoal):
 1. \<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil> < 2 ^ 256
[PROOF STEP]
using addBalance_val[OF **]
[PROOF STATE]
proof (prove)
using this:
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'
\<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil> < 2 ^ 256

goal (1 subgoal):
 1. \<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil> < 2 ^ 256
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil> < 2 ^ 256

goal (1 subgoal):
 1. \<lceil>accessBalance acc addr\<rceil> + \<lceil>val\<rceil> < 2 ^ 256
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
subBalance ads val acc = Some acc''
\<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil> < 2 ^ 256
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
subBalance ads val acc = Some acc''
\<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil> < 2 ^ 256

goal (1 subgoal):
 1. \<lceil>accessBalance acc addr\<rceil> + \<lceil>val\<rceil> < 2 ^ 256
[PROOF STEP]
using assms(2) subBalance_eq[OF *]
[PROOF STATE]
proof (prove)
using this:
subBalance ads val acc = Some acc''
\<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil> < 2 ^ 256
ads \<noteq> addr
ads \<noteq> ?ad' \<Longrightarrow> accessBalance acc ?ad' = accessBalance acc'' ?ad'

goal (1 subgoal):
 1. \<lceil>accessBalance acc addr\<rceil> + \<lceil>val\<rceil> < 2 ^ 256
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc addr\<rceil> + \<lceil>val\<rceil> < 2 ^ 256

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma transfer_add:
  assumes "transfer ads addr val acc = Some acc'"
      and "addr \<noteq> ads"
  shows "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' addr) = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc addr) + ReadL\<^sub>i\<^sub>n\<^sub>t val"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>accessBalance acc' addr\<rceil> = \<lceil>accessBalance acc addr\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lceil>accessBalance acc' addr\<rceil> = \<lceil>accessBalance acc addr\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
transfer ads addr val acc = Some acc'
[PROOF STEP]
obtain acc''
    where *: "subBalance ads val acc = Some acc''"
      and **: "addBalance addr val acc'' = Some acc'"
[PROOF STATE]
proof (prove)
using this:
transfer ads addr val acc = Some acc'

goal (1 subgoal):
 1. (\<And>acc''. \<lbrakk>subBalance ads val acc = Some acc''; addBalance addr val acc'' = Some acc'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp split:if_split_asm)
[PROOF STATE]
proof (state)
this:
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'

goal (1 subgoal):
 1. \<lceil>accessBalance acc' addr\<rceil> = \<lceil>accessBalance acc addr\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
addr \<noteq> ads
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'
[PROOF STEP]
have "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc addr) = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc'' addr)"
[PROOF STATE]
proof (prove)
using this:
addr \<noteq> ads
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'

goal (1 subgoal):
 1. \<lceil>accessBalance acc addr\<rceil> = \<lceil>accessBalance acc'' addr\<rceil>
[PROOF STEP]
using subBalance_eq[OF *]
[PROOF STATE]
proof (prove)
using this:
addr \<noteq> ads
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'
ads \<noteq> ?ad' \<Longrightarrow> accessBalance acc ?ad' = accessBalance acc'' ?ad'

goal (1 subgoal):
 1. \<lceil>accessBalance acc addr\<rceil> = \<lceil>accessBalance acc'' addr\<rceil>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc addr\<rceil> = \<lceil>accessBalance acc'' addr\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc' addr\<rceil> = \<lceil>accessBalance acc addr\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc addr\<rceil> = \<lceil>accessBalance acc'' addr\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc' addr\<rceil> = \<lceil>accessBalance acc addr\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
have "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' addr) = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc'' addr) + ReadL\<^sub>i\<^sub>n\<^sub>t val"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>accessBalance acc' addr\<rceil> = \<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
using addBalance_add[OF **]
[PROOF STATE]
proof (prove)
using this:
\<lceil>accessBalance acc' addr\<rceil> = \<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc' addr\<rceil> = \<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc' addr\<rceil> = \<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc' addr\<rceil> = \<lceil>accessBalance acc addr\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lceil>accessBalance acc addr\<rceil> = \<lceil>accessBalance acc'' addr\<rceil>
\<lceil>accessBalance acc' addr\<rceil> = \<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lceil>accessBalance acc addr\<rceil> = \<lceil>accessBalance acc'' addr\<rceil>
\<lceil>accessBalance acc' addr\<rceil> = \<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc' addr\<rceil> = \<lceil>accessBalance acc addr\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
using Read_ShowL_id
[PROOF STATE]
proof (prove)
using this:
\<lceil>accessBalance acc addr\<rceil> = \<lceil>accessBalance acc'' addr\<rceil>
\<lceil>accessBalance acc' addr\<rceil> = \<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil>
\<lceil>\<lfloor>?x\<rfloor>\<rceil> = ?x

goal (1 subgoal):
 1. \<lceil>accessBalance acc' addr\<rceil> = \<lceil>accessBalance acc addr\<rceil> + \<lceil>val\<rceil>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc' addr\<rceil> = \<lceil>accessBalance acc addr\<rceil> + \<lceil>val\<rceil>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma transfer_sub:
  assumes "transfer ads addr val acc = Some acc'"
      and "addr \<noteq> ads"
  shows "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ads) = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ads) - ReadL\<^sub>i\<^sub>n\<^sub>t val"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>accessBalance acc' ads\<rceil> = \<lceil>accessBalance acc ads\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lceil>accessBalance acc' ads\<rceil> = \<lceil>accessBalance acc ads\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
transfer ads addr val acc = Some acc'
[PROOF STEP]
obtain acc''
    where *: "subBalance ads val acc = Some acc''"
      and **: "addBalance addr val acc'' = Some acc'"
[PROOF STATE]
proof (prove)
using this:
transfer ads addr val acc = Some acc'

goal (1 subgoal):
 1. (\<And>acc''. \<lbrakk>subBalance ads val acc = Some acc''; addBalance addr val acc'' = Some acc'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp split:if_split_asm)
[PROOF STATE]
proof (state)
this:
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ads\<rceil> = \<lceil>accessBalance acc ads\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'
[PROOF STEP]
have "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc'' ads) = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ads) - ReadL\<^sub>i\<^sub>n\<^sub>t val"
[PROOF STATE]
proof (prove)
using this:
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'

goal (1 subgoal):
 1. \<lceil>accessBalance acc'' ads\<rceil> = \<lceil>accessBalance acc ads\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
using subBalance_sub[OF *]
[PROOF STATE]
proof (prove)
using this:
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'
\<lceil>accessBalance acc'' ads\<rceil> = \<lceil>accessBalance acc ads\<rceil> - \<lceil>val\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc'' ads\<rceil> = \<lceil>accessBalance acc ads\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc'' ads\<rceil> = \<lceil>accessBalance acc ads\<rceil> - \<lceil>val\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ads\<rceil> = \<lceil>accessBalance acc ads\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc'' ads\<rceil> = \<lceil>accessBalance acc ads\<rceil> - \<lceil>val\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ads\<rceil> = \<lceil>accessBalance acc ads\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
addr \<noteq> ads
[PROOF STEP]
have "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ads) = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc'' ads)"
[PROOF STATE]
proof (prove)
using this:
addr \<noteq> ads

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ads\<rceil> = \<lceil>accessBalance acc'' ads\<rceil>
[PROOF STEP]
using addBalance_eq[OF **]
[PROOF STATE]
proof (prove)
using this:
addr \<noteq> ads
addr \<noteq> ?ad' \<Longrightarrow> accessBalance acc'' ?ad' = accessBalance acc' ?ad'

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ads\<rceil> = \<lceil>accessBalance acc'' ads\<rceil>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc' ads\<rceil> = \<lceil>accessBalance acc'' ads\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ads\<rceil> = \<lceil>accessBalance acc ads\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lceil>accessBalance acc'' ads\<rceil> = \<lceil>accessBalance acc ads\<rceil> - \<lceil>val\<rceil>
\<lceil>accessBalance acc' ads\<rceil> = \<lceil>accessBalance acc'' ads\<rceil>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lceil>accessBalance acc'' ads\<rceil> = \<lceil>accessBalance acc ads\<rceil> - \<lceil>val\<rceil>
\<lceil>accessBalance acc' ads\<rceil> = \<lceil>accessBalance acc'' ads\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ads\<rceil> = \<lceil>accessBalance acc ads\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
using Read_ShowL_id
[PROOF STATE]
proof (prove)
using this:
\<lceil>accessBalance acc'' ads\<rceil> = \<lceil>accessBalance acc ads\<rceil> - \<lceil>val\<rceil>
\<lceil>accessBalance acc' ads\<rceil> = \<lceil>accessBalance acc'' ads\<rceil>
\<lceil>\<lfloor>?x\<rfloor>\<rceil> = ?x

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ads\<rceil> = \<lceil>accessBalance acc ads\<rceil> - \<lceil>val\<rceil>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc' ads\<rceil> = \<lceil>accessBalance acc ads\<rceil> - \<lceil>val\<rceil>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma transfer_mono:
  assumes "transfer ads addr val acc = Some acc'"
  shows "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' addr) \<ge> ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc addr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
transfer ads addr val acc = Some acc'
[PROOF STEP]
obtain acc''
    where *: "subBalance ads val acc = Some acc''"
      and **: "addBalance addr val acc'' = Some acc'"
[PROOF STATE]
proof (prove)
using this:
transfer ads addr val acc = Some acc'

goal (1 subgoal):
 1. (\<And>acc''. \<lbrakk>subBalance ads val acc = Some acc''; addBalance addr val acc'' = Some acc'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp split:if_split_asm)
[PROOF STATE]
proof (state)
this:
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'

goal (1 subgoal):
 1. \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
proof (cases "addr = ads")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. addr = ads \<Longrightarrow> \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
 2. addr \<noteq> ads \<Longrightarrow> \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
addr = ads

goal (2 subgoals):
 1. addr = ads \<Longrightarrow> \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
 2. addr \<noteq> ads \<Longrightarrow> \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
subBalance ads val acc = Some acc''
addr = ads
[PROOF STEP]
have "acc'' = updateBalance addr (ShowL\<^sub>i\<^sub>n\<^sub>t (ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc addr) - ReadL\<^sub>i\<^sub>n\<^sub>t val)) acc"
[PROOF STATE]
proof (prove)
using this:
subBalance ads val acc = Some acc''
addr = ads

goal (1 subgoal):
 1. acc'' = updateBalance addr \<lfloor>\<lceil>accessBalance acc addr\<rceil> - \<lceil>val\<rceil>\<rfloor> acc
[PROOF STEP]
by (simp add:Let_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
acc'' = updateBalance addr \<lfloor>\<lceil>accessBalance acc addr\<rceil> - \<lceil>val\<rceil>\<rfloor> acc

goal (2 subgoals):
 1. addr = ads \<Longrightarrow> \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
 2. addr \<noteq> ads \<Longrightarrow> \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
acc'' = updateBalance addr \<lfloor>\<lceil>accessBalance acc addr\<rceil> - \<lceil>val\<rceil>\<rfloor> acc

goal (2 subgoals):
 1. addr = ads \<Longrightarrow> \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
 2. addr \<noteq> ads \<Longrightarrow> \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
from **
[PROOF STATE]
proof (chain)
picking this:
addBalance addr val acc'' = Some acc'
[PROOF STEP]
have "acc'=updateBalance addr (ShowL\<^sub>i\<^sub>n\<^sub>t (ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc'' addr) + ReadL\<^sub>i\<^sub>n\<^sub>t val)) acc''"
[PROOF STATE]
proof (prove)
using this:
addBalance addr val acc'' = Some acc'

goal (1 subgoal):
 1. acc' = updateBalance addr \<lfloor>\<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil>\<rfloor> acc''
[PROOF STEP]
by (simp add:Let_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
acc' = updateBalance addr \<lfloor>\<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil>\<rfloor> acc''

goal (2 subgoals):
 1. addr = ads \<Longrightarrow> \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
 2. addr \<noteq> ads \<Longrightarrow> \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
acc'' = updateBalance addr \<lfloor>\<lceil>accessBalance acc addr\<rceil> - \<lceil>val\<rceil>\<rfloor> acc
acc' = updateBalance addr \<lfloor>\<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil>\<rfloor> acc''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
acc'' = updateBalance addr \<lfloor>\<lceil>accessBalance acc addr\<rceil> - \<lceil>val\<rceil>\<rfloor> acc
acc' = updateBalance addr \<lfloor>\<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil>\<rfloor> acc''

goal (1 subgoal):
 1. \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
using Read_ShowL_id
[PROOF STATE]
proof (prove)
using this:
acc'' = updateBalance addr \<lfloor>\<lceil>accessBalance acc addr\<rceil> - \<lceil>val\<rceil>\<rfloor> acc
acc' = updateBalance addr \<lfloor>\<lceil>accessBalance acc'' addr\<rceil> + \<lceil>val\<rceil>\<rfloor> acc''
\<lceil>\<lfloor>?x\<rfloor>\<rceil> = ?x

goal (1 subgoal):
 1. \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>

goal (1 subgoal):
 1. addr \<noteq> ads \<Longrightarrow> \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. addr \<noteq> ads \<Longrightarrow> \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
addr \<noteq> ads

goal (1 subgoal):
 1. addr \<noteq> ads \<Longrightarrow> \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
addr \<noteq> ads
[PROOF STEP]
have "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc addr) \<le> ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc'' addr)"
[PROOF STATE]
proof (prove)
using this:
addr \<noteq> ads

goal (1 subgoal):
 1. \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc'' addr\<rceil>
[PROOF STEP]
using subBalance_eq[OF *]
[PROOF STATE]
proof (prove)
using this:
addr \<noteq> ads
ads \<noteq> ?ad' \<Longrightarrow> accessBalance acc ?ad' = accessBalance acc'' ?ad'

goal (1 subgoal):
 1. \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc'' addr\<rceil>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc'' addr\<rceil>

goal (1 subgoal):
 1. addr \<noteq> ads \<Longrightarrow> \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc'' addr\<rceil>

goal (1 subgoal):
 1. addr \<noteq> ads \<Longrightarrow> \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
have "\<dots> \<le> ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' addr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>accessBalance acc'' addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
using addBalance_mono[OF **]
[PROOF STATE]
proof (prove)
using this:
\<lceil>accessBalance acc'' addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc'' addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc'' addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>

goal (1 subgoal):
 1. addr \<noteq> ads \<Longrightarrow> \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc addr\<rceil> \<le> \<lceil>accessBalance acc' addr\<rceil>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma transfer_eq:
  assumes "transfer ads addr val acc = Some acc'"
      and "ad \<noteq> ads"
      and "ad \<noteq> addr"
  shows "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ad) = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
transfer ads addr val acc = Some acc'
[PROOF STEP]
obtain acc''
    where *: "subBalance ads val acc = Some acc''"
      and **: "addBalance addr val acc'' = Some acc'"
[PROOF STATE]
proof (prove)
using this:
transfer ads addr val acc = Some acc'

goal (1 subgoal):
 1. (\<And>acc''. \<lbrakk>subBalance ads val acc = Some acc''; addBalance addr val acc'' = Some acc'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp split:if_split_asm)
[PROOF STATE]
proof (state)
this:
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil>
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
ad \<noteq> addr
[PROOF STEP]
have "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ad) = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc'' ad)"
[PROOF STATE]
proof (prove)
using this:
ad \<noteq> addr

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc'' ad\<rceil>
[PROOF STEP]
using addBalance_eq[OF **]
[PROOF STATE]
proof (prove)
using this:
ad \<noteq> addr
addr \<noteq> ?ad' \<Longrightarrow> accessBalance acc'' ?ad' = accessBalance acc' ?ad'

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc'' ad\<rceil>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc'' ad\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc'' ad\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
ad \<noteq> ads
[PROOF STEP]
have "\<dots> = ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad)"
[PROOF STATE]
proof (prove)
using this:
ad \<noteq> ads

goal (1 subgoal):
 1. \<lceil>accessBalance acc'' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil>
[PROOF STEP]
using subBalance_eq[OF *]
[PROOF STATE]
proof (prove)
using this:
ad \<noteq> ads
ads \<noteq> ?ad' \<Longrightarrow> accessBalance acc ?ad' = accessBalance acc'' ?ad'

goal (1 subgoal):
 1. \<lceil>accessBalance acc'' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc'' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil>

goal (1 subgoal):
 1. \<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<lceil>accessBalance acc' ad\<rceil> = \<lceil>accessBalance acc ad\<rceil>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma transfer_limit:
  assumes "transfer ads addr val acc = Some acc'"
     and "\<forall>ad. ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad) \<ge> 0 \<and> ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc ad) < 2 ^ 256"
   shows "\<forall>ad. ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ad) \<ge> 0 \<and> ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ad) < 2 ^ 256"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ad. 0 \<le> \<lceil>accessBalance acc' ad\<rceil> \<and> \<lceil>accessBalance acc' ad\<rceil> < 2 ^ 256
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ad. 0 \<le> \<lceil>accessBalance acc' ad\<rceil> \<and> \<lceil>accessBalance acc' ad\<rceil> < 2 ^ 256
[PROOF STEP]
fix ad'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ad. 0 \<le> \<lceil>accessBalance acc' ad\<rceil> \<and> \<lceil>accessBalance acc' ad\<rceil> < 2 ^ 256
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
transfer ads addr val acc = Some acc'
[PROOF STEP]
obtain acc'' where "subBalance ads val acc = Some acc''" and "addBalance addr val acc'' = Some acc'"
[PROOF STATE]
proof (prove)
using this:
transfer ads addr val acc = Some acc'

goal (1 subgoal):
 1. (\<And>acc''. \<lbrakk>subBalance ads val acc = Some acc''; addBalance addr val acc'' = Some acc'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp split: if_split_asm)
[PROOF STATE]
proof (state)
this:
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'

goal (1 subgoal):
 1. \<And>ad. 0 \<le> \<lceil>accessBalance acc' ad\<rceil> \<and> \<lceil>accessBalance acc' ad\<rceil> < 2 ^ 256
[PROOF STEP]
with subBalance_limit[OF _ assms(2)]
[PROOF STATE]
proof (chain)
picking this:
subBalance ?ad ?val acc = Some ?acc' \<Longrightarrow> \<forall>ad. 0 \<le> \<lceil>accessBalance ?acc' ad\<rceil> \<and> \<lceil>accessBalance ?acc' ad\<rceil> < 2 ^ 256
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'
[PROOF STEP]
show "ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ad') \<ge> 0 \<and> ReadL\<^sub>i\<^sub>n\<^sub>t (accessBalance acc' ad') < 2 ^ 256"
[PROOF STATE]
proof (prove)
using this:
subBalance ?ad ?val acc = Some ?acc' \<Longrightarrow> \<forall>ad. 0 \<le> \<lceil>accessBalance ?acc' ad\<rceil> \<and> \<lceil>accessBalance ?acc' ad\<rceil> < 2 ^ 256
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'

goal (1 subgoal):
 1. 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
using addBalance_limit
[PROOF STATE]
proof (prove)
using this:
subBalance ?ad ?val acc = Some ?acc' \<Longrightarrow> \<forall>ad. 0 \<le> \<lceil>accessBalance ?acc' ad\<rceil> \<and> \<lceil>accessBalance ?acc' ad\<rceil> < 2 ^ 256
subBalance ads val acc = Some acc''
addBalance addr val acc'' = Some acc'
\<lbrakk>addBalance ?ad ?val ?acc = Some ?acc'; \<forall>ad. 0 \<le> \<lceil>accessBalance ?acc ad\<rceil> \<and> \<lceil>accessBalance ?acc ad\<rceil> < 2 ^ 256\<rbrakk> \<Longrightarrow> \<forall>ad. 0 \<le> \<lceil>accessBalance ?acc' ad\<rceil> \<and> \<lceil>accessBalance ?acc' ad\<rceil> < 2 ^ 256

goal (1 subgoal):
 1. 0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
0 \<le> \<lceil>accessBalance acc' ad'\<rceil> \<and> \<lceil>accessBalance acc' ad'\<rceil> < 2 ^ 256

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_before_rel_on_elems: "list_before_rel l \<subseteq> set l \<times> set l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_before_rel l \<subseteq> set l \<times> set l
[PROOF STEP]
unfolding list_before_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(a, b). \<exists>l1 l2 l3. l = l1 @ a # l2 @ b # l3} \<subseteq> set l \<times> set l
[PROOF STEP]
by auto


[STATEMENT]
lemma list_before_irrefl_eq_distinct: "irrefl (list_before_rel l) \<longleftrightarrow> distinct l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irrefl (list_before_rel l) = distinct l
[PROOF STEP]
using not_distinct_decomp[of l]
[PROOF STATE]
proof (prove)
using this:
\<not> distinct l \<Longrightarrow> \<exists>xs ys zs y. l = xs @ [y] @ ys @ [y] @ zs

goal (1 subgoal):
 1. irrefl (list_before_rel l) = distinct l
[PROOF STEP]
by (auto simp: irrefl_def list_before_rel_def)


[STATEMENT]
lemma list_before_rel_alt: "list_before_rel l = { (l!i, l!j) | i j. i<j \<and> j<length l }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_before_rel l = {(l ! i, l ! j) |i j. i < j \<and> j < length l}
[PROOF STEP]
unfolding list_before_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(a, b). \<exists>l1 l2 l3. l = l1 @ a # l2 @ b # l3} = {(l ! i, l ! j) |i j. i < j \<and> j < length l}
[PROOF STEP]
apply (rule; clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b l1 l2 l3. l = l1 @ a # l2 @ b # l3 \<Longrightarrow> \<exists>i. a = (l1 @ a # l2 @ b # l3) ! i \<and> (\<exists>j. b = (l1 @ a # l2 @ b # l3) ! j \<and> i < j \<and> j < Suc (Suc (length l1 + (length l2 + length l3))))
 2. \<And>i j. \<lbrakk>i < j; j < length l\<rbrakk> \<Longrightarrow> \<exists>l1 l2 l3. l = l1 @ l ! i # l2 @ l ! j # l3
[PROOF STEP]
subgoal for a b l1 l2 l3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l = l1 @ a # l2 @ b # l3 \<Longrightarrow> \<exists>i. a = (l1 @ a # l2 @ b # l3) ! i \<and> (\<exists>j. b = (l1 @ a # l2 @ b # l3) ! j \<and> i < j \<and> j < Suc (Suc (length l1 + (length l2 + length l3))))
[PROOF STEP]
apply (rule exI[of _ "length l1"]; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l = l1 @ a # l2 @ b # l3 \<Longrightarrow> \<exists>j. b = (l1 @ a # l2 @ b # l3) ! j \<and> length l1 < j \<and> j < Suc (Suc (length l1 + (length l2 + length l3)))
[PROOF STEP]
apply (rule exI[of _ "length l1 + Suc (length l2)"]; auto simp: nth_append)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < j; j < length l\<rbrakk> \<Longrightarrow> \<exists>l1 l2 l3. l = l1 @ l ! i # l2 @ l ! j # l3
[PROOF STEP]
subgoal for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < j; j < length l\<rbrakk> \<Longrightarrow> \<exists>l1 l2 l3. l = l1 @ l ! i # l2 @ l ! j # l3
[PROOF STEP]
apply (rule exI[of _ "take i l"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < j; j < length l\<rbrakk> \<Longrightarrow> \<exists>l2 l3. l = take i l @ l ! i # l2 @ l ! j # l3
[PROOF STEP]
apply (rule exI[of _ "drop (Suc i) (take j l)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < j; j < length l\<rbrakk> \<Longrightarrow> \<exists>l3. l = take i l @ l ! i # drop (Suc i) (take j l) @ l ! j # l3
[PROOF STEP]
apply (rule exI[of _ "drop (Suc j) l"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < j; j < length l\<rbrakk> \<Longrightarrow> l = take i l @ l ! i # drop (Suc i) (take j l) @ l ! j # drop (Suc j) l
[PROOF STEP]
by (simp add: Cons_nth_drop_Suc drop_take_drop_unsplit)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_before_trans[trans]: "distinct l \<Longrightarrow> trans (list_before_rel l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct l \<Longrightarrow> trans (list_before_rel l)
[PROOF STEP]
by (clarsimp simp: trans_def list_before_rel_alt) (metis index_nth_id less_trans)


[STATEMENT]
lemma list_before_asym: "distinct l \<Longrightarrow> asym (list_before_rel l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct l \<Longrightarrow> asym (list_before_rel l)
[PROOF STEP]
by (meson asym.intros irrefl_def list_before_irrefl_eq_distinct list_before_trans transE)


[STATEMENT]
lemma list_before_rel_empty[simp]: "list_before_rel [] = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_before_rel [] = {}
[PROOF STEP]
unfolding list_before_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(a, b). \<exists>l1 l2 l3. [] = l1 @ a # l2 @ b # l3} = {}
[PROOF STEP]
by auto


[STATEMENT]
lemma list_before_rel_cons: "list_before_rel (x#l) = ({x}\<times>set l) \<union> list_before_rel l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_before_rel (x # l) = {x} \<times> set l \<union> list_before_rel l
[PROOF STEP]
apply (intro equalityI subsetI; simp add: split_paired_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> list_before_rel (x # l) \<Longrightarrow> a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l
 2. \<And>a b. a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l \<Longrightarrow> (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
subgoal for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l) \<Longrightarrow> a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l) \<Longrightarrow> a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l
[PROOF STEP]
assume "(a,b) \<in> list_before_rel (x # l)"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> list_before_rel (x # l)

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l) \<Longrightarrow> a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
obtain i j where IDX_BOUND: "i<j" "j<Suc (length l)" and [simp]: "a=(x#l)!i" "b=(x#l)!j"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> list_before_rel (x # l)

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>i < j; j < Suc (length l); a = (x # l) ! i; b = (x # l) ! j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding list_before_rel_alt
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> {((x # l) ! i, (x # l) ! j) |i j. i < j \<and> j < length (x # l)}

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>i < j; j < Suc (length l); a = (x # l) ! i; b = (x # l) ! j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < j
j < Suc (length l)
a = (x # l) ! i
b = (x # l) ! j

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l) \<Longrightarrow> a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
i < j
j < Suc (length l)
a = (x # l) ! i
b = (x # l) ! j

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l) \<Longrightarrow> a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l
[PROOF STEP]
assume "i=0"
[PROOF STATE]
proof (state)
this:
i = 0

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l) \<Longrightarrow> a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l
[PROOF STEP]
hence "x=a" "b\<in>set l"
[PROOF STATE]
proof (prove)
using this:
i = 0

goal (1 subgoal):
 1. x = a &&& b \<in> set l
[PROOF STEP]
using IDX_BOUND
[PROOF STATE]
proof (prove)
using this:
i = 0
i < j
j < Suc (length l)

goal (1 subgoal):
 1. x = a &&& b \<in> set l
[PROOF STEP]
by (auto simp: nth_Cons split: nat.splits)
[PROOF STATE]
proof (state)
this:
x = a
b \<in> set l

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l) \<Longrightarrow> a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
i = 0 \<Longrightarrow> x = a
i = 0 \<Longrightarrow> b \<in> set l

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l) \<Longrightarrow> a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i = 0 \<Longrightarrow> x = a
i = 0 \<Longrightarrow> b \<in> set l

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l) \<Longrightarrow> a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
i = 0 \<Longrightarrow> x = a
i = 0 \<Longrightarrow> b \<in> set l

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l) \<Longrightarrow> a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l
[PROOF STEP]
assume "i\<noteq>0"
[PROOF STATE]
proof (state)
this:
i \<noteq> 0

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l) \<Longrightarrow> a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l
[PROOF STEP]
with IDX_BOUND
[PROOF STATE]
proof (chain)
picking this:
i < j
j < Suc (length l)
i \<noteq> 0
[PROOF STEP]
have "a=l!(i-1)" "b=l!(j-1)" "i-1 < j-1" "j-1 < length l"
[PROOF STATE]
proof (prove)
using this:
i < j
j < Suc (length l)
i \<noteq> 0

goal (1 subgoal):
 1. (a = l ! (i - 1) &&& b = l ! (j - 1)) &&& i - 1 < j - 1 &&& j - 1 < length l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = l ! (i - 1)
b = l ! (j - 1)
i - 1 < j - 1
j - 1 < length l

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l) \<Longrightarrow> a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l
[PROOF STEP]
hence "(a, b) \<in> list_before_rel l"
[PROOF STATE]
proof (prove)
using this:
a = l ! (i - 1)
b = l ! (j - 1)
i - 1 < j - 1
j - 1 < length l

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel l
[PROOF STEP]
unfolding list_before_rel_alt
[PROOF STATE]
proof (prove)
using this:
a = l ! (i - 1)
b = l ! (j - 1)
i - 1 < j - 1
j - 1 < length l

goal (1 subgoal):
 1. (a, b) \<in> {(l ! i, l ! j) |i j. i < j \<and> j < length l}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(a, b) \<in> list_before_rel l

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l) \<Longrightarrow> a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
i \<noteq> 0 \<Longrightarrow> (a, b) \<in> list_before_rel l

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l) \<Longrightarrow> a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i = 0 \<Longrightarrow> x = a
i = 0 \<Longrightarrow> b \<in> set l
i \<noteq> 0 \<Longrightarrow> (a, b) \<in> list_before_rel l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = 0 \<Longrightarrow> x = a
i = 0 \<Longrightarrow> b \<in> set l
i \<noteq> 0 \<Longrightarrow> (a, b) \<in> list_before_rel l

goal (1 subgoal):
 1. a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l \<Longrightarrow> (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
subgoal premises prems for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
assume [simp]: "a=x" and "b\<in>set l"
[PROOF STATE]
proof (state)
this:
a = x
b \<in> set l

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = x
b \<in> set l
[PROOF STEP]
obtain j where "b = l!j" "j<length l"
[PROOF STATE]
proof (prove)
using this:
a = x
b \<in> set l

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>b = l ! j; j < length l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: in_set_conv_nth)
[PROOF STATE]
proof (state)
this:
b = l ! j
j < length l

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
hence "a=(x#l)!0" "b = (x#l)!Suc j" "0 < Suc j" "Suc j < length (x#l)"
[PROOF STATE]
proof (prove)
using this:
b = l ! j
j < length l

goal (1 subgoal):
 1. (a = (x # l) ! 0 &&& b = (x # l) ! Suc j) &&& 0 < Suc j &&& Suc j < length (x # l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = (x # l) ! 0
b = (x # l) ! Suc j
0 < Suc j
Suc j < length (x # l)

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
a = (x # l) ! 0
b = (x # l) ! Suc j
0 < Suc j
Suc j < length (x # l)

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
unfolding list_before_rel_alt
[PROOF STATE]
proof (prove)
using this:
a = (x # l) ! 0
b = (x # l) ! Suc j
0 < Suc j
Suc j < length (x # l)

goal (1 subgoal):
 1. (a, b) \<in> {((x # l) ! i, (x # l) ! j) |i j. i < j \<and> j < length (x # l)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(a, b) \<in> list_before_rel (x # l)

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>a = x; b \<in> set l\<rbrakk> \<Longrightarrow> (a, b) \<in> list_before_rel (x # l)

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>a = x; b \<in> set l\<rbrakk> \<Longrightarrow> (a, b) \<in> list_before_rel (x # l)

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>a = x; b \<in> set l\<rbrakk> \<Longrightarrow> (a, b) \<in> list_before_rel (x # l)

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
assume "(a, b) \<in> list_before_rel l"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> list_before_rel l

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> list_before_rel l

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
unfolding list_before_rel_alt
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> {(l ! i, l ! j) |i j. i < j \<and> j < length l}

goal (1 subgoal):
 1. (a, b) \<in> {((x # l) ! i, (x # l) ! j) |i j. i < j \<and> j < length (x # l)}
[PROOF STEP]
by clarsimp (metis Suc_mono nth_Cons_Suc)
[PROOF STATE]
proof (state)
this:
(a, b) \<in> list_before_rel (x # l)

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(a, b) \<in> list_before_rel l \<Longrightarrow> (a, b) \<in> list_before_rel (x # l)

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a = x; b \<in> set l\<rbrakk> \<Longrightarrow> (a, b) \<in> list_before_rel (x # l)
(a, b) \<in> list_before_rel l \<Longrightarrow> (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a = x; b \<in> set l\<rbrakk> \<Longrightarrow> (a, b) \<in> list_before_rel (x # l)
(a, b) \<in> list_before_rel l \<Longrightarrow> (a, b) \<in> list_before_rel (x # l)

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
using prems
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a = x; b \<in> set l\<rbrakk> \<Longrightarrow> (a, b) \<in> list_before_rel (x # l)
(a, b) \<in> list_before_rel l \<Longrightarrow> (a, b) \<in> list_before_rel (x # l)
a = x \<and> b \<in> set l \<or> (a, b) \<in> list_before_rel l

goal (1 subgoal):
 1. (a, b) \<in> list_before_rel (x # l)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(a, b) \<in> list_before_rel (x # l)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_top_sorted_alt: "is_top_sorted R l \<longleftrightarrow> (\<forall>x y. (x,y)\<in>list_before_rel l \<longrightarrow> (y,x)\<notin>R\<^sup>*)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_top_sorted R l = (\<forall>x y. (x, y) \<in> list_before_rel l \<longrightarrow> (y, x) \<notin> R\<^sup>*)
[PROOF STEP]
unfolding is_top_sorted_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (list_before_rel l \<inter> (R\<^sup>*)\<inverse> = {}) = (\<forall>x y. (x, y) \<in> list_before_rel l \<longrightarrow> (y, x) \<notin> R\<^sup>*)
[PROOF STEP]
by auto


[STATEMENT]
lemma is_top_sorted_empty_rel[simp]: "is_top_sorted {} l \<longleftrightarrow> distinct l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_top_sorted {} l = distinct l
[PROOF STEP]
by (auto simp: is_top_sorted_def list_before_irrefl_eq_distinct[symmetric] irrefl_def)


[STATEMENT]
lemma is_top_sorted_empty_list[simp]: "is_top_sorted R []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_top_sorted R []
[PROOF STEP]
by (auto simp: is_top_sorted_def)


[STATEMENT]
lemma is_top_sorted_distinct:
  assumes "is_top_sorted R l"
  shows "distinct l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct l
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> distinct l \<Longrightarrow> False
[PROOF STEP]
assume "\<not>distinct l"
[PROOF STATE]
proof (state)
this:
\<not> distinct l

goal (1 subgoal):
 1. \<not> distinct l \<Longrightarrow> False
[PROOF STEP]
with list_before_irrefl_eq_distinct[of l]
[PROOF STATE]
proof (chain)
picking this:
irrefl (list_before_rel l) = distinct l
\<not> distinct l
[PROOF STEP]
obtain x where "(x,x)\<in>(list_before_rel l)"
[PROOF STATE]
proof (prove)
using this:
irrefl (list_before_rel l) = distinct l
\<not> distinct l

goal (1 subgoal):
 1. (\<And>x. (x, x) \<in> list_before_rel l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: irrefl_def)
[PROOF STATE]
proof (state)
this:
(x, x) \<in> list_before_rel l

goal (1 subgoal):
 1. \<not> distinct l \<Longrightarrow> False
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
is_top_sorted R l
(x, x) \<in> list_before_rel l
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
is_top_sorted R l
(x, x) \<in> list_before_rel l

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding is_top_sorted_def
[PROOF STATE]
proof (prove)
using this:
list_before_rel l \<inter> (R\<^sup>*)\<inverse> = {}
(x, x) \<in> list_before_rel l

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_top_sorted_cons: "is_top_sorted R (x#l) \<longleftrightarrow> ({x}\<times>set l \<inter> (R\<^sup>*)\<inverse> = {}) \<and> is_top_sorted R l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_top_sorted R (x # l) = ({x} \<times> set l \<inter> (R\<^sup>*)\<inverse> = {} \<and> is_top_sorted R l)
[PROOF STEP]
unfolding is_top_sorted_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (list_before_rel (x # l) \<inter> (R\<^sup>*)\<inverse> = {}) = ({x} \<times> set l \<inter> (R\<^sup>*)\<inverse> = {} \<and> list_before_rel l \<inter> (R\<^sup>*)\<inverse> = {})
[PROOF STEP]
by (auto simp: list_before_rel_cons)


[STATEMENT]
lemma is_top_sorted_append: "is_top_sorted R (l1@l2)
  \<longleftrightarrow> (set l1\<times>set l2 \<inter> (R\<^sup>*)\<inverse> = {}) \<and> is_top_sorted R l1 \<and> is_top_sorted R l2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_top_sorted R (l1 @ l2) = (set l1 \<times> set l2 \<inter> (R\<^sup>*)\<inverse> = {} \<and> is_top_sorted R l1 \<and> is_top_sorted R l2)
[PROOF STEP]
by (induction l1) (auto simp: is_top_sorted_cons)


[STATEMENT]
lemma is_top_sorted_remove_elem: "is_top_sorted R (l1@x#l2) \<Longrightarrow> is_top_sorted R (l1@l2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_top_sorted R (l1 @ x # l2) \<Longrightarrow> is_top_sorted R (l1 @ l2)
[PROOF STEP]
by (auto simp: is_top_sorted_cons is_top_sorted_append)


[STATEMENT]
lemma is_top_sorted_antimono:
  assumes "R\<subseteq>R'"
  assumes "is_top_sorted R' l"
  shows "is_top_sorted R l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_top_sorted R l
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
R \<subseteq> R'
is_top_sorted R' l

goal (1 subgoal):
 1. is_top_sorted R l
[PROOF STEP]
unfolding is_top_sorted_alt
[PROOF STATE]
proof (prove)
using this:
R \<subseteq> R'
\<forall>x y. (x, y) \<in> list_before_rel l \<longrightarrow> (y, x) \<notin> R'\<^sup>*

goal (1 subgoal):
 1. \<forall>x y. (x, y) \<in> list_before_rel l \<longrightarrow> (y, x) \<notin> R\<^sup>*
[PROOF STEP]
by (auto dest: rtrancl_mono_mp)


[STATEMENT]
lemma is_top_sorted_isolated_constraint:
  assumes "R' \<subseteq> R \<union> {x}\<times>X" "R'\<inter>UNIV\<times>{x} = {}"
  assumes "x\<notin>set l"
  assumes "is_top_sorted R l"
  shows "is_top_sorted R' l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_top_sorted R' l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_top_sorted R' l
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_top_sorted R' l
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_top_sorted R' l
[PROOF STEP]
assume "(a,b)\<in>R'\<^sup>*" "a\<noteq>x" "b\<noteq>x"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> R'\<^sup>*
a \<noteq> x
b \<noteq> x

goal (1 subgoal):
 1. is_top_sorted R' l
[PROOF STEP]
hence "(a,b)\<in>R\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> R'\<^sup>*
a \<noteq> x
b \<noteq> x

goal (1 subgoal):
 1. (a, b) \<in> R\<^sup>*
[PROOF STEP]
proof (induction rule: converse_rtrancl_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>b \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (b, b) \<in> R\<^sup>*
 2. \<And>y z. \<lbrakk>(y, z) \<in> R'; (z, b) \<in> R'\<^sup>*; \<lbrakk>z \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (z, b) \<in> R\<^sup>*; y \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (y, b) \<in> R\<^sup>*
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:
b \<noteq> x
b \<noteq> x

goal (2 subgoals):
 1. \<lbrakk>b \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (b, b) \<in> R\<^sup>*
 2. \<And>y z. \<lbrakk>(y, z) \<in> R'; (z, b) \<in> R'\<^sup>*; \<lbrakk>z \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (z, b) \<in> R\<^sup>*; y \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (y, b) \<in> R\<^sup>*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<noteq> x
b \<noteq> x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
b \<noteq> x
b \<noteq> x

goal (1 subgoal):
 1. (b, b) \<in> R\<^sup>*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(b, b) \<in> R\<^sup>*

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) \<in> R'; (z, b) \<in> R'\<^sup>*; \<lbrakk>z \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (z, b) \<in> R\<^sup>*; y \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (y, b) \<in> R\<^sup>*
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) \<in> R'; (z, b) \<in> R'\<^sup>*; \<lbrakk>z \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (z, b) \<in> R\<^sup>*; y \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (y, b) \<in> R\<^sup>*
[PROOF STEP]
case (step y z)
[PROOF STATE]
proof (state)
this:
(y, z) \<in> R'
(z, b) \<in> R'\<^sup>*
\<lbrakk>z \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (z, b) \<in> R\<^sup>*
y \<noteq> x
b \<noteq> x

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) \<in> R'; (z, b) \<in> R'\<^sup>*; \<lbrakk>z \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (z, b) \<in> R\<^sup>*; y \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (y, b) \<in> R\<^sup>*
[PROOF STEP]
with assms(1,2)
[PROOF STATE]
proof (chain)
picking this:
R' \<subseteq> R \<union> {x} \<times> X
R' \<inter> UNIV \<times> {x} = {}
(y, z) \<in> R'
(z, b) \<in> R'\<^sup>*
\<lbrakk>z \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (z, b) \<in> R\<^sup>*
y \<noteq> x
b \<noteq> x
[PROOF STEP]
have "z\<noteq>x" "(y,z)\<in>R"
[PROOF STATE]
proof (prove)
using this:
R' \<subseteq> R \<union> {x} \<times> X
R' \<inter> UNIV \<times> {x} = {}
(y, z) \<in> R'
(z, b) \<in> R'\<^sup>*
\<lbrakk>z \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (z, b) \<in> R\<^sup>*
y \<noteq> x
b \<noteq> x

goal (1 subgoal):
 1. z \<noteq> x &&& (y, z) \<in> R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<noteq> x
(y, z) \<in> R

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) \<in> R'; (z, b) \<in> R'\<^sup>*; \<lbrakk>z \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (z, b) \<in> R\<^sup>*; y \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (y, b) \<in> R\<^sup>*
[PROOF STEP]
with step
[PROOF STATE]
proof (chain)
picking this:
(y, z) \<in> R'
(z, b) \<in> R'\<^sup>*
\<lbrakk>z \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (z, b) \<in> R\<^sup>*
y \<noteq> x
b \<noteq> x
z \<noteq> x
(y, z) \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> R'
(z, b) \<in> R'\<^sup>*
\<lbrakk>z \<noteq> x; b \<noteq> x\<rbrakk> \<Longrightarrow> (z, b) \<in> R\<^sup>*
y \<noteq> x
b \<noteq> x
z \<noteq> x
(y, z) \<in> R

goal (1 subgoal):
 1. (y, b) \<in> R\<^sup>*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(y, b) \<in> R\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(a, b) \<in> R\<^sup>*

goal (1 subgoal):
 1. is_top_sorted R' l
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?a2, ?b2) \<in> R'\<^sup>*; ?a2 \<noteq> x; ?b2 \<noteq> x\<rbrakk> \<Longrightarrow> (?a2, ?b2) \<in> R\<^sup>*

goal (1 subgoal):
 1. is_top_sorted R' l
[PROOF STEP]
note AUX=this
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?a2, ?b2) \<in> R'\<^sup>*; ?a2 \<noteq> x; ?b2 \<noteq> x\<rbrakk> \<Longrightarrow> (?a2, ?b2) \<in> R\<^sup>*

goal (1 subgoal):
 1. is_top_sorted R' l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_top_sorted R' l
[PROOF STEP]
using assms(3,4) AUX list_before_rel_on_elems
[PROOF STATE]
proof (prove)
using this:
x \<notin> set l
is_top_sorted R l
\<lbrakk>(?a2, ?b2) \<in> R'\<^sup>*; ?a2 \<noteq> x; ?b2 \<noteq> x\<rbrakk> \<Longrightarrow> (?a2, ?b2) \<in> R\<^sup>*
list_before_rel ?l \<subseteq> set ?l \<times> set ?l

goal (1 subgoal):
 1. is_top_sorted R' l
[PROOF STEP]
unfolding is_top_sorted_def
[PROOF STATE]
proof (prove)
using this:
x \<notin> set l
list_before_rel l \<inter> (R\<^sup>*)\<inverse> = {}
\<lbrakk>(?a2, ?b2) \<in> R'\<^sup>*; ?a2 \<noteq> x; ?b2 \<noteq> x\<rbrakk> \<Longrightarrow> (?a2, ?b2) \<in> R\<^sup>*
list_before_rel ?l \<subseteq> set ?l \<times> set ?l

goal (1 subgoal):
 1. list_before_rel l \<inter> (R'\<^sup>*)\<inverse> = {}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
is_top_sorted R' l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<phi>E:
assumes \<phi>: "\<phi> (Trans s a ou s')" (is "\<phi> ?trn")
and step: "step s a = (ou, s')"
and rs: "reach s"
obtains
  (Friend) p aID uID' where "a = COMact (comSendCreateOFriend UID p aID uID')" "ou \<noteq> outErr"
                            "f ?trn = FrVal aID uID' True" "uID' \<notin> UIDs aID"
| (Unfriend) p aID uID' where "a = COMact (comSendDeleteOFriend UID p aID uID')" "ou \<noteq> outErr"
                              "f ?trn = FrVal aID uID' False" "uID' \<notin> UIDs aID"
| (OpenF) uid p uid' where "a = Cact (cFriend uid p uid')" "ou = outOK" "p = pass s uid"
                           "uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID"
                           "open s'" "\<not>open s"
                           "f ?trn = OVal True"
| (CloseF) uid p uid' where "a = Dact (dFriend uid p uid')" "ou = outOK" "p = pass s uid"
                            "uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID"
                            "open s" "\<not>open s'"
                            "f ?trn = OVal False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>p aID uID'. \<lbrakk>a = COMact (comSendCreateOFriend UID p aID uID'); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aID uID' True; uID' \<notin> UIDs aID\<rbrakk> \<Longrightarrow> thesis; \<And>p aID uID'. \<lbrakk>a = COMact (comSendDeleteOFriend UID p aID uID'); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aID uID' False; uID' \<notin> UIDs aID\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s'; \<not> open s; f (Trans s a ou s') = OVal True\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>p aID uID'. \<lbrakk>a = COMact (comSendCreateOFriend UID p aID uID'); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aID uID' True; uID' \<notin> UIDs aID\<rbrakk> \<Longrightarrow> thesis; \<And>p aID uID'. \<lbrakk>a = COMact (comSendDeleteOFriend UID p aID uID'); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aID uID' False; uID' \<notin> UIDs aID\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s'; \<not> open s; f (Trans s a ou s') = OVal True\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; ?P12\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>p aID uID'. \<lbrakk>a = COMact (comSendCreateOFriend UID p aID uID'); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aID uID' True; uID' \<notin> UIDs aID\<rbrakk> \<Longrightarrow> thesis; \<And>p aID uID'. \<lbrakk>a = COMact (comSendDeleteOFriend UID p aID uID'); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aID uID' False; uID' \<notin> UIDs aID\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s'; \<not> open s; f (Trans s a ou s') = OVal True\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; \<not> ?P12\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume "open s = open s'"
[PROOF STATE]
proof (state)
this:
open s = open s'

goal (2 subgoals):
 1. \<lbrakk>\<And>p aID uID'. \<lbrakk>a = COMact (comSendCreateOFriend UID p aID uID'); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aID uID' True; uID' \<notin> UIDs aID\<rbrakk> \<Longrightarrow> thesis; \<And>p aID uID'. \<lbrakk>a = COMact (comSendDeleteOFriend UID p aID uID'); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aID uID' False; uID' \<notin> UIDs aID\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s'; \<not> open s; f (Trans s a ou s') = OVal True\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; ?P12\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>p aID uID'. \<lbrakk>a = COMact (comSendCreateOFriend UID p aID uID'); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aID uID' True; uID' \<notin> UIDs aID\<rbrakk> \<Longrightarrow> thesis; \<And>p aID uID'. \<lbrakk>a = COMact (comSendDeleteOFriend UID p aID uID'); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aID uID' False; uID' \<notin> UIDs aID\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s'; \<not> open s; f (Trans s a ou s') = OVal True\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; \<not> ?P12\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with \<phi>
[PROOF STATE]
proof (chain)
picking this:
\<phi> (Trans s a ou s')
open s = open s'
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s a ou s')
open s = open s'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (elim \<phi>.elims) (auto intro: Friend Unfriend)
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<lbrakk>\<And>p aID uID'. \<lbrakk>a = COMact (comSendCreateOFriend UID p aID uID'); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aID uID' True; uID' \<notin> UIDs aID\<rbrakk> \<Longrightarrow> thesis; \<And>p aID uID'. \<lbrakk>a = COMact (comSendDeleteOFriend UID p aID uID'); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aID uID' False; uID' \<notin> UIDs aID\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s'; \<not> open s; f (Trans s a ou s') = OVal True\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; open s \<noteq> open s'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>p aID uID'. \<lbrakk>a = COMact (comSendCreateOFriend UID p aID uID'); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aID uID' True; uID' \<notin> UIDs aID\<rbrakk> \<Longrightarrow> thesis; \<And>p aID uID'. \<lbrakk>a = COMact (comSendDeleteOFriend UID p aID uID'); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aID uID' False; uID' \<notin> UIDs aID\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s'; \<not> open s; f (Trans s a ou s') = OVal True\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; open s \<noteq> open s'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume "open s \<noteq> open s'"
[PROOF STATE]
proof (state)
this:
open s \<noteq> open s'

goal (1 subgoal):
 1. \<lbrakk>\<And>p aID uID'. \<lbrakk>a = COMact (comSendCreateOFriend UID p aID uID'); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aID uID' True; uID' \<notin> UIDs aID\<rbrakk> \<Longrightarrow> thesis; \<And>p aID uID'. \<lbrakk>a = COMact (comSendDeleteOFriend UID p aID uID'); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aID uID' False; uID' \<notin> UIDs aID\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s'; \<not> open s; f (Trans s a ou s') = OVal True\<rbrakk> \<Longrightarrow> thesis; \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> thesis; open s \<noteq> open s'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open s \<noteq> open s'
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
open s \<noteq> open s'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (elim open_step_cases[OF _ step], goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s'; \<not> open s\<rbrakk> \<Longrightarrow> thesis
 2. \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
a = Cact (cFriend uid_ p_ uid'_)
ou = outOK
p_ = pass s uid_
uid_ \<in> UIDs AID \<and> uid'_ = UID \<or> uid_ = UID \<and> uid'_ \<in> UIDs AID
open s'
\<not> open s

goal (2 subgoals):
 1. \<And>uid p uid'. \<lbrakk>a = Cact (cFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s'; \<not> open s\<rbrakk> \<Longrightarrow> thesis
 2. \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Cact (cFriend uid_ p_ uid'_)
ou = outOK
p_ = pass s uid_
uid_ \<in> UIDs AID \<and> uid'_ = UID \<or> uid_ = UID \<and> uid'_ \<in> UIDs AID
open s'
\<not> open s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a = Cact (cFriend uid_ p_ uid'_)
ou = outOK
p_ = pass s uid_
uid_ \<in> UIDs AID \<and> uid'_ = UID \<or> uid_ = UID \<and> uid'_ \<in> UIDs AID
open s'
\<not> open s

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (intro OpenF) auto
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
a = Dact (dFriend uid_ p_ uid'_)
ou = outOK
p_ = pass s uid_
uid_ \<in> UIDs AID \<and> uid'_ = UID \<or> uid_ = UID \<and> uid'_ \<in> UIDs AID
open s
\<not> open s'

goal (1 subgoal):
 1. \<And>uid p uid'. \<lbrakk>a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Dact (dFriend uid_ p_ uid'_)
ou = outOK
p_ = pass s uid_
uid_ \<in> UIDs AID \<and> uid'_ = UID \<or> uid_ = UID \<and> uid'_ \<in> UIDs AID
open s
\<not> open s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a = Dact (dFriend uid_ p_ uid'_)
ou = outOK
p_ = pass s uid_
uid_ \<in> UIDs AID \<and> uid'_ = UID \<or> uid_ = UID \<and> uid'_ \<in> UIDs AID
open s
\<not> open s'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (intro CloseF) auto
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed