[STATEMENT]
lemma PO_m1_inv4_rfresh_trans [iff]:
  "{m1_inv4_rfresh \<inter> m1_inv3r_init \<inter> m1_inv2r_serv \<inter> m1_inv3_ifresh \<inter> m1_secrecy}
      trans m1
   {> m1_inv4_rfresh}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {m1_inv4_rfresh \<inter> m1_inv3r_init \<inter> m1_inv2r_serv \<inter> m1_inv3_ifresh \<inter> m1_secrecy} TS.trans m1 {> m1_inv4_rfresh}
[PROOF STEP]
apply (simp add: PO_hoare_defs m1_defs, safe intro!: m1_inv4_rfreshI, simp_all)
[PROOF STATE]
proof (prove)
goal (27 subgoals):
 1. \<And>Rb Rb' A A' B B' Kab xa xd. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; xd \<notin> dom (runs xa); Rb \<noteq> xd; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END]); Rb' \<noteq> xd; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> Rb = Rb'
 2. \<And>Rb Rb' A A' B B' Kab xa xe. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; xe \<notin> dom (runs xa); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> Rb = Rb'
 3. \<And>Rb Rb' A A' B B' Kab xa xf. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; xf \<notin> dom (runs xa); Rb \<noteq> xf; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END]); Rb' \<noteq> xf; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> Rb = Rb'
 4. \<And>Rb Rb' A A' B B' Kab xa xb xc xd xi a b. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xd = Some (Init, [xb, xc], []); Rb \<noteq> Rb'; (xi, a, b) \<in> m1_state.leak xa; xb \<in> bad; Rb \<noteq> xd; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END]); Rb' \<noteq> xd; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 5. \<And>Rb Rb' A A' B B' Kab xa xb xc xd a b Rs. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xd = Some (Init, [xb, xc], []); Rb \<noteq> Rb'; (sesK (Rs $ sk), a, b) \<in> m1_state.leak xa; runs xa Rs = Some (Serv, [xb, xc], [aNon (xd $ na)]); Rb \<noteq> xd; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END]); Rb' \<noteq> xd; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 6. \<And>Rb Rb' A A' B B' Kab xa xb xc xd xi. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xd = Some (Init, [xb, xc], []); (xi, xb) \<in> azC (runs xa); Rb \<noteq> Rb'; xb \<in> bad; Rb \<noteq> xd; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END]); Rb' \<noteq> xd; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 7. \<And>Rb Rb' A A' B B' Kab xa xb xc xd Rs. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xd = Some (Init, [xb, xc], []); (sesK (Rs $ sk), xb) \<in> azC (runs xa); runs xa Rs = Some (Serv, [xb, xc], [aNon (xd $ na)]); Rb \<noteq> xd; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END]); Rb' \<noteq> xd; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> Rb = Rb'
 8. \<And>Rb Rb' A A' B B' Kab xa xb xc xe xi a b. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [xb, xc], []); Rb \<noteq> Rb'; (xi, a, b) \<in> m1_state.leak xa; xc \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 9. \<And>Rb Rb' A A' B B' Kab xa xb xc xe a b Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [xb, xc], []); Rb \<noteq> Rb'; (sesK (Rs $ sk), a, b) \<in> m1_state.leak xa; runs xa Rs = Some (Serv, [xb, xc], [aNon Na]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 10. \<And>Rb Rb' A A' B B' Kab xa xb xc xe xi. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [xb, xc], []); (xi, xc) \<in> azC (runs xa); Rb \<noteq> Rb'; xc \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
A total of 27 subgoals...
[PROOF STEP]
apply (auto dest: m1_inv4_rfreshD)

\<comment> \<open>4 subgoals, from responder's final step 7\<close>
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Rb A A' B B' Kab xa xe. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); A' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb A A' B B' Kab xa xe. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); B' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 4. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rename_tac Rb A A' B B' Kab xa xe)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Rb A A' B B' Kab xa xe. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); A' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb A A' B B' Kab xa xe. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); B' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 4. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac B=B in m1_inv2r_servD, fast, fast, clarsimp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Rb A A' B B' xa xe Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk))]); A' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey (sesK (Rs $ sk)), END]); runs xa Rs = Some (Serv, [A, B], [aNon Na])\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb A A' B B' Kab xa xe. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); B' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 4. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (case_tac "B' \<notin> bad", auto dest: m1_inv2r_servD)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Rb A A' B B' xa xe Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk))]); A' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey (sesK (Rs $ sk)), END]); runs xa Rs = Some (Serv, [A, B], [aNon Na]); B' \<in> bad\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb A A' B B' Kab xa xe. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); B' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 4. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subgoal_tac "(sesK (Rs$sk), B') \<in> azC (runs xa)")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>Rb A A' B B' xa xe Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk))]); A' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey (sesK (Rs $ sk)), END]); runs xa Rs = Some (Serv, [A, B], [aNon Na]); B' \<in> bad; (sesK (Rs $ sk), B') \<in> azC (runs xa)\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb A A' B B' xa xe Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk))]); A' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey (sesK (Rs $ sk)), END]); runs xa Rs = Some (Serv, [A, B], [aNon Na]); B' \<in> bad\<rbrakk> \<Longrightarrow> (sesK (Rs $ sk), B') \<in> azC (runs xa)
 3. \<And>Rb A A' B B' Kab xa xe. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); B' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 4. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 5. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>Rb A A' B B' xa xe Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk))]); A' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey (sesK (Rs $ sk)), END]); runs xa Rs = Some (Serv, [A, B], [aNon Na]); B' \<in> bad\<rbrakk> \<Longrightarrow> (sesK (Rs $ sk), B') \<in> azC (runs xa)
 2. \<And>Rb A A' B B' xa xe Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk))]); A' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey (sesK (Rs $ sk)), END]); runs xa Rs = Some (Serv, [A, B], [aNon Na]); B' \<in> bad; (sesK (Rs $ sk), B') \<in> azC (runs xa)\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb A A' B B' Kab xa xe. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); B' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 4. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 5. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule m1_secrecyE, auto)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Rb A A' B B' xa xe Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk))]); A' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey (sesK (Rs $ sk)), END]); runs xa Rs = Some (Serv, [A, B], [aNon Na]); B' \<in> bad; (sesK (Rs $ sk), B') \<in> azC (runs xa)\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb A A' B B' Kab xa xe. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); B' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 4. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule azC.cases, auto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Rb A A' B B' Kab xa xe. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); B' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rename_tac Rb A A' B B' Kab xa xe)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Rb A A' B B' Kab xa xe. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); B' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac B=B in m1_inv2r_servD, fast, fast, clarify)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Rb A A' B B' Kab xa xe Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk))]); B' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey (sesK (Rs $ sk)), END]); runs xa Rs = Some (Serv, [A, B], [aNon Na])\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subgoal_tac "(sesK (Rs$sk), B') \<in> azC (runs xa)")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Rb A A' B B' Kab xa xe Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk))]); B' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey (sesK (Rs $ sk)), END]); runs xa Rs = Some (Serv, [A, B], [aNon Na]); (sesK (Rs $ sk), B') \<in> azC (runs xa)\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb A A' B B' Kab xa xe Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk))]); B' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey (sesK (Rs $ sk)), END]); runs xa Rs = Some (Serv, [A, B], [aNon Na])\<rbrakk> \<Longrightarrow> (sesK (Rs $ sk), B') \<in> azC (runs xa)
 3. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 4. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Rb A A' B B' Kab xa xe Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk))]); B' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey (sesK (Rs $ sk)), END]); runs xa Rs = Some (Serv, [A, B], [aNon Na])\<rbrakk> \<Longrightarrow> (sesK (Rs $ sk), B') \<in> azC (runs xa)
 2. \<And>Rb A A' B B' Kab xa xe Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk))]); B' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey (sesK (Rs $ sk)), END]); runs xa Rs = Some (Serv, [A, B], [aNon Na]); (sesK (Rs $ sk), B') \<in> azC (runs xa)\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 4. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule m1_secrecyE, auto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Rb A A' B B' xa xe Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk))]); B' \<in> bad; Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey (sesK (Rs $ sk)), END]); runs xa Rs = Some (Serv, [A, B], [aNon Na]); (sesK (Rs $ sk), B') \<in> azC (runs xa)\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule azC.cases, auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rename_tac Rb' A A' B B' Kab xa xe Ra)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (case_tac "A' \<notin> bad \<and> B' \<notin> bad", auto)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); A' \<notin> bad; B' \<notin> bad\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); A' \<in> bad\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); B' \<in> bad\<rbrakk> \<Longrightarrow> False
 4. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule m1_inv3r_initD, auto)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Rb' A A' B B' Kab xa xe Ra Raa nla. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); A' \<notin> bad; B' \<notin> bad; runs xa Raa = Some (Init, [A', B'], aKey Kab # aNon (Rb' $ nb) # nla)\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); A' \<in> bad\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); B' \<in> bad\<rbrakk> \<Longrightarrow> False
 4. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rename_tac Raa nla)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Rb' A A' B B' Kab xa xe Ra Raa nla. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); A' \<notin> bad; B' \<notin> bad; runs xa Raa = Some (Init, [A', B'], aKey Kab # aNon (Rb' $ nb) # nla)\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); A' \<in> bad\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); B' \<in> bad\<rbrakk> \<Longrightarrow> False
 4. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac Ra=Ra in m1_inv3_ifreshD, auto)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Rb' A A' B B' Kab xa xe Ra Raa nla. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); A' \<notin> bad; B' \<notin> bad; runs xa Raa = Some (Init, [A', B'], aKey Kab # aNon (Rb' $ nb) # nla)\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); A' \<in> bad\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); B' \<in> bad\<rbrakk> \<Longrightarrow> False
 4. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subgoal_tac "Ra = Raa", auto)

    \<comment> \<open>@{text "A' \<in> bad"}\<close>
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); A' \<in> bad\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); B' \<in> bad\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac B=B in m1_inv2r_servD, fast, fast, clarify)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Rb' A A' B B' Kab xa xe Ra Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey (sesK (Rs $ sk))]); runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk)), END]); A' \<in> bad; runs xa Rs = Some (Serv, [A, B], [aNon Na])\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); B' \<in> bad\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rename_tac Rs Na)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Rb' A A' B B' Kab xa xe Ra Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey (sesK (Rs $ sk))]); runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk)), END]); A' \<in> bad; runs xa Rs = Some (Serv, [A, B], [aNon Na])\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); B' \<in> bad\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (case_tac "B' \<notin> bad", auto dest: m1_inv2r_servD)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Rb' A A' B B' xa xe Ra Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey (sesK (Rs $ sk))]); runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk)), END]); A' \<in> bad; runs xa Rs = Some (Serv, [A, B], [aNon Na]); B' \<in> bad\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); B' \<in> bad\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subgoal_tac "(sesK (Rs$sk), B') \<in> azC (runs xa)")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Rb' A A' B B' xa xe Ra Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey (sesK (Rs $ sk))]); runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk)), END]); A' \<in> bad; runs xa Rs = Some (Serv, [A, B], [aNon Na]); B' \<in> bad; (sesK (Rs $ sk), B') \<in> azC (runs xa)\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb' A A' B B' xa xe Ra Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey (sesK (Rs $ sk))]); runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk)), END]); A' \<in> bad; runs xa Rs = Some (Serv, [A, B], [aNon Na]); B' \<in> bad\<rbrakk> \<Longrightarrow> (sesK (Rs $ sk), B') \<in> azC (runs xa)
 3. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); B' \<in> bad\<rbrakk> \<Longrightarrow> False
 4. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Rb' A A' B B' xa xe Ra Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey (sesK (Rs $ sk))]); runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk)), END]); A' \<in> bad; runs xa Rs = Some (Serv, [A, B], [aNon Na]); B' \<in> bad\<rbrakk> \<Longrightarrow> (sesK (Rs $ sk), B') \<in> azC (runs xa)
 2. \<And>Rb' A A' B B' xa xe Ra Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey (sesK (Rs $ sk))]); runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk)), END]); A' \<in> bad; runs xa Rs = Some (Serv, [A, B], [aNon Na]); B' \<in> bad; (sesK (Rs $ sk), B') \<in> azC (runs xa)\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); B' \<in> bad\<rbrakk> \<Longrightarrow> False
 4. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule m1_secrecyE, auto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Rb' A A' B B' xa xe Ra Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey (sesK (Rs $ sk))]); runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk)), END]); A' \<in> bad; runs xa Rs = Some (Serv, [A, B], [aNon Na]); B' \<in> bad; (sesK (Rs $ sk), B') \<in> azC (runs xa)\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); B' \<in> bad\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule azC.cases, auto)

    \<comment> \<open>@{text "B' \<in> bad"}\<close>
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Rb' A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey Kab]); runs xa Ra = Some (Init, [A, B], [aKey Kab, aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey Kab, END]); B' \<in> bad\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac B=B in m1_inv2r_servD, fast, fast, clarify)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Rb' A A' B B' Kab xa xe Ra Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey (sesK (Rs $ sk))]); runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk)), END]); B' \<in> bad; runs xa Rs = Some (Serv, [A, B], [aNon Na])\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rename_tac Rs Na)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Rb' A A' B B' Kab xa xe Ra Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey (sesK (Rs $ sk))]); runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk)), END]); B' \<in> bad; runs xa Rs = Some (Serv, [A, B], [aNon Na])\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subgoal_tac "(sesK (Rs$sk), B') \<in> azC (runs xa)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Rb' A A' B B' Kab xa xe Ra Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey (sesK (Rs $ sk))]); runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk)), END]); B' \<in> bad; runs xa Rs = Some (Serv, [A, B], [aNon Na]); (sesK (Rs $ sk), B') \<in> azC (runs xa)\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb' A A' B B' Kab xa xe Ra Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey (sesK (Rs $ sk))]); runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk)), END]); B' \<in> bad; runs xa Rs = Some (Serv, [A, B], [aNon Na])\<rbrakk> \<Longrightarrow> (sesK (Rs $ sk), B') \<in> azC (runs xa)
 3. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Rb' A A' B B' Kab xa xe Ra Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey (sesK (Rs $ sk))]); runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk)), END]); B' \<in> bad; runs xa Rs = Some (Serv, [A, B], [aNon Na])\<rbrakk> \<Longrightarrow> (sesK (Rs $ sk), B') \<in> azC (runs xa)
 2. \<And>Rb' A A' B B' Kab xa xe Ra Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey (sesK (Rs $ sk))]); runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk)), END]); B' \<in> bad; runs xa Rs = Some (Serv, [A, B], [aNon Na]); (sesK (Rs $ sk), B') \<in> azC (runs xa)\<rbrakk> \<Longrightarrow> False
 3. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule m1_secrecyE, auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Rb' A A' B B' xa xe Ra Rs Na. \<lbrakk>B \<notin> bad; A \<notin> bad; sesK (Rs $ sk) \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A, B], [aKey (sesK (Rs $ sk))]); runs xa Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon (xe $ nb)]); Rb' \<noteq> xe; runs xa Rb' = Some (Resp, [A', B'], [aKey (sesK (Rs $ sk)), END]); B' \<in> bad; runs xa Rs = Some (Serv, [A, B], [aNon Na]); (sesK (Rs $ sk), B') \<in> azC (runs xa)\<rbrakk> \<Longrightarrow> False
 2. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule azC.cases, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Rb A A' B B' Kab xa xe Ra. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule m1_inv3r_initD, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Rb A A' B B' Kab xa xe Ra Raa nla. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END]); runs xa Raa = Some (Init, [A, B], aKey Kab # aNon (Rb $ nb) # nla)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rename_tac Raa nla)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Rb A A' B B' Kab xa xe Ra Raa nla. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak xa); xa \<in> m1_secrecy; xa \<in> m1_inv3_ifresh; xa \<in> m1_inv2r_serv; xa \<in> m1_inv4_rfresh; xa \<in> m1_inv3r_init; runs xa xe = Some (Resp, [A', B'], [aKey Kab]); runs xa Ra = Some (Init, [A', B'], [aKey Kab, aNon (xe $ nb)]); Rb \<noteq> xe; runs xa Rb = Some (Resp, [A, B], [aKey Kab, END]); runs xa Raa = Some (Init, [A, B], aKey Kab # aNon (Rb $ nb) # nla)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subgoal_tac "Raa = Ra", auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma PO_m1_inv4_rfresh [iff]: "reach m1 \<subseteq> m1_inv4_rfresh"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reach m1 \<subseteq> m1_inv4_rfresh
[PROOF STEP]
apply (rule_tac
         J="m1_inv3r_init \<inter> m1_inv2r_serv \<inter> m1_inv3_ifresh \<inter> m1_secrecy"
       in inv_rule_incr)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. init m1 \<subseteq> m1_inv4_rfresh
 2. {m1_inv4_rfresh \<inter> (m1_inv3r_init \<inter> m1_inv2r_serv \<inter> m1_inv3_ifresh \<inter> m1_secrecy)} TS.trans m1 {> m1_inv4_rfresh}
 3. reach m1 \<subseteq> m1_inv3r_init \<inter> m1_inv2r_serv \<inter> m1_inv3_ifresh \<inter> m1_secrecy
[PROOF STEP]
apply (auto simp add: Int_assoc del: subsetI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma PO_m1_obs_inv4_rfresh [iff]: "oreach m1 \<subseteq> m1_inv4_rfresh"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oreach m1 \<subseteq> m1_inv4_rfresh
[PROOF STEP]
by (rule external_from_internal_invariant)
   (auto del: subsetI)


[STATEMENT]
lemma cont2val_val2cont_id: "cont2val oo val2cont = ID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont2val oo val2cont = ID
[PROOF STEP]
by (rule cfun_eqI, simp add: val2cont_def cont2val_def)


[STATEMENT]
lemma eval_body_strictExpr[simp]: "eval_body\<cdot>r\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_body\<cdot>r\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by (subst eval_body.unfold, simp)


[STATEMENT]
lemma eval_eval_body_eq: "eval = fix\<cdot>eval_body"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval = fix\<cdot>eval_body
[PROOF STEP]
by (rule cfun_eqI, subst eval_def, subst eval_body.unfold, simp)


[STATEMENT]
lemma unwrapC_strict[simp]: "unwrapC\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unwrapC\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
unfolding unwrapC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> g e s f. case g\<cdot>e of Nothing \<Rightarrow> f | Just\<cdot>n \<Rightarrow> s\<cdot>n)\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by (rule cfun_eqI)+ simp


[STATEMENT]
lemma wrapC_unwrapC_id: "wrapC oo unwrapC = ID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrapC oo unwrapC = ID
[PROOF STEP]
proof(intro cfun_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. (wrapC oo unwrapC)\<cdot>x\<cdot>xa = ID\<cdot>x\<cdot>xa
[PROOF STEP]
fix g e
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. (wrapC oo unwrapC)\<cdot>x\<cdot>xa = ID\<cdot>x\<cdot>xa
[PROOF STEP]
show "(wrapC oo unwrapC)\<cdot>g\<cdot>e = ID\<cdot>g\<cdot>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (wrapC oo unwrapC)\<cdot>g\<cdot>e = ID\<cdot>g\<cdot>e
[PROOF STEP]
by (cases "g\<cdot>e", simp_all add: wrapC_def unwrapC_def)
[PROOF STATE]
proof (state)
this:
(wrapC oo unwrapC)\<cdot>g\<cdot>e = ID\<cdot>g\<cdot>e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eval_body'_strictExpr[simp]: "eval_body'\<cdot>r\<cdot>\<bottom>\<cdot>s\<cdot>f = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_body'\<cdot>r\<cdot>\<bottom>\<cdot>s\<cdot>f = \<bottom>
[PROOF STEP]
by (subst eval_body'.unfold, simp)


[STATEMENT]
lemma eval_body'_eval_body_eq: "eval_body' = unwrapC oo eval_body oo wrapC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_body' = unwrapC oo eval_body oo wrapC
[PROOF STEP]
apply (intro cfun_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc. eval_body'\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc = (unwrapC oo eval_body oo wrapC)\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc
[PROOF STEP]
apply (unfold unwrapC_def wrapC_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc. eval_body'\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc = ((\<Lambda> g e s f. case g\<cdot>e of Nothing \<Rightarrow> f | Just\<cdot>n \<Rightarrow> s\<cdot>n) oo eval_body oo (\<Lambda> g e. g\<cdot>e\<cdot>Just\<cdot>Nothing))\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc
[PROOF STEP]
apply (case_tac xa)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x xa xb xc. xa = \<bottom> \<Longrightarrow> eval_body'\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc = ((\<Lambda> g e s f. case g\<cdot>e of Nothing \<Rightarrow> f | Just\<cdot>n \<Rightarrow> s\<cdot>n) oo eval_body oo (\<Lambda> g e. g\<cdot>e\<cdot>Just\<cdot>Nothing))\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc
 2. \<And>x xa xb xc Box. xa = Val\<cdot>Box \<Longrightarrow> eval_body'\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc = ((\<Lambda> g e s f. case g\<cdot>e of Nothing \<Rightarrow> f | Just\<cdot>n \<Rightarrow> s\<cdot>n) oo eval_body oo (\<Lambda> g e. g\<cdot>e\<cdot>Just\<cdot>Nothing))\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc
 3. \<And>x xa xb xc Expr1 Expr2. xa = Add\<cdot>Expr1\<cdot>Expr2 \<Longrightarrow> eval_body'\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc = ((\<Lambda> g e s f. case g\<cdot>e of Nothing \<Rightarrow> f | Just\<cdot>n \<Rightarrow> s\<cdot>n) oo eval_body oo (\<Lambda> g e. g\<cdot>e\<cdot>Just\<cdot>Nothing))\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc
 4. \<And>x xa xb xc. xa = Throw \<Longrightarrow> eval_body'\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc = ((\<Lambda> g e s f. case g\<cdot>e of Nothing \<Rightarrow> f | Just\<cdot>n \<Rightarrow> s\<cdot>n) oo eval_body oo (\<Lambda> g e. g\<cdot>e\<cdot>Just\<cdot>Nothing))\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc
 5. \<And>x xa xb xc Expr1 Expr2. xa = Catch\<cdot>Expr1\<cdot>Expr2 \<Longrightarrow> eval_body'\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc = ((\<Lambda> g e s f. case g\<cdot>e of Nothing \<Rightarrow> f | Just\<cdot>n \<Rightarrow> s\<cdot>n) oo eval_body oo (\<Lambda> g e. g\<cdot>e\<cdot>Just\<cdot>Nothing))\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa xb xc Expr1 Expr2. xa = Add\<cdot>Expr1\<cdot>Expr2 \<Longrightarrow> (case wrapC\<cdot>x\<cdot>Expr1 of Nothing \<Rightarrow> xc | Just\<cdot>n \<Rightarrow> case wrapC\<cdot>x\<cdot>Expr2 of Nothing \<Rightarrow> xc | Just\<cdot>m \<Rightarrow> xb\<cdot>(n + m)) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(mliftM2 (\<Lambda> a. Abs_cfun ((+) a))\<cdot>(x\<cdot>Expr1\<cdot>Just\<cdot>Nothing)\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing))
 2. \<And>xa xb xc. xa = Throw \<Longrightarrow> xc = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>mfail
 3. \<And>x xa xb xc Expr1 Expr2. xa = Catch\<cdot>Expr1\<cdot>Expr2 \<Longrightarrow> (case wrapC\<cdot>x\<cdot>Expr1 of Nothing \<Rightarrow> case wrapC\<cdot>x\<cdot>Expr2 of Nothing \<Rightarrow> xc | Just\<cdot>n \<Rightarrow> xb\<cdot>n | Just\<cdot>n \<Rightarrow> xb\<cdot>n) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(mcatch\<cdot>(x\<cdot>Expr1\<cdot>Just\<cdot>Nothing)\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing))
[PROOF STEP]
apply (simp add: wrapC_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa xb xc Expr1 Expr2. xa = Add\<cdot>Expr1\<cdot>Expr2 \<Longrightarrow> (case x\<cdot>Expr1\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> xc | Just\<cdot>n \<Rightarrow> case x\<cdot>Expr2\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> xc | Just\<cdot>m \<Rightarrow> xb\<cdot>(n + m)) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(mliftM2 (\<Lambda> a. Abs_cfun ((+) a))\<cdot>(x\<cdot>Expr1\<cdot>Just\<cdot>Nothing)\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing))
 2. \<And>xa xb xc. xa = Throw \<Longrightarrow> xc = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>mfail
 3. \<And>x xa xb xc Expr1 Expr2. xa = Catch\<cdot>Expr1\<cdot>Expr2 \<Longrightarrow> (case wrapC\<cdot>x\<cdot>Expr1 of Nothing \<Rightarrow> case wrapC\<cdot>x\<cdot>Expr2 of Nothing \<Rightarrow> xc | Just\<cdot>n \<Rightarrow> xb\<cdot>n | Just\<cdot>n \<Rightarrow> xb\<cdot>n) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(mcatch\<cdot>(x\<cdot>Expr1\<cdot>Just\<cdot>Nothing)\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing))
[PROOF STEP]
apply (case_tac "x\<cdot>Expr1\<cdot>Just\<cdot>Nothing")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x xa xb xc Expr1 Expr2. \<lbrakk>xa = Add\<cdot>Expr1\<cdot>Expr2; x\<cdot>Expr1\<cdot>Just\<cdot>Nothing = \<bottom>\<rbrakk> \<Longrightarrow> (case x\<cdot>Expr1\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> xc | Just\<cdot>n \<Rightarrow> case x\<cdot>Expr2\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> xc | Just\<cdot>m \<Rightarrow> xb\<cdot>(n + m)) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(mliftM2 (\<Lambda> a. Abs_cfun ((+) a))\<cdot>(x\<cdot>Expr1\<cdot>Just\<cdot>Nothing)\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing))
 2. \<And>x xa xb xc Expr1 Expr2. \<lbrakk>xa = Add\<cdot>Expr1\<cdot>Expr2; x\<cdot>Expr1\<cdot>Just\<cdot>Nothing = Nothing\<rbrakk> \<Longrightarrow> (case x\<cdot>Expr1\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> xc | Just\<cdot>n \<Rightarrow> case x\<cdot>Expr2\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> xc | Just\<cdot>m \<Rightarrow> xb\<cdot>(n + m)) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(mliftM2 (\<Lambda> a. Abs_cfun ((+) a))\<cdot>(x\<cdot>Expr1\<cdot>Just\<cdot>Nothing)\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing))
 3. \<And>x xa xb xc Expr1 Expr2 a. \<lbrakk>xa = Add\<cdot>Expr1\<cdot>Expr2; x\<cdot>Expr1\<cdot>Just\<cdot>Nothing = Just\<cdot>a\<rbrakk> \<Longrightarrow> (case x\<cdot>Expr1\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> xc | Just\<cdot>n \<Rightarrow> case x\<cdot>Expr2\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> xc | Just\<cdot>m \<Rightarrow> xb\<cdot>(n + m)) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(mliftM2 (\<Lambda> a. Abs_cfun ((+) a))\<cdot>(x\<cdot>Expr1\<cdot>Just\<cdot>Nothing)\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing))
 4. \<And>xa xb xc. xa = Throw \<Longrightarrow> xc = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>mfail
 5. \<And>x xa xb xc Expr1 Expr2. xa = Catch\<cdot>Expr1\<cdot>Expr2 \<Longrightarrow> (case wrapC\<cdot>x\<cdot>Expr1 of Nothing \<Rightarrow> case wrapC\<cdot>x\<cdot>Expr2 of Nothing \<Rightarrow> xc | Just\<cdot>n \<Rightarrow> xb\<cdot>n | Just\<cdot>n \<Rightarrow> xb\<cdot>n) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(mcatch\<cdot>(x\<cdot>Expr1\<cdot>Just\<cdot>Nothing)\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing))
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa xb xc Expr1 Expr2 a. \<lbrakk>xa = Add\<cdot>Expr1\<cdot>Expr2; x\<cdot>Expr1\<cdot>Just\<cdot>Nothing = Just\<cdot>a\<rbrakk> \<Longrightarrow> (case x\<cdot>Expr2\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> xc | Just\<cdot>m \<Rightarrow> xb\<cdot>(a + m)) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(mliftM2 (\<Lambda> a. Abs_cfun ((+) a))\<cdot>(Just\<cdot>a)\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing))
 2. \<And>xa xb xc. xa = Throw \<Longrightarrow> xc = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>mfail
 3. \<And>x xa xb xc Expr1 Expr2. xa = Catch\<cdot>Expr1\<cdot>Expr2 \<Longrightarrow> (case wrapC\<cdot>x\<cdot>Expr1 of Nothing \<Rightarrow> case wrapC\<cdot>x\<cdot>Expr2 of Nothing \<Rightarrow> xc | Just\<cdot>n \<Rightarrow> xb\<cdot>n | Just\<cdot>n \<Rightarrow> xb\<cdot>n) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(mcatch\<cdot>(x\<cdot>Expr1\<cdot>Just\<cdot>Nothing)\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing))
