[STATEMENT]
lemma nprv_cnjH:
"nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi> \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> \<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv (insert (cnj \<phi>1 \<phi>2) F) \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (insert (cnj \<phi>1 \<phi>2) F) \<psi>
[PROOF STEP]
apply(rule nprv_cut2[of _ \<phi>1 \<phi>2])
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (insert (cnj \<phi>1 \<phi>2) F) \<phi>1
 2. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (insert (cnj \<phi>1 \<phi>2) F) \<phi>2
 3. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> insert (cnj \<phi>1 \<phi>2) F \<subseteq> fmla
 4. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite (insert (cnj \<phi>1 \<phi>2) F)
 5. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<phi>1 \<in> fmla
 6. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<phi>2 \<in> fmla
 7. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 8. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (insert \<phi>2 (insert \<phi>1 (insert (cnj \<phi>1 \<phi>2) F))) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (insert (cnj \<phi>1 \<phi>2) F) \<phi>1
[PROOF STEP]
by (auto simp: nprv_impI_rev prv_imp_cnjL prv_imp_cnjR prv_nprvI)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (insert (cnj \<phi>1 \<phi>2) F) \<phi>2
 2. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> insert (cnj \<phi>1 \<phi>2) F \<subseteq> fmla
 3. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite (insert (cnj \<phi>1 \<phi>2) F)
 4. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<phi>1 \<in> fmla
 5. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<phi>2 \<in> fmla
 6. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 7. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (insert \<phi>2 (insert \<phi>1 (insert (cnj \<phi>1 \<phi>2) F))) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (insert (cnj \<phi>1 \<phi>2) F) \<phi>2
[PROOF STEP]
by (auto simp: nprv_impI_rev prv_imp_cnjL prv_imp_cnjR prv_nprvI)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> insert (cnj \<phi>1 \<phi>2) F \<subseteq> fmla
 2. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite (insert (cnj \<phi>1 \<phi>2) F)
 3. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<phi>1 \<in> fmla
 4. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<phi>2 \<in> fmla
 5. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 6. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (insert \<phi>2 (insert \<phi>1 (insert (cnj \<phi>1 \<phi>2) F))) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> insert (cnj \<phi>1 \<phi>2) F \<subseteq> fmla
