[STATEMENT]
lemma setbydecision_all_append_subset: "simple_ruleset (rs1 @ rs2) \<Longrightarrow>
            setbydecision_all TYPE('pkt_ext) iface rs1 FinalDeny \<union> {ip. \<forall>p :: ('i::len,'pkt_ext) tagged_packet_scheme.
            approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface:=iface_sel iface, p_src := ip\<rparr>) rs2 Undecided = Decision FinalDeny \<and>
            approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface:=iface_sel iface, p_src := ip\<rparr>) rs1 Undecided = Undecided}
            \<subseteq>
            setbydecision_all TYPE('pkt_ext) iface (rs1 @ rs2) FinalDeny"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_ruleset (rs1 @ rs2) \<Longrightarrow> setbydecision_all TYPE('pkt_ext) iface rs1 FinalDeny \<union> {ip. \<forall>p. approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := ip\<rparr>) rs2 Undecided = Decision FinalDeny \<and> approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := ip\<rparr>) rs1 Undecided = Undecided} \<subseteq> setbydecision_all TYPE('pkt_ext) iface (rs1 @ rs2) FinalDeny
[PROOF STEP]
unfolding setbydecision_all_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_ruleset (rs1 @ rs2) \<Longrightarrow> {ip. \<forall>p. approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := ip\<rparr>) rs1 Undecided = Decision FinalDeny} \<union> {ip. \<forall>p. approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := ip\<rparr>) rs2 Undecided = Decision FinalDeny \<and> approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := ip\<rparr>) rs1 Undecided = Undecided} \<subseteq> {ip. \<forall>p. approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := ip\<rparr>) (rs1 @ rs2) Undecided = Decision FinalDeny}
[PROOF STEP]
apply(subst Set.Collect_disj_eq[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_ruleset (rs1 @ rs2) \<Longrightarrow> {x. (\<forall>p. approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) rs1 Undecided = Decision FinalDeny) \<or> (\<forall>p. approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) rs2 Undecided = Decision FinalDeny \<and> approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) rs1 Undecided = Undecided)} \<subseteq> {ip. \<forall>p. approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := ip\<rparr>) (rs1 @ rs2) Undecided = Decision FinalDeny}
[PROOF STEP]
apply(rule Set.Collect_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. simple_ruleset (rs1 @ rs2) \<Longrightarrow> (\<forall>p. approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) rs1 Undecided = Decision FinalDeny) \<or> (\<forall>p. approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) rs2 Undecided = Decision FinalDeny \<and> approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) rs1 Undecided = Undecided) \<longrightarrow> (\<forall>p. approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) (rs1 @ rs2) Undecided = Decision FinalDeny)
[PROOF STEP]
apply(subst approximating_bigstep_fun_seq_Undecided_t_wf)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x p. simple_ruleset (rs1 @ rs2) \<Longrightarrow> wf_ruleset (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) (rs1 @ rs2)
 2. \<And>x. simple_ruleset (rs1 @ rs2) \<Longrightarrow> (\<forall>p. approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) rs1 Undecided = Decision FinalDeny) \<or> (\<forall>p. approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) rs2 Undecided = Decision FinalDeny \<and> approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) rs1 Undecided = Undecided) \<longrightarrow> (\<forall>p. approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) rs1 Undecided = Undecided \<and> approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) rs2 Undecided = Decision FinalDeny \<or> approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) rs1 Undecided = Decision FinalDeny \<and> Decision FinalDeny \<noteq> Undecided)
[PROOF STEP]
apply(simp add: simple_imp_good_ruleset good_imp_wf_ruleset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. simple_ruleset (rs1 @ rs2) \<Longrightarrow> (\<forall>p. approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) rs1 Undecided = Decision FinalDeny) \<or> (\<forall>p. approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) rs2 Undecided = Decision FinalDeny \<and> approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) rs1 Undecided = Undecided) \<longrightarrow> (\<forall>p. approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) rs1 Undecided = Undecided \<and> approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) rs2 Undecided = Decision FinalDeny \<or> approximating_bigstep_fun (common_matcher, in_doubt_allow) (p\<lparr>p_iiface := iface_sel iface, p_src := x\<rparr>) rs1 Undecided = Decision FinalDeny \<and> Decision FinalDeny \<noteq> Undecided)
[PROOF STEP]
apply(simp add: not_FinalAllow)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma add_rat_root_cond:
  shows "root_cond (cf_pos_poly (poly_add_rat m p),l,r) x = root_cond (p, l - m, r - m) (x - of_rat m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root_cond (cf_pos_poly (poly_add_rat m p), l, r) x = root_cond (p, l - m, r - m) (x - real_of_rat m)
[PROOF STEP]
by (unfold root_cond_def, auto simp add: add_rat_roots hom_distribs)


[STATEMENT]
lemma rel_S_neg_distr_imp:
  fixes Co1 :: "'co1 \<Rightarrow> 'co1' \<Rightarrow> bool" and Co1' :: "'co1' \<Rightarrow> 'co1'' \<Rightarrow> bool"
    and Co2 :: "'co2 \<Rightarrow> 'co2' \<Rightarrow> bool" and Co2' :: "'co2' \<Rightarrow> 'co2'' \<Rightarrow> bool"
    and Contra1 :: "'contra1 \<Rightarrow> 'contra1' \<Rightarrow> bool" and Contra1' :: "'contra1' \<Rightarrow> 'contra1'' \<Rightarrow> bool"
    and Contra2 :: "'contra2 \<Rightarrow> 'contra2' \<Rightarrow> bool" and Contra2' :: "'contra2' \<Rightarrow> 'contra2'' \<Rightarrow> bool"
    and tytok_S' :: "('l1 \<times> ('l1 \<times> 'l1'') \<times> 'l1'' \<times> 'l2 \<times> ('l2 \<times> 'l2'') \<times> 'l2'' \<times> 'f) itself"
    and tytok_S :: "('l1 \<times> 'l1' \<times> 'l1'' \<times> 'l2 \<times> 'l2' \<times> 'l2'' \<times> 'f) itself"
  assumes "rel_S_neg_distr_cond' Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_S'"
  shows "rel_S_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_S_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_S
