[STATEMENT]
lemma dg_prod_3_is_arrI'[dg_prod_cs_intros]:
  assumes "F = [f, f', f'']\<^sub>\<circ>"
    and "A = [a, a', a'']\<^sub>\<circ>"
    and "B = [b, b', b'']\<^sub>\<circ>"
    and "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
    and "f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'"
    and "f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''"
  shows "F : A \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F : A \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> B
[PROOF STEP]
using assms(4,5,6)
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'
f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''

goal (1 subgoal):
 1. F : A \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> B
[PROOF STEP]
unfolding assms(1,2,3)
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'
f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''

goal (1 subgoal):
 1. [f, f', f'']\<^sub>\<circ> : [a, a', a'']\<^sub>\<circ> \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> [b, b', b'']\<^sub>\<circ>
[PROOF STEP]
by (rule dg_prod_3_is_arrI)


[STATEMENT]
lemma dg_prod_3_is_arrE:
  assumes "F : A \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> B"
  obtains f f' f'' a a' a'' b b' b''
    where "F = [f, f', f'']\<^sub>\<circ>"
      and "A = [a, a', a'']\<^sub>\<circ>"
      and "B = [b, b', b'']\<^sub>\<circ>"
      and "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
      and "f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'"
      and "f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f f' f'' a a' a'' b b' b''. \<lbrakk>F = [f, f', f'']\<^sub>\<circ>; A = [a, a', a'']\<^sub>\<circ>; B = [b, b', b'']\<^sub>\<circ>; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'; f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>f f' f'' a a' a'' b b' b''. \<lbrakk>F = [f, f', f'']\<^sub>\<circ>; A = [a, a', a'']\<^sub>\<circ>; B = [b, b', b'']\<^sub>\<circ>; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'; f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from dg_prod_is_arrD[OF assms[unfolded dg_prod_3_def]]
[PROOF STATE]
proof (chain)
picking this:
vsv F
\<D>\<^sub>\<circ> F = 3\<^sub>\<nat>
vsv A
\<D>\<^sub>\<circ> A = 3\<^sub>\<nat>
vsv B
\<D>\<^sub>\<circ> B = 3\<^sub>\<nat>
?i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> F\<lparr>?i\<rparr> : A\<lparr>?i\<rparr> \<mapsto>\<^bsub>if ?i = []\<^sub>\<circ> \<Rightarrow> \<AA> | ?i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>\<^esub> B\<lparr>?i\<rparr>
[PROOF STEP]
have [simp]: "vsv F" "\<D>\<^sub>\<circ> F = 3\<^sub>\<nat>" "vsv A" "\<D>\<^sub>\<circ> A = 3\<^sub>\<nat>" "vsv B" "\<D>\<^sub>\<circ> B = 3\<^sub>\<nat>"
    and F_app: "\<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> F\<lparr>i\<rparr> : A\<lparr>i\<rparr> \<mapsto>\<^bsub>if3 \<AA> \<BB> \<CC> i\<^esub> B\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
using this:
vsv F
\<D>\<^sub>\<circ> F = 3\<^sub>\<nat>
vsv A
\<D>\<^sub>\<circ> A = 3\<^sub>\<nat>
vsv B
\<D>\<^sub>\<circ> B = 3\<^sub>\<nat>
?i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> F\<lparr>?i\<rparr> : A\<lparr>?i\<rparr> \<mapsto>\<^bsub>if ?i = []\<^sub>\<circ> \<Rightarrow> \<AA> | ?i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>\<^esub> B\<lparr>?i\<rparr>

goal (1 subgoal):
 1. ((vsv F &&& \<D>\<^sub>\<circ> F = 3\<^sub>\<nat> &&& vsv A) &&& \<D>\<^sub>\<circ> A = 3\<^sub>\<nat> &&& vsv B &&& \<D>\<^sub>\<circ> B = 3\<^sub>\<nat>) &&& (\<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> F\<lparr>i\<rparr> : A\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>\<^esub> B\<lparr>i\<rparr>)
[PROOF STEP]
by (auto simp: three)
[PROOF STATE]
proof (state)
this:
vsv F
\<D>\<^sub>\<circ> F = 3\<^sub>\<nat>
vsv A
\<D>\<^sub>\<circ> A = 3\<^sub>\<nat>
vsv B
\<D>\<^sub>\<circ> B = 3\<^sub>\<nat>
?i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> F\<lparr>?i\<rparr> : A\<lparr>?i\<rparr> \<mapsto>\<^bsub>if ?i = []\<^sub>\<circ> \<Rightarrow> \<AA> | ?i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>\<^esub> B\<lparr>?i\<rparr>

goal (1 subgoal):
 1. (\<And>f f' f'' a a' a'' b b' b''. \<lbrakk>F = [f, f', f'']\<^sub>\<circ>; A = [a, a', a'']\<^sub>\<circ>; B = [b, b', b'']\<^sub>\<circ>; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'; f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "F = [vpfst F, vpsnd F, vpthrd F]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F = [F\<lparr>[]\<^sub>\<circ>\<rparr>, F\<lparr>1\<^sub>\<nat>\<rparr>, F\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: vsv_vfsequence_three)
[PROOF STATE]
proof (state)
this:
F = [F\<lparr>[]\<^sub>\<circ>\<rparr>, F\<lparr>1\<^sub>\<nat>\<rparr>, F\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>f f' f'' a a' a'' b b' b''. \<lbrakk>F = [f, f', f'']\<^sub>\<circ>; A = [a, a', a'']\<^sub>\<circ>; B = [b, b', b'']\<^sub>\<circ>; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'; f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
F = [F\<lparr>[]\<^sub>\<circ>\<rparr>, F\<lparr>1\<^sub>\<nat>\<rparr>, F\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>f f' f'' a a' a'' b b' b''. \<lbrakk>F = [f, f', f'']\<^sub>\<circ>; A = [a, a', a'']\<^sub>\<circ>; B = [b, b', b'']\<^sub>\<circ>; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'; f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "A = [vpfst A, vpsnd A, vpthrd A]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = [A\<lparr>[]\<^sub>\<circ>\<rparr>, A\<lparr>1\<^sub>\<nat>\<rparr>, A\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: vsv_vfsequence_three)
[PROOF STATE]
proof (state)
this:
A = [A\<lparr>[]\<^sub>\<circ>\<rparr>, A\<lparr>1\<^sub>\<nat>\<rparr>, A\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>f f' f'' a a' a'' b b' b''. \<lbrakk>F = [f, f', f'']\<^sub>\<circ>; A = [a, a', a'']\<^sub>\<circ>; B = [b, b', b'']\<^sub>\<circ>; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'; f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A = [A\<lparr>[]\<^sub>\<circ>\<rparr>, A\<lparr>1\<^sub>\<nat>\<rparr>, A\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>f f' f'' a a' a'' b b' b''. \<lbrakk>F = [f, f', f'']\<^sub>\<circ>; A = [a, a', a'']\<^sub>\<circ>; B = [b, b', b'']\<^sub>\<circ>; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'; f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "B = [vpfst B, vpsnd B, vpthrd B]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B = [B\<lparr>[]\<^sub>\<circ>\<rparr>, B\<lparr>1\<^sub>\<nat>\<rparr>, B\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: vsv_vfsequence_three)
[PROOF STATE]
proof (state)
this:
B = [B\<lparr>[]\<^sub>\<circ>\<rparr>, B\<lparr>1\<^sub>\<nat>\<rparr>, B\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>f f' f'' a a' a'' b b' b''. \<lbrakk>F = [f, f', f'']\<^sub>\<circ>; A = [a, a', a'']\<^sub>\<circ>; B = [b, b', b'']\<^sub>\<circ>; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'; f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
B = [B\<lparr>[]\<^sub>\<circ>\<rparr>, B\<lparr>1\<^sub>\<nat>\<rparr>, B\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>f f' f'' a a' a'' b b' b''. \<lbrakk>F = [f, f', f'']\<^sub>\<circ>; A = [a, a', a'']\<^sub>\<circ>; B = [b, b', b'']\<^sub>\<circ>; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'; f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from F_app[of 0]
[PROOF STATE]
proof (chain)
picking this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> F\<lparr>[]\<^sub>\<circ>\<rparr> : A\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>if []\<^sub>\<circ> = []\<^sub>\<circ> \<Rightarrow> \<AA> | []\<^sub>\<circ> = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>\<^esub> B\<lparr>[]\<^sub>\<circ>\<rparr>
[PROOF STEP]
have "vpfst F : vpfst A \<mapsto>\<^bsub>\<AA>\<^esub> vpfst B"
[PROOF STATE]
proof (prove)
using this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> F\<lparr>[]\<^sub>\<circ>\<rparr> : A\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>if []\<^sub>\<circ> = []\<^sub>\<circ> \<Rightarrow> \<AA> | []\<^sub>\<circ> = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>\<^esub> B\<lparr>[]\<^sub>\<circ>\<rparr>

goal (1 subgoal):
 1. F\<lparr>[]\<^sub>\<circ>\<rparr> : A\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> B\<lparr>[]\<^sub>\<circ>\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
F\<lparr>[]\<^sub>\<circ>\<rparr> : A\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> B\<lparr>[]\<^sub>\<circ>\<rparr>

goal (1 subgoal):
 1. (\<And>f f' f'' a a' a'' b b' b''. \<lbrakk>F = [f, f', f'']\<^sub>\<circ>; A = [a, a', a'']\<^sub>\<circ>; B = [b, b', b'']\<^sub>\<circ>; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'; f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
F\<lparr>[]\<^sub>\<circ>\<rparr> : A\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> B\<lparr>[]\<^sub>\<circ>\<rparr>

goal (1 subgoal):
 1. (\<And>f f' f'' a a' a'' b b' b''. \<lbrakk>F = [f, f', f'']\<^sub>\<circ>; A = [a, a', a'']\<^sub>\<circ>; B = [b, b', b'']\<^sub>\<circ>; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'; f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from F_app[of \<open>1\<^sub>\<nat>\<close>]
[PROOF STATE]
proof (chain)
picking this:
1\<^sub>\<nat> \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> F\<lparr>1\<^sub>\<nat>\<rparr> : A\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>if 1\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | 1\<^sub>\<nat> = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>\<^esub> B\<lparr>1\<^sub>\<nat>\<rparr>
[PROOF STEP]
have "vpsnd F : vpsnd A \<mapsto>\<^bsub>\<BB>\<^esub> vpsnd B"
[PROOF STATE]
proof (prove)
using this:
1\<^sub>\<nat> \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> F\<lparr>1\<^sub>\<nat>\<rparr> : A\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>if 1\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | 1\<^sub>\<nat> = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>\<^esub> B\<lparr>1\<^sub>\<nat>\<rparr>

goal (1 subgoal):
 1. F\<lparr>1\<^sub>\<nat>\<rparr> : A\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> B\<lparr>1\<^sub>\<nat>\<rparr>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
F\<lparr>1\<^sub>\<nat>\<rparr> : A\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> B\<lparr>1\<^sub>\<nat>\<rparr>

goal (1 subgoal):
 1. (\<And>f f' f'' a a' a'' b b' b''. \<lbrakk>F = [f, f', f'']\<^sub>\<circ>; A = [a, a', a'']\<^sub>\<circ>; B = [b, b', b'']\<^sub>\<circ>; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'; f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
F\<lparr>1\<^sub>\<nat>\<rparr> : A\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> B\<lparr>1\<^sub>\<nat>\<rparr>

goal (1 subgoal):
 1. (\<And>f f' f'' a a' a'' b b' b''. \<lbrakk>F = [f, f', f'']\<^sub>\<circ>; A = [a, a', a'']\<^sub>\<circ>; B = [b, b', b'']\<^sub>\<circ>; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'; f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from F_app[of \<open>2\<^sub>\<nat>\<close>]
[PROOF STATE]
proof (chain)
picking this:
2\<^sub>\<nat> \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> F\<lparr>2\<^sub>\<nat>\<rparr> : A\<lparr>2\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>if 2\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | 2\<^sub>\<nat> = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>\<^esub> B\<lparr>2\<^sub>\<nat>\<rparr>
[PROOF STEP]
have "vpthrd F : vpthrd A \<mapsto>\<^bsub>\<CC>\<^esub> vpthrd B"
[PROOF STATE]
proof (prove)
using this:
2\<^sub>\<nat> \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> F\<lparr>2\<^sub>\<nat>\<rparr> : A\<lparr>2\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>if 2\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | 2\<^sub>\<nat> = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>\<^esub> B\<lparr>2\<^sub>\<nat>\<rparr>

goal (1 subgoal):
 1. F\<lparr>2\<^sub>\<nat>\<rparr> : A\<lparr>2\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> B\<lparr>2\<^sub>\<nat>\<rparr>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
F\<lparr>2\<^sub>\<nat>\<rparr> : A\<lparr>2\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> B\<lparr>2\<^sub>\<nat>\<rparr>

goal (1 subgoal):
 1. (\<And>f f' f'' a a' a'' b b' b''. \<lbrakk>F = [f, f', f'']\<^sub>\<circ>; A = [a, a', a'']\<^sub>\<circ>; B = [b, b', b'']\<^sub>\<circ>; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'; f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
F = [F\<lparr>[]\<^sub>\<circ>\<rparr>, F\<lparr>1\<^sub>\<nat>\<rparr>, F\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
A = [A\<lparr>[]\<^sub>\<circ>\<rparr>, A\<lparr>1\<^sub>\<nat>\<rparr>, A\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
B = [B\<lparr>[]\<^sub>\<circ>\<rparr>, B\<lparr>1\<^sub>\<nat>\<rparr>, B\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
F\<lparr>[]\<^sub>\<circ>\<rparr> : A\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> B\<lparr>[]\<^sub>\<circ>\<rparr>
F\<lparr>1\<^sub>\<nat>\<rparr> : A\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> B\<lparr>1\<^sub>\<nat>\<rparr>
F\<lparr>2\<^sub>\<nat>\<rparr> : A\<lparr>2\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> B\<lparr>2\<^sub>\<nat>\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
F = [F\<lparr>[]\<^sub>\<circ>\<rparr>, F\<lparr>1\<^sub>\<nat>\<rparr>, F\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
A = [A\<lparr>[]\<^sub>\<circ>\<rparr>, A\<lparr>1\<^sub>\<nat>\<rparr>, A\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
B = [B\<lparr>[]\<^sub>\<circ>\<rparr>, B\<lparr>1\<^sub>\<nat>\<rparr>, B\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
F\<lparr>[]\<^sub>\<circ>\<rparr> : A\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> B\<lparr>[]\<^sub>\<circ>\<rparr>
F\<lparr>1\<^sub>\<nat>\<rparr> : A\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> B\<lparr>1\<^sub>\<nat>\<rparr>
F\<lparr>2\<^sub>\<nat>\<rparr> : A\<lparr>2\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> B\<lparr>2\<^sub>\<nat>\<rparr>

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
F = [F\<lparr>[]\<^sub>\<circ>\<rparr>, F\<lparr>1\<^sub>\<nat>\<rparr>, F\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
A = [A\<lparr>[]\<^sub>\<circ>\<rparr>, A\<lparr>1\<^sub>\<nat>\<rparr>, A\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
B = [B\<lparr>[]\<^sub>\<circ>\<rparr>, B\<lparr>1\<^sub>\<nat>\<rparr>, B\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
F\<lparr>[]\<^sub>\<circ>\<rparr> : A\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> B\<lparr>[]\<^sub>\<circ>\<rparr>
F\<lparr>1\<^sub>\<nat>\<rparr> : A\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> B\<lparr>1\<^sub>\<nat>\<rparr>
F\<lparr>2\<^sub>\<nat>\<rparr> : A\<lparr>2\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> B\<lparr>2\<^sub>\<nat>\<rparr>
\<lbrakk>F = [?f, ?f', ?f'']\<^sub>\<circ>; A = [?a, ?a', ?a'']\<^sub>\<circ>; B = [?b, ?b', ?b'']\<^sub>\<circ>; ?f : ?a \<mapsto>\<^bsub>\<AA>\<^esub> ?b; ?f' : ?a' \<mapsto>\<^bsub>\<BB>\<^esub> ?b'; ?f'' : ?a'' \<mapsto>\<^bsub>\<CC>\<^esub> ?b''\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_3_Dom_vsv: "vsv ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>)
[PROOF STEP]
unfolding dg_prod_3_def dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>3\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>3\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)
[PROOF STEP]
by simp


[STATEMENT]
lemma dg_prod_3_Dom_vdomain[dg_cs_simps]:
  "\<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>) = (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>) = (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dg_prod_3_def dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>3\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>3\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>) = (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>3\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>)
[PROOF STEP]
by simp


[STATEMENT]
lemma dg_prod_3_Dom_app[dg_prod_cs_simps]:
  assumes "[f, f', f'']\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>"
  shows "(\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>\<lparr>f, f', f''\<rparr>\<^sub>\<bullet> =
    [\<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Dom\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Dom\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Dom\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
[f, f', f'']\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
obtain A B where F: "[f, f', f'']\<^sub>\<circ> : A \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> B"
[PROOF STATE]
proof (prove)
using this:
[f, f', f'']\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>A B. [f, f', f'']\<^sub>\<circ> : A \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> B \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto intro: is_arrI)
[PROOF STATE]
proof (state)
this:
[f, f', f'']\<^sub>\<circ> : A \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> B

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Dom\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[f, f', f'']\<^sub>\<circ> : A \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> B
[PROOF STEP]
have Dom_F: "(\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>\<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = A"
[PROOF STATE]
proof (prove)
using this:
[f, f', f'']\<^sub>\<circ> : A \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> B

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = A
[PROOF STEP]
by (simp add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
(\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = A

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Dom\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ>
[PROOF STEP]
from F
[PROOF STATE]
proof (chain)
picking this:
[f, f', f'']\<^sub>\<circ> : A \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> B
[PROOF STEP]
obtain a a' a'' b b' b''
    where A_def: "A = [a, a', a'']\<^sub>\<circ>"
      and "B = [b, b', b'']\<^sub>\<circ>"
      and "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
      and "f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'"
      and "f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''"
[PROOF STATE]
proof (prove)
using this:
[f, f', f'']\<^sub>\<circ> : A \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> B

goal (1 subgoal):
 1. (\<And>a a' a'' b b' b''. \<lbrakk>A = [a, a', a'']\<^sub>\<circ>; B = [b, b', b'']\<^sub>\<circ>; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'; f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim dg_prod_3_is_arrE[OF \<AA> \<BB> \<CC>]) simp
[PROOF STATE]
proof (state)
this:
A = [a, a', a'']\<^sub>\<circ>
B = [b, b', b'']\<^sub>\<circ>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'
f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Dom\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = [a, a', a'']\<^sub>\<circ>
B = [b, b', b'']\<^sub>\<circ>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'
f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''
[PROOF STEP]
have Dom_f: "\<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a"
    and Dom_f': "\<BB>\<lparr>Dom\<rparr>\<lparr>f'\<rparr> = a'"
    and Dom_f'': "\<CC>\<lparr>Dom\<rparr>\<lparr>f''\<rparr> = a''"
[PROOF STATE]
proof (prove)
using this:
A = [a, a', a'']\<^sub>\<circ>
B = [b, b', b'']\<^sub>\<circ>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'
f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''

goal (1 subgoal):
 1. \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a &&& \<BB>\<lparr>Dom\<rparr>\<lparr>f'\<rparr> = a' &&& \<CC>\<lparr>Dom\<rparr>\<lparr>f''\<rparr> = a''
[PROOF STEP]
by (simp_all add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
\<BB>\<lparr>Dom\<rparr>\<lparr>f'\<rparr> = a'
\<CC>\<lparr>Dom\<rparr>\<lparr>f''\<rparr> = a''

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Dom\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Dom\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ>
[PROOF STEP]
unfolding Dom_F A_def Dom_f Dom_f' Dom_f''
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a, a', a'']\<^sub>\<circ> = [a, a', a'']\<^sub>\<circ>
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Dom\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_3_Dom_vrange:
  "\<R>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
proof(rule vsv.vsv_vrange_vsubset, unfold dg_cs_simps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
show "vsv ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>)
[PROOF STEP]
by (rule dg_prod_3_Dom_vsv)
[PROOF STATE]
proof (state)
this:
vsv ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
fix F
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
assume prems: "F \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (state)
this:
F \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
F \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
obtain f f' f'' where F_def: "F = [f, f', f'']\<^sub>\<circ>"
    and f: "f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>"
    and f': "f' \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
    and f'': "f'' \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
F \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>f f' f''. \<lbrakk>F = [f, f', f'']\<^sub>\<circ>; f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f' \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>; f'' \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim dg_prod_3_ArrE[OF \<AA> \<BB> \<CC>]) simp
[PROOF STATE]
proof (state)
this:
F = [f, f', f'']\<^sub>\<circ>
f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f' \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
f'' \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
from f f' f''
[PROOF STATE]
proof (chain)
picking this:
f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f' \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
f'' \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
obtain a a' a'' b b' b''
    where f: "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
      and f': "f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'"
      and f'': "f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''"
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f' \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
f'' \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>a b a' b' a'' b''. \<lbrakk>f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'; f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson is_arrI)
[PROOF STATE]
proof (state)
this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'
f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
from \<AA> \<BB> f f' f''
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'
f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''
[PROOF STEP]
show "(\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>\<lparr>F\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'
f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>\<lparr>F\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding F_def dg_prod_3_Dom_app[OF prems[unfolded F_def]]
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'
f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''

goal (1 subgoal):
 1. [\<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Dom\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros dg_prod_cs_intros)
[PROOF STATE]
proof (state)
this:
(\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Dom\<rparr>\<lparr>F\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_3_Cod_vsv: "vsv ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>)
[PROOF STEP]
unfolding dg_prod_3_def dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>3\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>3\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)
[PROOF STEP]
by simp


[STATEMENT]
lemma dg_prod_3_Cod_vdomain[dg_cs_simps]:
  "\<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>) = (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>) = (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dg_prod_3_def dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>3\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>3\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>) = (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>3\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>)
[PROOF STEP]
by simp


[STATEMENT]
lemma dg_prod_3_Cod_app[dg_prod_cs_simps]:
  assumes "[f, f', f'']\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>"
  shows
    "(\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>\<lparr>f, f', f''\<rparr>\<^sub>\<bullet> =
      [\<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Cod\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Cod\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Cod\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
[f, f', f'']\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
obtain A B where F: "[f, f', f'']\<^sub>\<circ> : A \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> B"
[PROOF STATE]
proof (prove)
using this:
[f, f', f'']\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>A B. [f, f', f'']\<^sub>\<circ> : A \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> B \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto intro: is_arrI)
[PROOF STATE]
proof (state)
this:
[f, f', f'']\<^sub>\<circ> : A \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> B

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Cod\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[f, f', f'']\<^sub>\<circ> : A \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> B
[PROOF STEP]
have Cod_F: "(\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>\<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = B"
[PROOF STATE]
proof (prove)
using this:
[f, f', f'']\<^sub>\<circ> : A \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> B

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = B
[PROOF STEP]
by (simp add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
(\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = B

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Cod\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ>
[PROOF STEP]
from F
[PROOF STATE]
proof (chain)
picking this:
[f, f', f'']\<^sub>\<circ> : A \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> B
[PROOF STEP]
obtain a a' a'' b b' b''
    where "A = [a, a', a'']\<^sub>\<circ>"
      and B_def: "B = [b, b', b'']\<^sub>\<circ>"
      and "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
      and "f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'"
      and "f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''"
[PROOF STATE]
proof (prove)
using this:
[f, f', f'']\<^sub>\<circ> : A \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> B

goal (1 subgoal):
 1. (\<And>a a' a'' b b' b''. \<lbrakk>A = [a, a', a'']\<^sub>\<circ>; B = [b, b', b'']\<^sub>\<circ>; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'; f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim dg_prod_3_is_arrE[OF \<AA> \<BB> \<CC>]) simp
[PROOF STATE]
proof (state)
this:
A = [a, a', a'']\<^sub>\<circ>
B = [b, b', b'']\<^sub>\<circ>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'
f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Cod\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = [a, a', a'']\<^sub>\<circ>
B = [b, b', b'']\<^sub>\<circ>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'
f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''
[PROOF STEP]
have Cod_f: "\<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b"
    and Cod_f': "\<BB>\<lparr>Cod\<rparr>\<lparr>f'\<rparr> = b'"
    and Cod_f'': "\<CC>\<lparr>Cod\<rparr>\<lparr>f''\<rparr> = b''"
[PROOF STATE]
proof (prove)
using this:
A = [a, a', a'']\<^sub>\<circ>
B = [b, b', b'']\<^sub>\<circ>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'
f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''

goal (1 subgoal):
 1. \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b &&& \<BB>\<lparr>Cod\<rparr>\<lparr>f'\<rparr> = b' &&& \<CC>\<lparr>Cod\<rparr>\<lparr>f''\<rparr> = b''
[PROOF STEP]
by (simp_all add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b
\<BB>\<lparr>Cod\<rparr>\<lparr>f'\<rparr> = b'
\<CC>\<lparr>Cod\<rparr>\<lparr>f''\<rparr> = b''

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Cod\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Cod\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ>
[PROOF STEP]
unfolding Cod_F B_def Cod_f Cod_f' Cod_f''
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [b, b', b'']\<^sub>\<circ> = [b, b', b'']\<^sub>\<circ>
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr> \<lparr>f, f', f''\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Cod\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_3_Cod_vrange:
  "\<R>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
proof(rule vsv.vsv_vrange_vsubset, unfold dg_cs_simps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
show "vsv ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>)
[PROOF STEP]
by (rule dg_prod_3_Cod_vsv)
[PROOF STATE]
proof (state)
this:
vsv ((\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
fix F
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
assume prems: "F \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (state)
this:
F \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
F \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
obtain f f' f'' where F_def: "F = [f, f', f'']\<^sub>\<circ>"
    and f: "f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>"
    and f': "f' \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
    and f'': "f'' \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
F \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>f f' f''. \<lbrakk>F = [f, f', f'']\<^sub>\<circ>; f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f' \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>; f'' \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim dg_prod_3_ArrE[OF \<AA> \<BB> \<CC>]) simp
[PROOF STATE]
proof (state)
this:
F = [f, f', f'']\<^sub>\<circ>
f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f' \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
f'' \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
from f f' f''
[PROOF STATE]
proof (chain)
picking this:
f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f' \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
f'' \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
obtain a a' a'' b b' b''
    where f: "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
      and f': "f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'"
      and f'': "f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''"
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f' \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
f'' \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>a b a' b' a'' b''. \<lbrakk>f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'; f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis is_arrI)
[PROOF STATE]
proof (state)
this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'
f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
from \<AA> \<BB> \<CC> f f' f''
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
digraph \<alpha> \<CC>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'
f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''
[PROOF STEP]
show
    "(\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>\<lparr>F\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
digraph \<alpha> \<CC>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'
f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>\<lparr>F\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding F_def dg_prod_3_Cod_app[OF prems[unfolded F_def]]
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
digraph \<alpha> \<CC>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'
f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''

goal (1 subgoal):
 1. [\<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f'\<rparr>, \<CC>\<lparr>Cod\<rparr>\<lparr>f''\<rparr>]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
by
      (
        cs_concl cs_shallow
          cs_simp: dg_cs_simps cs_intro: dg_cs_intros dg_prod_cs_intros
      )
[PROOF STATE]
proof (state)
this:
(\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Cod\<rparr>\<lparr>F\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [code]:
  "hashcode (set xs) = fold (plus o cube o hashcode) (remdups xs) (uint32_of_nat (length (remdups xs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hashcode (set xs) = fold ((+) \<circ> cube \<circ> hashcode) (remdups xs) (uint32_of_nat (length (remdups xs)))
[PROOF STEP]
by (simp add: fold_set_fold_remdups length_remdups_card_conv)


[STATEMENT]
lemma [code]:
  "hashcode (abs_ltln\<^sub>P \<phi>) = hashcode (min_dnf \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hashcode (abs_ltln\<^sub>P \<phi>) = hashcode (min_dnf \<phi>)
[PROOF STEP]
by simp


[STATEMENT]
lemma min_dnf_rep_abs[simp]:
  "min_dnf (Unf (rep_ltln\<^sub>Q (abs_ltln\<^sub>Q \<phi>))) = min_dnf (Unf \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_dnf (Unf (rep_ltln\<^sub>Q (abs_ltln\<^sub>Q \<phi>))) = min_dnf (Unf \<phi>)
[PROOF STEP]
using Quotient3_ltln\<^sub>Q ltl_prop_equiv_min_dnf ltl_prop_unfold_equiv_def rep_abs_rsp
[PROOF STATE]
proof (prove)
using this:
Quotient3 (\<sim>\<^sub>Q) abs_ltln\<^sub>Q rep_ltln\<^sub>Q
?\<phi> \<sim>\<^sub>P ?\<psi> = (min_dnf ?\<phi> = min_dnf ?\<psi>)
?\<phi> \<sim>\<^sub>Q ?\<psi> \<equiv> Unf ?\<phi> \<sim>\<^sub>P Unf ?\<psi>
\<lbrakk>Quotient3 ?R ?Abs ?Rep; ?R ?x1.0 ?x2.0\<rbrakk> \<Longrightarrow> ?R ?x1.0 (?Rep (?Abs ?x2.0))

goal (1 subgoal):
 1. min_dnf (Unf (rep_ltln\<^sub>Q (abs_ltln\<^sub>Q \<phi>))) = min_dnf (Unf \<phi>)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma [code]:
  "hashcode (abs_ltln\<^sub>Q \<phi>) = hashcode (min_dnf (Unf \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hashcode (abs_ltln\<^sub>Q \<phi>) = hashcode (min_dnf (Unf \<phi>))
[PROOF STEP]
by simp


[STATEMENT]
lemma linorder_finite_sup_selective:
  fixes f :: "'a::finite \<Rightarrow> 'b::linorder_stone_algebra_expansion"
  shows "\<exists>i . (\<Squnion>\<^sub>k f k) = f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. sup_monoid.sum f {k. True} = f i
[PROOF STEP]
apply (induct rule: comp_inf.one_sup_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<exists>ia. f i = f ia
 2. \<And>j I. \<lbrakk>j \<notin> I; \<exists>i. sup_monoid.sum f I = f i\<rbrakk> \<Longrightarrow> \<exists>i. f j \<squnion> sup_monoid.sum f I = f i
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j I. \<lbrakk>j \<notin> I; \<exists>i. sup_monoid.sum f I = f i\<rbrakk> \<Longrightarrow> \<exists>i. f j \<squnion> sup_monoid.sum f I = f i
[PROOF STEP]
using sup_selective
[PROOF STATE]
proof (prove)
using this:
?x \<squnion> ?y = ?x \<or> ?x \<squnion> ?y = ?y

goal (1 subgoal):
 1. \<And>j I. \<lbrakk>j \<notin> I; \<exists>i. sup_monoid.sum f I = f i\<rbrakk> \<Longrightarrow> \<exists>i. f j \<squnion> sup_monoid.sum f I = f i
[PROOF STEP]
by fastforce


[STATEMENT]
lemma linorder_top_finite_sup:
  fixes f :: "'a::finite \<Rightarrow> 'b::linorder_stone_algebra_expansion"
  assumes "\<forall>k . f k \<noteq> top"
    shows "(\<Squnion>\<^sub>k f k) \<noteq> top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum f {k. True} \<noteq> top
[PROOF STEP]
by (metis assms linorder_finite_sup_selective)


[STATEMENT]
lemma comp_top_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "(f \<odot> mtop) (i,j) = (\<Squnion>\<^sub>k f (i,k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<odot> mtop) (i, j) = sup_monoid.sum (\<lambda>k. f (i, k)) {k. True}
[PROOF STEP]
apply (unfold times_matrix_def top_matrix_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (i, j) of (i, j) \<Rightarrow> sup_monoid.sum (\<lambda>k. f (i, k) * top) {k. True}) = sup_monoid.sum (\<lambda>k. f (i, k)) {k. True}
[PROOF STEP]
by (metis (no_types, lifting) case_prod_conv comp_right_one one_def sup_monoid.sum.cong)


[STATEMENT]
lemma top_comp_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "(mtop \<odot> f) (i,j) = (\<Squnion>\<^sub>k f (k,j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mtop \<odot> f) (i, j) = sup_monoid.sum (\<lambda>k. f (k, j)) {k. True}
[PROOF STEP]
apply (unfold times_matrix_def top_matrix_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (i, j) of (i, j) \<Rightarrow> sup_monoid.sum (\<lambda>k. top * f (k, j)) {k. True}) = sup_monoid.sum (\<lambda>k. f (k, j)) {k. True}
[PROOF STEP]
by (metis (no_types, lifting) case_prod_conv comp_left_one one_def sup_monoid.sum.cong)


[STATEMENT]
lemma univalent_linorder_matrix_1:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_stone_relation_algebra.univalent f"
      and "f (i,j) \<noteq> bot"
      and "f (i,k) \<noteq> bot"
    shows "j = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j = k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j = k
[PROOF STEP]
have "(f\<^sup>t \<odot> f) (j,k) = (\<Squnion>\<^sub>l (f\<^sup>t) (j,l) * f (l,k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f\<^sup>t \<odot> f) (j, k) = sup_monoid.sum (\<lambda>l. (f\<^sup>t) (j, l) * f (l, k)) {l. True}
[PROOF STEP]
by (simp add: times_matrix_def)
[PROOF STATE]
proof (state)
this:
(f\<^sup>t \<odot> f) (j, k) = sup_monoid.sum (\<lambda>l. (f\<^sup>t) (j, l) * f (l, k)) {l. True}

goal (1 subgoal):
 1. j = k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(f\<^sup>t \<odot> f) (j, k) = sup_monoid.sum (\<lambda>l. (f\<^sup>t) (j, l) * f (l, k)) {l. True}

goal (1 subgoal):
 1. j = k
[PROOF STEP]
have "... = (\<Squnion>\<^sub>l (f (l,j))\<^sup>T * f (l,k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. (f\<^sup>t) (j, l) * f (l, k)) {l. True} = sup_monoid.sum (\<lambda>l. f (l, j)\<^sup>T * f (l, k)) {l. True}
[PROOF STEP]
by (simp add: conv_matrix_def)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. (f\<^sup>t) (j, l) * f (l, k)) {l. True} = sup_monoid.sum (\<lambda>l. f (l, j)\<^sup>T * f (l, k)) {l. True}

goal (1 subgoal):
 1. j = k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. (f\<^sup>t) (j, l) * f (l, k)) {l. True} = sup_monoid.sum (\<lambda>l. f (l, j)\<^sup>T * f (l, k)) {l. True}

goal (1 subgoal):
 1. j = k
[PROOF STEP]
have "... = (\<Squnion>\<^sub>l f (l,j) * f (l,k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. f (l, j)\<^sup>T * f (l, k)) {l. True} = sup_monoid.sum (\<lambda>l. f (l, j) * f (l, k)) {l. True}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. f (l, j)\<^sup>T * f (l, k)) {l. True} = sup_monoid.sum (\<lambda>l. f (l, j) * f (l, k)) {l. True}

goal (1 subgoal):
 1. j = k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. f (l, j)\<^sup>T * f (l, k)) {l. True} = sup_monoid.sum (\<lambda>l. f (l, j) * f (l, k)) {l. True}

goal (1 subgoal):
 1. j = k
[PROOF STEP]
have "... \<ge> f (i,j) * f (i,k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (i, j) * f (i, k) \<le> sup_monoid.sum (\<lambda>l. f (l, j) * f (l, k)) {l. True}
[PROOF STEP]
using comp_inf.ub_sum
[PROOF STATE]
proof (prove)
using this:
?f ?i \<le> sup_monoid.sum ?f {k. True}

goal (1 subgoal):
 1. f (i, j) * f (i, k) \<le> sup_monoid.sum (\<lambda>l. f (l, j) * f (l, k)) {l. True}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
f (i, j) * f (i, k) \<le> sup_monoid.sum (\<lambda>l. f (l, j) * f (l, k)) {l. True}

goal (1 subgoal):
 1. j = k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f (i, j) * f (i, k) \<le> (f\<^sup>t \<odot> f) (j, k)
[PROOF STEP]
have "(f\<^sup>t \<odot> f) (j,k) \<noteq> bot"
[PROOF STATE]
proof (prove)
using this:
f (i, j) * f (i, k) \<le> (f\<^sup>t \<odot> f) (j, k)

goal (1 subgoal):
 1. (f\<^sup>t \<odot> f) (j, k) \<noteq> bot
[PROOF STEP]
using assms(2,3) bot.extremum_uniqueI times_dense
[PROOF STATE]
proof (prove)
using this:
f (i, j) * f (i, k) \<le> (f\<^sup>t \<odot> f) (j, k)
f (i, j) \<noteq> bot
f (i, k) \<noteq> bot
?a \<le> bot \<Longrightarrow> ?a = bot
\<lbrakk>?x \<noteq> bot; ?y \<noteq> bot\<rbrakk> \<Longrightarrow> ?x * ?y \<noteq> bot

goal (1 subgoal):
 1. (f\<^sup>t \<odot> f) (j, k) \<noteq> bot
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(f\<^sup>t \<odot> f) (j, k) \<noteq> bot

goal (1 subgoal):
 1. j = k
[PROOF STEP]
hence "mone (j,k) \<noteq> (bot::'b)"
[PROOF STATE]
proof (prove)
using this:
(f\<^sup>t \<odot> f) (j, k) \<noteq> bot

goal (1 subgoal):
 1. mone (j, k) \<noteq> bot
[PROOF STEP]
by (metis assms(1) bot.extremum_uniqueI less_eq_matrix_def)
[PROOF STATE]
proof (state)
this:
mone (j, k) \<noteq> bot

goal (1 subgoal):
 1. j = k
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mone (j, k) \<noteq> bot

goal (1 subgoal):
 1. j = k
[PROOF STEP]
by (metis (mono_tags, lifting) case_prod_conv one_matrix_def)
[PROOF STATE]
proof (state)
this:
j = k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma univalent_linorder_matrix_2:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "\<forall>i j k . f (i,j) \<noteq> bot \<and> f (i,k) \<noteq> bot \<longrightarrow> j = k"
    shows "matrix_stone_relation_algebra.univalent f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.univalent f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.univalent f
[PROOF STEP]
show "f\<^sup>t \<odot> f \<preceq> mone"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.univalent f
[PROOF STEP]
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e a b. (f\<^sup>t \<odot> f) (a, b) \<le> mone (a, b)
[PROOF STEP]
fix j k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e a b. (f\<^sup>t \<odot> f) (a, b) \<le> mone (a, b)
[PROOF STEP]
show "(f\<^sup>t \<odot> f) (j,k) \<le> mone (j,k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f\<^sup>t \<odot> f) (j, k) \<le> mone (j, k)
[PROOF STEP]
proof (cases "j = k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j = k \<Longrightarrow> (f\<^sup>t \<odot> f) (j, k) \<le> mone (j, k)
 2. j \<noteq> k \<Longrightarrow> (f\<^sup>t \<odot> f) (j, k) \<le> mone (j, k)
[PROOF STEP]
assume "j = k"
[PROOF STATE]
proof (state)
this:
j = k

goal (2 subgoals):
 1. j = k \<Longrightarrow> (f\<^sup>t \<odot> f) (j, k) \<le> mone (j, k)
 2. j \<noteq> k \<Longrightarrow> (f\<^sup>t \<odot> f) (j, k) \<le> mone (j, k)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
j = k

goal (1 subgoal):
 1. (f\<^sup>t \<odot> f) (j, k) \<le> mone (j, k)
[PROOF STEP]
by (simp add: one_matrix_def)
[PROOF STATE]
proof (state)
this:
(f\<^sup>t \<odot> f) (j, k) \<le> mone (j, k)

goal (1 subgoal):
 1. j \<noteq> k \<Longrightarrow> (f\<^sup>t \<odot> f) (j, k) \<le> mone (j, k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j \<noteq> k \<Longrightarrow> (f\<^sup>t \<odot> f) (j, k) \<le> mone (j, k)
[PROOF STEP]
assume "j \<noteq> k"
[PROOF STATE]
proof (state)
this:
j \<noteq> k

goal (1 subgoal):
 1. j \<noteq> k \<Longrightarrow> (f\<^sup>t \<odot> f) (j, k) \<le> mone (j, k)
[PROOF STEP]
hence "(\<Squnion>\<^sub>i f (i,j) * f (i,k)) = bot"
[PROOF STATE]
proof (prove)
using this:
j \<noteq> k

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>i. f (i, j) * f (i, k)) {i. True} = bot
[PROOF STEP]
by (metis (no_types, lifting) assms semiring.mult_not_zero sup_monoid.sum.neutral)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>i. f (i, j) * f (i, k)) {i. True} = bot

goal (1 subgoal):
 1. j \<noteq> k \<Longrightarrow> (f\<^sup>t \<odot> f) (j, k) \<le> mone (j, k)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sup_monoid.sum (\<lambda>i. f (i, j) * f (i, k)) {i. True} = bot

goal (1 subgoal):
 1. (f\<^sup>t \<odot> f) (j, k) \<le> mone (j, k)
[PROOF STEP]
by (simp add: times_matrix_def conv_matrix_def)
[PROOF STATE]
proof (state)
this:
(f\<^sup>t \<odot> f) (j, k) \<le> mone (j, k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(f\<^sup>t \<odot> f) (j, k) \<le> mone (j, k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
matrix_stone_relation_algebra.univalent f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma univalent_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.univalent f \<longleftrightarrow> (\<forall>i j k . f (i,j) \<noteq> bot \<and> f (i,k) \<noteq> bot \<longrightarrow> j = k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.univalent f = (\<forall>i j k. f (i, j) \<noteq> bot \<and> f (i, k) \<noteq> bot \<longrightarrow> j = k)
[PROOF STEP]
using univalent_linorder_matrix_1 univalent_linorder_matrix_2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>matrix_stone_relation_algebra.univalent ?f; ?f (?i, ?j) \<noteq> bot; ?f (?i, ?k) \<noteq> bot\<rbrakk> \<Longrightarrow> ?j = ?k
\<forall>i j k. ?f (i, j) \<noteq> bot \<and> ?f (i, k) \<noteq> bot \<longrightarrow> j = k \<Longrightarrow> matrix_stone_relation_algebra.univalent ?f

goal (1 subgoal):
 1. matrix_stone_relation_algebra.univalent f = (\<forall>i j k. f (i, j) \<noteq> bot \<and> f (i, k) \<noteq> bot \<longrightarrow> j = k)
[PROOF STEP]
by auto


[STATEMENT]
lemma injective_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.injective f \<longleftrightarrow> (\<forall>i j k . f (j,i) \<noteq> bot \<and> f (k,i) \<noteq> bot \<longrightarrow> j = k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.injective f = (\<forall>i j k. f (j, i) \<noteq> bot \<and> f (k, i) \<noteq> bot \<longrightarrow> j = k)
[PROOF STEP]
by (unfold matrix_stone_relation_algebra.injective_conv_univalent univalent_linorder_matrix) (simp add: conv_matrix_def)


[STATEMENT]
lemma total_linorder_matrix_1:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_stone_relation_algebra.total_var f"
    shows "\<exists>j . f (i,j) = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. f (i, j) = top
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j. f (i, j) = top
[PROOF STEP]
have "mone (i,i) \<le> (f \<odot> f\<^sup>t) (i,i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mone (i, i) \<le> (f \<odot> f\<^sup>t) (i, i)
[PROOF STEP]
using assms less_eq_matrix_def
[PROOF STATE]
proof (prove)
using this:
matrix_stone_relation_algebra.total_var f
(?f \<preceq> ?g) = (\<forall>e. ?f e \<le> ?g e)

goal (1 subgoal):
 1. mone (i, i) \<le> (f \<odot> f\<^sup>t) (i, i)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mone (i, i) \<le> (f \<odot> f\<^sup>t) (i, i)

goal (1 subgoal):
 1. \<exists>j. f (i, j) = top
[PROOF STEP]
hence "top = (f \<odot> f\<^sup>t) (i,i)"
[PROOF STATE]
proof (prove)
using this:
mone (i, i) \<le> (f \<odot> f\<^sup>t) (i, i)

goal (1 subgoal):
 1. top = (f \<odot> f\<^sup>t) (i, i)
[PROOF STEP]
by (simp add: one_matrix_def top.extremum_unique)
[PROOF STATE]
proof (state)
this:
top = (f \<odot> f\<^sup>t) (i, i)

goal (1 subgoal):
 1. \<exists>j. f (i, j) = top
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
top = (f \<odot> f\<^sup>t) (i, i)

goal (1 subgoal):
 1. \<exists>j. f (i, j) = top
[PROOF STEP]
have "... = (\<Squnion>\<^sub>j f (i,j) * (f\<^sup>t) (j,i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<odot> f\<^sup>t) (i, i) = sup_monoid.sum (\<lambda>j. f (i, j) * (f\<^sup>t) (j, i)) {j. True}
[PROOF STEP]
by (simp add: times_matrix_def)
[PROOF STATE]
proof (state)
this:
(f \<odot> f\<^sup>t) (i, i) = sup_monoid.sum (\<lambda>j. f (i, j) * (f\<^sup>t) (j, i)) {j. True}

goal (1 subgoal):
 1. \<exists>j. f (i, j) = top
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(f \<odot> f\<^sup>t) (i, i) = sup_monoid.sum (\<lambda>j. f (i, j) * (f\<^sup>t) (j, i)) {j. True}

goal (1 subgoal):
 1. \<exists>j. f (i, j) = top
[PROOF STEP]
have "... = (\<Squnion>\<^sub>j f (i,j) * f (i,j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>j. f (i, j) * (f\<^sup>t) (j, i)) {j. True} = sup_monoid.sum (\<lambda>j. f (i, j) * f (i, j)) {j. True}
[PROOF STEP]
by (simp add: conv_matrix_def)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>j. f (i, j) * (f\<^sup>t) (j, i)) {j. True} = sup_monoid.sum (\<lambda>j. f (i, j) * f (i, j)) {j. True}

goal (1 subgoal):
 1. \<exists>j. f (i, j) = top
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>j. f (i, j) * (f\<^sup>t) (j, i)) {j. True} = sup_monoid.sum (\<lambda>j. f (i, j) * f (i, j)) {j. True}

goal (1 subgoal):
 1. \<exists>j. f (i, j) = top
[PROOF STEP]
have "... = (\<Squnion>\<^sub>j f (i,j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>j. f (i, j) * f (i, j)) {j. True} = sup_monoid.sum (\<lambda>j. f (i, j)) {j. True}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>j. f (i, j) * f (i, j)) {j. True} = sup_monoid.sum (\<lambda>j. f (i, j)) {j. True}

goal (1 subgoal):
 1. \<exists>j. f (i, j) = top
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
top = sup_monoid.sum (\<lambda>j. f (i, j)) {j. True}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
top = sup_monoid.sum (\<lambda>j. f (i, j)) {j. True}

goal (1 subgoal):
 1. \<exists>j. f (i, j) = top
[PROOF STEP]
by (metis linorder_top_finite_sup)
[PROOF STATE]
proof (state)
this:
\<exists>j. f (i, j) = top

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma total_linorder_matrix_2:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "\<forall>i . \<exists>j . f (i,j) = top"
    shows "matrix_stone_relation_algebra.total_var f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.total_var f
[PROOF STEP]
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e a b. mone (a, b) \<le> (f \<odot> f\<^sup>t) (a, b)
[PROOF STEP]
fix j k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e a b. mone (a, b) \<le> (f \<odot> f\<^sup>t) (a, b)
[PROOF STEP]
show "mone (j,k) \<le> (f \<odot> f\<^sup>t) (j,k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)
[PROOF STEP]
proof (cases "j = k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j = k \<Longrightarrow> mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)
 2. j \<noteq> k \<Longrightarrow> mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)
[PROOF STEP]
assume "j = k"
[PROOF STATE]
proof (state)
this:
j = k

goal (2 subgoals):
 1. j = k \<Longrightarrow> mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)
 2. j \<noteq> k \<Longrightarrow> mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)
[PROOF STEP]
hence "(\<Squnion>\<^sub>i f (j,i) * (f\<^sup>t) (i,k)) = (\<Squnion>\<^sub>i f (j,i))"
[PROOF STATE]
proof (prove)
using this:
j = k

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>i. f (j, i) * (f\<^sup>t) (i, k)) {i. True} = sup_monoid.sum (\<lambda>i. f (j, i)) {i. True}
[PROOF STEP]
by (simp add: conv_matrix_def)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>i. f (j, i) * (f\<^sup>t) (i, k)) {i. True} = sup_monoid.sum (\<lambda>i. f (j, i)) {i. True}

goal (2 subgoals):
 1. j = k \<Longrightarrow> mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)
 2. j \<noteq> k \<Longrightarrow> mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>i. f (j, i) * (f\<^sup>t) (i, k)) {i. True} = sup_monoid.sum (\<lambda>i. f (j, i)) {i. True}

goal (2 subgoals):
 1. j = k \<Longrightarrow> mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)
 2. j \<noteq> k \<Longrightarrow> mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)
[PROOF STEP]
have "... = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>i. f (j, i)) {i. True} = top
[PROOF STEP]
by (metis (no_types) assms comp_inf.ub_sum sup.absorb2 sup_top_left)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>i. f (j, i)) {i. True} = top

goal (2 subgoals):
 1. j = k \<Longrightarrow> mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)
 2. j \<noteq> k \<Longrightarrow> mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sup_monoid.sum (\<lambda>i. f (j, i) * (f\<^sup>t) (i, k)) {i. True} = top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sup_monoid.sum (\<lambda>i. f (j, i) * (f\<^sup>t) (i, k)) {i. True} = top

goal (1 subgoal):
 1. mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)
[PROOF STEP]
by (simp add: times_matrix_def)
[PROOF STATE]
proof (state)
this:
mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)

goal (1 subgoal):
 1. j \<noteq> k \<Longrightarrow> mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j \<noteq> k \<Longrightarrow> mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)
[PROOF STEP]
assume "j \<noteq> k"
[PROOF STATE]
proof (state)
this:
j \<noteq> k

goal (1 subgoal):
 1. j \<noteq> k \<Longrightarrow> mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
j \<noteq> k

goal (1 subgoal):
 1. mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)
[PROOF STEP]
by (simp add: one_matrix_def)
[PROOF STATE]
proof (state)
this:
mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mone (j, k) \<le> (f \<odot> f\<^sup>t) (j, k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma total_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_bounded_idempotent_semiring.total f \<longleftrightarrow> (\<forall>i . \<exists>j . f (i,j) = top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_bounded_idempotent_semiring.total f = (\<forall>i. \<exists>j. f (i, j) = top)
[PROOF STEP]
using total_linorder_matrix_1 total_linorder_matrix_2 matrix_stone_relation_algebra.total_var
[PROOF STATE]
proof (prove)
using this:
matrix_stone_relation_algebra.total_var ?f \<Longrightarrow> \<exists>j. ?f (?i, j) = top
\<forall>i. \<exists>j. ?f (i, j) = top \<Longrightarrow> matrix_stone_relation_algebra.total_var ?f
matrix_bounded_idempotent_semiring.total ?x = matrix_stone_relation_algebra.total_var ?x

goal (1 subgoal):
 1. matrix_bounded_idempotent_semiring.total f = (\<forall>i. \<exists>j. f (i, j) = top)
[PROOF STEP]
by auto


[STATEMENT]
lemma surjective_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_bounded_idempotent_semiring.surjective f \<longleftrightarrow> (\<forall>j . \<exists>i . f (i,j) = top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_bounded_idempotent_semiring.surjective f = (\<forall>j. \<exists>i. f (i, j) = top)
[PROOF STEP]
by (unfold matrix_stone_relation_algebra.surjective_conv_total total_linorder_matrix) (simp add: conv_matrix_def)


[STATEMENT]
lemma mapping_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.mapping f \<longleftrightarrow> (\<forall>i . \<exists>j . f (i,j) = top \<and> (\<forall>k . j \<noteq> k \<longrightarrow> f (i,k) = bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.mapping f = (\<forall>i. \<exists>j. f (i, j) = top \<and> (\<forall>k. j \<noteq> k \<longrightarrow> f (i, k) = bot))
[PROOF STEP]
by (unfold total_linorder_matrix univalent_linorder_matrix) (metis (mono_tags, opaque_lifting) comp_inf.mult_1_right comp_inf.mult_right_zero)


[STATEMENT]
lemma mapping_linorder_matrix_unique:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.mapping f \<longleftrightarrow> (\<forall>i . \<exists>!j . f (i,j) = top \<and> (\<forall>k . j \<noteq> k \<longrightarrow> f (i,k) = bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.mapping f = (\<forall>i. \<exists>!j. f (i, j) = top \<and> (\<forall>k. j \<noteq> k \<longrightarrow> f (i, k) = bot))
[PROOF STEP]
apply (unfold mapping_linorder_matrix)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i. \<exists>j. f (i, j) = top \<and> (\<forall>k. j \<noteq> k \<longrightarrow> f (i, k) = bot)) = (\<forall>i. \<exists>!j. f (i, j) = top \<and> (\<forall>k. j \<noteq> k \<longrightarrow> f (i, k) = bot))
[PROOF STEP]
using bot_not_top
[PROOF STATE]
proof (prove)
using this:
bot \<noteq> top

goal (1 subgoal):
 1. (\<forall>i. \<exists>j. f (i, j) = top \<and> (\<forall>k. j \<noteq> k \<longrightarrow> f (i, k) = bot)) = (\<forall>i. \<exists>!j. f (i, j) = top \<and> (\<forall>k. j \<noteq> k \<longrightarrow> f (i, k) = bot))
[PROOF STEP]
by auto


[STATEMENT]
lemma bijective_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.bijective f \<longleftrightarrow> (\<forall>j . \<exists>i . f (i,j) = top \<and> (\<forall>k . i \<noteq> k \<longrightarrow> f (k,j) = bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.bijective f = (\<forall>j. \<exists>i. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
by (unfold matrix_stone_relation_algebra.bijective_conv_mapping mapping_linorder_matrix) (simp add: conv_matrix_def)


[STATEMENT]
lemma bijective_linorder_matrix_unique:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.bijective f \<longleftrightarrow> (\<forall>j . \<exists>!i . f (i,j) = top \<and> (\<forall>k . i \<noteq> k \<longrightarrow> f (k,j) = bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.bijective f = (\<forall>j. \<exists>!i. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
by (unfold matrix_stone_relation_algebra.bijective_conv_mapping mapping_linorder_matrix_unique) (simp add: conv_matrix_def)


[STATEMENT]
lemma pp_total_linorder_matrix_1:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  assumes "\<ominus>(f \<odot> mtop) = mbot"
    shows "\<exists>j . f (i,j) \<noteq> bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. f (i, j) \<noteq> bot
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j. f (i, j) \<noteq> bot
[PROOF STEP]
have "\<not>(\<exists>j . f (i,j) \<noteq> bot) \<Longrightarrow> \<ominus>(f \<odot> mtop) \<noteq> mbot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>j. f (i, j) \<noteq> bot \<Longrightarrow> \<ominus> (f \<odot> mtop) \<noteq> mbot
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>j. f (i, j) \<noteq> bot \<Longrightarrow> \<ominus> (f \<odot> mtop) \<noteq> mbot
[PROOF STEP]
assume "\<not>(\<exists>j . f (i,j) \<noteq> bot)"
[PROOF STATE]
proof (state)
this:
\<nexists>j. f (i, j) \<noteq> bot

goal (1 subgoal):
 1. \<nexists>j. f (i, j) \<noteq> bot \<Longrightarrow> \<ominus> (f \<odot> mtop) \<noteq> mbot
[PROOF STEP]
hence "top = -(f \<odot> mtop) (i,i)"
[PROOF STATE]
proof (prove)
using this:
\<nexists>j. f (i, j) \<noteq> bot

goal (1 subgoal):
 1. top = - (f \<odot> mtop) (i, i)
[PROOF STEP]
by (simp add: comp_top_linorder_matrix linorder_finite_sup_selective)
[PROOF STATE]
proof (state)
this:
top = - (f \<odot> mtop) (i, i)

goal (1 subgoal):
 1. \<nexists>j. f (i, j) \<noteq> bot \<Longrightarrow> \<ominus> (f \<odot> mtop) \<noteq> mbot
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
top = - (f \<odot> mtop) (i, i)

goal (1 subgoal):
 1. \<nexists>j. f (i, j) \<noteq> bot \<Longrightarrow> \<ominus> (f \<odot> mtop) \<noteq> mbot
[PROOF STEP]
have "... = (\<ominus>(f \<odot> mtop)) (i,i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (f \<odot> mtop) (i, i) = (\<ominus> (f \<odot> mtop)) (i, i)
[PROOF STEP]
by (simp add: uminus_matrix_def)
[PROOF STATE]
proof (state)
this:
- (f \<odot> mtop) (i, i) = (\<ominus> (f \<odot> mtop)) (i, i)

goal (1 subgoal):
 1. \<nexists>j. f (i, j) \<noteq> bot \<Longrightarrow> \<ominus> (f \<odot> mtop) \<noteq> mbot
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
top = (\<ominus> (f \<odot> mtop)) (i, i)
[PROOF STEP]
show "\<ominus>(f \<odot> mtop) \<noteq> mbot"
[PROOF STATE]
proof (prove)
using this:
top = (\<ominus> (f \<odot> mtop)) (i, i)

goal (1 subgoal):
 1. \<ominus> (f \<odot> mtop) \<noteq> mbot
[PROOF STEP]
by (metis bot_matrix_def bot_not_top)
[PROOF STATE]
proof (state)
this:
\<ominus> (f \<odot> mtop) \<noteq> mbot

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<nexists>j. f (i, j) \<noteq> bot \<Longrightarrow> \<ominus> (f \<odot> mtop) \<noteq> mbot

goal (1 subgoal):
 1. \<exists>j. f (i, j) \<noteq> bot
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<nexists>j. f (i, j) \<noteq> bot \<Longrightarrow> \<ominus> (f \<odot> mtop) \<noteq> mbot

goal (1 subgoal):
 1. \<exists>j. f (i, j) \<noteq> bot
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<nexists>j. f (i, j) \<noteq> bot \<Longrightarrow> \<ominus> (f \<odot> mtop) \<noteq> mbot
matrix_p_algebra.dense (f \<odot> mtop)

goal (1 subgoal):
 1. \<exists>j. f (i, j) \<noteq> bot
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>j. f (i, j) \<noteq> bot

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pp_total_linorder_matrix_2:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "\<forall>i . \<exists>j . f (i,j) \<noteq> bot"
    shows "\<ominus>(f \<odot> mtop) = mbot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_p_algebra.dense (f \<odot> mtop)
[PROOF STEP]
proof (rule ext, rule prod_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. (\<ominus> (f \<odot> mtop)) (a, b) = mbot (a, b)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. (\<ominus> (f \<odot> mtop)) (a, b) = mbot (a, b)
[PROOF STEP]
have "(\<ominus>(f \<odot> mtop)) (i,j) = -(\<Squnion>\<^sub>k f (i,k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<ominus> (f \<odot> mtop)) (i, j) = - sup_monoid.sum (\<lambda>k. f (i, k)) {k. True}
[PROOF STEP]
by (simp add: comp_top_linorder_matrix uminus_matrix_def)
[PROOF STATE]
proof (state)
this:
(\<ominus> (f \<odot> mtop)) (i, j) = - sup_monoid.sum (\<lambda>k. f (i, k)) {k. True}

goal (1 subgoal):
 1. \<And>x a b. (\<ominus> (f \<odot> mtop)) (a, b) = mbot (a, b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<ominus> (f \<odot> mtop)) (i, j) = - sup_monoid.sum (\<lambda>k. f (i, k)) {k. True}

goal (1 subgoal):
 1. \<And>x a b. (\<ominus> (f \<odot> mtop)) (a, b) = mbot (a, b)
[PROOF STEP]
have "... = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dense (sup_monoid.sum (\<lambda>k. f (i, k)) {k. True})
[PROOF STEP]
by (metis antisym assms bot.extremum comp_inf.ub_sum uminus_def)
[PROOF STATE]
proof (state)
this:
dense (sup_monoid.sum (\<lambda>k. f (i, k)) {k. True})

goal (1 subgoal):
 1. \<And>x a b. (\<ominus> (f \<odot> mtop)) (a, b) = mbot (a, b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<ominus> (f \<odot> mtop)) (i, j) = bot
[PROOF STEP]
show "(\<ominus>(f \<odot> mtop)) (i,j) = mbot (i,j)"
[PROOF STATE]
proof (prove)
using this:
(\<ominus> (f \<odot> mtop)) (i, j) = bot

goal (1 subgoal):
 1. (\<ominus> (f \<odot> mtop)) (i, j) = mbot (i, j)
[PROOF STEP]
by (simp add: bot_matrix_def)
[PROOF STATE]
proof (state)
this:
(\<ominus> (f \<odot> mtop)) (i, j) = mbot (i, j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pp_total_linorder_matrix_3:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "\<ominus>(f \<odot> mtop) = mbot \<longleftrightarrow> (\<forall>i . \<exists>j . f (i,j) \<noteq> bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_p_algebra.dense (f \<odot> mtop) = (\<forall>i. \<exists>j. f (i, j) \<noteq> bot)
[PROOF STEP]
using pp_total_linorder_matrix_1 pp_total_linorder_matrix_2
[PROOF STATE]
proof (prove)
using this:
matrix_p_algebra.dense (?f \<odot> mtop) \<Longrightarrow> \<exists>j. ?f (?i, j) \<noteq> bot
\<forall>i. \<exists>j. ?f (i, j) \<noteq> bot \<Longrightarrow> matrix_p_algebra.dense (?f \<odot> mtop)

goal (1 subgoal):
 1. matrix_p_algebra.dense (f \<odot> mtop) = (\<forall>i. \<exists>j. f (i, j) \<noteq> bot)
[PROOF STEP]
by auto


[STATEMENT]
lemma pp_total_linorder_matrix:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_bounded_idempotent_semiring.total (\<ominus>\<ominus>f) \<longleftrightarrow> (\<forall>i . \<exists>j . f (i,j) \<noteq> bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_bounded_idempotent_semiring.total (\<ominus> \<ominus> f) = (\<forall>i. \<exists>j. f (i, j) \<noteq> bot)
[PROOF STEP]
using matrix_stone_relation_algebra.pp_total pp_total_linorder_matrix_1 pp_total_linorder_matrix_2
[PROOF STATE]
proof (prove)
using this:
matrix_bounded_idempotent_semiring.total (\<ominus> \<ominus> ?x) = matrix_p_algebra.dense (?x \<odot> mtop)
matrix_p_algebra.dense (?f \<odot> mtop) \<Longrightarrow> \<exists>j. ?f (?i, j) \<noteq> bot
\<forall>i. \<exists>j. ?f (i, j) \<noteq> bot \<Longrightarrow> matrix_p_algebra.dense (?f \<odot> mtop)

goal (1 subgoal):
 1. matrix_bounded_idempotent_semiring.total (\<ominus> \<ominus> f) = (\<forall>i. \<exists>j. f (i, j) \<noteq> bot)
[PROOF STEP]
by auto


[STATEMENT]
lemma pp_mapping_linorder_matrix:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.pp_mapping f \<longleftrightarrow> (\<forall>i . \<exists>j . f (i,j) \<noteq> bot \<and> (\<forall>k . j \<noteq> k \<longrightarrow> f (i,k) = bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.pp_mapping f = (\<forall>i. \<exists>j. f (i, j) \<noteq> bot \<and> (\<forall>k. j \<noteq> k \<longrightarrow> f (i, k) = bot))
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) pp_total_linorder_matrix univalent_linorder_matrix_1 univalent_linorder_matrix_2)


[STATEMENT]
lemma pp_mapping_linorder_matrix_unique:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.pp_mapping f \<longleftrightarrow> (\<forall>i . \<exists>!j . f (i,j) \<noteq> bot \<and> (\<forall>k . j \<noteq> k \<longrightarrow> f (i,k) = bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.pp_mapping f = (\<forall>i. \<exists>!j. f (i, j) \<noteq> bot \<and> (\<forall>k. j \<noteq> k \<longrightarrow> f (i, k) = bot))
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. matrix_stone_relation_algebra.pp_mapping f \<Longrightarrow> \<forall>i. \<exists>!j. f (i, j) \<noteq> bot \<and> (\<forall>k. j \<noteq> k \<longrightarrow> f (i, k) = bot)
 2. \<forall>i. \<exists>!j. f (i, j) \<noteq> bot \<and> (\<forall>k. j \<noteq> k \<longrightarrow> f (i, k) = bot) \<Longrightarrow> matrix_stone_relation_algebra.pp_mapping f
[PROOF STEP]
using pp_mapping_linorder_matrix
[PROOF STATE]
proof (prove)
using this:
matrix_stone_relation_algebra.pp_mapping ?f = (\<forall>i. \<exists>j. ?f (i, j) \<noteq> bot \<and> (\<forall>k. j \<noteq> k \<longrightarrow> ?f (i, k) = bot))

goal (2 subgoals):
 1. matrix_stone_relation_algebra.pp_mapping f \<Longrightarrow> \<forall>i. \<exists>!j. f (i, j) \<noteq> bot \<and> (\<forall>k. j \<noteq> k \<longrightarrow> f (i, k) = bot)
 2. \<forall>i. \<exists>!j. f (i, j) \<noteq> bot \<and> (\<forall>k. j \<noteq> k \<longrightarrow> f (i, k) = bot) \<Longrightarrow> matrix_stone_relation_algebra.pp_mapping f
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<exists>!j. f (i, j) \<noteq> bot \<and> (\<forall>k. j \<noteq> k \<longrightarrow> f (i, k) = bot) \<Longrightarrow> matrix_stone_relation_algebra.pp_mapping f
[PROOF STEP]
by (metis pp_total_linorder_matrix univalent_linorder_matrix)


[STATEMENT]
lemma pp_surjective_linorder_matrix_1:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "\<ominus>(mtop \<odot> f) = mbot \<longleftrightarrow> (\<forall>j . \<exists>i . f (i,j) \<noteq> bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_p_algebra.dense (mtop \<odot> f) = (\<forall>j. \<exists>i. f (i, j) \<noteq> bot)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_p_algebra.dense (mtop \<odot> f) = (\<forall>j. \<exists>i. f (i, j) \<noteq> bot)
[PROOF STEP]
have "\<ominus>(mtop \<odot> f) = mbot \<longleftrightarrow> (\<ominus>(mtop \<odot> f))\<^sup>t = mbot\<^sup>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_p_algebra.dense (mtop \<odot> f) = ((\<ominus> (mtop \<odot> f))\<^sup>t = mbot\<^sup>t)
[PROOF STEP]
by (metis matrix_stone_relation_algebra.conv_involutive)
[PROOF STATE]
proof (state)
this:
matrix_p_algebra.dense (mtop \<odot> f) = ((\<ominus> (mtop \<odot> f))\<^sup>t = mbot\<^sup>t)

goal (1 subgoal):
 1. matrix_p_algebra.dense (mtop \<odot> f) = (\<forall>j. \<exists>i. f (i, j) \<noteq> bot)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
matrix_p_algebra.dense (mtop \<odot> f) = ((\<ominus> (mtop \<odot> f))\<^sup>t = mbot\<^sup>t)

goal (1 subgoal):
 1. matrix_p_algebra.dense (mtop \<odot> f) = (\<forall>j. \<exists>i. f (i, j) \<noteq> bot)
[PROOF STEP]
have "... \<longleftrightarrow> \<ominus>(f\<^sup>t \<odot> mtop) = mbot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<ominus> (mtop \<odot> f))\<^sup>t = mbot\<^sup>t) = matrix_p_algebra.dense (f\<^sup>t \<odot> mtop)
[PROOF STEP]
by (simp add: matrix_stone_relation_algebra.conv_complement matrix_stone_relation_algebra.conv_dist_comp)
[PROOF STATE]
proof (state)
this:
((\<ominus> (mtop \<odot> f))\<^sup>t = mbot\<^sup>t) = matrix_p_algebra.dense (f\<^sup>t \<odot> mtop)

goal (1 subgoal):
 1. matrix_p_algebra.dense (mtop \<odot> f) = (\<forall>j. \<exists>i. f (i, j) \<noteq> bot)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<ominus> (mtop \<odot> f))\<^sup>t = mbot\<^sup>t) = matrix_p_algebra.dense (f\<^sup>t \<odot> mtop)

goal (1 subgoal):
 1. matrix_p_algebra.dense (mtop \<odot> f) = (\<forall>j. \<exists>i. f (i, j) \<noteq> bot)
[PROOF STEP]
have "... \<longleftrightarrow> (\<forall>i . \<exists>j . (f\<^sup>t) (i,j) \<noteq> bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_p_algebra.dense (f\<^sup>t \<odot> mtop) = (\<forall>i. \<exists>j. (f\<^sup>t) (i, j) \<noteq> bot)
[PROOF STEP]
using pp_total_linorder_matrix_3
[PROOF STATE]
proof (prove)
using this:
matrix_p_algebra.dense (?f \<odot> mtop) = (\<forall>i. \<exists>j. ?f (i, j) \<noteq> bot)

goal (1 subgoal):
 1. matrix_p_algebra.dense (f\<^sup>t \<odot> mtop) = (\<forall>i. \<exists>j. (f\<^sup>t) (i, j) \<noteq> bot)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_p_algebra.dense (f\<^sup>t \<odot> mtop) = (\<forall>i. \<exists>j. (f\<^sup>t) (i, j) \<noteq> bot)

goal (1 subgoal):
 1. matrix_p_algebra.dense (mtop \<odot> f) = (\<forall>j. \<exists>i. f (i, j) \<noteq> bot)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
matrix_p_algebra.dense (f\<^sup>t \<odot> mtop) = (\<forall>i. \<exists>j. (f\<^sup>t) (i, j) \<noteq> bot)

goal (1 subgoal):
 1. matrix_p_algebra.dense (mtop \<odot> f) = (\<forall>j. \<exists>i. f (i, j) \<noteq> bot)
[PROOF STEP]
have "... \<longleftrightarrow> (\<forall>j . \<exists>i . f (i,j) \<noteq> bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i. \<exists>j. (f\<^sup>t) (i, j) \<noteq> bot) = (\<forall>j. \<exists>i. f (i, j) \<noteq> bot)
[PROOF STEP]
by (simp add: conv_matrix_def)
[PROOF STATE]
proof (state)
this:
(\<forall>i. \<exists>j. (f\<^sup>t) (i, j) \<noteq> bot) = (\<forall>j. \<exists>i. f (i, j) \<noteq> bot)

goal (1 subgoal):
 1. matrix_p_algebra.dense (mtop \<odot> f) = (\<forall>j. \<exists>i. f (i, j) \<noteq> bot)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
matrix_p_algebra.dense (mtop \<odot> f) = (\<forall>j. \<exists>i. f (i, j) \<noteq> bot)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
matrix_p_algebra.dense (mtop \<odot> f) = (\<forall>j. \<exists>i. f (i, j) \<noteq> bot)

goal (1 subgoal):
 1. matrix_p_algebra.dense (mtop \<odot> f) = (\<forall>j. \<exists>i. f (i, j) \<noteq> bot)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
matrix_p_algebra.dense (mtop \<odot> f) = (\<forall>j. \<exists>i. f (i, j) \<noteq> bot)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pp_surjective_linorder_matrix:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_bounded_idempotent_semiring.surjective (\<ominus>\<ominus>f) \<longleftrightarrow> (\<forall>j . \<exists>i . f (i,j) \<noteq> bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_bounded_idempotent_semiring.surjective (\<ominus> \<ominus> f) = (\<forall>j. \<exists>i. f (i, j) \<noteq> bot)
[PROOF STEP]
using matrix_stone_relation_algebra.pp_surjective pp_surjective_linorder_matrix_1
[PROOF STATE]
proof (prove)
using this:
matrix_bounded_idempotent_semiring.surjective (\<ominus> \<ominus> ?x) = matrix_p_algebra.dense (mtop \<odot> ?x)
matrix_p_algebra.dense (mtop \<odot> ?f) = (\<forall>j. \<exists>i. ?f (i, j) \<noteq> bot)

goal (1 subgoal):
 1. matrix_bounded_idempotent_semiring.surjective (\<ominus> \<ominus> f) = (\<forall>j. \<exists>i. f (i, j) \<noteq> bot)
[PROOF STEP]
by auto


[STATEMENT]
lemma pp_bijective_linorder_matrix:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.pp_bijective f \<longleftrightarrow> (\<forall>j . \<exists>i . f (i,j) \<noteq> bot \<and> (\<forall>k . i \<noteq> k \<longrightarrow> f (k,j) = bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.pp_bijective f = (\<forall>j. \<exists>i. f (i, j) \<noteq> bot \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
by (unfold matrix_stone_relation_algebra.pp_bijective_conv_mapping pp_mapping_linorder_matrix) (simp add: conv_matrix_def)


[STATEMENT]
lemma pp_bijective_linorder_matrix_unique:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.pp_bijective f \<longleftrightarrow> (\<forall>j . \<exists>!i . f (i,j) \<noteq> bot \<and> (\<forall>k . i \<noteq> k \<longrightarrow> f (k,j) = bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.pp_bijective f = (\<forall>j. \<exists>!i. f (i, j) \<noteq> bot \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
by (unfold matrix_stone_relation_algebra.pp_bijective_conv_mapping pp_mapping_linorder_matrix_unique) (simp add: conv_matrix_def)