[PROOF STEP]
by (auto simp: nprv_impI_rev prv_imp_cnjL prv_imp_cnjR prv_nprvI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite (insert (cnj \<phi>1 \<phi>2) F)
 2. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<phi>1 \<in> fmla
 3. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<phi>2 \<in> fmla
 4. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 5. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (insert \<phi>2 (insert \<phi>1 (insert (cnj \<phi>1 \<phi>2) F))) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> finite (insert (cnj \<phi>1 \<phi>2) F)
[PROOF STEP]
by (auto simp: nprv_impI_rev prv_imp_cnjL prv_imp_cnjR prv_nprvI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<phi>1 \<in> fmla
 2. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<phi>2 \<in> fmla
 3. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 4. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (insert \<phi>2 (insert \<phi>1 (insert (cnj \<phi>1 \<phi>2) F))) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<phi>1 \<in> fmla
[PROOF STEP]
by (auto simp: nprv_impI_rev prv_imp_cnjL prv_imp_cnjR prv_nprvI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<phi>2 \<in> fmla
 2. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 3. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (insert \<phi>2 (insert \<phi>1 (insert (cnj \<phi>1 \<phi>2) F))) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<phi>2 \<in> fmla
[PROOF STEP]
by (auto simp: nprv_impI_rev prv_imp_cnjL prv_imp_cnjR prv_nprvI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 2. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (insert \<phi>2 (insert \<phi>1 (insert (cnj \<phi>1 \<phi>2) F))) \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
[PROOF STEP]
by (auto simp: nprv_impI_rev prv_imp_cnjL prv_imp_cnjR prv_nprvI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv (insert \<phi>2 (insert \<phi>1 (insert (cnj \<phi>1 \<phi>2) F))) \<psi>
[PROOF STEP]
by (meson cnj finite.insertI insert_iff insert_subset nprv_mono subset_insertI)


[STATEMENT]
lemma nprv_exi_commute:
assumes [simp]: "x \<in> var" "y \<in> var" "\<phi> \<in> fmla"
shows "nprv {exi x (exi y \<phi>)} (exi y (exi x \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {exi x (exi y \<phi>)} (exi y (exi x \<phi>))
[PROOF STEP]
apply(rule nprv_exiE0[of x "exi y \<phi>"], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {exi y \<phi>, exi x (exi y \<phi>)} (exi y (exi x \<phi>))
[PROOF STEP]
apply(rule nprv_clear2_2, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {exi y \<phi>} (exi y (exi x \<phi>))
[PROOF STEP]
apply(rule nprv_exiE0[of y \<phi>], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {\<phi>, exi y \<phi>} (exi y (exi x \<phi>))
[PROOF STEP]
apply(rule nprv_clear2_2, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {\<phi>} (exi y (exi x \<phi>))
[PROOF STEP]
apply(rule nprv_exiI[of _ _ "Var y"], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {\<phi>} (exi x \<phi>)
[PROOF STEP]
by (rule nprv_exiI[of _ _ "Var x"], auto)


[STATEMENT]
lemma prv_exi_commute:
assumes [simp]: "x \<in> var" "y \<in> var" "\<phi> \<in> fmla"
shows "prv (imp (exi x (exi y \<phi>)) (exi y (exi x \<phi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (exi x (exi y \<phi>)) (exi y (exi x \<phi>)))
[PROOF STEP]
apply(rule nprv_prvI, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {} (imp (exi x (exi y \<phi>)) (exi y (exi x \<phi>)))
[PROOF STEP]
apply(rule nprv_impI, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {exi x (exi y \<phi>)} (exi y (exi x \<phi>))
[PROOF STEP]
by (rule nprv_exi_commute, auto)


[STATEMENT]
lemma nprv_exuI:
assumes n1: "nprv F (subst \<phi> t x)" and n2: "nprv (insert \<phi> F) (eql (Var x) t)"
and i[simp]: "F \<subseteq> fmla" "finite F" "\<phi> \<in> fmla" "t \<in> trm" "x \<in> var"   "x \<notin> FvarsT t"
and u: "x \<notin> (\<Union>\<phi> \<in> F. Fvars \<phi>)"
shows "nprv F (exu x \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F (exu x \<phi>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nprv F (exu x \<phi>)
[PROOF STEP]
define z where "z \<equiv> getFr [x] [t] [\<phi>]"
[PROOF STATE]
proof (state)
this:
z \<equiv> getFr [x] [t] [\<phi>]

goal (1 subgoal):
 1. nprv F (exu x \<phi>)
[PROOF STEP]
have z_facts[simp]: "z \<in> var" "z \<noteq> x" "x \<noteq> z"   "z \<notin> FvarsT t" "z \<notin> Fvars \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z \<in> var &&& z \<noteq> x) &&& x \<noteq> z &&& z \<notin> FvarsT t &&& z \<notin> Fvars \<phi>
[PROOF STEP]
using getFr_FvarsT_Fvars[of "[x]" "[t]" "[\<phi>]"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set [x] \<subseteq> var; set [t] \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> getFr [x] [t] [\<phi>] \<in> var \<and> getFr [x] [t] [\<phi>] \<notin> set [x] \<and> (?t \<in> set [t] \<longrightarrow> getFr [x] [t] [\<phi>] \<notin> FvarsT ?t) \<and> (?\<phi> \<in> set [\<phi>] \<longrightarrow> getFr [x] [t] [\<phi>] \<notin> Fvars ?\<phi>)

goal (1 subgoal):
 1. (z \<in> var &&& z \<noteq> x) &&& x \<noteq> z &&& z \<notin> FvarsT t &&& z \<notin> Fvars \<phi>
[PROOF STEP]
unfolding z_def[symmetric]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set [x] \<subseteq> var; set [t] \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> z \<in> var \<and> z \<notin> set [x] \<and> (?t \<in> set [t] \<longrightarrow> z \<notin> FvarsT ?t) \<and> (?\<phi> \<in> set [\<phi>] \<longrightarrow> z \<notin> Fvars ?\<phi>)

goal (1 subgoal):
 1. (z \<in> var &&& z \<noteq> x) &&& x \<noteq> z &&& z \<notin> FvarsT t &&& z \<notin> Fvars \<phi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> var
z \<noteq> x
x \<noteq> z
z \<notin> FvarsT t
z \<notin> Fvars \<phi>

goal (1 subgoal):
 1. nprv F (exu x \<phi>)
[PROOF STEP]
have 0: "exu x \<phi> = cnj (exi x \<phi>) (exi z (all x (imp \<phi> (eql (Var x) (Var z)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exu x \<phi> = cnj (exi x \<phi>) (exi z (all x (imp \<phi> (eql (Var x) (Var z)))))
[PROOF STEP]
by (simp add: exu_def_var[of _ z])
[PROOF STATE]
proof (state)
this:
exu x \<phi> = cnj (exi x \<phi>) (exi z (all x (imp \<phi> (eql (Var x) (Var z)))))

goal (1 subgoal):
 1. nprv F (exu x \<phi>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F (exu x \<phi>)
[PROOF STEP]
unfolding 0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F (cnj (exi x \<phi>) (exi z (all x (imp \<phi> (eql (Var x) (Var z))))))
[PROOF STEP]
apply(rule nprv_cnjI, auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nprv F (exi x \<phi>)
 2. nprv F (exi z (all x (imp \<phi> (eql (Var x) (Var z)))))
[PROOF STEP]
apply(rule nprv_exiI[of _ _ t], auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nprv F (subst \<phi> t x)
 2. nprv F (exi z (all x (imp \<phi> (eql (Var x) (Var z)))))
[PROOF STEP]
apply(rule n1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F (exi z (all x (imp \<phi> (eql (Var x) (Var z)))))
[PROOF STEP]
(**)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F (exi z (all x (imp \<phi> (eql (Var x) (Var z)))))
[PROOF STEP]
apply(rule nprv_exiI[of _ _ t], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F (all x (imp \<phi> (eql (Var x) t)))
[PROOF STEP]
apply(rule nprv_allI, insert u, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xa\<in>F. x \<notin> Fvars xa \<Longrightarrow> nprv F (imp \<phi> (eql (Var x) t))
[PROOF STEP]
apply(rule nprv_impI, insert n2, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
nprv F (exu x \<phi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nprv_exuI_var:
assumes n1: "nprv F (subst \<phi> t x)" and n2: "nprv (insert (subst \<phi> (Var y) x) F) (eql (Var y) t)"
and i[simp]: "F \<subseteq> fmla" "finite F" "\<phi> \<in> fmla" "t \<in> trm" "x \<in> var"
"y \<in> var" "y \<notin> FvarsT t" and u: "y \<notin> (\<Union>\<phi> \<in> F. Fvars \<phi>)" and yx: "y = x \<or> y \<notin> Fvars \<phi>"
shows "nprv F (exu x \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F (exu x \<phi>)
[PROOF STEP]
apply(subst exu_rename2[of _ _ y])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<phi> \<in> fmla
 2. x \<in> var
 3. y \<in> var
 4. y = x \<or> y \<notin> Fvars \<phi>
 5. nprv F (exu y (subst \<phi> (Var y) x))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. x \<in> var
 2. y \<in> var
 3. y = x \<or> y \<notin> Fvars \<phi>
 4. nprv F (exu y (subst \<phi> (Var y) x))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> var
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. y \<in> var
 2. y = x \<or> y \<notin> Fvars \<phi>
 3. nprv F (exu y (subst \<phi> (Var y) x))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> var
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. y = x \<or> y \<notin> Fvars \<phi>
 2. nprv F (exu y (subst \<phi> (Var y) x))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = x \<or> y \<notin> Fvars \<phi>
[PROOF STEP]
using yx
[PROOF STATE]
proof (prove)
using this:
y = x \<or> y \<notin> Fvars \<phi>

goal (1 subgoal):
 1. y = x \<or> y \<notin> Fvars \<phi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F (exu y (subst \<phi> (Var y) x))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F (exu y (subst \<phi> (Var y) x))
[PROOF STEP]
apply(intro nprv_exuI[of _ _ t])
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. nprv F (subst (subst \<phi> (Var y) x) t y)
 2. nprv (insert (subst \<phi> (Var y) x) F) (eql (Var y) t)
 3. F \<subseteq> fmla
 4. finite F
 5. subst \<phi> (Var y) x \<in> fmla
 6. t \<in> trm
 7. y \<in> var
 8. y \<notin> FvarsT t
 9. y \<notin> \<Union> (Fvars ` F)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F (subst (subst \<phi> (Var y) x) t y)
[PROOF STEP]
by (metis i(3) i(4) i(5) i(6) n1 subst_same_Var subst_subst yx)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. nprv (insert (subst \<phi> (Var y) x) F) (eql (Var y) t)
 2. F \<subseteq> fmla
 3. finite F
 4. subst \<phi> (Var y) x \<in> fmla
 5. t \<in> trm
 6. y \<in> var
 7. y \<notin> FvarsT t
 8. y \<notin> \<Union> (Fvars ` F)
[PROOF STEP]
using n2 u
[PROOF STATE]
proof (prove)
using this:
nprv (insert (subst \<phi> (Var y) x) F) (eql (Var y) t)
y \<notin> \<Union> (Fvars ` F)

goal (8 subgoals):
 1. nprv (insert (subst \<phi> (Var y) x) F) (eql (Var y) t)
 2. F \<subseteq> fmla
 3. finite F
 4. subst \<phi> (Var y) x \<in> fmla
 5. t \<in> trm
 6. y \<in> var
 7. y \<notin> FvarsT t
 8. y \<notin> \<Union> (Fvars ` F)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.


[STATEMENT]
lemma nprv_exuI_exi:
assumes n1: "nprv F (exi x \<phi>)" and n2: "nprv (insert (subst \<phi> (Var y) x) (insert \<phi> F)) (eql (Var y) (Var x))"
and i[simp]: "F \<subseteq> fmla" "finite F" "\<phi> \<in> fmla" "x \<in> var" "y \<in> var" "y \<noteq> x" "y \<notin> Fvars \<phi>"
and u: "x \<notin> (\<Union>\<phi> \<in> F. Fvars \<phi>)" "y \<notin> (\<Union>\<phi> \<in> F. Fvars \<phi>)"
shows "nprv F (exu x \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F (exu x \<phi>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nprv F (exu x \<phi>)
[PROOF STEP]
have e: "nprv (insert \<phi> F) (exu x \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv (insert \<phi> F) (exu x \<phi>)
[PROOF STEP]
apply(rule nprv_exuI_var[of _ _ "Var x" _ y])
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. nprv (insert \<phi> F) (subst \<phi> (Var x) x)
 2. nprv (insert (subst \<phi> (Var y) x) (insert \<phi> F)) (eql (Var y) (Var x))
 3. insert \<phi> F \<subseteq> fmla
 4. finite (insert \<phi> F)
 5. \<phi> \<in> fmla
 6. Var x \<in> trm
 7. x \<in> var
 8. y \<in> var
 9. y \<notin> FvarsT (Var x)
 10. y \<notin> \<Union> (Fvars ` insert \<phi> F)
A total of 11 subgoals...
[PROOF STEP]
using n2 u
[PROOF STATE]
proof (prove)
using this:
nprv (insert (subst \<phi> (Var y) x) (insert \<phi> F)) (eql (Var y) (Var x))
x \<notin> \<Union> (Fvars ` F)
y \<notin> \<Union> (Fvars ` F)

goal (11 subgoals):
 1. nprv (insert \<phi> F) (subst \<phi> (Var x) x)
 2. nprv (insert (subst \<phi> (Var y) x) (insert \<phi> F)) (eql (Var y) (Var x))
 3. insert \<phi> F \<subseteq> fmla
 4. finite (insert \<phi> F)
 5. \<phi> \<in> fmla
 6. Var x \<in> trm
 7. x \<in> var
 8. y \<in> var
 9. y \<notin> FvarsT (Var x)
 10. y \<notin> \<Union> (Fvars ` insert \<phi> F)
A total of 11 subgoals...
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nprv (insert \<phi> F) (exu x \<phi>)

goal (1 subgoal):
 1. nprv F (exu x \<phi>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F (exu x \<phi>)
[PROOF STEP]
apply(rule nprv_cut[OF n1], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv (insert (exi x \<phi>) F) (exu x \<phi>)
[PROOF STEP]
apply(rule nprv_exiE0, insert u, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>xa\<in>F. x \<notin> Fvars xa; \<forall>x\<in>F. y \<notin> Fvars x\<rbrakk> \<Longrightarrow> nprv (insert \<phi> (insert (exi x \<phi>) F)) (exu x \<phi>)
[PROOF STEP]
apply(rule nprv_mono[OF e], auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
nprv F (exu x \<phi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_exu_imp_exi:
assumes [simp]: "\<phi> \<in> fmla" "x \<in> var"
shows "prv (imp (exu x \<phi>) (exi x \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (exu x \<phi>) (exi x \<phi>))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (exu x \<phi>) (exi x \<phi>))
[PROOF STEP]
define z where z: "z \<equiv> getFr [x] [] [\<phi>]"
[PROOF STATE]
proof (state)
this:
z \<equiv> getFr [x] [] [\<phi>]

goal (1 subgoal):
 1. prv (imp (exu x \<phi>) (exi x \<phi>))
[PROOF STEP]
have z_facts[simp]: "z \<in> var" "z \<noteq> x" "x \<noteq> z" "z \<notin> Fvars \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z \<in> var &&& z \<noteq> x) &&& x \<noteq> z &&& z \<notin> Fvars \<phi>
[PROOF STEP]
using getFr_FvarsT_Fvars[of "[x]" "[]" "[\<phi>]"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set [x] \<subseteq> var; set [] \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> getFr [x] [] [\<phi>] \<in> var \<and> getFr [x] [] [\<phi>] \<notin> set [x] \<and> (?t \<in> set [] \<longrightarrow> getFr [x] [] [\<phi>] \<notin> FvarsT ?t) \<and> (?\<phi> \<in> set [\<phi>] \<longrightarrow> getFr [x] [] [\<phi>] \<notin> Fvars ?\<phi>)

goal (1 subgoal):
 1. (z \<in> var &&& z \<noteq> x) &&& x \<noteq> z &&& z \<notin> Fvars \<phi>
[PROOF STEP]
unfolding z
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set [x] \<subseteq> var; set [] \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> getFr [x] [] [\<phi>] \<in> var \<and> getFr [x] [] [\<phi>] \<notin> set [x] \<and> (?t \<in> set [] \<longrightarrow> getFr [x] [] [\<phi>] \<notin> FvarsT ?t) \<and> (?\<phi> \<in> set [\<phi>] \<longrightarrow> getFr [x] [] [\<phi>] \<notin> Fvars ?\<phi>)

goal (1 subgoal):
 1. (getFr [x] [] [\<phi>] \<in> var &&& getFr [x] [] [\<phi>] \<noteq> x) &&& x \<noteq> getFr [x] [] [\<phi>] &&& getFr [x] [] [\<phi>] \<notin> Fvars \<phi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> var
z \<noteq> x
x \<noteq> z
z \<notin> Fvars \<phi>

goal (1 subgoal):
 1. prv (imp (exu x \<phi>) (exi x \<phi>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (exu x \<phi>) (exi x \<phi>))
[PROOF STEP]
unfolding exu_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (let y = getFr [x] [] [\<phi>] in cnj (exi x \<phi>) (exi y (all x (imp \<phi> (eql (Var x) (Var y)))))) (exi x \<phi>))
[PROOF STEP]
by (simp add: Let_def z[symmetric] prv_imp_cnjL)
[PROOF STATE]
proof (state)
this:
prv (imp (exu x \<phi>) (exi x \<phi>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prv_exu_exi:
  assumes "x \<in> var" "\<phi> \<in> fmla" "prv (exu x \<phi>)"
  shows "prv (exi x \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (exi x \<phi>)
[PROOF STEP]
by (meson assms exi exu prv_exu_imp_exi prv_imp_mp)


[STATEMENT]
lemma nprv_exuE_exi:
assumes n1: "nprv F (exu x \<phi>)" and n2: "nprv (insert \<phi> F) \<psi>"
and i[simp]: "F \<subseteq> fmla" "finite F" "\<phi> \<in> fmla" "x \<in> var" "\<psi> \<in> fmla" "x \<notin> Fvars \<psi>"
and u: "x \<notin> (\<Union>\<phi> \<in> F. Fvars \<phi>)"
shows "nprv F \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
nprv F (exu x \<phi>)
nprv (insert \<phi> F) \<psi>
F \<subseteq> fmla
finite F
\<phi> \<in> fmla
x \<in> var
\<psi> \<in> fmla
x \<notin> Fvars \<psi>
x \<notin> \<Union> (Fvars ` F)

goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
apply-
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> nprv F \<psi>
[PROOF STEP]
apply(rule nprv_exiE[of _ x \<phi>])
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> nprv F (exi x \<phi>)
 2. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> nprv (insert \<phi> F) \<psi>
 3. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> F \<subseteq> fmla
 4. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> finite F
 5. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> \<phi> \<in> fmla
 6. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> x \<in> var
 7. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 8. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> x \<notin> \<Union> (Fvars ` F)
 9. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> x \<notin> Fvars \<psi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> nprv F (exi x \<phi>)
[PROOF STEP]
by (rule nprv_addImpLemmaI[OF prv_exu_imp_exi[of \<phi> x]]) auto
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> nprv (insert \<phi> F) \<psi>
 2. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> F \<subseteq> fmla
 3. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> finite F
 4. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> \<phi> \<in> fmla
 5. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> x \<in> var
 6. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> \<psi> \<in> fmla
 7. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> x \<notin> \<Union> (Fvars ` F)
 8. \<lbrakk>nprv F (exu x \<phi>); nprv (insert \<phi> F) \<psi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla; x \<in> var; \<psi> \<in> fmla; x \<notin> Fvars \<psi>; x \<notin> \<Union> (Fvars ` F)\<rbrakk> \<Longrightarrow> x \<notin> Fvars \<psi>
[PROOF STEP]
by auto


[STATEMENT]
lemma nprv_exuF_exi:
assumes n1: "exu x \<phi> \<in> F" and n2: "nprv (insert \<phi> F) \<psi>"
and i[simp]: "F \<subseteq> fmla" "finite F" "\<phi> \<in> fmla" "x \<in> var" "\<psi> \<in> fmla" "x \<notin> Fvars \<psi>"
and u: "x \<notin> (\<Union>\<phi> \<in> F. Fvars \<phi>)"
shows "nprv F \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
using assms  nprv_exuE_exi nprv_hyp
[PROOF STATE]
proof (prove)
using this:
exu x \<phi> \<in> F
nprv (insert \<phi> F) \<psi>
F \<subseteq> fmla
finite F
\<phi> \<in> fmla
x \<in> var
\<psi> \<in> fmla
x \<notin> Fvars \<psi>
x \<notin> \<Union> (Fvars ` F)
\<lbrakk>nprv ?F (exu ?x ?\<phi>); nprv (insert ?\<phi> ?F) ?\<psi>; ?F \<subseteq> fmla; finite ?F; ?\<phi> \<in> fmla; ?x \<in> var; ?\<psi> \<in> fmla; ?x \<notin> Fvars ?\<psi>; ?x \<notin> \<Union> (Fvars ` ?F)\<rbrakk> \<Longrightarrow> nprv ?F ?\<psi>
\<lbrakk>?\<phi> \<in> ?F; ?F \<subseteq> fmla; finite ?F\<rbrakk> \<Longrightarrow> nprv ?F ?\<phi>

goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
by metis


[STATEMENT]
lemma prv_exu_uni:
assumes [simp]: "\<phi> \<in> fmla" "x \<in> var" "t1 \<in> trm" "t2 \<in> trm"
shows "prv (imp (exu x \<phi>) (imp (subst \<phi> t1 x) (imp (subst \<phi> t2 x) (eql t1 t2))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (exu x \<phi>) (imp (subst \<phi> t1 x) (imp (subst \<phi> t2 x) (eql t1 t2))))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prv (imp (exu x \<phi>) (imp (subst \<phi> t1 x) (imp (subst \<phi> t2 x) (eql t1 t2))))
[PROOF STEP]
define z where z: "z \<equiv> getFr [x] [t1,t2] [\<phi>]"
[PROOF STATE]
proof (state)
this:
z \<equiv> getFr [x] [t1, t2] [\<phi>]

goal (1 subgoal):
 1. prv (imp (exu x \<phi>) (imp (subst \<phi> t1 x) (imp (subst \<phi> t2 x) (eql t1 t2))))
[PROOF STEP]
have z_facts[simp]: "z \<in> var" "z \<noteq> x" "x \<noteq> z" "z \<notin> Fvars \<phi>"  "z \<notin> FvarsT t1" "z \<notin> FvarsT t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z \<in> var &&& z \<noteq> x &&& x \<noteq> z) &&& z \<notin> Fvars \<phi> &&& z \<notin> FvarsT t1 &&& z \<notin> FvarsT t2
[PROOF STEP]
using getFr_FvarsT_Fvars[of "[x]" "[t1,t2]" "[\<phi>]"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set [x] \<subseteq> var; set [t1, t2] \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> getFr [x] [t1, t2] [\<phi>] \<in> var \<and> getFr [x] [t1, t2] [\<phi>] \<notin> set [x] \<and> (?t \<in> set [t1, t2] \<longrightarrow> getFr [x] [t1, t2] [\<phi>] \<notin> FvarsT ?t) \<and> (?\<phi> \<in> set [\<phi>] \<longrightarrow> getFr [x] [t1, t2] [\<phi>] \<notin> Fvars ?\<phi>)

goal (1 subgoal):
 1. (z \<in> var &&& z \<noteq> x &&& x \<noteq> z) &&& z \<notin> Fvars \<phi> &&& z \<notin> FvarsT t1 &&& z \<notin> FvarsT t2
[PROOF STEP]
unfolding z
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set [x] \<subseteq> var; set [t1, t2] \<subseteq> trm; set [\<phi>] \<subseteq> fmla\<rbrakk> \<Longrightarrow> getFr [x] [t1, t2] [\<phi>] \<in> var \<and> getFr [x] [t1, t2] [\<phi>] \<notin> set [x] \<and> (?t \<in> set [t1, t2] \<longrightarrow> getFr [x] [t1, t2] [\<phi>] \<notin> FvarsT ?t) \<and> (?\<phi> \<in> set [\<phi>] \<longrightarrow> getFr [x] [t1, t2] [\<phi>] \<notin> Fvars ?\<phi>)

goal (1 subgoal):
 1. (getFr [x] [t1, t2] [\<phi>] \<in> var &&& getFr [x] [t1, t2] [\<phi>] \<noteq> x &&& x \<noteq> getFr [x] [t1, t2] [\<phi>]) &&& getFr [x] [t1, t2] [\<phi>] \<notin> Fvars \<phi> &&& getFr [x] [t1, t2] [\<phi>] \<notin> FvarsT t1 &&& getFr [x] [t1, t2] [\<phi>] \<notin> FvarsT t2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> var
z \<noteq> x
x \<noteq> z
z \<notin> Fvars \<phi>
z \<notin> FvarsT t1
z \<notin> FvarsT t2

goal (1 subgoal):
 1. prv (imp (exu x \<phi>) (imp (subst \<phi> t1 x) (imp (subst \<phi> t2 x) (eql t1 t2))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (imp (exu x \<phi>) (imp (subst \<phi> t1 x) (imp (subst \<phi> t2 x) (eql t1 t2))))
[PROOF STEP]
apply(rule nprv_prvI, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {} (imp (exu x \<phi>) (imp (subst \<phi> t1 x) (imp (subst \<phi> t2 x) (eql t1 t2))))
[PROOF STEP]
apply(rule nprv_impI, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {exu x \<phi>} (imp (subst \<phi> t1 x) (imp (subst \<phi> t2 x) (eql t1 t2)))
[PROOF STEP]
apply(simp add: exu_def_var[of _ z])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {cnj (exi x \<phi>) (exi z (all x (imp \<phi> (eql (Var x) (Var z)))))} (imp (subst \<phi> t1 x) (imp (subst \<phi> t2 x) (eql t1 t2)))
[PROOF STEP]
apply(rule nprv_cnjE0, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {exi x \<phi>, exi z (all x (imp \<phi> (eql (Var x) (Var z)))), cnj (exi x \<phi>) (exi z (all x (imp \<phi> (eql (Var x) (Var z)))))} (imp (subst \<phi> t1 x) (imp (subst \<phi> t2 x) (eql t1 t2)))
[PROOF STEP]
apply(rule nprv_clear3_1, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {exi z (all x (imp \<phi> (eql (Var x) (Var z)))), cnj (exi x \<phi>) (exi z (all x (imp \<phi> (eql (Var x) (Var z)))))} (imp (subst \<phi> t1 x) (imp (subst \<phi> t2 x) (eql t1 t2)))
[PROOF STEP]
apply(rule nprv_clear2_2, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {exi z (all x (imp \<phi> (eql (Var x) (Var z))))} (imp (subst \<phi> t1 x) (imp (subst \<phi> t2 x) (eql t1 t2)))
[PROOF STEP]
apply(rule nprv_exiE0, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {all x (imp \<phi> (eql (Var x) (Var z))), exi z (all x (imp \<phi> (eql (Var x) (Var z))))} (imp (subst \<phi> t1 x) (imp (subst \<phi> t2 x) (eql t1 t2)))
[PROOF STEP]
apply(rule nprv_clear2_2, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {all x (imp \<phi> (eql (Var x) (Var z)))} (imp (subst \<phi> t1 x) (imp (subst \<phi> t2 x) (eql t1 t2)))
[PROOF STEP]
apply(rule nprv_allE0[of _ _ _ t1], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {imp (subst \<phi> t1 x) (eql t1 (Var z)), all x (imp \<phi> (eql (Var x) (Var z)))} (imp (subst \<phi> t1 x) (imp (subst \<phi> t2 x) (eql t1 t2)))
[PROOF STEP]
apply(rule nprv_allE0[of _ _ _ t2], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {imp (subst \<phi> t2 x) (eql t2 (Var z)), imp (subst \<phi> t1 x) (eql t1 (Var z)), all x (imp \<phi> (eql (Var x) (Var z)))} (imp (subst \<phi> t1 x) (imp (subst \<phi> t2 x) (eql t1 t2)))
[PROOF STEP]
apply(rule nprv_clear3_3, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {imp (subst \<phi> t2 x) (eql t2 (Var z)), imp (subst \<phi> t1 x) (eql t1 (Var z))} (imp (subst \<phi> t1 x) (imp (subst \<phi> t2 x) (eql t1 t2)))
[PROOF STEP]
apply(rule nprv_impI, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {subst \<phi> t1 x, imp (subst \<phi> t2 x) (eql t2 (Var z)), imp (subst \<phi> t1 x) (eql t1 (Var z))} (imp (subst \<phi> t2 x) (eql t1 t2))
[PROOF STEP]
apply(rule nprv_impI, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {subst \<phi> t2 x, subst \<phi> t1 x, imp (subst \<phi> t2 x) (eql t2 (Var z)), imp (subst \<phi> t1 x) (eql t1 (Var z))} (eql t1 t2)
[PROOF STEP]
apply(rule nprv_impE01, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {eql t2 (Var z), subst \<phi> t2 x, subst \<phi> t1 x, imp (subst \<phi> t2 x) (eql t2 (Var z)), imp (subst \<phi> t1 x) (eql t1 (Var z))} (eql t1 t2)
[PROOF STEP]
apply(rule nprv_clear5_2, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {eql t2 (Var z), subst \<phi> t1 x, imp (subst \<phi> t2 x) (eql t2 (Var z)), imp (subst \<phi> t1 x) (eql t1 (Var z))} (eql t1 t2)
[PROOF STEP]
apply(rule nprv_clear4_3, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {eql t2 (Var z), subst \<phi> t1 x, imp (subst \<phi> t1 x) (eql t1 (Var z))} (eql t1 t2)
[PROOF STEP]
apply(rule nprv_impE01, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {eql t1 (Var z), eql t2 (Var z), subst \<phi> t1 x, imp (subst \<phi> t1 x) (eql t1 (Var z))} (eql t1 t2)
[PROOF STEP]
apply(rule nprv_clear4_3, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {eql t1 (Var z), eql t2 (Var z), imp (subst \<phi> t1 x) (eql t1 (Var z))} (eql t1 t2)
[PROOF STEP]
apply(rule nprv_clear3_3, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {eql t1 (Var z), eql t2 (Var z)} (eql t1 t2)
[PROOF STEP]
apply(rule nprv_eql_symE0[of t2 "Var z"], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {eql (Var z) t2, eql t1 (Var z), eql t2 (Var z)} (eql t1 t2)
[PROOF STEP]
apply(rule nprv_eql_transE012, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prv (imp (exu x \<phi>) (imp (subst \<phi> t1 x) (imp (subst \<phi> t2 x) (eql t1 t2))))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eval\<^sub>1_preserves_len:
  "P \<turnstile>\<^sub>1 \<langle>e\<^sub>0,(h\<^sub>0,ls\<^sub>0)\<rangle> \<Rightarrow> \<langle>e\<^sub>1,(h\<^sub>1,ls\<^sub>1)\<rangle> \<Longrightarrow> length ls\<^sub>0 = length ls\<^sub>1"
and evals\<^sub>1_preserves_len:
  "P \<turnstile>\<^sub>1 \<langle>es\<^sub>0,(h\<^sub>0,ls\<^sub>0)\<rangle> [\<Rightarrow>] \<langle>es\<^sub>1,(h\<^sub>1,ls\<^sub>1)\<rangle> \<Longrightarrow> length ls\<^sub>0 = length ls\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<turnstile>\<^sub>1 \<langle>e\<^sub>0,(h\<^sub>0, ls\<^sub>0)\<rangle> \<Rightarrow> \<langle>e\<^sub>1,(h\<^sub>1, ls\<^sub>1)\<rangle> \<Longrightarrow> length ls\<^sub>0 = length ls\<^sub>1) &&& (P \<turnstile>\<^sub>1 \<langle>es\<^sub>0,(h\<^sub>0, ls\<^sub>0)\<rangle> [\<Rightarrow>] \<langle>es\<^sub>1,(h\<^sub>1, ls\<^sub>1)\<rangle> \<Longrightarrow> length ls\<^sub>0 = length ls\<^sub>1)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<turnstile>\<^sub>1 \<langle>e\<^sub>0,(h\<^sub>0, ls\<^sub>0)\<rangle> \<Rightarrow> \<langle>e\<^sub>1,(h\<^sub>1, ls\<^sub>1)\<rangle> \<Longrightarrow> length ls\<^sub>0 = length ls\<^sub>1) &&& (P \<turnstile>\<^sub>1 \<langle>es\<^sub>0,(h\<^sub>0, ls\<^sub>0)\<rangle> [\<Rightarrow>] \<langle>es\<^sub>1,(h\<^sub>1, ls\<^sub>1)\<rangle> \<Longrightarrow> length ls\<^sub>0 = length ls\<^sub>1)
[PROOF STEP]
by (induct rule:eval\<^sub>1_evals\<^sub>1_inducts, simp_all)


[STATEMENT]
lemma evals\<^sub>1_preserves_elen:
  "\<And>es' s s'. P \<turnstile>\<^sub>1 \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>es',s'\<rangle> \<Longrightarrow> length es = length es'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>es' s s'. P \<turnstile>\<^sub>1 \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>es',s'\<rangle> \<Longrightarrow> length es = length es'
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>es' s s'. P \<turnstile>\<^sub>1 \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>es',s'\<rangle> \<Longrightarrow> length es = length es'
[PROOF STEP]
by(induct es type:list) (auto elim:evals\<^sub>1.cases)


[STATEMENT]
lemma eval\<^sub>1_final: "P \<turnstile>\<^sub>1 \<langle>e,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle> \<Longrightarrow> final e'"
 and evals\<^sub>1_final: "P \<turnstile>\<^sub>1 \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>es',s'\<rangle> \<Longrightarrow> finals es'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<turnstile>\<^sub>1 \<langle>e,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle> \<Longrightarrow> final e') &&& (P \<turnstile>\<^sub>1 \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>es',s'\<rangle> \<Longrightarrow> finals es')
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<turnstile>\<^sub>1 \<langle>e,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle> \<Longrightarrow> final e') &&& (P \<turnstile>\<^sub>1 \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>es',s'\<rangle> \<Longrightarrow> finals es')
[PROOF STEP]
by(induct rule:eval\<^sub>1_evals\<^sub>1.inducts, simp_all)


[STATEMENT]
lemma n_sub_one:
  "n(x) \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive (n x)
[PROOF STEP]
by (metis sup_left_top sup_ge2 n_dist_sup n_top)


[STATEMENT]
lemma n_isotone:
  "x \<le> y \<Longrightarrow> n(x) \<le> n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> n x \<le> n y
[PROOF STEP]
by (metis le_iff_sup n_dist_sup)


[STATEMENT]
lemma n_mult_idempotent:
  "n(x) * n(x) = n(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. idempotent (n x)
[PROOF STEP]
by (metis mult_assoc mult_1_right n_export n_sub_mult_bot n_top)


[STATEMENT]
lemma n_mult_bot:
  "n(x) = n(x * bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n x = n (x * bot)
[PROOF STEP]
by (metis sup_commute sup_left_top sup_bot_right mult_left_dist_sup mult_1_right n_dist_sup n_sub_mult_bot n_top)


[STATEMENT]
lemma n_mult_left_upper_bound:
  "n(x) \<le> n(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n x \<le> n (x * y)
[PROOF STEP]
by (metis mult_right_isotone n_isotone n_mult_bot bot_least)


[STATEMENT]
lemma n_mult_right_bot:
  "n(x) * bot = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n x * bot = bot
[PROOF STEP]
by (metis sup_left_top sup_bot_left mult_left_one mult_1_right n_export n_dist_sup n_sub_mult_bot n_top n_bot)


[STATEMENT]
lemma n_mult_n:
  "n(x * n(y)) = n(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (x * n y) = n x
[PROOF STEP]
by (metis mult_assoc n_mult_right_bot n_mult_bot)


[STATEMENT]
lemma n_mult_left_absorb_sup:
  "n(x) * (n(x) \<squnion> n(y)) = n(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n x * (n x \<squnion> n y) = n x
[PROOF STEP]
by (metis sup_left_top mult_left_dist_sup mult_1_right n_dist_sup n_mult_idempotent n_top)


[STATEMENT]
lemma n_mult_right_absorb_sup:
  "(n(x) \<squnion> n(y)) * n(y) = n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n x \<squnion> n y) * n y = n y
[PROOF STEP]
by (metis sup_commute sup_left_top mult_left_one mult_right_dist_sup n_dist_sup n_mult_idempotent n_top)


[STATEMENT]
lemma n_sup_left_absorb_mult:
  "n(x) \<squnion> n(x) * n(y) = n(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n x \<squnion> n x * n y = n x
[PROOF STEP]
using mult_left_dist_sup n_mult_idempotent n_mult_left_absorb_sup
[PROOF STATE]
proof (prove)
using this:
?x * (?y \<squnion> ?z) = ?x * ?y \<squnion> ?x * ?z
idempotent (n ?x)
n ?x * (n ?x \<squnion> n ?y) = n ?x

goal (1 subgoal):
 1. n x \<squnion> n x * n y = n x
[PROOF STEP]
by auto


[STATEMENT]
lemma n_sup_right_absorb_mult:
  "n(x) * n(y) \<squnion> n(y) = n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n x * n y \<squnion> n y = n y
[PROOF STEP]
using mult_right_dist_sup n_mult_idempotent n_mult_right_absorb_sup
[PROOF STATE]
proof (prove)
using this:
(?x \<squnion> ?y) * ?z = ?x * ?z \<squnion> ?y * ?z
idempotent (n ?x)
(n ?x \<squnion> n ?y) * n ?y = n ?y

goal (1 subgoal):
 1. n x * n y \<squnion> n y = n y
[PROOF STEP]
by auto


[STATEMENT]
lemma n_mult_commutative:
  "n(x) * n(y) = n(y) * n(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n x * n y = n y * n x
[PROOF STEP]
by (smt sup_commute mult_left_dist_sup mult_right_dist_sup n_sup_left_absorb_mult n_sup_right_absorb_mult n_export n_mult_idempotent)


[STATEMENT]
lemma n_sup_left_dist_mult:
  "n(x) \<squnion> n(y) * n(z) = (n(x) \<squnion> n(y)) * (n(x) \<squnion> n(z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n x \<squnion> n y * n z = (n x \<squnion> n y) * (n x \<squnion> n z)
[PROOF STEP]
by (metis sup_assoc mult_left_dist_sup mult_right_dist_sup n_sup_right_absorb_mult n_mult_commutative n_mult_left_absorb_sup)


[STATEMENT]
lemma n_sup_right_dist_mult:
  "n(x) * n(y) \<squnion> n(z) = (n(x) \<squnion> n(z)) * (n(y) \<squnion> n(z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n x * n y \<squnion> n z = (n x \<squnion> n z) * (n y \<squnion> n z)
[PROOF STEP]
by (simp add: sup_commute n_sup_left_dist_mult)


[STATEMENT]
lemma n_order:
  "n(x) \<le> n(y) \<longleftrightarrow> n(x) * n(y) = n(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n x \<le> n y) = (n x * n y = n x)
[PROOF STEP]
by (metis le_iff_sup n_sup_right_absorb_mult n_mult_left_absorb_sup)


[STATEMENT]
lemma n_mult_left_lower_bound:
  "n(x) * n(y) \<le> n(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n x * n y \<le> n x
[PROOF STEP]
by (simp add: sup.orderI n_sup_left_absorb_mult)


[STATEMENT]
lemma n_mult_right_lower_bound:
  "n(x) * n(y) \<le> n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n x * n y \<le> n y
[PROOF STEP]
by (simp add: le_iff_sup n_sup_right_absorb_mult)


[STATEMENT]
lemma n_mult_least_upper_bound:
  "n(x) \<le> n(y) \<and> n(x) \<le> n(z) \<longleftrightarrow> n(x) \<le> n(y) * n(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n x \<le> n y \<and> n x \<le> n z) = (n x \<le> n y * n z)
[PROOF STEP]
by (metis order.trans mult_left_isotone n_mult_commutative n_mult_right_lower_bound n_order)


[STATEMENT]
lemma n_mult_left_divisibility:
  "n(x) \<le> n(y) \<longleftrightarrow> (\<exists>z . n(x) = n(y) * n(z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n x \<le> n y) = (\<exists>z. n x = n y * n z)
[PROOF STEP]
by (metis n_mult_commutative n_mult_left_lower_bound n_order)


[STATEMENT]
lemma n_mult_right_divisibility:
  "n(x) \<le> n(y) \<longleftrightarrow> (\<exists>z . n(x) = n(z) * n(y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n x \<le> n y) = (\<exists>z. n x = n z * n y)
[PROOF STEP]
by (simp add: n_mult_commutative n_mult_left_divisibility)


[STATEMENT]
lemma n_one:
  "n(1) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (1::'a) = bot
[PROOF STEP]
by (metis mult_left_one n_mult_bot n_bot)


[STATEMENT]
lemma n_split_equal:
  "x \<squnion> n(x * L) * top = x * bot \<squnion> n(x * L) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> n (x * L) * top = x * bot \<squnion> n (x * L) * top
[PROOF STEP]
using n_split order_trans sup.cobounded1 sup_same_context zero_right_mult_decreasing
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?x * bot \<squnion> n (?x * L) * top
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z
?a \<le> ?a \<squnion> ?b
\<lbrakk>?x \<le> ?y \<squnion> ?z; ?y \<le> ?x \<squnion> ?z\<rbrakk> \<Longrightarrow> ?x \<squnion> ?z = ?y \<squnion> ?z
?x * bot \<le> ?x

goal (1 subgoal):
 1. x \<squnion> n (x * L) * top = x * bot \<squnion> n (x * L) * top
[PROOF STEP]
by blast


[STATEMENT]
lemma n_split_top:
  "x * top \<le> x * bot \<squnion> n(x * L) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * top \<le> x * bot \<squnion> n (x * L) * top
[PROOF STEP]
by (metis mult_left_isotone n_split vector_bot_closed vector_mult_closed vector_sup_closed vector_top_closed)


[STATEMENT]
lemma n_L:
  "n(L) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n L = (1::'a)
[PROOF STEP]
by (metis sup_bot_left order.antisym mult_left_one n_export n_isotone n_mult_commutative n_split_top n_sub_one n_top)


[STATEMENT]
lemma n_split_L:
  "x * L = x * bot \<squnion> n(x * L) * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * L = x * bot \<squnion> n (x * L) * L
[PROOF STEP]
by (metis mult_1_right n_L n_L_split)


[STATEMENT]
lemma n_n_L:
  "n(n(x) * L) = n(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (n x * L) = n x
[PROOF STEP]
by (simp add: n_export n_L)


[STATEMENT]
lemma n_L_decreasing:
  "n(x) * L \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n x * L \<le> x
[PROOF STEP]
by (metis mult_left_zero n_L_split order_trans sup.orderI zero_right_mult_decreasing mult_assoc n_mult_bot)


[STATEMENT]
lemma n_galois:
  "n(x) \<le> n(y) \<longleftrightarrow> n(x) * L \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n x \<le> n y) = (n x * L \<le> y)
[PROOF STEP]
by (metis order.trans mult_left_isotone n_L_decreasing n_isotone n_n_L)


[STATEMENT]
lemma split_L:
  "x * L \<le> x * bot \<squnion> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * L \<le> x * bot \<squnion> L
[PROOF STEP]
by (metis sup_commute sup_left_isotone n_galois n_L n_split_L n_sub_one)


[STATEMENT]
lemma L_left_zero:
  "L * x = L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L * x = L
[PROOF STEP]
by (metis order.antisym mult.left_neutral mult_left_zero zero_right_mult_decreasing n_L n_L_decreasing n_mult_bot mult.assoc)


[STATEMENT]
lemma n_mult:
  "n(x * n(y) * L) = n(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (x * n y * L) = n (x * y)
[PROOF STEP]
using n_L_split n_dist_sup sup.absorb2 n_mult_left_upper_bound n_mult_bot n_n_L
[PROOF STATE]
proof (prove)
using this:
?x * n ?y * L = ?x * bot \<squnion> n (?x * ?y) * L
n (?x \<squnion> ?y) = n ?x \<squnion> n ?y
?a \<le> ?b \<Longrightarrow> ?a \<squnion> ?b = ?b
n ?x \<le> n (?x * ?y)
n ?x = n (?x * bot)
n (n ?x * L) = n ?x

goal (1 subgoal):
 1. n (x * n y * L) = n (x * y)
[PROOF STEP]
by auto


[STATEMENT]
lemma n_mult_top:
  "n(x * n(y) * top) = n(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (x * n y * top) = n (x * y)
[PROOF STEP]
by (metis mult_1_right n_mult n_top)


[STATEMENT]
lemma n_top_L:
  "n(x * top) = n(x * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (x * top) = n (x * L)
[PROOF STEP]
by (metis mult_1_right n_L n_mult_top)


[STATEMENT]
lemma n_top_split:
  "x * n(y) * top \<le> x * bot \<squnion> n(x * y) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * n y * top \<le> x * bot \<squnion> n (x * y) * top
[PROOF STEP]
by (metis mult_assoc n_mult n_mult_right_bot n_split_top)


[STATEMENT]
lemma n_mult_right_upper_bound:
  "n(x * y) \<le> n(z) \<longleftrightarrow> n(x) \<le> n(z) \<and> x * n(y) * L \<le> x * bot \<squnion> n(z) * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n (x * y) \<le> n z) = (n x \<le> n z \<and> x * n y * L \<le> x * bot \<squnion> n z * L)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n (x * y) \<le> n z \<Longrightarrow> n x \<le> n z \<and> x * n y * L \<le> x * bot \<squnion> n z * L
 2. n x \<le> n z \<and> x * n y * L \<le> x * bot \<squnion> n z * L \<Longrightarrow> n (x * y) \<le> n z
[PROOF STEP]
apply (metis sup_right_isotone order.eq_iff mult_isotone n_L_split n_mult_left_upper_bound order_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n x \<le> n z \<and> x * n y * L \<le> x * bot \<squnion> n z * L \<Longrightarrow> n (x * y) \<le> n z
[PROOF STEP]
by (smt (verit, ccfv_threshold) n_dist_sup n_export sup.absorb_iff2 n_mult n_mult_commutative n_mult_bot n_n_L)


[STATEMENT]
lemma n_preserves_equation:
  "n(y) * x \<le> x * n(y) \<longleftrightarrow> n(y) * x = n(y) * x * n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n y * x \<le> x * n y) = (n y * x = n y * x * n y)
[PROOF STEP]
using eq_refl test_preserves_equation n_mult_idempotent n_sub_one
[PROOF STATE]
proof (prove)
using this:
?x = ?y \<Longrightarrow> ?x \<le> ?y
\<lbrakk>dense_rel ?p; coreflexive ?p\<rbrakk> \<Longrightarrow> (?p * ?x \<le> ?x * ?p) = (?p * ?x = ?p * ?x * ?p)
idempotent (n ?x)
coreflexive (n ?x)

goal (1 subgoal):
 1. (n y * x \<le> x * n y) = (n y * x = n y * x * n y)
[PROOF STEP]
by auto


[STATEMENT]
lemma ni_bot:
  "ni(bot) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni bot = bot
[PROOF STEP]
by (simp add: n_bot ni_def)


[STATEMENT]
lemma ni_one:
  "ni(1) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni (1::'a) = bot
[PROOF STEP]
by (simp add: n_one ni_def)


[STATEMENT]
lemma ni_L:
  "ni(L) = L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni L = L
[PROOF STEP]
by (simp add: n_L ni_def)


[STATEMENT]
lemma ni_top:
  "ni(top) = L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni top = L
[PROOF STEP]
by (simp add: n_top ni_def)


[STATEMENT]
lemma ni_dist_sup:
  "ni(x \<squnion> y) = ni(x) \<squnion> ni(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni (x \<squnion> y) = ni x \<squnion> ni y
[PROOF STEP]
by (simp add: mult_right_dist_sup n_dist_sup ni_def)


[STATEMENT]
lemma ni_mult_bot:
  "ni(x) = ni(x * bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni x = ni (x * bot)
[PROOF STEP]
using n_mult_bot ni_def
[PROOF STATE]
proof (prove)
using this:
n ?x = n (?x * bot)
ni ?x = n ?x * L

goal (1 subgoal):
 1. ni x = ni (x * bot)
[PROOF STEP]
by auto


[STATEMENT]
lemma ni_split:
  "x * ni(y) = x * bot \<squnion> ni(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * ni y = x * bot \<squnion> ni (x * y)
[PROOF STEP]
using n_L_split mult_assoc ni_def
[PROOF STATE]
proof (prove)
using this:
?x * n ?y * L = ?x * bot \<squnion> n (?x * ?y) * L
?a * ?b * ?c = ?a * (?b * ?c)
ni ?x = n ?x * L

goal (1 subgoal):
 1. x * ni y = x * bot \<squnion> ni (x * y)
[PROOF STEP]
by auto


[STATEMENT]
lemma ni_decreasing:
  "ni(x) \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni x \<le> x
[PROOF STEP]
by (simp add: n_L_decreasing ni_def)


[STATEMENT]
lemma ni_isotone:
  "x \<le> y \<Longrightarrow> ni(x) \<le> ni(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> ni x \<le> ni y
[PROOF STEP]
using mult_left_isotone n_isotone ni_def
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?x * ?z \<le> ?y * ?z
?x \<le> ?y \<Longrightarrow> n ?x \<le> n ?y
ni ?x = n ?x * L

goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> ni x \<le> ni y
[PROOF STEP]
by auto


[STATEMENT]
lemma ni_mult_left_upper_bound:
  "ni(x) \<le> ni(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni x \<le> ni (x * y)
[PROOF STEP]
using mult_left_isotone n_mult_left_upper_bound ni_def
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?x * ?z \<le> ?y * ?z
n ?x \<le> n (?x * ?y)
ni ?x = n ?x * L

goal (1 subgoal):
 1. ni x \<le> ni (x * y)
[PROOF STEP]
by force


[STATEMENT]
lemma ni_idempotent:
  "ni(ni(x)) = ni(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni (ni x) = ni x
[PROOF STEP]
by (simp add: n_n_L ni_def)


[STATEMENT]
lemma ni_below_L:
  "ni(x) \<le> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni x \<le> L
[PROOF STEP]
using n_L n_galois n_sub_one ni_def
[PROOF STATE]
proof (prove)
using this:
n L = (1::'a)
(n ?x \<le> n ?y) = (n ?x * L \<le> ?y)
coreflexive (n ?x)
ni ?x = n ?x * L

goal (1 subgoal):
 1. ni x \<le> L
[PROOF STEP]
by auto


[STATEMENT]
lemma ni_left_zero:
  "ni(x) * y = ni(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni x * y = ni x
[PROOF STEP]
by (simp add: L_left_zero mult_assoc ni_def)


[STATEMENT]
lemma ni_split_L:
  "x * L = x * bot \<squnion> ni(x * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * L = x * bot \<squnion> ni (x * L)
[PROOF STEP]
using n_split_L ni_def
[PROOF STATE]
proof (prove)
using this:
?x * L = ?x * bot \<squnion> n (?x * L) * L
ni ?x = n ?x * L

goal (1 subgoal):
 1. x * L = x * bot \<squnion> ni (x * L)
[PROOF STEP]
by auto


[STATEMENT]
lemma ni_top_L:
  "ni(x * top) = ni(x * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni (x * top) = ni (x * L)
[PROOF STEP]
by (simp add: n_top_L ni_def)


[STATEMENT]
lemma ni_galois:
  "ni(x) \<le> ni(y) \<longleftrightarrow> ni(x) \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ni x \<le> ni y) = (ni x \<le> y)
[PROOF STEP]
by (metis n_galois n_n_L ni_def)


[STATEMENT]
lemma ni_mult:
  "ni(x * ni(y)) = ni(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni (x * ni y) = ni (x * y)
[PROOF STEP]
using mult_assoc n_mult ni_def
[PROOF STATE]
proof (prove)
using this:
?a * ?b * ?c = ?a * (?b * ?c)
n (?x * n ?y * L) = n (?x * ?y)
ni ?x = n ?x * L

goal (1 subgoal):
 1. ni (x * ni y) = ni (x * y)
[PROOF STEP]
by auto


[STATEMENT]
lemma ni_n_order:
  "ni(x) \<le> ni(y) \<longleftrightarrow> n(x) \<le> n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ni x \<le> ni y) = (n x \<le> n y)
[PROOF STEP]
using n_galois ni_def ni_galois
[PROOF STATE]
proof (prove)
using this:
(n ?x \<le> n ?y) = (n ?x * L \<le> ?y)
ni ?x = n ?x * L
(ni ?x \<le> ni ?y) = (ni ?x \<le> ?y)

goal (1 subgoal):
 1. (ni x \<le> ni y) = (n x \<le> n y)
[PROOF STEP]
by auto


[STATEMENT]
lemma ni_n_equal:
  "ni(x) = ni(y) \<longleftrightarrow> n(x) = n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ni x = ni y) = (n x = n y)
[PROOF STEP]
by (metis n_n_L ni_def)


[STATEMENT]
lemma ni_mult_right_upper_bound:
  "ni(x * y) \<le> ni(z) \<longleftrightarrow> ni(x) \<le> ni(z) \<and> x * ni(y) \<le> x * bot \<squnion> ni(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ni (x * y) \<le> ni z) = (ni x \<le> ni z \<and> x * ni y \<le> x * bot \<squnion> ni z)
[PROOF STEP]
using mult_assoc n_mult_right_upper_bound ni_def ni_n_order
[PROOF STATE]
proof (prove)
using this:
?a * ?b * ?c = ?a * (?b * ?c)
(n (?x * ?y) \<le> n ?z) = (n ?x \<le> n ?z \<and> ?x * n ?y * L \<le> ?x * bot \<squnion> n ?z * L)
ni ?x = n ?x * L
(ni ?x \<le> ni ?y) = (n ?x \<le> n ?y)

goal (1 subgoal):
 1. (ni (x * y) \<le> ni z) = (ni x \<le> ni z \<and> x * ni y \<le> x * bot \<squnion> ni z)
[PROOF STEP]
by auto


[STATEMENT]
lemma n_ni:
  "n(ni(x)) = n(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (ni x) = n x
[PROOF STEP]
by (simp add: n_n_L ni_def)


[STATEMENT]
lemma ni_n:
  "ni(n(x)) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni (n x) = bot
[PROOF STEP]
by (metis n_mult_right_bot ni_mult_bot ni_bot)


[STATEMENT]
lemma ni_n_galois:
  "n(x) \<le> n(y) \<longleftrightarrow> ni(x) \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n x \<le> n y) = (ni x \<le> y)
[PROOF STEP]
by (simp add: n_galois ni_def)


[STATEMENT]
lemma n_mult_ni:
  "n(x * ni(y)) = n(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (x * ni y) = n (x * y)
[PROOF STEP]
using ni_mult ni_n_equal
[PROOF STATE]
proof (prove)
using this:
ni (?x * ni ?y) = ni (?x * ?y)
(ni ?x = ni ?y) = (n ?x = n ?y)

goal (1 subgoal):
 1. n (x * ni y) = n (x * y)
[PROOF STEP]
by auto


[STATEMENT]
lemma ni_mult_n:
  "ni(x * n(y)) = ni(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni (x * n y) = ni x
[PROOF STEP]
by (simp add: n_mult_n ni_def)


[STATEMENT]
lemma ni_export:
  "ni(n(x) * y) = n(x) * ni(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni (n x * y) = n x * ni y
[PROOF STEP]
by (simp add: n_mult_right_bot ni_split)


[STATEMENT]
lemma ni_mult_top:
  "ni(x * n(y) * top) = ni(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni (x * n y * top) = ni (x * y)
[PROOF STEP]
by (simp add: n_mult_top ni_def)


[STATEMENT]
lemma ni_n_bot:
  "ni(x) = bot \<longleftrightarrow> n(x) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ni x = bot) = (n x = bot)
[PROOF STEP]
using n_bot ni_n_equal ni_bot
[PROOF STATE]
proof (prove)
using this:
n bot = bot
(ni ?x = ni ?y) = (n ?x = n ?y)
ni bot = bot

goal (1 subgoal):
 1. (ni x = bot) = (n x = bot)
[PROOF STEP]
by force


[STATEMENT]
lemma ni_n_L:
  "ni(x) = L \<longleftrightarrow> n(x) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ni x = L) = (n x = (1::'a))
[PROOF STEP]
using n_L ni_L ni_n_equal
[PROOF STATE]
proof (prove)
using this:
n L = (1::'a)
ni L = L
(ni ?x = ni ?y) = (n ?x = n ?y)

goal (1 subgoal):
 1. (ni x = L) = (n x = (1::'a))
[PROOF STEP]
by force


[STATEMENT]
lemma simp_nImage[simp]:
  "\<exists>y . Rep_nImage x = n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. Rep_nImage x = n y
[PROOF STEP]
using Rep_nImage
[PROOF STATE]
proof (prove)
using this:
Rep_nImage ?x \<in> {x. \<exists>y. x = n y}

goal (1 subgoal):
 1. \<exists>y. Rep_nImage x = n y
[PROOF STEP]
by simp


[STATEMENT]
lemma mult_L_circ:
  "(x * L)\<^sup>\<circ> = 1 \<squnion> x * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * L)\<^sup>\<circ> = Rf x L
[PROOF STEP]
by (metis L_left_zero circ_mult mult_assoc)


[STATEMENT]
lemma mult_L_circ_mult:
  "(x * L)\<^sup>\<circ> * y = y \<squnion> x * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * L)\<^sup>\<circ> * y = y \<squnion> x * L
[PROOF STEP]
by (metis L_left_zero mult_L_circ mult_assoc mult_left_one mult_right_dist_sup)


[STATEMENT]
lemma circ_L:
  "L\<^sup>\<circ> = L \<squnion> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L\<^sup>\<circ> = L \<squnion> (1::'a)
[PROOF STEP]
by (metis L_left_zero sup_commute circ_left_unfold)


[STATEMENT]
lemma circ_n_L:
  "x\<^sup>\<circ> * n(x) * L = x\<^sup>\<circ> * bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<circ> * n x * L = x\<^sup>\<circ> * bot
[PROOF STEP]
by (metis sup_bot_left circ_left_unfold circ_plus_same mult_left_zero n_L_split n_dist_sup n_mult_bot n_one ni_def ni_split)


[STATEMENT]
lemma n_circ_left_unfold:
  "n(x\<^sup>\<circ>) = n(x * x\<^sup>\<circ>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (x\<^sup>\<circ>) = n (x * x\<^sup>\<circ>)
[PROOF STEP]
by (metis circ_n_L circ_plus_same n_mult n_mult_bot)


[STATEMENT]
lemma ni_circ:
  "ni(x)\<^sup>\<circ> = 1 \<squnion> ni(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni x\<^sup>\<circ> = (1::'a) \<squnion> ni x
[PROOF STEP]
by (simp add: mult_L_circ ni_def)


[STATEMENT]
lemma circ_ni:
  "x\<^sup>\<circ> * ni(x) = x\<^sup>\<circ> * bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<circ> * ni x = x\<^sup>\<circ> * bot
[PROOF STEP]
using circ_n_L ni_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
?x\<^sup>\<circ> * n ?x * L = ?x\<^sup>\<circ> * bot
ni ?x = n ?x * L
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. x\<^sup>\<circ> * ni x = x\<^sup>\<circ> * bot
[PROOF STEP]
by auto


[STATEMENT]
lemma ni_circ_left_unfold:
  "ni(x\<^sup>\<circ>) = ni(x * x\<^sup>\<circ>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ni (x\<^sup>\<circ>) = ni (x * x\<^sup>\<circ>)
[PROOF STEP]
by (simp add: ni_def n_circ_left_unfold)


[STATEMENT]
lemma n_circ_import:
  "n(y) * x \<le> x * n(y) \<Longrightarrow> n(y) * x\<^sup>\<circ> = n(y) * (n(y) * x)\<^sup>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n y * x \<le> x * n y \<Longrightarrow> n y * x\<^sup>\<circ> = n y * (n y * x)\<^sup>\<circ>
[PROOF STEP]
by (simp add: circ_import n_mult_idempotent n_sub_one)


[STATEMENT]
lemma L_below_one_circ:
  "L \<le> 1\<^sup>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L \<le> (1::'a)\<^sup>\<circ>
[PROOF STEP]
by (metis sup_left_divisibility circ_circ circ_one)


[STATEMENT]
lemma circ_below_L_sup_star:
  "x\<^sup>\<circ> \<le> L \<squnion> x\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<circ> \<le> L \<squnion> x\<^sup>\<star>
[PROOF STEP]
by (metis circ_circ circ_increasing)


[STATEMENT]
lemma L_sup_circ_sup_star:
  "L \<squnion> x\<^sup>\<circ> = L \<squnion> x\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L \<squnion> x\<^sup>\<circ> = L \<squnion> x\<^sup>\<star>
[PROOF STEP]
by (metis circ_circ circ_star star_circ)


[STATEMENT]
lemma circ_one_L:
  "1\<^sup>\<circ> = L \<squnion> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a)\<^sup>\<circ> = L \<squnion> (1::'a)
[PROOF STEP]
using circ_circ circ_one star_one
[PROOF STATE]
proof (prove)
using this:
?x\<^sup>\<circ>\<^sup>\<circ> = L \<squnion> ?x\<^sup>\<star>
(1::'a)\<^sup>\<circ> = (1::'a)\<^sup>\<circ>\<^sup>\<circ>
(1::'a)\<^sup>\<star> = (1::'a)

goal (1 subgoal):
 1. (1::'a)\<^sup>\<circ> = L \<squnion> (1::'a)
[PROOF STEP]
by auto


[STATEMENT]
lemma one_circ_zero:
  "L = 1\<^sup>\<circ> * bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L = (1::'a)\<^sup>\<circ> * bot
[PROOF STEP]
by (metis L_left_zero circ_L circ_ni circ_one_L circ_plus_same ni_L)


[STATEMENT]
lemma circ_not_simulate:
  "(\<forall>x y z . x * z \<le> z * y \<longrightarrow> x\<^sup>\<circ> * z \<le> z * y\<^sup>\<circ>) \<longrightarrow> 1 = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x y z. x * z \<le> z * y \<longrightarrow> x\<^sup>\<circ> * z \<le> z * y\<^sup>\<circ>) \<longrightarrow> (1::'a) = bot
[PROOF STEP]
by (metis L_left_zero circ_one_L order.eq_iff mult_left_one mult_left_zero mult_right_sub_dist_sup_left n_L n_bot bot_least)


[STATEMENT]
lemma star_circ_L:
  "x\<^sup>\<star>\<^sup>\<circ> = L \<squnion> x\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<star>\<^sup>\<circ> = L \<squnion> x\<^sup>\<star>
[PROOF STEP]
by (simp add: circ_circ star_circ)


[STATEMENT]
lemma circ_circ_2:
  "x\<^sup>\<circ>\<^sup>\<circ> = L \<squnion> x\<^sup>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<circ>\<^sup>\<circ> = L \<squnion> x\<^sup>\<circ>
[PROOF STEP]
by (simp add: L_sup_circ_sup_star circ_circ)


[STATEMENT]
lemma circ_sup_6:
  "L \<squnion> (x \<squnion> y)\<^sup>\<circ> = (x\<^sup>\<circ> * y\<^sup>\<circ>)\<^sup>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L \<squnion> (x \<squnion> y)\<^sup>\<circ> = (x\<^sup>\<circ> * y\<^sup>\<circ>)\<^sup>\<circ>
[PROOF STEP]
by (metis circ_circ_2 sup_assoc sup_commute circ_sup_1 circ_circ_sup circ_decompose_4)


[STATEMENT]
lemma circ_sup_7:
  "(x\<^sup>\<circ> * y\<^sup>\<circ>)\<^sup>\<circ> = L \<squnion> (x \<squnion> y)\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>\<circ> * y\<^sup>\<circ>)\<^sup>\<circ> = L \<squnion> (x \<squnion> y)\<^sup>\<star>
[PROOF STEP]
using L_sup_circ_sup_star circ_sup_6
[PROOF STATE]
proof (prove)
using this:
L \<squnion> ?x\<^sup>\<circ> = L \<squnion> ?x\<^sup>\<star>
L \<squnion> (?x \<squnion> ?y)\<^sup>\<circ> = (?x\<^sup>\<circ> * ?y\<^sup>\<circ>)\<^sup>\<circ>

goal (1 subgoal):
 1. (x\<^sup>\<circ> * y\<^sup>\<circ>)\<^sup>\<circ> = L \<squnion> (x \<squnion> y)\<^sup>\<star>
[PROOF STEP]
by auto


[STATEMENT]
lemma mult_L_star:
  "(x * L)\<^sup>\<star> = 1 \<squnion> x * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * L)\<^sup>\<star> = Rf x L
[PROOF STEP]
by (simp add: L_left_zero transitive_star mult_assoc)


[STATEMENT]
lemma mult_L_omega:
  "(x * L)\<^sup>\<omega> = x * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * L)\<^sup>\<omega> = x * L
[PROOF STEP]
by (metis L_left_zero omega_slide)


[STATEMENT]
lemma mult_L_sup_star:
  "(x * L \<squnion> y)\<^sup>\<star> = y\<^sup>\<star> \<squnion> y\<^sup>\<star> * x * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * L \<squnion> y)\<^sup>\<star> = y\<^sup>\<star> \<squnion> y\<^sup>\<star> * x * L
[PROOF STEP]
by (metis L_left_zero star.mult_zero_sup_circ_2 sup_commute mult_assoc)


[STATEMENT]
lemma mult_L_sup_omega:
  "(x * L \<squnion> y)\<^sup>\<omega> = y\<^sup>\<omega> \<squnion> y\<^sup>\<star> * x * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * L \<squnion> y)\<^sup>\<omega> = y\<^sup>\<omega> \<squnion> y\<^sup>\<star> * x * L
[PROOF STEP]
by (metis L_left_zero mult_bot_add_omega sup_commute mult_assoc)


[STATEMENT]
lemma mult_L_sup_circ:
  "(x * L \<squnion> y)\<^sup>\<Omega> = n(y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> \<squnion> y\<^sup>\<star> * x * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * L \<squnion> y)\<^sup>\<Omega> = n (y\<^sup>\<omega>) * L \<squnion> y\<^sup>\<star> \<squnion> y\<^sup>\<star> * x * L
[PROOF STEP]
by (smt sup_assoc sup_commute Omega_def le_iff_sup mult_L_sup_omega mult_L_sup_star mult_right_dist_sup n_L_decreasing n_dist_sup)


[STATEMENT]
lemma circ_sup_n:
  "(x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega> = n((x\<^sup>\<star> * y)\<^sup>\<omega>) * L \<squnion> ((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star> \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * n(x\<^sup>\<omega>) * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega> = n ((x\<^sup>\<star> * y)\<^sup>\<omega>) * L \<squnion> ((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star> \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * n (x\<^sup>\<omega>) * L)
[PROOF STEP]
by (smt L_left_zero sup_assoc sup_commute Omega_def mult_L_sup_circ mult_assoc mult_left_dist_sup mult_right_dist_sup)


[STATEMENT]
lemma n_omega_induct:
  "n(y) \<le> n(x * y \<squnion> z) \<Longrightarrow> n(y) \<le> n(x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n y \<le> n (x * y \<squnion> z) \<Longrightarrow> n y \<le> n (x\<^sup>\<omega> \<squnion> x\<^sup>\<star> * z)
[PROOF STEP]
by (smt sup_commute mult_assoc n_dist_sup n_galois n_mult omega_induct)


[STATEMENT]
lemma n_Omega_left_unfold:
  "1 \<squnion> x * x\<^sup>\<Omega> = x\<^sup>\<Omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rf x (x\<^sup>\<Omega>) = x\<^sup>\<Omega>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Rf x (x\<^sup>\<Omega>) = x\<^sup>\<Omega>
[PROOF STEP]
have "1 \<squnion> x * x\<^sup>\<Omega> = 1 \<squnion> x * n(x\<^sup>\<omega>) * L \<squnion> x * x\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rf x (x\<^sup>\<Omega>) = Rf (x * n (x\<^sup>\<omega>)) L \<squnion> x\<^sup>+
[PROOF STEP]
by (simp add: Omega_def semiring.distrib_left sup_assoc mult_assoc)
[PROOF STATE]
proof (state)
this:
Rf x (x\<^sup>\<Omega>) = Rf (x * n (x\<^sup>\<omega>)) L \<squnion> x\<^sup>+

goal (1 subgoal):
 1. Rf x (x\<^sup>\<Omega>) = x\<^sup>\<Omega>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Rf x (x\<^sup>\<Omega>) = Rf (x * n (x\<^sup>\<omega>)) L \<squnion> x\<^sup>+

goal (1 subgoal):
 1. Rf x (x\<^sup>\<Omega>) = x\<^sup>\<Omega>
[PROOF STEP]
have "... = n(x * x\<^sup>\<omega>) * L \<squnion> (1 \<squnion> x * x\<^sup>\<star>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rf (x * n (x\<^sup>\<omega>)) L \<squnion> x\<^sup>+ = n (x * x\<^sup>\<omega>) * L \<squnion> ((1::'a) \<squnion> x\<^sup>+)
[PROOF STEP]
by (metis sup_assoc sup_commute sup_bot_left mult_left_dist_sup n_L_split)
[PROOF STATE]
proof (state)
this:
Rf (x * n (x\<^sup>\<omega>)) L \<squnion> x\<^sup>+ = n (x * x\<^sup>\<omega>) * L \<squnion> ((1::'a) \<squnion> x\<^sup>+)

goal (1 subgoal):
 1. Rf x (x\<^sup>\<Omega>) = x\<^sup>\<Omega>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Rf (x * n (x\<^sup>\<omega>)) L \<squnion> x\<^sup>+ = n (x * x\<^sup>\<omega>) * L \<squnion> ((1::'a) \<squnion> x\<^sup>+)

goal (1 subgoal):
 1. Rf x (x\<^sup>\<Omega>) = x\<^sup>\<Omega>
[PROOF STEP]
have "... = n(x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (x * x\<^sup>\<omega>) * L \<squnion> ((1::'a) \<squnion> x\<^sup>+) = n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star>
[PROOF STEP]
using omega_unfold star_left_unfold_equal
[PROOF STATE]
proof (prove)
using this:
?y\<^sup>\<omega> = ?y * ?y\<^sup>\<omega>
(1::'a) \<squnion> ?x\<^sup>+ = ?x\<^sup>\<star>

goal (1 subgoal):
 1. n (x * x\<^sup>\<omega>) * L \<squnion> ((1::'a) \<squnion> x\<^sup>+) = n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n (x * x\<^sup>\<omega>) * L \<squnion> ((1::'a) \<squnion> x\<^sup>+) = n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star>

goal (1 subgoal):
 1. Rf x (x\<^sup>\<Omega>) = x\<^sup>\<Omega>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n (x * x\<^sup>\<omega>) * L \<squnion> ((1::'a) \<squnion> x\<^sup>+) = n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star>

goal (1 subgoal):
 1. Rf x (x\<^sup>\<Omega>) = x\<^sup>\<Omega>
[PROOF STEP]
have "... = x\<^sup>\<Omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> = x\<^sup>\<Omega>
[PROOF STEP]
by (simp add: Omega_def)
[PROOF STATE]
proof (state)
this:
n (x\<^sup>\<omega>) * L \<squnion> x\<^sup>\<star> = x\<^sup>\<Omega>

goal (1 subgoal):
 1. Rf x (x\<^sup>\<Omega>) = x\<^sup>\<Omega>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Rf x (x\<^sup>\<Omega>) = x\<^sup>\<Omega>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Rf x (x\<^sup>\<Omega>) = x\<^sup>\<Omega>

goal (1 subgoal):
 1. Rf x (x\<^sup>\<Omega>) = x\<^sup>\<Omega>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Rf x (x\<^sup>\<Omega>) = x\<^sup>\<Omega>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma n_Omega_circ_sup:
  "(x \<squnion> y)\<^sup>\<Omega> = (x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<squnion> y)\<^sup>\<Omega> = (x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x \<squnion> y)\<^sup>\<Omega> = (x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega>
[PROOF STEP]
have "(x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega> = n((x\<^sup>\<star> * y)\<^sup>\<omega>) * L \<squnion> ((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star> \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * n(x\<^sup>\<omega>) * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega> = n ((x\<^sup>\<star> * y)\<^sup>\<omega>) * L \<squnion> ((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star> \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * n (x\<^sup>\<omega>) * L)
[PROOF STEP]
by (simp add: circ_sup_n)
[PROOF STATE]
proof (state)
this:
(x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega> = n ((x\<^sup>\<star> * y)\<^sup>\<omega>) * L \<squnion> ((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star> \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * n (x\<^sup>\<omega>) * L)

goal (1 subgoal):
 1. (x \<squnion> y)\<^sup>\<Omega> = (x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega> = n ((x\<^sup>\<star> * y)\<^sup>\<omega>) * L \<squnion> ((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star> \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * n (x\<^sup>\<omega>) * L)

goal (1 subgoal):
 1. (x \<squnion> y)\<^sup>\<Omega> = (x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega>
[PROOF STEP]
have "... = n((x\<^sup>\<star> * y)\<^sup>\<omega>) * L \<squnion> n((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega>) * L \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * bot \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n ((x\<^sup>\<star> * y)\<^sup>\<omega>) * L \<squnion> ((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star> \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * n (x\<^sup>\<omega>) * L) = n ((x\<^sup>\<star> * y)\<^sup>\<omega>) * L \<squnion> n ((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega>) * L \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * bot \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star>
[PROOF STEP]
using n_L_split sup.left_commute sup_commute
[PROOF STATE]
proof (prove)
using this:
?x * n ?y * L = ?x * bot \<squnion> n (?x * ?y) * L
?b \<squnion> (?a \<squnion> ?c) = ?a \<squnion> (?b \<squnion> ?c)
?x \<squnion> ?y = ?y \<squnion> ?x

goal (1 subgoal):
 1. n ((x\<^sup>\<star> * y)\<^sup>\<omega>) * L \<squnion> ((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star> \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * n (x\<^sup>\<omega>) * L) = n ((x\<^sup>\<star> * y)\<^sup>\<omega>) * L \<squnion> n ((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega>) * L \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * bot \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n ((x\<^sup>\<star> * y)\<^sup>\<omega>) * L \<squnion> ((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star> \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * n (x\<^sup>\<omega>) * L) = n ((x\<^sup>\<star> * y)\<^sup>\<omega>) * L \<squnion> n ((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega>) * L \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * bot \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star>

goal (1 subgoal):
 1. (x \<squnion> y)\<^sup>\<Omega> = (x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n ((x\<^sup>\<star> * y)\<^sup>\<omega>) * L \<squnion> ((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star> \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * n (x\<^sup>\<omega>) * L) = n ((x\<^sup>\<star> * y)\<^sup>\<omega>) * L \<squnion> n ((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega>) * L \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * bot \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star>

goal (1 subgoal):
 1. (x \<squnion> y)\<^sup>\<Omega> = (x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega>
[PROOF STEP]
have "... = n((x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega>) * L \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n ((x\<^sup>\<star> * y)\<^sup>\<omega>) * L \<squnion> n ((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega>) * L \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * bot \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star> = n ((x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega>) * L \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star>
[PROOF STEP]
by (smt sup_assoc sup_bot_left mult_left_dist_sup mult_right_dist_sup n_dist_sup)
[PROOF STATE]
proof (state)
this:
n ((x\<^sup>\<star> * y)\<^sup>\<omega>) * L \<squnion> n ((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega>) * L \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * bot \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star> = n ((x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega>) * L \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star>

goal (1 subgoal):
 1. (x \<squnion> y)\<^sup>\<Omega> = (x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n ((x\<^sup>\<star> * y)\<^sup>\<omega>) * L \<squnion> n ((x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega>) * L \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * bot \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star> = n ((x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega>) * L \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star>

goal (1 subgoal):
 1. (x \<squnion> y)\<^sup>\<Omega> = (x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega>
[PROOF STEP]
have "... = (x \<squnion> y)\<^sup>\<Omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n ((x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega>) * L \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star> = (x \<squnion> y)\<^sup>\<Omega>
[PROOF STEP]
by (simp add: Omega_def omega_decompose star.circ_sup_9)
[PROOF STATE]
proof (state)
this:
n ((x\<^sup>\<star> * y)\<^sup>\<omega> \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<omega>) * L \<squnion> (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star> = (x \<squnion> y)\<^sup>\<Omega>

goal (1 subgoal):
 1. (x \<squnion> y)\<^sup>\<Omega> = (x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega> = (x \<squnion> y)\<^sup>\<Omega>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega> = (x \<squnion> y)\<^sup>\<Omega>

goal (1 subgoal):
 1. (x \<squnion> y)\<^sup>\<Omega> = (x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega>
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(x \<squnion> y)\<^sup>\<Omega> = (x\<^sup>\<Omega> * y)\<^sup>\<Omega> * x\<^sup>\<Omega>

goal:
No subgoals!
[PROOF STEP]
qed