[STATEMENT]
theorem GodExistenceImpliesNecExistence: "\<lfloor>\<^bold>\<exists> G \<^bold>\<rightarrow>  \<^bold>\<box>\<^bold>\<exists>\<^sup>E G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
assume "\<exists>x. G x w"
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w
[PROOF STEP]
obtain g where 1: "G g w"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w

goal (1 subgoal):
 1. (\<And>g. \<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
hence "NE g w"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w

goal (1 subgoal):
 1. \<forall>x. x g w \<and> (\<forall>xa. (xa g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xb. (existsAt xb \<^bold>\<rightarrow> x xb \<^bold>\<rightarrow> xa xb) v)) w) \<longrightarrow> (\<^bold>\<box>mexistsActB x) w
[PROOF STEP]
using A5
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w
\<lfloor>\<P> (\<lambda>x w. \<forall>xa. xa x w \<and> (\<forall>xb. (xb x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. (existsAt x \<^bold>\<rightarrow> xa x \<^bold>\<rightarrow> xb x) v)) w) \<longrightarrow> (\<^bold>\<box>mexistsActB xa) w)\<rfloor>

goal (1 subgoal):
 1. \<forall>x. x g w \<and> (\<forall>xa. (xa g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xb. (existsAt xb \<^bold>\<rightarrow> x xb \<^bold>\<rightarrow> xa xb) v)) w) \<longrightarrow> (\<^bold>\<box>mexistsActB x) w
[PROOF STEP]
by auto                     \<comment> \<open>axiom 11.25\<close>
[PROOF STATE]
proof (state)
this:
\<forall>x. x g w \<and> (\<forall>xa. (xa g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xb. (existsAt xb \<^bold>\<rightarrow> x xb \<^bold>\<rightarrow> xa xb) v)) w) \<longrightarrow> (\<^bold>\<box>mexistsActB x) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
hence "\<forall>Y. (\<E> Y g w) \<longrightarrow> (\<^bold>\<box>\<^bold>\<exists>\<^sup>E Y) w"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x g w \<and> (\<forall>xa. (xa g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xb. (existsAt xb \<^bold>\<rightarrow> x xb \<^bold>\<rightarrow> xa xb) v)) w) \<longrightarrow> (\<^bold>\<box>mexistsActB x) w

goal (1 subgoal):
 1. \<forall>Y. Y g w \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> Y xa \<^bold>\<rightarrow> x xa) v)) w) \<longrightarrow> (\<^bold>\<box>mexistsActB Y) w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>Y. Y g w \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> Y xa \<^bold>\<rightarrow> x xa) v)) w) \<longrightarrow> (\<^bold>\<box>mexistsActB Y) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
hence 2: "(\<E> G g w) \<longrightarrow> (\<^bold>\<box>\<^bold>\<exists>\<^sup>E G) w"
[PROOF STATE]
proof (prove)
using this:
\<forall>Y. Y g w \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> Y xa \<^bold>\<rightarrow> x xa) v)) w) \<longrightarrow> (\<^bold>\<box>mexistsActB Y) w

goal (1 subgoal):
 1. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w
[PROOF STEP]
by (rule allE)
[PROOF STATE]
proof (state)
this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
have  "(\<^bold>\<forall>x. G x \<^bold>\<rightarrow> (\<E> G x)) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w)
[PROOF STEP]
using GodIsEssential
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w))\<rfloor>

goal (1 subgoal):
 1. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w)
[PROOF STEP]
by (rule allE)     \<comment> \<open>GodIsEssential follows from Axioms 11.11 and 11.3B\<close>
[PROOF STATE]
proof (state)
this:
\<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
hence  "(G g \<^bold>\<rightarrow> (\<E> G g)) w"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w)

goal (1 subgoal):
 1. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)
[PROOF STEP]
by (rule allE)
[PROOF STATE]
proof (state)
this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
hence  "G g w \<longrightarrow> \<E> G g w"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)

goal (1 subgoal):
 1. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
from this 1
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)
\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w
[PROOF STEP]
have 3: "\<E> G g w"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)
\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w

goal (1 subgoal):
 1. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)
[PROOF STEP]
by (rule mp)
[PROOF STATE]
proof (state)
this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
from 2 3
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)
[PROOF STEP]
have "(\<^bold>\<box>\<^bold>\<exists>\<^sup>E G) w"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)

goal (1 subgoal):
 1. (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w
[PROOF STEP]
by (rule mp)
[PROOF STATE]
proof (state)
this:
(\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w \<Longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
hence "(\<exists>x. G x w) \<longrightarrow> (\<^bold>\<box>\<^bold>\<exists>\<^sup>E G) w"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w \<Longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w

goal (1 subgoal):
 1. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w
[PROOF STEP]
by (rule impI)
[PROOF STATE]
proof (state)
this:
(\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
hence "((\<^bold>\<exists>x. G x) \<^bold>\<rightarrow>  \<^bold>\<box>\<^bold>\<exists>\<^sup>E G) w"
[PROOF STATE]
proof (prove)
using this:
(\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w

goal (1 subgoal):
 1. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) ?w2) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) ?w2

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) ?w2) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) ?w2

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
by (rule allI)
[PROOF STATE]
proof (state)
this:
\<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "\<lfloor>\<^bold>\<forall>\<Phi>.(\<Phi> \<^bold>\<rightarrow> (\<^bold>\<box> \<Phi>))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
oops


[STATEMENT]
lemma True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
nitpick[satisfy]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
oops \<comment> \<open>model found: axioms still consistent\<close>


[STATEMENT]
lemma modal_distr: "\<lfloor>\<^bold>\<box>(\<phi> \<^bold>\<rightarrow> \<psi>)\<rfloor> \<Longrightarrow> \<lfloor>(\<^bold>\<diamond>\<phi> \<^bold>\<rightarrow> \<^bold>\<diamond>\<psi>)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. universal (\<lambda>w. (r) w \<^bold>\<rightarrow> \<phi> \<^bold>\<rightarrow> \<psi>) \<Longrightarrow> \<lfloor>\<^bold>\<diamond>\<phi> \<^bold>\<rightarrow> \<^bold>\<diamond>\<psi>\<rfloor>
[PROOF STEP]
by blast


[STATEMENT]
lemma modal_trans: "(\<lfloor>\<phi> \<^bold>\<rightarrow> \<psi>\<rfloor> \<and> \<lfloor>\<psi> \<^bold>\<rightarrow> \<chi>\<rfloor>) \<Longrightarrow> \<lfloor>\<phi> \<^bold>\<rightarrow> \<chi>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<phi> \<^bold>\<rightarrow> \<psi>\<rfloor> \<and> \<lfloor>\<psi> \<^bold>\<rightarrow> \<chi>\<rfloor> \<Longrightarrow> \<lfloor>\<phi> \<^bold>\<rightarrow> \<chi>\<rfloor>
[PROOF STEP]
by simp


