[STATEMENT]
theorem stutter_invariant_next_free:
  assumes phi: "stutter_invariant \<phi>"
  obtains \<psi> where "next_free \<psi>" "atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>"
                  "\<forall>\<sigma>. (\<sigma> \<Turnstile>\<^sub>p \<psi>) = (\<sigma> \<Turnstile>\<^sub>p \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "atoms_pltl \<phi> \<subseteq> atoms_pltl \<phi>" "finite (atoms_pltl \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atoms_pltl \<phi> \<subseteq> atoms_pltl \<phi> &&& finite (atoms_pltl \<phi>)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
atoms_pltl \<phi> \<subseteq> atoms_pltl \<phi>
finite (atoms_pltl \<phi>)

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
atoms_pltl \<phi> \<subseteq> atoms_pltl \<phi>
finite (atoms_pltl \<phi>)
[PROOF STEP]
obtain \<psi> where
    psi: "next_free \<psi>" "atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>" and
    equiv: "\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence (atoms_pltl \<phi>) \<sigma> \<longrightarrow> (\<sigma> \<Turnstile>\<^sub>p \<psi>) = (\<sigma> \<Turnstile>\<^sub>p \<phi>)"
[PROOF STATE]
proof (prove)
using this:
atoms_pltl \<phi> \<subseteq> atoms_pltl \<phi>
finite (atoms_pltl \<phi>)

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence (atoms_pltl \<phi>) \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast dest: ex_next_free_stutter_free_canonical)
[PROOF STATE]
proof (state)
this:
next_free \<psi>
atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>
\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence (atoms_pltl \<phi>) \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>next_free \<psi>\<close>
[PROOF STATE]
proof (chain)
picking this:
next_free \<psi>
[PROOF STEP]
have sinv: "stutter_invariant \<psi>"
[PROOF STATE]
proof (prove)
using this:
next_free \<psi>

goal (1 subgoal):
 1. stutter_invariant \<psi>
[PROOF STEP]
by (rule next_free_stutter_invariant)
[PROOF STATE]
proof (state)
this:
stutter_invariant \<psi>

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
stutter_invariant \<psi>

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
fix \<sigma>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain \<tau> where 1: "\<tau> \<simeq> atoms_pltl \<phi> \<simeq> \<sigma>" and 2: "canonical_sequence (atoms_pltl \<phi>) \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<tau>. \<lbrakk>\<tau> \<simeq>atoms_pltl \<phi>\<simeq> \<sigma>; canonical_sequence (atoms_pltl \<phi>) \<tau>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule canonical_exists)
[PROOF STATE]
proof (state)
this:
\<tau> \<simeq>atoms_pltl \<phi>\<simeq> \<sigma>
canonical_sequence (atoms_pltl \<phi>) \<tau>

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from 1 \<open>atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<tau> \<simeq>atoms_pltl \<phi>\<simeq> \<sigma>
atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>
[PROOF STEP]
have 3: "\<tau> \<simeq> atoms_pltl \<psi> \<simeq> \<sigma>"
[PROOF STATE]
proof (prove)
using this:
\<tau> \<simeq>atoms_pltl \<phi>\<simeq> \<sigma>
atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>

goal (1 subgoal):
 1. \<tau> \<simeq>atoms_pltl \<psi>\<simeq> \<sigma>
[PROOF STEP]
by (rule seq_sim_mono)
[PROOF STATE]
proof (state)
this:
\<tau> \<simeq>atoms_pltl \<psi>\<simeq> \<sigma>

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
\<tau> \<simeq>atoms_pltl \<phi>\<simeq> \<sigma>
[PROOF STEP]
have "(\<sigma> \<Turnstile>\<^sub>p \<phi>) = (\<tau> \<Turnstile>\<^sub>p \<phi>)"
[PROOF STATE]
proof (prove)
using this:
\<tau> \<simeq>atoms_pltl \<phi>\<simeq> \<sigma>

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>
[PROOF STEP]
by (simp add: pltl_seq_sim)
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p \<phi> = \<tau> \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from phi stutter_reduced_equivalent
[PROOF STATE]
proof (chain)
picking this:
stutter_invariant \<phi>
\<natural>?\<sigma> \<approx> ?\<sigma>
[PROOF STEP]
have "... = (\<natural>\<tau> \<Turnstile>\<^sub>p \<phi>)"
[PROOF STATE]
proof (prove)
using this:
stutter_invariant \<phi>
\<natural>?\<sigma> \<approx> ?\<sigma>

goal (1 subgoal):
 1. \<tau> \<Turnstile>\<^sub>p \<phi> = \<natural>\<tau> \<Turnstile>\<^sub>p \<phi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<tau> \<Turnstile>\<^sub>p \<phi> = \<natural>\<tau> \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<tau> \<Turnstile>\<^sub>p \<phi> = \<natural>\<tau> \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from 2[THEN canonical_reduced] equiv stutter_reduced_stutter_free
[PROOF STATE]
proof (chain)
picking this:
canonical_sequence (atoms_pltl \<phi>) (\<natural>\<tau>)
\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence (atoms_pltl \<phi>) \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>
stutter_free (\<natural>?\<sigma>)
[PROOF STEP]
have "... = (\<natural>\<tau> \<Turnstile>\<^sub>p \<psi>)"
[PROOF STATE]
proof (prove)
using this:
canonical_sequence (atoms_pltl \<phi>) (\<natural>\<tau>)
\<forall>\<sigma>. stutter_free \<sigma> \<and> canonical_sequence (atoms_pltl \<phi>) \<sigma> \<longrightarrow> \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>
stutter_free (\<natural>?\<sigma>)

goal (1 subgoal):
 1. \<natural>\<tau> \<Turnstile>\<^sub>p \<phi> = \<natural>\<tau> \<Turnstile>\<^sub>p \<psi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<natural>\<tau> \<Turnstile>\<^sub>p \<phi> = \<natural>\<tau> \<Turnstile>\<^sub>p \<psi>

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<natural>\<tau> \<Turnstile>\<^sub>p \<phi> = \<natural>\<tau> \<Turnstile>\<^sub>p \<psi>

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from sinv stutter_reduced_equivalent
[PROOF STATE]
proof (chain)
picking this:
stutter_invariant \<psi>
\<natural>?\<sigma> \<approx> ?\<sigma>
[PROOF STEP]
have "... = (\<tau> \<Turnstile>\<^sub>p \<psi>)"
[PROOF STATE]
proof (prove)
using this:
stutter_invariant \<psi>
\<natural>?\<sigma> \<approx> ?\<sigma>

goal (1 subgoal):
 1. \<natural>\<tau> \<Turnstile>\<^sub>p \<psi> = \<tau> \<Turnstile>\<^sub>p \<psi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<natural>\<tau> \<Turnstile>\<^sub>p \<psi> = \<tau> \<Turnstile>\<^sub>p \<psi>

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<natural>\<tau> \<Turnstile>\<^sub>p \<psi> = \<tau> \<Turnstile>\<^sub>p \<psi>

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from 3
[PROOF STATE]
proof (chain)
picking this:
\<tau> \<simeq>atoms_pltl \<psi>\<simeq> \<sigma>
[PROOF STEP]
have "... = (\<sigma> \<Turnstile>\<^sub>p \<psi>)"
[PROOF STATE]
proof (prove)
using this:
\<tau> \<simeq>atoms_pltl \<psi>\<simeq> \<sigma>

goal (1 subgoal):
 1. \<tau> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<psi>
[PROOF STEP]
by (simp add: pltl_seq_sim)
[PROOF STATE]
proof (state)
this:
\<tau> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<psi>

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<Turnstile>\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p \<psi>
[PROOF STEP]
have "(\<sigma> \<Turnstile>\<^sub>p \<psi>) = (\<sigma> \<Turnstile>\<^sub>p \<phi>)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<Turnstile>\<^sub>p \<phi> = \<sigma> \<Turnstile>\<^sub>p \<psi>

goal (1 subgoal):
 1. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>
[PROOF STEP]
by (rule sym)
[PROOF STATE]
proof (state)
this:
\<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?\<sigma>2 \<Turnstile>\<^sub>p \<psi> = ?\<sigma>2 \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>next_free \<psi>; atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with psi that
[PROOF STATE]
proof (chain)
picking this:
next_free \<psi>
atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>
\<lbrakk>next_free ?\<psi>; atoms_pltl ?\<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p ?\<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis
?\<sigma>2 \<Turnstile>\<^sub>p \<psi> = ?\<sigma>2 \<Turnstile>\<^sub>p \<phi>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
next_free \<psi>
atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi>
\<lbrakk>next_free ?\<psi>; atoms_pltl ?\<psi> \<subseteq> atoms_pltl \<phi>; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p ?\<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> thesis
?\<sigma>2 \<Turnstile>\<^sub>p \<psi> = ?\<sigma>2 \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem pltl_stutter_invariant:
  "stutter_invariant \<phi> \<longleftrightarrow>
   (\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> \<longleftrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stutter_invariant \<phi> = (\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stutter_invariant \<phi> = (\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stutter_invariant \<phi> = (\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>))
[PROOF STEP]
assume "stutter_invariant \<phi>"
[PROOF STATE]
proof (state)
this:
stutter_invariant \<phi>

goal (1 subgoal):
 1. stutter_invariant \<phi> = (\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>))
[PROOF STEP]
hence "\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> \<longleftrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>)"
[PROOF STATE]
proof (prove)
using this:
stutter_invariant \<phi>

goal (1 subgoal):
 1. \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)
