[STATEMENT]
lemma nbae_rel_id[simp]: "\<langle>Id, Id\<rangle> nbae_rel = Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Id, Id\<rangle>nbae_rel = Id
[PROOF STEP]
unfolding nbae_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(A\<^sub>1, A\<^sub>2). (alphabete A\<^sub>1, alphabete A\<^sub>2) \<in> \<langle>Id\<rangle>set_rel \<and> (initiale A\<^sub>1, initiale A\<^sub>2) \<in> \<langle>Id\<rangle>set_rel \<and> (transitione A\<^sub>1, transitione A\<^sub>2) \<in> \<langle>Id \<times>\<^sub>r Id \<times>\<^sub>r Id\<rangle>set_rel \<and> (acceptinge A\<^sub>1, acceptinge A\<^sub>2) \<in> \<langle>Id\<rangle>set_rel} = Id
[PROOF STEP]
using nbae.expand
[PROOF STATE]
proof (prove)
using this:
alphabete ?nbae = alphabete ?nbae' \<and> initiale ?nbae = initiale ?nbae' \<and> transitione ?nbae = transitione ?nbae' \<and> acceptinge ?nbae = acceptinge ?nbae' \<Longrightarrow> ?nbae = ?nbae'

goal (1 subgoal):
 1. {(A\<^sub>1, A\<^sub>2). (alphabete A\<^sub>1, alphabete A\<^sub>2) \<in> \<langle>Id\<rangle>set_rel \<and> (initiale A\<^sub>1, initiale A\<^sub>2) \<in> \<langle>Id\<rangle>set_rel \<and> (transitione A\<^sub>1, transitione A\<^sub>2) \<in> \<langle>Id \<times>\<^sub>r Id \<times>\<^sub>r Id\<rangle>set_rel \<and> (acceptinge A\<^sub>1, acceptinge A\<^sub>2) \<in> \<langle>Id\<rangle>set_rel} = Id
[PROOF STEP]
by auto


[STATEMENT]
lemma nbae_rel_comp[simp]: "\<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle> nbae_rel = \<langle>L\<^sub>1, S\<^sub>1\<rangle> nbae_rel O \<langle>L\<^sub>2, S\<^sub>2\<rangle> nbae_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle>nbae_rel = \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel O \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> \<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle>nbae_rel \<Longrightarrow> (a, b) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel O \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel
 2. \<And>a b x y z. \<lbrakk>(x, y) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel; (y, z) \<in> \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel\<rbrakk> \<Longrightarrow> (x, z) \<in> \<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle>nbae_rel
[PROOF STEP]
fix A B
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> \<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle>nbae_rel \<Longrightarrow> (a, b) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel O \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel
 2. \<And>a b x y z. \<lbrakk>(x, y) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel; (y, z) \<in> \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel\<rbrakk> \<Longrightarrow> (x, z) \<in> \<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle>nbae_rel
[PROOF STEP]
assume 1: "(A, B) \<in> \<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle> nbae_rel"
[PROOF STATE]
proof (state)
this:
(A, B) \<in> \<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle>nbae_rel

goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> \<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle>nbae_rel \<Longrightarrow> (a, b) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel O \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel
 2. \<And>a b x y z. \<lbrakk>(x, y) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel; (y, z) \<in> \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel\<rbrakk> \<Longrightarrow> (x, z) \<in> \<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle>nbae_rel
[PROOF STEP]
obtain a b c d where 2:
      "(alphabete A, a) \<in> \<langle>L\<^sub>1\<rangle> set_rel" "(a, alphabete B) \<in> \<langle>L\<^sub>2\<rangle> set_rel"
      "(initiale A, b) \<in> \<langle>S\<^sub>1\<rangle> set_rel" "(b, initiale B) \<in> \<langle>S\<^sub>2\<rangle> set_rel"
      "(transitione A, c) \<in> \<langle>S\<^sub>1 \<times>\<^sub>r L\<^sub>1 \<times>\<^sub>r S\<^sub>1\<rangle> set_rel" "(c, transitione B) \<in> \<langle>S\<^sub>2 \<times>\<^sub>r L\<^sub>2 \<times>\<^sub>r S\<^sub>2\<rangle> set_rel"
      "(acceptinge A, d) \<in> \<langle>S\<^sub>1\<rangle> set_rel" "(d, acceptinge B) \<in> \<langle>S\<^sub>2\<rangle> set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>(alphabete A, a) \<in> \<langle>L\<^sub>1\<rangle>set_rel; (a, alphabete B) \<in> \<langle>L\<^sub>2\<rangle>set_rel; (initiale A, b) \<in> \<langle>S\<^sub>1\<rangle>set_rel; (b, initiale B) \<in> \<langle>S\<^sub>2\<rangle>set_rel; (transitione A, c) \<in> \<langle>S\<^sub>1 \<times>\<^sub>r L\<^sub>1 \<times>\<^sub>r S\<^sub>1\<rangle>set_rel; (c, transitione B) \<in> \<langle>S\<^sub>2 \<times>\<^sub>r L\<^sub>2 \<times>\<^sub>r S\<^sub>2\<rangle>set_rel; (acceptinge A, d) \<in> \<langle>S\<^sub>1\<rangle>set_rel; (d, acceptinge B) \<in> \<langle>S\<^sub>2\<rangle>set_rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
(A, B) \<in> \<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle>nbae_rel

goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>(alphabete A, a) \<in> \<langle>L\<^sub>1\<rangle>set_rel; (a, alphabete B) \<in> \<langle>L\<^sub>2\<rangle>set_rel; (initiale A, b) \<in> \<langle>S\<^sub>1\<rangle>set_rel; (b, initiale B) \<in> \<langle>S\<^sub>2\<rangle>set_rel; (transitione A, c) \<in> \<langle>S\<^sub>1 \<times>\<^sub>r L\<^sub>1 \<times>\<^sub>r S\<^sub>1\<rangle>set_rel; (c, transitione B) \<in> \<langle>S\<^sub>2 \<times>\<^sub>r L\<^sub>2 \<times>\<^sub>r S\<^sub>2\<rangle>set_rel; (acceptinge A, d) \<in> \<langle>S\<^sub>1\<rangle>set_rel; (d, acceptinge B) \<in> \<langle>S\<^sub>2\<rangle>set_rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding nbae_rel_def prod_rel_compp set_rel_compp
[PROOF STATE]
proof (prove)
using this:
(A, B) \<in> {(A\<^sub>1, A\<^sub>2). (alphabete A\<^sub>1, alphabete A\<^sub>2) \<in> \<langle>L\<^sub>1\<rangle>set_rel O \<langle>L\<^sub>2\<rangle>set_rel \<and> (initiale A\<^sub>1, initiale A\<^sub>2) \<in> \<langle>S\<^sub>1\<rangle>set_rel O \<langle>S\<^sub>2\<rangle>set_rel \<and> (transitione A\<^sub>1, transitione A\<^sub>2) \<in> \<langle>S\<^sub>1 \<times>\<^sub>r L\<^sub>1 \<times>\<^sub>r S\<^sub>1\<rangle>set_rel O \<langle>S\<^sub>2 \<times>\<^sub>r L\<^sub>2 \<times>\<^sub>r S\<^sub>2\<rangle>set_rel \<and> (acceptinge A\<^sub>1, acceptinge A\<^sub>2) \<in> \<langle>S\<^sub>1\<rangle>set_rel O \<langle>S\<^sub>2\<rangle>set_rel}

goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>(alphabete A, a) \<in> \<langle>L\<^sub>1\<rangle>set_rel; (a, alphabete B) \<in> \<langle>L\<^sub>2\<rangle>set_rel; (initiale A, b) \<in> \<langle>S\<^sub>1\<rangle>set_rel; (b, initiale B) \<in> \<langle>S\<^sub>2\<rangle>set_rel; (transitione A, c) \<in> \<langle>S\<^sub>1 \<times>\<^sub>r L\<^sub>1 \<times>\<^sub>r S\<^sub>1\<rangle>set_rel; (c, transitione B) \<in> \<langle>S\<^sub>2 \<times>\<^sub>r L\<^sub>2 \<times>\<^sub>r S\<^sub>2\<rangle>set_rel; (acceptinge A, d) \<in> \<langle>S\<^sub>1\<rangle>set_rel; (d, acceptinge B) \<in> \<langle>S\<^sub>2\<rangle>set_rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(alphabete A, a) \<in> \<langle>L\<^sub>1\<rangle>set_rel
(a, alphabete B) \<in> \<langle>L\<^sub>2\<rangle>set_rel
(initiale A, b) \<in> \<langle>S\<^sub>1\<rangle>set_rel
(b, initiale B) \<in> \<langle>S\<^sub>2\<rangle>set_rel
(transitione A, c) \<in> \<langle>S\<^sub>1 \<times>\<^sub>r L\<^sub>1 \<times>\<^sub>r S\<^sub>1\<rangle>set_rel
(c, transitione B) \<in> \<langle>S\<^sub>2 \<times>\<^sub>r L\<^sub>2 \<times>\<^sub>r S\<^sub>2\<rangle>set_rel
(acceptinge A, d) \<in> \<langle>S\<^sub>1\<rangle>set_rel
(d, acceptinge B) \<in> \<langle>S\<^sub>2\<rangle>set_rel

goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> \<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle>nbae_rel \<Longrightarrow> (a, b) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel O \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel
 2. \<And>a b x y z. \<lbrakk>(x, y) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel; (y, z) \<in> \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel\<rbrakk> \<Longrightarrow> (x, z) \<in> \<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle>nbae_rel
[PROOF STEP]
show "(A, B) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle> nbae_rel O \<langle>L\<^sub>2, S\<^sub>2\<rangle> nbae_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A, B) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel O \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (A, ?b) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel
 2. (?b, B) \<in> \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel
[PROOF STEP]
show "(A, nbae a b c d) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle> nbae_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A, nbae a b c d) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
(alphabete A, a) \<in> \<langle>L\<^sub>1\<rangle>set_rel
(a, alphabete B) \<in> \<langle>L\<^sub>2\<rangle>set_rel
(initiale A, b) \<in> \<langle>S\<^sub>1\<rangle>set_rel
(b, initiale B) \<in> \<langle>S\<^sub>2\<rangle>set_rel
(transitione A, c) \<in> \<langle>S\<^sub>1 \<times>\<^sub>r L\<^sub>1 \<times>\<^sub>r S\<^sub>1\<rangle>set_rel
(c, transitione B) \<in> \<langle>S\<^sub>2 \<times>\<^sub>r L\<^sub>2 \<times>\<^sub>r S\<^sub>2\<rangle>set_rel
(acceptinge A, d) \<in> \<langle>S\<^sub>1\<rangle>set_rel
(d, acceptinge B) \<in> \<langle>S\<^sub>2\<rangle>set_rel

goal (1 subgoal):
 1. (A, nbae a b c d) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel
[PROOF STEP]
unfolding nbae_rel_def
[PROOF STATE]
proof (prove)
using this:
(alphabete A, a) \<in> \<langle>L\<^sub>1\<rangle>set_rel
(a, alphabete B) \<in> \<langle>L\<^sub>2\<rangle>set_rel
(initiale A, b) \<in> \<langle>S\<^sub>1\<rangle>set_rel
(b, initiale B) \<in> \<langle>S\<^sub>2\<rangle>set_rel
(transitione A, c) \<in> \<langle>S\<^sub>1 \<times>\<^sub>r L\<^sub>1 \<times>\<^sub>r S\<^sub>1\<rangle>set_rel
(c, transitione B) \<in> \<langle>S\<^sub>2 \<times>\<^sub>r L\<^sub>2 \<times>\<^sub>r S\<^sub>2\<rangle>set_rel
(acceptinge A, d) \<in> \<langle>S\<^sub>1\<rangle>set_rel
(d, acceptinge B) \<in> \<langle>S\<^sub>2\<rangle>set_rel

goal (1 subgoal):
 1. (A, nbae a b c d) \<in> {(A\<^sub>1, A\<^sub>2). (alphabete A\<^sub>1, alphabete A\<^sub>2) \<in> \<langle>L\<^sub>1\<rangle>set_rel \<and> (initiale A\<^sub>1, initiale A\<^sub>2) \<in> \<langle>S\<^sub>1\<rangle>set_rel \<and> (transitione A\<^sub>1, transitione A\<^sub>2) \<in> \<langle>S\<^sub>1 \<times>\<^sub>r L\<^sub>1 \<times>\<^sub>r S\<^sub>1\<rangle>set_rel \<and> (acceptinge A\<^sub>1, acceptinge A\<^sub>2) \<in> \<langle>S\<^sub>1\<rangle>set_rel}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(A, nbae a b c d) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel

goal (1 subgoal):
 1. (nbae a b c d, B) \<in> \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel
[PROOF STEP]
show "(nbae a b c d, B) \<in> \<langle>L\<^sub>2, S\<^sub>2\<rangle> nbae_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nbae a b c d, B) \<in> \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
(alphabete A, a) \<in> \<langle>L\<^sub>1\<rangle>set_rel
(a, alphabete B) \<in> \<langle>L\<^sub>2\<rangle>set_rel
(initiale A, b) \<in> \<langle>S\<^sub>1\<rangle>set_rel
(b, initiale B) \<in> \<langle>S\<^sub>2\<rangle>set_rel
(transitione A, c) \<in> \<langle>S\<^sub>1 \<times>\<^sub>r L\<^sub>1 \<times>\<^sub>r S\<^sub>1\<rangle>set_rel
(c, transitione B) \<in> \<langle>S\<^sub>2 \<times>\<^sub>r L\<^sub>2 \<times>\<^sub>r S\<^sub>2\<rangle>set_rel
(acceptinge A, d) \<in> \<langle>S\<^sub>1\<rangle>set_rel
(d, acceptinge B) \<in> \<langle>S\<^sub>2\<rangle>set_rel

goal (1 subgoal):
 1. (nbae a b c d, B) \<in> \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel
[PROOF STEP]
unfolding nbae_rel_def
[PROOF STATE]
proof (prove)
using this:
(alphabete A, a) \<in> \<langle>L\<^sub>1\<rangle>set_rel
(a, alphabete B) \<in> \<langle>L\<^sub>2\<rangle>set_rel
(initiale A, b) \<in> \<langle>S\<^sub>1\<rangle>set_rel
(b, initiale B) \<in> \<langle>S\<^sub>2\<rangle>set_rel
(transitione A, c) \<in> \<langle>S\<^sub>1 \<times>\<^sub>r L\<^sub>1 \<times>\<^sub>r S\<^sub>1\<rangle>set_rel
(c, transitione B) \<in> \<langle>S\<^sub>2 \<times>\<^sub>r L\<^sub>2 \<times>\<^sub>r S\<^sub>2\<rangle>set_rel
(acceptinge A, d) \<in> \<langle>S\<^sub>1\<rangle>set_rel
(d, acceptinge B) \<in> \<langle>S\<^sub>2\<rangle>set_rel

goal (1 subgoal):
 1. (nbae a b c d, B) \<in> {(A\<^sub>1, A\<^sub>2). (alphabete A\<^sub>1, alphabete A\<^sub>2) \<in> \<langle>L\<^sub>2\<rangle>set_rel \<and> (initiale A\<^sub>1, initiale A\<^sub>2) \<in> \<langle>S\<^sub>2\<rangle>set_rel \<and> (transitione A\<^sub>1, transitione A\<^sub>2) \<in> \<langle>S\<^sub>2 \<times>\<^sub>r L\<^sub>2 \<times>\<^sub>r S\<^sub>2\<rangle>set_rel \<and> (acceptinge A\<^sub>1, acceptinge A\<^sub>2) \<in> \<langle>S\<^sub>2\<rangle>set_rel}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(nbae a b c d, B) \<in> \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(A, B) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel O \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel

