[STATEMENT]
lemma P16_invariant:
shows "invariant (composition) P16"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant composition P16
[PROOF STEP]
proof (rule invariantI, simp_all only:split_paired_all)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> ioa.start composition \<Longrightarrow> P16 (a, b)
 2. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P16 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P16 (aa, ba)
[PROOF STEP]
fix s1 s2
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> ioa.start composition \<Longrightarrow> P16 (a, b)
 2. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P16 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P16 (aa, ba)
[PROOF STEP]
assume "(s1,s2) \<in> ioa.start (composition)"
[PROOF STATE]
proof (state)
this:
(s1, s2) \<in> ioa.start composition

goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> ioa.start composition \<Longrightarrow> P16 (a, b)
 2. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P16 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P16 (aa, ba)
[PROOF STEP]
thus "P16 (s1,s2)"
[PROOF STATE]
proof (prove)
using this:
(s1, s2) \<in> ioa.start composition

goal (1 subgoal):
 1. P16 (s1, s2)
[PROOF STEP]
using ids
[PROOF STATE]
proof (prove)
using this:
(s1, s2) \<in> ioa.start composition
0 < id1
id1 < id2

goal (1 subgoal):
 1. P16 (s1, s2)
[PROOF STEP]
by (auto simp add:comp_simps)
[PROOF STATE]
proof (state)
this:
P16 (s1, s2)

goal (1 subgoal):
 1. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P16 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P16 (aa, ba)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P16 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P16 (aa, ba)
[PROOF STEP]
fix s1 s2 t1 t2 a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P16 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P16 (aa, ba)
[PROOF STEP]
assume hyp: "P16 (s1,s2)" and trans:"(s1,s2) \<midarrow>a\<midarrow>composition\<longrightarrow> (t1,t2)"
[PROOF STATE]
proof (state)
this:
P16 (s1, s2)
(s1, s2) \<midarrow>a\<midarrow>composition\<longrightarrow> (t1, t2)

goal (1 subgoal):
 1. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P16 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P16 (aa, ba)
[PROOF STEP]
show "P16 (t1,t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P16 (t1, t2)
[PROOF STEP]
using trans and hyp
[PROOF STATE]
proof (prove)
using this:
(s1, s2) \<midarrow>a\<midarrow>composition\<longrightarrow> (t1, t2)
P16 (s1, s2)

goal (1 subgoal):
 1. P16 (t1, t2)
[PROOF STEP]
by (cases rule:trans_elim) auto
[PROOF STATE]
proof (state)
this:
P16 (t1, t2)

goal:
No subgoals!
[PROOF STEP]
qed