[STATEMENT]
theorem possExistenceImpliesNecEx: "\<lfloor>\<^bold>\<diamond>\<^bold>\<exists> G \<^bold>\<rightarrow> \<^bold>\<box>\<^bold>\<exists>\<^sup>E G\<rfloor>" \<comment> \<open>local consequence\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>
[PROOF STEP]
have "\<lfloor>\<^bold>\<exists> G \<^bold>\<rightarrow> \<^bold>\<box>\<^bold>\<exists>\<^sup>E G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
using GodExistenceImpliesNecExistence
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
[PROOF STEP]
by simp \<comment> \<open>follows from Axioms 11.11, 11.25 and 11.3B\<close>
[PROOF STATE]
proof (state)
this:
\<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>
[PROOF STEP]
hence "\<lfloor>\<^bold>\<box>(\<^bold>\<exists> G \<^bold>\<rightarrow> \<^bold>\<box>\<^bold>\<exists>\<^sup>E G)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>

goal (1 subgoal):
 1. universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) v)
[PROOF STEP]
using NEC
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) w)\<rfloor>
\<lfloor>?\<phi>\<rfloor> \<Longrightarrow> universal (\<lambda>w. (r) w \<^bold>\<rightarrow> ?\<phi>)

goal (1 subgoal):
 1. universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) v)

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>
[PROOF STEP]
hence 1: "\<lfloor>\<^bold>\<diamond>\<^bold>\<exists> G \<^bold>\<rightarrow> \<^bold>\<diamond>\<^bold>\<box>\<^bold>\<exists>\<^sup>E G\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))) v)

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<^bold>\<rightarrow> \<^bold>\<diamond>\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>
[PROOF STEP]
by (rule modal_distr)
[PROOF STATE]
proof (state)
this:
\<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<^bold>\<rightarrow> \<^bold>\<diamond>\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>
[PROOF STEP]
have 2: "\<lfloor>\<^bold>\<diamond>\<^bold>\<box>\<^bold>\<exists>\<^sup>E G \<^bold>\<rightarrow> \<^bold>\<box>\<^bold>\<exists>\<^sup>E G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>
[PROOF STEP]
using symm tran
[PROOF STATE]
proof (prove)
using this:
universal (\<lambda>x y. x r y \<longrightarrow> y r x)
universal (\<lambda>x y. \<lfloor>(\<lambda>z. x r y \<and> y r z \<longrightarrow> x r z)\<rfloor>)

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>
[PROOF STEP]
by metis \<comment> \<open>frame conditions\<close>
[PROOF STATE]
proof (state)
this:
\<lfloor>\<^bold>\<diamond>\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>
[PROOF STEP]
from 1 2
[PROOF STATE]
proof (chain)
picking this:
\<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<^bold>\<rightarrow> \<^bold>\<diamond>\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>
\<lfloor>\<^bold>\<diamond>\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>
[PROOF STEP]
have "\<lfloor>\<^bold>\<diamond>\<^bold>\<exists> G \<^bold>\<rightarrow> \<^bold>\<diamond>\<^bold>\<box>\<^bold>\<exists>\<^sup>E G\<rfloor> \<and> \<lfloor>\<^bold>\<diamond>\<^bold>\<box>\<^bold>\<exists>\<^sup>E G \<^bold>\<rightarrow> \<^bold>\<box>\<^bold>\<exists>\<^sup>E G\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<^bold>\<rightarrow> \<^bold>\<diamond>\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>
\<lfloor>\<^bold>\<diamond>\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<^bold>\<rightarrow> \<^bold>\<diamond>\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor> \<and> \<lfloor>\<^bold>\<diamond>\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<^bold>\<rightarrow> \<^bold>\<diamond>\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor> \<and> \<lfloor>\<^bold>\<diamond>\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<^bold>\<rightarrow> \<^bold>\<diamond>\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor> \<and> \<lfloor>\<^bold>\<diamond>\<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>
[PROOF STEP]
by (rule modal_trans)
[PROOF STATE]
proof (state)
this:
\<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma T4: "\<lfloor>\<^bold>\<diamond>\<^bold>\<exists> G\<rfloor> \<longrightarrow> \<lfloor>\<^bold>\<box>\<^bold>\<exists>\<^sup>E G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. serial (\<lambda>w v. w r v \<and> (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<longrightarrow> universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)))
[PROOF STEP]
using possExistenceImpliesNecEx
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<^bold>\<diamond>(\<lambda>v. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v))\<rfloor>

goal (1 subgoal):
 1. serial (\<lambda>w v. w r v \<and> (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<longrightarrow> universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)))
[PROOF STEP]
by (rule localImpGlobalCons)  \<comment> \<open>global consequence\<close>


[STATEMENT]
lemma GodNecExists: "\<lfloor>\<^bold>\<box>\<^bold>\<exists>\<^sup>E G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)))
[PROOF STEP]
using T3 T4
[PROOF STATE]
proof (prove)
using this:
serial (\<lambda>w v. w r v \<and> (\<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)))
serial (\<lambda>w v. w r v \<and> (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<longrightarrow> universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)))

goal (1 subgoal):
 1. universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)))
[PROOF STEP]
by metis


[STATEMENT]
lemma God_starNecExists: "\<lfloor>\<^bold>\<box>\<^bold>\<exists>\<^sup>E G*\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v = xa x v)))
[PROOF STEP]
using GodNecExists GodDefsAreEquivalent
[PROOF STATE]
proof (prove)
using this:
universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)))
\<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) = (\<forall>xa. \<P> xa w = xa x w))\<rfloor>

goal (1 subgoal):
 1. universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. \<P> xa v = xa x v)))
[PROOF STEP]
by simp


[STATEMENT]
theorem Monotheism_LeibnizEq: "\<lfloor>\<^bold>\<forall>x. G x \<^bold>\<rightarrow> (\<^bold>\<forall>y. G y \<^bold>\<rightarrow> (x  \<^bold>\<approx>\<^sup>L y))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) \<longrightarrow> (\<forall>xb. (xb x \<^bold>\<rightarrow> xb xa) w)))\<rfloor>
[PROOF STEP]
using GodDefsAreEquivalent
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) = (\<forall>xa. \<P> xa w = xa x w))\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) \<longrightarrow> (\<forall>xb. (xb x \<^bold>\<rightarrow> xb xa) w)))\<rfloor>
[PROOF STEP]
by simp


[STATEMENT]
lemma GodExistenceIsValid: "\<lfloor>\<^bold>\<exists>\<^sup>E G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. existsAt x w \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w))\<rfloor>
[PROOF STEP]
using GodNecExists refl
[PROOF STATE]
proof (prove)
using this:
universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)))
reflexive (r)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. existsAt x w \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w))\<rfloor>
[PROOF STEP]
by auto \<comment> \<open>reflexivity is now required by the solver\<close>


