[STATEMENT]
lemma taq_proots_gt_code[code]:
  "TaQ_gt_rats a p q = (
    if poly p a \<noteq> 0 then
      (let
      ip = clear_de p;
      iq = clear_de q
      in ri_changes_gt_spmods a ip (pderiv ip * iq))
    else
       Code.abort (STR ''Roots at border yet to be supported'')
                              (\<lambda>_. TaQ_gt_rats a p q)
    )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
proof (cases "poly p a = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. poly p a = 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
 2. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
poly p a = 0

goal (2 subgoals):
 1. poly p a = 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
 2. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poly p a = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
poly p a = 0

goal (1 subgoal):
 1. TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
poly p a \<noteq> 0

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
define ip iq where "ip = clear_de p" and "iq = clear_de q"
[PROOF STATE]
proof (state)
this:
ip = clear_de p
iq = clear_de q

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
define dp dq where "dp = rat_of_int (de_lcm p)" and "dq = rat_of_int (de_lcm q)"
[PROOF STATE]
proof (state)
this:
dp = rat_of_int (de_lcm p)
dq = rat_of_int (de_lcm q)

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
define aa where "aa = real_of_rat a"
[PROOF STATE]
proof (state)
this:
aa = real_of_rat a

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
have "dp > 0" "dq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < dp &&& 0 < dq
[PROOF STEP]
unfolding dp_def dq_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < rat_of_int (de_lcm p) &&& 0 < rat_of_int (de_lcm q)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
0 < dp
0 < dq

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
have ip:"of_int_poly ip = smult dp p" and iq:"of_int_poly iq = smult dq q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_poly ip = smult dp p &&& of_int_poly iq = smult dq q
[PROOF STEP]
using clear_de
[PROOF STATE]
proof (prove)
using this:
of_int_poly (clear_de ?p) = smult (rat_of_int (de_lcm ?p)) ?p

goal (1 subgoal):
 1. of_int_poly ip = smult dp p &&& of_int_poly iq = smult dq q
[PROOF STEP]
unfolding ip_def iq_def dp_def dq_def
[PROOF STATE]
proof (prove)
using this:
of_int_poly (clear_de ?p) = smult (rat_of_int (de_lcm ?p)) ?p

goal (1 subgoal):
 1. of_int_poly (clear_de p) = smult (rat_of_int (de_lcm p)) p &&& of_int_poly (clear_de q) = smult (rat_of_int (de_lcm q)) q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int_poly ip = smult dp p
of_int_poly iq = smult dq q

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
have "TaQ_gt_rats a p q = taq {x. poly (map_poly real_of_rat (of_int_poly ip)) x = 0
        \<and> aa < x}
        (map_poly real_of_rat (of_int_poly iq))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TaQ_gt_rats a p q = taq {x. poly (map_poly real_of_rat (of_int_poly ip)) x = 0 \<and> aa < x} (map_poly real_of_rat (of_int_poly iq))
[PROOF STEP]
unfolding TaQ_gt_rats_def ip iq aa_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. taq {x. poly (map_poly real_of_rat p) x = 0 \<and> real_of_rat a < x} (map_poly real_of_rat q) = taq {x. poly (map_poly real_of_rat (smult dp p)) x = 0 \<and> real_of_rat a < x} (map_poly real_of_rat (smult dq q))
[PROOF STEP]
using \<open>dp > 0\<close> \<open>dq >0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < dp
0 < dq

goal (1 subgoal):
 1. taq {x. poly (map_poly real_of_rat p) x = 0 \<and> real_of_rat a < x} (map_poly real_of_rat q) = taq {x. poly (map_poly real_of_rat (smult dp p)) x = 0 \<and> real_of_rat a < x} (map_poly real_of_rat (smult dq q))
[PROOF STEP]
by (simp add:of_rat_hom.map_poly_hom_smult taq_smult_pos)
[PROOF STATE]
proof (state)
this:
TaQ_gt_rats a p q = taq {x. poly (map_poly real_of_rat (of_int_poly ip)) x = 0 \<and> aa < x} (map_poly real_of_rat (of_int_poly iq))

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
TaQ_gt_rats a p q = taq {x. poly (map_poly real_of_rat (of_int_poly ip)) x = 0 \<and> aa < x} (map_poly real_of_rat (of_int_poly iq))

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
have "... = taq {x. poly (of_int_poly ip) x = (0::real)
        \<and> aa < x } (of_int_poly iq)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. taq {x. poly (map_poly real_of_rat (of_int_poly ip)) x = 0 \<and> aa < x} (map_poly real_of_rat (of_int_poly iq)) = taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq)
[PROOF STEP]
by (simp add:map_poly_map_poly comp_def)
[PROOF STATE]
proof (state)
this:
taq {x. poly (map_poly real_of_rat (of_int_poly ip)) x = 0 \<and> aa < x} (map_poly real_of_rat (of_int_poly iq)) = taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq)

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
taq {x. poly (map_poly real_of_rat (of_int_poly ip)) x = 0 \<and> aa < x} (map_poly real_of_rat (of_int_poly iq)) = taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq)

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
have "... = changes_gt_smods aa (of_int_poly ip)
      (pderiv (of_int_poly ip) * of_int_poly iq)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq)
[PROOF STEP]
have "poly (map_poly of_int ip) aa \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (of_int_poly ip) aa \<noteq> 0
[PROOF STEP]
unfolding aa_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (of_int_poly ip) (real_of_rat a) \<noteq> 0
[PROOF STEP]
using False \<open>0 < dp\<close> ip rat_int.map_poly_R_hom_commute
[PROOF STATE]
proof (prove)
using this:
poly p a \<noteq> 0
0 < dp
of_int_poly ip = smult dp p
poly (of_int_poly ?p) (real_of_rat ?x) = real_of_rat (poly (of_int_poly ?p) ?x)

goal (1 subgoal):
 1. poly (of_int_poly ip) (real_of_rat a) \<noteq> 0
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
poly (of_int_poly ip) aa \<noteq> 0

goal (1 subgoal):
 1. taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq)
[PROOF STEP]
from sturm_tarski_above[OF this]
[PROOF STATE]
proof (chain)
picking this:
taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} ?q = changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * ?q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} ?q = changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * ?q)

goal (1 subgoal):
 1. taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq)

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
taq {x. poly (of_int_poly ip) x = 0 \<and> aa < x} (of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq)

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
have "... = changes_gt_smods aa (of_int_poly ip) (of_int_poly (pderiv ip * iq))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (of_int_poly (pderiv ip * iq))
[PROOF STEP]
by (simp add: of_int_hom.map_poly_pderiv of_int_poly_hom.hom_mult)
[PROOF STATE]
proof (state)
this:
changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (of_int_poly (pderiv ip * iq))

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
changes_gt_smods aa (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq) = changes_gt_smods aa (of_int_poly ip) (of_int_poly (pderiv ip * iq))

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
have "... = ri_changes_gt_spmods a ip (pderiv ip * iq)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. changes_gt_smods aa (of_int_poly ip) (of_int_poly (pderiv ip * iq)) = ri_changes_gt_spmods a ip (pderiv ip * iq)
[PROOF STEP]
using rat_int.changes_spmods_smods
[PROOF STATE]
proof (prove)
using this:
ri_changes_itv_spmods ?a ?b ?p ?q = changes_itv_smods (real_of_rat ?a) (real_of_rat ?b) (of_int_poly ?p) (of_int_poly ?q)
ri_changes_R_spmods ?p ?q = changes_R_smods (of_int_poly ?p) (of_int_poly ?q)
ri_changes_gt_spmods ?a ?p ?q = changes_gt_smods (real_of_rat ?a) (of_int_poly ?p) (of_int_poly ?q)
ri_changes_le_spmods ?b ?p ?q = changes_le_smods (real_of_rat ?b) (of_int_poly ?p) (of_int_poly ?q)

goal (1 subgoal):
 1. changes_gt_smods aa (of_int_poly ip) (of_int_poly (pderiv ip * iq)) = ri_changes_gt_spmods a ip (pderiv ip * iq)
[PROOF STEP]
unfolding aa_def
[PROOF STATE]
proof (prove)
using this:
ri_changes_itv_spmods ?a ?b ?p ?q = changes_itv_smods (real_of_rat ?a) (real_of_rat ?b) (of_int_poly ?p) (of_int_poly ?q)
ri_changes_R_spmods ?p ?q = changes_R_smods (of_int_poly ?p) (of_int_poly ?q)
ri_changes_gt_spmods ?a ?p ?q = changes_gt_smods (real_of_rat ?a) (of_int_poly ?p) (of_int_poly ?q)
ri_changes_le_spmods ?b ?p ?q = changes_le_smods (real_of_rat ?b) (of_int_poly ?p) (of_int_poly ?q)