goal (1 subgoal):
 1. \<And>a b x y z. \<lbrakk>(x, y) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel; (y, z) \<in> \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel\<rbrakk> \<Longrightarrow> (x, z) \<in> \<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle>nbae_rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b x y z. \<lbrakk>(x, y) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel; (y, z) \<in> \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel\<rbrakk> \<Longrightarrow> (x, z) \<in> \<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle>nbae_rel
[PROOF STEP]
show "(A, C) \<in> \<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle> nbae_rel"
      if "(A, B) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle> nbae_rel" "(B, C) \<in> \<langle>L\<^sub>2, S\<^sub>2\<rangle> nbae_rel" for A B C
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A, C) \<in> \<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle>nbae_rel
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
(A, B) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel
(B, C) \<in> \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel

goal (1 subgoal):
 1. (A, C) \<in> \<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle>nbae_rel
[PROOF STEP]
unfolding nbae_rel_def prod_rel_compp set_rel_compp
[PROOF STATE]
proof (prove)
using this:
(A, B) \<in> {(A\<^sub>1, A\<^sub>2). (alphabete A\<^sub>1, alphabete A\<^sub>2) \<in> \<langle>L\<^sub>1\<rangle>set_rel \<and> (initiale A\<^sub>1, initiale A\<^sub>2) \<in> \<langle>S\<^sub>1\<rangle>set_rel \<and> (transitione A\<^sub>1, transitione A\<^sub>2) \<in> \<langle>S\<^sub>1 \<times>\<^sub>r L\<^sub>1 \<times>\<^sub>r S\<^sub>1\<rangle>set_rel \<and> (acceptinge A\<^sub>1, acceptinge A\<^sub>2) \<in> \<langle>S\<^sub>1\<rangle>set_rel}
(B, C) \<in> {(A\<^sub>1, A\<^sub>2). (alphabete A\<^sub>1, alphabete A\<^sub>2) \<in> \<langle>L\<^sub>2\<rangle>set_rel \<and> (initiale A\<^sub>1, initiale A\<^sub>2) \<in> \<langle>S\<^sub>2\<rangle>set_rel \<and> (transitione A\<^sub>1, transitione A\<^sub>2) \<in> \<langle>S\<^sub>2 \<times>\<^sub>r L\<^sub>2 \<times>\<^sub>r S\<^sub>2\<rangle>set_rel \<and> (acceptinge A\<^sub>1, acceptinge A\<^sub>2) \<in> \<langle>S\<^sub>2\<rangle>set_rel}

goal (1 subgoal):
 1. (A, C) \<in> {(A\<^sub>1, A\<^sub>2). (alphabete A\<^sub>1, alphabete A\<^sub>2) \<in> \<langle>L\<^sub>1\<rangle>set_rel O \<langle>L\<^sub>2\<rangle>set_rel \<and> (initiale A\<^sub>1, initiale A\<^sub>2) \<in> \<langle>S\<^sub>1\<rangle>set_rel O \<langle>S\<^sub>2\<rangle>set_rel \<and> (transitione A\<^sub>1, transitione A\<^sub>2) \<in> \<langle>S\<^sub>1 \<times>\<^sub>r L\<^sub>1 \<times>\<^sub>r S\<^sub>1\<rangle>set_rel O \<langle>S\<^sub>2 \<times>\<^sub>r L\<^sub>2 \<times>\<^sub>r S\<^sub>2\<rangle>set_rel \<and> (acceptinge A\<^sub>1, acceptinge A\<^sub>2) \<in> \<langle>S\<^sub>1\<rangle>set_rel O \<langle>S\<^sub>2\<rangle>set_rel}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?A, ?B) \<in> \<langle>L\<^sub>1, S\<^sub>1\<rangle>nbae_rel; (?B, ?C) \<in> \<langle>L\<^sub>2, S\<^sub>2\<rangle>nbae_rel\<rbrakk> \<Longrightarrow> (?A, ?C) \<in> \<langle>L\<^sub>1 O L\<^sub>2, S\<^sub>1 O S\<^sub>2\<rangle>nbae_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nbae_scheme_itype[autoref_itype]:
      "nbae ::\<^sub>i \<langle>L\<rangle>\<^sub>i i_set \<rightarrow>\<^sub>i \<langle>S\<rangle>\<^sub>i i_set \<rightarrow>\<^sub>i \<langle>\<langle>S, \<langle>L, S\<rangle>\<^sub>i i_prod\<rangle>\<^sub>i i_prod\<rangle>\<^sub>i i_set \<rightarrow>\<^sub>i \<langle>S\<rangle>\<^sub>i i_set \<rightarrow>\<^sub>i
        \<langle>L, S\<rangle>\<^sub>i i_nbae_scheme"
      "alphabete ::\<^sub>i \<langle>L, S\<rangle>\<^sub>i i_nbae_scheme \<rightarrow>\<^sub>i \<langle>L\<rangle>\<^sub>i i_set"
      "initiale ::\<^sub>i \<langle>L, S\<rangle>\<^sub>i i_nbae_scheme \<rightarrow>\<^sub>i \<langle>S\<rangle>\<^sub>i i_set"
      "transitione ::\<^sub>i \<langle>L, S\<rangle>\<^sub>i i_nbae_scheme \<rightarrow>\<^sub>i \<langle>\<langle>S, \<langle>L, S\<rangle>\<^sub>i i_prod\<rangle>\<^sub>i i_prod\<rangle>\<^sub>i i_set"
      "acceptinge ::\<^sub>i \<langle>L, S\<rangle>\<^sub>i i_nbae_scheme \<rightarrow>\<^sub>i \<langle>S\<rangle>\<^sub>i i_set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nbae ::\<^sub>i \<langle>L\<rangle>\<^sub>ii_set \<rightarrow>\<^sub>i \<langle>S\<rangle>\<^sub>ii_set \<rightarrow>\<^sub>i \<langle>\<langle>S, \<langle>L, S\<rangle>\<^sub>ii_prod\<rangle>\<^sub>ii_prod\<rangle>\<^sub>ii_set \<rightarrow>\<^sub>i \<langle>S\<rangle>\<^sub>ii_set \<rightarrow>\<^sub>i \<langle>L, S\<rangle>\<^sub>ii_nbae_scheme &&& alphabete ::\<^sub>i \<langle>L, S\<rangle>\<^sub>ii_nbae_scheme \<rightarrow>\<^sub>i \<langle>L\<rangle>\<^sub>ii_set) &&& initiale ::\<^sub>i \<langle>L, S\<rangle>\<^sub>ii_nbae_scheme \<rightarrow>\<^sub>i \<langle>S\<rangle>\<^sub>ii_set &&& transitione ::\<^sub>i \<langle>L, S\<rangle>\<^sub>ii_nbae_scheme \<rightarrow>\<^sub>i \<langle>\<langle>S, \<langle>L, S\<rangle>\<^sub>ii_prod\<rangle>\<^sub>ii_prod\<rangle>\<^sub>ii_set &&& acceptinge ::\<^sub>i \<langle>L, S\<rangle>\<^sub>ii_nbae_scheme \<rightarrow>\<^sub>i \<langle>S\<rangle>\<^sub>ii_set
[PROOF STEP]
by auto