[STATEMENT]
theorem Monotheism_normalModel: "\<lfloor>\<^bold>\<exists>x.\<^bold>\<forall>y. G y \<^bold>\<leftrightarrow> x \<^bold>\<approx> y\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>
[PROOF STEP]
have "\<lfloor>\<^bold>\<exists>\<^sup>E G\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. existsAt x w \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w))\<rfloor>
[PROOF STEP]
using GodExistenceIsValid
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<exists>x. existsAt x w \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w))\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. existsAt x w \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w))\<rfloor>
[PROOF STEP]
by simp \<comment> \<open>follows from corollary 11.28\<close>
[PROOF STATE]
proof (state)
this:
\<lfloor>(\<lambda>w. \<exists>x. existsAt x w \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w))\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>
[PROOF STEP]
hence "(\<^bold>\<exists>\<^sup>E G) w"
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<exists>x. existsAt x w \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w))\<rfloor>

goal (1 subgoal):
 1. \<exists>x. existsAt x w \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w)
[PROOF STEP]
by (rule allE)
[PROOF STATE]
proof (state)
this:
\<exists>x. existsAt x w \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. existsAt x w \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w)
[PROOF STEP]
obtain g where 1: "existsAt g w \<and> G g w"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. existsAt x w \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w)

goal (1 subgoal):
 1. (\<And>g. existsAt g w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
existsAt g w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>
[PROOF STEP]
hence 2: "\<E> G g w"
[PROOF STATE]
proof (prove)
using this:
existsAt g w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w)

goal (1 subgoal):
 1. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)
[PROOF STEP]
using GodIsEssential
[PROOF STATE]
proof (prove)
using this:
existsAt g w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w)
\<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w))\<rfloor>

goal (1 subgoal):
 1. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)
[PROOF STEP]
by blast \<comment> \<open>follows from ax. 11.11/11.3B\<close>
[PROOF STATE]
proof (state)
this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>
[PROOF STEP]
have "G y w \<longleftrightarrow> (g \<^bold>\<approx> y) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) = (g = y)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w \<Longrightarrow> g = y
 2. g = y \<Longrightarrow> \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
assume "G y w"
[PROOF STATE]
proof (state)
this:
\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w

goal (2 subgoals):
 1. \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w \<Longrightarrow> g = y
 2. g = y \<Longrightarrow> \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
hence 3: "\<E> G y w"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w

goal (1 subgoal):
 1. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)
[PROOF STEP]
using GodIsEssential
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
\<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w))\<rfloor>

goal (1 subgoal):
 1. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)

goal (2 subgoals):
 1. \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w \<Longrightarrow> g = y
 2. g = y \<Longrightarrow> \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
have "(\<E> G y \<^bold>\<rightarrow> (G \<Rrightarrow> id y)) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> x = y)) w
[PROOF STEP]
using EssencesCharacterizeCompletely
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x xa. x xa w \<and> (\<forall>xb. (xb xa \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. (existsAt xa \<^bold>\<rightarrow> x xa \<^bold>\<rightarrow> xb xa) v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>xb. existsAt xb v \<longrightarrow> x xb v \<longrightarrow> xb = xa)) w)\<rfloor>

goal (1 subgoal):
 1. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> x = y)) w
[PROOF STEP]
by simp \<comment> \<open>follows from theorem 11.23\<close>
[PROOF STATE]
proof (state)
this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> x = y)) w

goal (2 subgoals):
 1. \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w \<Longrightarrow> g = y
 2. g = y \<Longrightarrow> \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
hence "\<E> G y w \<longrightarrow> ((G \<Rrightarrow> id y) w)"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> x = y)) w

goal (1 subgoal):
 1. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> x = y)) w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> x = y)) w

goal (2 subgoals):
 1. \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w \<Longrightarrow> g = y
 2. g = y \<Longrightarrow> \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
from this 3
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> x = y)) w
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)
[PROOF STEP]
have "(G \<Rrightarrow> id y) w"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w) \<longrightarrow> (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> x = y)) w
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)

goal (1 subgoal):
 1. (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> x = y)) w
[PROOF STEP]
by (rule mp)
[PROOF STATE]
proof (state)
this:
(\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> x = y)) w

goal (2 subgoals):
 1. \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w \<Longrightarrow> g = y
 2. g = y \<Longrightarrow> \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
hence "(\<^bold>\<box>(\<^bold>\<forall>\<^sup>Ez. G z \<^bold>\<rightarrow> z \<^bold>\<approx> y)) w"
[PROOF STATE]
proof (prove)
using this:
(\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> x = y)) w

goal (1 subgoal):
 1. (\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> x = y)) w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> x = y)) w

goal (2 subgoals):
 1. \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w \<Longrightarrow> g = y
 2. g = y \<Longrightarrow> \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
hence "\<forall>x. w r x \<longrightarrow> ((\<forall>z. (existsAt z x \<and> G z x) \<longrightarrow> z = y))"
[PROOF STATE]
proof (prove)
using this:
(\<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> x = y)) w

goal (1 subgoal):
 1. (\<^bold>\<box>(\<lambda>x. \<forall>z. existsAt z x \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa z) x) \<longrightarrow> z = y)) w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<^bold>\<box>(\<lambda>x. \<forall>z. existsAt z x \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa z) x) \<longrightarrow> z = y)) w

goal (2 subgoals):
 1. \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w \<Longrightarrow> g = y
 2. g = y \<Longrightarrow> \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
hence "w r w \<longrightarrow> ((\<forall>z. (existsAt z w \<and> G z w) \<longrightarrow> z = y))"
[PROOF STATE]
proof (prove)
using this:
(\<^bold>\<box>(\<lambda>x. \<forall>z. existsAt z x \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa z) x) \<longrightarrow> z = y)) w

goal (1 subgoal):
 1. w r w \<longrightarrow> (\<forall>z. existsAt z w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x z) w) \<longrightarrow> z = y)
[PROOF STEP]
by (rule allE)
[PROOF STATE]
proof (state)
this:
w r w \<longrightarrow> (\<forall>z. existsAt z w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x z) w) \<longrightarrow> z = y)

goal (2 subgoals):
 1. \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w \<Longrightarrow> g = y
 2. g = y \<Longrightarrow> \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
hence "\<forall>z. (w r w \<and> existsAt z w \<and> G z w) \<longrightarrow> z = y"
[PROOF STATE]
proof (prove)
using this:
w r w \<longrightarrow> (\<forall>z. existsAt z w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x z) w) \<longrightarrow> z = y)

goal (1 subgoal):
 1. \<forall>z. w r w \<and> existsAt z w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x z) w) \<longrightarrow> z = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>z. w r w \<and> existsAt z w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x z) w) \<longrightarrow> z = y

goal (2 subgoals):
 1. \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w \<Longrightarrow> g = y
 2. g = y \<Longrightarrow> \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
hence 4: "(w r w \<and> existsAt g w \<and> G g w) \<longrightarrow> g = y"
[PROOF STATE]
proof (prove)
using this:
\<forall>z. w r w \<and> existsAt z w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x z) w) \<longrightarrow> z = y

