[STATEMENT]
lemma IIA_swf: "IIA(swf f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IIA (swf f)
[PROOF STEP]
proof(clarsimp simp: IIA_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P P' a b. \<lbrakk>P \<in> Prof; P' \<in> Prof; \<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)\<rbrakk> \<Longrightarrow> (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
fix P P' a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P P' a b. \<lbrakk>P \<in> Prof; P' \<in> Prof; \<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)\<rbrakk> \<Longrightarrow> (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
assume "P:Prof" "P':Prof" and iff: "\<forall>i. ((a,b) \<in> P i) = ((a,b) \<in> P' i)"
[PROOF STATE]
proof (state)
this:
P \<in> Prof
P' \<in> Prof
\<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)

goal (1 subgoal):
 1. \<And>P P' a b. \<lbrakk>P \<in> Prof; P' \<in> Prof; \<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)\<rbrakk> \<Longrightarrow> (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
hence [simp]: "!!i x. (x,x) ~: P i \<and> (x,x) ~: P' i"
[PROOF STATE]
proof (prove)
using this:
P \<in> Prof
P' \<in> Prof
\<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)

goal (1 subgoal):
 1. \<And>i x. (x, x) \<notin> P i \<and> (x, x) \<notin> P' i
[PROOF STEP]
by(simp add:Prof_def Pi_def slo_defs)
[PROOF STATE]
proof (state)
this:
(?x, ?x) \<notin> P ?i \<and> (?x, ?x) \<notin> P' ?i