[STATEMENT]
lemma nbaei_param[param, autoref_rules]:
    "(nbaei, nbaei) \<in> \<langle>L\<rangle> list_rel \<rightarrow> \<langle>S\<rangle> list_rel \<rightarrow> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle> list_rel \<rightarrow>
      \<langle>S\<rangle> list_rel \<rightarrow> \<langle>L, S\<rangle> nbaei_rel"
    "(alphabetei, alphabetei) \<in> \<langle>L, S\<rangle> nbaei_rel \<rightarrow> \<langle>L\<rangle> list_rel"
    "(initialei, initialei) \<in> \<langle>L, S\<rangle> nbaei_rel \<rightarrow> \<langle>S\<rangle> list_rel"
    "(transitionei, transitionei) \<in> \<langle>L, S\<rangle> nbaei_rel \<rightarrow> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle> list_rel"
    "(acceptingei, acceptingei) \<in> \<langle>L, S\<rangle> nbaei_rel \<rightarrow> \<langle>S\<rangle> list_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((nbaei, nbaei) \<in> \<langle>L\<rangle>list_rel \<rightarrow> \<langle>S\<rangle>list_rel \<rightarrow> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>list_rel \<rightarrow> \<langle>S\<rangle>list_rel \<rightarrow> \<langle>L, S\<rangle>nbaei_rel &&& (alphabetei, alphabetei) \<in> \<langle>L, S\<rangle>nbaei_rel \<rightarrow> \<langle>L\<rangle>list_rel) &&& (initialei, initialei) \<in> \<langle>L, S\<rangle>nbaei_rel \<rightarrow> \<langle>S\<rangle>list_rel &&& (transitionei, transitionei) \<in> \<langle>L, S\<rangle>nbaei_rel \<rightarrow> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>list_rel &&& (acceptingei, acceptingei) \<in> \<langle>L, S\<rangle>nbaei_rel \<rightarrow> \<langle>S\<rangle>list_rel
[PROOF STEP]
unfolding nbaei_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((nbaei, nbaei) \<in> \<langle>L\<rangle>list_rel \<rightarrow> \<langle>S\<rangle>list_rel \<rightarrow> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>list_rel \<rightarrow> \<langle>S\<rangle>list_rel \<rightarrow> {(A\<^sub>1, A\<^sub>2). (alphabetei A\<^sub>1, alphabetei A\<^sub>2) \<in> \<langle>L\<rangle>list_rel \<and> (initialei A\<^sub>1, initialei A\<^sub>2) \<in> \<langle>S\<rangle>list_rel \<and> (transitionei A\<^sub>1, transitionei A\<^sub>2) \<in> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>list_rel \<and> (acceptingei A\<^sub>1, acceptingei A\<^sub>2) \<in> \<langle>S\<rangle>list_rel} &&& (alphabetei, alphabetei) \<in> {(A\<^sub>1, A\<^sub>2). (alphabetei A\<^sub>1, alphabetei A\<^sub>2) \<in> \<langle>L\<rangle>list_rel \<and> (initialei A\<^sub>1, initialei A\<^sub>2) \<in> \<langle>S\<rangle>list_rel \<and> (transitionei A\<^sub>1, transitionei A\<^sub>2) \<in> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>list_rel \<and> (acceptingei A\<^sub>1, acceptingei A\<^sub>2) \<in> \<langle>S\<rangle>list_rel} \<rightarrow> \<langle>L\<rangle>list_rel) &&& (initialei, initialei) \<in> {(A\<^sub>1, A\<^sub>2). (alphabetei A\<^sub>1, alphabetei A\<^sub>2) \<in> \<langle>L\<rangle>list_rel \<and> (initialei A\<^sub>1, initialei A\<^sub>2) \<in> \<langle>S\<rangle>list_rel \<and> (transitionei A\<^sub>1, transitionei A\<^sub>2) \<in> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>list_rel \<and> (acceptingei A\<^sub>1, acceptingei A\<^sub>2) \<in> \<langle>S\<rangle>list_rel} \<rightarrow> \<langle>S\<rangle>list_rel &&& (transitionei, transitionei) \<in> {(A\<^sub>1, A\<^sub>2). (alphabetei A\<^sub>1, alphabetei A\<^sub>2) \<in> \<langle>L\<rangle>list_rel \<and> (initialei A\<^sub>1, initialei A\<^sub>2) \<in> \<langle>S\<rangle>list_rel \<and> (transitionei A\<^sub>1, transitionei A\<^sub>2) \<in> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>list_rel \<and> (acceptingei A\<^sub>1, acceptingei A\<^sub>2) \<in> \<langle>S\<rangle>list_rel} \<rightarrow> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>list_rel &&& (acceptingei, acceptingei) \<in> {(A\<^sub>1, A\<^sub>2). (alphabetei A\<^sub>1, alphabetei A\<^sub>2) \<in> \<langle>L\<rangle>list_rel \<and> (initialei A\<^sub>1, initialei A\<^sub>2) \<in> \<langle>S\<rangle>list_rel \<and> (transitionei A\<^sub>1, transitionei A\<^sub>2) \<in> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>list_rel \<and> (acceptingei A\<^sub>1, acceptingei A\<^sub>2) \<in> \<langle>S\<rangle>list_rel} \<rightarrow> \<langle>S\<rangle>list_rel
[PROOF STEP]
by auto


[STATEMENT]
lemma nbaei_nbae_param[param, autoref_rules]:
    "(nbaei, nbae) \<in> \<langle>L\<rangle> list_set_rel \<rightarrow> \<langle>S\<rangle> list_set_rel \<rightarrow> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle> list_set_rel \<rightarrow>
      \<langle>S\<rangle> list_set_rel \<rightarrow> \<langle>L, S\<rangle> nbaei_nbae_rel"
    "(alphabetei, alphabete) \<in> \<langle>L, S\<rangle> nbaei_nbae_rel \<rightarrow> \<langle>L\<rangle> list_set_rel"
    "(initialei, initiale) \<in> \<langle>L, S\<rangle> nbaei_nbae_rel \<rightarrow> \<langle>S\<rangle> list_set_rel"
    "(transitionei, transitione) \<in> \<langle>L, S\<rangle> nbaei_nbae_rel \<rightarrow> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle> list_set_rel"
    "(acceptingei, acceptinge) \<in> \<langle>L, S\<rangle> nbaei_nbae_rel \<rightarrow> \<langle>S\<rangle> list_set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((nbaei, nbae) \<in> \<langle>L\<rangle>list_set_rel \<rightarrow> \<langle>S\<rangle>list_set_rel \<rightarrow> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>list_set_rel \<rightarrow> \<langle>S\<rangle>list_set_rel \<rightarrow> \<langle>L, S\<rangle>nbaei_nbae_rel &&& (alphabetei, alphabete) \<in> \<langle>L, S\<rangle>nbaei_nbae_rel \<rightarrow> \<langle>L\<rangle>list_set_rel) &&& (initialei, initiale) \<in> \<langle>L, S\<rangle>nbaei_nbae_rel \<rightarrow> \<langle>S\<rangle>list_set_rel &&& (transitionei, transitione) \<in> \<langle>L, S\<rangle>nbaei_nbae_rel \<rightarrow> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>list_set_rel &&& (acceptingei, acceptinge) \<in> \<langle>L, S\<rangle>nbaei_nbae_rel \<rightarrow> \<langle>S\<rangle>list_set_rel