goal (1 subgoal):
 1. w r w \<and> existsAt g w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<longrightarrow> g = y
[PROOF STEP]
by (rule allE)
[PROOF STATE]
proof (state)
this:
w r w \<and> existsAt g w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<longrightarrow> g = y

goal (2 subgoals):
 1. \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w \<Longrightarrow> g = y
 2. g = y \<Longrightarrow> \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
have "w r w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w r w
[PROOF STEP]
using refl
[PROOF STATE]
proof (prove)
using this:
reflexive (r)

goal (1 subgoal):
 1. w r w
[PROOF STEP]
by simp \<comment> \<open>using frame reflexivity (Axiom M)\<close>
[PROOF STATE]
proof (state)
this:
w r w

goal (2 subgoals):
 1. \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w \<Longrightarrow> g = y
 2. g = y \<Longrightarrow> \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
hence  "w r w \<and> (existsAt g w \<and> G g w)"
[PROOF STATE]
proof (prove)
using this:
w r w

goal (1 subgoal):
 1. w r w \<and> existsAt g w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
w r w
existsAt g w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w)

goal (1 subgoal):
 1. w r w \<and> existsAt g w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w)
[PROOF STEP]
by (rule conjI)
[PROOF STATE]
proof (state)
this:
w r w \<and> existsAt g w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w)

goal (2 subgoals):
 1. \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w \<Longrightarrow> g = y
 2. g = y \<Longrightarrow> \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
from 4 this
[PROOF STATE]
proof (chain)
picking this:
w r w \<and> existsAt g w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<longrightarrow> g = y
w r w \<and> existsAt g w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w)
[PROOF STEP]
have "g = y"
[PROOF STATE]
proof (prove)
using this:
w r w \<and> existsAt g w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<longrightarrow> g = y
w r w \<and> existsAt g w \<and> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w)

goal (1 subgoal):
 1. g = y
[PROOF STEP]
by (rule mp)
[PROOF STATE]
proof (state)
this:
g = y

goal (2 subgoals):
 1. \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w \<Longrightarrow> g = y
 2. g = y \<Longrightarrow> \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
thus "(g \<^bold>\<approx> y) w"
[PROOF STATE]
proof (prove)
using this:
g = y

goal (1 subgoal):
 1. g = y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g = y

goal (1 subgoal):
 1. g = y \<Longrightarrow> \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g = y \<Longrightarrow> \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
assume "(g \<^bold>\<approx> y) w"
[PROOF STATE]
proof (state)
this:
g = y

goal (1 subgoal):
 1. g = y \<Longrightarrow> \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
from this 2
[PROOF STATE]
proof (chain)
picking this:
g = y
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)
[PROOF STEP]
have "\<E> G y w"
[PROOF STATE]
proof (prove)
using this:
g = y
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x g) w) \<and> (\<forall>x. (x g \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)

goal (1 subgoal):
 1. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)

goal (1 subgoal):
 1. g = y \<Longrightarrow> \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
thus "G y w "
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) \<and> (\<forall>x. (x y \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>xa. existsAt xa v \<longrightarrow> (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) v) \<longrightarrow> x xa v)) w)

goal (1 subgoal):
 1. \<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w
[PROOF STEP]
by (rule conjunct1)
[PROOF STATE]
proof (state)
this:
\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) = (g = y)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x ?y2) w) = (g = ?y2)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>
[PROOF STEP]
hence "\<forall>y. G y w \<longleftrightarrow> (g \<^bold>\<approx> y) w"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. (\<P> x \<^bold>\<rightarrow> x ?y2) w) = (g = ?y2)

goal (1 subgoal):
 1. \<forall>y. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) = (g = y)
[PROOF STEP]
by (rule allI)
[PROOF STATE]
proof (state)
this:
\<forall>y. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) = (g = y)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>
[PROOF STEP]
hence "\<exists>x. (\<forall>y. G y w \<longleftrightarrow> (x \<^bold>\<approx> y) w)"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) = (g = y)

goal (1 subgoal):
 1. \<exists>x. \<forall>y. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) = (x = y)
[PROOF STEP]
by (rule exI)
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>y. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) = (x = y)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>
[PROOF STEP]
hence "(\<^bold>\<exists>x. (\<^bold>\<forall>y. G y \<^bold>\<leftrightarrow> (x \<^bold>\<approx> y))) w"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. \<forall>y. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x y) w) = (x = y)

goal (1 subgoal):
 1. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) ?w2) = (x = xa)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) ?w2) = (x = xa)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>
[PROOF STEP]
by (rule allI)
[PROOF STATE]
proof (state)
this:
\<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma GodImpliesExistence: "\<lfloor>\<^bold>\<forall>x. G x \<^bold>\<rightarrow> E! x\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<exists>xa. existsAt xa w \<and> xa = x))\<rfloor>
[PROOF STEP]
using GodExistenceIsValid Monotheism_normalModel
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<exists>x. existsAt x w \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w))\<rfloor>
\<lfloor>(\<lambda>w. \<exists>x. \<forall>xa. (\<forall>x. (\<P> x \<^bold>\<rightarrow> x xa) w) = (x = xa))\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<exists>xa. existsAt xa w \<and> xa = x))\<rfloor>
[PROOF STEP]
by metis


[STATEMENT]
lemma PosPropertiesNecExist: "\<lfloor>\<^bold>\<forall>Y. \<P> Y \<^bold>\<rightarrow> \<^bold>\<box>\<^bold>\<exists>\<^sup>E Y\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<P> x \<^bold>\<rightarrow> \<^bold>\<box>mexistsActB x) w)\<rfloor>
[PROOF STEP]
using GodNecExists A4a
[PROOF STATE]
proof (prove)
using this:
universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)))
\<lfloor>(\<lambda>w. \<forall>x. (\<P> x \<^bold>\<rightarrow> \<^bold>\<box>\<P> x) w)\<rfloor>

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (\<P> x \<^bold>\<rightarrow> \<^bold>\<box>mexistsActB x) w)\<rfloor>
[PROOF STEP]
by meson \<comment> \<open>proposition 11.31: follows from corollary 11.28 and axiom A4a\<close>


[STATEMENT]
lemma useful: "(\<forall>x. \<phi> x \<longrightarrow> \<psi>) \<Longrightarrow> ((\<exists>x. \<phi> x) \<longrightarrow> \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. \<phi> x \<longrightarrow> \<psi> \<Longrightarrow> (\<exists>x. \<phi> x) \<longrightarrow> \<psi>
[PROOF STEP]
by simp


[STATEMENT]
lemma ModalCollapse: "\<lfloor>\<^bold>\<forall>\<Phi>.(\<Phi> \<^bold>\<rightarrow> (\<^bold>\<box> \<Phi>))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
fix Q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
have "(\<^bold>\<forall>x. G x \<^bold>\<rightarrow> (\<E> G x)) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w)
[PROOF STEP]
using GodIsEssential
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w))\<rfloor>