[PROOF STEP]
by (rule stutter_invariant_next_free) blast
[PROOF STATE]
proof (state)
this:
\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)

goal (1 subgoal):
 1. stutter_invariant \<phi> = (\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
stutter_invariant \<phi> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)

goal (1 subgoal):
 1. stutter_invariant \<phi> = (\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stutter_invariant \<phi> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)

goal (1 subgoal):
 1. stutter_invariant \<phi> = (\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
stutter_invariant \<phi> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)

goal (1 subgoal):
 1. stutter_invariant \<phi> = (\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>))
[PROOF STEP]
fix \<psi>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stutter_invariant \<phi> = (\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>))
[PROOF STEP]
assume 1: "next_free \<psi>" and 2: "\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> \<longleftrightarrow> \<sigma> \<Turnstile>\<^sub>p \<phi>"
[PROOF STATE]
proof (state)
this:
next_free \<psi>
\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>

goal (1 subgoal):
 1. stutter_invariant \<phi> = (\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>))
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
next_free \<psi>
[PROOF STEP]
have "stutter_invariant \<psi>"
[PROOF STATE]
proof (prove)
using this:
next_free \<psi>

goal (1 subgoal):
 1. stutter_invariant \<psi>
[PROOF STEP]
by (rule next_free_stutter_invariant)
[PROOF STATE]
proof (state)
this:
stutter_invariant \<psi>

goal (1 subgoal):
 1. stutter_invariant \<phi> = (\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>))
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>
stutter_invariant \<psi>
[PROOF STEP]
have "stutter_invariant \<phi>"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>
stutter_invariant \<psi>

goal (1 subgoal):
 1. stutter_invariant \<phi>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
stutter_invariant \<phi>

goal (1 subgoal):
 1. stutter_invariant \<phi> = (\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>next_free ?\<psi>2; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p ?\<psi>2 = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> stutter_invariant \<phi>

goal (1 subgoal):
 1. stutter_invariant \<phi> = (\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
stutter_invariant \<phi> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)
\<lbrakk>next_free ?\<psi>2; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p ?\<psi>2 = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> stutter_invariant \<phi>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
stutter_invariant \<phi> \<Longrightarrow> \<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>)
\<lbrakk>next_free ?\<psi>2; \<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p ?\<psi>2 = \<sigma> \<Turnstile>\<^sub>p \<phi>\<rbrakk> \<Longrightarrow> stutter_invariant \<phi>