[PROOF STEP]
apply (case_tac "x\<cdot>Expr2\<cdot>Just\<cdot>Nothing")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x xa xb xc Expr1 Expr2 a. \<lbrakk>xa = Add\<cdot>Expr1\<cdot>Expr2; x\<cdot>Expr1\<cdot>Just\<cdot>Nothing = Just\<cdot>a; x\<cdot>Expr2\<cdot>Just\<cdot>Nothing = \<bottom>\<rbrakk> \<Longrightarrow> (case x\<cdot>Expr2\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> xc | Just\<cdot>m \<Rightarrow> xb\<cdot>(a + m)) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(mliftM2 (\<Lambda> a. Abs_cfun ((+) a))\<cdot>(Just\<cdot>a)\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing))
 2. \<And>x xa xb xc Expr1 Expr2 a. \<lbrakk>xa = Add\<cdot>Expr1\<cdot>Expr2; x\<cdot>Expr1\<cdot>Just\<cdot>Nothing = Just\<cdot>a; x\<cdot>Expr2\<cdot>Just\<cdot>Nothing = Nothing\<rbrakk> \<Longrightarrow> (case x\<cdot>Expr2\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> xc | Just\<cdot>m \<Rightarrow> xb\<cdot>(a + m)) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(mliftM2 (\<Lambda> a. Abs_cfun ((+) a))\<cdot>(Just\<cdot>a)\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing))
 3. \<And>x xa xb xc Expr1 Expr2 a aa. \<lbrakk>xa = Add\<cdot>Expr1\<cdot>Expr2; x\<cdot>Expr1\<cdot>Just\<cdot>Nothing = Just\<cdot>a; x\<cdot>Expr2\<cdot>Just\<cdot>Nothing = Just\<cdot>aa\<rbrakk> \<Longrightarrow> (case x\<cdot>Expr2\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> xc | Just\<cdot>m \<Rightarrow> xb\<cdot>(a + m)) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(mliftM2 (\<Lambda> a. Abs_cfun ((+) a))\<cdot>(Just\<cdot>a)\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing))
 4. \<And>xa xb xc. xa = Throw \<Longrightarrow> xc = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>mfail
 5. \<And>x xa xb xc Expr1 Expr2. xa = Catch\<cdot>Expr1\<cdot>Expr2 \<Longrightarrow> (case wrapC\<cdot>x\<cdot>Expr1 of Nothing \<Rightarrow> case wrapC\<cdot>x\<cdot>Expr2 of Nothing \<Rightarrow> xc | Just\<cdot>n \<Rightarrow> xb\<cdot>n | Just\<cdot>n \<Rightarrow> xb\<cdot>n) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(mcatch\<cdot>(x\<cdot>Expr1\<cdot>Just\<cdot>Nothing)\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing))
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa xb xc. xa = Throw \<Longrightarrow> xc = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>mfail
 2. \<And>x xa xb xc Expr1 Expr2. xa = Catch\<cdot>Expr1\<cdot>Expr2 \<Longrightarrow> (case wrapC\<cdot>x\<cdot>Expr1 of Nothing \<Rightarrow> case wrapC\<cdot>x\<cdot>Expr2 of Nothing \<Rightarrow> xc | Just\<cdot>n \<Rightarrow> xb\<cdot>n | Just\<cdot>n \<Rightarrow> xb\<cdot>n) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(mcatch\<cdot>(x\<cdot>Expr1\<cdot>Just\<cdot>Nothing)\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing))