goal (1 subgoal):
 1. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w)
[PROOF STEP]
by (rule allE) \<comment> \<open>follows from Axioms 11.11 and 11.3B\<close>
[PROOF STATE]
proof (state)
this:
\<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
hence "\<forall>x. G x w \<longrightarrow> \<E> G x w"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w)

goal (1 subgoal):
 1. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
hence "\<forall>x. G x w \<longrightarrow> (\<^bold>\<forall>Z. Z x \<^bold>\<rightarrow> \<^bold>\<box>(\<^bold>\<forall>\<^sup>Ez. G z \<^bold>\<rightarrow> Z z)) w"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<and> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w)

goal (1 subgoal):
 1. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w)

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
hence "\<forall>x. G x w \<longrightarrow> ((\<lambda>y. Q) x \<^bold>\<rightarrow> \<^bold>\<box>(\<^bold>\<forall>\<^sup>Ez. G z \<^bold>\<rightarrow> (\<lambda>y. Q) z)) w"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (\<forall>xa. (xa x \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> xa x v)) w)

goal (1 subgoal):
 1. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> Q v)) w
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> Q v)) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
hence "\<forall>x. G x w \<longrightarrow> (Q \<^bold>\<rightarrow> \<^bold>\<box>(\<^bold>\<forall>\<^sup>Ez. G z \<^bold>\<rightarrow> Q)) w"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> Q v)) w

goal (1 subgoal):
 1. \<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> Q v)) w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> Q v)) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
hence 1: "(\<exists>x. G x w) \<longrightarrow> ((Q \<^bold>\<rightarrow> \<^bold>\<box>(\<^bold>\<forall>\<^sup>Ez. G z \<^bold>\<rightarrow> Q)) w)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> Q v)) w

goal (1 subgoal):
 1. (\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> Q v)) w
[PROOF STEP]
by (rule useful)
[PROOF STATE]
proof (state)
this:
(\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> Q v)) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
have "\<exists>x. G x w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w
[PROOF STEP]
using GodExistenceIsValid
[PROOF STATE]
proof (prove)
using this:
\<lfloor>(\<lambda>w. \<exists>x. existsAt x w \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w))\<rfloor>

goal (1 subgoal):
 1. \<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
from 1 this
[PROOF STATE]
proof (chain)
picking this:
(\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> Q v)) w
\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w
[PROOF STEP]
have "(Q \<^bold>\<rightarrow> \<^bold>\<box>(\<^bold>\<forall>\<^sup>Ez. G z \<^bold>\<rightarrow> Q)) w"
[PROOF STATE]
proof (prove)
using this:
(\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w) \<longrightarrow> (Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> Q v)) w
\<exists>x. \<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) w

goal (1 subgoal):
 1. (Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> Q v)) w
[PROOF STEP]
by (rule mp)
[PROOF STATE]
proof (state)
this:
(Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> Q v)) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
hence "(Q \<^bold>\<rightarrow> \<^bold>\<box>((\<^bold>\<exists>\<^sup>Ez. G z) \<^bold>\<rightarrow> Q)) w"
[PROOF STATE]
proof (prove)
using this:
(Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> Q v)) w

goal (1 subgoal):
 1. (Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. (\<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<longrightarrow> Q v)) w
[PROOF STEP]
using useful
[PROOF STATE]
proof (prove)
using this:
(Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<forall>x. existsAt x v \<longrightarrow> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v) \<longrightarrow> Q v)) w
\<forall>x. ?\<phi> x \<longrightarrow> ?\<psi> \<Longrightarrow> (\<exists>x. ?\<phi> x) \<longrightarrow> ?\<psi>

goal (1 subgoal):
 1. (Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. (\<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<longrightarrow> Q v)) w
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. (\<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<longrightarrow> Q v)) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
hence "(Q \<^bold>\<rightarrow> (\<^bold>\<box>(\<^bold>\<exists>\<^sup>Ez. G z) \<^bold>\<rightarrow> \<^bold>\<box>Q)) w"
[PROOF STATE]
proof (prove)
using this:
(Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. (\<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<longrightarrow> Q v)) w

goal (1 subgoal):
 1. (Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<^bold>\<rightarrow> \<^bold>\<box>Q) w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<^bold>\<rightarrow> \<^bold>\<box>Q) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
hence "(Q \<^bold>\<rightarrow> \<^bold>\<box>Q) w"
[PROOF STATE]
proof (prove)
using this:
(Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<^bold>\<rightarrow> \<^bold>\<box>Q) w

goal (1 subgoal):
 1. (Q \<^bold>\<rightarrow> \<^bold>\<box>Q) w
[PROOF STEP]
using GodNecExists
[PROOF STATE]
proof (prove)
using this:
(Q \<^bold>\<rightarrow> \<^bold>\<box>(\<lambda>v. \<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)) \<^bold>\<rightarrow> \<^bold>\<box>Q) w
universal (\<lambda>w v. w r v \<longrightarrow> (\<exists>x. existsAt x v \<and> (\<forall>xa. (\<P> xa \<^bold>\<rightarrow> xa x) v)))

goal (1 subgoal):
 1. (Q \<^bold>\<rightarrow> \<^bold>\<box>Q) w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(Q \<^bold>\<rightarrow> \<^bold>\<box>Q) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?Q2 \<^bold>\<rightarrow> \<^bold>\<box>?Q2) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
hence "(\<^bold>\<forall>\<Phi>. \<Phi> \<^bold>\<rightarrow> \<^bold>\<box> \<Phi>) w"
[PROOF STATE]
proof (prove)
using this:
(?Q2 \<^bold>\<rightarrow> \<^bold>\<box>?Q2) w

goal (1 subgoal):
 1. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w
[PROOF STEP]
by (rule allI)
[PROOF STATE]
proof (state)
this:
\<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) ?w2

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) ?w2

goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>
[PROOF STEP]
by (rule allI)
[PROOF STATE]
proof (state)
this:
\<lfloor>(\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w)\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqExcD:
"eqExcD pap pap1 =
 (titlePaper pap = titlePaper pap1 \<and> abstractPaper pap = abstractPaper pap1 \<and>
  contentPaper pap = contentPaper pap1 \<and>
  reviewsPaper pap = reviewsPaper pap1 \<and> disPaper pap = disPaper pap1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcD pap pap1 = (titlePaper pap = titlePaper pap1 \<and> abstractPaper pap = abstractPaper pap1 \<and> contentPaper pap = contentPaper pap1 \<and> reviewsPaper pap = reviewsPaper pap1 \<and> disPaper pap = disPaper pap1)
[PROOF STEP]
by(cases pap, cases pap1, auto)


[STATEMENT]
lemma eqExcD_eq[simp,intro!]: "eqExcD pap pap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcD pap pap
[PROOF STEP]
by(cases pap) auto


[STATEMENT]
lemma eqExcD_sym:
assumes "eqExcD pap pap1"
shows "eqExcD pap1 pap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcD pap1 pap
[PROOF STEP]
apply(cases pap, cases pap1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x1a x2a x3a x4a x5a x6a. \<lbrakk>pap = Paper x1 x2 x3 x4 x5 x6; pap1 = Paper x1a x2a x3a x4a x5a x6a\<rbrakk> \<Longrightarrow> eqExcD pap1 pap
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqExcD pap pap1

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x1a x2a x3a x4a x5a x6a. \<lbrakk>pap = Paper x1 x2 x3 x4 x5 x6; pap1 = Paper x1a x2a x3a x4a x5a x6a\<rbrakk> \<Longrightarrow> eqExcD pap1 pap
[PROOF STEP]
by auto


[STATEMENT]
lemma eqExcD_trans:
assumes "eqExcD pap pap1" and "eqExcD pap1 pap2"
shows "eqExcD pap pap2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcD pap pap2
[PROOF STEP]
apply(cases pap, cases pap1, cases pap2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x1a x2a x3a x4a x5a x6a x1b x2b x3b x4b x5b x6b. \<lbrakk>pap = Paper x1 x2 x3 x4 x5 x6; pap1 = Paper x1a x2a x3a x4a x5a x6a; pap2 = Paper x1b x2b x3b x4b x5b x6b\<rbrakk> \<Longrightarrow> eqExcD pap pap2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqExcD pap pap1
eqExcD pap1 pap2

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x1a x2a x3a x4a x5a x6a x1b x2b x3b x4b x5b x6b. \<lbrakk>pap = Paper x1 x2 x3 x4 x5 x6; pap1 = Paper x1a x2a x3a x4a x5a x6a; pap2 = Paper x1b x2b x3b x4b x5b x6b\<rbrakk> \<Longrightarrow> eqExcD pap pap2
[PROOF STEP]
by auto


[STATEMENT]
lemma eeqExcPID_eeq[simp,intro!]: "eeqExcPID s s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eeqExcPID s s
[PROOF STEP]
unfolding eeqExcPID_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>pid. if pid = PID then eqExcD (s pid) (s pid) else s pid = s pid
[PROOF STEP]
by auto


[STATEMENT]
lemma eeqExcPID_sym:
assumes "eeqExcPID s s1" shows "eeqExcPID s1 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eeqExcPID s1 s
[PROOF STEP]
using assms eqExcD_sym
[PROOF STATE]
proof (prove)
using this:
eeqExcPID s s1
eqExcD ?pap ?pap1.0 \<Longrightarrow> eqExcD ?pap1.0 ?pap

goal (1 subgoal):
 1. eeqExcPID s1 s
[PROOF STEP]
unfolding eeqExcPID_def
[PROOF STATE]
proof (prove)
using this:
\<forall>pid. if pid = PID then eqExcD (s pid) (s1 pid) else s pid = s1 pid
eqExcD ?pap ?pap1.0 \<Longrightarrow> eqExcD ?pap1.0 ?pap

goal (1 subgoal):
 1. \<forall>pid. if pid = PID then eqExcD (s1 pid) (s pid) else s1 pid = s pid
[PROOF STEP]
by auto


[STATEMENT]
lemma eeqExcPID_trans:
assumes "eeqExcPID s s1" and "eeqExcPID s1 s2" shows "eeqExcPID s s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eeqExcPID s s2
[PROOF STEP]
using assms eqExcD_trans
[PROOF STATE]
proof (prove)
using this:
eeqExcPID s s1
eeqExcPID s1 s2
\<lbrakk>eqExcD ?pap ?pap1.0; eqExcD ?pap1.0 ?pap2.0\<rbrakk> \<Longrightarrow> eqExcD ?pap ?pap2.0

goal (1 subgoal):
 1. eeqExcPID s s2
[PROOF STEP]
unfolding eeqExcPID_def
[PROOF STATE]
proof (prove)
using this:
\<forall>pid. if pid = PID then eqExcD (s pid) (s1 pid) else s pid = s1 pid
\<forall>pid. if pid = PID then eqExcD (s1 pid) (s2 pid) else s1 pid = s2 pid
\<lbrakk>eqExcD ?pap ?pap1.0; eqExcD ?pap1.0 ?pap2.0\<rbrakk> \<Longrightarrow> eqExcD ?pap ?pap2.0

goal (1 subgoal):
 1. \<forall>pid. if pid = PID then eqExcD (s pid) (s2 pid) else s pid = s2 pid
[PROOF STEP]
by simp blast


[STATEMENT]
lemma eeqExcPID_imp:
"eeqExcPID paps paps1 \<Longrightarrow> eqExcD (paps PID) (paps1 PID)"
"\<lbrakk>eeqExcPID paps paps1; pid \<noteq> PID\<rbrakk> \<Longrightarrow> paps pid = paps1 pid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (eeqExcPID paps paps1 \<Longrightarrow> eqExcD (paps PID) (paps1 PID)) &&& (\<lbrakk>eeqExcPID paps paps1; pid \<noteq> PID\<rbrakk> \<Longrightarrow> paps pid = paps1 pid)
[PROOF STEP]
unfolding eeqExcPID_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>pid. if pid = PID then eqExcD (paps pid) (paps1 pid) else paps pid = paps1 pid \<Longrightarrow> eqExcD (paps PID) (paps1 PID)) &&& (\<lbrakk>\<forall>pid. if pid = PID then eqExcD (paps pid) (paps1 pid) else paps pid = paps1 pid; pid \<noteq> PID\<rbrakk> \<Longrightarrow> paps pid = paps1 pid)
[PROOF STEP]
by auto


[STATEMENT]
lemma eeqExcPID_cong:
assumes "eeqExcPID paps paps1"
and "pid = PID \<Longrightarrow> eqExcD uu uu1"
and "pid \<noteq> PID \<Longrightarrow> uu = uu1"
shows "eeqExcPID (paps (pid := uu)) (paps1(pid := uu1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eeqExcPID (paps(pid := uu)) (paps1(pid := uu1))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eeqExcPID paps paps1
pid = PID \<Longrightarrow> eqExcD uu uu1
pid \<noteq> PID \<Longrightarrow> uu = uu1

goal (1 subgoal):
 1. eeqExcPID (paps(pid := uu)) (paps1(pid := uu1))
[PROOF STEP]
unfolding eeqExcPID_def
[PROOF STATE]
proof (prove)
using this:
\<forall>pid. if pid = PID then eqExcD (paps pid) (paps1 pid) else paps pid = paps1 pid
pid = PID \<Longrightarrow> eqExcD uu uu1
pid \<noteq> PID \<Longrightarrow> uu = uu1

goal (1 subgoal):
 1. \<forall>pida. if pida = PID then eqExcD ((paps(pid := uu)) pida) ((paps1(pid := uu1)) pida) else (paps(pid := uu)) pida = (paps1(pid := uu1)) pida
[PROOF STEP]
by auto


[STATEMENT]
lemma eeqExcPID_RDD:
"eeqExcPID paps paps1 \<Longrightarrow>
 titlePaper (paps PID) = titlePaper (paps1 PID) \<and>
 abstractPaper (paps PID) = abstractPaper (paps1 PID) \<and>
 contentPaper (paps PID) = contentPaper (paps1 PID) \<and>
 reviewsPaper (paps PID) = reviewsPaper (paps1 PID) \<and>
 disPaper (paps PID) = disPaper (paps1 PID)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eeqExcPID paps paps1 \<Longrightarrow> titlePaper (paps PID) = titlePaper (paps1 PID) \<and> abstractPaper (paps PID) = abstractPaper (paps1 PID) \<and> contentPaper (paps PID) = contentPaper (paps1 PID) \<and> reviewsPaper (paps PID) = reviewsPaper (paps1 PID) \<and> disPaper (paps PID) = disPaper (paps1 PID)
[PROOF STEP]
using eeqExcPID_def
[PROOF STATE]
proof (prove)
using this:
eeqExcPID ?paps ?paps1.0 \<equiv> \<forall>pid. if pid = PID then eqExcD (?paps pid) (?paps1.0 pid) else ?paps pid = ?paps1.0 pid

goal (1 subgoal):
 1. eeqExcPID paps paps1 \<Longrightarrow> titlePaper (paps PID) = titlePaper (paps1 PID) \<and> abstractPaper (paps PID) = abstractPaper (paps1 PID) \<and> contentPaper (paps PID) = contentPaper (paps1 PID) \<and> reviewsPaper (paps PID) = reviewsPaper (paps1 PID) \<and> disPaper (paps PID) = disPaper (paps1 PID)
[PROOF STEP]
unfolding eqExcD
[PROOF STATE]
proof (prove)
using this:
eeqExcPID ?paps ?paps1.0 \<equiv> \<forall>pid. if pid = PID then titlePaper (?paps pid) = titlePaper (?paps1.0 pid) \<and> abstractPaper (?paps pid) = abstractPaper (?paps1.0 pid) \<and> contentPaper (?paps pid) = contentPaper (?paps1.0 pid) \<and> reviewsPaper (?paps pid) = reviewsPaper (?paps1.0 pid) \<and> disPaper (?paps pid) = disPaper (?paps1.0 pid) else ?paps pid = ?paps1.0 pid

goal (1 subgoal):
 1. eeqExcPID paps paps1 \<Longrightarrow> titlePaper (paps PID) = titlePaper (paps1 PID) \<and> abstractPaper (paps PID) = abstractPaper (paps1 PID) \<and> contentPaper (paps PID) = contentPaper (paps1 PID) \<and> reviewsPaper (paps PID) = reviewsPaper (paps1 PID) \<and> disPaper (paps PID) = disPaper (paps1 PID)
[PROOF STEP]
by auto


[STATEMENT]
lemma eqExcPID_eq[simp,intro!]: "eqExcPID s s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID s s
[PROOF STEP]
unfolding eqExcPID_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. confIDs s = confIDs s \<and> conf s = conf s \<and> userIDs s = userIDs s \<and> pass s = pass s \<and> user s = user s \<and> roles s = roles s \<and> paperIDs s = paperIDs s \<and> eeqExcPID (paper s) (paper s) \<and> pref s = pref s \<and> voronkov s = voronkov s \<and> news s = news s \<and> phase s = phase s
[PROOF STEP]
by auto


[STATEMENT]
lemma eqExcPID_sym:
assumes "eqExcPID s s1" shows "eqExcPID s1 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID s1 s
[PROOF STEP]
using assms eeqExcPID_sym
[PROOF STATE]
proof (prove)
using this:
eqExcPID s s1
eeqExcPID ?s ?s1.0 \<Longrightarrow> eeqExcPID ?s1.0 ?s

goal (1 subgoal):
 1. eqExcPID s1 s
[PROOF STEP]
unfolding eqExcPID_def
[PROOF STATE]
proof (prove)
using this:
confIDs s = confIDs s1 \<and> conf s = conf s1 \<and> userIDs s = userIDs s1 \<and> pass s = pass s1 \<and> user s = user s1 \<and> roles s = roles s1 \<and> paperIDs s = paperIDs s1 \<and> eeqExcPID (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1
eeqExcPID ?s ?s1.0 \<Longrightarrow> eeqExcPID ?s1.0 ?s

goal (1 subgoal):
 1. confIDs s1 = confIDs s \<and> conf s1 = conf s \<and> userIDs s1 = userIDs s \<and> pass s1 = pass s \<and> user s1 = user s \<and> roles s1 = roles s \<and> paperIDs s1 = paperIDs s \<and> eeqExcPID (paper s1) (paper s) \<and> pref s1 = pref s \<and> voronkov s1 = voronkov s \<and> news s1 = news s \<and> phase s1 = phase s
[PROOF STEP]
by auto


[STATEMENT]
lemma eqExcPID_trans:
assumes "eqExcPID s s1" and "eqExcPID s1 s2" shows "eqExcPID s s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID s s2
[PROOF STEP]
using assms eeqExcPID_trans
[PROOF STATE]
proof (prove)
using this:
eqExcPID s s1
eqExcPID s1 s2
\<lbrakk>eeqExcPID ?s ?s1.0; eeqExcPID ?s1.0 ?s2.0\<rbrakk> \<Longrightarrow> eeqExcPID ?s ?s2.0

goal (1 subgoal):
 1. eqExcPID s s2
[PROOF STEP]
unfolding eqExcPID_def
[PROOF STATE]
proof (prove)
using this:
confIDs s = confIDs s1 \<and> conf s = conf s1 \<and> userIDs s = userIDs s1 \<and> pass s = pass s1 \<and> user s = user s1 \<and> roles s = roles s1 \<and> paperIDs s = paperIDs s1 \<and> eeqExcPID (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1
confIDs s1 = confIDs s2 \<and> conf s1 = conf s2 \<and> userIDs s1 = userIDs s2 \<and> pass s1 = pass s2 \<and> user s1 = user s2 \<and> roles s1 = roles s2 \<and> paperIDs s1 = paperIDs s2 \<and> eeqExcPID (paper s1) (paper s2) \<and> pref s1 = pref s2 \<and> voronkov s1 = voronkov s2 \<and> news s1 = news s2 \<and> phase s1 = phase s2
\<lbrakk>eeqExcPID ?s ?s1.0; eeqExcPID ?s1.0 ?s2.0\<rbrakk> \<Longrightarrow> eeqExcPID ?s ?s2.0

goal (1 subgoal):
 1. confIDs s = confIDs s2 \<and> conf s = conf s2 \<and> userIDs s = userIDs s2 \<and> pass s = pass s2 \<and> user s = user s2 \<and> roles s = roles s2 \<and> paperIDs s = paperIDs s2 \<and> eeqExcPID (paper s) (paper s2) \<and> pref s = pref s2 \<and> voronkov s = voronkov s2 \<and> news s = news s2 \<and> phase s = phase s2
[PROOF STEP]
by auto


[STATEMENT]
lemma eqExcPID_imp:
"eqExcPID s s1 \<Longrightarrow>
 confIDs s = confIDs s1 \<and> conf s = conf s1 \<and>
 userIDs s = userIDs s1 \<and> pass s = pass s1 \<and> user s = user s1 \<and> roles s = roles s1 \<and>
 paperIDs s = paperIDs s1
 \<and>
 eeqExcPID (paper s) (paper s1)
 \<and>
 pref s = pref s1 \<and>
 voronkov s = voronkov s1 \<and>
 news s = news s1 \<and> phase s = phase s1 \<and>

 getAllPaperIDs s = getAllPaperIDs s1 \<and>
 isRev s cid uid pid = isRev s1 cid uid pid \<and>
 getReviewIndex s cid uid pid = getReviewIndex s1 cid uid pid \<and>
 getRevRole s cid uid pid = getRevRole s1 cid uid pid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID s s1 \<Longrightarrow> confIDs s = confIDs s1 \<and> conf s = conf s1 \<and> userIDs s = userIDs s1 \<and> pass s = pass s1 \<and> user s = user s1 \<and> roles s = roles s1 \<and> paperIDs s = paperIDs s1 \<and> eeqExcPID (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1 \<and> getAllPaperIDs s = getAllPaperIDs s1 \<and> isRev s cid uid pid = isRev s1 cid uid pid \<and> getReviewIndex s cid uid pid = getReviewIndex s1 cid uid pid \<and> getRevRole s cid uid pid = getRevRole s1 cid uid pid
[PROOF STEP]
unfolding eqExcPID_def getAllPaperIDs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. confIDs s = confIDs s1 \<and> conf s = conf s1 \<and> userIDs s = userIDs s1 \<and> pass s = pass s1 \<and> user s = user s1 \<and> roles s = roles s1 \<and> paperIDs s = paperIDs s1 \<and> eeqExcPID (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1 \<Longrightarrow> confIDs s = confIDs s1 \<and> conf s = conf s1 \<and> userIDs s = userIDs s1 \<and> pass s = pass s1 \<and> user s = user s1 \<and> roles s = roles s1 \<and> paperIDs s = paperIDs s1 \<and> eeqExcPID (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1 \<and> cmap (paperIDs s) (confIDs s) = cmap (paperIDs s1) (confIDs s1) \<and> isRev s cid uid pid = isRev s1 cid uid pid \<and> getReviewIndex s cid uid pid = getReviewIndex s1 cid uid pid \<and> getRevRole s cid uid pid = getRevRole s1 cid uid pid
[PROOF STEP]
unfolding isRev_def getReviewIndex_def getRevRole_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. confIDs s = confIDs s1 \<and> conf s = conf s1 \<and> userIDs s = userIDs s1 \<and> pass s = pass s1 \<and> user s = user s1 \<and> roles s = roles s1 \<and> paperIDs s = paperIDs s1 \<and> eeqExcPID (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1 \<Longrightarrow> confIDs s = confIDs s1 \<and> conf s = conf s1 \<and> userIDs s = userIDs s1 \<and> pass s = pass s1 \<and> user s = user s1 \<and> roles s = roles s1 \<and> paperIDs s = paperIDs s1 \<and> eeqExcPID (paper s) (paper s1) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1 \<and> cmap (paperIDs s) (confIDs s) = cmap (paperIDs s1) (confIDs s1) \<and> list_ex (isRevRoleFor pid) (roles s cid uid) = list_ex (isRevRoleFor pid) (roles s1 cid uid) \<and> (case find (isRevRoleFor pid) (roles s cid uid) of Some (Rev papID' n) \<Rightarrow> n) = (case find (isRevRoleFor pid) (roles s1 cid uid) of Some (Rev papID' n) \<Rightarrow> n) \<and> find (isRevRoleFor pid) (roles s cid uid) = find (isRevRoleFor pid) (roles s1 cid uid)
[PROOF STEP]
by auto


[STATEMENT]
lemma eqExcPID_imp1:
"eqExcPID s s1 \<Longrightarrow> eqExcD (paper s pid) (paper s1 pid)"
"eqExcPID s s1 \<Longrightarrow> pid \<noteq> PID \<or> PID \<noteq> pid \<Longrightarrow>
    paper s pid = paper s1 pid \<and>
    getNthReview s pid n = getNthReview s1 pid n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (eqExcPID s s1 \<Longrightarrow> eqExcD (paper s pid) (paper s1 pid)) &&& (\<lbrakk>eqExcPID s s1; pid \<noteq> PID \<or> PID \<noteq> pid\<rbrakk> \<Longrightarrow> paper s pid = paper s1 pid \<and> getNthReview s pid n = getNthReview s1 pid n)
[PROOF STEP]
unfolding eqExcPID_def getNthReview_def eeqExcPID_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (confIDs s = confIDs s1 \<and> conf s = conf s1 \<and> userIDs s = userIDs s1 \<and> pass s = pass s1 \<and> user s = user s1 \<and> roles s = roles s1 \<and> paperIDs s = paperIDs s1 \<and> (\<forall>pid. if pid = PID then eqExcD (paper s pid) (paper s1 pid) else paper s pid = paper s1 pid) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1 \<Longrightarrow> eqExcD (paper s pid) (paper s1 pid)) &&& (\<lbrakk>confIDs s = confIDs s1 \<and> conf s = conf s1 \<and> userIDs s = userIDs s1 \<and> pass s = pass s1 \<and> user s = user s1 \<and> roles s = roles s1 \<and> paperIDs s = paperIDs s1 \<and> (\<forall>pid. if pid = PID then eqExcD (paper s pid) (paper s1 pid) else paper s pid = paper s1 pid) \<and> pref s = pref s1 \<and> voronkov s = voronkov s1 \<and> news s = news s1 \<and> phase s = phase s1; pid \<noteq> PID \<or> PID \<noteq> pid\<rbrakk> \<Longrightarrow> paper s pid = paper s1 pid \<and> reviewsPaper (paper s pid) ! n = reviewsPaper (paper s1 pid) ! n)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confIDs s = confIDs s1; conf s = conf s1; userIDs s = userIDs s1; pass s = pass s1; user s = user s1; roles s = roles s1; paperIDs s = paperIDs s1; \<forall>pid. (pid = PID \<longrightarrow> eqExcD (paper s PID) (paper s1 PID)) \<and> (pid = PID \<or> paper s pid = paper s1 pid); pref s = pref s1; voronkov s = voronkov s1; news s = news s1; phase s = phase s1\<rbrakk> \<Longrightarrow> eqExcD (paper s pid) (paper s1 pid)
[PROOF STEP]
by (metis eqExcD_eq)