goal (1 subgoal):
 1. changes_gt_smods (real_of_rat a) (of_int_poly ip) (of_int_poly (pderiv ip * iq)) = ri_changes_gt_spmods a ip (pderiv ip * iq)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
changes_gt_smods aa (of_int_poly ip) (of_int_poly (pderiv ip * iq)) = ri_changes_gt_spmods a ip (pderiv ip * iq)

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
TaQ_gt_rats a p q = ri_changes_gt_spmods a ip (pderiv ip * iq)
[PROOF STEP]
have "TaQ_gt_rats a p q = ri_changes_gt_spmods a ip (pderiv ip * iq) "
[PROOF STATE]
proof (prove)
using this:
TaQ_gt_rats a p q = ri_changes_gt_spmods a ip (pderiv ip * iq)

goal (1 subgoal):
 1. TaQ_gt_rats a p q = ri_changes_gt_spmods a ip (pderiv ip * iq)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
TaQ_gt_rats a p q = ri_changes_gt_spmods a ip (pderiv ip * iq)

goal (1 subgoal):
 1. poly p a \<noteq> 0 \<Longrightarrow> TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
TaQ_gt_rats a p q = ri_changes_gt_spmods a ip (pderiv ip * iq)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
TaQ_gt_rats a p q = ri_changes_gt_spmods a ip (pderiv ip * iq)

goal (1 subgoal):
 1. TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
unfolding Let_def ip_def iq_def
[PROOF STATE]
proof (prove)
using this:
TaQ_gt_rats a p q = ri_changes_gt_spmods a (clear_de p) (pderiv (clear_de p) * clear_de q)

goal (1 subgoal):
 1. TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then ri_changes_gt_spmods a (clear_de p) (pderiv (clear_de p) * clear_de q) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
TaQ_gt_rats a p q = ri_changes_gt_spmods a (clear_de p) (pderiv (clear_de p) * clear_de q)
poly p a \<noteq> 0

goal (1 subgoal):
 1. TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then ri_changes_gt_spmods a (clear_de p) (pderiv (clear_de p) * clear_de q) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
