[STATEMENT]
lemma op_ntsmcf_components[smc_op_simps]:
  shows "op_ntsmcf \<NN>\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>"
    and "op_ntsmcf \<NN>\<lparr>NTDom\<rparr> = op_smcf (\<NN>\<lparr>NTCod\<rparr>)"
    and "op_ntsmcf \<NN>\<lparr>NTCod\<rparr> = op_smcf (\<NN>\<lparr>NTDom\<rparr>)"
    and "op_ntsmcf \<NN>\<lparr>NTDGDom\<rparr> = op_smc (\<NN>\<lparr>NTDGDom\<rparr>)"
    and "op_ntsmcf \<NN>\<lparr>NTDGCod\<rparr> = op_smc (\<NN>\<lparr>NTDGCod\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (op_ntsmcf \<NN>\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr> &&& op_ntsmcf \<NN>\<lparr>NTDom\<rparr> = op_smcf (\<NN>\<lparr>NTCod\<rparr>)) &&& op_ntsmcf \<NN>\<lparr>NTCod\<rparr> = op_smcf (\<NN>\<lparr>NTDom\<rparr>) &&& op_ntsmcf \<NN>\<lparr>NTDGDom\<rparr> = op_smc (\<NN>\<lparr>NTDGDom\<rparr>) &&& op_ntsmcf \<NN>\<lparr>NTDGCod\<rparr> = op_smc (\<NN>\<lparr>NTDGCod\<rparr>)
[PROOF STEP]
unfolding op_ntsmcf_def nt_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, op_smcf (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), op_smcf (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = \<NN>\<lparr>[]\<^sub>\<circ>\<rparr> &&& [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, op_smcf (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), op_smcf (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = op_smcf (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>)) &&& [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, op_smcf (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), op_smcf (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = op_smcf (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>) &&& [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, op_smcf (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), op_smcf (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = op_smc (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>) &&& [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, op_smcf (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), op_smcf (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr> = op_smc (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)
[PROOF STEP]
by (auto simp: nat_omega_simps)