[PROOF STEP]
unfolding nbaei_nbae_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((nbaei, nbae) \<in> \<langle>L\<rangle>list_set_rel \<rightarrow> \<langle>S\<rangle>list_set_rel \<rightarrow> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>list_set_rel \<rightarrow> \<langle>S\<rangle>list_set_rel \<rightarrow> {(A\<^sub>1, A\<^sub>2). (alphabetei A\<^sub>1, alphabete A\<^sub>2) \<in> \<langle>L\<rangle>list_set_rel \<and> (initialei A\<^sub>1, initiale A\<^sub>2) \<in> \<langle>S\<rangle>list_set_rel \<and> (transitionei A\<^sub>1, transitione A\<^sub>2) \<in> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>list_set_rel \<and> (acceptingei A\<^sub>1, acceptinge A\<^sub>2) \<in> \<langle>S\<rangle>list_set_rel} &&& (alphabetei, alphabete) \<in> {(A\<^sub>1, A\<^sub>2). (alphabetei A\<^sub>1, alphabete A\<^sub>2) \<in> \<langle>L\<rangle>list_set_rel \<and> (initialei A\<^sub>1, initiale A\<^sub>2) \<in> \<langle>S\<rangle>list_set_rel \<and> (transitionei A\<^sub>1, transitione A\<^sub>2) \<in> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>list_set_rel \<and> (acceptingei A\<^sub>1, acceptinge A\<^sub>2) \<in> \<langle>S\<rangle>list_set_rel} \<rightarrow> \<langle>L\<rangle>list_set_rel) &&& (initialei, initiale) \<in> {(A\<^sub>1, A\<^sub>2). (alphabetei A\<^sub>1, alphabete A\<^sub>2) \<in> \<langle>L\<rangle>list_set_rel \<and> (initialei A\<^sub>1, initiale A\<^sub>2) \<in> \<langle>S\<rangle>list_set_rel \<and> (transitionei A\<^sub>1, transitione A\<^sub>2) \<in> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>list_set_rel \<and> (acceptingei A\<^sub>1, acceptinge A\<^sub>2) \<in> \<langle>S\<rangle>list_set_rel} \<rightarrow> \<langle>S\<rangle>list_set_rel &&& (transitionei, transitione) \<in> {(A\<^sub>1, A\<^sub>2). (alphabetei A\<^sub>1, alphabete A\<^sub>2) \<in> \<langle>L\<rangle>list_set_rel \<and> (initialei A\<^sub>1, initiale A\<^sub>2) \<in> \<langle>S\<rangle>list_set_rel \<and> (transitionei A\<^sub>1, transitione A\<^sub>2) \<in> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>list_set_rel \<and> (acceptingei A\<^sub>1, acceptinge A\<^sub>2) \<in> \<langle>S\<rangle>list_set_rel} \<rightarrow> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>list_set_rel &&& (acceptingei, acceptinge) \<in> {(A\<^sub>1, A\<^sub>2). (alphabetei A\<^sub>1, alphabete A\<^sub>2) \<in> \<langle>L\<rangle>list_set_rel \<and> (initialei A\<^sub>1, initiale A\<^sub>2) \<in> \<langle>S\<rangle>list_set_rel \<and> (transitionei A\<^sub>1, transitione A\<^sub>2) \<in> \<langle>S \<times>\<^sub>r L \<times>\<^sub>r S\<rangle>list_set_rel \<and> (acceptingei A\<^sub>1, acceptinge A\<^sub>2) \<in> \<langle>S\<rangle>list_set_rel} \<rightarrow> \<langle>S\<rangle>list_set_rel
[PROOF STEP]
by auto