TaQ_gt_rats a p q = (if poly p a \<noteq> 0 then let ip = clear_de p; iq = clear_de q in ri_changes_gt_spmods a ip (pderiv ip * iq) else Code.abort STR ''Roots at border yet to be supported'' (\<lambda>_. TaQ_gt_rats a p q))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma worklist_tree_aux_rule:
assumes "worklist_tree_aux succs f (ws,s) = Some(ws',s')"
and "invariant I succs"
and "\<forall>x \<in> set ws. I x"
and "\<And>s. P [] s s"
and "\<And>r x ws s. I x \<Longrightarrow> \<forall>x \<in> set ws. I x \<Longrightarrow> P ws (f x s) r \<Longrightarrow> P (x#ws) s r"
shows "\<exists>rs. set rs = ((Rel succs)\<^sup>* ) `` (set ws) \<and> P rs s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'
[PROOF STEP]
let ?R = "(Rel succs)\<^sup>* `` set ws"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'
[PROOF STEP]
from worklist_tree_aux_Some_foldl[OF assms(1)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> s' = foldl (\<lambda>s x. f x s) s rs
[PROOF STEP]
obtain rs where
    rs: "set rs = ?R" "s' = foldl (\<lambda>s x. f x s) s rs"
[PROOF STATE]
proof (prove)
using this:
\<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> s' = foldl (\<lambda>s x. f x s) s rs

goal (1 subgoal):
 1. (\<And>rs. \<lbrakk>set rs = (Rel succs)\<^sup>* `` set ws; s' = foldl (\<lambda>s x. f x s) s rs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set rs = (Rel succs)\<^sup>* `` set ws
s' = foldl (\<lambda>s x. f x s) s rs

goal (1 subgoal):
 1. \<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
set rs = (Rel succs)\<^sup>* `` set ws
s' = foldl (\<lambda>s x. f x s) s rs

goal (1 subgoal):
 1. \<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'
[PROOF STEP]
fix xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'
[PROOF STEP]
have "(\<forall>x \<in> set xs. I x) \<Longrightarrow> P xs s (foldl (\<lambda>s x. f x s) s xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set xs. I x \<Longrightarrow> P xs s (foldl (\<lambda>s x. f x s) s xs)
[PROOF STEP]
proof(induct xs arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. Ball (set []) I \<Longrightarrow> P [] s (foldl (\<lambda>s x. f x s) s [])
 2. \<And>a xs s. \<lbrakk>\<And>s. Ball (set xs) I \<Longrightarrow> P xs s (foldl (\<lambda>s x. f x s) s xs); Ball (set (a # xs)) I\<rbrakk> \<Longrightarrow> P (a # xs) s (foldl (\<lambda>s x. f x s) s (a # xs))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set []. I a

goal (2 subgoals):
 1. \<And>s. Ball (set []) I \<Longrightarrow> P [] s (foldl (\<lambda>s x. f x s) s [])
 2. \<And>a xs s. \<lbrakk>\<And>s. Ball (set xs) I \<Longrightarrow> P xs s (foldl (\<lambda>s x. f x s) s xs); Ball (set (a # xs)) I\<rbrakk> \<Longrightarrow> P (a # xs) s (foldl (\<lambda>s x. f x s) s (a # xs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P [] s (foldl (\<lambda>s x. f x s) s [])
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
P [] ?s ?s

goal (1 subgoal):
 1. P [] s (foldl (\<lambda>s x. f x s) s [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P [] s (foldl (\<lambda>s x. f x s) s [])

goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<And>s. Ball (set xs) I \<Longrightarrow> P xs s (foldl (\<lambda>s x. f x s) s xs); Ball (set (a # xs)) I\<rbrakk> \<Longrightarrow> P (a # xs) s (foldl (\<lambda>s x. f x s) s (a # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<And>s. Ball (set xs) I \<Longrightarrow> P xs s (foldl (\<lambda>s x. f x s) s xs); Ball (set (a # xs)) I\<rbrakk> \<Longrightarrow> P (a # xs) s (foldl (\<lambda>s x. f x s) s (a # xs))
[PROOF STEP]
case Cons
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set xs_. I a \<Longrightarrow> P xs_ ?s (foldl (\<lambda>s x. f x s) ?s xs_)
\<forall>a\<in>set (a_ # xs_). I a

goal (1 subgoal):
 1. \<And>a xs s. \<lbrakk>\<And>s. Ball (set xs) I \<Longrightarrow> P xs s (foldl (\<lambda>s x. f x s) s xs); Ball (set (a # xs)) I\<rbrakk> \<Longrightarrow> P (a # xs) s (foldl (\<lambda>s x. f x s) s (a # xs))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set xs_. I a \<Longrightarrow> P xs_ ?s (foldl (\<lambda>s x. f x s) ?s xs_)
\<forall>a\<in>set (a_ # xs_). I a

goal (1 subgoal):
 1. P (a_ # xs_) s (foldl (\<lambda>s x. f x s) s (a_ # xs_))
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set xs_. I a \<Longrightarrow> P xs_ ?s (foldl (\<lambda>s x. f x s) ?s xs_)
\<forall>a\<in>set (a_ # xs_). I a
\<lbrakk>I ?x; \<forall>x\<in>set ?ws. I x; P ?ws (f ?x ?s) ?r\<rbrakk> \<Longrightarrow> P (?x # ?ws) ?s ?r

goal (1 subgoal):
 1. P (a_ # xs_) s (foldl (\<lambda>s x. f x s) s (a_ # xs_))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P (a_ # xs_) s (foldl (\<lambda>s x. f x s) s (a_ # xs_))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set xs. I x \<Longrightarrow> P xs s (foldl (\<lambda>s x. f x s) s xs)

goal (1 subgoal):
 1. \<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set ?xs2. I x \<Longrightarrow> P ?xs2 s (foldl (\<lambda>s x. f x s) s ?xs2)

goal (1 subgoal):
 1. \<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'
[PROOF STEP]
with invariant_succs[OF assms(2,3)]
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>(Rel succs)\<^sup>* `` set ws. I x
\<forall>x\<in>set ?xs2. I x \<Longrightarrow> P ?xs2 s (foldl (\<lambda>s x. f x s) s ?xs2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>(Rel succs)\<^sup>* `` set ws. I x
\<forall>x\<in>set ?xs2. I x \<Longrightarrow> P ?xs2 s (foldl (\<lambda>s x. f x s) s ?xs2)

goal (1 subgoal):
 1. \<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'
[PROOF STEP]
by (metis rs)
[PROOF STATE]
proof (state)
this:
\<exists>rs. set rs = (Rel succs)\<^sup>* `` set ws \<and> P rs s s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Agent_univ: "(UNIV :: Agent set) = {Robot}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV = {Robot}
[PROOF STEP]
unfolding UNIV_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_ext (\<lambda>x. True) = {Robot}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x = Robot
[PROOF STEP]
apply (case_tac x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x = Robot \<Longrightarrow> x = Robot
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma infer_l_fresh:
  assumes  "\<turnstile> l \<Rightarrow> \<tau>"
  shows "atom x \<sharp> \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom x \<sharp> \<tau>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atom x \<sharp> \<tau>
[PROOF STEP]
have "[] ; {||}  \<turnstile>\<^sub>w\<^sub>f GNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  [] ; {||}  \<turnstile>\<^sub>w\<^sub>f GNil
[PROOF STEP]
using wfG_nilI wfTh_emptyI
[PROOF STATE]
proof (prove)
using this:
   \<turnstile>\<^sub>w\<^sub>f ?\<Theta>  \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f GNil
   \<turnstile>\<^sub>w\<^sub>f []

goal (1 subgoal):
 1.  [] ; {||}  \<turnstile>\<^sub>w\<^sub>f GNil
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 [] ; {||}  \<turnstile>\<^sub>w\<^sub>f GNil

goal (1 subgoal):
 1. atom x \<sharp> \<tau>
[PROOF STEP]
hence "[] ; {||} ; GNil   \<turnstile>\<^sub>w\<^sub>f \<tau>"
[PROOF STATE]
proof (prove)
using this:
 [] ; {||}  \<turnstile>\<^sub>w\<^sub>f GNil

goal (1 subgoal):
 1.  [] ; {||} ; GNil   \<turnstile>\<^sub>w\<^sub>f \<tau>
[PROOF STEP]
using assms infer_l_wf
[PROOF STATE]
proof (prove)
using this:
 [] ; {||}  \<turnstile>\<^sub>w\<^sub>f GNil
 \<turnstile> l \<Rightarrow> \<tau>
\<lbrakk> \<turnstile> ?l \<Rightarrow> ?\<tau>;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> \<rbrakk> \<Longrightarrow>    \<turnstile>\<^sub>w\<^sub>f ?\<Theta>
\<lbrakk> \<turnstile> ?l \<Rightarrow> ?\<tau>;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma>
\<lbrakk> \<turnstile> ?l \<Rightarrow> ?\<tau>;  ?\<Theta> ; ?\<B>  \<turnstile>\<^sub>w\<^sub>f ?\<Gamma> \<rbrakk> \<Longrightarrow>  ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?\<tau>

goal (1 subgoal):
 1.  [] ; {||} ; GNil   \<turnstile>\<^sub>w\<^sub>f \<tau>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 [] ; {||} ; GNil   \<turnstile>\<^sub>w\<^sub>f \<tau>

goal (1 subgoal):
 1. atom x \<sharp> \<tau>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
 [] ; {||} ; GNil   \<turnstile>\<^sub>w\<^sub>f \<tau>

goal (1 subgoal):
 1. atom x \<sharp> \<tau>
[PROOF STEP]
using  fresh_def wfT_supp
[PROOF STATE]
proof (prove)
using this:
 [] ; {||} ; GNil   \<turnstile>\<^sub>w\<^sub>f \<tau>
?a \<sharp> ?x \<equiv> ?a \<notin> supp ?x
 ?\<Theta> ; ?\<B> ; ?\<Gamma>   \<turnstile>\<^sub>w\<^sub>f ?\<tau>  \<Longrightarrow> supp ?\<tau> \<subseteq> atom_dom ?\<Gamma> \<union> supp ?\<B>

goal (1 subgoal):
 1. atom x \<sharp> \<tau>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
atom x \<sharp> \<tau>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma roofed_gen_minus_web [simp]: "roofed_gen (\<Gamma> \<ominus> f) = roofed_gen \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. roofed_gen (\<Gamma> \<ominus> f) = roofed_gen \<Gamma>
[PROOF STEP]
by(simp add: fun_eq_iff roofed_def)


[STATEMENT]
lemma connected_verts_G_eq_T:
  assumes "graph G" and "connected G"
  shows "verts T = verts G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. verts T = verts G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. verts T = verts G
[PROOF STEP]
have "root \<in> verts G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root \<in> verts G
[PROOF STEP]
using root_in_G
[PROOF STATE]
proof (prove)
using this:
root \<in> verts G

goal (1 subgoal):
 1. root \<in> verts G
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
root \<in> verts G

goal (1 subgoal):
 1. verts T = verts G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
root \<in> verts G
[PROOF STEP]
have "\<forall>x\<in>verts G. root \<rightarrow>\<^sup>*\<^bsub>G\<^esub> x"
[PROOF STATE]
proof (prove)
using this:
root \<in> verts G

goal (1 subgoal):
 1. \<forall>x\<in>verts G. root \<rightarrow>\<^sup>*\<^bsub>G\<^esub> x
[PROOF STEP]
using graph.connected_iff_reachable assms(1,2)
[PROOF STATE]
proof (prove)
using this:
root \<in> verts G
graph ?G \<Longrightarrow> Digraph_Component.connected ?G = ((\<forall>x\<in>verts ?G. \<forall>y\<in>verts ?G. x \<rightarrow>\<^sup>*\<^bsub>?G\<^esub> y) \<and> verts ?G \<noteq> {})
graph G
Digraph_Component.connected G

goal (1 subgoal):
 1. \<forall>x\<in>verts G. root \<rightarrow>\<^sup>*\<^bsub>G\<^esub> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>verts G. root \<rightarrow>\<^sup>*\<^bsub>G\<^esub> x

goal (1 subgoal):
 1. verts T = verts G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>verts G. root \<rightarrow>\<^sup>*\<^bsub>G\<^esub> x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>verts G. root \<rightarrow>\<^sup>*\<^bsub>G\<^esub> x

goal (1 subgoal):
 1. verts T = verts G
[PROOF STEP]
using reachable_verts_G_eq_T
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>verts G. root \<rightarrow>\<^sup>*\<^bsub>G\<^esub> x
\<forall>x\<in>verts G. root \<rightarrow>\<^sup>*\<^bsub>G\<^esub> x \<Longrightarrow> verts T = verts G

goal (1 subgoal):
 1. verts T = verts G
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
verts T = verts G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nf_ACI_nFAND:
  "\<lbrakk>sorted \<phi>s; distinct \<phi>s; list_all nf_ACI \<phi>s; list_all (\<lambda>x. \<not> is_FAnd x) \<phi>s\<rbrakk> \<Longrightarrow> nf_ACI (nFAND \<phi>s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted \<phi>s; distinct \<phi>s; list_all nf_ACI \<phi>s; list_all (\<lambda>x. \<not> is_FAnd x) \<phi>s\<rbrakk> \<Longrightarrow> nf_ACI (nFAND \<phi>s)
[PROOF STEP]
by (induct \<phi>s rule: nFAND.induct)
    (auto simp: juncts_list_singleton conjuncts_list_nFAND nf_ACI_D)


[STATEMENT]
lemma show_law_nat [show_law_intros]:
  "show_law showsp_nat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. show_law showsp_nat n
[PROOF STEP]
by (rule show_lawI, induct n rule: nat_less_induct) (simp add: show_law_simps showsp_nat.simps)


[STATEMENT]
lemma ac_cong_set2_is_semialg:
  assumes "k \<in> Units (Zp_res_ring n)"
  assumes "n > 0"
  shows "is_semialgebraic 2 (ac_cong_set2 n k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_semialgebraic 2 (ac_cong_set2 n k)
[PROOF STEP]
using  ac_cong_set_is_univ_semialg ac_cong_set2_cartesian_product[of k n]
      cartesian_product_is_semialgebraic[of 1 "((\<lambda>a. [a]) ` ac_cong_set n k)" 1 " ((\<lambda>a. [a]) ` val_ring_constant_ac_set n k)"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < ?n; ?k \<in> Units (residue_ring (p ^ ?n))\<rbrakk> \<Longrightarrow> is_univ_semialgebraic (ac_cong_set ?n ?k)
\<lbrakk>k \<in> Units (residue_ring (p ^ n)); 0 < n\<rbrakk> \<Longrightarrow> ac_cong_set2 n k = cartesian_product ((\<lambda>a. [a]) ` ac_cong_set n k) ((\<lambda>a. [a]) ` val_ring_constant_ac_set n k)
\<lbrakk>is_semialgebraic 1 ((\<lambda>a. [a]) ` ac_cong_set n k); is_semialgebraic 1 ((\<lambda>a. [a]) ` val_ring_constant_ac_set n k)\<rbrakk> \<Longrightarrow> is_semialgebraic (1 + 1) (cartesian_product ((\<lambda>a. [a]) ` ac_cong_set n k) ((\<lambda>a. [a]) ` val_ring_constant_ac_set n k))

goal (1 subgoal):
 1. is_semialgebraic 2 (ac_cong_set2 n k)
[PROOF STEP]
by (metis assms(1) assms(2) is_univ_semialgebraicE less_one less_or_eq_imp_le nat_neq_iff
      one_add_one val_ring_constant_ac_set_is_univ_semialgebraic zero_not_in_residue_units)


[STATEMENT]
lemma sums_minus_ereal: "\<not> {- \<infinity>, \<infinity>} \<subseteq> f ` UNIV \<Longrightarrow> (\<lambda>n. - f n::ereal) sums x \<Longrightarrow> f sums - x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> {- \<infinity>, \<infinity>} \<subseteq> range f; (\<lambda>n. - f n) sums x\<rbrakk> \<Longrightarrow> f sums - x
[PROOF STEP]
unfolding sums_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> {- \<infinity>, \<infinity>} \<subseteq> range f; (\<lambda>n. \<Sum>n<n. - f n) \<longlonglongrightarrow> x\<rbrakk> \<Longrightarrow> (\<lambda>n. sum f {..<n}) \<longlonglongrightarrow> - x
[PROOF STEP]
apply (subst ereal_Lim_uminus)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> {- \<infinity>, \<infinity>} \<subseteq> range f; (\<lambda>n. \<Sum>n<n. - f n) \<longlonglongrightarrow> x\<rbrakk> \<Longrightarrow> (\<lambda>x. - sum f {..<x}) \<longlonglongrightarrow> - (- x)
[PROOF STEP]
apply (subst (asm) setsum_negf_ereal)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<not> {- \<infinity>, \<infinity>} \<subseteq> range f \<Longrightarrow> \<not> {- \<infinity>, \<infinity>} \<subseteq> f ` {..<n}
 2. \<lbrakk>\<not> {- \<infinity>, \<infinity>} \<subseteq> range f; (\<lambda>n. - sum f {..<n}) \<longlonglongrightarrow> x\<rbrakk> \<Longrightarrow> (\<lambda>x. - sum f {..<x}) \<longlonglongrightarrow> - (- x)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma map_append: "map f (append xs ys) = append (map f xs) (map f ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f (xs @ ys) = map f xs @ map f ys
[PROOF STEP]
by simp


[STATEMENT]
lemma spr_ii_sim: "sim SPR.MC spr_ii_simMC spr_ii_sim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. sim_range SPR.MC spr_ii_simMC spr_ii_sim
 2. sim_val SPR.MC spr_ii_simMC spr_ii_sim
 3. sim_f SPR.MC spr_ii_simMC spr_ii_sim
 4. sim_r SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
show "sim_range SPR.MC spr_ii_simMC spr_ii_sim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_range SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
by (rule sim_rangeI) (simp_all add: spr_ii_sim_def)
[PROOF STATE]
proof (state)
this:
sim_range SPR.MC spr_ii_simMC spr_ii_sim

goal (3 subgoals):
 1. sim_val SPR.MC spr_ii_simMC spr_ii_sim
 2. sim_f SPR.MC spr_ii_simMC spr_ii_sim
 3. sim_r SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sim_val SPR.MC spr_ii_simMC spr_ii_sim
 2. sim_f SPR.MC spr_ii_simMC spr_ii_sim
 3. sim_r SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
show "sim_val SPR.MC spr_ii_simMC spr_ii_sim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_val SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
by (rule sim_valI) simp
[PROOF STATE]
proof (state)
this:
sim_val SPR.MC spr_ii_simMC spr_ii_sim

goal (2 subgoals):
 1. sim_f SPR.MC spr_ii_simMC spr_ii_sim
 2. sim_r SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sim_f SPR.MC spr_ii_simMC spr_ii_sim
 2. sim_r SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
show "sim_f SPR.MC spr_ii_simMC spr_ii_sim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_f SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
unfolding spr_ii_simRels_def spr_ii_sim_def mkKripke_def SPR.mkM_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_f \<lparr>worlds = SPR.jkbpC, relations = \<lambda>a. {(t, t'). {t, t'} \<subseteq> SPR.jkbpC \<and> spr_jview a t = spr_jview a t'}, valuation = envVal \<circ> tLast\<rparr> \<lparr>worlds = (\<lambda>t. (tObsC_ii_abs t, tLast t)) ` SPR.jkbpC, relations = \<lambda>a. Restr {(s, s') |s s'. envObs a (snd s) = envObs a (snd s') \<and> fst s = fst s'} ((\<lambda>t. (tObsC_ii_abs t, tLast t)) ` SPR.jkbpC), valuation = spr_ii_simVal\<rparr> (\<lambda>t. (tObsC_ii_abs t, tLast t))
[PROOF STEP]
by (rule sim_fI, auto simp del: split_paired_Ex)
[PROOF STATE]
proof (state)
this:
sim_f SPR.MC spr_ii_simMC spr_ii_sim

goal (1 subgoal):
 1. sim_r SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sim_r SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
show "sim_r SPR.MC spr_ii_simMC spr_ii_sim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_r SPR.MC spr_ii_simMC spr_ii_sim
[PROOF STEP]
by (rule spr_ii_sim_r)
[PROOF STATE]
proof (state)
this:
sim_r SPR.MC spr_ii_simMC spr_ii_sim

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pos_les_eq_append_diff [simp]:
  "p \<le>\<^sub>p q \<Longrightarrow> p @ (q -\<^sub>p p) = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le>\<^sub>p q \<Longrightarrow> p @ q -\<^sub>p p = q
[PROOF STEP]
by (metis option.sel pos_diff_def position_less_eq_def remove_prefix_append)


[STATEMENT]
lemma bind_fmap: "bind\<cdot>(fmap\<cdot>f\<cdot>xs)\<cdot>k = bind\<cdot>xs\<cdot>(\<Lambda> x. k\<cdot>(f\<cdot>x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap\<cdot>f\<cdot>xs \<bind> k = xs \<bind> (\<Lambda> x. k\<cdot>(f\<cdot>x))
[PROOF STEP]
by (simp add: monad_fmap bind_bind)


[STATEMENT]
lemma refl_ta_eps [simp]: "eps (refl_ta \<F> q) = {||}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eps (refl_ta \<F> q) = {||}
[PROOF STEP]
by (auto simp: refl_ta_def)


[STATEMENT]
lemma scc_root_is_discovered:
    "scc_root s v scc \<Longrightarrow> v \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scc_root s v scc \<Longrightarrow> v \<in> dom (discovered s)
[PROOF STEP]
by (simp add: scc_root_def)


[STATEMENT]
lemma scc_root_exists:
    assumes "is_scc E scc"
    and scc: "scc \<inter> dom (discovered s) \<noteq> {}"
    shows "\<exists>r. scc_root s r scc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
let ?S = "scc \<inter> dom (discovered s)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
from discovered_finite
[PROOF STATE]
proof (chain)
picking this:
finite (dom (discovered s))
[PROOF STEP]
have "finite (\<delta> s`?S)"
[PROOF STATE]
proof (prove)
using this:
finite (dom (discovered s))

goal (1 subgoal):
 1. finite (\<delta> s ` (scc \<inter> dom (discovered s)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (\<delta> s ` (scc \<inter> dom (discovered s)))

goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (\<delta> s ` (scc \<inter> dom (discovered s)))

goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
from scc
[PROOF STATE]
proof (chain)
picking this:
scc \<inter> dom (discovered s) \<noteq> {}
[PROOF STEP]
have "\<delta> s ` ?S \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
scc \<inter> dom (discovered s) \<noteq> {}

goal (1 subgoal):
 1. \<delta> s ` (scc \<inter> dom (discovered s)) \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<delta> s ` (scc \<inter> dom (discovered s)) \<noteq> {}

goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<delta> s ` (scc \<inter> dom (discovered s)) \<noteq> {}

goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
have "\<And>(x::nat) f A. x \<notin> f ` A \<or> (\<exists>y. x = f y \<and> y \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x f A. x \<notin> f ` A \<or> (\<exists>y. x = f y \<and> y \<in> A)
[PROOF STEP]
by blast
      \<comment> \<open>autogenerated by sledgehammer\<close>
[PROOF STATE]
proof (state)
this:
?x7 \<notin> ?f7 ` ?A7 \<or> (\<exists>y. ?x7 = ?f7 y \<and> y \<in> ?A7)

goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (\<delta> s ` (scc \<inter> dom (discovered s)))
\<delta> s ` (scc \<inter> dom (discovered s)) \<noteq> {}
?x7 \<notin> ?f7 ` ?A7 \<or> (\<exists>y. ?x7 = ?f7 y \<and> y \<in> ?A7)
[PROOF STEP]
have "\<exists>x \<in> ?S. \<delta> s x = Min (\<delta> s ` ?S)"
[PROOF STATE]
proof (prove)
using this:
finite (\<delta> s ` (scc \<inter> dom (discovered s)))
\<delta> s ` (scc \<inter> dom (discovered s)) \<noteq> {}
?x7 \<notin> ?f7 ` ?A7 \<or> (\<exists>y. ?x7 = ?f7 y \<and> y \<in> ?A7)

goal (1 subgoal):
 1. \<exists>x\<in>scc \<inter> dom (discovered s). \<delta> s x = Min (\<delta> s ` (scc \<inter> dom (discovered s)))
[PROOF STEP]
by (metis Min_in)
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>scc \<inter> dom (discovered s). \<delta> s x = Min (\<delta> s ` (scc \<inter> dom (discovered s)))

goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
with Min_disc_is_scc_root \<open>is_scc E scc\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?v \<in> ?scc; ?v \<in> dom (discovered s); is_scc E ?scc; \<delta> s ?v = Min (\<delta> s ` (?scc \<inter> dom (discovered s)))\<rbrakk> \<Longrightarrow> scc_root s ?v ?scc
is_scc E scc
\<exists>x\<in>scc \<inter> dom (discovered s). \<delta> s x = Min (\<delta> s ` (scc \<inter> dom (discovered s)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> ?scc; ?v \<in> dom (discovered s); is_scc E ?scc; \<delta> s ?v = Min (\<delta> s ` (?scc \<inter> dom (discovered s)))\<rbrakk> \<Longrightarrow> scc_root s ?v ?scc
is_scc E scc
\<exists>x\<in>scc \<inter> dom (discovered s). \<delta> s x = Min (\<delta> s ` (scc \<inter> dom (discovered s)))

goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r. scc_root s r scc

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in category) cat_ntcf_rcomp_Hom_ntcf_id:
  assumes "\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>(-,ntcf_id \<FF>-) = ntcf_id Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(-,\<FF>-)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>(-,ntcf_id \<FF>-) = ntcf_id Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(-,\<FF>-)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>(-,ntcf_id \<FF>-) = ntcf_id Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(-,\<FF>-)
[PROOF STEP]
interpret \<FF>: is_functor \<alpha> \<BB> \<CC> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>(-,ntcf_id \<FF>-) = ntcf_id Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(-,\<FF>-)
[PROOF STEP]
from category_axioms assms
[PROOF STATE]
proof (chain)
picking this:
category \<alpha> \<CC>
\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
category \<alpha> \<CC>
\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>(-,ntcf_id \<FF>-) = ntcf_id Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(-,\<FF>-)
[PROOF STEP]
unfolding ntcf_rcomp_Hom_def ntcf_id_components \<FF>.cf_HomCod
[PROOF STATE]
proof (prove)
using this:
category \<alpha> \<CC>
\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>(ntcf_id (dghm_id \<CC>)-,ntcf_id \<FF>-) = ntcf_id Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(-,\<FF>-)
[PROOF STEP]
by (cs_concl cs_simp: ntcf_rcomp_Hom_def cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>(-,ntcf_id \<FF>-) = ntcf_id Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(-,\<FF>-)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in vsv) vsv_vrange_VLambda_app:
  assumes "g ` elts A = elts (\<D>\<^sub>\<circ> r)"
  shows "\<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>) = \<R>\<^sub>\<circ> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>) = \<R>\<^sub>\<circ> r
[PROOF STEP]
proof(intro vsubset_antisym vsv.vsv_vrange_vsubset, unfold vdomain_VLambda)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> A \<Longrightarrow> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
 3. vsv r
 4. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r \<Longrightarrow> r\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
[PROOF STEP]
show "(\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r" if "x \<in>\<^sub>\<circ> A" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
from assms that
[PROOF STATE]
proof (chain)
picking this:
g ` elts A = elts (\<D>\<^sub>\<circ> r)
x \<in>\<^sub>\<circ> A
[PROOF STEP]
have "g x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r"
[PROOF STATE]
proof (prove)
using this:
g ` elts A = elts (\<D>\<^sub>\<circ> r)
x \<in>\<^sub>\<circ> A

goal (1 subgoal):
 1. g x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r

goal (1 subgoal):
 1. (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r
[PROOF STEP]
have "r\<lparr>g x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r"
[PROOF STATE]
proof (prove)
using this:
g x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r

goal (1 subgoal):
 1. r\<lparr>g x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
r\<lparr>g x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r

goal (1 subgoal):
 1. (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> A
r\<lparr>g x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> A
r\<lparr>g x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r

goal (1 subgoal):
 1. (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in>\<^sub>\<circ> A \<Longrightarrow> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)\<lparr>?x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> r

goal (3 subgoals):
 1. vsv (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
 2. vsv r
 3. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r \<Longrightarrow> r\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
[PROOF STEP]
show "r\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)" if "x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
[PROOF STEP]
from that assms
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r
g ` elts A = elts (\<D>\<^sub>\<circ> r)
[PROOF STEP]
have "x \<in> g ` elts A"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r
g ` elts A = elts (\<D>\<^sub>\<circ> r)

goal (1 subgoal):
 1. x \<in> g ` elts A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> g ` elts A

goal (1 subgoal):
 1. r\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> g ` elts A
[PROOF STEP]
obtain c where c: "c \<in>\<^sub>\<circ> A" and x_def: "x = g c"
[PROOF STATE]
proof (prove)
using this:
x \<in> g ` elts A

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<in>\<^sub>\<circ> A; x = g c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
c \<in>\<^sub>\<circ> A
x = g c

goal (1 subgoal):
 1. r\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
[PROOF STEP]
from c
[PROOF STATE]
proof (chain)
picking this:
c \<in>\<^sub>\<circ> A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c \<in>\<^sub>\<circ> A

goal (1 subgoal):
 1. r\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
[PROOF STEP]
unfolding x_def
[PROOF STATE]
proof (prove)
using this:
c \<in>\<^sub>\<circ> A

goal (1 subgoal):
 1. r\<lparr>g c\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> r \<Longrightarrow> r\<lparr>?x\<rparr> \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)

goal (2 subgoals):
 1. vsv (\<lambda>x\<in>\<^sub>\<circ>A. r\<lparr>g x\<rparr>)
 2. vsv r
[PROOF STEP]
qed auto


[STATEMENT]
lemma (in category) cat_is_iso_arr_if_ntcf_Hom_snd_is_iso_ntcf:
  assumes "f : s \<mapsto>\<^bsub>\<CC>\<^esub> r"
    and "Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-) :
      Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(r,-) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>"
  shows "f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
f : s \<mapsto>\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
have r: "r \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>" and s: "s \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
f : s \<mapsto>\<^bsub>\<CC>\<^esub> r

goal (1 subgoal):
 1. r \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> &&& s \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
s \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
note unique = cat_ntcf_Hom_snd_is_iso_ntcf_Hom_snd_unique[OF r s assms(2)]
[PROOF STATE]
proof (state)
this:
Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr> : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-) = Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr>,-)
\<lbrakk>?f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>; Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-) = Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(?f,-)\<rbrakk> \<Longrightarrow> ?f = Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr>

goal (1 subgoal):
 1. f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
from unique(1)
[PROOF STATE]
proof (chain)
picking this:
Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr> : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
have Ym_Hf:
    "Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr> : s \<mapsto>\<^bsub>\<CC>\<^esub> r"
[PROOF STATE]
proof (prove)
using this:
Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr> : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r

goal (1 subgoal):
 1. Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr> : s \<mapsto>\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr> : s \<mapsto>\<^bsub>\<CC>\<^esub> r

goal (1 subgoal):
 1. f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
from unique(1)
[PROOF STATE]
proof (chain)
picking this:
Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr> : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr> : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r

goal (1 subgoal):
 1. f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
unfolding cat_ntcf_Hom_snd_inj[OF unique(2) assms(1) Ym_Hf, symmetric]
[PROOF STATE]
proof (prove)
using this:
f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r

goal (1 subgoal):
 1. f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Fvar_pbeta [simp]: "(Fvar x \<Rightarrow>\<^sub>\<beta> t) = (t = Fvar x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Fvar x => t) = (t = Fvar x)
[PROOF STEP]
by auto


[STATEMENT]
lemma iMOD_plus: "
  x \<in> [r, mod m] \<Longrightarrow> (x + k \<in> [r, mod m]) = (k mod m = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> [ r, mod m ] \<Longrightarrow> (x + k \<in> [ r, mod m ]) = (k mod m = 0)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> [ r, mod m ]; x + k \<in> [ r, mod m ]\<rbrakk> \<Longrightarrow> k mod m = 0
 2. \<lbrakk>x \<in> [ r, mod m ]; m dvd k\<rbrakk> \<Longrightarrow> x + k \<in> [ r, mod m ]
[PROOF STEP]
apply (drule iMOD_modD)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x mod m = r mod m; (x + k) mod m = r mod m\<rbrakk> \<Longrightarrow> k mod m = 0
 2. \<lbrakk>x \<in> [ r, mod m ]; m dvd k\<rbrakk> \<Longrightarrow> x + k \<in> [ r, mod m ]
[PROOF STEP]
apply (rule mod_add_eq_imp_mod_0[of x, THEN iffD1])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x mod m = r mod m; (x + k) mod m = r mod m\<rbrakk> \<Longrightarrow> (x + k) mod m = x mod m
 2. \<lbrakk>x \<in> [ r, mod m ]; m dvd k\<rbrakk> \<Longrightarrow> x + k \<in> [ r, mod m ]
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> [ r, mod m ]; m dvd k\<rbrakk> \<Longrightarrow> x + k \<in> [ r, mod m ]
[PROOF STEP]
apply (erule dvdE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ka. \<lbrakk>x \<in> [ r, mod m ]; k = m * ka\<rbrakk> \<Longrightarrow> x + k \<in> [ r, mod m ]
[PROOF STEP]
apply (simp add: mult.commute iMOD_plus_divisor_mult)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iIN_cut_less1: "
  \<lbrakk> t \<in> [n\<dots>,d]; n < t \<rbrakk> \<Longrightarrow> [n\<dots>,d] \<down>< t = [n\<dots>, t - Suc n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> [n\<dots>,d]; n < t\<rbrakk> \<Longrightarrow> [n\<dots>,d] \<down>< t = [n\<dots>,t - Suc n]
[PROOF STEP]
by (simp add: iIN_cut_less iT_iff)


[STATEMENT]
lemma size_list [simp]: " \<lbrakk>0 < size big; invar big; list big = []\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < size big; invar big; Big.list big = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
proof(induction big rule: list.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>common. \<lbrakk>0 < size (Common common); invar (Common common); Big.list (Common common) = []\<rbrakk> \<Longrightarrow> False
 2. \<And>extra uu_ uv_ remained big aux count. \<lbrakk>0 < size (Reverse (Current extra uu_ uv_ remained) big aux count); invar (Reverse (Current extra uu_ uv_ remained) big aux count); Big.list (Reverse (Current extra uu_ uv_ remained) big aux count) = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
0 < size (Common common_)
invar (Common common_)
Big.list (Common common_) = []

goal (2 subgoals):
 1. \<And>common. \<lbrakk>0 < size (Common common); invar (Common common); Big.list (Common common) = []\<rbrakk> \<Longrightarrow> False
 2. \<And>extra uu_ uv_ remained big aux count. \<lbrakk>0 < size (Reverse (Current extra uu_ uv_ remained) big aux count); invar (Reverse (Current extra uu_ uv_ remained) big aux count); Big.list (Reverse (Current extra uu_ uv_ remained) big aux count) = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < size (Common common_)
invar (Common common_)
Big.list (Common common_) = []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 < size (Common common_)
invar (Common common_)
Big.list (Common common_) = []

goal (1 subgoal):
 1. False
[PROOF STEP]
using list_size
[PROOF STATE]
proof (prove)
using this:
0 < size (Common common_)
invar (Common common_)
Big.list (Common common_) = []
\<lbrakk>0 < size ?common; Common.list ?common = []; invar ?common\<rbrakk> \<Longrightarrow> False

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

goal (1 subgoal):
 1. \<And>extra uu_ uv_ remained big aux count. \<lbrakk>0 < size (Reverse (Current extra uu_ uv_ remained) big aux count); invar (Reverse (Current extra uu_ uv_ remained) big aux count); Big.list (Reverse (Current extra uu_ uv_ remained) big aux count) = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>extra uu_ uv_ remained big aux count. \<lbrakk>0 < size (Reverse (Current extra uu_ uv_ remained) big aux count); invar (Reverse (Current extra uu_ uv_ remained) big aux count); Big.list (Reverse (Current extra uu_ uv_ remained) big aux count) = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
0 < size (Reverse (Current extra_ uu_ uv_ remained_) big_ aux_ count_)
invar (Reverse (Current extra_ uu_ uv_ remained_) big_ aux_ count_)
Big.list (Reverse (Current extra_ uu_ uv_ remained_) big_ aux_ count_) = []

goal (1 subgoal):
 1. \<And>extra uu_ uv_ remained big aux count. \<lbrakk>0 < size (Reverse (Current extra uu_ uv_ remained) big aux count); invar (Reverse (Current extra uu_ uv_ remained) big aux count); Big.list (Reverse (Current extra uu_ uv_ remained) big aux count) = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < size (Reverse (Current extra_ uu_ uv_ remained_) big_ aux_ count_)
invar (Reverse (Current extra_ uu_ uv_ remained_) big_ aux_ count_)
Big.list (Reverse (Current extra_ uu_ uv_ remained_) big_ aux_ count_) = []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 < size (Reverse (Current extra_ uu_ uv_ remained_) big_ aux_ count_)
invar (Reverse (Current extra_ uu_ uv_ remained_) big_ aux_ count_)
Big.list (Reverse (Current extra_ uu_ uv_ remained_) big_ aux_ count_) = []

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis list.distinct(1) list_Reverse)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma size_size_new: "\<lbrakk>invar (big :: 'a state); 0 < size big\<rbrakk> \<Longrightarrow> 0 < size_new big"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar big; 0 < size big\<rbrakk> \<Longrightarrow> 0 < size_new big
[PROOF STEP]
by(induction big)(auto simp: size_size_new)


[STATEMENT]
lemma at_neg_neg2:"\<Turnstile>\<^bold>\<not>(\<^bold>@c \<^bold>\<not> \<phi>) \<^bold>\<rightarrow> (\<^bold>@c  \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ts v. \<not> (\<forall>v'. v = c > v' \<longrightarrow> \<not> \<phi> ts v') \<longrightarrow> (\<forall>v'. v = c > v' \<longrightarrow> \<phi> ts v')
[PROOF STEP]
using switch_unique switch_def switch_refl
[PROOF STATE]
proof (prove)
using this:
?v = ?c > ?u \<and> ?v = ?c > ?w \<longrightarrow> ?u = ?w
?v = ?c > ?w \<equiv> ext ?v = ext ?w \<and> lan ?v = lan ?w \<and> own ?w = ?c \<and> more ?v = more ?w
?v = own ?v > ?v

goal (1 subgoal):
 1. \<forall>ts v. \<not> (\<forall>v'. v = c > v' \<longrightarrow> \<not> \<phi> ts v') \<longrightarrow> (\<forall>v'. v = c > v' \<longrightarrow> \<phi> ts v')
[PROOF STEP]
by metis


[STATEMENT]
lemma simulation_language:
    assumes "alphabet A \<subseteq> alphabet B"
    assumes "\<And> p. p \<in> initial A \<Longrightarrow> \<exists> q \<in> initial B. (p, q) \<in> R"
    assumes "\<And> a p p' q. p' \<in> transition A a p \<Longrightarrow> (p, q) \<in> R \<Longrightarrow> \<exists> q' \<in> transition B a q. (p', q') \<in> R"
    assumes "\<And> p q. (p, q) \<in> R \<Longrightarrow> accepting A p \<Longrightarrow> accepting B q"
    shows "language A \<subseteq> language B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. language A \<subseteq> language B
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> language A \<Longrightarrow> x \<in> language B
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> language A \<Longrightarrow> x \<in> language B
[PROOF STEP]
assume 1: "w \<in> language A"
[PROOF STATE]
proof (state)
this:
w \<in> language A

goal (1 subgoal):
 1. \<And>x. x \<in> language A \<Longrightarrow> x \<in> language B
[PROOF STEP]
obtain r p where 2: "p \<in> initial A" "run A (w ||| r) p" "infs (accepting A) (p ## r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p r. \<lbrakk>p \<in> initial A; run A (w ||| r) p; infs (accepting A) (p ## r)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
w \<in> language A

goal (1 subgoal):
 1. (\<And>p r. \<lbrakk>p \<in> initial A; run A (w ||| r) p; infs (accepting A) (p ## r)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
p \<in> initial A
run A (w ||| r) p
infs (accepting A) (p ## r)

goal (1 subgoal):
 1. \<And>x. x \<in> language A \<Longrightarrow> x \<in> language B
[PROOF STEP]
define P where "P n q \<equiv> (target (stake n (w ||| r)) p, q) \<in> R" for n q
[PROOF STATE]
proof (state)
this:
P ?n ?q \<equiv> (target (stake ?n (w ||| r)) p, ?q) \<in> R

goal (1 subgoal):
 1. \<And>x. x \<in> language A \<Longrightarrow> x \<in> language B
[PROOF STEP]
obtain q where 3: "q \<in> initial B" "(p, q) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q. \<lbrakk>q \<in> initial B; (p, q) \<in> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2) 2(1)
[PROOF STATE]
proof (prove)
using this:
?p \<in> initial A \<Longrightarrow> \<exists>q\<in>initial B. (?p, q) \<in> R
p \<in> initial A

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>q \<in> initial B; (p, q) \<in> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<in> initial B
(p, q) \<in> R

goal (1 subgoal):
 1. \<And>x. x \<in> language A \<Longrightarrow> x \<in> language B
[PROOF STEP]
obtain ws where 4:
      "run B ws q" "\<And> i. P (0 + i) (target (stake i ws) q)" "\<And> i. fst (ws !! i) = w !! (0 + i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (rule nba.invariant_run_index)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?P2 ?n2 ?p2
 2. \<And>n p. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; ?P2 n p\<rbrakk> \<Longrightarrow> \<exists>a. (fst a \<in> alphabet ?A2 \<and> snd a \<in> transition ?A2 (fst a) p) \<and> ?P2 (Suc n) (snd a) \<and> ?Q2 n p a
 3. \<And>r. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; run ?A2 r ?p2; \<And>i. ?P2 (?n2 + i) (target (stake i r) ?p2); \<And>i. ?Q2 (?n2 + i) (target (stake i r) ?p2) (r !! i)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "stake k (w ||| r) @- (w !! k, target (stake (Suc k) (w ||| r)) p) ##
        sdrop (Suc k) (w ||| r) = w ||| r" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stake k (w ||| r) @- (w !! k, target (stake (Suc k) (w ||| r)) p) ## sdrop (Suc k) (w ||| r) = w ||| r
[PROOF STEP]
by (metis id_stake_snth_sdrop snth_szip sscan_snth szip_smap_snd nba.trace_alt_def)
[PROOF STATE]
proof (state)
this:
stake ?k (w ||| r) @- (w !! ?k, target (stake (Suc ?k) (w ||| r)) p) ## sdrop (Suc ?k) (w ||| r) = w ||| r

goal (3 subgoals):
 1. (\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?P2 ?n2 ?p2
 2. \<And>n p. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; ?P2 n p\<rbrakk> \<Longrightarrow> \<exists>a. (fst a \<in> alphabet ?A2 \<and> snd a \<in> transition ?A2 (fst a) p) \<and> ?P2 (Suc n) (snd a) \<and> ?Q2 n p a
 3. \<And>r. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; run ?A2 r ?p2; \<And>i. ?P2 (?n2 + i) (target (stake i r) ?p2); \<And>i. ?Q2 (?n2 + i) (target (stake i r) ?p2) (r !! i)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
stake ?k (w ||| r) @- (w !! ?k, target (stake (Suc ?k) (w ||| r)) p) ## sdrop (Suc ?k) (w ||| r) = w ||| r

goal (3 subgoals):
 1. (\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?P2 ?n2 ?p2
 2. \<And>n p. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; ?P2 n p\<rbrakk> \<Longrightarrow> \<exists>a. (fst a \<in> alphabet ?A2 \<and> snd a \<in> transition ?A2 (fst a) p) \<and> ?P2 (Suc n) (snd a) \<and> ?Q2 n p a
 3. \<And>r. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; run ?A2 r ?p2; \<And>i. ?P2 (?n2 + i) (target (stake i r) ?p2); \<And>i. ?Q2 (?n2 + i) (target (stake i r) ?p2) (r !! i)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "run A \<dots> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run A (w ||| r) p
[PROOF STEP]
using 2(2)
[PROOF STATE]
proof (prove)
using this:
run A (w ||| r) p

goal (1 subgoal):
 1. run A (w ||| r) p
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
run A (w ||| r) p

goal (3 subgoals):
 1. (\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?P2 ?n2 ?p2
 2. \<And>n p. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; ?P2 n p\<rbrakk> \<Longrightarrow> \<exists>a. (fst a \<in> alphabet ?A2 \<and> snd a \<in> transition ?A2 (fst a) p) \<and> ?P2 (Suc n) (snd a) \<and> ?Q2 n p a
 3. \<And>r. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; run ?A2 r ?p2; \<And>i. ?P2 (?n2 + i) (target (stake i r) ?p2); \<And>i. ?Q2 (?n2 + i) (target (stake i r) ?p2) (r !! i)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
run A (stake ?k1 (w ||| r) @- (w !! ?k1, target (stake (Suc ?k1) (w ||| r)) p) ## sdrop (Suc ?k1) (w ||| r)) p
[PROOF STEP]
show "\<exists> a. (fst a \<in> alphabet B \<and> snd a \<in> transition B (fst a) q) \<and>
        P (Suc n) (snd a) \<and> fst a = w !! n" if "P n q" for n q
[PROOF STATE]
proof (prove)
using this:
run A (stake ?k1 (w ||| r) @- (w !! ?k1, target (stake (Suc ?k1) (w ||| r)) p) ## sdrop (Suc ?k1) (w ||| r)) p

goal (1 subgoal):
 1. \<exists>a. (fst a \<in> alphabet B \<and> snd a \<in> transition B (fst a) q) \<and> P (Suc n) (snd a) \<and> fst a = w !! n
[PROOF STEP]
using assms(1, 3) that
[PROOF STATE]
proof (prove)
using this:
run A (stake ?k1 (w ||| r) @- (w !! ?k1, target (stake (Suc ?k1) (w ||| r)) p) ## sdrop (Suc ?k1) (w ||| r)) p
alphabet A \<subseteq> alphabet B
\<lbrakk>?p' \<in> transition A ?a ?p; (?p, ?q) \<in> R\<rbrakk> \<Longrightarrow> \<exists>q'\<in>transition B ?a ?q. (?p', q') \<in> R
P n q

goal (1 subgoal):
 1. \<exists>a. (fst a \<in> alphabet B \<and> snd a \<in> transition B (fst a) q) \<and> P (Suc n) (snd a) \<and> fst a = w !! n
[PROOF STEP]
unfolding P_def
[PROOF STATE]
proof (prove)
using this:
run A (stake ?k1 (w ||| r) @- (w !! ?k1, target (stake (Suc ?k1) (w ||| r)) p) ## sdrop (Suc ?k1) (w ||| r)) p
alphabet A \<subseteq> alphabet B
\<lbrakk>?p' \<in> transition A ?a ?p; (?p, ?q) \<in> R\<rbrakk> \<Longrightarrow> \<exists>q'\<in>transition B ?a ?q. (?p', q') \<in> R
(target (stake n (w ||| r)) p, q) \<in> R

goal (1 subgoal):
 1. \<exists>a. (fst a \<in> alphabet B \<and> snd a \<in> transition B (fst a) q) \<and> (target (stake (Suc n) (w ||| r)) p, snd a) \<in> R \<and> fst a = w !! n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
P ?n ?q \<Longrightarrow> \<exists>a. (fst a \<in> alphabet B \<and> snd a \<in> transition B (fst a) ?q) \<and> P (Suc ?n) (snd a) \<and> fst a = w !! ?n

goal (2 subgoals):
 1. (\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> P ?n2 ?p2
 2. \<And>r. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; run B r ?p2; \<And>i. P (?n2 + i) (target (stake i r) ?p2); \<And>i. fst (r !! i) = w !! (?n2 + i)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show "P 0 q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P 0 q
[PROOF STEP]
unfolding P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (target (stake 0 (w ||| r)) p, q) \<in> R
[PROOF STEP]
using 3(2)
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> R

goal (1 subgoal):
 1. (target (stake 0 (w ||| r)) p, q) \<in> R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P 0 q

goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>ws. \<lbrakk>run B ws q; \<And>i. P (0 + i) (target (stake i ws) q); \<And>i. fst (ws !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis; run B r q; \<And>i. P (0 + i) (target (stake i r) q); \<And>i. fst (r !! i) = w !! (0 + i)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
qed rule
[PROOF STATE]
proof (state)
this:
run B ws q
P (0 + ?i) (target (stake ?i ws) q)
fst (ws !! ?i) = w !! (0 + ?i)

goal (1 subgoal):
 1. \<And>x. x \<in> language A \<Longrightarrow> x \<in> language B
[PROOF STEP]
obtain s where 5: "ws = w ||| s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. ws = w ||| s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 4(3)
[PROOF STATE]
proof (prove)
using this:
fst (ws !! ?i) = w !! (0 + ?i)

goal (1 subgoal):
 1. (\<And>s. ws = w ||| s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis add.left_neutral eqI_snth snth_smap szip_smap)
[PROOF STATE]
proof (state)
this:
ws = w ||| s

goal (1 subgoal):
 1. \<And>x. x \<in> language A \<Longrightarrow> x \<in> language B
[PROOF STEP]
show "w \<in> language B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> language B
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?p \<in> initial B
 2. run B (w ||| ?r) ?p
 3. infs (accepting B) (?p ## ?r)
[PROOF STEP]
show "q \<in> initial B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> initial B
[PROOF STEP]
using 3(1)
[PROOF STATE]
proof (prove)
using this:
q \<in> initial B

goal (1 subgoal):
 1. q \<in> initial B
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
q \<in> initial B

goal (2 subgoals):
 1. run B (w ||| ?r) q
 2. infs (accepting B) (q ## ?r)
[PROOF STEP]
show "run B (w ||| s) q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run B (w ||| s) q
[PROOF STEP]
using 4(1)
[PROOF STATE]
proof (prove)
using this:
run B ws q

goal (1 subgoal):
 1. run B (w ||| s) q
[PROOF STEP]
unfolding 5
[PROOF STATE]
proof (prove)
using this:
run B (w ||| s) q

goal (1 subgoal):
 1. run B (w ||| s) q
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
run B (w ||| s) q

goal (1 subgoal):
 1. infs (accepting B) (q ## s)
[PROOF STEP]
have 6: "(\<lambda> a b. (a, b) \<in> R) \<le> (\<lambda> a b. accepting A a \<longrightarrow> accepting B b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a b. (a, b) \<in> R) \<le> (\<lambda>a b. accepting A a \<longrightarrow> accepting B b)
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?p, ?q) \<in> R; accepting A ?p\<rbrakk> \<Longrightarrow> accepting B ?q

goal (1 subgoal):
 1. (\<lambda>a b. (a, b) \<in> R) \<le> (\<lambda>a b. accepting A a \<longrightarrow> accepting B b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>a b. (a, b) \<in> R) \<le> (\<lambda>a b. accepting A a \<longrightarrow> accepting B b)

goal (1 subgoal):
 1. infs (accepting B) (q ## s)
[PROOF STEP]
have 7: "stream_all2 (\<lambda> p q. (p, q) \<in> R) (trace (w ||| r) p) (trace (w ||| s) q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_all2 (\<lambda>p q. (p, q) \<in> R) (trace (w ||| r) p) (trace (w ||| s) q)
[PROOF STEP]
using 4(2)
[PROOF STATE]
proof (prove)
using this:
P (0 + ?i) (target (stake ?i ws) q)

goal (1 subgoal):
 1. stream_all2 (\<lambda>p q. (p, q) \<in> R) (trace (w ||| r) p) (trace (w ||| s) q)
[PROOF STEP]
unfolding P_def 5
[PROOF STATE]
proof (prove)
using this:
(target (stake (0 + ?i) (w ||| r)) p, target (stake ?i (w ||| s)) q) \<in> R

goal (1 subgoal):
 1. stream_all2 (\<lambda>p q. (p, q) \<in> R) (trace (w ||| r) p) (trace (w ||| s) q)
[PROOF STEP]
by (simp add: stream_rel_snth del: stake.simps(2))
[PROOF STATE]
proof (state)
this:
stream_all2 (\<lambda>p q. (p, q) \<in> R) (trace (w ||| r) p) (trace (w ||| s) q)

goal (1 subgoal):
 1. infs (accepting B) (q ## s)
[PROOF STEP]
have 8: "stream_all2 (\<lambda> a b. accepting A a \<longrightarrow> accepting B b) r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_all2 (\<lambda>a b. accepting A a \<longrightarrow> accepting B b) r s
[PROOF STEP]
using stream.rel_mono 6 7
[PROOF STATE]
proof (prove)
using this:
?R \<le> ?Ra \<Longrightarrow> stream_all2 ?R \<le> stream_all2 ?Ra
(\<lambda>a b. (a, b) \<in> R) \<le> (\<lambda>a b. accepting A a \<longrightarrow> accepting B b)
stream_all2 (\<lambda>p q. (p, q) \<in> R) (trace (w ||| r) p) (trace (w ||| s) q)

goal (1 subgoal):
 1. stream_all2 (\<lambda>a b. accepting A a \<longrightarrow> accepting B b) r s
[PROOF STEP]
unfolding nba.trace_alt_def
[PROOF STATE]
proof (prove)
using this:
?R \<le> ?Ra \<Longrightarrow> stream_all2 ?R \<le> stream_all2 ?Ra
(\<lambda>a b. (a, b) \<in> R) \<le> (\<lambda>a b. accepting A a \<longrightarrow> accepting B b)
stream_all2 (\<lambda>p q. (p, q) \<in> R) (smap snd (w ||| r)) (smap snd (w ||| s))

goal (1 subgoal):
 1. stream_all2 (\<lambda>a b. accepting A a \<longrightarrow> accepting B b) r s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stream_all2 (\<lambda>a b. accepting A a \<longrightarrow> accepting B b) r s

goal (1 subgoal):
 1. infs (accepting B) (q ## s)
[PROOF STEP]
show "infs (accepting B) (q ## s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infs (accepting B) (q ## s)
[PROOF STEP]
using infs_mono_strong 8 2(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>stream_all2 (\<lambda>a b. ?P a \<longrightarrow> ?Q b) ?u ?v; infs ?P ?u\<rbrakk> \<Longrightarrow> infs ?Q ?v
stream_all2 (\<lambda>a b. accepting A a \<longrightarrow> accepting B b) r s
infs (accepting A) (p ## r)

goal (1 subgoal):
 1. infs (accepting B) (q ## s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
infs (accepting B) (q ## s)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
w \<in> language B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_nonempty:
assumes "x \<noteq> []"
shows    "Suc 0 \<le> length x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc 0 \<le> length x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> []

goal (1 subgoal):
 1. Suc 0 \<le> length x
[PROOF STEP]
by (metis length_greater_0_conv less_eq_Suc_le)


[STATEMENT]
lemma left_unique_rel_gpv [transfer_rule]:
  "\<lbrakk> left_unique A; left_unique B \<rbrakk> \<Longrightarrow> left_unique (rel_gpv A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>left_unique A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (rel_gpv A B)
[PROOF STEP]
unfolding left_unique_alt_def gpv.rel_conversep[symmetric] gpv.rel_compp[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A OO A\<inverse>\<inverse> \<le> (=); B OO B\<inverse>\<inverse> \<le> (=)\<rbrakk> \<Longrightarrow> rel_gpv (A OO A\<inverse>\<inverse>) (B OO B\<inverse>\<inverse>) \<le> (=)
[PROOF STEP]
by(subst gpv.rel_eq[symmetric])(rule gpv.rel_mono)