[PROOF STEP]
apply (simp add: mfail_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc Expr1 Expr2. xa = Catch\<cdot>Expr1\<cdot>Expr2 \<Longrightarrow> (case wrapC\<cdot>x\<cdot>Expr1 of Nothing \<Rightarrow> case wrapC\<cdot>x\<cdot>Expr2 of Nothing \<Rightarrow> xc | Just\<cdot>n \<Rightarrow> xb\<cdot>n | Just\<cdot>n \<Rightarrow> xb\<cdot>n) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(mcatch\<cdot>(x\<cdot>Expr1\<cdot>Just\<cdot>Nothing)\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing))
[PROOF STEP]
apply (simp add: mcatch_def wrapC_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc Expr1 Expr2. xa = Catch\<cdot>Expr1\<cdot>Expr2 \<Longrightarrow> (case x\<cdot>Expr1\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> case x\<cdot>Expr2\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> xc | Just\<cdot>n \<Rightarrow> xb\<cdot>n | Just\<cdot>n \<Rightarrow> xb\<cdot>n) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(Maybe_case\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing)\<cdot>(Abs_cfun (Rep_cfun Just))\<cdot>(x\<cdot>Expr1\<cdot>Just\<cdot>Nothing))
[PROOF STEP]
apply (case_tac "x\<cdot>Expr1\<cdot>Just\<cdot>Nothing")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa xb xc Expr1 Expr2. \<lbrakk>xa = Catch\<cdot>Expr1\<cdot>Expr2; x\<cdot>Expr1\<cdot>Just\<cdot>Nothing = \<bottom>\<rbrakk> \<Longrightarrow> (case x\<cdot>Expr1\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> case x\<cdot>Expr2\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> xc | Just\<cdot>n \<Rightarrow> xb\<cdot>n | Just\<cdot>n \<Rightarrow> xb\<cdot>n) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(Maybe_case\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing)\<cdot>(Abs_cfun (Rep_cfun Just))\<cdot>(x\<cdot>Expr1\<cdot>Just\<cdot>Nothing))
 2. \<And>x xa xb xc Expr1 Expr2. \<lbrakk>xa = Catch\<cdot>Expr1\<cdot>Expr2; x\<cdot>Expr1\<cdot>Just\<cdot>Nothing = Nothing\<rbrakk> \<Longrightarrow> (case x\<cdot>Expr1\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> case x\<cdot>Expr2\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> xc | Just\<cdot>n \<Rightarrow> xb\<cdot>n | Just\<cdot>n \<Rightarrow> xb\<cdot>n) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(Maybe_case\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing)\<cdot>(Abs_cfun (Rep_cfun Just))\<cdot>(x\<cdot>Expr1\<cdot>Just\<cdot>Nothing))
 3. \<And>x xa xb xc Expr1 Expr2 a. \<lbrakk>xa = Catch\<cdot>Expr1\<cdot>Expr2; x\<cdot>Expr1\<cdot>Just\<cdot>Nothing = Just\<cdot>a\<rbrakk> \<Longrightarrow> (case x\<cdot>Expr1\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> case x\<cdot>Expr2\<cdot>Just\<cdot>Nothing of Nothing \<Rightarrow> xc | Just\<cdot>n \<Rightarrow> xb\<cdot>n | Just\<cdot>n \<Rightarrow> xb\<cdot>n) = Maybe_case\<cdot>xc\<cdot>(Abs_cfun (Rep_cfun xb))\<cdot>(Maybe_case\<cdot>(x\<cdot>Expr2\<cdot>Just\<cdot>Nothing)\<cdot>(Abs_cfun (Rep_cfun Just))\<cdot>(x\<cdot>Expr1\<cdot>Just\<cdot>Nothing))
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma eval_body_final_strictExpr[simp]: "eval_body_final\<cdot>r\<cdot>\<bottom>\<cdot>s\<cdot>f = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_body_final\<cdot>r\<cdot>\<bottom>\<cdot>s\<cdot>f = \<bottom>
[PROOF STEP]
by (subst eval_body_final.unfold, simp)