[STATEMENT]
lemma nbaei_nbae_id_param[param]: "(nbaei_nbae, id) \<in> \<langle>L, S\<rangle> nbaei_nbae_rel \<rightarrow> \<langle>L, S\<rangle> nbae_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nbaei_nbae, id) \<in> \<langle>L, S\<rangle>nbaei_nbae_rel \<rightarrow> \<langle>L, S\<rangle>nbae_rel
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>L, S\<rangle>nbaei_nbae_rel \<Longrightarrow> (nbaei_nbae a, id a') \<in> \<langle>L, S\<rangle>nbae_rel
[PROOF STEP]
fix Ai A
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>L, S\<rangle>nbaei_nbae_rel \<Longrightarrow> (nbaei_nbae a, id a') \<in> \<langle>L, S\<rangle>nbae_rel
[PROOF STEP]
assume 1: "(Ai, A) \<in> \<langle>L, S\<rangle> nbaei_nbae_rel"
[PROOF STATE]
proof (state)
this:
(Ai, A) \<in> \<langle>L, S\<rangle>nbaei_nbae_rel

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>L, S\<rangle>nbaei_nbae_rel \<Longrightarrow> (nbaei_nbae a, id a') \<in> \<langle>L, S\<rangle>nbae_rel
[PROOF STEP]
have 2: "nbaei_nbae Ai = nbae (set (alphabetei Ai)) (set (initialei Ai))
      (set (transitionei Ai)) (set (acceptingei Ai))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nbaei_nbae Ai = nbae (set (alphabetei Ai)) (set (initialei Ai)) (set (transitionei Ai)) (set (acceptingei Ai))
[PROOF STEP]
unfolding nbaei_nbae_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nbae (set (alphabetei Ai)) (set (initialei Ai)) (set (transitionei Ai)) (set (acceptingei Ai)) = nbae (set (alphabetei Ai)) (set (initialei Ai)) (set (transitionei Ai)) (set (acceptingei Ai))
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
nbaei_nbae Ai = nbae (set (alphabetei Ai)) (set (initialei Ai)) (set (transitionei Ai)) (set (acceptingei Ai))

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>L, S\<rangle>nbaei_nbae_rel \<Longrightarrow> (nbaei_nbae a, id a') \<in> \<langle>L, S\<rangle>nbae_rel
[PROOF STEP]
have 3: "id A = nbae (id (alphabete A)) (id (initiale A))
      (id (transitione A)) (id (acceptinge A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id A = nbae (id (alphabete A)) (id (initiale A)) (id (transitione A)) (id (acceptinge A))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
id A = nbae (id (alphabete A)) (id (initiale A)) (id (transitione A)) (id (acceptinge A))

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>L, S\<rangle>nbaei_nbae_rel \<Longrightarrow> (nbaei_nbae a, id a') \<in> \<langle>L, S\<rangle>nbae_rel
[PROOF STEP]
show "(nbaei_nbae Ai, id A) \<in> \<langle>L, S\<rangle> nbae_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nbaei_nbae Ai, id A) \<in> \<langle>L, S\<rangle>nbae_rel
[PROOF STEP]
unfolding 2 3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nbae (set (alphabetei Ai)) (set (initialei Ai)) (set (transitionei Ai)) (set (acceptingei Ai)), nbae (id (alphabete A)) (id (initiale A)) (id (transitione A)) (id (acceptinge A))) \<in> \<langle>L, S\<rangle>nbae_rel
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
(Ai, A) \<in> \<langle>L, S\<rangle>nbaei_nbae_rel

goal (1 subgoal):
 1. (nbae (set (alphabetei Ai)) (set (initialei Ai)) (set (transitionei Ai)) (set (acceptingei Ai)), nbae (id (alphabete A)) (id (initiale A)) (id (transitione A)) (id (acceptinge A))) \<in> \<langle>L, S\<rangle>nbae_rel
[PROOF STEP]
by parametricity
[PROOF STATE]
proof (state)
this:
(nbaei_nbae Ai, id A) \<in> \<langle>L, S\<rangle>nbae_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nba_nbae_param[param]: "(nba_nbae, nba_nbae) \<in> \<langle>L, S\<rangle> nba_rel \<rightarrow> \<langle>L, S\<rangle> nbae_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nba_nbae, nba_nbae) \<in> \<langle>L, S\<rangle>nba_rel \<rightarrow> \<langle>L, S\<rangle>nbae_rel
[PROOF STEP]
unfolding nba_nbae_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>A. nbae (alphabet A) (initial A) (transitions (alphabet A) (nodes A) (transition A)) (Set.filter (accepting A) (nodes A)), \<lambda>A. nbae (alphabet A) (initial A) (transitions (alphabet A) (nodes A) (transition A)) (Set.filter (accepting A) (nodes A))) \<in> \<langle>L, S\<rangle>nba_rel \<rightarrow> \<langle>L, S\<rangle>nbae_rel
[PROOF STEP]
by parametricity


[STATEMENT]
lemma nbae_nba_param[param]:
    assumes "bijective L" "bijective S"
    shows "(nbae_nba, nbae_nba) \<in> \<langle>L, S\<rangle> nbae_rel \<rightarrow> \<langle>L, S\<rangle> nba_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nbae_nba, nbae_nba) \<in> \<langle>L, S\<rangle>nbae_rel \<rightarrow> \<langle>L, S\<rangle>nba_rel
[PROOF STEP]
using assms assms(2)[unfolded bijective_alt]
[PROOF STATE]
proof (prove)
using this:
bijective L
bijective S
single_valued S \<and> single_valued (S\<inverse>)

goal (1 subgoal):
 1. (nbae_nba, nbae_nba) \<in> \<langle>L, S\<rangle>nbae_rel \<rightarrow> \<langle>L, S\<rangle>nba_rel
[PROOF STEP]
unfolding nbae_nba_def
[PROOF STATE]
proof (prove)
using this:
bijective L
bijective S
single_valued S \<and> single_valued (S\<inverse>)

goal (1 subgoal):
 1. (\<lambda>A. nba (alphabete A) (initiale A) (succs (transitione A)) (\<lambda>p. p \<in> acceptinge A), \<lambda>A. nba (alphabete A) (initiale A) (succs (transitione A)) (\<lambda>p. p \<in> acceptinge A)) \<in> \<langle>L, S\<rangle>nbae_rel \<rightarrow> \<langle>L, S\<rangle>nba_rel
[PROOF STEP]
by parametricity auto


[STATEMENT]
lemma nbae_nba_nba_nbae_param[param]:
    "((nbae_nba \<circ> nba_nbae) A, id A) \<in> \<langle>Id_on (alphabet A), Id_on (nodes A)\<rangle> nba_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((nbae_nba \<circ> nba_nbae) A, id A) \<in> \<langle>Id_on (alphabet A), Id_on (nodes A)\<rangle>nba_rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((nbae_nba \<circ> nba_nbae) A, id A) \<in> \<langle>Id_on (alphabet A), Id_on (nodes A)\<rangle>nba_rel
[PROOF STEP]
have "(nbae_nba \<circ> nba_nbae) A = nba (alphabet A) (initial A)
      (succs (transitions (alphabet A) (nodes A) (transition A))) (\<lambda> p. p \<in> Set.filter (accepting A) (nodes A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nbae_nba \<circ> nba_nbae) A = nba (alphabet A) (initial A) (succs (transitions (alphabet A) (nodes A) (transition A))) (\<lambda>p. p \<in> Set.filter (accepting A) (nodes A))
[PROOF STEP]
unfolding nbae_nba_def nba_nbae_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>A. nba (alphabete A) (initiale A) (succs (transitione A)) (\<lambda>p. p \<in> acceptinge A)) \<circ> (\<lambda>A. nbae (alphabet A) (initial A) (transitions (alphabet A) (nodes A) (transition A)) (Set.filter (accepting A) (nodes A)))) A = nba (alphabet A) (initial A) (succs (transitions (alphabet A) (nodes A) (transition A))) (\<lambda>p. p \<in> Set.filter (accepting A) (nodes A))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(nbae_nba \<circ> nba_nbae) A = nba (alphabet A) (initial A) (succs (transitions (alphabet A) (nodes A) (transition A))) (\<lambda>p. p \<in> Set.filter (accepting A) (nodes A))

goal (1 subgoal):
 1. ((nbae_nba \<circ> nba_nbae) A, id A) \<in> \<langle>Id_on (alphabet A), Id_on (nodes A)\<rangle>nba_rel
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(nbae_nba \<circ> nba_nbae) A = nba (alphabet A) (initial A) (succs (transitions (alphabet A) (nodes A) (transition A))) (\<lambda>p. p \<in> Set.filter (accepting A) (nodes A))

goal (1 subgoal):
 1. ((nbae_nba \<circ> nba_nbae) A, id A) \<in> \<langle>Id_on (alphabet A), Id_on (nodes A)\<rangle>nba_rel
[PROOF STEP]
have "(\<dots>, nba (alphabet A) (initial A) (transition A) (accepting A)) \<in>
      \<langle>Id_on (alphabet A), Id_on (nodes A)\<rangle> nba_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nba (alphabet A) (initial A) (succs (transitions (alphabet A) (nodes A) (transition A))) (\<lambda>p. p \<in> Set.filter (accepting A) (nodes A)), nba (alphabet A) (initial A) (transition A) (accepting A)) \<in> \<langle>Id_on (alphabet A), Id_on (nodes A)\<rangle>nba_rel
[PROOF STEP]
using nba_rel_eq
[PROOF STATE]
proof (prove)
using this:
(?A, ?A) \<in> \<langle>Id_on (alphabet ?A), Id_on (nodes ?A)\<rangle>nba_rel

goal (1 subgoal):
 1. (nba (alphabet A) (initial A) (succs (transitions (alphabet A) (nodes A) (transition A))) (\<lambda>p. p \<in> Set.filter (accepting A) (nodes A)), nba (alphabet A) (initial A) (transition A) (accepting A)) \<in> \<langle>Id_on (alphabet A), Id_on (nodes A)\<rangle>nba_rel
[PROOF STEP]
by parametricity auto
[PROOF STATE]
proof (state)
this:
(nba (alphabet A) (initial A) (succs (transitions (alphabet A) (nodes A) (transition A))) (\<lambda>p. p \<in> Set.filter (accepting A) (nodes A)), nba (alphabet A) (initial A) (transition A) (accepting A)) \<in> \<langle>Id_on (alphabet A), Id_on (nodes A)\<rangle>nba_rel

goal (1 subgoal):
 1. ((nbae_nba \<circ> nba_nbae) A, id A) \<in> \<langle>Id_on (alphabet A), Id_on (nodes A)\<rangle>nba_rel
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(nba (alphabet A) (initial A) (succs (transitions (alphabet A) (nodes A) (transition A))) (\<lambda>p. p \<in> Set.filter (accepting A) (nodes A)), nba (alphabet A) (initial A) (transition A) (accepting A)) \<in> \<langle>Id_on (alphabet A), Id_on (nodes A)\<rangle>nba_rel

goal (1 subgoal):
 1. ((nbae_nba \<circ> nba_nbae) A, id A) \<in> \<langle>Id_on (alphabet A), Id_on (nodes A)\<rangle>nba_rel
[PROOF STEP]
have  "nba (alphabet A) (initial A) (transition A) (accepting A) = id A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nba (alphabet A) (initial A) (transition A) (accepting A) = id A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nba (alphabet A) (initial A) (transition A) (accepting A) = id A

goal (1 subgoal):
 1. ((nbae_nba \<circ> nba_nbae) A, id A) \<in> \<langle>Id_on (alphabet A), Id_on (nodes A)\<rangle>nba_rel
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((nbae_nba \<circ> nba_nbae) A, id A) \<in> \<langle>Id_on (alphabet A), Id_on (nodes A)\<rangle>nba_rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((nbae_nba \<circ> nba_nbae) A, id A) \<in> \<langle>Id_on (alphabet A), Id_on (nodes A)\<rangle>nba_rel

goal (1 subgoal):
 1. ((nbae_nba \<circ> nba_nbae) A, id A) \<in> \<langle>Id_on (alphabet A), Id_on (nodes A)\<rangle>nba_rel
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
((nbae_nba \<circ> nba_nbae) A, id A) \<in> \<langle>Id_on (alphabet A), Id_on (nodes A)\<rangle>nba_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nbaei_nba_id[param]: "(nbae_nba \<circ> nbaei_nbae, id) \<in> \<langle>L, S\<rangle> nbaei_nba_rel \<rightarrow> \<langle>L, S\<rangle> nba_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nbae_nba \<circ> nbaei_nbae, id) \<in> \<langle>L, S\<rangle>nbaei_nba_rel \<rightarrow> \<langle>L, S\<rangle>nba_rel
[PROOF STEP]
unfolding nbaei_nba_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nbae_nba \<circ> nbaei_nbae, id) \<in> {(Ae, A). (nbae_nba (nbaei_nbae Ae), A) \<in> \<langle>L, S\<rangle>nba_rel} \<rightarrow> \<langle>L, S\<rangle>nba_rel
[PROOF STEP]
by auto


[STATEMENT]
lemma nbae_nba_impl_refine[autoref_rules]:
    assumes "GEN_OP leq HOL.eq (L \<rightarrow> L \<rightarrow> bool_rel)"
    assumes "GEN_OP seq HOL.eq (S \<rightarrow> S \<rightarrow> bool_rel)"
    shows "(nbae_nba_impl leq seq, nbae_nba) \<in> \<langle>L, S\<rangle> nbaei_nbae_rel \<rightarrow> \<langle>L, S\<rangle> nbai_nba_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nbae_nba_impl leq seq, nbae_nba) \<in> \<langle>L, S\<rangle>nbaei_nbae_rel \<rightarrow> \<langle>L, S\<rangle>nbai_nba_rel
[PROOF STEP]
using nbae_nba_impl.refine assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?leq, (=)) \<in> ?L \<rightarrow> ?L \<rightarrow> bool_rel; (?seq, (=)) \<in> ?S \<rightarrow> ?S \<rightarrow> bool_rel\<rbrakk> \<Longrightarrow> (nbae_nba_impl ?leq ?seq, nbae_nba) \<in> \<langle>?L, ?S\<rangle>nbaei_nbae_rel \<rightarrow> \<langle>?L, ?S\<rangle>nbai_nba_rel
GEN_OP leq (=) (L \<rightarrow> L \<rightarrow> bool_rel)
GEN_OP seq (=) (S \<rightarrow> S \<rightarrow> bool_rel)

goal (1 subgoal):
 1. (nbae_nba_impl leq seq, nbae_nba) \<in> \<langle>L, S\<rangle>nbaei_nbae_rel \<rightarrow> \<langle>L, S\<rangle>nbai_nba_rel
[PROOF STEP]
unfolding autoref_tag_defs
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?leq, (=)) \<in> ?L \<rightarrow> ?L \<rightarrow> bool_rel; (?seq, (=)) \<in> ?S \<rightarrow> ?S \<rightarrow> bool_rel\<rbrakk> \<Longrightarrow> (nbae_nba_impl ?leq ?seq, nbae_nba) \<in> \<langle>?L, ?S\<rangle>nbaei_nbae_rel \<rightarrow> \<langle>?L, ?S\<rangle>nbai_nba_rel
(leq, (=)) \<in> L \<rightarrow> L \<rightarrow> bool_rel
(seq, (=)) \<in> S \<rightarrow> S \<rightarrow> bool_rel