[PROOF STEP]
unfolding rel_S_neg_distr_cond_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>L1 L1' L2 L2'. rel_S (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') \<le> rel_S L1 L2 Co1 Co2 Contra1 Contra2 OO rel_S L1' L2' Co1' Co2' Contra1' Contra2'
[PROOF STEP]
proof (intro allI predicate2I relcomppI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>L1 L1' L2 L2' x y. rel_S (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y \<Longrightarrow> rel_S L1 L2 Co1 Co2 Contra1 Contra2 x (?b5 L1 L1' L2 L2' x y)
 2. \<And>L1 L1' L2 L2' x y. rel_S (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y \<Longrightarrow> rel_S L1' L2' Co1' Co2' Contra1' Contra2' (?b5 L1 L1' L2 L2' x y) y
[PROOF STEP]
fix L1 :: "'l1 \<Rightarrow> 'l1' \<Rightarrow> bool" and L1' :: "'l1' \<Rightarrow> 'l1'' \<Rightarrow> bool"
    and L2 :: "'l2 \<Rightarrow> 'l2' \<Rightarrow> bool" and L2' :: "'l2' \<Rightarrow> 'l2'' \<Rightarrow> bool"
    and x :: "(_, _, _, _, _, _, 'f) S" and y :: "(_, _, _, _, _, _, 'f) S"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>L1 L1' L2 L2' x y. rel_S (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y \<Longrightarrow> rel_S L1 L2 Co1 Co2 Contra1 Contra2 x (?b5 L1 L1' L2 L2' x y)
 2. \<And>L1 L1' L2 L2' x y. rel_S (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y \<Longrightarrow> rel_S L1' L2' Co1' Co2' Contra1' Contra2' (?b5 L1 L1' L2 L2' x y) y
[PROOF STEP]
assume *: "rel_S (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2')
    (Contra1 OO Contra1') (Contra2 OO Contra2') x y"
[PROOF STATE]
proof (state)
this:
rel_S (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y

goal (2 subgoals):
 1. \<And>L1 L1' L2 L2' x y. rel_S (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y \<Longrightarrow> rel_S L1 L2 Co1 Co2 Contra1 Contra2 x (?b5 L1 L1' L2 L2' x y)
 2. \<And>L1 L1' L2 L2' x y. rel_S (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y \<Longrightarrow> rel_S L1' L2' Co1' Co2' Contra1' Contra2' (?b5 L1 L1' L2 L2' x y) y
[PROOF STEP]
let ?z = "map_S (relcompp_witness L1 L1') (relcompp_witness L2 L2') id id id id
    (rel_S_witness' (L1 OO L1') (L2 OO L2') Co1 Co1' Co2 Co2'
    Contra1 Contra1' Contra2 Contra2' (x, y))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>L1 L1' L2 L2' x y. rel_S (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y \<Longrightarrow> rel_S L1 L2 Co1 Co2 Contra1 Contra2 x (?b5 L1 L1' L2 L2' x y)
 2. \<And>L1 L1' L2 L2' x y. rel_S (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y \<Longrightarrow> rel_S L1' L2' Co1' Co2' Contra1' Contra2' (?b5 L1 L1' L2 L2' x y) y
[PROOF STEP]
show "rel_S L1 L2 Co1 Co2 Contra1 Contra2 x ?z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_S L1 L2 Co1 Co2 Contra1 Contra2 x (map_S (relcompp_witness L1 L1') (relcompp_witness L2 L2') id id id id (rel_S_witness' (L1 OO L1') (L2 OO L2') Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (x, y)))
[PROOF STEP]
apply(subst map_S_id[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_S L1 L2 Co1 Co2 Contra1 Contra2 (map_S id id id id id id x) (map_S (relcompp_witness L1 L1') (relcompp_witness L2 L2') id id id id (rel_S_witness' (L1 OO L1') (L2 OO L2') Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (x, y)))
[PROOF STEP]
apply(rule map_S_rel_cong)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. rel_S ?L1.0 ?L2.0 ?Co1.0 ?Co2.0 ?Contra1.0 ?Contra2.0 x (rel_S_witness' (L1 OO L1') (L2 OO L2') Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (x, y))
 2. \<And>x y. ?L1.0 x y \<Longrightarrow> L1 (id x) (relcompp_witness L1 L1' y)
 3. \<And>x y. ?L2.0 x y \<Longrightarrow> L2 (id x) (relcompp_witness L2 L2' y)
 4. \<And>x y. ?Co1.0 x y \<Longrightarrow> Co1 (id x) (id y)
 5. \<And>x y. ?Co2.0 x y \<Longrightarrow> Co2 (id x) (id y)
 6. \<And>x y. Contra1 x y \<Longrightarrow> ?Contra1.0 (id x) (id y)
 7. \<And>x y. Contra2 x y \<Longrightarrow> ?Contra2.0 (id x) (id y)
[PROOF STEP]
apply(rule rel_S_witness'1[OF * assms])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x y. case y of (x', y) \<Rightarrow> x' = x \<and> (L1 OO L1') x y \<Longrightarrow> L1 (id x) (relcompp_witness L1 L1' y)
 2. \<And>x y. case y of (x', y) \<Rightarrow> x' = x \<and> (L2 OO L2') x y \<Longrightarrow> L2 (id x) (relcompp_witness L2 L2' y)
 3. \<And>x y. Co1 x y \<Longrightarrow> Co1 (id x) (id y)
 4. \<And>x y. Co2 x y \<Longrightarrow> Co2 (id x) (id y)
 5. \<And>x y. Contra1 x y \<Longrightarrow> Contra1 (id x) (id y)
 6. \<And>x y. Contra2 x y \<Longrightarrow> Contra2 (id x) (id y)
[PROOF STEP]
apply(auto simp add: vimage2p_def del: relcomppE elim!: relcompp_witness)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
rel_S L1 L2 Co1 Co2 Contra1 Contra2 x (map_S (relcompp_witness L1 L1') (relcompp_witness L2 L2') id id id id (rel_S_witness' (L1 OO L1') (L2 OO L2') Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (x, y)))

goal (1 subgoal):
 1. \<And>L1 L1' L2 L2' x y. rel_S (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y \<Longrightarrow> rel_S L1' L2' Co1' Co2' Contra1' Contra2' (map_S (relcompp_witness L1 L1') (relcompp_witness L2 L2') id id id id (rel_S_witness' (L1 OO L1') (L2 OO L2') Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (x, y))) y
[PROOF STEP]
show "rel_S L1' L2' Co1' Co2' Contra1' Contra2' ?z y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_S L1' L2' Co1' Co2' Contra1' Contra2' (map_S (relcompp_witness L1 L1') (relcompp_witness L2 L2') id id id id (rel_S_witness' (L1 OO L1') (L2 OO L2') Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (x, y))) y
[PROOF STEP]
apply(rewrite in "rel_S _ _ _ _ _ _ _ \<hole>" map_S_id[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_S L1' L2' Co1' Co2' Contra1' Contra2' (map_S (relcompp_witness L1 L1') (relcompp_witness L2 L2') id id id id (rel_S_witness' (L1 OO L1') (L2 OO L2') Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (x, y))) (map_S id id id id id id y)
[PROOF STEP]
apply(rule map_S_rel_cong)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. rel_S ?L1.3 ?L2.3 ?Co1.3 ?Co2.3 ?Contra1.3 ?Contra2.3 (rel_S_witness' (L1 OO L1') (L2 OO L2') Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (x, y)) y
 2. \<And>x y. ?L1.3 x y \<Longrightarrow> L1' (relcompp_witness L1 L1' x) (id y)
 3. \<And>x y. ?L2.3 x y \<Longrightarrow> L2' (relcompp_witness L2 L2' x) (id y)
 4. \<And>x y. ?Co1.3 x y \<Longrightarrow> Co1' (id x) (id y)
 5. \<And>x y. ?Co2.3 x y \<Longrightarrow> Co2' (id x) (id y)
 6. \<And>x y. Contra1' x y \<Longrightarrow> ?Contra1.3 (id x) (id y)
 7. \<And>x y. Contra2' x y \<Longrightarrow> ?Contra2.3 (id x) (id y)
[PROOF STEP]
apply(rule rel_S_witness'2[OF * assms])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x y. (case x of (x, y') \<Rightarrow> \<lambda>y. y' = y \<and> (L1 OO L1') x y) y \<Longrightarrow> L1' (relcompp_witness L1 L1' x) (id y)
 2. \<And>x y. (case x of (x, y') \<Rightarrow> \<lambda>y. y' = y \<and> (L2 OO L2') x y) y \<Longrightarrow> L2' (relcompp_witness L2 L2' x) (id y)
 3. \<And>x y. Co1' x y \<Longrightarrow> Co1' (id x) (id y)
 4. \<And>x y. Co2' x y \<Longrightarrow> Co2' (id x) (id y)
 5. \<And>x y. Contra1' x y \<Longrightarrow> Contra1' (id x) (id y)
 6. \<And>x y. Contra2' x y \<Longrightarrow> Contra2' (id x) (id y)
[PROOF STEP]
apply(auto simp add: vimage2p_def del: relcomppE elim!: relcompp_witness)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
rel_S L1' L2' Co1' Co2' Contra1' Contra2' (map_S (relcompp_witness L1 L1') (relcompp_witness L2 L2') id id id id (rel_S_witness' (L1 OO L1') (L2 OO L2') Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (x, y))) y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma USUP_atLeast_Suc:
  "(\<Squnion> i \<in> {Suc m..} \<bullet> P(i)) = (\<Squnion> i \<in> {m..} \<bullet> P(Suc i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Squnion> i \<in> {Suc m..} \<bullet> P i) = (\<Squnion> i \<in> {m..} \<bullet> P (Suc i))
[PROOF STEP]
by (rel_simp, metis (full_types) Suc_le_D not_less_eq_eq)


[STATEMENT]
lemma upred_eq_true [simp]: "(p =\<^sub>u true) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p =\<^sub>u true) = p
[PROOF STEP]
by (pred_auto)


[STATEMENT]
lemma construct_cycle_post:
  assumes "\<not> q \<noteq> x"
      and "(construct_path_inv q x y D W \<and> D \<le> R \<and> D * x = 0 \<and> y * x\<^sup>T \<le> R)"
    shows "W + y * x\<^sup>T \<noteq> 0 \<and> W + y * x\<^sup>T \<le> R \<and> cycle (W + y * x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W + y * x\<^sup>T \<noteq> 0 \<and> W + y * x\<^sup>T \<le> R \<and> cycle (W + y * x\<^sup>T)
[PROOF STEP]
proof(intro conjI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. W + y * x\<^sup>T \<noteq> 0
 2. W + y * x\<^sup>T \<le> R
 3. path (W + y * x\<^sup>T)
 4. many_strongly_connected (W + y * x\<^sup>T)
[PROOF STEP]
let ?C = "W + y*x\<^sup>T"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. W + y * x\<^sup>T \<noteq> 0
 2. W + y * x\<^sup>T \<le> R
 3. path (W + y * x\<^sup>T)
 4. many_strongly_connected (W + y * x\<^sup>T)
[PROOF STEP]
show "?C \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W + y * x\<^sup>T \<noteq> 0
[PROOF STEP]
by (metis assms acyclic_imp_one_step_different_points(2) no_trivial_inverse point_def ss423bij
              sup_bot.monoid_axioms monoid.left_neutral)
[PROOF STATE]
proof (state)
this:
W + y * x\<^sup>T \<noteq> 0

goal (3 subgoals):
 1. W + y * x\<^sup>T \<le> R
 2. path (W + y * x\<^sup>T)
 3. many_strongly_connected (W + y * x\<^sup>T)
[PROOF STEP]
show "?C \<le> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W + y * x\<^sup>T \<le> R
[PROOF STEP]
using assms(2) order_trans sup.boundedI
[PROOF STATE]
proof (prove)
using this:
(is_acyclic D \<and> point x \<and> point y \<and> point q \<and> D\<^sup>\<star> * q \<le> D\<^sup>T\<^sup>\<star> * x \<and> W \<le> D \<and> terminating_path W \<and> (W = 0) = (q = y) \<and> (W \<noteq> 0) = (q = start_points W \<and> y = end_points W)) \<and> D \<le> R \<and> D * x = 0 \<and> y * x\<^sup>T \<le> R
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z
\<lbrakk>?b \<le> ?a; ?c \<le> ?a\<rbrakk> \<Longrightarrow> ?b + ?c \<le> ?a

goal (1 subgoal):
 1. W + y * x\<^sup>T \<le> R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
W + y * x\<^sup>T \<le> R

goal (2 subgoals):
 1. path (W + y * x\<^sup>T)
 2. many_strongly_connected (W + y * x\<^sup>T)
[PROOF STEP]
show "path (W + y * x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (W + y * x\<^sup>T)
[PROOF STEP]
by (metis assms construct_tree_pre edge_is_path less_eq_def path_edge_equals_cycle
              point_is_point terminating_iff1)
[PROOF STATE]
proof (state)
this:
path (W + y * x\<^sup>T)

goal (1 subgoal):
 1. many_strongly_connected (W + y * x\<^sup>T)
[PROOF STEP]
show "many_strongly_connected (W + y * x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. many_strongly_connected (W + y * x\<^sup>T)
[PROOF STEP]
by (metis assms construct_tree_pre bot_least conv_zero less_eq_def
              path_edge_equals_cycle star_conv star_subid terminating_iff1)
[PROOF STATE]
proof (state)
this:
many_strongly_connected (W + y * x\<^sup>T)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in node_histories) node_order_is_total:
  assumes "e1 \<in> set (history i)"
      and "e2 \<in> set (history i)"
      and "e1 \<noteq> e2"
    shows "e1 \<sqsubset>\<^sup>i e2 \<or> e2 \<sqsubset>\<^sup>i e1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e1 \<sqsubset>\<^sup>i e2 \<or> e2 \<sqsubset>\<^sup>i e1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
e1 \<in> set (history i)
e2 \<in> set (history i)
e1 \<noteq> e2

goal (1 subgoal):
 1. e1 \<sqsubset>\<^sup>i e2 \<or> e2 \<sqsubset>\<^sup>i e1
[PROOF STEP]
unfolding history_order_def
[PROOF STATE]
proof (prove)
using this:
e1 \<in> set (history i)
e2 \<in> set (history i)
e1 \<noteq> e2

goal (1 subgoal):
 1. (\<exists>xs ys zs. xs @ e1 # ys @ e2 # zs = history i) \<or> (\<exists>xs ys zs. xs @ e2 # ys @ e1 # zs = history i)
[PROOF STEP]
by(metis list_split_two_elems histories_distinct)


[STATEMENT]
lemma [iff]: "((c\<^sub>1;c\<^sub>2) \<down> s\<^sub>0) = (c\<^sub>1 \<down> s\<^sub>0 \<and> (\<forall>s\<^sub>1. s\<^sub>0 -c\<^sub>1\<rightarrow> s\<^sub>1 \<longrightarrow> c\<^sub>2 \<down> s\<^sub>1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((c\<^sub>1; c\<^sub>2) \<down> s\<^sub>0) = (c\<^sub>1 \<down> s\<^sub>0 \<and> (\<forall>s\<^sub>1. s\<^sub>0 -c\<^sub>1\<rightarrow> s\<^sub>1 \<longrightarrow> c\<^sub>2 \<down> s\<^sub>1))
[PROOF STEP]
apply(rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (c\<^sub>1; c\<^sub>2) \<down> s\<^sub>0 \<Longrightarrow> c\<^sub>1 \<down> s\<^sub>0 \<and> (\<forall>s\<^sub>1. s\<^sub>0 -c\<^sub>1\<rightarrow> s\<^sub>1 \<longrightarrow> c\<^sub>2 \<down> s\<^sub>1)
 2. c\<^sub>1 \<down> s\<^sub>0 \<and> (\<forall>s\<^sub>1. s\<^sub>0 -c\<^sub>1\<rightarrow> s\<^sub>1 \<longrightarrow> c\<^sub>2 \<down> s\<^sub>1) \<Longrightarrow> (c\<^sub>1; c\<^sub>2) \<down> s\<^sub>0
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. c\<^sub>1 \<down> s\<^sub>0 \<and> (\<forall>s\<^sub>1. s\<^sub>0 -c\<^sub>1\<rightarrow> s\<^sub>1 \<longrightarrow> c\<^sub>2 \<down> s\<^sub>1) \<Longrightarrow> (c\<^sub>1; c\<^sub>2) \<down> s\<^sub>0
 2. (c\<^sub>1; c\<^sub>2) \<down> s\<^sub>0 \<Longrightarrow> c\<^sub>1 \<down> s\<^sub>0 \<and> (\<forall>s\<^sub>1. s\<^sub>0 -c\<^sub>1\<rightarrow> s\<^sub>1 \<longrightarrow> c\<^sub>2 \<down> s\<^sub>1)
[PROOF STEP]
apply(best intro:termi.intros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c\<^sub>1; c\<^sub>2) \<down> s\<^sub>0 \<Longrightarrow> c\<^sub>1 \<down> s\<^sub>0 \<and> (\<forall>s\<^sub>1. s\<^sub>0 -c\<^sub>1\<rightarrow> s\<^sub>1 \<longrightarrow> c\<^sub>2 \<down> s\<^sub>1)
[PROOF STEP]
apply(erule termi.cases)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>f s. \<lbrakk>(c\<^sub>1; c\<^sub>2) = Do f; s\<^sub>0 = s; f s \<noteq> {}\<rbrakk> \<Longrightarrow> c\<^sub>1 \<down> s\<^sub>0 \<and> (\<forall>s\<^sub>1. s\<^sub>0 -c\<^sub>1\<rightarrow> s\<^sub>1 \<longrightarrow> c\<^sub>2 \<down> s\<^sub>1)
 2. \<And>c\<^sub>1' s\<^sub>0' c\<^sub>2'. \<lbrakk>(c\<^sub>1; c\<^sub>2) = (c\<^sub>1'; c\<^sub>2'); s\<^sub>0 = s\<^sub>0'; c\<^sub>1' \<down> s\<^sub>0'; \<forall>s\<^sub>1. s\<^sub>0' -c\<^sub>1'\<rightarrow> s\<^sub>1 \<longrightarrow> c\<^sub>2' \<down> s\<^sub>1\<rbrakk> \<Longrightarrow> c\<^sub>1 \<down> s\<^sub>0 \<and> (\<forall>s\<^sub>1. s\<^sub>0 -c\<^sub>1\<rightarrow> s\<^sub>1 \<longrightarrow> c\<^sub>2 \<down> s\<^sub>1)
 3. \<And>b s c\<^sub>1' c\<^sub>2'. \<lbrakk>(c\<^sub>1; c\<^sub>2) = IF b THEN c\<^sub>1' ELSE c\<^sub>2'; s\<^sub>0 = s; b s; c\<^sub>1' \<down> s\<rbrakk> \<Longrightarrow> c\<^sub>1 \<down> s\<^sub>0 \<and> (\<forall>s\<^sub>1. s\<^sub>0 -c\<^sub>1\<rightarrow> s\<^sub>1 \<longrightarrow> c\<^sub>2 \<down> s\<^sub>1)
 4. \<And>b s c\<^sub>2' c\<^sub>1'. \<lbrakk>(c\<^sub>1; c\<^sub>2) = IF b THEN c\<^sub>1' ELSE c\<^sub>2'; s\<^sub>0 = s; \<not> b s; c\<^sub>2' \<down> s\<rbrakk> \<Longrightarrow> c\<^sub>1 \<down> s\<^sub>0 \<and> (\<forall>s\<^sub>1. s\<^sub>0 -c\<^sub>1\<rightarrow> s\<^sub>1 \<longrightarrow> c\<^sub>2 \<down> s\<^sub>1)
 5. \<And>b s c. \<lbrakk>(c\<^sub>1; c\<^sub>2) = WHILE b DO c; s\<^sub>0 = s; \<not> b s\<rbrakk> \<Longrightarrow> c\<^sub>1 \<down> s\<^sub>0 \<and> (\<forall>s\<^sub>1. s\<^sub>0 -c\<^sub>1\<rightarrow> s\<^sub>1 \<longrightarrow> c\<^sub>2 \<down> s\<^sub>1)
 6. \<And>b s c. \<lbrakk>(c\<^sub>1; c\<^sub>2) = WHILE b DO c; s\<^sub>0 = s; b s; c \<down> s; \<forall>t. s -c\<rightarrow> t \<longrightarrow> WHILE b DO c \<down> t\<rbrakk> \<Longrightarrow> c\<^sub>1 \<down> s\<^sub>0 \<and> (\<forall>s\<^sub>1. s\<^sub>0 -c\<^sub>1\<rightarrow> s\<^sub>1 \<longrightarrow> c\<^sub>2 \<down> s\<^sub>1)
 7. \<And>c f s g. \<lbrakk>(c\<^sub>1; c\<^sub>2) = LOCAL f; c; g; s\<^sub>0 = s; c \<down> f s\<rbrakk> \<Longrightarrow> c\<^sub>1 \<down> s\<^sub>0 \<and> (\<forall>s\<^sub>1. s\<^sub>0 -c\<^sub>1\<rightarrow> s\<^sub>1 \<longrightarrow> c\<^sub>2 \<down> s\<^sub>1)
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma surj_map_IInf: "surj (map_IInf::('a::complete_lattice_with_dual upset \<Rightarrow> 'b::complete_lattice_with_dual upset) \<Rightarrow> ('a \<Rightarrow> 'b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. top_pres ((`) map_IInf)
[PROOF STEP]
by (metis map_us_map_IInf_iff surjI)


[STATEMENT]
lemma next_recvupd_vacant:
  "vacant_upto (c_records (shd s)) t \<Longrightarrow> next_recvupd s \<Longrightarrow> vacant_upto (c_records (shd (stl s))) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>NrecVacantUpto (shd s) t; next_recvupd s\<rbrakk> \<Longrightarrow> NrecVacantUpto (shd (stl s)) t
[PROOF STEP]
by (auto simp add: next_recvupd'_def Let_def)


[STATEMENT]
lemma these_insert[simp]: "Option.these (insert x A) = (case x of Some a \<Rightarrow> insert a | None \<Rightarrow> id) (Option.these A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Option.these (insert x A) = (case x of None \<Rightarrow> id | Some a \<Rightarrow> insert a) (Option.these A)
[PROOF STEP]
by (auto simp: Option.these_def split: option.splits) force


[STATEMENT]
theorem ACI_norm_wf[simp]:
  "wf n \<guillemotleft>r\<guillemotright> = wf n r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.wf n \<guillemotleft>r\<guillemotright> = local.wf n r
[PROOF STEP]
proof (induct r arbitrary: n)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>n. local.wf n \<guillemotleft>Zero\<guillemotright> = local.wf n Zero
 2. \<And>n. local.wf n \<guillemotleft>Full\<guillemotright> = local.wf n Full
 3. \<And>n. local.wf n \<guillemotleft>One\<guillemotright> = local.wf n One
 4. \<And>x n. local.wf n \<guillemotleft>Atom x\<guillemotright> = local.wf n (Atom x)
 5. \<And>r1 r2 n. \<lbrakk>\<And>n. local.wf n \<guillemotleft>r1\<guillemotright> = local.wf n r1; \<And>n. local.wf n \<guillemotleft>r2\<guillemotright> = local.wf n r2\<rbrakk> \<Longrightarrow> local.wf n \<guillemotleft>Plus r1 r2\<guillemotright> = local.wf n (Plus r1 r2)
 6. \<And>r1 r2 n. \<lbrakk>\<And>n. local.wf n \<guillemotleft>r1\<guillemotright> = local.wf n r1; \<And>n. local.wf n \<guillemotleft>r2\<guillemotright> = local.wf n r2\<rbrakk> \<Longrightarrow> local.wf n \<guillemotleft>Times r1 r2\<guillemotright> = local.wf n (Times r1 r2)
 7. \<And>r n. (\<And>n. local.wf n \<guillemotleft>r\<guillemotright> = local.wf n r) \<Longrightarrow> local.wf n \<guillemotleft>Star r\<guillemotright> = local.wf n (Star r)
 8. \<And>r n. (\<And>n. local.wf n \<guillemotleft>r\<guillemotright> = local.wf n r) \<Longrightarrow> local.wf n \<guillemotleft>rexp.Not r\<guillemotright> = local.wf n (rexp.Not r)
 9. \<And>r1 r2 n. \<lbrakk>\<And>n. local.wf n \<guillemotleft>r1\<guillemotright> = local.wf n r1; \<And>n. local.wf n \<guillemotleft>r2\<guillemotright> = local.wf n r2\<rbrakk> \<Longrightarrow> local.wf n \<guillemotleft>rexp.Inter r1 r2\<guillemotright> = local.wf n (rexp.Inter r1 r2)
 10. \<And>r n. (\<And>n. local.wf n \<guillemotleft>r\<guillemotright> = local.wf n r) \<Longrightarrow> local.wf n \<guillemotleft>Pr r\<guillemotright> = local.wf n (Pr r)
[PROOF STEP]
case (Plus r1 r2)
[PROOF STATE]
proof (state)
this:
local.wf ?n \<guillemotleft>r1\<guillemotright> = local.wf ?n r1
local.wf ?n \<guillemotleft>r2\<guillemotright> = local.wf ?n r2

goal (10 subgoals):
 1. \<And>n. local.wf n \<guillemotleft>Zero\<guillemotright> = local.wf n Zero
 2. \<And>n. local.wf n \<guillemotleft>Full\<guillemotright> = local.wf n Full
 3. \<And>n. local.wf n \<guillemotleft>One\<guillemotright> = local.wf n One
 4. \<And>x n. local.wf n \<guillemotleft>Atom x\<guillemotright> = local.wf n (Atom x)
 5. \<And>r1 r2 n. \<lbrakk>\<And>n. local.wf n \<guillemotleft>r1\<guillemotright> = local.wf n r1; \<And>n. local.wf n \<guillemotleft>r2\<guillemotright> = local.wf n r2\<rbrakk> \<Longrightarrow> local.wf n \<guillemotleft>Plus r1 r2\<guillemotright> = local.wf n (Plus r1 r2)
 6. \<And>r1 r2 n. \<lbrakk>\<And>n. local.wf n \<guillemotleft>r1\<guillemotright> = local.wf n r1; \<And>n. local.wf n \<guillemotleft>r2\<guillemotright> = local.wf n r2\<rbrakk> \<Longrightarrow> local.wf n \<guillemotleft>Times r1 r2\<guillemotright> = local.wf n (Times r1 r2)
 7. \<And>r n. (\<And>n. local.wf n \<guillemotleft>r\<guillemotright> = local.wf n r) \<Longrightarrow> local.wf n \<guillemotleft>Star r\<guillemotright> = local.wf n (Star r)
 8. \<And>r n. (\<And>n. local.wf n \<guillemotleft>r\<guillemotright> = local.wf n r) \<Longrightarrow> local.wf n \<guillemotleft>rexp.Not r\<guillemotright> = local.wf n (rexp.Not r)
 9. \<And>r1 r2 n. \<lbrakk>\<And>n. local.wf n \<guillemotleft>r1\<guillemotright> = local.wf n r1; \<And>n. local.wf n \<guillemotleft>r2\<guillemotright> = local.wf n r2\<rbrakk> \<Longrightarrow> local.wf n \<guillemotleft>rexp.Inter r1 r2\<guillemotright> = local.wf n (rexp.Inter r1 r2)
 10. \<And>r n. (\<And>n. local.wf n \<guillemotleft>r\<guillemotright> = local.wf n r) \<Longrightarrow> local.wf n \<guillemotleft>Pr r\<guillemotright> = local.wf n (Pr r)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
local.wf ?n \<guillemotleft>r1\<guillemotright> = local.wf ?n r1
local.wf ?n \<guillemotleft>r2\<guillemotright> = local.wf ?n r2

goal (1 subgoal):
 1. local.wf n \<guillemotleft>Plus r1 r2\<guillemotright> = local.wf n (Plus r1 r2)
[PROOF STEP]
using toplevel_summands_wf[of n "\<guillemotleft>r1\<guillemotright>"] toplevel_summands_wf[of n "\<guillemotleft>r2\<guillemotright>"]
[PROOF STATE]
proof (prove)
using this:
local.wf ?n \<guillemotleft>r1\<guillemotright> = local.wf ?n r1
local.wf ?n \<guillemotleft>r2\<guillemotright> = local.wf ?n r2
local.wf n \<guillemotleft>r1\<guillemotright> = (\<forall>r\<in>toplevel_summands \<guillemotleft>r1\<guillemotright>. local.wf n r)
local.wf n \<guillemotleft>r2\<guillemotright> = (\<forall>r\<in>toplevel_summands \<guillemotleft>r2\<guillemotright>. local.wf n r)

goal (1 subgoal):
 1. local.wf n \<guillemotleft>Plus r1 r2\<guillemotright> = local.wf n (Plus r1 r2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.wf n \<guillemotleft>Plus r1 r2\<guillemotright> = local.wf n (Plus r1 r2)

goal (9 subgoals):
 1. \<And>n. local.wf n \<guillemotleft>Zero\<guillemotright> = local.wf n Zero
 2. \<And>n. local.wf n \<guillemotleft>Full\<guillemotright> = local.wf n Full
 3. \<And>n. local.wf n \<guillemotleft>One\<guillemotright> = local.wf n One
 4. \<And>x n. local.wf n \<guillemotleft>Atom x\<guillemotright> = local.wf n (Atom x)
 5. \<And>r1 r2 n. \<lbrakk>\<And>n. local.wf n \<guillemotleft>r1\<guillemotright> = local.wf n r1; \<And>n. local.wf n \<guillemotleft>r2\<guillemotright> = local.wf n r2\<rbrakk> \<Longrightarrow> local.wf n \<guillemotleft>Times r1 r2\<guillemotright> = local.wf n (Times r1 r2)
 6. \<And>r n. (\<And>n. local.wf n \<guillemotleft>r\<guillemotright> = local.wf n r) \<Longrightarrow> local.wf n \<guillemotleft>Star r\<guillemotright> = local.wf n (Star r)
 7. \<And>r n. (\<And>n. local.wf n \<guillemotleft>r\<guillemotright> = local.wf n r) \<Longrightarrow> local.wf n \<guillemotleft>rexp.Not r\<guillemotright> = local.wf n (rexp.Not r)
 8. \<And>r1 r2 n. \<lbrakk>\<And>n. local.wf n \<guillemotleft>r1\<guillemotright> = local.wf n r1; \<And>n. local.wf n \<guillemotleft>r2\<guillemotright> = local.wf n r2\<rbrakk> \<Longrightarrow> local.wf n \<guillemotleft>rexp.Inter r1 r2\<guillemotright> = local.wf n (rexp.Inter r1 r2)
 9. \<And>r n. (\<And>n. local.wf n \<guillemotleft>r\<guillemotright> = local.wf n r) \<Longrightarrow> local.wf n \<guillemotleft>Pr r\<guillemotright> = local.wf n (Pr r)
[PROOF STEP]
qed auto


[STATEMENT]
lemma unit_ex: "(\<exists>u::unit. P u) = P ()"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>u. P u) = P ()
[PROOF STEP]
by auto


[STATEMENT]
lemma is_cnf_BigAnd: "is_cnf (\<^bold>\<And>ls) \<longleftrightarrow> (\<forall>l \<in> set ls. is_cnf l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_cnf \<^bold>\<And>ls = (\<forall>l\<in>set ls. is_cnf l)
[PROOF STEP]
by(induction ls; simp)


[STATEMENT]
lemma HSem_bot_eq:
  shows "\<lbrace>\<Gamma>\<rbrace>\<bottom> = \<^bold>\<lbrakk>\<Gamma>\<^bold>\<rbrakk>\<^bsub>\<lbrace>\<Gamma>\<rbrace>\<bottom>\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace> \<Gamma> \<rbrace>\<bottom> = \<^bold>\<lbrakk> \<Gamma> \<^bold>\<rbrakk>\<^bsub>\<lbrace> \<Gamma> \<rbrace>\<bottom>\<^esub>
[PROOF STEP]
by (subst HSem_eq) simp


[STATEMENT]
lemma ESem_fresh_cong_below_subset:
  assumes "fv e \<subseteq> S"
  assumes "\<rho> f|` S \<sqsubseteq> \<rho>' f|` S"
  shows "\<lbrakk> e \<rbrakk>\<^bsub>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> e \<rbrakk>\<^bsub>\<rho>'\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk> e \<rbrakk>\<^bsub>\<rho>\<^esub> \<sqsubseteq> \<lbrakk> e \<rbrakk>\<^bsub>\<rho>'\<^esub>
[PROOF STEP]
by (rule ESem_fresh_cong_below[OF  env_restr_below_subset[OF assms]])


[STATEMENT]
lemma \<tau>Red1_conv [iff]:
  "\<tau>Red1g uf P t h (ex, exs) (ex', exs') = (uf,P,t \<turnstile>1 \<langle>ex/exs, h\<rangle> -\<epsilon>\<rightarrow> \<langle>ex'/exs', h\<rangle> \<and> \<tau>Move1 P h (ex, exs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Red1g uf P t h (ex, exs) (ex', exs') = (uf,P,t \<turnstile>1 \<langle>ex/exs,h\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>ex'/exs',h\<rangle> \<and> \<tau>Move1 P h (ex, exs))
[PROOF STEP]
by(simp add: \<tau>Red1g_def)


[STATEMENT]
lemma Prop1B:
  "secure c \<Longrightarrow> \<Turnstile> c : Sec (\<lambda> (r, t) . \<exists> s . (s , c \<Down> r) \<and> s \<approx> t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. secure c \<Longrightarrow>  \<Turnstile> c : Sec (\<lambda>(r, t). \<exists>s. s , c \<Down> r  \<and>  s \<approx> t )
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. secure c \<Longrightarrow>  \<Turnstile> c : Sec (\<lambda>(r, t). \<exists>s. s , c \<Down> r  \<and>  s \<approx> t )
[PROOF STEP]
apply (simp add: VDM_valid_def Sec_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. secure c \<Longrightarrow> \<forall>s t. s , c \<Down> t  \<longrightarrow> (\<forall>r.  s \<approx> r  \<longrightarrow> (\<exists>s. s , c \<Down> t  \<and>  s \<approx> r )) \<and> (\<forall>r. (\<exists>sa. sa , c \<Down> r  \<and>  sa \<approx> s ) \<longrightarrow>  r \<approx> t )
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>secure c; s , c \<Down> t \<rbrakk> \<Longrightarrow> (\<forall>r.  s \<approx> r  \<longrightarrow> (\<exists>s. s , c \<Down> t  \<and>  s \<approx> r )) \<and> (\<forall>r. (\<exists>sa. sa , c \<Down> r  \<and>  sa \<approx> s ) \<longrightarrow>  r \<approx> t )
[PROOF STEP]
apply (unfold secure_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>\<forall>s t ss tt.  s \<approx> t  \<longrightarrow> s , c \<Down> ss  \<longrightarrow> t , c \<Down> tt  \<longrightarrow>  ss \<approx> tt ; s , c \<Down> t \<rbrakk> \<Longrightarrow> (\<forall>r.  s \<approx> r  \<longrightarrow> (\<exists>s. s , c \<Down> t  \<and>  s \<approx> r )) \<and> (\<forall>r. (\<exists>sa. sa , c \<Down> r  \<and>  sa \<approx> s ) \<longrightarrow>  r \<approx> t )
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>\<forall>s t ss tt.  s \<approx> t  \<longrightarrow> s , c \<Down> ss  \<longrightarrow> t , c \<Down> tt  \<longrightarrow>  ss \<approx> tt ; s , c \<Down> t \<rbrakk> \<Longrightarrow> \<forall>r.  s \<approx> r  \<longrightarrow> (\<exists>s. s , c \<Down> t  \<and>  s \<approx> r )
 2. \<And>s t. \<lbrakk>\<forall>s t ss tt.  s \<approx> t  \<longrightarrow> s , c \<Down> ss  \<longrightarrow> t , c \<Down> tt  \<longrightarrow>  ss \<approx> tt ; s , c \<Down> t \<rbrakk> \<Longrightarrow> \<forall>r. (\<exists>sa. sa , c \<Down> r  \<and>  sa \<approx> s ) \<longrightarrow>  r \<approx> t
[PROOF STEP]
apply (rule, rule)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s t r. \<lbrakk>\<forall>s t ss tt.  s \<approx> t  \<longrightarrow> s , c \<Down> ss  \<longrightarrow> t , c \<Down> tt  \<longrightarrow>  ss \<approx> tt ; s , c \<Down> t ;  s \<approx> r \<rbrakk> \<Longrightarrow> \<exists>s. s , c \<Down> t  \<and>  s \<approx> r
 2. \<And>s t. \<lbrakk>\<forall>s t ss tt.  s \<approx> t  \<longrightarrow> s , c \<Down> ss  \<longrightarrow> t , c \<Down> tt  \<longrightarrow>  ss \<approx> tt ; s , c \<Down> t \<rbrakk> \<Longrightarrow> \<forall>r. (\<exists>sa. sa , c \<Down> r  \<and>  sa \<approx> s ) \<longrightarrow>  r \<approx> t
[PROOF STEP]
apply (rule_tac x=s in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s t r. \<lbrakk>\<forall>s t ss tt.  s \<approx> t  \<longrightarrow> s , c \<Down> ss  \<longrightarrow> t , c \<Down> tt  \<longrightarrow>  ss \<approx> tt ; s , c \<Down> t ;  s \<approx> r \<rbrakk> \<Longrightarrow> s , c \<Down> t  \<and>  s \<approx> r
 2. \<And>s t. \<lbrakk>\<forall>s t ss tt.  s \<approx> t  \<longrightarrow> s , c \<Down> ss  \<longrightarrow> t , c \<Down> tt  \<longrightarrow>  ss \<approx> tt ; s , c \<Down> t \<rbrakk> \<Longrightarrow> \<forall>r. (\<exists>sa. sa , c \<Down> r  \<and>  sa \<approx> s ) \<longrightarrow>  r \<approx> t
[PROOF STEP]
apply(rule, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>\<forall>s t ss tt.  s \<approx> t  \<longrightarrow> s , c \<Down> ss  \<longrightarrow> t , c \<Down> tt  \<longrightarrow>  ss \<approx> tt ; s , c \<Down> t \<rbrakk> \<Longrightarrow> \<forall>r. (\<exists>sa. sa , c \<Down> r  \<and>  sa \<approx> s ) \<longrightarrow>  r \<approx> t
[PROOF STEP]
apply (rule, rule, erule exE, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t r sa. \<lbrakk>\<forall>s t ss tt.  s \<approx> t  \<longrightarrow> s , c \<Down> ss  \<longrightarrow> t , c \<Down> tt  \<longrightarrow>  ss \<approx> tt ; s , c \<Down> t ; sa , c \<Down> r ;  sa \<approx> s \<rbrakk> \<Longrightarrow>  r \<approx> t
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma powr_less_cancel2: "0 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> x.^a < y.^a \<Longrightarrow> x < y"
  for a x y ::real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < a; 0 < x; 0 < y; x .^ a < y .^ a\<rbrakk> \<Longrightarrow> x < y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 < a; 0 < x; 0 < y; x .^ a < y .^ a\<rbrakk> \<Longrightarrow> x < y
[PROOF STEP]
assume a_pos: "0 < a" and x_pos: "0 < x" and y_pos: "0 < y"
[PROOF STATE]
proof (state)
this:
0 < a
0 < x
0 < y

goal (1 subgoal):
 1. \<lbrakk>0 < a; 0 < x; 0 < y; x .^ a < y .^ a\<rbrakk> \<Longrightarrow> x < y
[PROOF STEP]
show "x.^a < y.^a \<Longrightarrow> x < y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x .^ a < y .^ a \<Longrightarrow> x < y
[PROOF STEP]
proof (erule contrapos_pp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> \<not> x .^ a < y .^ a
[PROOF STEP]
assume "\<not> x < y"
[PROOF STATE]
proof (state)
this:
\<not> x < y

goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> \<not> x .^ a < y .^ a
[PROOF STEP]
hence "x \<ge> y"
[PROOF STATE]
proof (prove)
using this:
\<not> x < y

goal (1 subgoal):
 1. y \<le> x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
y \<le> x

goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> \<not> x .^ a < y .^ a
[PROOF STEP]
hence "x.^a \<ge> y.^a"
[PROOF STATE]
proof (prove)
using this:
y \<le> x

goal (1 subgoal):
 1. y .^ a \<le> x .^ a
[PROOF STEP]
proof (cases "x = y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>y \<le> x; x = y\<rbrakk> \<Longrightarrow> y .^ a \<le> x .^ a
 2. \<lbrakk>y \<le> x; x \<noteq> y\<rbrakk> \<Longrightarrow> y .^ a \<le> x .^ a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = y

goal (2 subgoals):
 1. \<lbrakk>y \<le> x; x = y\<rbrakk> \<Longrightarrow> y .^ a \<le> x .^ a
 2. \<lbrakk>y \<le> x; x \<noteq> y\<rbrakk> \<Longrightarrow> y .^ a \<le> x .^ a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = y

goal (1 subgoal):
 1. y .^ a \<le> x .^ a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y .^ a \<le> x .^ a

goal (1 subgoal):
 1. \<lbrakk>y \<le> x; x \<noteq> y\<rbrakk> \<Longrightarrow> y .^ a \<le> x .^ a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>y \<le> x; x \<noteq> y\<rbrakk> \<Longrightarrow> y .^ a \<le> x .^ a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. \<lbrakk>y \<le> x; x \<noteq> y\<rbrakk> \<Longrightarrow> y .^ a \<le> x .^ a
[PROOF STEP]
hence "x.^a > y.^a"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y

goal (1 subgoal):
 1. y .^ a < x .^ a
[PROOF STEP]
using \<open>x \<ge> y\<close> powr_less_mono2 a_pos y_pos
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
y \<le> x
\<lbrakk>0 < ?a; 0 \<le> ?x; ?x < ?y\<rbrakk> \<Longrightarrow> ?x .^ ?a < ?y .^ ?a
0 < a
0 < y

goal (1 subgoal):
 1. y .^ a < x .^ a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y .^ a < x .^ a

goal (1 subgoal):
 1. \<lbrakk>y \<le> x; x \<noteq> y\<rbrakk> \<Longrightarrow> y .^ a \<le> x .^ a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
y .^ a < x .^ a

goal (1 subgoal):
 1. y .^ a \<le> x .^ a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y .^ a \<le> x .^ a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
y .^ a \<le> x .^ a

goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> \<not> x .^ a < y .^ a
[PROOF STEP]
thus "\<not> x.^a < y.^a"
[PROOF STATE]
proof (prove)
using this:
y .^ a \<le> x .^ a

goal (1 subgoal):
 1. \<not> x .^ a < y .^ a
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<not> x .^ a < y .^ a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x .^ a < y .^ a \<Longrightarrow> x < y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma addO_exp\<omega>_inj:
  assumes "addO n (exp\<omega> m) = addO n' (exp\<omega> m')"
  shows "n = n'" and "m = m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = n' &&& m = m'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = n'
 2. m = m'
[PROOF STEP]
have "addO n (exp\<omega> m) = addO n' (exp\<omega> m') \<Longrightarrow> n = n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addO n (exp\<omega> m) = addO n' (exp\<omega> m') \<Longrightarrow> n = n'
[PROOF STEP]
by (induct m arbitrary: m'; case_tac m';
      force simp: \<omega>_def dest!: fun_cong[of _ _ 1])
[PROOF STATE]
proof (state)
this:
addO n (exp\<omega> m) = addO n' (exp\<omega> m') \<Longrightarrow> n = n'

goal (2 subgoals):
 1. n = n'
 2. m = m'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
addO n (exp\<omega> m) = addO n' (exp\<omega> m') \<Longrightarrow> n = n'

goal (2 subgoals):
 1. n = n'
 2. m = m'
[PROOF STEP]
have "addO n (exp\<omega> m) = addO n (exp\<omega> m') \<Longrightarrow> m = m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addO n (exp\<omega> m) = addO n (exp\<omega> m') \<Longrightarrow> m = m'
[PROOF STEP]
apply (induct m arbitrary: n m'; case_tac m')
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>n m'. \<lbrakk>addO n (exp\<omega> Z) = addO n (exp\<omega> m'); m' = Z\<rbrakk> \<Longrightarrow> Z = m'
 2. \<And>n m' x2. \<lbrakk>addO n (exp\<omega> Z) = addO n (exp\<omega> m'); m' = S x2\<rbrakk> \<Longrightarrow> Z = m'
 3. \<And>n m' x3. \<lbrakk>addO n (exp\<omega> Z) = addO n (exp\<omega> m'); m' = L x3\<rbrakk> \<Longrightarrow> Z = m'
 4. \<And>m n m'. \<lbrakk>\<And>n m'. addO n (exp\<omega> m) = addO n (exp\<omega> m') \<Longrightarrow> m = m'; addO n (exp\<omega> (S m)) = addO n (exp\<omega> m'); m' = Z\<rbrakk> \<Longrightarrow> S m = m'
 5. \<And>m n m' x2. \<lbrakk>\<And>n m'. addO n (exp\<omega> m) = addO n (exp\<omega> m') \<Longrightarrow> m = m'; addO n (exp\<omega> (S m)) = addO n (exp\<omega> m'); m' = S x2\<rbrakk> \<Longrightarrow> S m = m'
 6. \<And>m n m' x3. \<lbrakk>\<And>n m'. addO n (exp\<omega> m) = addO n (exp\<omega> m') \<Longrightarrow> m = m'; addO n (exp\<omega> (S m)) = addO n (exp\<omega> m'); m' = L x3\<rbrakk> \<Longrightarrow> S m = m'
 7. \<And>x n m'. \<lbrakk>\<And>xa n m'. \<lbrakk>xa \<in> range x; addO n (exp\<omega> xa) = addO n (exp\<omega> m')\<rbrakk> \<Longrightarrow> xa = m'; addO n (exp\<omega> (L x)) = addO n (exp\<omega> m'); m' = Z\<rbrakk> \<Longrightarrow> L x = m'
 8. \<And>x n m' x2. \<lbrakk>\<And>xa n m'. \<lbrakk>xa \<in> range x; addO n (exp\<omega> xa) = addO n (exp\<omega> m')\<rbrakk> \<Longrightarrow> xa = m'; addO n (exp\<omega> (L x)) = addO n (exp\<omega> m'); m' = S x2\<rbrakk> \<Longrightarrow> L x = m'
 9. \<And>x n m' x3. \<lbrakk>\<And>xa n m'. \<lbrakk>xa \<in> range x; addO n (exp\<omega> xa) = addO n (exp\<omega> m')\<rbrakk> \<Longrightarrow> xa = m'; addO n (exp\<omega> (L x)) = addO n (exp\<omega> m'); m' = L x3\<rbrakk> \<Longrightarrow> L x = m'
[PROOF STEP]
apply (auto 0 3 simp: \<omega>_def intro: rangeI
      dest: arg_cong[of _ _ "evalO 1"] fun_cong[of _ _ 0] fun_cong[of _ _ 1])[8]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x n m' x3. \<lbrakk>\<And>xa n m'. \<lbrakk>xa \<in> range x; addO n (exp\<omega> xa) = addO n (exp\<omega> m')\<rbrakk> \<Longrightarrow> xa = m'; addO n (exp\<omega> (L x)) = addO n (exp\<omega> m'); m' = L x3\<rbrakk> \<Longrightarrow> L x = m'
[PROOF STEP]
(* 1 left *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x n m' x3. \<lbrakk>\<And>xa n m'. \<lbrakk>xa \<in> range x; addO n (exp\<omega> xa) = addO n (exp\<omega> m')\<rbrakk> \<Longrightarrow> xa = m'; addO n (exp\<omega> (L x)) = addO n (exp\<omega> m'); m' = L x3\<rbrakk> \<Longrightarrow> L x = m'
[PROOF STEP]
by simp (meson ext rangeI)
[PROOF STATE]
proof (state)
this:
addO n (exp\<omega> m) = addO n (exp\<omega> m') \<Longrightarrow> m = m'

goal (2 subgoals):
 1. n = n'
 2. m = m'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
addO n (exp\<omega> m) = addO n' (exp\<omega> m') \<Longrightarrow> n = n'
addO n (exp\<omega> m) = addO n (exp\<omega> m') \<Longrightarrow> m = m'
[PROOF STEP]
show "n = n'" and "m = m'"
[PROOF STATE]
proof (prove)
using this:
addO n (exp\<omega> m) = addO n' (exp\<omega> m') \<Longrightarrow> n = n'
addO n (exp\<omega> m) = addO n (exp\<omega> m') \<Longrightarrow> m = m'

goal (1 subgoal):
 1. n = n' &&& m = m'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
addO n (exp\<omega> m) = addO n' (exp\<omega> m') \<Longrightarrow> n = n'
addO n (exp\<omega> m) = addO n (exp\<omega> m') \<Longrightarrow> m = m'
addO n (exp\<omega> m) = addO n' (exp\<omega> m')

goal (1 subgoal):
 1. n = n' &&& m = m'
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
n = n'
m = m'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ruleSet:
assumes "R' \<subseteq> upRules"
    and "R = Ax \<union> R'"
    and "(Ps,C) \<in> R*"
shows "\<exists> S r. extendRule S r = (Ps,C) \<and> (r \<in> R' \<or> r \<in> Ax)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>S r. extendRule S r = (Ps, C) \<and> (r \<in> R' \<or> r \<in> Ax)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>S r. extendRule S r = (Ps, C) \<and> (r \<in> R' \<or> r \<in> Ax)
[PROOF STEP]
from \<open>(Ps,C) \<in> R*\<close>
[PROOF STATE]
proof (chain)
picking this:
(Ps, C) \<in> R*
[PROOF STEP]
have "\<exists> S r. extendRule S r = (Ps,C) \<and> r \<in> R"
[PROOF STATE]
proof (prove)
using this:
(Ps, C) \<in> R*

goal (1 subgoal):
 1. \<exists>S r. extendRule S r = (Ps, C) \<and> r \<in> R
[PROOF STEP]
by (cases) auto
[PROOF STATE]
proof (state)
this:
\<exists>S r. extendRule S r = (Ps, C) \<and> r \<in> R

goal (1 subgoal):
 1. \<exists>S r. extendRule S r = (Ps, C) \<and> (r \<in> R' \<or> r \<in> Ax)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>S r. extendRule S r = (Ps, C) \<and> r \<in> R
[PROOF STEP]
obtain S r where "(Ps,C) = extendRule S r" and "r \<in> R"
[PROOF STATE]
proof (prove)
using this:
\<exists>S r. extendRule S r = (Ps, C) \<and> r \<in> R

goal (1 subgoal):
 1. (\<And>S r. \<lbrakk>(Ps, C) = extendRule S r; r \<in> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S a b. \<lbrakk>\<And>S a b. \<lbrakk>(Ps, C) = extendRule S (a, b); (a, b) \<in> R\<rbrakk> \<Longrightarrow> thesis; extendRule S (a, b) = (Ps, C); (a, b) \<in> R\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (drule_tac x=S in meta_spec,drule_tac x=a in meta_spec, drule_tac x=b in meta_spec) auto
[PROOF STATE]
proof (state)
this:
(Ps, C) = extendRule S r
r \<in> R

goal (1 subgoal):
 1. \<exists>S r. extendRule S r = (Ps, C) \<and> (r \<in> R' \<or> r \<in> Ax)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(Ps, C) = extendRule S r
r \<in> R

goal (1 subgoal):
 1. \<exists>S r. extendRule S r = (Ps, C) \<and> (r \<in> R' \<or> r \<in> Ax)
[PROOF STEP]
from \<open>r \<in> R\<close> and \<open>R = Ax \<union> R'\<close>
[PROOF STATE]
proof (chain)
picking this:
r \<in> R
R = Ax \<union> R'
[PROOF STEP]
have "r \<in> Ax \<or> r \<in> R'"
[PROOF STATE]
proof (prove)
using this:
r \<in> R
R = Ax \<union> R'

goal (1 subgoal):
 1. r \<in> Ax \<or> r \<in> R'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r \<in> Ax \<or> r \<in> R'

goal (1 subgoal):
 1. \<exists>S r. extendRule S r = (Ps, C) \<and> (r \<in> R' \<or> r \<in> Ax)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(Ps, C) = extendRule S r
r \<in> R
r \<in> Ax \<or> r \<in> R'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(Ps, C) = extendRule S r
r \<in> R
r \<in> Ax \<or> r \<in> R'

goal (1 subgoal):
 1. \<exists>S r. extendRule S r = (Ps, C) \<and> (r \<in> R' \<or> r \<in> Ax)
[PROOF STEP]
by (rule_tac x=S in exI,rule_tac x=r in exI) (auto)
[PROOF STATE]
proof (state)
this:
\<exists>S r. extendRule S r = (Ps, C) \<and> (r \<in> R' \<or> r \<in> Ax)

goal:
No subgoals!
[PROOF STEP]
qed