[STATEMENT]
lemma eval_body'_eval_body_final_eq: "eval_body_final oo unwrapC oo wrapC = eval_body'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_body_final oo unwrapC oo wrapC = eval_body'
[PROOF STEP]
apply (rule cfun_eqI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc. (eval_body_final oo unwrapC oo wrapC)\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc = eval_body'\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc
[PROOF STEP]
apply (case_tac xa)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x xa xb xc. xa = \<bottom> \<Longrightarrow> (eval_body_final oo unwrapC oo wrapC)\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc = eval_body'\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc
 2. \<And>x xa xb xc Box. xa = Val\<cdot>Box \<Longrightarrow> (eval_body_final oo unwrapC oo wrapC)\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc = eval_body'\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc
 3. \<And>x xa xb xc Expr1 Expr2. xa = Add\<cdot>Expr1\<cdot>Expr2 \<Longrightarrow> (eval_body_final oo unwrapC oo wrapC)\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc = eval_body'\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc
 4. \<And>x xa xb xc. xa = Throw \<Longrightarrow> (eval_body_final oo unwrapC oo wrapC)\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc = eval_body'\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc
 5. \<And>x xa xb xc Expr1 Expr2. xa = Catch\<cdot>Expr1\<cdot>Expr2 \<Longrightarrow> (eval_body_final oo unwrapC oo wrapC)\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc = eval_body'\<cdot>x\<cdot>xa\<cdot>xb\<cdot>xc
[PROOF STEP]
apply (simp_all add: unwrapC_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "eval = eval_final"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval = eval_final
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval = eval_final
[PROOF STEP]
have "eval = fix\<cdot>eval_body"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval = fix\<cdot>eval_body
[PROOF STEP]
by (rule eval_eval_body_eq)
[PROOF STATE]
proof (state)
this:
eval = fix\<cdot>eval_body

goal (1 subgoal):
 1. eval = eval_final
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval = fix\<cdot>eval_body

goal (1 subgoal):
 1. eval = eval_final
[PROOF STEP]
from wrapC_unwrapC_id unwrapC_strict
[PROOF STATE]
proof (chain)
picking this:
wrapC oo unwrapC = ID
unwrapC\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
have "\<dots> = wrapC\<cdot>(fix\<cdot>eval_body_final)"
[PROOF STATE]
proof (prove)
using this:
wrapC oo unwrapC = ID
unwrapC\<cdot>\<bottom> = \<bottom>

goal (1 subgoal):
 1. fix\<cdot>eval_body = wrapC\<cdot>(fix\<cdot>eval_body_final)
[PROOF STEP]
apply (rule worker_wrapper_fusion_new)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unwrapC oo eval_body oo wrapC = eval_body_final oo unwrapC oo wrapC
[PROOF STEP]
using eval_body'_eval_body_final_eq eval_body'_eval_body_eq
[PROOF STATE]
proof (prove)
using this:
eval_body_final oo unwrapC oo wrapC = eval_body'
eval_body' = unwrapC oo eval_body oo wrapC

goal (1 subgoal):
 1. unwrapC oo eval_body oo wrapC = eval_body_final oo unwrapC oo wrapC
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fix\<cdot>eval_body = wrapC\<cdot>(fix\<cdot>eval_body_final)

goal (1 subgoal):
 1. eval = eval_final
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fix\<cdot>eval_body = wrapC\<cdot>(fix\<cdot>eval_body_final)

goal (1 subgoal):
 1. eval = eval_final
[PROOF STEP]
have "\<dots> = eval_final"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrapC\<cdot>(fix\<cdot>eval_body_final) = eval_final
[PROOF STEP]
unfolding eval_final_def eval_work_final_def wrapC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> g e. g\<cdot>e\<cdot>Just\<cdot>Nothing)\<cdot>(fix\<cdot>eval_body_final) = (\<Lambda> e. fix\<cdot>eval_body_final\<cdot>e\<cdot>Just\<cdot>Nothing)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wrapC\<cdot>(fix\<cdot>eval_body_final) = eval_final

goal (1 subgoal):
 1. eval = eval_final
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
eval = eval_final
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval = eval_final

goal (1 subgoal):
 1. eval = eval_final
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
eval = eval_final

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma apfst_fst_snd: "apfst f x = (f (fst x), snd x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apfst f x = (f (fst x), snd x)
[PROOF STEP]
by (rule apfst_conv[of _ "fst x" "snd x" for x, unfolded prod.collapse])


[STATEMENT]
lemma apfst_comp_rpair_const: "apfst f \<circ> (\<lambda>x. (x, y)) = (\<lambda>x. (x, y)) \<circ> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apfst f \<circ> (\<lambda>x. (x, y)) = (\<lambda>x. (x, y)) \<circ> f
[PROOF STEP]
by (simp add: comp_def)


[STATEMENT]
lemma length_remove1_less[termination_simp]: "x \<in> set xs \<Longrightarrow> length (remove1 x xs) < length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> length (remove1 x xs) < length xs
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma map_filter_neq_eq_filter_map:
  "map f (filter (\<lambda>y. f x \<noteq> f y) xs) = filter (\<lambda>z. f x \<noteq> z) (map f xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f (filter (\<lambda>y. f x \<noteq> f y) xs) = filter ((\<noteq>) (f x)) (map f xs)
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma mset_map_remdups_gen:
  "mset (map f (remdups_gen f xs)) = mset (remdups_gen (\<lambda>x. x) (map f xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (map f (remdups_gen f xs)) = mset (remdups_gen (\<lambda>x. x) (map f xs))
[PROOF STEP]
by (induct f xs rule: remdups_gen.induct) (auto simp: map_filter_neq_eq_filter_map)


[STATEMENT]
lemma mset_remdups_gen_ident: "mset (remdups_gen (\<lambda>x. x) xs) = mset_set (set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (remdups_gen (\<lambda>x. x) xs) = mset_set (set xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mset (remdups_gen (\<lambda>x. x) xs) = mset_set (set xs)
[PROOF STEP]
have "f = (\<lambda>x. x) \<Longrightarrow> mset (remdups_gen f xs) = mset_set (set xs)" for f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = (\<lambda>x. x) \<Longrightarrow> mset (remdups_gen f xs) = mset_set (set xs)
[PROOF STEP]
proof (induct f xs rule: remdups_gen.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f. f = (\<lambda>x. x) \<Longrightarrow> mset (remdups_gen f []) = mset_set (set [])
 2. \<And>f x xs. \<lbrakk>f = (\<lambda>x. x) \<Longrightarrow> mset (remdups_gen f (filter (\<lambda>y. f x \<noteq> f y) xs)) = mset_set (set (filter (\<lambda>y. f x \<noteq> f y) xs)); f = (\<lambda>x. x)\<rbrakk> \<Longrightarrow> mset (remdups_gen f (x # xs)) = mset_set (set (x # xs))
[PROOF STEP]
case (2 f x xs)
[PROOF STATE]
proof (state)
this:
f = (\<lambda>x. x) \<Longrightarrow> mset (remdups_gen f (filter (\<lambda>y. f x \<noteq> f y) xs)) = mset_set (set (filter (\<lambda>y. f x \<noteq> f y) xs))
f = (\<lambda>x. x)

goal (2 subgoals):
 1. \<And>f. f = (\<lambda>x. x) \<Longrightarrow> mset (remdups_gen f []) = mset_set (set [])
 2. \<And>f x xs. \<lbrakk>f = (\<lambda>x. x) \<Longrightarrow> mset (remdups_gen f (filter (\<lambda>y. f x \<noteq> f y) xs)) = mset_set (set (filter (\<lambda>y. f x \<noteq> f y) xs)); f = (\<lambda>x. x)\<rbrakk> \<Longrightarrow> mset (remdups_gen f (x # xs)) = mset_set (set (x # xs))
[PROOF STEP]
note ih = this(1) and f = this(2)
[PROOF STATE]
proof (state)
this:
f = (\<lambda>x. x) \<Longrightarrow> mset (remdups_gen f (filter (\<lambda>y. f x \<noteq> f y) xs)) = mset_set (set (filter (\<lambda>y. f x \<noteq> f y) xs))
f = (\<lambda>x. x)

goal (2 subgoals):
 1. \<And>f. f = (\<lambda>x. x) \<Longrightarrow> mset (remdups_gen f []) = mset_set (set [])
 2. \<And>f x xs. \<lbrakk>f = (\<lambda>x. x) \<Longrightarrow> mset (remdups_gen f (filter (\<lambda>y. f x \<noteq> f y) xs)) = mset_set (set (filter (\<lambda>y. f x \<noteq> f y) xs)); f = (\<lambda>x. x)\<rbrakk> \<Longrightarrow> mset (remdups_gen f (x # xs)) = mset_set (set (x # xs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (remdups_gen f (x # xs)) = mset_set (set (x # xs))
[PROOF STEP]
unfolding f remdups_gen.simps ih[OF f, unfolded f] mset.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_mset x (mset_set (set (filter ((\<noteq>) x) xs))) = mset_set (set (x # xs))
[PROOF STEP]
by (metis finite_set list.simps(15) mset_set.insert_remove removeAll_filter_not_eq
          remove_code(1) remove_def)
[PROOF STATE]
proof (state)
this:
mset (remdups_gen f (x # xs)) = mset_set (set (x # xs))

goal (1 subgoal):
 1. \<And>f. f = (\<lambda>x. x) \<Longrightarrow> mset (remdups_gen f []) = mset_set (set [])
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
?f = (\<lambda>x. x) \<Longrightarrow> mset (remdups_gen ?f xs) = mset_set (set xs)

goal (1 subgoal):
 1. mset (remdups_gen (\<lambda>x. x) xs) = mset_set (set xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?f = (\<lambda>x. x) \<Longrightarrow> mset (remdups_gen ?f xs) = mset_set (set xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?f = (\<lambda>x. x) \<Longrightarrow> mset (remdups_gen ?f xs) = mset_set (set xs)

goal (1 subgoal):
 1. mset (remdups_gen (\<lambda>x. x) xs) = mset_set (set xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mset (remdups_gen (\<lambda>x. x) xs) = mset_set (set xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma funpow_fixpoint: "f x = x \<Longrightarrow> (f ^^ n) x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x = x \<Longrightarrow> (f ^^ n) x = x
[PROOF STEP]
by (induct n) auto


[STATEMENT]
lemma rtranclp_imp_eq_image: "(\<forall>x y. R x y \<longrightarrow> f x = f y) \<Longrightarrow> R\<^sup>*\<^sup>* x y \<Longrightarrow> f x = f y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x y. R x y \<longrightarrow> f x = f y; R\<^sup>*\<^sup>* x y\<rbrakk> \<Longrightarrow> f x = f y
[PROOF STEP]
by (erule rtranclp.induct) auto


[STATEMENT]
lemma tranclp_imp_eq_image: "(\<forall>x y. R x y \<longrightarrow> f x = f y) \<Longrightarrow> R\<^sup>+\<^sup>+ x y \<Longrightarrow> f x = f y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x y. R x y \<longrightarrow> f x = f y; R\<^sup>+\<^sup>+ x y\<rbrakk> \<Longrightarrow> f x = f y
[PROOF STEP]
by (erule tranclp.induct) auto


[STATEMENT]
lemma less_atm_irrefl: "\<not> less_atm A A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> less_atm A A
[PROOF STEP]
using ex_ground_subst less_atm_ground less_atm_stable
[PROOF STATE]
proof (prove)
using this:
Ex is_ground_subst
\<lbrakk>is_ground_atm ?A; is_ground_atm ?B; less_atm ?A ?B\<rbrakk> \<Longrightarrow> ?A < ?B
less_atm ?A ?B \<Longrightarrow> less_atm (?A \<cdot>a ?\<sigma>) (?B \<cdot>a ?\<sigma>)

goal (1 subgoal):
 1. \<not> less_atm A A
[PROOF STEP]
unfolding is_ground_subst_def
[PROOF STATE]
proof (prove)
using this:
\<exists>\<sigma>. \<forall>A. is_ground_atm (A \<cdot>a \<sigma>)
\<lbrakk>is_ground_atm ?A; is_ground_atm ?B; less_atm ?A ?B\<rbrakk> \<Longrightarrow> ?A < ?B
less_atm ?A ?B \<Longrightarrow> less_atm (?A \<cdot>a ?\<sigma>) (?B \<cdot>a ?\<sigma>)

goal (1 subgoal):
 1. \<not> less_atm A A
[PROOF STEP]
by blast


[STATEMENT]
lemma remove_all_mset_minus: "mset ys \<subseteq># mset xs \<Longrightarrow> mset (remove_all xs ys) = mset xs - mset ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset ys \<subseteq># mset xs \<Longrightarrow> mset (remove_all xs ys) = mset xs - mset ys
[PROOF STEP]
proof (induction ys arbitrary: xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs. mset [] \<subseteq># mset xs \<Longrightarrow> mset (remove_all xs []) = mset xs - mset []
 2. \<And>a ys xs. \<lbrakk>\<And>xs. mset ys \<subseteq># mset xs \<Longrightarrow> mset (remove_all xs ys) = mset xs - mset ys; mset (a # ys) \<subseteq># mset xs\<rbrakk> \<Longrightarrow> mset (remove_all xs (a # ys)) = mset xs - mset (a # ys)
[PROOF STEP]
case (Cons y ys)
[PROOF STATE]
proof (state)
this:
mset ys \<subseteq># mset ?xs \<Longrightarrow> mset (remove_all ?xs ys) = mset ?xs - mset ys
mset (y # ys) \<subseteq># mset xs

goal (2 subgoals):
 1. \<And>xs. mset [] \<subseteq># mset xs \<Longrightarrow> mset (remove_all xs []) = mset xs - mset []
 2. \<And>a ys xs. \<lbrakk>\<And>xs. mset ys \<subseteq># mset xs \<Longrightarrow> mset (remove_all xs ys) = mset xs - mset ys; mset (a # ys) \<subseteq># mset xs\<rbrakk> \<Longrightarrow> mset (remove_all xs (a # ys)) = mset xs - mset (a # ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (remove_all xs (y # ys)) = mset xs - mset (y # ys)
[PROOF STEP]
proof (cases "y \<in> set xs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y \<in> set xs \<Longrightarrow> mset (remove_all xs (y # ys)) = mset xs - mset (y # ys)
 2. y \<notin> set xs \<Longrightarrow> mset (remove_all xs (y # ys)) = mset xs - mset (y # ys)
[PROOF STEP]
case y_in: True
[PROOF STATE]
proof (state)
this:
y \<in> set xs

goal (2 subgoals):
 1. y \<in> set xs \<Longrightarrow> mset (remove_all xs (y # ys)) = mset xs - mset (y # ys)
 2. y \<notin> set xs \<Longrightarrow> mset (remove_all xs (y # ys)) = mset xs - mset (y # ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> set xs
[PROOF STEP]
have subs: "mset ys \<subseteq># mset (remove1 y xs)"
[PROOF STATE]
proof (prove)
using this:
y \<in> set xs

goal (1 subgoal):
 1. mset ys \<subseteq># mset (remove1 y xs)
[PROOF STEP]
using Cons(2)
[PROOF STATE]
proof (prove)
using this:
y \<in> set xs
mset (y # ys) \<subseteq># mset xs

goal (1 subgoal):
 1. mset ys \<subseteq># mset (remove1 y xs)
[PROOF STEP]
by (simp add: insert_subset_eq_iff)
[PROOF STATE]
proof (state)
this:
mset ys \<subseteq># mset (remove1 y xs)

goal (2 subgoals):
 1. y \<in> set xs \<Longrightarrow> mset (remove_all xs (y # ys)) = mset xs - mset (y # ys)
 2. y \<notin> set xs \<Longrightarrow> mset (remove_all xs (y # ys)) = mset xs - mset (y # ys)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (remove_all xs (y # ys)) = mset xs - mset (y # ys)
[PROOF STEP]
using y_in Cons subs
[PROOF STATE]
proof (prove)
using this:
y \<in> set xs
mset ys \<subseteq># mset ?xs \<Longrightarrow> mset (remove_all ?xs ys) = mset ?xs - mset ys
mset (y # ys) \<subseteq># mset xs
mset ys \<subseteq># mset (remove1 y xs)

goal (1 subgoal):
 1. mset (remove_all xs (y # ys)) = mset xs - mset (y # ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset (remove_all xs (y # ys)) = mset xs - mset (y # ys)

goal (1 subgoal):
 1. y \<notin> set xs \<Longrightarrow> mset (remove_all xs (y # ys)) = mset xs - mset (y # ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<notin> set xs \<Longrightarrow> mset (remove_all xs (y # ys)) = mset xs - mset (y # ys)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
y \<notin> set xs

goal (1 subgoal):
 1. y \<notin> set xs \<Longrightarrow> mset (remove_all xs (y # ys)) = mset xs - mset (y # ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<notin> set xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<notin> set xs

goal (1 subgoal):
 1. mset (remove_all xs (y # ys)) = mset xs - mset (y # ys)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
y \<notin> set xs
mset ys \<subseteq># mset ?xs \<Longrightarrow> mset (remove_all ?xs ys) = mset ?xs - mset ys
mset (y # ys) \<subseteq># mset xs

goal (1 subgoal):
 1. mset (remove_all xs (y # ys)) = mset xs - mset (y # ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset (remove_all xs (y # ys)) = mset xs - mset (y # ys)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mset (remove_all xs (y # ys)) = mset xs - mset (y # ys)

goal (1 subgoal):
 1. \<And>xs. mset [] \<subseteq># mset xs \<Longrightarrow> mset (remove_all xs []) = mset xs - mset []
[PROOF STEP]
qed auto


[STATEMENT]
lemma select_min_weight_clause_in: "select_min_weight_clause P0 P \<in> set (P0 # P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. select_min_weight_clause P0 P \<in> set (P0 # P)
[PROOF STEP]
by (induct P arbitrary: P0) auto


[STATEMENT]
lemma is_final_dstate_funpow_imp_deterministic_RP_neq_None:
  "is_final_dstate ((deterministic_RP_step ^^ k) St) \<Longrightarrow> deterministic_RP St \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_final_dstate ((deterministic_RP_step ^^ k) St) \<Longrightarrow> deterministic_RP St \<noteq> None
[PROOF STEP]
proof (induct k arbitrary: St)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>St. is_final_dstate ((deterministic_RP_step ^^ 0) St) \<Longrightarrow> deterministic_RP St \<noteq> None
 2. \<And>k St. \<lbrakk>\<And>St. is_final_dstate ((deterministic_RP_step ^^ k) St) \<Longrightarrow> deterministic_RP St \<noteq> None; is_final_dstate ((deterministic_RP_step ^^ Suc k) St)\<rbrakk> \<Longrightarrow> deterministic_RP St \<noteq> None
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
is_final_dstate ((deterministic_RP_step ^^ k) ?St) \<Longrightarrow> deterministic_RP ?St \<noteq> None
is_final_dstate ((deterministic_RP_step ^^ Suc k) St)

goal (2 subgoals):
 1. \<And>St. is_final_dstate ((deterministic_RP_step ^^ 0) St) \<Longrightarrow> deterministic_RP St \<noteq> None
 2. \<And>k St. \<lbrakk>\<And>St. is_final_dstate ((deterministic_RP_step ^^ k) St) \<Longrightarrow> deterministic_RP St \<noteq> None; is_final_dstate ((deterministic_RP_step ^^ Suc k) St)\<rbrakk> \<Longrightarrow> deterministic_RP St \<noteq> None
[PROOF STEP]
note ih = this(1) and final_Sk = this(2)[simplified, unfolded funpow_swap1]
[PROOF STATE]
proof (state)
this:
is_final_dstate ((deterministic_RP_step ^^ k) ?St) \<Longrightarrow> deterministic_RP ?St \<noteq> None
is_final_dstate ((deterministic_RP_step ^^ k) (deterministic_RP_step St))

goal (2 subgoals):
 1. \<And>St. is_final_dstate ((deterministic_RP_step ^^ 0) St) \<Longrightarrow> deterministic_RP St \<noteq> None
 2. \<And>k St. \<lbrakk>\<And>St. is_final_dstate ((deterministic_RP_step ^^ k) St) \<Longrightarrow> deterministic_RP St \<noteq> None; is_final_dstate ((deterministic_RP_step ^^ Suc k) St)\<rbrakk> \<Longrightarrow> deterministic_RP St \<noteq> None
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deterministic_RP St \<noteq> None
[PROOF STEP]
using ih[OF final_Sk]
[PROOF STATE]
proof (prove)
using this:
deterministic_RP (deterministic_RP_step St) \<noteq> None

goal (1 subgoal):
 1. deterministic_RP St \<noteq> None
[PROOF STEP]
by (subst deterministic_RP.simps) (simp add: prod.case_eq_if)
[PROOF STATE]
proof (state)
this:
deterministic_RP St \<noteq> None

goal (1 subgoal):
 1. \<And>St. is_final_dstate ((deterministic_RP_step ^^ 0) St) \<Longrightarrow> deterministic_RP St \<noteq> None
[PROOF STEP]
qed (subst deterministic_RP.simps, simp add: prod.case_eq_if)


[STATEMENT]
lemma is_reducible_lit_mono_cls:
  "mset C \<subseteq># mset C' \<Longrightarrow> is_reducible_lit Ds C L \<Longrightarrow> is_reducible_lit Ds C' L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mset C \<subseteq># mset C'; is_reducible_lit Ds C L\<rbrakk> \<Longrightarrow> is_reducible_lit Ds C' L
[PROOF STEP]
unfolding is_reducible_lit_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mset C \<subseteq># mset C'; \<exists>D\<in>set Ds. \<exists>L'\<in>set D. \<exists>\<sigma>. - L = L' \<cdot>l \<sigma> \<and> mset (remove1 L' D) \<cdot> \<sigma> \<subseteq># mset C\<rbrakk> \<Longrightarrow> \<exists>D\<in>set Ds. \<exists>L'\<in>set D. \<exists>\<sigma>. - L = L' \<cdot>l \<sigma> \<and> mset (remove1 L' D) \<cdot> \<sigma> \<subseteq># mset C'
[PROOF STEP]
by (blast intro: subset_mset.trans)


[STATEMENT]
lemma is_reducible_lit_mset_iff:
  "mset C = mset C' \<Longrightarrow> is_reducible_lit Ds C' L \<longleftrightarrow> is_reducible_lit Ds C L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset C = mset C' \<Longrightarrow> is_reducible_lit Ds C' L = is_reducible_lit Ds C L
[PROOF STEP]
by (metis is_reducible_lit_mono_cls subset_mset.order_refl)