goal (1 subgoal):
 1. (nbae_nba_impl leq seq, nbae_nba) \<in> \<langle>L, S\<rangle>nbaei_nbae_rel \<rightarrow> \<langle>L, S\<rangle>nbai_nba_rel
[PROOF STEP]
by this


[STATEMENT]
lemma exec_step_input_StepTD[simp]:
assumes "exec_step_input P C M pc ics = StepT Cs a" shows "ics = Throwing Cs a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ics = Throwing Cs a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
exec_step_input P C M pc ics = StepT Cs a

goal (1 subgoal):
 1. ics = Throwing Cs a
[PROOF STEP]
proof(cases ics)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>exec_step_input P C M pc ics = StepT Cs a; ics = No_ics\<rbrakk> \<Longrightarrow> ics = Throwing Cs a
 2. \<And>x21 x22. \<lbrakk>exec_step_input P C M pc ics = StepT Cs a; ics = Calling x21 x22\<rbrakk> \<Longrightarrow> ics = Throwing Cs a
 3. \<And>x3. \<lbrakk>exec_step_input P C M pc ics = StepT Cs a; ics = Called x3\<rbrakk> \<Longrightarrow> ics = Throwing Cs a
 4. \<And>x41 x42. \<lbrakk>exec_step_input P C M pc ics = StepT Cs a; ics = Throwing x41 x42\<rbrakk> \<Longrightarrow> ics = Throwing Cs a
[PROOF STEP]
case (Called Cs)
[PROOF STATE]
proof (state)
this:
ics = Called Cs

goal (4 subgoals):
 1. \<lbrakk>exec_step_input P C M pc ics = StepT Cs a; ics = No_ics\<rbrakk> \<Longrightarrow> ics = Throwing Cs a
 2. \<And>x21 x22. \<lbrakk>exec_step_input P C M pc ics = StepT Cs a; ics = Calling x21 x22\<rbrakk> \<Longrightarrow> ics = Throwing Cs a
 3. \<And>x3. \<lbrakk>exec_step_input P C M pc ics = StepT Cs a; ics = Called x3\<rbrakk> \<Longrightarrow> ics = Throwing Cs a
 4. \<And>x41 x42. \<lbrakk>exec_step_input P C M pc ics = StepT Cs a; ics = Throwing x41 x42\<rbrakk> \<Longrightarrow> ics = Throwing Cs a
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
exec_step_input P C M pc ics = StepT Cs a
ics = Called Cs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_step_input P C M pc ics = StepT Cs a
ics = Called Cs

goal (1 subgoal):
 1. ics = Throwing Cs a
[PROOF STEP]
by(cases Cs; simp)
[PROOF STATE]
proof (state)
this:
ics = Throwing Cs a

goal (3 subgoals):
 1. \<lbrakk>exec_step_input P C M pc ics = StepT Cs a; ics = No_ics\<rbrakk> \<Longrightarrow> ics = Throwing Cs a
 2. \<And>x21 x22. \<lbrakk>exec_step_input P C M pc ics = StepT Cs a; ics = Calling x21 x22\<rbrakk> \<Longrightarrow> ics = Throwing Cs a
 3. \<And>x41 x42. \<lbrakk>exec_step_input P C M pc ics = StepT Cs a; ics = Throwing x41 x42\<rbrakk> \<Longrightarrow> ics = Throwing Cs a
[PROOF STEP]
qed(auto)


[STATEMENT]
lemma exec_step_input_StepCD[simp]:
assumes "exec_step_input P C M pc ics = StepC C' Cs" shows "ics = Calling C' Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ics = Calling C' Cs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
exec_step_input P C M pc ics = StepC C' Cs

goal (1 subgoal):
 1. ics = Calling C' Cs
[PROOF STEP]
proof(cases ics)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>exec_step_input P C M pc ics = StepC C' Cs; ics = No_ics\<rbrakk> \<Longrightarrow> ics = Calling C' Cs
 2. \<And>x21 x22. \<lbrakk>exec_step_input P C M pc ics = StepC C' Cs; ics = Calling x21 x22\<rbrakk> \<Longrightarrow> ics = Calling C' Cs
 3. \<And>x3. \<lbrakk>exec_step_input P C M pc ics = StepC C' Cs; ics = Called x3\<rbrakk> \<Longrightarrow> ics = Calling C' Cs
 4. \<And>x41 x42. \<lbrakk>exec_step_input P C M pc ics = StepC C' Cs; ics = Throwing x41 x42\<rbrakk> \<Longrightarrow> ics = Calling C' Cs
[PROOF STEP]
case (Called Cs)
[PROOF STATE]
proof (state)
this:
ics = Called Cs

goal (4 subgoals):
 1. \<lbrakk>exec_step_input P C M pc ics = StepC C' Cs; ics = No_ics\<rbrakk> \<Longrightarrow> ics = Calling C' Cs
 2. \<And>x21 x22. \<lbrakk>exec_step_input P C M pc ics = StepC C' Cs; ics = Calling x21 x22\<rbrakk> \<Longrightarrow> ics = Calling C' Cs
 3. \<And>x3. \<lbrakk>exec_step_input P C M pc ics = StepC C' Cs; ics = Called x3\<rbrakk> \<Longrightarrow> ics = Calling C' Cs
 4. \<And>x41 x42. \<lbrakk>exec_step_input P C M pc ics = StepC C' Cs; ics = Throwing x41 x42\<rbrakk> \<Longrightarrow> ics = Calling C' Cs
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
exec_step_input P C M pc ics = StepC C' Cs
ics = Called Cs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_step_input P C M pc ics = StepC C' Cs
ics = Called Cs

goal (1 subgoal):
 1. ics = Calling C' Cs
[PROOF STEP]
by(cases Cs; simp)
[PROOF STATE]
proof (state)
this:
ics = Calling C' Cs

