[STATEMENT]
lemma not_restricted_swap_inputs:
  "not_restricted (I x1a) G \<Longrightarrow>
   apply_guards G (join_ir i r) \<Longrightarrow>
   apply_guards G (join_ir (i[x1a := x1]) r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>not_restricted (I x1a) G; apply_guards G (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards G (join_ir (i[x1a := x1]) r)
[PROOF STEP]
proof(induct G)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>not_restricted (I x1a) []; apply_guards [] (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards [] (join_ir (i[x1a := x1]) r)
 2. \<And>a G. \<lbrakk>\<lbrakk>not_restricted (I x1a) G; apply_guards G (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards G (join_ir (i[x1a := x1]) r); not_restricted (I x1a) (a # G); apply_guards (a # G) (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards (a # G) (join_ir (i[x1a := x1]) r)
[PROOF STEP]
case (Cons a G)
[PROOF STATE]
proof (state)
this:
\<lbrakk>not_restricted (I x1a) G; apply_guards G (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards G (join_ir (i[x1a := x1]) r)
not_restricted (I x1a) (a # G)
apply_guards (a # G) (join_ir i r)

goal (2 subgoals):
 1. \<lbrakk>not_restricted (I x1a) []; apply_guards [] (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards [] (join_ir (i[x1a := x1]) r)
 2. \<And>a G. \<lbrakk>\<lbrakk>not_restricted (I x1a) G; apply_guards G (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards G (join_ir (i[x1a := x1]) r); not_restricted (I x1a) (a # G); apply_guards (a # G) (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards (a # G) (join_ir (i[x1a := x1]) r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>not_restricted (I x1a) G; apply_guards G (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards G (join_ir (i[x1a := x1]) r)
not_restricted (I x1a) (a # G)
apply_guards (a # G) (join_ir i r)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>not_restricted (I x1a) G; apply_guards G (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards G (join_ir (i[x1a := x1]) r)
not_restricted (I x1a) (a # G)
apply_guards (a # G) (join_ir i r)

goal (1 subgoal):
 1. apply_guards (a # G) (join_ir (i[x1a := x1]) r)
[PROOF STEP]
apply (simp add: apply_guards_cons not_restricted_cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>apply_guards G (join_ir (i[x1a := x1]) r); \<not> gexp_constrains a (V (I x1a)) \<and> not_restricted (I x1a) G; gval a (join_ir i r) = true \<and> apply_guards G (join_ir i r)\<rbrakk> \<Longrightarrow> gval a (join_ir (i[x1a := x1]) r) = true
[PROOF STEP]
using input_not_constrained_gval_swap_inputs
[PROOF STATE]
proof (prove)
using this:
\<not> gexp_constrains ?a (V (I ?v)) \<Longrightarrow> gval ?a (join_ir ?i ?c) = gval ?a (join_ir (?i[?v := ?x]) ?c)

goal (1 subgoal):
 1. \<lbrakk>apply_guards G (join_ir (i[x1a := x1]) r); \<not> gexp_constrains a (V (I x1a)) \<and> not_restricted (I x1a) G; gval a (join_ir i r) = true \<and> apply_guards G (join_ir i r)\<rbrakk> \<Longrightarrow> gval a (join_ir (i[x1a := x1]) r) = true
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
apply_guards (a # G) (join_ir (i[x1a := x1]) r)

goal (1 subgoal):
 1. \<lbrakk>not_restricted (I x1a) []; apply_guards [] (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards [] (join_ir (i[x1a := x1]) r)
[PROOF STEP]
qed auto