goal (1 subgoal):
 1. stutter_invariant \<phi> = (\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
stutter_invariant \<phi> = (\<exists>\<psi>. next_free \<psi> \<and> atoms_pltl \<psi> \<subseteq> atoms_pltl \<phi> \<and> (\<forall>\<sigma>. \<sigma> \<Turnstile>\<^sub>p \<psi> = \<sigma> \<Turnstile>\<^sub>p \<phi>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ltlc_next_free_iff[simp]: "next_free (ltlc_to_pltl \<phi>) \<longleftrightarrow> ltlc_next_free \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_free (ltlc_to_pltl \<phi>) = ltlc_next_free \<phi>
[PROOF STEP]
by (induction \<phi>) auto


[STATEMENT]
theorem ltlc_next_free_stutter_invariant:
  assumes next_free: "ltlc_next_free \<phi>"
  assumes eq: "r \<approx> r'"
  shows "r \<Turnstile>\<^sub>c \<phi> \<longleftrightarrow> r' \<Turnstile>\<^sub>c \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<Turnstile>\<^sub>c \<phi> = r' \<Turnstile>\<^sub>c \<phi>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<Turnstile>\<^sub>c \<phi> = r' \<Turnstile>\<^sub>c \<phi>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<Turnstile>\<^sub>c \<phi> = r' \<Turnstile>\<^sub>c \<phi>
[PROOF STEP]
fix r r'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<Turnstile>\<^sub>c \<phi> = r' \<Turnstile>\<^sub>c \<phi>
[PROOF STEP]
assume eq: "r \<approx> r'" and holds: "r \<Turnstile>\<^sub>c \<phi>"
[PROOF STATE]
proof (state)
this:
r \<approx> r'
r \<Turnstile>\<^sub>c \<phi>

goal (1 subgoal):
 1. r \<Turnstile>\<^sub>c \<phi> = r' \<Turnstile>\<^sub>c \<phi>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<approx> r'
r \<Turnstile>\<^sub>c \<phi>
[PROOF STEP]
have "r \<Turnstile>\<^sub>p (ltlc_to_pltl \<phi>)"
[PROOF STATE]
proof (prove)
using this:
r \<approx> r'
r \<Turnstile>\<^sub>c \<phi>

goal (1 subgoal):
 1. r \<Turnstile>\<^sub>p ltlc_to_pltl \<phi>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r \<Turnstile>\<^sub>p ltlc_to_pltl \<phi>

goal (1 subgoal):
 1. r \<Turnstile>\<^sub>c \<phi> = r' \<Turnstile>\<^sub>c \<phi>
[PROOF STEP]
from next_free_stutter_invariant[of "ltlc_to_pltl \<phi>"] next_free
[PROOF STATE]
proof (chain)
picking this:
next_free (ltlc_to_pltl \<phi>) \<Longrightarrow> stutter_invariant (ltlc_to_pltl \<phi>)
ltlc_next_free \<phi>
[PROOF STEP]
have "PLTL.stutter_invariant (ltlc_to_pltl \<phi>)"
[PROOF STATE]
proof (prove)
using this:
next_free (ltlc_to_pltl \<phi>) \<Longrightarrow> stutter_invariant (ltlc_to_pltl \<phi>)
ltlc_next_free \<phi>

goal (1 subgoal):
 1. stutter_invariant (ltlc_to_pltl \<phi>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stutter_invariant (ltlc_to_pltl \<phi>)

goal (1 subgoal):
 1. r \<Turnstile>\<^sub>c \<phi> = r' \<Turnstile>\<^sub>c \<phi>
[PROOF STEP]
from stutter_invariantD[OF this eq] holds
[PROOF STATE]
proof (chain)
picking this:
r \<Turnstile>\<^sub>p ltlc_to_pltl \<phi> = r' \<Turnstile>\<^sub>p ltlc_to_pltl \<phi>
r \<Turnstile>\<^sub>c \<phi>
[PROOF STEP]
have "r' \<Turnstile>\<^sub>c \<phi>"
[PROOF STATE]
proof (prove)
using this:
r \<Turnstile>\<^sub>p ltlc_to_pltl \<phi> = r' \<Turnstile>\<^sub>p ltlc_to_pltl \<phi>
r \<Turnstile>\<^sub>c \<phi>

goal (1 subgoal):
 1. r' \<Turnstile>\<^sub>c \<phi>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r' \<Turnstile>\<^sub>c \<phi>

goal (1 subgoal):
 1. r \<Turnstile>\<^sub>c \<phi> = r' \<Turnstile>\<^sub>c \<phi>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?ra2 \<approx> ?r'a2; ?ra2 \<Turnstile>\<^sub>c \<phi>\<rbrakk> \<Longrightarrow> ?r'a2 \<Turnstile>\<^sub>c \<phi>

goal (1 subgoal):
 1. r \<Turnstile>\<^sub>c \<phi> = r' \<Turnstile>\<^sub>c \<phi>
[PROOF STEP]
note aux=this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?ra2 \<approx> ?r'a2; ?ra2 \<Turnstile>\<^sub>c \<phi>\<rbrakk> \<Longrightarrow> ?r'a2 \<Turnstile>\<^sub>c \<phi>

goal (1 subgoal):
 1. r \<Turnstile>\<^sub>c \<phi> = r' \<Turnstile>\<^sub>c \<phi>
[PROOF STEP]
from aux[of r r'] aux[of r' r] eq stutter_equiv_sym[OF eq]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>r \<approx> r'; r \<Turnstile>\<^sub>c \<phi>\<rbrakk> \<Longrightarrow> r' \<Turnstile>\<^sub>c \<phi>
\<lbrakk>r' \<approx> r; r' \<Turnstile>\<^sub>c \<phi>\<rbrakk> \<Longrightarrow> r \<Turnstile>\<^sub>c \<phi>
r \<approx> r'
r' \<approx> r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>r \<approx> r'; r \<Turnstile>\<^sub>c \<phi>\<rbrakk> \<Longrightarrow> r' \<Turnstile>\<^sub>c \<phi>
\<lbrakk>r' \<approx> r; r' \<Turnstile>\<^sub>c \<phi>\<rbrakk> \<Longrightarrow> r \<Turnstile>\<^sub>c \<phi>
r \<approx> r'
r' \<approx> r

goal (1 subgoal):
 1. r \<Turnstile>\<^sub>c \<phi> = r' \<Turnstile>\<^sub>c \<phi>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r \<Turnstile>\<^sub>c \<phi> = r' \<Turnstile>\<^sub>c \<phi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ntsmcf_tdghm_components:
  shows [slicing_simps]: "ntsmcf_tdghm \<NN>\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>"
    and [slicing_commute]: "ntsmcf_tdghm \<NN>\<lparr>NTDom\<rparr> = smcf_dghm (\<NN>\<lparr>NTDom\<rparr>)"
    and [slicing_commute]: "ntsmcf_tdghm \<NN>\<lparr>NTCod\<rparr> = smcf_dghm (\<NN>\<lparr>NTCod\<rparr>)"
    and [slicing_commute]: "ntsmcf_tdghm \<NN>\<lparr>NTDGDom\<rparr> = smc_dg (\<NN>\<lparr>NTDGDom\<rparr>)"
    and [slicing_commute]: "ntsmcf_tdghm \<NN>\<lparr>NTDGCod\<rparr> = smc_dg (\<NN>\<lparr>NTDGCod\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ntsmcf_tdghm \<NN>\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr> &&& ntsmcf_tdghm \<NN>\<lparr>NTDom\<rparr> = smcf_dghm (\<NN>\<lparr>NTDom\<rparr>)) &&& ntsmcf_tdghm \<NN>\<lparr>NTCod\<rparr> = smcf_dghm (\<NN>\<lparr>NTCod\<rparr>) &&& ntsmcf_tdghm \<NN>\<lparr>NTDGDom\<rparr> = smc_dg (\<NN>\<lparr>NTDGDom\<rparr>) &&& ntsmcf_tdghm \<NN>\<lparr>NTDGCod\<rparr> = smc_dg (\<NN>\<lparr>NTDGCod\<rparr>)
[PROOF STEP]
unfolding ntsmcf_tdghm_def nt_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, smcf_dghm (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), smcf_dghm (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), smc_dg (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), smc_dg (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = \<NN>\<lparr>[]\<^sub>\<circ>\<rparr> &&& [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, smcf_dghm (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), smcf_dghm (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), smc_dg (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), smc_dg (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = smcf_dghm (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>)) &&& [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, smcf_dghm (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), smcf_dghm (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), smc_dg (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), smc_dg (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = smcf_dghm (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>) &&& [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, smcf_dghm (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), smcf_dghm (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), smc_dg (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), smc_dg (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = smc_dg (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>) &&& [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, smcf_dghm (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), smcf_dghm (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), smc_dg (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), smc_dg (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr> = smc_dg (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)
[PROOF STEP]
by (auto simp: nat_omega_simps)


[STATEMENT]
lemma (in is_ntsmcf) ntsmcf_is_tdghm':
  assumes "\<FF>' = smcf_dghm \<FF>"
    and "\<GG>' = smcf_dghm \<GG>"
    and "\<AA>' = smc_dg \<AA>"
    and "\<BB>' = smc_dg \<BB>"
  shows "ntsmcf_tdghm \<NN> : \<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntsmcf_tdghm \<NN> : \<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
unfolding assms(1-4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntsmcf_tdghm \<NN> : smcf_dghm \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm \<GG> : smc_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<BB>
[PROOF STEP]
by (rule ntsmcf_is_tdghm)


[STATEMENT]
lemma (in is_ntsmcf) is_ntsmcf_axioms'[smc_cs_intros]:
  assumes "\<alpha>' = \<alpha>" and "\<AA>' = \<AA>" and "\<BB>' = \<BB>" and "\<FF>' = \<FF>" and "\<GG>' = \<GG>"
  shows "\<NN> : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>'\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>'\<^esub> \<BB>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule is_ntsmcf_axioms)


[STATEMENT]
lemma is_ntsmcfI':
  assumes "\<Z> \<alpha>"
    and "vfsequence \<NN>"
    and "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "vcard \<NN> = 5\<^sub>\<nat>"
    and "\<NN>\<lparr>NTDom\<rparr> = \<FF>"
    and "\<NN>\<lparr>NTCod\<rparr> = \<GG>"
    and "\<NN>\<lparr>NTDGDom\<rparr> = \<AA>"
    and "\<NN>\<lparr>NTDGCod\<rparr> = \<BB>"
    and "vsv (\<NN>\<lparr>NTMap\<rparr>)"
    and "\<D>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>"
    and "\<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
    and "\<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow>
      \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
  shows "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (intro is_ntsmcfI is_tdghmI, unfold ntsmcf_tdghm_components slicing_simps)
    (
      simp_all add:
        assms nat_omega_simps
        ntsmcf_tdghm_def
        is_semifunctorD(6)[OF assms(3)]
        is_semifunctorD(6)[OF assms(4)]
    )


[STATEMENT]
lemma is_ntsmcfD':
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<Z> \<alpha>"
    and "vfsequence \<NN>"
    and "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "vcard \<NN> = 5\<^sub>\<nat>"
    and "\<NN>\<lparr>NTDom\<rparr> = \<FF>"
    and "\<NN>\<lparr>NTCod\<rparr> = \<GG>"
    and "\<NN>\<lparr>NTDGDom\<rparr> = \<AA>"
    and "\<NN>\<lparr>NTDGCod\<rparr> = \<BB>"
    and "vsv (\<NN>\<lparr>NTMap\<rparr>)"
    and "\<D>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>"
    and "\<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
    and "\<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow>
      \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<Z> \<alpha> &&& vfsequence \<NN> &&& \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>) &&& \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB> &&& vcard \<NN> = 5\<^sub>\<nat> &&& \<NN>\<lparr>NTDom\<rparr> = \<FF>) &&& (\<NN>\<lparr>NTCod\<rparr> = \<GG> &&& \<NN>\<lparr>NTDGDom\<rparr> = \<AA> &&& \<NN>\<lparr>NTDGCod\<rparr> = \<BB>) &&& (vsv (\<NN>\<lparr>NTMap\<rparr>) &&& \<D>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>) &&& (\<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) &&& (\<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)
[PROOF STEP]
by
    (
      simp_all add:
        is_ntsmcfD(2-11)[OF assms]
        is_tdghmD[OF is_ntsmcfD(6)[OF assms], unfolded slicing_simps]
    )


[STATEMENT]
lemma is_ntsmcfE':
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
  obtains "\<Z> \<alpha>"
    and "vfsequence \<NN>"
    and "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "vcard \<NN> = 5\<^sub>\<nat>"
    and "\<NN>\<lparr>NTDom\<rparr> = \<FF>"
    and "\<NN>\<lparr>NTCod\<rparr> = \<GG>"
    and "\<NN>\<lparr>NTDGDom\<rparr> = \<AA>"
    and "\<NN>\<lparr>NTDGCod\<rparr> = \<BB>"
    and "vsv (\<NN>\<lparr>NTMap\<rparr>)"
    and "\<D>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>"
    and "\<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
    and "\<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow>
      \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<Z> \<alpha>; vfsequence \<NN>; \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>; \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>; vcard \<NN> = 5\<^sub>\<nat>; \<NN>\<lparr>NTDom\<rparr> = \<FF>; \<NN>\<lparr>NTCod\<rparr> = \<GG>; \<NN>\<lparr>NTDGDom\<rparr> = \<AA>; \<NN>\<lparr>NTDGCod\<rparr> = \<BB>; vsv (\<NN>\<lparr>NTMap\<rparr>); \<D>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>; \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>; \<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. (\<lbrakk>\<Z> \<alpha>; vfsequence \<NN>; \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>; \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>; vcard \<NN> = 5\<^sub>\<nat>; \<NN>\<lparr>NTDom\<rparr> = \<FF>; \<NN>\<lparr>NTCod\<rparr> = \<GG>; \<NN>\<lparr>NTDGDom\<rparr> = \<AA>; \<NN>\<lparr>NTDGCod\<rparr> = \<BB>; vsv (\<NN>\<lparr>NTMap\<rparr>); \<D>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>; \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>; \<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp add: is_ntsmcfD')


[STATEMENT]
lemma (in is_ntsmcf) ntsmcf_Comp_commute':
  assumes "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b" and "g : c \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
  shows
    "\<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> g) =
      (\<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>) \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> g) = \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> g
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
g : c \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>

goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> g) = \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> g
[PROOF STEP]
by
    (
      cs_concl cs_shallow
        cs_simp: ntsmcf_Comp_commute semicategory.smc_Comp_assoc[symmetric]
        cs_intro: smc_cs_intros
    )


[STATEMENT]
lemma (in is_ntsmcf) ntsmcf_Comp_commute'':
  assumes "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b" and "g : c \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
  shows
    "\<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> g) =
      (\<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>) \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> g) = \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> g
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
g : c \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>

goal (1 subgoal):
 1. \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> g) = \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> g
[PROOF STEP]
by
    (
      cs_concl
        cs_simp: ntsmcf_Comp_commute semicategory.smc_Comp_assoc[symmetric]
        cs_intro: smc_cs_intros
    )


[STATEMENT]
lemma ntsmcf_eqI:
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<NN>' : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>'"
    and "\<NN>\<lparr>NTMap\<rparr> = \<NN>'\<lparr>NTMap\<rparr>"
    and "\<FF> = \<FF>'"
    and "\<GG> = \<GG>'"
    and "\<AA> = \<AA>'"
    and "\<BB> = \<BB>'"
  shows "\<NN> = \<NN>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> = \<NN>'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<NN> = \<NN>'
[PROOF STEP]
interpret L: is_ntsmcf \<alpha> \<AA> \<BB> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<NN> = \<NN>'
[PROOF STEP]
interpret R: is_ntsmcf \<alpha> \<AA>' \<BB>' \<FF>' \<GG>' \<NN>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN>' : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<NN> = \<NN>'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> = \<NN>'
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv \<NN>
 2. vsv \<NN>'
 3. \<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> \<NN>'
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = \<NN>'\<lparr>a\<rparr>
[PROOF STEP]
have dom: "\<D>\<^sub>\<circ> \<NN> = 5\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> \<NN> = 5\<^sub>\<nat>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: smc_cs_simps V_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> \<NN> = 5\<^sub>\<nat>

goal (4 subgoals):
 1. vsv \<NN>
 2. vsv \<NN>'
 3. \<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> \<NN>'
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = \<NN>'\<lparr>a\<rparr>
[PROOF STEP]
show "\<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> \<NN>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> \<NN>'
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: smc_cs_simps V_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> \<NN>'

goal (3 subgoals):
 1. vsv \<NN>
 2. vsv \<NN>'
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = \<NN>'\<lparr>a\<rparr>
[PROOF STEP]
from assms(4-7)
[PROOF STATE]
proof (chain)
picking this:
\<FF> = \<FF>'
\<GG> = \<GG>'
\<AA> = \<AA>'
\<BB> = \<BB>'
[PROOF STEP]
have sup:
      "\<NN>\<lparr>NTDom\<rparr> = \<NN>'\<lparr>NTDom\<rparr>" "\<NN>\<lparr>NTCod\<rparr> = \<NN>'\<lparr>NTCod\<rparr>"
      "\<NN>\<lparr>NTDGDom\<rparr> = \<NN>'\<lparr>NTDGDom\<rparr>" "\<NN>\<lparr>NTDGCod\<rparr> = \<NN>'\<lparr>NTDGCod\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<FF> = \<FF>'
\<GG> = \<GG>'
\<AA> = \<AA>'
\<BB> = \<BB>'

goal (1 subgoal):
 1. (\<NN>\<lparr>NTDom\<rparr> = \<NN>'\<lparr>NTDom\<rparr> &&& \<NN>\<lparr>NTCod\<rparr> = \<NN>'\<lparr>NTCod\<rparr>) &&& \<NN>\<lparr>NTDGDom\<rparr> = \<NN>'\<lparr>NTDGDom\<rparr> &&& \<NN>\<lparr>NTDGCod\<rparr> = \<NN>'\<lparr>NTDGCod\<rparr>
[PROOF STEP]
by (simp_all add: smc_cs_simps)
[PROOF STATE]
proof (state)
this:
\<NN>\<lparr>NTDom\<rparr> = \<NN>'\<lparr>NTDom\<rparr>
\<NN>\<lparr>NTCod\<rparr> = \<NN>'\<lparr>NTCod\<rparr>
\<NN>\<lparr>NTDGDom\<rparr> = \<NN>'\<lparr>NTDGDom\<rparr>
\<NN>\<lparr>NTDGCod\<rparr> = \<NN>'\<lparr>NTDGCod\<rparr>

goal (3 subgoals):
 1. vsv \<NN>
 2. vsv \<NN>'
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = \<NN>'\<lparr>a\<rparr>
[PROOF STEP]
show "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = \<NN>'\<lparr>a\<rparr>" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = \<NN>'\<lparr>a\<rparr>
[PROOF STEP]
by (unfold dom, elim_in_numeral, insert assms(3) sup)
        (auto simp: nt_field_simps)
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>?a\<rparr> = \<NN>'\<lparr>?a\<rparr>

goal (2 subgoals):
 1. vsv \<NN>
 2. vsv \<NN>'
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<NN> = \<NN>'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ntsmcf_tdghm_eqI:
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<NN>' : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>'"
    and "\<FF> = \<FF>'"
    and "\<GG> = \<GG>'"
    and "\<AA> = \<AA>'"
    and "\<BB> = \<BB>'"
    and "ntsmcf_tdghm \<NN> = ntsmcf_tdghm \<NN>'"
  shows "\<NN> = \<NN>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> = \<NN>'
[PROOF STEP]
proof(rule ntsmcf_eqI[of \<alpha>])
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<NN> : ?\<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<NN>' : ?\<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>'
 3. \<NN>\<lparr>NTMap\<rparr> = \<NN>'\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
from assms(7)
[PROOF STATE]
proof (chain)
picking this:
ntsmcf_tdghm \<NN> = ntsmcf_tdghm \<NN>'
[PROOF STEP]
have "ntsmcf_tdghm \<NN>\<lparr>NTMap\<rparr> = ntsmcf_tdghm \<NN>'\<lparr>NTMap\<rparr>"
[PROOF STATE]
proof (prove)
using this:
ntsmcf_tdghm \<NN> = ntsmcf_tdghm \<NN>'

goal (1 subgoal):
 1. ntsmcf_tdghm \<NN>\<lparr>NTMap\<rparr> = ntsmcf_tdghm \<NN>'\<lparr>NTMap\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ntsmcf_tdghm \<NN>\<lparr>NTMap\<rparr> = ntsmcf_tdghm \<NN>'\<lparr>NTMap\<rparr>

goal (7 subgoals):
 1. \<NN> : ?\<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<NN>' : ?\<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>'
 3. \<NN>\<lparr>NTMap\<rparr> = \<NN>'\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ntsmcf_tdghm \<NN>\<lparr>NTMap\<rparr> = ntsmcf_tdghm \<NN>'\<lparr>NTMap\<rparr>
[PROOF STEP]
show "\<NN>\<lparr>NTMap\<rparr> = \<NN>'\<lparr>NTMap\<rparr>"
[PROOF STATE]
proof (prove)
using this:
ntsmcf_tdghm \<NN>\<lparr>NTMap\<rparr> = ntsmcf_tdghm \<NN>'\<lparr>NTMap\<rparr>

goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr> = \<NN>'\<lparr>NTMap\<rparr>
[PROOF STEP]
unfolding slicing_simps
[PROOF STATE]
proof (prove)
using this:
\<NN>\<lparr>NTMap\<rparr> = \<NN>'\<lparr>NTMap\<rparr>

goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr> = \<NN>'\<lparr>NTMap\<rparr>
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<NN>\<lparr>NTMap\<rparr> = \<NN>'\<lparr>NTMap\<rparr>

goal (6 subgoals):
 1. \<NN> : ?\<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<NN>' : ?\<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>'
 3. ?\<FF> = ?\<FF>'
 4. ?\<GG> = ?\<GG>'
 5. ?\<AA> = ?\<AA>'
 6. ?\<BB> = ?\<BB>'
[PROOF STEP]
from assms(3-6)
[PROOF STATE]
proof (chain)
picking this:
\<FF> = \<FF>'
\<GG> = \<GG>'
\<AA> = \<AA>'
\<BB> = \<BB>'
[PROOF STEP]
show "\<FF> = \<FF>'" "\<GG> = \<GG>'" "\<AA> = \<AA>'" "\<BB> = \<BB>'"
[PROOF STATE]
proof (prove)
using this:
\<FF> = \<FF>'
\<GG> = \<GG>'
\<AA> = \<AA>'
\<BB> = \<BB>'

goal (1 subgoal):
 1. (\<FF> = \<FF>' &&& \<GG> = \<GG>') &&& \<AA> = \<AA>' &&& \<BB> = \<BB>'
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<FF> = \<FF>'
\<GG> = \<GG>'
\<AA> = \<AA>'
\<BB> = \<BB>'

goal (2 subgoals):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 2. \<NN>' : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
qed (simp_all add: assms(1,2))


[STATEMENT]
lemma (in is_ntsmcf) ntsmcf_def:
  "\<NN> = [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> = [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv \<NN>
 2. vsv [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
 3. \<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>\<lparr>a\<rparr>
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> \<NN> = 5\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> \<NN> = 5\<^sub>\<nat>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: smc_cs_simps V_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> \<NN> = 5\<^sub>\<nat>

goal (4 subgoals):
 1. vsv \<NN>
 2. vsv [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
 3. \<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>\<lparr>a\<rparr>
[PROOF STEP]
have dom_rhs:
    "\<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>]\<^sub>\<circ> = 5\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>]\<^sub>\<circ> = 5\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>]\<^sub>\<circ> = 5\<^sub>\<nat>

goal (4 subgoals):
 1. vsv \<NN>
 2. vsv [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
 3. \<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>]\<^sub>\<circ> = 5\<^sub>\<nat>
[PROOF STEP]
show "\<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
using this:
\<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>]\<^sub>\<circ> = 5\<^sub>\<nat>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
[PROOF STEP]
unfolding dom_lhs dom_rhs
[PROOF STATE]
proof (prove)
using this:
5\<^sub>\<nat> = 5\<^sub>\<nat>

goal (1 subgoal):
 1. 5\<^sub>\<nat> = \<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>

goal (3 subgoals):
 1. vsv \<NN>
 2. vsv [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>\<lparr>a\<rparr>
[PROOF STEP]
show "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow>
    \<NN>\<lparr>a\<rparr> = [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>\<lparr>a\<rparr>"
    for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>\<lparr>a\<rparr>
[PROOF STEP]
by (unfold dom_lhs, elim_in_numeral, unfold nt_field_simps)
      (simp_all add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>?a\<rparr> = [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>\<lparr>?a\<rparr>

goal (2 subgoals):
 1. vsv \<NN>
 2. vsv [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
[PROOF STEP]
qed (auto simp: vsv_axioms)


[STATEMENT]
lemma (in is_ntsmcf) ntsmcf_in_Vset:
  assumes "\<Z> \<beta>" and "\<alpha> \<in>\<^sub>\<circ> \<beta>"
  shows "\<NN> \<in>\<^sub>\<circ> Vset \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<NN> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
interpret \<beta>: \<Z> \<beta>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Z> \<beta>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<NN> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
note [smc_cs_intros] =
    ntsmcf_NTMap_in_Vset
    NTDom.smcf_in_Vset
    NTCod.smcf_in_Vset
    NTDom.HomDom.smc_in_Vset
    NTDom.HomCod.smc_in_Vset
[PROOF STATE]
proof (state)
this:
\<alpha> \<in>\<^sub>\<circ> ?\<beta> \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr> \<in>\<^sub>\<circ> Vset ?\<beta>
\<lbrakk>\<Z> ?\<beta>; \<alpha> \<in>\<^sub>\<circ> ?\<beta>\<rbrakk> \<Longrightarrow> \<FF> \<in>\<^sub>\<circ> Vset ?\<beta>
\<lbrakk>\<Z> ?\<beta>; \<alpha> \<in>\<^sub>\<circ> ?\<beta>\<rbrakk> \<Longrightarrow> \<GG> \<in>\<^sub>\<circ> Vset ?\<beta>
\<lbrakk>\<Z> ?\<beta>; \<alpha> \<in>\<^sub>\<circ> ?\<beta>\<rbrakk> \<Longrightarrow> \<AA> \<in>\<^sub>\<circ> Vset ?\<beta>
\<lbrakk>\<Z> ?\<beta>; \<alpha> \<in>\<^sub>\<circ> ?\<beta>\<rbrakk> \<Longrightarrow> \<BB> \<in>\<^sub>\<circ> Vset ?\<beta>

goal (1 subgoal):
 1. \<NN> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<in>\<^sub>\<circ> \<beta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in>\<^sub>\<circ> \<beta>

goal (1 subgoal):
 1. \<NN> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
by (subst ntsmcf_def)
      (
        cs_concl cs_shallow
          cs_simp: smc_cs_simps cs_intro: smc_cs_intros V_cs_intros
      )
[PROOF STATE]
proof (state)
this:
\<NN> \<in>\<^sub>\<circ> Vset \<beta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_ntsmcf) ntsmcf_is_ntsmcf_if_ge_Limit:
  assumes "\<Z> \<beta>" and "\<alpha> \<in>\<^sub>\<circ> \<beta>"
  shows "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<beta>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<beta>\<^esub> \<BB>
[PROOF STEP]
proof(intro is_ntsmcfI )
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<Z> \<beta>
 2. vfsequence \<NN>
 3. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<beta>\<^esub> \<BB>
 4. \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<beta>\<^esub> \<BB>
 5. vcard \<NN> = 5\<^sub>\<nat>
 6. ntsmcf_tdghm \<NN> : smcf_dghm \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm \<GG> : smc_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<beta>\<^esub> smc_dg \<BB>
 7. \<NN>\<lparr>NTDom\<rparr> = \<FF>
 8. \<NN>\<lparr>NTCod\<rparr> = \<GG>
 9. \<NN>\<lparr>NTDGDom\<rparr> = \<AA>
 10. \<NN>\<lparr>NTDGCod\<rparr> = \<BB>
A total of 11 subgoals...
[PROOF STEP]
show "ntsmcf_tdghm \<NN> :
    smcf_dghm \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm \<GG> : smc_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<beta>\<^esub> smc_dg \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntsmcf_tdghm \<NN> : smcf_dghm \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm \<GG> : smc_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<beta>\<^esub> smc_dg \<BB>
[PROOF STEP]
by (rule is_tdghm.tdghm_is_tdghm_if_ge_Limit[OF ntsmcf_is_tdghm assms])
[PROOF STATE]
proof (state)
this:
ntsmcf_tdghm \<NN> : smcf_dghm \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm \<GG> : smc_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<beta>\<^esub> smc_dg \<BB>

goal (10 subgoals):
 1. \<Z> \<beta>
 2. vfsequence \<NN>
 3. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<beta>\<^esub> \<BB>
 4. \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<beta>\<^esub> \<BB>
 5. vcard \<NN> = 5\<^sub>\<nat>
 6. \<NN>\<lparr>NTDom\<rparr> = \<FF>
 7. \<NN>\<lparr>NTCod\<rparr> = \<GG>
 8. \<NN>\<lparr>NTDGDom\<rparr> = \<AA>
 9. \<NN>\<lparr>NTDGCod\<rparr> = \<BB>
 10. \<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "\<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
    if "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b" for f a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by
      (
        use that in
          \<open>cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros\<close>
      )+
[PROOF STATE]
proof (state)
this:
?f : ?a \<mapsto>\<^bsub>\<AA>\<^esub> ?b \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>?b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> = \<GG>\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>?a\<rparr>

goal (9 subgoals):
 1. \<Z> \<beta>
 2. vfsequence \<NN>
 3. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<beta>\<^esub> \<BB>
 4. \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<beta>\<^esub> \<BB>
 5. vcard \<NN> = 5\<^sub>\<nat>
 6. \<NN>\<lparr>NTDom\<rparr> = \<FF>
 7. \<NN>\<lparr>NTCod\<rparr> = \<GG>
 8. \<NN>\<lparr>NTDGDom\<rparr> = \<AA>
 9. \<NN>\<lparr>NTDGCod\<rparr> = \<BB>
[PROOF STEP]
qed
  (
    cs_concl cs_shallow
      cs_simp: smc_cs_simps
      cs_intro:
        smc_cs_intros
        V_cs_intros
        assms
        NTDom.smcf_is_semifunctor_if_ge_Limit
        NTCod.smcf_is_semifunctor_if_ge_Limit
   )+


[STATEMENT]
lemma small_all_ntsmcfs[simp]:
  "small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
proof(cases \<open>\<Z> \<alpha>\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Z> \<alpha> \<Longrightarrow> small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}
 2. \<not> \<Z> \<alpha> \<Longrightarrow> small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<Z> \<alpha>

goal (2 subgoals):
 1. \<Z> \<alpha> \<Longrightarrow> small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}
 2. \<not> \<Z> \<alpha> \<Longrightarrow> small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
from is_ntsmcf.ntsmcf_in_Vset
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?\<NN> : ?\<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>; \<Z> ?\<beta>; ?\<alpha> \<in>\<^sub>\<circ> ?\<beta>\<rbrakk> \<Longrightarrow> ?\<NN> \<in>\<^sub>\<circ> Vset ?\<beta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<NN> : ?\<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>; \<Z> ?\<beta>; ?\<alpha> \<in>\<^sub>\<circ> ?\<beta>\<rbrakk> \<Longrightarrow> ?\<NN> \<in>\<^sub>\<circ> Vset ?\<beta>

goal (1 subgoal):
 1. small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
by (intro down[of _ \<open>Vset (\<alpha> + \<omega>)\<close>])
      (auto simp: True \<Z>.\<Z>_Limit_\<alpha>\<omega> \<Z>.\<Z>_\<omega>_\<alpha>\<omega> \<Z>.intro \<Z>.\<Z>_\<alpha>_\<alpha>\<omega>)
[PROOF STATE]
proof (state)
this:
small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}

goal (1 subgoal):
 1. \<not> \<Z> \<alpha> \<Longrightarrow> small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<Z> \<alpha> \<Longrightarrow> small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> \<Z> \<alpha>

goal (1 subgoal):
 1. \<not> \<Z> \<alpha> \<Longrightarrow> small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> \<Z> \<alpha>
[PROOF STEP]
have "{\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>} = {}"
[PROOF STATE]
proof (prove)
using this:
\<not> \<Z> \<alpha>

goal (1 subgoal):
 1. {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>} = {}

goal (1 subgoal):
 1. \<not> \<Z> \<alpha> \<Longrightarrow> small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>} = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>} = {}

goal (1 subgoal):
 1. small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma small_ntsmcfs[simp]: "small {\<NN>. \<exists>\<FF> \<GG>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small {\<NN>. \<exists>\<FF> \<GG>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
by (rule down[of _ \<open>set {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}\<close>])
    auto


[STATEMENT]
lemma small_these_ntcfs[simp]: "small {\<NN>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small {\<NN>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
by (rule down[of _ \<open>set {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>}\<close>])
    auto


[STATEMENT]
lemma these_ntsmcfs_iff(*not simp*):
  "\<NN> \<in>\<^sub>\<circ> these_ntsmcfs \<alpha> \<AA> \<BB> \<FF> \<GG> \<longleftrightarrow> \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<NN> \<in>\<^sub>\<circ> these_ntsmcfs \<alpha> \<AA> \<BB> \<FF> \<GG>) = \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by auto


[STATEMENT]
lemma op_tdghm_ntsmcf_tdghm[slicing_commute]:
  "op_tdghm (ntsmcf_tdghm \<NN>) = ntsmcf_tdghm (op_ntsmcf \<NN>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_tdghm (ntsmcf_tdghm \<NN>) = ntsmcf_tdghm (op_ntsmcf \<NN>)
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (op_tdghm (ntsmcf_tdghm \<NN>))
 2. vsv (ntsmcf_tdghm (op_ntsmcf \<NN>))
 3. \<D>\<^sub>\<circ> (op_tdghm (ntsmcf_tdghm \<NN>)) = \<D>\<^sub>\<circ> (ntsmcf_tdghm (op_ntsmcf \<NN>))
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_tdghm (ntsmcf_tdghm \<NN>)) \<Longrightarrow> op_tdghm (ntsmcf_tdghm \<NN>)\<lparr>a\<rparr> = ntsmcf_tdghm (op_ntsmcf \<NN>)\<lparr>a\<rparr>
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> (op_tdghm (ntsmcf_tdghm \<NN>)) = 5\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (op_tdghm (ntsmcf_tdghm \<NN>)) = 5\<^sub>\<nat>
[PROOF STEP]
unfolding op_tdghm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [ntsmcf_tdghm \<NN>\<lparr>NTMap\<rparr>, op_dghm (ntsmcf_tdghm \<NN>\<lparr>NTCod\<rparr>), op_dghm (ntsmcf_tdghm \<NN>\<lparr>NTDom\<rparr>), op_dg (ntsmcf_tdghm \<NN>\<lparr>NTDGDom\<rparr>), op_dg (ntsmcf_tdghm \<NN>\<lparr>NTDGCod\<rparr>)]\<^sub>\<circ> = 5\<^sub>\<nat>
[PROOF STEP]
by (auto simp: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (op_tdghm (ntsmcf_tdghm \<NN>)) = 5\<^sub>\<nat>

goal (4 subgoals):
 1. vsv (op_tdghm (ntsmcf_tdghm \<NN>))
 2. vsv (ntsmcf_tdghm (op_ntsmcf \<NN>))
 3. \<D>\<^sub>\<circ> (op_tdghm (ntsmcf_tdghm \<NN>)) = \<D>\<^sub>\<circ> (ntsmcf_tdghm (op_ntsmcf \<NN>))
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_tdghm (ntsmcf_tdghm \<NN>)) \<Longrightarrow> op_tdghm (ntsmcf_tdghm \<NN>)\<lparr>a\<rparr> = ntsmcf_tdghm (op_ntsmcf \<NN>)\<lparr>a\<rparr>
[PROOF STEP]
have dom_rhs: "\<D>\<^sub>\<circ> (ntsmcf_tdghm (op_ntsmcf \<NN>)) = 5\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (ntsmcf_tdghm (op_ntsmcf \<NN>)) = 5\<^sub>\<nat>
[PROOF STEP]
unfolding ntsmcf_tdghm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [op_ntsmcf \<NN>\<lparr>NTMap\<rparr>, smcf_dghm (op_ntsmcf \<NN>\<lparr>NTDom\<rparr>), smcf_dghm (op_ntsmcf \<NN>\<lparr>NTCod\<rparr>), smc_dg (op_ntsmcf \<NN>\<lparr>NTDGDom\<rparr>), smc_dg (op_ntsmcf \<NN>\<lparr>NTDGCod\<rparr>)]\<^sub>\<circ> = 5\<^sub>\<nat>
[PROOF STEP]
by (auto simp: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (ntsmcf_tdghm (op_ntsmcf \<NN>)) = 5\<^sub>\<nat>

goal (4 subgoals):
 1. vsv (op_tdghm (ntsmcf_tdghm \<NN>))
 2. vsv (ntsmcf_tdghm (op_ntsmcf \<NN>))
 3. \<D>\<^sub>\<circ> (op_tdghm (ntsmcf_tdghm \<NN>)) = \<D>\<^sub>\<circ> (ntsmcf_tdghm (op_ntsmcf \<NN>))
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_tdghm (ntsmcf_tdghm \<NN>)) \<Longrightarrow> op_tdghm (ntsmcf_tdghm \<NN>)\<lparr>a\<rparr> = ntsmcf_tdghm (op_ntsmcf \<NN>)\<lparr>a\<rparr>
[PROOF STEP]
show "\<D>\<^sub>\<circ> (op_tdghm (ntsmcf_tdghm \<NN>)) = \<D>\<^sub>\<circ> (ntsmcf_tdghm (op_ntsmcf \<NN>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (op_tdghm (ntsmcf_tdghm \<NN>)) = \<D>\<^sub>\<circ> (ntsmcf_tdghm (op_ntsmcf \<NN>))
[PROOF STEP]
unfolding dom_lhs dom_rhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 5\<^sub>\<nat> = 5\<^sub>\<nat>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (op_tdghm (ntsmcf_tdghm \<NN>)) = \<D>\<^sub>\<circ> (ntsmcf_tdghm (op_ntsmcf \<NN>))

goal (3 subgoals):
 1. vsv (op_tdghm (ntsmcf_tdghm \<NN>))
 2. vsv (ntsmcf_tdghm (op_ntsmcf \<NN>))
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_tdghm (ntsmcf_tdghm \<NN>)) \<Longrightarrow> op_tdghm (ntsmcf_tdghm \<NN>)\<lparr>a\<rparr> = ntsmcf_tdghm (op_ntsmcf \<NN>)\<lparr>a\<rparr>
[PROOF STEP]
show "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_tdghm (ntsmcf_tdghm \<NN>)) \<Longrightarrow>
    op_tdghm (ntsmcf_tdghm \<NN>)\<lparr>a\<rparr> = ntsmcf_tdghm (op_ntsmcf \<NN>)\<lparr>a\<rparr>"
    for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_tdghm (ntsmcf_tdghm \<NN>)) \<Longrightarrow> op_tdghm (ntsmcf_tdghm \<NN>)\<lparr>a\<rparr> = ntsmcf_tdghm (op_ntsmcf \<NN>)\<lparr>a\<rparr>
[PROOF STEP]
by
      (
        unfold dom_lhs,
        elim_in_numeral,
        unfold ntsmcf_tdghm_def op_ntsmcf_def op_tdghm_def nt_field_simps
      )
      (auto simp: nat_omega_simps slicing_commute[symmetric])
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_tdghm (ntsmcf_tdghm \<NN>)) \<Longrightarrow> op_tdghm (ntsmcf_tdghm \<NN>)\<lparr>?a\<rparr> = ntsmcf_tdghm (op_ntsmcf \<NN>)\<lparr>?a\<rparr>

goal (2 subgoals):
 1. vsv (op_tdghm (ntsmcf_tdghm \<NN>))
 2. vsv (ntsmcf_tdghm (op_ntsmcf \<NN>))
[PROOF STEP]
qed (auto simp: ntsmcf_tdghm_def op_tdghm_def)


[STATEMENT]
lemma (in is_ntsmcf) is_ntsmcf_op:
  "op_ntsmcf \<NN> : op_smcf \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<FF> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntsmcf \<NN> : op_smcf \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<FF> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>
[PROOF STEP]
proof(rule is_ntsmcfI, unfold smc_op_simps)
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (op_ntsmcf \<NN>)
 3. op_smcf \<GG> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>
 4. op_smcf \<FF> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>
 5. vcard (op_ntsmcf \<NN>) = 5\<^sub>\<nat>
 6. ntsmcf_tdghm (op_ntsmcf \<NN>) : smcf_dghm (op_smcf \<GG>) \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm (op_smcf \<FF>) : smc_dg (op_smc \<AA>) \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg (op_smc \<BB>)
 7. op_smcf (\<NN>\<lparr>NTCod\<rparr>) = op_smcf \<GG>
 8. op_smcf (\<NN>\<lparr>NTDom\<rparr>) = op_smcf \<FF>
 9. op_smc (\<NN>\<lparr>NTDGDom\<rparr>) = op_smc \<AA>
 10. op_smc (\<NN>\<lparr>NTDGCod\<rparr>) = op_smc \<BB>
A total of 11 subgoals...
[PROOF STEP]
show "vfsequence (op_ntsmcf \<NN>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (op_ntsmcf \<NN>)
[PROOF STEP]
by (simp add: op_ntsmcf_def)
[PROOF STATE]
proof (state)
this:
vfsequence (op_ntsmcf \<NN>)

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. op_smcf \<GG> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>
 3. op_smcf \<FF> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>
 4. vcard (op_ntsmcf \<NN>) = 5\<^sub>\<nat>
 5. ntsmcf_tdghm (op_ntsmcf \<NN>) : smcf_dghm (op_smcf \<GG>) \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm (op_smcf \<FF>) : smc_dg (op_smc \<AA>) \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg (op_smc \<BB>)
 6. op_smcf (\<NN>\<lparr>NTCod\<rparr>) = op_smcf \<GG>
 7. op_smcf (\<NN>\<lparr>NTDom\<rparr>) = op_smcf \<FF>
 8. op_smc (\<NN>\<lparr>NTDGDom\<rparr>) = op_smc \<AA>
 9. op_smc (\<NN>\<lparr>NTDGCod\<rparr>) = op_smc \<BB>
 10. \<And>a b f. f : b \<mapsto>\<^bsub>\<AA>\<^esub> a \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "vcard (op_ntsmcf \<NN>) = 5\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (op_ntsmcf \<NN>) = 5\<^sub>\<nat>
[PROOF STEP]
by (simp add: op_ntsmcf_def nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (op_ntsmcf \<NN>) = 5\<^sub>\<nat>

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. op_smcf \<GG> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>
 3. op_smcf \<FF> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>
 4. ntsmcf_tdghm (op_ntsmcf \<NN>) : smcf_dghm (op_smcf \<GG>) \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm (op_smcf \<FF>) : smc_dg (op_smc \<AA>) \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg (op_smc \<BB>)
 5. op_smcf (\<NN>\<lparr>NTCod\<rparr>) = op_smcf \<GG>
 6. op_smcf (\<NN>\<lparr>NTDom\<rparr>) = op_smcf \<FF>
 7. op_smc (\<NN>\<lparr>NTDGDom\<rparr>) = op_smc \<AA>
 8. op_smc (\<NN>\<lparr>NTDGCod\<rparr>) = op_smc \<BB>
 9. \<And>a b f. f : b \<mapsto>\<^bsub>\<AA>\<^esub> a \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix f a b
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<Z> \<alpha>
 2. op_smcf \<GG> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>
 3. op_smcf \<FF> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>
 4. ntsmcf_tdghm (op_ntsmcf \<NN>) : smcf_dghm (op_smcf \<GG>) \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm (op_smcf \<FF>) : smc_dg (op_smc \<AA>) \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg (op_smc \<BB>)
 5. op_smcf (\<NN>\<lparr>NTCod\<rparr>) = op_smcf \<GG>
 6. op_smcf (\<NN>\<lparr>NTDom\<rparr>) = op_smcf \<FF>
 7. op_smc (\<NN>\<lparr>NTDGDom\<rparr>) = op_smc \<AA>
 8. op_smc (\<NN>\<lparr>NTDGCod\<rparr>) = op_smc \<BB>
 9. \<And>a b f. f : b \<mapsto>\<^bsub>\<AA>\<^esub> a \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume "f : b \<mapsto>\<^bsub>\<AA>\<^esub> a"
[PROOF STATE]
proof (state)
this:
f : b \<mapsto>\<^bsub>\<AA>\<^esub> a

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. op_smcf \<GG> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>
 3. op_smcf \<FF> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>
 4. ntsmcf_tdghm (op_ntsmcf \<NN>) : smcf_dghm (op_smcf \<GG>) \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm (op_smcf \<FF>) : smc_dg (op_smc \<AA>) \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg (op_smc \<BB>)
 5. op_smcf (\<NN>\<lparr>NTCod\<rparr>) = op_smcf \<GG>
 6. op_smcf (\<NN>\<lparr>NTDom\<rparr>) = op_smcf \<FF>
 7. op_smc (\<NN>\<lparr>NTDGDom\<rparr>) = op_smc \<AA>
 8. op_smc (\<NN>\<lparr>NTDGCod\<rparr>) = op_smc \<BB>
 9. \<And>a b f. f : b \<mapsto>\<^bsub>\<AA>\<^esub> a \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
with is_ntsmcf_axioms
[PROOF STATE]
proof (chain)
picking this:
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
f : b \<mapsto>\<^bsub>\<AA>\<^esub> a
[PROOF STEP]
show
    "\<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> =
      \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
f : b \<mapsto>\<^bsub>\<AA>\<^esub> a

goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: smc_cs_simps smc_op_simps cs_intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
\<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> \<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (8 subgoals):
 1. \<Z> \<alpha>
 2. op_smcf \<GG> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>
 3. op_smcf \<FF> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>
 4. ntsmcf_tdghm (op_ntsmcf \<NN>) : smcf_dghm (op_smcf \<GG>) \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm (op_smcf \<FF>) : smc_dg (op_smc \<AA>) \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg (op_smc \<BB>)
 5. op_smcf (\<NN>\<lparr>NTCod\<rparr>) = op_smcf \<GG>
 6. op_smcf (\<NN>\<lparr>NTDom\<rparr>) = op_smcf \<FF>
 7. op_smc (\<NN>\<lparr>NTDGDom\<rparr>) = op_smc \<AA>
 8. op_smc (\<NN>\<lparr>NTDGCod\<rparr>) = op_smc \<BB>
[PROOF STEP]
qed
  (
    insert is_ntsmcf_axioms,
    (
      cs_concl cs_shallow
        cs_simp: smc_cs_simps slicing_commute[symmetric]
        cs_intro: smc_cs_intros smc_op_intros dg_op_intros slicing_intros
    )+
  )


[STATEMENT]
lemma (in is_ntsmcf) is_ntsmcf_op'[smc_op_intros]:
  assumes "\<GG>' = op_smcf \<GG>"
    and "\<FF>' = op_smcf \<FF>"
    and "\<AA>' = op_smc \<AA>"
    and "\<BB>' = op_smc \<BB>"
  shows "op_ntsmcf \<NN> : \<GG>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF>' : \<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntsmcf \<NN> : \<GG>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF>' : \<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntsmcf \<NN> : op_smcf \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<FF> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>
[PROOF STEP]
by (rule is_ntsmcf_op)


[STATEMENT]
lemma (in is_ntsmcf) ntsmcf_op_ntsmcf_op_ntsmcf[smc_op_simps]:
  "op_ntsmcf (op_ntsmcf \<NN>) = \<NN>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntsmcf (op_ntsmcf \<NN>) = \<NN>
[PROOF STEP]
proof(rule ntsmcf_eqI[of \<alpha> \<AA> \<BB> \<FF> \<GG> _ \<AA> \<BB> \<FF> \<GG>], unfold smc_op_simps)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. op_ntsmcf (op_ntsmcf \<NN>) : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 2. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 3. \<NN>\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>
 4. \<FF> = \<FF>
 5. \<GG> = \<GG>
 6. \<AA> = \<AA>
 7. \<BB> = \<BB>
[PROOF STEP]
interpret op:
    is_ntsmcf \<alpha> \<open>op_smc \<AA>\<close> \<open>op_smc \<BB>\<close> \<open>op_smcf \<GG>\<close> \<open>op_smcf \<FF>\<close> \<open>op_ntsmcf \<NN>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntsmcf \<NN> : op_smcf \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<FF> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>
[PROOF STEP]
by (rule is_ntsmcf_op)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. op_ntsmcf (op_ntsmcf \<NN>) : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 2. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 3. \<NN>\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>
 4. \<FF> = \<FF>
 5. \<GG> = \<GG>
 6. \<AA> = \<AA>
 7. \<BB> = \<BB>
[PROOF STEP]
from op.is_ntsmcf_op
[PROOF STATE]
proof (chain)
picking this:
op_ntsmcf (op_ntsmcf \<NN>) : op_smcf (op_smcf \<FF>) \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf (op_smcf \<GG>) : op_smc (op_smc \<AA>) \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc (op_smc \<BB>)
[PROOF STEP]
show
    "op_ntsmcf (op_ntsmcf \<NN>) : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
using this:
op_ntsmcf (op_ntsmcf \<NN>) : op_smcf (op_smcf \<FF>) \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf (op_smcf \<GG>) : op_smc (op_smc \<AA>) \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc (op_smc \<BB>)

goal (1 subgoal):
 1. op_ntsmcf (op_ntsmcf \<NN>) : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (simp add: smc_op_simps)
[PROOF STATE]
proof (state)
this:
op_ntsmcf (op_ntsmcf \<NN>) : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

goal (6 subgoals):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 2. \<NN>\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>
 3. \<FF> = \<FF>
 4. \<GG> = \<GG>
 5. \<AA> = \<AA>
 6. \<BB> = \<BB>
[PROOF STEP]
qed (auto simp: smc_cs_intros)


[STATEMENT]
lemma eq_op_ntsmcf_iff:
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<NN>' : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>'"
  shows "op_ntsmcf \<NN> = op_ntsmcf \<NN>' \<longleftrightarrow> \<NN> = \<NN>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (op_ntsmcf \<NN> = op_ntsmcf \<NN>') = (\<NN> = \<NN>')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. op_ntsmcf \<NN> = op_ntsmcf \<NN>' \<Longrightarrow> \<NN> = \<NN>'
 2. \<NN> = \<NN>' \<Longrightarrow> op_ntsmcf \<NN> = op_ntsmcf \<NN>'
[PROOF STEP]
interpret L: is_ntsmcf \<alpha> \<AA> \<BB> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. op_ntsmcf \<NN> = op_ntsmcf \<NN>' \<Longrightarrow> \<NN> = \<NN>'
 2. \<NN> = \<NN>' \<Longrightarrow> op_ntsmcf \<NN> = op_ntsmcf \<NN>'
[PROOF STEP]
interpret R: is_ntsmcf \<alpha> \<AA>' \<BB>' \<FF>' \<GG>' \<NN>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN>' : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. op_ntsmcf \<NN> = op_ntsmcf \<NN>' \<Longrightarrow> \<NN> = \<NN>'
 2. \<NN> = \<NN>' \<Longrightarrow> op_ntsmcf \<NN> = op_ntsmcf \<NN>'
[PROOF STEP]
assume prems: "op_ntsmcf \<NN> = op_ntsmcf \<NN>'"
[PROOF STATE]
proof (state)
this:
op_ntsmcf \<NN> = op_ntsmcf \<NN>'

goal (2 subgoals):
 1. op_ntsmcf \<NN> = op_ntsmcf \<NN>' \<Longrightarrow> \<NN> = \<NN>'
 2. \<NN> = \<NN>' \<Longrightarrow> op_ntsmcf \<NN> = op_ntsmcf \<NN>'
[PROOF STEP]
show "\<NN> = \<NN>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> = \<NN>'
[PROOF STEP]
proof(rule ntsmcf_eqI[OF assms])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<NN>\<lparr>NTMap\<rparr> = \<NN>'\<lparr>NTMap\<rparr>
 2. \<FF> = \<FF>'
 3. \<GG> = \<GG>'
 4. \<AA> = \<AA>'
 5. \<BB> = \<BB>'
[PROOF STEP]
from prems L.ntsmcf_op_ntsmcf_op_ntsmcf R.ntsmcf_op_ntsmcf_op_ntsmcf
[PROOF STATE]
proof (chain)
picking this:
op_ntsmcf \<NN> = op_ntsmcf \<NN>'
op_ntsmcf (op_ntsmcf \<NN>) = \<NN>
op_ntsmcf (op_ntsmcf \<NN>') = \<NN>'
[PROOF STEP]
show
      "\<NN>\<lparr>NTMap\<rparr> = \<NN>'\<lparr>NTMap\<rparr>"
[PROOF STATE]
proof (prove)
using this:
op_ntsmcf \<NN> = op_ntsmcf \<NN>'
op_ntsmcf (op_ntsmcf \<NN>) = \<NN>
op_ntsmcf (op_ntsmcf \<NN>') = \<NN>'

goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr> = \<NN>'\<lparr>NTMap\<rparr>
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
\<NN>\<lparr>NTMap\<rparr> = \<NN>'\<lparr>NTMap\<rparr>

goal (4 subgoals):
 1. \<FF> = \<FF>'
 2. \<GG> = \<GG>'
 3. \<AA> = \<AA>'
 4. \<BB> = \<BB>'
[PROOF STEP]
from prems L.ntsmcf_op_ntsmcf_op_ntsmcf R.ntsmcf_op_ntsmcf_op_ntsmcf
[PROOF STATE]
proof (chain)
picking this:
op_ntsmcf \<NN> = op_ntsmcf \<NN>'
op_ntsmcf (op_ntsmcf \<NN>) = \<NN>
op_ntsmcf (op_ntsmcf \<NN>') = \<NN>'
[PROOF STEP]
have "\<NN>\<lparr>NTDom\<rparr> = \<NN>'\<lparr>NTDom\<rparr>"
      and "\<NN>\<lparr>NTCod\<rparr> = \<NN>'\<lparr>NTCod\<rparr>"
      and "\<NN>\<lparr>NTDGDom\<rparr> = \<NN>'\<lparr>NTDGDom\<rparr>"
      and "\<NN>\<lparr>NTDGCod\<rparr> = \<NN>'\<lparr>NTDGCod\<rparr>"
[PROOF STATE]
proof (prove)
using this:
op_ntsmcf \<NN> = op_ntsmcf \<NN>'
op_ntsmcf (op_ntsmcf \<NN>) = \<NN>
op_ntsmcf (op_ntsmcf \<NN>') = \<NN>'

goal (1 subgoal):
 1. (\<NN>\<lparr>NTDom\<rparr> = \<NN>'\<lparr>NTDom\<rparr> &&& \<NN>\<lparr>NTCod\<rparr> = \<NN>'\<lparr>NTCod\<rparr>) &&& \<NN>\<lparr>NTDGDom\<rparr> = \<NN>'\<lparr>NTDGDom\<rparr> &&& \<NN>\<lparr>NTDGCod\<rparr> = \<NN>'\<lparr>NTDGCod\<rparr>
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
\<NN>\<lparr>NTDom\<rparr> = \<NN>'\<lparr>NTDom\<rparr>
\<NN>\<lparr>NTCod\<rparr> = \<NN>'\<lparr>NTCod\<rparr>
\<NN>\<lparr>NTDGDom\<rparr> = \<NN>'\<lparr>NTDGDom\<rparr>
\<NN>\<lparr>NTDGCod\<rparr> = \<NN>'\<lparr>NTDGCod\<rparr>

goal (4 subgoals):
 1. \<FF> = \<FF>'
 2. \<GG> = \<GG>'
 3. \<AA> = \<AA>'
 4. \<BB> = \<BB>'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<NN>\<lparr>NTDom\<rparr> = \<NN>'\<lparr>NTDom\<rparr>
\<NN>\<lparr>NTCod\<rparr> = \<NN>'\<lparr>NTCod\<rparr>
\<NN>\<lparr>NTDGDom\<rparr> = \<NN>'\<lparr>NTDGDom\<rparr>
\<NN>\<lparr>NTDGCod\<rparr> = \<NN>'\<lparr>NTDGCod\<rparr>
[PROOF STEP]
show "\<FF> = \<FF>'" "\<GG> = \<GG>'" "\<AA> = \<AA>'" "\<BB> = \<BB>'"
[PROOF STATE]
proof (prove)
using this:
\<NN>\<lparr>NTDom\<rparr> = \<NN>'\<lparr>NTDom\<rparr>
\<NN>\<lparr>NTCod\<rparr> = \<NN>'\<lparr>NTCod\<rparr>
\<NN>\<lparr>NTDGDom\<rparr> = \<NN>'\<lparr>NTDGDom\<rparr>
\<NN>\<lparr>NTDGCod\<rparr> = \<NN>'\<lparr>NTDGCod\<rparr>

goal (1 subgoal):
 1. (\<FF> = \<FF>' &&& \<GG> = \<GG>') &&& \<AA> = \<AA>' &&& \<BB> = \<BB>'
[PROOF STEP]
by (auto simp: smc_cs_simps)
[PROOF STATE]
proof (state)
this:
\<FF> = \<FF>'
\<GG> = \<GG>'
\<AA> = \<AA>'
\<BB> = \<BB>'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<NN> = \<NN>'

goal (1 subgoal):
 1. \<NN> = \<NN>' \<Longrightarrow> op_ntsmcf \<NN> = op_ntsmcf \<NN>'
[PROOF STEP]
qed auto