[STATEMENT]
lemma ReachableSplit[rule_format]:
  "(M, l,s, k, t) \<in> Reachable \<Longrightarrow>
    1 \<le> k \<longrightarrow>
   ((\<exists> n m r ll. (M,l,s,n,ll,r):Step \<and>
                 (M,ll,r,m,t):Reachable \<and> Suc m +n =k) \<or>
    (\<exists> n ops S h c m par R ops1 code l0.
          s=(ops,S,h) \<and> get_ins M l = Some (invokeS c m) \<and>
          mbody_is c m (par,code,l0) \<and> (ops,par,R,ops1):Frame \<and>
          ((par,code,l0), l0, ([],R,h), n, t):Reachable \<and> Suc n = k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, k, t) \<in> Reachable \<Longrightarrow> 1 \<le> k \<longrightarrow> (\<exists>n m r ll. (M, l, s, n, ll, r) \<in> Step \<and> (M, ll, r, m, t) \<in> Reachable \<and> Suc m + n = k) \<or> (\<exists>n ops S h c m par R ops1 code l0. s = (ops, S, h) \<and> get_ins M l = Some (invokeS c m) \<and> mbody_is c m (par, code, l0) \<and> (ops, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable \<and> Suc n = k)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, k, t) \<in> Reachable \<Longrightarrow> 1 \<le> k \<longrightarrow> (\<exists>n m r ll. (M, l, s, n, ll, r) \<in> Step \<and> (M, ll, r, m, t) \<in> Reachable \<and> Suc m + n = k) \<or> (\<exists>n ops S h c m par R ops1 code l0. s = (ops, S, h) \<and> get_ins M l = Some (invokeS c m) \<and> mbody_is c m (par, code, l0) \<and> (ops, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable \<and> Suc n = k)
[PROOF STEP]
apply (erule Reachable.induct, simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M l s n ll r m t k. \<lbrakk>(M, l, s, n, ll, r) \<in> Step; (M, ll, r, m, t) \<in> Reachable; Suc 0 \<le> m \<longrightarrow> (\<exists>n ma a aa b lla. (M, ll, r, n, lla, a, aa, b) \<in> Step \<and> (M, lla, (a, aa, b), ma, t) \<in> Reachable \<and> Suc (ma + n) = m) \<or> (\<exists>n ops S h. r = (ops, S, h) \<and> (\<exists>c ma. get_ins M ll = Some (invokeS c ma) \<and> (\<exists>par R ops1 code l0. mbody_is c ma (par, code, l0) \<and> (ops, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable \<and> Suc n = m))); k = Suc (m + n)\<rbrakk> \<Longrightarrow> (\<exists>na ma a aa b ll. (M, l, s, na, ll, a, aa, b) \<in> Step \<and> (M, ll, (a, aa, b), ma, t) \<in> Reachable \<and> ma + na = m + n) \<or> (\<exists>na ops S h. s = (ops, S, h) \<and> (\<exists>c ma. get_ins M l = Some (invokeS c ma) \<and> (\<exists>par R ops1 code l0. mbody_is c ma (par, code, l0) \<and> (ops, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), na, t) \<in> Reachable \<and> na = m + n)))
 2. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; Suc 0 \<le> n \<longrightarrow> (\<exists>na m a aa b ll. ((par, code, l0), l0, ([], R, h), na, ll, a, aa, b) \<in> Step \<and> ((par, code, l0), ll, (a, aa, b), m, t) \<in> Reachable \<and> Suc (m + na) = n) \<or> (\<exists>na c m. get_ins (par, code, l0) l0 = Some (invokeS c m) \<and> (\<exists>par R ops1 code l0. mbody_is c m (par, code, l0) \<and> ([], par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), na, t) \<in> Reachable \<and> Suc na = n)); k = Suc n\<rbrakk> \<Longrightarrow> (\<exists>na m a aa b ll. (M, l, (ops, S, h), na, ll, a, aa, b) \<in> Step \<and> (M, ll, (a, aa, b), m, t) \<in> Reachable \<and> m + na = n) \<or> (\<exists>par R ops1 code l0. mbody_is C m (par, code, l0) \<and> (ops, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b l ab ac ba n ll ad ae bb m af ag bc. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; ((a, aa, b), ll, (ad, ae, bb), m, af, ag, bc) \<in> Reachable; Suc 0 \<le> m \<longrightarrow> (\<exists>n ma ab ac ba lla. ((a, aa, b), ll, (ad, ae, bb), n, lla, ab, ac, ba) \<in> Step \<and> ((a, aa, b), lla, (ab, ac, ba), ma, af, ag, bc) \<in> Reachable \<and> Suc (ma + n) = m) \<or> (\<exists>n c ma. get_ins (a, aa, b) ll = Some (invokeS c ma) \<and> (\<exists>par R ops1 code l0. mbody_is c ma (par, code, l0) \<and> (ad, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, bb), n, af, ag, bc) \<in> Reachable \<and> Suc n = m)); \<forall>na c ma. get_ins (a, aa, b) l = Some (invokeS c ma) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, af, ag, bc) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c ma (par, code, l0) \<longrightarrow> na \<noteq> m + n)\<rbrakk> \<Longrightarrow> \<exists>na ma ad ae bb ll. ((a, aa, b), l, (ab, ac, ba), na, ll, ad, ae, bb) \<in> Step \<and> ((a, aa, b), ll, (ad, ae, bb), ma, af, ag, bc) \<in> Reachable \<and> ma + na = m + n
 2. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; Suc 0 \<le> n \<longrightarrow> (\<exists>na m a aa b ll. ((par, code, l0), l0, ([], R, h), na, ll, a, aa, b) \<in> Step \<and> ((par, code, l0), ll, (a, aa, b), m, t) \<in> Reachable \<and> Suc (m + na) = n) \<or> (\<exists>na c m. get_ins (par, code, l0) l0 = Some (invokeS c m) \<and> (\<exists>par R ops1 code l0. mbody_is c m (par, code, l0) \<and> ([], par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), na, t) \<in> Reachable \<and> Suc na = n)); k = Suc n\<rbrakk> \<Longrightarrow> (\<exists>na m a aa b ll. (M, l, (ops, S, h), na, ll, a, aa, b) \<in> Step \<and> (M, ll, (a, aa, b), m, t) \<in> Reachable \<and> m + na = n) \<or> (\<exists>par R ops1 code l0. mbody_is C m (par, code, l0) \<and> (ops, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable)
[PROOF STEP]
apply (case_tac m, clarsimp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a aa b l ab ac ba n ll ad ae bb af ag bc. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; ((a, aa, b), ll, (ad, ae, bb), 0, af, ag, bc) \<in> Reachable; \<forall>na c m. get_ins (a, aa, b) l = Some (invokeS c m) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, af, ag, bc) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c m (par, code, l0) \<longrightarrow> na \<noteq> n)\<rbrakk> \<Longrightarrow> \<exists>na m ad ae bb ll. ((a, aa, b), l, (ab, ac, ba), na, ll, ad, ae, bb) \<in> Step \<and> ((a, aa, b), ll, (ad, ae, bb), m, af, ag, bc) \<in> Reachable \<and> m + na = n
 2. \<And>a aa b l ab ac ba n ll ad ae bb m af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; ((a, aa, b), ll, (ad, ae, bb), m, af, ag, bc) \<in> Reachable; Suc 0 \<le> m \<longrightarrow> (\<exists>n ma ab ac ba lla. ((a, aa, b), ll, (ad, ae, bb), n, lla, ab, ac, ba) \<in> Step \<and> ((a, aa, b), lla, (ab, ac, ba), ma, af, ag, bc) \<in> Reachable \<and> Suc (ma + n) = m) \<or> (\<exists>n c ma. get_ins (a, aa, b) ll = Some (invokeS c ma) \<and> (\<exists>par R ops1 code l0. mbody_is c ma (par, code, l0) \<and> (ad, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, bb), n, af, ag, bc) \<in> Reachable \<and> Suc n = m)); \<forall>na c ma. get_ins (a, aa, b) l = Some (invokeS c ma) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, af, ag, bc) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c ma (par, code, l0) \<longrightarrow> na \<noteq> m + n); m = Suc nat\<rbrakk> \<Longrightarrow> \<exists>na ma ad ae bb ll. ((a, aa, b), l, (ab, ac, ba), na, ll, ad, ae, bb) \<in> Step \<and> ((a, aa, b), ll, (ad, ae, bb), ma, af, ag, bc) \<in> Reachable \<and> ma + na = m + n
 3. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; Suc 0 \<le> n \<longrightarrow> (\<exists>na m a aa b ll. ((par, code, l0), l0, ([], R, h), na, ll, a, aa, b) \<in> Step \<and> ((par, code, l0), ll, (a, aa, b), m, t) \<in> Reachable \<and> Suc (m + na) = n) \<or> (\<exists>na c m. get_ins (par, code, l0) l0 = Some (invokeS c m) \<and> (\<exists>par R ops1 code l0. mbody_is c m (par, code, l0) \<and> ([], par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), na, t) \<in> Reachable \<and> Suc na = n)); k = Suc n\<rbrakk> \<Longrightarrow> (\<exists>na m a aa b ll. (M, l, (ops, S, h), na, ll, a, aa, b) \<in> Step \<and> (M, ll, (a, aa, b), m, t) \<in> Reachable \<and> m + na = n) \<or> (\<exists>par R ops1 code l0. mbody_is C m (par, code, l0) \<and> (ops, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable)
[PROOF STEP]
apply (drule ZeroHeightReachableElim[simplified], clarsimp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a aa b l ab ac ba n ll ad ae bb. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; \<forall>na c m. get_ins (a, aa, b) l = Some (invokeS c m) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, ad, ae, bb) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c m (par, code, l0) \<longrightarrow> na \<noteq> n)\<rbrakk> \<Longrightarrow> \<exists>na m af ag bc ll. ((a, aa, b), l, (ab, ac, ba), na, ll, af, ag, bc) \<in> Step \<and> ((a, aa, b), ll, (af, ag, bc), m, ad, ae, bb) \<in> Reachable \<and> m + na = n
 2. \<And>a aa b l ab ac ba n ll ad ae bb m af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; ((a, aa, b), ll, (ad, ae, bb), m, af, ag, bc) \<in> Reachable; Suc 0 \<le> m \<longrightarrow> (\<exists>n ma ab ac ba lla. ((a, aa, b), ll, (ad, ae, bb), n, lla, ab, ac, ba) \<in> Step \<and> ((a, aa, b), lla, (ab, ac, ba), ma, af, ag, bc) \<in> Reachable \<and> Suc (ma + n) = m) \<or> (\<exists>n c ma. get_ins (a, aa, b) ll = Some (invokeS c ma) \<and> (\<exists>par R ops1 code l0. mbody_is c ma (par, code, l0) \<and> (ad, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, bb), n, af, ag, bc) \<in> Reachable \<and> Suc n = m)); \<forall>na c ma. get_ins (a, aa, b) l = Some (invokeS c ma) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, af, ag, bc) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c ma (par, code, l0) \<longrightarrow> na \<noteq> m + n); m = Suc nat\<rbrakk> \<Longrightarrow> \<exists>na ma ad ae bb ll. ((a, aa, b), l, (ab, ac, ba), na, ll, ad, ae, bb) \<in> Step \<and> ((a, aa, b), ll, (ad, ae, bb), ma, af, ag, bc) \<in> Reachable \<and> ma + na = m + n
 3. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; Suc 0 \<le> n \<longrightarrow> (\<exists>na m a aa b ll. ((par, code, l0), l0, ([], R, h), na, ll, a, aa, b) \<in> Step \<and> ((par, code, l0), ll, (a, aa, b), m, t) \<in> Reachable \<and> Suc (m + na) = n) \<or> (\<exists>na c m. get_ins (par, code, l0) l0 = Some (invokeS c m) \<and> (\<exists>par R ops1 code l0. mbody_is c m (par, code, l0) \<and> ([], par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), na, t) \<in> Reachable \<and> Suc na = n)); k = Suc n\<rbrakk> \<Longrightarrow> (\<exists>na m a aa b ll. (M, l, (ops, S, h), na, ll, a, aa, b) \<in> Step \<and> (M, ll, (a, aa, b), m, t) \<in> Reachable \<and> m + na = n) \<or> (\<exists>par R ops1 code l0. mbody_is C m (par, code, l0) \<and> (ops, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable)
[PROOF STEP]
apply (rule, rule,rule, rule,rule, rule, rule, assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a aa b l ab ac ba n ll ad ae bb. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; \<forall>na c m. get_ins (a, aa, b) l = Some (invokeS c m) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, ad, ae, bb) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c m (par, code, l0) \<longrightarrow> na \<noteq> n)\<rbrakk> \<Longrightarrow> ((a, aa, b), ll, (ad, ae, bb), ?m19 a aa b l ab ac ba n ll ad ae bb, ad, ae, bb) \<in> Reachable \<and> ?m19 a aa b l ab ac ba n ll ad ae bb + n = n
 2. \<And>a aa b l ab ac ba n ll ad ae bb m af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; ((a, aa, b), ll, (ad, ae, bb), m, af, ag, bc) \<in> Reachable; Suc 0 \<le> m \<longrightarrow> (\<exists>n ma ab ac ba lla. ((a, aa, b), ll, (ad, ae, bb), n, lla, ab, ac, ba) \<in> Step \<and> ((a, aa, b), lla, (ab, ac, ba), ma, af, ag, bc) \<in> Reachable \<and> Suc (ma + n) = m) \<or> (\<exists>n c ma. get_ins (a, aa, b) ll = Some (invokeS c ma) \<and> (\<exists>par R ops1 code l0. mbody_is c ma (par, code, l0) \<and> (ad, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, bb), n, af, ag, bc) \<in> Reachable \<and> Suc n = m)); \<forall>na c ma. get_ins (a, aa, b) l = Some (invokeS c ma) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, af, ag, bc) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c ma (par, code, l0) \<longrightarrow> na \<noteq> m + n); m = Suc nat\<rbrakk> \<Longrightarrow> \<exists>na ma ad ae bb ll. ((a, aa, b), l, (ab, ac, ba), na, ll, ad, ae, bb) \<in> Step \<and> ((a, aa, b), ll, (ad, ae, bb), ma, af, ag, bc) \<in> Reachable \<and> ma + na = m + n
 3. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; Suc 0 \<le> n \<longrightarrow> (\<exists>na m a aa b ll. ((par, code, l0), l0, ([], R, h), na, ll, a, aa, b) \<in> Step \<and> ((par, code, l0), ll, (a, aa, b), m, t) \<in> Reachable \<and> Suc (m + na) = n) \<or> (\<exists>na c m. get_ins (par, code, l0) l0 = Some (invokeS c m) \<and> (\<exists>par R ops1 code l0. mbody_is c m (par, code, l0) \<and> ([], par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), na, t) \<in> Reachable \<and> Suc na = n)); k = Suc n\<rbrakk> \<Longrightarrow> (\<exists>na m a aa b ll. (M, l, (ops, S, h), na, ll, a, aa, b) \<in> Step \<and> (M, ll, (a, aa, b), m, t) \<in> Reachable \<and> m + na = n) \<or> (\<exists>par R ops1 code l0. mbody_is C m (par, code, l0) \<and> (ops, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable)
[PROOF STEP]
apply (rule,rule Reachable_zero)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a aa b l ab ac ba n ll ad ae bb. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; \<forall>na c m. get_ins (a, aa, b) l = Some (invokeS c m) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, ad, ae, bb) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c m (par, code, l0) \<longrightarrow> na \<noteq> n)\<rbrakk> \<Longrightarrow> ?m19 a aa b l ab ac ba n ll ad ae bb = 0
 2. \<And>a aa b l ab ac ba n ll ad ae bb. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; \<forall>na c m. get_ins (a, aa, b) l = Some (invokeS c m) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, ad, ae, bb) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c m (par, code, l0) \<longrightarrow> na \<noteq> n)\<rbrakk> \<Longrightarrow> (ad, ae, bb) = (ad, ae, bb)
 3. \<And>a aa b l ab ac ba n ll ad ae bb. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; \<forall>na c m. get_ins (a, aa, b) l = Some (invokeS c m) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, ad, ae, bb) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c m (par, code, l0) \<longrightarrow> na \<noteq> n)\<rbrakk> \<Longrightarrow> ?m19 a aa b l ab ac ba n ll ad ae bb + n = n
 4. \<And>a aa b l ab ac ba n ll ad ae bb m af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; ((a, aa, b), ll, (ad, ae, bb), m, af, ag, bc) \<in> Reachable; Suc 0 \<le> m \<longrightarrow> (\<exists>n ma ab ac ba lla. ((a, aa, b), ll, (ad, ae, bb), n, lla, ab, ac, ba) \<in> Step \<and> ((a, aa, b), lla, (ab, ac, ba), ma, af, ag, bc) \<in> Reachable \<and> Suc (ma + n) = m) \<or> (\<exists>n c ma. get_ins (a, aa, b) ll = Some (invokeS c ma) \<and> (\<exists>par R ops1 code l0. mbody_is c ma (par, code, l0) \<and> (ad, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, bb), n, af, ag, bc) \<in> Reachable \<and> Suc n = m)); \<forall>na c ma. get_ins (a, aa, b) l = Some (invokeS c ma) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, af, ag, bc) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c ma (par, code, l0) \<longrightarrow> na \<noteq> m + n); m = Suc nat\<rbrakk> \<Longrightarrow> \<exists>na ma ad ae bb ll. ((a, aa, b), l, (ab, ac, ba), na, ll, ad, ae, bb) \<in> Step \<and> ((a, aa, b), ll, (ad, ae, bb), ma, af, ag, bc) \<in> Reachable \<and> ma + na = m + n
 5. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; Suc 0 \<le> n \<longrightarrow> (\<exists>na m a aa b ll. ((par, code, l0), l0, ([], R, h), na, ll, a, aa, b) \<in> Step \<and> ((par, code, l0), ll, (a, aa, b), m, t) \<in> Reachable \<and> Suc (m + na) = n) \<or> (\<exists>na c m. get_ins (par, code, l0) l0 = Some (invokeS c m) \<and> (\<exists>par R ops1 code l0. mbody_is c m (par, code, l0) \<and> ([], par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), na, t) \<in> Reachable \<and> Suc na = n)); k = Suc n\<rbrakk> \<Longrightarrow> (\<exists>na m a aa b ll. (M, l, (ops, S, h), na, ll, a, aa, b) \<in> Step \<and> (M, ll, (a, aa, b), m, t) \<in> Reachable \<and> m + na = n) \<or> (\<exists>par R ops1 code l0. mbody_is C m (par, code, l0) \<and> (ops, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a aa b l ab ac ba n ll ad ae bb. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; \<forall>na c m. get_ins (a, aa, b) l = Some (invokeS c m) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, ad, ae, bb) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c m (par, code, l0) \<longrightarrow> na \<noteq> n)\<rbrakk> \<Longrightarrow> (ad, ae, bb) = (ad, ae, bb)
 2. \<And>a aa b l ab ac ba n ll ad ae bb. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; \<forall>na c m. get_ins (a, aa, b) l = Some (invokeS c m) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, ad, ae, bb) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c m (par, code, l0) \<longrightarrow> na \<noteq> n)\<rbrakk> \<Longrightarrow> 0 + n = n
 3. \<And>a aa b l ab ac ba n ll ad ae bb m af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; ((a, aa, b), ll, (ad, ae, bb), m, af, ag, bc) \<in> Reachable; Suc 0 \<le> m \<longrightarrow> (\<exists>n ma ab ac ba lla. ((a, aa, b), ll, (ad, ae, bb), n, lla, ab, ac, ba) \<in> Step \<and> ((a, aa, b), lla, (ab, ac, ba), ma, af, ag, bc) \<in> Reachable \<and> Suc (ma + n) = m) \<or> (\<exists>n c ma. get_ins (a, aa, b) ll = Some (invokeS c ma) \<and> (\<exists>par R ops1 code l0. mbody_is c ma (par, code, l0) \<and> (ad, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, bb), n, af, ag, bc) \<in> Reachable \<and> Suc n = m)); \<forall>na c ma. get_ins (a, aa, b) l = Some (invokeS c ma) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, af, ag, bc) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c ma (par, code, l0) \<longrightarrow> na \<noteq> m + n); m = Suc nat\<rbrakk> \<Longrightarrow> \<exists>na ma ad ae bb ll. ((a, aa, b), l, (ab, ac, ba), na, ll, ad, ae, bb) \<in> Step \<and> ((a, aa, b), ll, (ad, ae, bb), ma, af, ag, bc) \<in> Reachable \<and> ma + na = m + n
 4. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; Suc 0 \<le> n \<longrightarrow> (\<exists>na m a aa b ll. ((par, code, l0), l0, ([], R, h), na, ll, a, aa, b) \<in> Step \<and> ((par, code, l0), ll, (a, aa, b), m, t) \<in> Reachable \<and> Suc (m + na) = n) \<or> (\<exists>na c m. get_ins (par, code, l0) l0 = Some (invokeS c m) \<and> (\<exists>par R ops1 code l0. mbody_is c m (par, code, l0) \<and> ([], par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), na, t) \<in> Reachable \<and> Suc na = n)); k = Suc n\<rbrakk> \<Longrightarrow> (\<exists>na m a aa b ll. (M, l, (ops, S, h), na, ll, a, aa, b) \<in> Step \<and> (M, ll, (a, aa, b), m, t) \<in> Reachable \<and> m + na = n) \<or> (\<exists>par R ops1 code l0. mbody_is C m (par, code, l0) \<and> (ops, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a aa b l ab ac ba n ll ad ae bb. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; \<forall>na c m. get_ins (a, aa, b) l = Some (invokeS c m) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, ad, ae, bb) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c m (par, code, l0) \<longrightarrow> na \<noteq> n)\<rbrakk> \<Longrightarrow> 0 + n = n
 2. \<And>a aa b l ab ac ba n ll ad ae bb m af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; ((a, aa, b), ll, (ad, ae, bb), m, af, ag, bc) \<in> Reachable; Suc 0 \<le> m \<longrightarrow> (\<exists>n ma ab ac ba lla. ((a, aa, b), ll, (ad, ae, bb), n, lla, ab, ac, ba) \<in> Step \<and> ((a, aa, b), lla, (ab, ac, ba), ma, af, ag, bc) \<in> Reachable \<and> Suc (ma + n) = m) \<or> (\<exists>n c ma. get_ins (a, aa, b) ll = Some (invokeS c ma) \<and> (\<exists>par R ops1 code l0. mbody_is c ma (par, code, l0) \<and> (ad, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, bb), n, af, ag, bc) \<in> Reachable \<and> Suc n = m)); \<forall>na c ma. get_ins (a, aa, b) l = Some (invokeS c ma) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, af, ag, bc) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c ma (par, code, l0) \<longrightarrow> na \<noteq> m + n); m = Suc nat\<rbrakk> \<Longrightarrow> \<exists>na ma ad ae bb ll. ((a, aa, b), l, (ab, ac, ba), na, ll, ad, ae, bb) \<in> Step \<and> ((a, aa, b), ll, (ad, ae, bb), ma, af, ag, bc) \<in> Reachable \<and> ma + na = m + n
 3. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; Suc 0 \<le> n \<longrightarrow> (\<exists>na m a aa b ll. ((par, code, l0), l0, ([], R, h), na, ll, a, aa, b) \<in> Step \<and> ((par, code, l0), ll, (a, aa, b), m, t) \<in> Reachable \<and> Suc (m + na) = n) \<or> (\<exists>na c m. get_ins (par, code, l0) l0 = Some (invokeS c m) \<and> (\<exists>par R ops1 code l0. mbody_is c m (par, code, l0) \<and> ([], par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), na, t) \<in> Reachable \<and> Suc na = n)); k = Suc n\<rbrakk> \<Longrightarrow> (\<exists>na m a aa b ll. (M, l, (ops, S, h), na, ll, a, aa, b) \<in> Step \<and> (M, ll, (a, aa, b), m, t) \<in> Reachable \<and> m + na = n) \<or> (\<exists>par R ops1 code l0. mbody_is C m (par, code, l0) \<and> (ops, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b l ab ac ba n ll ad ae bb m af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; ((a, aa, b), ll, (ad, ae, bb), m, af, ag, bc) \<in> Reachable; Suc 0 \<le> m \<longrightarrow> (\<exists>n ma ab ac ba lla. ((a, aa, b), ll, (ad, ae, bb), n, lla, ab, ac, ba) \<in> Step \<and> ((a, aa, b), lla, (ab, ac, ba), ma, af, ag, bc) \<in> Reachable \<and> Suc (ma + n) = m) \<or> (\<exists>n c ma. get_ins (a, aa, b) ll = Some (invokeS c ma) \<and> (\<exists>par R ops1 code l0. mbody_is c ma (par, code, l0) \<and> (ad, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, bb), n, af, ag, bc) \<in> Reachable \<and> Suc n = m)); \<forall>na c ma. get_ins (a, aa, b) l = Some (invokeS c ma) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, af, ag, bc) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c ma (par, code, l0) \<longrightarrow> na \<noteq> m + n); m = Suc nat\<rbrakk> \<Longrightarrow> \<exists>na ma ad ae bb ll. ((a, aa, b), l, (ab, ac, ba), na, ll, ad, ae, bb) \<in> Step \<and> ((a, aa, b), ll, (ad, ae, bb), ma, af, ag, bc) \<in> Reachable \<and> ma + na = m + n
 2. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; Suc 0 \<le> n \<longrightarrow> (\<exists>na m a aa b ll. ((par, code, l0), l0, ([], R, h), na, ll, a, aa, b) \<in> Step \<and> ((par, code, l0), ll, (a, aa, b), m, t) \<in> Reachable \<and> Suc (m + na) = n) \<or> (\<exists>na c m. get_ins (par, code, l0) l0 = Some (invokeS c m) \<and> (\<exists>par R ops1 code l0. mbody_is c m (par, code, l0) \<and> ([], par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), na, t) \<in> Reachable \<and> Suc na = n)); k = Suc n\<rbrakk> \<Longrightarrow> (\<exists>na m a aa b ll. (M, l, (ops, S, h), na, ll, a, aa, b) \<in> Step \<and> (M, ll, (a, aa, b), m, t) \<in> Reachable \<and> m + na = n) \<or> (\<exists>par R ops1 code l0. mbody_is C m (par, code, l0) \<and> (ops, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b l ab ac ba n ll ad ae bb af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; ((a, aa, b), ll, (ad, ae, bb), Suc nat, af, ag, bc) \<in> Reachable; (\<exists>n m ab ac ba lla. ((a, aa, b), ll, (ad, ae, bb), n, lla, ab, ac, ba) \<in> Step \<and> ((a, aa, b), lla, (ab, ac, ba), m, af, ag, bc) \<in> Reachable \<and> m + n = nat) \<or> (\<exists>n c m. get_ins (a, aa, b) ll = Some (invokeS c m) \<and> (\<exists>par R ops1 code l0. mbody_is c m (par, code, l0) \<and> (ad, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, bb), n, af, ag, bc) \<in> Reachable \<and> n = nat)); \<forall>na c m. get_ins (a, aa, b) l = Some (invokeS c m) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, af, ag, bc) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c m (par, code, l0) \<longrightarrow> na \<noteq> Suc (nat + n))\<rbrakk> \<Longrightarrow> \<exists>na m ad ae bb ll. ((a, aa, b), l, (ab, ac, ba), na, ll, ad, ae, bb) \<in> Step \<and> ((a, aa, b), ll, (ad, ae, bb), m, af, ag, bc) \<in> Reachable \<and> m + na = Suc (nat + n)
 2. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; Suc 0 \<le> n \<longrightarrow> (\<exists>na m a aa b ll. ((par, code, l0), l0, ([], R, h), na, ll, a, aa, b) \<in> Step \<and> ((par, code, l0), ll, (a, aa, b), m, t) \<in> Reachable \<and> Suc (m + na) = n) \<or> (\<exists>na c m. get_ins (par, code, l0) l0 = Some (invokeS c m) \<and> (\<exists>par R ops1 code l0. mbody_is c m (par, code, l0) \<and> ([], par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), na, t) \<in> Reachable \<and> Suc na = n)); k = Suc n\<rbrakk> \<Longrightarrow> (\<exists>na m a aa b ll. (M, l, (ops, S, h), na, ll, a, aa, b) \<in> Step \<and> (M, ll, (a, aa, b), m, t) \<in> Reachable \<and> m + na = n) \<or> (\<exists>par R ops1 code l0. mbody_is C m (par, code, l0) \<and> (ops, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable)
[PROOF STEP]
apply (rule, rule,rule, rule,rule, rule,rule,assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b l ab ac ba n ll ad ae bb af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; ((a, aa, b), ll, (ad, ae, bb), Suc nat, af, ag, bc) \<in> Reachable; (\<exists>n m ab ac ba lla. ((a, aa, b), ll, (ad, ae, bb), n, lla, ab, ac, ba) \<in> Step \<and> ((a, aa, b), lla, (ab, ac, ba), m, af, ag, bc) \<in> Reachable \<and> m + n = nat) \<or> (\<exists>n c m. get_ins (a, aa, b) ll = Some (invokeS c m) \<and> (\<exists>par R ops1 code l0. mbody_is c m (par, code, l0) \<and> (ad, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, bb), n, af, ag, bc) \<in> Reachable \<and> n = nat)); \<forall>na c m. get_ins (a, aa, b) l = Some (invokeS c m) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, af, ag, bc) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c m (par, code, l0) \<longrightarrow> na \<noteq> Suc (nat + n))\<rbrakk> \<Longrightarrow> ((a, aa, b), ll, (ad, ae, bb), ?m44 a aa b l ab ac ba n ll ad ae bb af ag bc nat, af, ag, bc) \<in> Reachable \<and> ?m44 a aa b l ab ac ba n ll ad ae bb af ag bc nat + n = Suc (nat + n)
 2. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; Suc 0 \<le> n \<longrightarrow> (\<exists>na m a aa b ll. ((par, code, l0), l0, ([], R, h), na, ll, a, aa, b) \<in> Step \<and> ((par, code, l0), ll, (a, aa, b), m, t) \<in> Reachable \<and> Suc (m + na) = n) \<or> (\<exists>na c m. get_ins (par, code, l0) l0 = Some (invokeS c m) \<and> (\<exists>par R ops1 code l0. mbody_is c m (par, code, l0) \<and> ([], par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), na, t) \<in> Reachable \<and> Suc na = n)); k = Suc n\<rbrakk> \<Longrightarrow> (\<exists>na m a aa b ll. (M, l, (ops, S, h), na, ll, a, aa, b) \<in> Step \<and> (M, ll, (a, aa, b), m, t) \<in> Reachable \<and> m + na = n) \<or> (\<exists>par R ops1 code l0. mbody_is C m (par, code, l0) \<and> (ops, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable)
[PROOF STEP]
apply (rule,assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b l ab ac ba n ll ad ae bb af ag bc nat. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; ((a, aa, b), ll, (ad, ae, bb), Suc nat, af, ag, bc) \<in> Reachable; (\<exists>n m ab ac ba lla. ((a, aa, b), ll, (ad, ae, bb), n, lla, ab, ac, ba) \<in> Step \<and> ((a, aa, b), lla, (ab, ac, ba), m, af, ag, bc) \<in> Reachable \<and> m + n = nat) \<or> (\<exists>n c m. get_ins (a, aa, b) ll = Some (invokeS c m) \<and> (\<exists>par R ops1 code l0. mbody_is c m (par, code, l0) \<and> (ad, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, bb), n, af, ag, bc) \<in> Reachable \<and> n = nat)); \<forall>na c m. get_ins (a, aa, b) l = Some (invokeS c m) \<longrightarrow> (\<forall>par R ops1 code l0. ((par, code, l0), l0, ([], R, ba), na, af, ag, bc) \<in> Reachable \<longrightarrow> (ab, par, R, ops1) \<in> Frame \<longrightarrow> mbody_is c m (par, code, l0) \<longrightarrow> na \<noteq> Suc (nat + n))\<rbrakk> \<Longrightarrow> Suc nat + n = Suc (nat + n)
 2. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; Suc 0 \<le> n \<longrightarrow> (\<exists>na m a aa b ll. ((par, code, l0), l0, ([], R, h), na, ll, a, aa, b) \<in> Step \<and> ((par, code, l0), ll, (a, aa, b), m, t) \<in> Reachable \<and> Suc (m + na) = n) \<or> (\<exists>na c m. get_ins (par, code, l0) l0 = Some (invokeS c m) \<and> (\<exists>par R ops1 code l0. mbody_is c m (par, code, l0) \<and> ([], par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), na, t) \<in> Reachable \<and> Suc na = n)); k = Suc n\<rbrakk> \<Longrightarrow> (\<exists>na m a aa b ll. (M, l, (ops, S, h), na, ll, a, aa, b) \<in> Step \<and> (M, ll, (a, aa, b), m, t) \<in> Reachable \<and> m + na = n) \<or> (\<exists>par R ops1 code l0. mbody_is C m (par, code, l0) \<and> (ops, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; Suc 0 \<le> n \<longrightarrow> (\<exists>na m a aa b ll. ((par, code, l0), l0, ([], R, h), na, ll, a, aa, b) \<in> Step \<and> ((par, code, l0), ll, (a, aa, b), m, t) \<in> Reachable \<and> Suc (m + na) = n) \<or> (\<exists>na c m. get_ins (par, code, l0) l0 = Some (invokeS c m) \<and> (\<exists>par R ops1 code l0. mbody_is c m (par, code, l0) \<and> ([], par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), na, t) \<in> Reachable \<and> Suc na = n)); k = Suc n\<rbrakk> \<Longrightarrow> (\<exists>na m a aa b ll. (M, l, (ops, S, h), na, ll, a, aa, b) \<in> Step \<and> (M, ll, (a, aa, b), m, t) \<in> Reachable \<and> m + na = n) \<or> (\<exists>par R ops1 code l0. mbody_is C m (par, code, l0) \<and> (ops, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable)
[PROOF STEP]
apply (rule disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; Suc 0 \<le> n \<longrightarrow> (\<exists>na m a aa b ll. ((par, code, l0), l0, ([], R, h), na, ll, a, aa, b) \<in> Step \<and> ((par, code, l0), ll, (a, aa, b), m, t) \<in> Reachable \<and> Suc (m + na) = n) \<or> (\<exists>na c m. get_ins (par, code, l0) l0 = Some (invokeS c m) \<and> (\<exists>par R ops1 code l0. mbody_is c m (par, code, l0) \<and> ([], par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), na, t) \<in> Reachable \<and> Suc na = n)); k = Suc n\<rbrakk> \<Longrightarrow> \<exists>par R ops1 code l0. mbody_is C m (par, code, l0) \<and> (ops, par, R, ops1) \<in> Frame \<and> ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Reachable_returnElim[rule_format]:
"(M,l,s,k,t) \<in> Reachable \<Longrightarrow> get_ins M l = Some vreturn \<longrightarrow> t=s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, k, t) \<in> Reachable \<Longrightarrow> get_ins M l = Some vreturn \<longrightarrow> t = s
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, l, s, k, t) \<in> Reachable \<Longrightarrow> get_ins M l = Some vreturn \<longrightarrow> t = s
[PROOF STEP]
apply (erule Reachable.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>k t s M l. \<lbrakk>k = 0; t = s\<rbrakk> \<Longrightarrow> get_ins M l = Some vreturn \<longrightarrow> t = s
 2. \<And>M l s n ll r m t k. \<lbrakk>(M, l, s, n, ll, r) \<in> Step; (M, ll, r, m, t) \<in> Reachable; get_ins M ll = Some vreturn \<longrightarrow> t = r; k = Suc m + n\<rbrakk> \<Longrightarrow> get_ins M l = Some vreturn \<longrightarrow> t = s
 3. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; get_ins (par, code, l0) l0 = Some vreturn \<longrightarrow> t = ([], R, h); k = Suc n\<rbrakk> \<Longrightarrow> get_ins M l = Some vreturn \<longrightarrow> t = s
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M l s n ll r m t k. \<lbrakk>(M, l, s, n, ll, r) \<in> Step; (M, ll, r, m, t) \<in> Reachable; get_ins M ll = Some vreturn \<longrightarrow> t = r; k = Suc m + n\<rbrakk> \<Longrightarrow> get_ins M l = Some vreturn \<longrightarrow> t = s
 2. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; get_ins (par, code, l0) l0 = Some vreturn \<longrightarrow> t = ([], R, h); k = Suc n\<rbrakk> \<Longrightarrow> get_ins M l = Some vreturn \<longrightarrow> t = s
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b l ab ac ba n ll ad ae bb m af ag bc. \<lbrakk>((a, aa, b), l, (ab, ac, ba), n, ll, ad, ae, bb) \<in> Step; ((a, aa, b), ll, (ad, ae, bb), m, af, ag, bc) \<in> Reachable; get_ins (a, aa, b) ll = Some vreturn \<longrightarrow> af = ad \<and> ag = ae \<and> bc = bb; get_ins (a, aa, b) l = Some vreturn\<rbrakk> \<Longrightarrow> af = ab \<and> ag = ac \<and> bc = ba
 2. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; get_ins (par, code, l0) l0 = Some vreturn \<longrightarrow> t = ([], R, h); k = Suc n\<rbrakk> \<Longrightarrow> get_ins M l = Some vreturn \<longrightarrow> t = s
[PROOF STEP]
apply (drule RetElim1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a aa b l ab ac ba n ll ad ae bb m af ag bc. \<lbrakk>((a, aa, b), ll, (ad, ae, bb), m, af, ag, bc) \<in> Reachable; get_ins (a, aa, b) ll = Some vreturn \<longrightarrow> af = ad \<and> ag = ae \<and> bc = bb; get_ins (a, aa, b) l = Some vreturn\<rbrakk> \<Longrightarrow> get_ins (a, aa, b) l = Some vreturn
 2. \<And>a aa b l ab ac ba n ll ad ae bb m af ag bc. \<lbrakk>((a, aa, b), ll, (ad, ae, bb), m, af, ag, bc) \<in> Reachable; get_ins (a, aa, b) ll = Some vreturn \<longrightarrow> af = ad \<and> ag = ae \<and> bc = bb; get_ins (a, aa, b) l = Some vreturn; False\<rbrakk> \<Longrightarrow> af = ab \<and> ag = ac \<and> bc = ba
 3. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; get_ins (par, code, l0) l0 = Some vreturn \<longrightarrow> t = ([], R, h); k = Suc n\<rbrakk> \<Longrightarrow> get_ins M l = Some vreturn \<longrightarrow> t = s
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b l ab ac ba n ll ad ae bb m af ag bc. \<lbrakk>((a, aa, b), ll, (ad, ae, bb), m, af, ag, bc) \<in> Reachable; get_ins (a, aa, b) ll = Some vreturn \<longrightarrow> af = ad \<and> ag = ae \<and> bc = bb; get_ins (a, aa, b) l = Some vreturn; False\<rbrakk> \<Longrightarrow> af = ab \<and> ag = ac \<and> bc = ba
 2. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; get_ins (par, code, l0) l0 = Some vreturn \<longrightarrow> t = ([], R, h); k = Suc n\<rbrakk> \<Longrightarrow> get_ins M l = Some vreturn \<longrightarrow> t = s
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C m par code l0 M l s ops S h R ops1 n t k. \<lbrakk>mbody_is C m (par, code, l0); get_ins M l = Some (invokeS C m); s = (ops, S, h); (ops, par, R, ops1) \<in> Frame; ((par, code, l0), l0, ([], R, h), n, t) \<in> Reachable; get_ins (par, code, l0) l0 = Some vreturn \<longrightarrow> t = ([], R, h); k = Suc n\<rbrakk> \<Longrightarrow> get_ins M l = Some vreturn \<longrightarrow> t = s
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma transform_simps:
  "\<T>\<^bsub>a\<^esub> (App e x) = App (\<T>\<^bsub>inc\<cdot>a\<^esub> e) x"
  "\<T>\<^bsub>a\<^esub> (Lam [x]. e) = Lam [x]. \<T>\<^bsub>pred\<cdot>a\<^esub> e"
  "\<T>\<^bsub>a\<^esub> (Var x) = Var x"
  "\<T>\<^bsub>a\<^esub> (Let \<Gamma> e) = Let (map_transform Aeta_expand (Aheap \<Gamma> e\<cdot>a) (map_transform (\<lambda>a. \<T>\<^bsub>a\<^esub>) (Aheap \<Gamma> e\<cdot>a) \<Gamma>)) (\<T>\<^bsub>a\<^esub> e)"
  "\<T>\<^bsub>a\<^esub> (Bool b) = Bool b"
  "\<T>\<^bsub>a\<^esub> (scrut ? e1 : e2) = (\<T>\<^bsub>0\<^esub> scrut ? \<T>\<^bsub>a\<^esub> e1 : \<T>\<^bsub>a\<^esub> e2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<T>\<^bsub>a\<^esub> (App e x) = App (\<T>\<^bsub>inc\<cdot>a\<^esub> e) x &&& \<T>\<^bsub>a\<^esub> (Lam [x]. e) = Lam [x]. \<T>\<^bsub>pred\<cdot>a\<^esub> e &&& \<T>\<^bsub>a\<^esub> (Var x) = Var x) &&& \<T>\<^bsub>a\<^esub> (Terms.Let \<Gamma> e) = Terms.Let (map_transform Aeta_expand (Aheap \<Gamma> e\<cdot>a) (map_transform transform_syn (Aheap \<Gamma> e\<cdot>a) \<Gamma>)) (\<T>\<^bsub>a\<^esub> e) &&& \<T>\<^bsub>a\<^esub> (Bool b) = Bool b &&& \<T>\<^bsub>a\<^esub> (scrut ? e1 : e2) = (\<T>\<^bsub>0\<^esub> scrut ? \<T>\<^bsub>a\<^esub> e1 : \<T>\<^bsub>a\<^esub> e2)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma short_circuit:
    "a\<and>b \<longleftrightarrow> (if a then b else False)"
    "a\<or>b \<longleftrightarrow> (if a then True else b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<and> b) = (if a then b else False) &&& (a \<or> b) = (if a then True else b)
[PROOF STEP]
by auto


[STATEMENT]
lemma BB_PROTECT_cong[named_ss vcg_bb cong]: "BB_PROTECT a = BB_PROTECT a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BB_PROTECT a = BB_PROTECT a
[PROOF STEP]
by simp


[STATEMENT]
lemma BB_PROTECT: "p \<equiv> BB_PROTECT p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<equiv> BB_PROTECT p
[PROOF STEP]
by (simp add: BB_PROTECT_def)


[STATEMENT]
lemma [unfolded short_circuit,named_ss vcg_bb]:
    fixes x y :: char and xs ys :: string
    shows
    "x#xs = y#ys \<longleftrightarrow> x=y \<and> xs=ys"
    "x#xs \<noteq> []" "[] \<noteq> x#xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs = y # ys) = (x = y \<and> xs = ys) &&& x # xs \<noteq> [] &&& [] \<noteq> x # xs
[PROOF STEP]
by auto


[STATEMENT]
lemma [named_ss vcg_bb]:
    fixes s::state
    shows
    "(s(x:=v)) x = v"
    "(s(x:=v)) y = (if x=y then v else s y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s(x := v)) x = v &&& (s(x := v)) y = (if x = y then v else s y)
[PROOF STEP]
by auto


[STATEMENT]
lemma [named_ss vcg_bb]:
    fixes a::val
    shows
    "(a(i:=pv)) i = pv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a(i := pv)) i = pv
[PROOF STEP]
by auto


[STATEMENT]
lemma combine_query': "<s|t> (x#xs) = (if is_global (x#xs) then t (x#xs) else s (x#xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <s|t> (x # xs) = (if is_global (x # xs) then t (x # xs) else s (x # xs))
[PROOF STEP]
by (auto simp: combine_query)


[STATEMENT]
lemma combine_upd':
    "<s|t>((x#xs):=v) = (if is_global (x#xs) then <s|t((x#xs):=v)> else <s((x#xs):=v)|t>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <s|t>(x # xs := v) = (if is_global (x # xs) then <s|t(x # xs := v)> else <s(x # xs := v)|t>)
[PROOF STEP]
by (auto simp: combine_upd)


[STATEMENT]
lemma query_prog[named_ss vcg_bb]: "(\<pi>(k\<mapsto>v)) k' = (if k'=k then Some v else \<pi> k')" for \<pi> :: program
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi>(k \<mapsto> v)) k' = (if k' = k then Some v else \<pi> k')
[PROOF STEP]
by auto


[STATEMENT]
lemma set_filter_simps[named_ss vcg_bb]:
    "Set.filter P {} = {}"
    "Set.filter P (insert x xs) = (if P x then insert x (Set.filter P xs) else Set.filter P xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Set.filter P {} = {} &&& Set.filter P (insert x xs) = (if P x then insert x (Set.filter P xs) else Set.filter P xs)
[PROOF STEP]
by auto


[STATEMENT]
lemma set_collect_simps[named_ss vcg_bb]:
    "Set.filter P UNIV = Collect P"
    "Set.filter P (Collect Q) = Collect (\<lambda>x. P x \<and> Q x)"
    "x\<in>UNIV"
    "x\<in>Collect P \<longleftrightarrow> P x"
    "insert x UNIV = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Set.filter P UNIV = Collect P &&& Set.filter P (Collect Q) = {x. P x \<and> Q x}) &&& x \<in> UNIV &&& (x \<in> Collect P) = P x &&& insert x UNIV = UNIV
[PROOF STEP]
by auto


[STATEMENT]
lemma applyUnitPropagateEffect:
assumes
  "InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)" and
  "InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)" and
  "InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)"

  "\<not> (getConflictFlag state)"
  "getQ state \<noteq> []"
shows
  "let uLiteral = hd (getQ state) in
   let state' = applyUnitPropagate state in
      \<exists> uClause. formulaEntailsClause (getF state) uClause \<and>
                 isUnitClause uClause uLiteral (elements (getM state)) \<and>
                 (getM state') = (getM state) @ [(uLiteral, False)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let uLiteral = hd (getQ state); state' = applyUnitPropagate state in \<exists>uClause. formulaEntailsClause (getF state) uClause \<and> isUnitClause uClause uLiteral (elements (getM state)) \<and> getM state' = getM state @ [(uLiteral, False)]
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let uLiteral = hd (getQ state); state' = applyUnitPropagate state in \<exists>uClause. formulaEntailsClause (getF state) uClause \<and> isUnitClause uClause uLiteral (elements (getM state)) \<and> getM state' = getM state @ [(uLiteral, False)]
[PROOF STEP]
let ?uLiteral = "hd (getQ state)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let uLiteral = hd (getQ state); state' = applyUnitPropagate state in \<exists>uClause. formulaEntailsClause (getF state) uClause \<and> isUnitClause uClause uLiteral (elements (getM state)) \<and> getM state' = getM state @ [(uLiteral, False)]
[PROOF STEP]
obtain uClause
    where "uClause el (getF state)" "isUnitClause uClause ?uLiteral (elements (getM state))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>uClause. \<lbrakk>uClause el getF state; isUnitClause uClause (hd (getQ state)) (elements (getM state))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
\<not> getConflictFlag state
getQ state \<noteq> []

goal (1 subgoal):
 1. (\<And>uClause. \<lbrakk>uClause el getF state; isUnitClause uClause (hd (getQ state)) (elements (getM state))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding InvariantQCharacterization_def
[PROOF STATE]
proof (prove)
using this:
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
\<not> getConflictFlag state \<longrightarrow> (\<forall>l. l el getQ state = (\<exists>c. c el getF state \<and> isUnitClause c l (elements (getM state))))
\<not> getConflictFlag state
getQ state \<noteq> []

goal (1 subgoal):
 1. (\<And>uClause. \<lbrakk>uClause el getF state; isUnitClause uClause (hd (getQ state)) (elements (getM state))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
uClause el getF state
isUnitClause uClause (hd (getQ state)) (elements (getM state))

goal (1 subgoal):
 1. let uLiteral = hd (getQ state); state' = applyUnitPropagate state in \<exists>uClause. formulaEntailsClause (getF state) uClause \<and> isUnitClause uClause uLiteral (elements (getM state)) \<and> getM state' = getM state @ [(uLiteral, False)]
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
uClause el getF state
isUnitClause uClause (hd (getQ state)) (elements (getM state))

goal (1 subgoal):
 1. let uLiteral = hd (getQ state); state' = applyUnitPropagate state in \<exists>uClause. formulaEntailsClause (getF state) uClause \<and> isUnitClause uClause uLiteral (elements (getM state)) \<and> getM state' = getM state @ [(uLiteral, False)]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
uClause el getF state
isUnitClause uClause (hd (getQ state)) (elements (getM state))
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
\<not> getConflictFlag state
getQ state \<noteq> []

goal (1 subgoal):
 1. let uLiteral = hd (getQ state); state' = applyUnitPropagate state in \<exists>uClause. formulaEntailsClause (getF state) uClause \<and> isUnitClause uClause uLiteral (elements (getM state)) \<and> getM state' = getM state @ [(uLiteral, False)]
[PROOF STEP]
using assertLiteralEffect[of "state" "?uLiteral" "False"]
[PROOF STATE]
proof (prove)
using this:
uClause el getF state
isUnitClause uClause (hd (getQ state)) (elements (getM state))
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
\<not> getConflictFlag state
getQ state \<noteq> []
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getM (assertLiteral (hd (getQ state)) False state) = getM state @ [(hd (getQ state), False)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getF (assertLiteral (hd (getQ state)) False state) = getF state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getSATFlag (assertLiteral (hd (getQ state)) False state) = getSATFlag state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> isPrefix (getQ state) (getQ (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. let uLiteral = hd (getQ state); state' = applyUnitPropagate state in \<exists>uClause. formulaEntailsClause (getF state) uClause \<and> isUnitClause uClause uLiteral (elements (getM state)) \<and> getM state' = getM state @ [(uLiteral, False)]
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
using this:
uClause el getF state
isUnitClause uClause (hd (getQ state)) (elements (getM state))
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
\<not> getConflictFlag state
getQ state \<noteq> []
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getM (assertLiteral (hd (getQ state)) False state) = getM state @ [(hd (getQ state), False)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getF (assertLiteral (hd (getQ state)) False state) = getF state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getSATFlag (assertLiteral (hd (getQ state)) False state) = getSATFlag state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> isPrefix (getQ state) (getQ (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. let uLiteral = hd (getQ state); state' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in \<exists>uClause. formulaEntailsClause (getF state) uClause \<and> isUnitClause uClause uLiteral (elements (getM state)) \<and> getM state' = getM state @ [(uLiteral, False)]
[PROOF STEP]
using formulaEntailsItsClauses[of "uClause" "getF state"]
[PROOF STATE]
proof (prove)
using this:
uClause el getF state
isUnitClause uClause (hd (getQ state)) (elements (getM state))
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
\<not> getConflictFlag state
getQ state \<noteq> []
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getM (assertLiteral (hd (getQ state)) False state) = getM state @ [(hd (getQ state), False)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getF (assertLiteral (hd (getQ state)) False state) = getF state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> getSATFlag (assertLiteral (hd (getQ state)) False state) = getSATFlag state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)\<rbrakk> \<Longrightarrow> isPrefix (getQ state) (getQ (assertLiteral (hd (getQ state)) False state))
uClause el getF state \<Longrightarrow> formulaEntailsClause (getF state) uClause

goal (1 subgoal):
 1. let uLiteral = hd (getQ state); state' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in \<exists>uClause. formulaEntailsClause (getF state) uClause \<and> isUnitClause uClause uLiteral (elements (getM state)) \<and> getM state' = getM state @ [(uLiteral, False)]
[PROOF STEP]
by (auto simp add: Let_def )
[PROOF STATE]
proof (state)
this:
let uLiteral = hd (getQ state); state' = applyUnitPropagate state in \<exists>uClause. formulaEntailsClause (getF state) uClause \<and> isUnitClause uClause uLiteral (elements (getM state)) \<and> getM state' = getM state @ [(uLiteral, False)]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantConsistentAfterApplyUnitPropagate:
assumes
  "InvariantConsistent (getM state)"
  "InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)" and
  "InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)" and
  "InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)"
  "getQ state \<noteq> []"
  "\<not> (getConflictFlag state)"
shows
  "let state' = applyUnitPropagate state in
     InvariantConsistent (getM state')
  "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantConsistent (getM state')
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantConsistent (getM state')
[PROOF STEP]
let ?uLiteral = "hd (getQ state)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantConsistent (getM state')
[PROOF STEP]
let ?state' = "applyUnitPropagate state"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantConsistent (getM state')
[PROOF STEP]
obtain uClause
    where "isUnitClause uClause ?uLiteral (elements (getM state))" and
    "(getM ?state') = (getM state) @ [(?uLiteral, False)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>uClause. \<lbrakk>isUnitClause uClause (hd (getQ state)) (elements (getM state)); getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state

goal (1 subgoal):
 1. (\<And>uClause. \<lbrakk>isUnitClause uClause (hd (getQ state)) (elements (getM state)); getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using applyUnitPropagateEffect[of "state"]
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); \<not> getConflictFlag state; getQ state \<noteq> []\<rbrakk> \<Longrightarrow> let uLiteral = hd (getQ state); state' = applyUnitPropagate state in \<exists>uClause. formulaEntailsClause (getF state) uClause \<and> isUnitClause uClause uLiteral (elements (getM state)) \<and> getM state' = getM state @ [(uLiteral, False)]

goal (1 subgoal):
 1. (\<And>uClause. \<lbrakk>isUnitClause uClause (hd (getQ state)) (elements (getM state)); getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: Let_def)
[PROOF STATE]
proof (state)
this:
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantConsistent (getM state')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantConsistent (getM state')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
InvariantConsistent (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantConsistent (getM state')
[PROOF STEP]
using InvariantConsistentAfterUnitPropagate[of "getM state" "uClause" "?uLiteral" "getM ?state'"]
[PROOF STATE]
proof (prove)
using this:
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
InvariantConsistent (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantConsistent (getM state); isUnitClause uClause (hd (getQ state)) (elements (getM state)); getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]\<rbrakk> \<Longrightarrow> InvariantConsistent (getM (applyUnitPropagate state))

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantConsistent (getM state')
[PROOF STEP]
by (auto simp add: Let_def)
[PROOF STATE]
proof (state)
this:
let state' = applyUnitPropagate state in InvariantConsistent (getM state')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantUniqAfterApplyUnitPropagate:
assumes
  "InvariantUniq (getM state)"
  "InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)" and
  "InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)" and
  "InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)"
  "getQ state \<noteq> []"
  "\<not> (getConflictFlag state)"
shows
  "let state' = applyUnitPropagate state in
     InvariantUniq (getM state')
  "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantUniq (getM state')
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantUniq (getM state')
[PROOF STEP]
let ?uLiteral = "hd (getQ state)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantUniq (getM state')
[PROOF STEP]
let ?state' = "applyUnitPropagate state"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantUniq (getM state')
[PROOF STEP]
obtain uClause
    where "isUnitClause uClause ?uLiteral (elements (getM state))" and
    "(getM ?state') = (getM state) @ [(?uLiteral, False)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>uClause. \<lbrakk>isUnitClause uClause (hd (getQ state)) (elements (getM state)); getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state

goal (1 subgoal):
 1. (\<And>uClause. \<lbrakk>isUnitClause uClause (hd (getQ state)) (elements (getM state)); getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using applyUnitPropagateEffect[of "state"]
[PROOF STATE]
proof (prove)
using this:
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); \<not> getConflictFlag state; getQ state \<noteq> []\<rbrakk> \<Longrightarrow> let uLiteral = hd (getQ state); state' = applyUnitPropagate state in \<exists>uClause. formulaEntailsClause (getF state) uClause \<and> isUnitClause uClause uLiteral (elements (getM state)) \<and> getM state' = getM state @ [(uLiteral, False)]

goal (1 subgoal):
 1. (\<And>uClause. \<lbrakk>isUnitClause uClause (hd (getQ state)) (elements (getM state)); getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: Let_def)
[PROOF STATE]
proof (state)
this:
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantUniq (getM state')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantUniq (getM state')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantUniq (getM state')
[PROOF STEP]
using InvariantUniqAfterUnitPropagate[of "getM state" "uClause" "?uLiteral" "getM ?state'"]
[PROOF STATE]
proof (prove)
using this:
isUnitClause uClause (hd (getQ state)) (elements (getM state))
getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]
InvariantUniq (getM state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantUniq (getM state); isUnitClause uClause (hd (getQ state)) (elements (getM state)); getM (applyUnitPropagate state) = getM state @ [(hd (getQ state), False)]\<rbrakk> \<Longrightarrow> InvariantUniq (getM (applyUnitPropagate state))

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantUniq (getM state')
[PROOF STEP]
by (auto simp add: Let_def)
[PROOF STATE]
proof (state)
this:
let state' = applyUnitPropagate state in InvariantUniq (getM state')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InvariantWatchCharacterizationAfterApplyUnitPropagate:
assumes
  "InvariantConsistent (getM state)"
  "InvariantUniq (getM state)"
  "InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)" and
  "InvariantWatchListsUniq (getWatchList state)" and
  "InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)"
  "InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)" and
  "InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)"
  "InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)"
  "InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)"
  "(getQ state) \<noteq> []"
  "\<not> (getConflictFlag state)"
shows
  "let state' = applyUnitPropagate state in
        InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
let ?uLiteral = "hd (getQ state)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
let ?state' = "assertLiteral ?uLiteral False state"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
let ?state'' = "applyUnitPropagate state"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
have "InvariantConsistent (getM ?state')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state

goal (1 subgoal):
 1. InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
using InvariantConsistentAfterApplyUnitPropagate[of "state"]
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantConsistent (getM state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); getQ state \<noteq> []; \<not> getConflictFlag state\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state in InvariantConsistent (getM state')

goal (1 subgoal):
 1. InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantConsistent (getM state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); getQ state \<noteq> []; \<not> getConflictFlag state\<rbrakk> \<Longrightarrow> let state' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in InvariantConsistent (getM state')

goal (1 subgoal):
 1. InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
by (auto simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
have "InvariantUniq (getM ?state')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InvariantUniq (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state

goal (1 subgoal):
 1. InvariantUniq (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
using InvariantUniqAfterApplyUnitPropagate[of "state"]
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantUniq (getM state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); getQ state \<noteq> []; \<not> getConflictFlag state\<rbrakk> \<Longrightarrow> let state' = applyUnitPropagate state in InvariantUniq (getM state')

goal (1 subgoal):
 1. InvariantUniq (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantUniq (getM state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state); getQ state \<noteq> []; \<not> getConflictFlag state\<rbrakk> \<Longrightarrow> let state' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in InvariantUniq (getM state')

goal (1 subgoal):
 1. InvariantUniq (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
by (auto simp add: Let_def)
[PROOF STATE]
proof (state)
this:
InvariantUniq (getM (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
InvariantUniq (getM (assertLiteral (hd (getQ state)) False state))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
InvariantUniq (getM (assertLiteral (hd (getQ state)) False state))

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
InvariantUniq (getM (assertLiteral (hd (getQ state)) False state))
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
using InvariantWatchCharacterizationAfterAssertLiteral[of "state" "?uLiteral" "False"]
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
InvariantUniq (getM (assertLiteral (hd (getQ state)) False state))
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantConsistent (getM state @ [(hd (getQ state), False)]); InvariantUniq (getM state @ [(hd (getQ state), False)]); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchListsUniq (getWatchList state); InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
using assertLiteralEffect
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
InvariantUniq (getM (assertLiteral (hd (getQ state)) False state))
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantConsistent (getM state @ [(hd (getQ state), False)]); InvariantUniq (getM state @ [(hd (getQ state), False)]); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchListsUniq (getWatchList state); InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList ?state) (getF ?state); InvariantWatchesEl (getF ?state) (getWatch1 ?state) (getWatch2 ?state)\<rbrakk> \<Longrightarrow> getM (assertLiteral ?l ?d ?state) = getM ?state @ [(?l, ?d)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList ?state) (getF ?state); InvariantWatchesEl (getF ?state) (getWatch1 ?state) (getWatch2 ?state)\<rbrakk> \<Longrightarrow> getF (assertLiteral ?l ?d ?state) = getF ?state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList ?state) (getF ?state); InvariantWatchesEl (getF ?state) (getWatch1 ?state) (getWatch2 ?state)\<rbrakk> \<Longrightarrow> getSATFlag (assertLiteral ?l ?d ?state) = getSATFlag ?state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList ?state) (getF ?state); InvariantWatchesEl (getF ?state) (getWatch1 ?state) (getWatch2 ?state)\<rbrakk> \<Longrightarrow> isPrefix (getQ ?state) (getQ (assertLiteral ?l ?d ?state))

goal (1 subgoal):
 1. let state' = applyUnitPropagate state in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
unfolding applyUnitPropagate_def
[PROOF STATE]
proof (prove)
using this:
InvariantConsistent (getM (assertLiteral (hd (getQ state)) False state))
InvariantUniq (getM (assertLiteral (hd (getQ state)) False state))
InvariantConsistent (getM state)
InvariantUniq (getM state)
InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state)
InvariantWatchListsUniq (getWatchList state)
InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state)
InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state)
InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)
InvariantQCharacterization (getConflictFlag state) (getQ state) (getF state) (getM state)
getQ state \<noteq> []
\<not> getConflictFlag state
\<lbrakk>InvariantConsistent (getM state @ [(hd (getQ state), False)]); InvariantUniq (getM state @ [(hd (getQ state), False)]); InvariantWatchListsContainOnlyClausesFromF (getWatchList state) (getF state); InvariantWatchListsUniq (getWatchList state); InvariantWatchListsCharacterization (getWatchList state) (getWatch1 state) (getWatch2 state); InvariantWatchesEl (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchesDiffer (getF state) (getWatch1 state) (getWatch2 state); InvariantWatchCharacterization (getF state) (getWatch1 state) (getWatch2 state) (getM state)\<rbrakk> \<Longrightarrow> let state' = assertLiteral (hd (getQ state)) False state in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList ?state) (getF ?state); InvariantWatchesEl (getF ?state) (getWatch1 ?state) (getWatch2 ?state)\<rbrakk> \<Longrightarrow> getM (assertLiteral ?l ?d ?state) = getM ?state @ [(?l, ?d)]
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList ?state) (getF ?state); InvariantWatchesEl (getF ?state) (getWatch1 ?state) (getWatch2 ?state)\<rbrakk> \<Longrightarrow> getF (assertLiteral ?l ?d ?state) = getF ?state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList ?state) (getF ?state); InvariantWatchesEl (getF ?state) (getWatch1 ?state) (getWatch2 ?state)\<rbrakk> \<Longrightarrow> getSATFlag (assertLiteral ?l ?d ?state) = getSATFlag ?state
\<lbrakk>InvariantWatchListsContainOnlyClausesFromF (getWatchList ?state) (getF ?state); InvariantWatchesEl (getF ?state) (getWatch1 ?state) (getWatch2 ?state)\<rbrakk> \<Longrightarrow> isPrefix (getQ ?state) (getQ (assertLiteral ?l ?d ?state))

goal (1 subgoal):
 1. let state' = let state' = assertLiteral (hd (getQ state)) False state in state'\<lparr>getQ := tl (getQ state')\<rparr> in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
let state' = applyUnitPropagate state in InvariantWatchCharacterization (getF state') (getWatch1 state') (getWatch2 state') (getM state')

goal:
No subgoals!
[PROOF STEP]
qed