goal (3 subgoals):
 1. \<lbrakk>exec_step_input P C M pc ics = StepC C' Cs; ics = No_ics\<rbrakk> \<Longrightarrow> ics = Calling C' Cs
 2. \<And>x21 x22. \<lbrakk>exec_step_input P C M pc ics = StepC C' Cs; ics = Calling x21 x22\<rbrakk> \<Longrightarrow> ics = Calling C' Cs
 3. \<And>x41 x42. \<lbrakk>exec_step_input P C M pc ics = StepC C' Cs; ics = Throwing x41 x42\<rbrakk> \<Longrightarrow> ics = Calling C' Cs
[PROOF STEP]
qed(auto)


[STATEMENT]
lemma exec_step_input_StepC2D[simp]:
assumes "exec_step_input P C M pc ics = StepC2 C' Cs" shows "ics = Called (C'#Cs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ics = Called (C' # Cs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
exec_step_input P C M pc ics = StepC2 C' Cs

goal (1 subgoal):
 1. ics = Called (C' # Cs)
[PROOF STEP]
proof(cases ics)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>exec_step_input P C M pc ics = StepC2 C' Cs; ics = No_ics\<rbrakk> \<Longrightarrow> ics = Called (C' # Cs)
 2. \<And>x21 x22. \<lbrakk>exec_step_input P C M pc ics = StepC2 C' Cs; ics = Calling x21 x22\<rbrakk> \<Longrightarrow> ics = Called (C' # Cs)
 3. \<And>x3. \<lbrakk>exec_step_input P C M pc ics = StepC2 C' Cs; ics = Called x3\<rbrakk> \<Longrightarrow> ics = Called (C' # Cs)
 4. \<And>x41 x42. \<lbrakk>exec_step_input P C M pc ics = StepC2 C' Cs; ics = Throwing x41 x42\<rbrakk> \<Longrightarrow> ics = Called (C' # Cs)
[PROOF STEP]
case (Called Cs)
[PROOF STATE]
proof (state)
this:
ics = Called Cs

goal (4 subgoals):
 1. \<lbrakk>exec_step_input P C M pc ics = StepC2 C' Cs; ics = No_ics\<rbrakk> \<Longrightarrow> ics = Called (C' # Cs)
 2. \<And>x21 x22. \<lbrakk>exec_step_input P C M pc ics = StepC2 C' Cs; ics = Calling x21 x22\<rbrakk> \<Longrightarrow> ics = Called (C' # Cs)
 3. \<And>x3. \<lbrakk>exec_step_input P C M pc ics = StepC2 C' Cs; ics = Called x3\<rbrakk> \<Longrightarrow> ics = Called (C' # Cs)
 4. \<And>x41 x42. \<lbrakk>exec_step_input P C M pc ics = StepC2 C' Cs; ics = Throwing x41 x42\<rbrakk> \<Longrightarrow> ics = Called (C' # Cs)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
exec_step_input P C M pc ics = StepC2 C' Cs
ics = Called Cs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_step_input P C M pc ics = StepC2 C' Cs
ics = Called Cs

goal (1 subgoal):
 1. ics = Called (C' # Cs)
[PROOF STEP]
by(cases Cs; simp)
[PROOF STATE]
proof (state)
this:
ics = Called (C' # Cs)

goal (3 subgoals):
 1. \<lbrakk>exec_step_input P C M pc ics = StepC2 C' Cs; ics = No_ics\<rbrakk> \<Longrightarrow> ics = Called (C' # Cs)
 2. \<And>x21 x22. \<lbrakk>exec_step_input P C M pc ics = StepC2 C' Cs; ics = Calling x21 x22\<rbrakk> \<Longrightarrow> ics = Called (C' # Cs)
 3. \<And>x41 x42. \<lbrakk>exec_step_input P C M pc ics = StepC2 C' Cs; ics = Throwing x41 x42\<rbrakk> \<Longrightarrow> ics = Called (C' # Cs)
[PROOF STEP]
qed(auto)


[STATEMENT]
lemma exec_step_input_StepID:
assumes "exec_step_input P C M pc ics = StepI i"
shows "(ics = Called [] \<or> ics = No_ics) \<and> instrs_of P C M ! pc = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ics = Called [] \<or> ics = No_ics) \<and> instrs_of P C M ! pc = i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
exec_step_input P C M pc ics = StepI i

goal (1 subgoal):
 1. (ics = Called [] \<or> ics = No_ics) \<and> instrs_of P C M ! pc = i
[PROOF STEP]
proof(cases ics)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>exec_step_input P C M pc ics = StepI i; ics = No_ics\<rbrakk> \<Longrightarrow> (ics = Called [] \<or> ics = No_ics) \<and> instrs_of P C M ! pc = i
 2. \<And>x21 x22. \<lbrakk>exec_step_input P C M pc ics = StepI i; ics = Calling x21 x22\<rbrakk> \<Longrightarrow> (ics = Called [] \<or> ics = No_ics) \<and> instrs_of P C M ! pc = i
 3. \<And>x3. \<lbrakk>exec_step_input P C M pc ics = StepI i; ics = Called x3\<rbrakk> \<Longrightarrow> (ics = Called [] \<or> ics = No_ics) \<and> instrs_of P C M ! pc = i
 4. \<And>x41 x42. \<lbrakk>exec_step_input P C M pc ics = StepI i; ics = Throwing x41 x42\<rbrakk> \<Longrightarrow> (ics = Called [] \<or> ics = No_ics) \<and> instrs_of P C M ! pc = i
[PROOF STEP]
case (Called Cs)
[PROOF STATE]
proof (state)
this:
ics = Called Cs

goal (4 subgoals):
 1. \<lbrakk>exec_step_input P C M pc ics = StepI i; ics = No_ics\<rbrakk> \<Longrightarrow> (ics = Called [] \<or> ics = No_ics) \<and> instrs_of P C M ! pc = i
 2. \<And>x21 x22. \<lbrakk>exec_step_input P C M pc ics = StepI i; ics = Calling x21 x22\<rbrakk> \<Longrightarrow> (ics = Called [] \<or> ics = No_ics) \<and> instrs_of P C M ! pc = i
 3. \<And>x3. \<lbrakk>exec_step_input P C M pc ics = StepI i; ics = Called x3\<rbrakk> \<Longrightarrow> (ics = Called [] \<or> ics = No_ics) \<and> instrs_of P C M ! pc = i
 4. \<And>x41 x42. \<lbrakk>exec_step_input P C M pc ics = StepI i; ics = Throwing x41 x42\<rbrakk> \<Longrightarrow> (ics = Called [] \<or> ics = No_ics) \<and> instrs_of P C M ! pc = i
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
exec_step_input P C M pc ics = StepI i
ics = Called Cs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_step_input P C M pc ics = StepI i
ics = Called Cs

goal (1 subgoal):
 1. (ics = Called [] \<or> ics = No_ics) \<and> instrs_of P C M ! pc = i
[PROOF STEP]
by(cases Cs; simp)
[PROOF STATE]
proof (state)
this:
(ics = Called [] \<or> ics = No_ics) \<and> instrs_of P C M ! pc = i

goal (3 subgoals):
 1. \<lbrakk>exec_step_input P C M pc ics = StepI i; ics = No_ics\<rbrakk> \<Longrightarrow> (ics = Called [] \<or> ics = No_ics) \<and> instrs_of P C M ! pc = i
 2. \<And>x21 x22. \<lbrakk>exec_step_input P C M pc ics = StepI i; ics = Calling x21 x22\<rbrakk> \<Longrightarrow> (ics = Called [] \<or> ics = No_ics) \<and> instrs_of P C M ! pc = i
 3. \<And>x41 x42. \<lbrakk>exec_step_input P C M pc ics = StepI i; ics = Throwing x41 x42\<rbrakk> \<Longrightarrow> (ics = Called [] \<or> ics = No_ics) \<and> instrs_of P C M ! pc = i
[PROOF STEP]
qed(auto)