goal (1 subgoal):
 1. \<And>P P' a b. \<lbrakk>P \<in> Prof; P' \<in> Prof; \<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)\<rbrakk> \<Longrightarrow> (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
have iff':  "a\<noteq>b \<longrightarrow> (\<forall>i. ((b,a) \<in> P i) = ((b,a) \<in> P' i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> b \<longrightarrow> (\<forall>i. (b <\<^bsub>P i\<^esub> a) = (b <\<^bsub>P' i\<^esub> a))
[PROOF STEP]
using iff \<open>P:Prof\<close> \<open>P':Prof\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)
P \<in> Prof
P' \<in> Prof

goal (1 subgoal):
 1. a \<noteq> b \<longrightarrow> (\<forall>i. (b <\<^bsub>P i\<^esub> a) = (b <\<^bsub>P' i\<^esub> a))
[PROOF STEP]
unfolding Prof_def Pi_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)
P \<in> {f. \<forall>x. x \<in> I \<longrightarrow> f x \<in> Lin}
P' \<in> {f. \<forall>x. x \<in> I \<longrightarrow> f x \<in> Lin}

goal (1 subgoal):
 1. a \<noteq> b \<longrightarrow> (\<forall>i. (b <\<^bsub>P i\<^esub> a) = (b <\<^bsub>P' i\<^esub> a))
[PROOF STEP]
by simp (metis iff notin_Lin_iff)
[PROOF STATE]
proof (state)
this:
a \<noteq> b \<longrightarrow> (\<forall>i. (b <\<^bsub>P i\<^esub> a) = (b <\<^bsub>P' i\<^esub> a))

goal (1 subgoal):
 1. \<And>P P' a b. \<lbrakk>P \<in> Prof; P' \<in> Prof; \<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)\<rbrakk> \<Longrightarrow> (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
let ?abP = "Top {a,b} o P"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P P' a b. \<lbrakk>P \<in> Prof; P' \<in> Prof; \<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)\<rbrakk> \<Longrightarrow> (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
let ?abP' = "Top {a,b} o P'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P P' a b. \<lbrakk>P \<in> Prof; P' \<in> Prof; \<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)\<rbrakk> \<Longrightarrow> (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
have "\<forall>i c. (c, f ?abP) : ?abP i \<longrightarrow> (c, f ?abP) : ?abP' i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i c. c <\<^bsub>(Top {a, b} \<circ> P) i\<^esub> f (Top {a, b} \<circ> P) \<longrightarrow> c <\<^bsub>(Top {a, b} \<circ> P') i\<^esub> f (Top {a, b} \<circ> P)
[PROOF STEP]
using una_Top[of P "{a,b}", OF \<open>P:Prof\<close>] iff iff'
[PROOF STATE]
proof (prove)
using this:
{a, b} \<noteq> {} \<Longrightarrow> f (Top {a, b} \<circ> P) \<in> {a, b}
\<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)
a \<noteq> b \<longrightarrow> (\<forall>i. (b <\<^bsub>P i\<^esub> a) = (b <\<^bsub>P' i\<^esub> a))

goal (1 subgoal):
 1. \<forall>i c. c <\<^bsub>(Top {a, b} \<circ> P) i\<^esub> f (Top {a, b} \<circ> P) \<longrightarrow> c <\<^bsub>(Top {a, b} \<circ> P') i\<^esub> f (Top {a, b} \<circ> P)
[PROOF STEP]
by(auto simp add:Top_def)
[PROOF STATE]
proof (state)
this:
\<forall>i c. c <\<^bsub>(Top {a, b} \<circ> P) i\<^esub> f (Top {a, b} \<circ> P) \<longrightarrow> c <\<^bsub>(Top {a, b} \<circ> P') i\<^esub> f (Top {a, b} \<circ> P)

goal (1 subgoal):
 1. \<And>P P' a b. \<lbrakk>P \<in> Prof; P' \<in> Prof; \<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)\<rbrakk> \<Longrightarrow> (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i c. c <\<^bsub>(Top {a, b} \<circ> P) i\<^esub> f (Top {a, b} \<circ> P) \<longrightarrow> c <\<^bsub>(Top {a, b} \<circ> P') i\<^esub> f (Top {a, b} \<circ> P)
[PROOF STEP]
have "f (Top {a,b} \<circ> P) = f (Top {a,b} \<circ> P')"
[PROOF STATE]
proof (prove)
using this:
\<forall>i c. c <\<^bsub>(Top {a, b} \<circ> P) i\<^esub> f (Top {a, b} \<circ> P) \<longrightarrow> c <\<^bsub>(Top {a, b} \<circ> P') i\<^esub> f (Top {a, b} \<circ> P)

goal (1 subgoal):
 1. f (Top {a, b} \<circ> P) = f (Top {a, b} \<circ> P')
[PROOF STEP]
using Top_in_Prof[OF \<open>P:Prof\<close>] Top_in_Prof[OF \<open>P':Prof\<close>]
          mono[of "Top {a, b} \<circ> P"]
[PROOF STATE]
proof (prove)
using this:
\<forall>i c. c <\<^bsub>(Top {a, b} \<circ> P) i\<^esub> f (Top {a, b} \<circ> P) \<longrightarrow> c <\<^bsub>(Top {a, b} \<circ> P') i\<^esub> f (Top {a, b} \<circ> P)
Top ?S \<circ> P \<in> Prof
Top ?S \<circ> P' \<in> Prof
\<lbrakk>Top {a, b} \<circ> P \<in> Prof; ?P' \<in> Prof; \<forall>i aa. aa <\<^bsub>(Top {a, b} \<circ> P) i\<^esub> f (Top {a, b} \<circ> P) \<longrightarrow> aa <\<^bsub>?P' i\<^esub> f (Top {a, b} \<circ> P)\<rbrakk> \<Longrightarrow> f ?P' = f (Top {a, b} \<circ> P)

goal (1 subgoal):
 1. f (Top {a, b} \<circ> P) = f (Top {a, b} \<circ> P')
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
f (Top {a, b} \<circ> P) = f (Top {a, b} \<circ> P')

goal (1 subgoal):
 1. \<And>P P' a b. \<lbrakk>P \<in> Prof; P' \<in> Prof; \<forall>i. (a <\<^bsub>P i\<^esub> b) = (a <\<^bsub>P' i\<^esub> b)\<rbrakk> \<Longrightarrow> (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
thus "(a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)"
[PROOF STATE]
proof (prove)
using this:
f (Top {a, b} \<circ> P) = f (Top {a, b} \<circ> P')

goal (1 subgoal):
 1. (a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)
[PROOF STEP]
by(simp add: swf_def)
[PROOF STATE]
proof (state)
this:
(a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)

goal:
No subgoals!
[PROOF STEP]
qed