[STATEMENT]
theorem BenOr_termination:
  shows "\<exists>r v. decide (rho r p) = Some v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
from comm_global
[PROOF STATE]
proof (chain)
picking this:
BenOr_commGlobal HOs
[PROOF STEP]
obtain r1 where r1:
    "\<forall>q. HOs r1 p = HOs r1 q"
    "\<forall>q. (coin r1 p :: val) = coin r1 q"
    "two_step r1 = 1"
[PROOF STATE]
proof (prove)
using this:
BenOr_commGlobal HOs

goal (1 subgoal):
 1. (\<And>r1. \<lbrakk>\<forall>q. HOs r1 p = HOs r1 q; \<forall>q. coin r1 p = coin r1 q; two_step r1 = 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(simp add: BenOr_commGlobal_def all_conj_distrib, blast)
[PROOF STATE]
proof (state)
this:
\<forall>q. HOs r1 p = HOs r1 q
\<forall>q. coin r1 p = coin r1 q
two_step r1 = 1

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
from r1
[PROOF STATE]
proof (chain)
picking this:
\<forall>q. HOs r1 p = HOs r1 q
\<forall>q. coin r1 p = coin r1 q
two_step r1 = 1
[PROOF STEP]
obtain r0 where r1_def: "r1 = Suc r0" and step_r0: "two_step r0 = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>q. HOs r1 p = HOs r1 q
\<forall>q. coin r1 p = coin r1 q
two_step r1 = 1

goal (1 subgoal):
 1. (\<And>r0. \<lbrakk>r1 = Suc r0; two_step r0 = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases r1) (auto simp add: two_step_phase_Suc two_step_def mod_Suc)
[PROOF STATE]
proof (state)
this:
r1 = Suc r0
two_step r0 = 0

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
define cfg0 where "cfg0 = rho r0"
[PROOF STATE]
proof (state)
this:
cfg0 = rho r0

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
define cfg1 where "cfg1 = rho r1"
[PROOF STATE]
proof (state)
this:
cfg1 = rho r1

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
define r2 where "r2 = Suc r1"
[PROOF STATE]
proof (state)
this:
r2 = Suc r1

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
define cfg2 where "cfg2 = rho r2"
[PROOF STATE]
proof (state)
this:
cfg2 = rho r2

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
define r3 where "r3 = Suc r2"
[PROOF STATE]
proof (state)
this:
r3 = Suc r2

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
define cfg3 where "cfg3 = rho r3"
[PROOF STATE]
proof (state)
this:
cfg3 = rho r3

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
define cfg4 where "cfg4 = rho (Suc r3)"
[PROOF STATE]
proof (state)
this:
cfg4 = rho (Suc r3)

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
have step_r2: "two_step r2 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. two_step r2 = 0
[PROOF STEP]
using r1
[PROOF STATE]
proof (prove)
using this:
\<forall>q. HOs r1 p = HOs r1 q
\<forall>q. coin r1 p = coin r1 q
two_step r1 = 1

goal (1 subgoal):
 1. two_step r2 = 0
[PROOF STEP]
by(auto simp add: r2_def two_step_phase_Suc)
[PROOF STATE]
proof (state)
this:
two_step r2 = 0

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
from
    run[simplified HORun_def SHORun_def, THEN CSHORun_step, THEN spec, where x="r0"]
    run[simplified HORun_def SHORun_def, THEN CSHORun_step, THEN spec, where x="r1"]
    run[simplified HORun_def SHORun_def, THEN CSHORun_step, THEN spec, where x="r2"]
    run[simplified HORun_def SHORun_def, THEN CSHORun_step, THEN spec, where x="r3"]
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<mu>. \<forall>p. \<mu> p \<in> get_msgs (sendMsg BenOr_A r0) (rho r0) (HOs r0) (HOs r0) p \<and> CnextState BenOr_A r0 p (rho r0 p) (\<mu> p) undefined (rho (Suc r0) p)
\<exists>\<mu>. \<forall>p. \<mu> p \<in> get_msgs (sendMsg BenOr_A r1) (rho r1) (HOs r1) (HOs r1) p \<and> CnextState BenOr_A r1 p (rho r1 p) (\<mu> p) undefined (rho (Suc r1) p)
\<exists>\<mu>. \<forall>p. \<mu> p \<in> get_msgs (sendMsg BenOr_A r2) (rho r2) (HOs r2) (HOs r2) p \<and> CnextState BenOr_A r2 p (rho r2 p) (\<mu> p) undefined (rho (Suc r2) p)
\<exists>\<mu>. \<forall>p. \<mu> p \<in> get_msgs (sendMsg BenOr_A r3) (rho r3) (HOs r3) (HOs r3) p \<and> CnextState BenOr_A r3 p (rho r3 p) (\<mu> p) undefined (rho (Suc r3) p)
[PROOF STEP]
obtain \<mu>0 \<mu>1 \<mu>2 \<mu>3 where
    send0: "\<forall>p. \<mu>0 p \<in> get_msgs (send0 r0) cfg0 (HOs r0) (HOs r0) p"
    and step0: "\<forall>p. next0 r0 p (cfg0 p) (\<mu>0 p) (cfg1 p)"
    and send1: "\<forall>p. \<mu>1 p \<in> get_msgs (send1 r1) cfg1 (HOs r1) (HOs r1) p"
    and step1: "\<forall>p. next1 r1 p (cfg1 p) (\<mu>1 p) (cfg2 p)"
    and send2: "\<forall>p. \<mu>2 p \<in> get_msgs (send0 r2) cfg2 (HOs r2) (HOs r2) p"
    and step2: "\<forall>p. next0 r2 p (cfg2 p) (\<mu>2 p) (cfg3 p)"
    and send3: "\<forall>p. \<mu>3 p \<in> get_msgs (send1 r3) cfg3 (HOs r3) (HOs r3) p"
    and step3: "\<forall>p. next1 r3 p (cfg3 p) (\<mu>3 p) (cfg4 p)"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<mu>. \<forall>p. \<mu> p \<in> get_msgs (sendMsg BenOr_A r0) (rho r0) (HOs r0) (HOs r0) p \<and> CnextState BenOr_A r0 p (rho r0 p) (\<mu> p) undefined (rho (Suc r0) p)
\<exists>\<mu>. \<forall>p. \<mu> p \<in> get_msgs (sendMsg BenOr_A r1) (rho r1) (HOs r1) (HOs r1) p \<and> CnextState BenOr_A r1 p (rho r1 p) (\<mu> p) undefined (rho (Suc r1) p)
\<exists>\<mu>. \<forall>p. \<mu> p \<in> get_msgs (sendMsg BenOr_A r2) (rho r2) (HOs r2) (HOs r2) p \<and> CnextState BenOr_A r2 p (rho r2 p) (\<mu> p) undefined (rho (Suc r2) p)
\<exists>\<mu>. \<forall>p. \<mu> p \<in> get_msgs (sendMsg BenOr_A r3) (rho r3) (HOs r3) (HOs r3) p \<and> CnextState BenOr_A r3 p (rho r3 p) (\<mu> p) undefined (rho (Suc r3) p)

goal (1 subgoal):
 1. (\<And>\<mu>0 \<mu>1 \<mu>2 \<mu>3. \<lbrakk>\<forall>p. \<mu>0 p \<in> get_msgs (send0 r0) cfg0 (HOs r0) (HOs r0) p; \<forall>p. next0 r0 p (cfg0 p) (\<mu>0 p) (cfg1 p); \<forall>p. \<mu>1 p \<in> get_msgs (send1 r1) cfg1 (HOs r1) (HOs r1) p; \<forall>p. next1 r1 p (cfg1 p) (\<mu>1 p) (cfg2 p); \<forall>p. \<mu>2 p \<in> get_msgs (send0 r2) cfg2 (HOs r2) (HOs r2) p; \<forall>p. next0 r2 p (cfg2 p) (\<mu>2 p) (cfg3 p); \<forall>p. \<mu>3 p \<in> get_msgs (send1 r3) cfg3 (HOs r3) (HOs r3) p; \<forall>p. next1 r3 p (cfg3 p) (\<mu>3 p) (cfg4 p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: BenOr_A_def BenOr_HOMachine_def
      two_step_phase_Suc BenOr_nextState_def BenOr_sendMsg_def all_conj_distrib
      CHOAlgorithm.truncate_def step_r0 r1_def r2_def r3_def
      cfg0_def cfg1_def cfg2_def cfg3_def cfg4_def
      )
[PROOF STATE]
proof (state)
this:
\<forall>p. \<mu>0 p \<in> get_msgs (send0 r0) cfg0 (HOs r0) (HOs r0) p
\<forall>p. next0 r0 p (cfg0 p) (\<mu>0 p) (cfg1 p)
\<forall>p. \<mu>1 p \<in> get_msgs (send1 r1) cfg1 (HOs r1) (HOs r1) p
\<forall>p. next1 r1 p (cfg1 p) (\<mu>1 p) (cfg2 p)
\<forall>p. \<mu>2 p \<in> get_msgs (send0 r2) cfg2 (HOs r2) (HOs r2) p
\<forall>p. next0 r2 p (cfg2 p) (\<mu>2 p) (cfg3 p)
\<forall>p. \<mu>3 p \<in> get_msgs (send1 r3) cfg3 (HOs r3) (HOs r3) p
\<forall>p. next1 r3 p (cfg3 p) (\<mu>3 p) (cfg4 p)

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
let ?v = "x (cfg2 p)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
from per_rd r1
[PROOF STATE]
proof (chain)
picking this:
\<forall>r. BenOr_commPerRd (HOs r)
\<forall>q. HOs r1 p = HOs r1 q
\<forall>q. coin r1 p = coin r1 q
two_step r1 = 1
[PROOF STEP]
have xs: "\<forall>q. x (cfg2 q) = ?v"
[PROOF STATE]
proof (prove)
using this:
\<forall>r. BenOr_commPerRd (HOs r)
\<forall>q. HOs r1 p = HOs r1 q
\<forall>q. coin r1 p = coin r1 q
two_step r1 = 1

goal (1 subgoal):
 1. \<forall>q. x (cfg2 q) = x (cfg2 p)
[PROOF STEP]
proof(cases "\<exists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>r. BenOr_commPerRd (HOs r); \<forall>q. HOs r1 p = HOs r1 q; \<forall>q. coin r1 p = coin r1 q; two_step r1 = 1; \<exists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w\<rbrakk> \<Longrightarrow> \<forall>q. x (cfg2 q) = x (cfg2 p)
 2. \<lbrakk>\<forall>r. BenOr_commPerRd (HOs r); \<forall>q. HOs r1 p = HOs r1 q; \<forall>q. coin r1 p = coin r1 q; two_step r1 = 1; \<nexists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w\<rbrakk> \<Longrightarrow> \<forall>q. x (cfg2 q) = x (cfg2 p)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w

goal (2 subgoals):
 1. \<lbrakk>\<forall>r. BenOr_commPerRd (HOs r); \<forall>q. HOs r1 p = HOs r1 q; \<forall>q. coin r1 p = coin r1 q; two_step r1 = 1; \<exists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w\<rbrakk> \<Longrightarrow> \<forall>q. x (cfg2 q) = x (cfg2 p)
 2. \<lbrakk>\<forall>r. BenOr_commPerRd (HOs r); \<forall>q. HOs r1 p = HOs r1 q; \<forall>q. coin r1 p = coin r1 q; two_step r1 = 1; \<nexists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w\<rbrakk> \<Longrightarrow> \<forall>q. x (cfg2 q) = x (cfg2 p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w
[PROOF STEP]
obtain q w where q_w: "q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w"
[PROOF STATE]
proof (prove)
using this:
\<exists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w

goal (1 subgoal):
 1. (\<And>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w

goal (2 subgoals):
 1. \<lbrakk>\<forall>r. BenOr_commPerRd (HOs r); \<forall>q. HOs r1 p = HOs r1 q; \<forall>q. coin r1 p = coin r1 q; two_step r1 = 1; \<exists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w\<rbrakk> \<Longrightarrow> \<forall>q. x (cfg2 q) = x (cfg2 p)
 2. \<lbrakk>\<forall>r. BenOr_commPerRd (HOs r); \<forall>q. HOs r1 p = HOs r1 q; \<forall>q. coin r1 p = coin r1 q; two_step r1 = 1; \<nexists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w\<rbrakk> \<Longrightarrow> \<forall>q. x (cfg2 q) = x (cfg2 p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w
[PROOF STEP]
have "\<forall>q'. vote (cfg1 q') \<in> {None, Some w}"
[PROOF STATE]
proof (prove)
using this:
q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w

goal (1 subgoal):
 1. \<forall>q'. vote (cfg1 q') \<in> {None, Some w}
[PROOF STEP]
using  same_new_vote[OF send0 step0 step_r0]
[PROOF STATE]
proof (prove)
using this:
q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w
(\<And>v. \<forall>p w. vote (cfg1 p) = Some w \<longrightarrow> w = v \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<forall>q'. vote (cfg1 q') \<in> {None, Some w}
[PROOF STEP]
by (metis insert_iff not_None_eq)
[PROOF STATE]
proof (state)
this:
\<forall>q'. vote (cfg1 q') \<in> {None, Some w}

goal (2 subgoals):
 1. \<lbrakk>\<forall>r. BenOr_commPerRd (HOs r); \<forall>q. HOs r1 p = HOs r1 q; \<forall>q. coin r1 p = coin r1 q; two_step r1 = 1; \<exists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w\<rbrakk> \<Longrightarrow> \<forall>q. x (cfg2 q) = x (cfg2 p)
 2. \<lbrakk>\<forall>r. BenOr_commPerRd (HOs r); \<forall>q. HOs r1 p = HOs r1 q; \<forall>q. coin r1 p = coin r1 q; two_step r1 = 1; \<nexists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w\<rbrakk> \<Longrightarrow> \<forall>q. x (cfg2 q) = x (cfg2 p)
[PROOF STEP]
hence "\<forall>q'. x (cfg2 q') = w"
[PROOF STATE]
proof (prove)
using this:
\<forall>q'. vote (cfg1 q') \<in> {None, Some w}

goal (1 subgoal):
 1. \<forall>q'. x (cfg2 q') = w
[PROOF STEP]
using step1 send1 q_w
[PROOF STATE]
proof (prove)
using this:
\<forall>q'. vote (cfg1 q') \<in> {None, Some w}
\<forall>p. next1 r1 p (cfg1 p) (\<mu>1 p) (cfg2 p)
\<forall>p. \<mu>1 p \<in> get_msgs (send1 r1) cfg1 (HOs r1) (HOs r1) p
q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w

goal (1 subgoal):
 1. \<forall>q'. x (cfg2 q') = w
[PROOF STEP]
apply(auto simp add: next1_def all_conj_distrib dec_update_def x_update_def
        get_msgs_benign send1_def isVote_def msgRcvd_def identicalVoteRcvd_def
        someVoteRcvd_def restrict_map_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q'. \<lbrakk>\<forall>p. (\<exists>v. (\<forall>q. q \<in> HOs r1 p \<longrightarrow> vote (cfg1 q) = Some v) \<and> decide (cfg2 p) = Some v) \<or> (\<forall>v. \<exists>q. (q \<in> HOs r1 p \<longrightarrow> vote (cfg1 q) \<noteq> Some v) \<and> q \<in> HOs r1 p) \<and> decide (cfg2 p) = decide (cfg1 p); \<forall>p. \<mu>1 p = (\<lambda>x. if x \<in> HOs r1 p then (Some \<circ> (\<lambda>q. Vote (vote (cfg1 q)))) x else None); \<forall>q'. vote (cfg1 q') = None \<or> vote (cfg1 q') = Some w; q \<in> HOs r1 p; vote (cfg1 q) = Some w; \<forall>p. vote (cfg2 p) = None; \<forall>p. (\<exists>q. (q \<in> HOs r1 p \<longrightarrow> (\<exists>y. vote (cfg1 q) = Some y) \<and> x (cfg2 p) = the (vote (cfg1 q))) \<and> q \<in> HOs r1 p) \<or> (\<forall>x. x \<in> HOs r1 p \<longrightarrow> vote (cfg1 x) = None) \<and> x (cfg2 p) = coin r1 p\<rbrakk> \<Longrightarrow> x (cfg2 q') = w
[PROOF STEP]
by (metis (erased, opaque_lifting) option.distinct(2) option.sel r1(1))
[PROOF STATE]
proof (state)
this:
\<forall>q'. x (cfg2 q') = w

goal (2 subgoals):
 1. \<lbrakk>\<forall>r. BenOr_commPerRd (HOs r); \<forall>q. HOs r1 p = HOs r1 q; \<forall>q. coin r1 p = coin r1 q; two_step r1 = 1; \<exists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w\<rbrakk> \<Longrightarrow> \<forall>q. x (cfg2 q) = x (cfg2 p)
 2. \<lbrakk>\<forall>r. BenOr_commPerRd (HOs r); \<forall>q. HOs r1 p = HOs r1 q; \<forall>q. coin r1 p = coin r1 q; two_step r1 = 1; \<nexists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w\<rbrakk> \<Longrightarrow> \<forall>q. x (cfg2 q) = x (cfg2 p)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>q'. x (cfg2 q') = w

goal (1 subgoal):
 1. \<forall>q. x (cfg2 q) = x (cfg2 p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>q. x (cfg2 q) = x (cfg2 p)

goal (1 subgoal):
 1. \<lbrakk>\<forall>r. BenOr_commPerRd (HOs r); \<forall>q. HOs r1 p = HOs r1 q; \<forall>q. coin r1 p = coin r1 q; two_step r1 = 1; \<nexists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w\<rbrakk> \<Longrightarrow> \<forall>q. x (cfg2 q) = x (cfg2 p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>r. BenOr_commPerRd (HOs r); \<forall>q. HOs r1 p = HOs r1 q; \<forall>q. coin r1 p = coin r1 q; two_step r1 = 1; \<nexists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w\<rbrakk> \<Longrightarrow> \<forall>q. x (cfg2 q) = x (cfg2 p)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w

goal (1 subgoal):
 1. \<lbrakk>\<forall>r. BenOr_commPerRd (HOs r); \<forall>q. HOs r1 p = HOs r1 q; \<forall>q. coin r1 p = coin r1 q; two_step r1 = 1; \<nexists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w\<rbrakk> \<Longrightarrow> \<forall>q. x (cfg2 q) = x (cfg2 p)
[PROOF STEP]
hence "\<forall>q'. x (cfg2 q') = coin r1 q'"
[PROOF STATE]
proof (prove)
using this:
\<nexists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w

goal (1 subgoal):
 1. \<forall>q'. x (cfg2 q') = coin r1 q'
[PROOF STEP]
using r1 step1 send1
[PROOF STATE]
proof (prove)
using this:
\<nexists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w
\<forall>q. HOs r1 p = HOs r1 q
\<forall>q. coin r1 p = coin r1 q
two_step r1 = 1
\<forall>p. next1 r1 p (cfg1 p) (\<mu>1 p) (cfg2 p)
\<forall>p. \<mu>1 p \<in> get_msgs (send1 r1) cfg1 (HOs r1) (HOs r1) p

goal (1 subgoal):
 1. \<forall>q'. x (cfg2 q') = coin r1 q'
[PROOF STEP]
apply(auto simp add: next1_def all_conj_distrib dec_update_def x_update_def
        get_msgs_benign send1_def isVote_def msgRcvd_def identicalVoteRcvd_def
        someVoteRcvd_def restrict_map_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q'. \<lbrakk>\<forall>p. (\<exists>v. (\<forall>q. q \<in> HOs r1 p \<longrightarrow> vote (cfg1 q) = Some v) \<and> decide (cfg2 p) = Some v) \<or> (\<forall>v. \<exists>q. (q \<in> HOs r1 p \<longrightarrow> vote (cfg1 q) \<noteq> Some v) \<and> q \<in> HOs r1 p) \<and> decide (cfg2 p) = decide (cfg1 p); \<forall>p. \<mu>1 p = (\<lambda>x. if x \<in> HOs r1 p then (Some \<circ> (\<lambda>q. Vote (vote (cfg1 q)))) x else None); \<forall>q. q \<in> HOs r1 p \<longrightarrow> vote (cfg1 q) = None; \<forall>q. HOs r1 p = HOs r1 q; \<forall>q. coin r1 p = coin r1 q; two_step r1 = Suc 0; \<forall>p. vote (cfg2 p) = None; \<forall>p. (\<exists>q. (q \<in> HOs r1 p \<longrightarrow> (\<exists>y. vote (cfg1 q) = Some y) \<and> x (cfg2 p) = the (vote (cfg1 q))) \<and> q \<in> HOs r1 p) \<or> (\<forall>x. x \<in> HOs r1 p \<longrightarrow> vote (cfg1 x) = None) \<and> x (cfg2 p) = coin r1 p\<rbrakk> \<Longrightarrow> x (cfg2 q') = coin r1 q'
[PROOF STEP]
by (metis False)
[PROOF STATE]
proof (state)
this:
\<forall>q'. x (cfg2 q') = coin r1 q'

goal (1 subgoal):
 1. \<lbrakk>\<forall>r. BenOr_commPerRd (HOs r); \<forall>q. HOs r1 p = HOs r1 q; \<forall>q. coin r1 p = coin r1 q; two_step r1 = 1; \<nexists>q w. q \<in> HOs r1 p \<and> vote (cfg1 q) = Some w\<rbrakk> \<Longrightarrow> \<forall>q. x (cfg2 q) = x (cfg2 p)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>q'. x (cfg2 q') = coin r1 q'

goal (1 subgoal):
 1. \<forall>q. x (cfg2 q) = x (cfg2 p)
[PROOF STEP]
using r1
[PROOF STATE]
proof (prove)
using this:
\<forall>q'. x (cfg2 q') = coin r1 q'
\<forall>q. HOs r1 p = HOs r1 q
\<forall>q. coin r1 p = coin r1 q
two_step r1 = 1

goal (1 subgoal):
 1. \<forall>q. x (cfg2 q) = x (cfg2 p)
[PROOF STEP]
by(metis)
[PROOF STATE]
proof (state)
this:
\<forall>q. x (cfg2 q) = x (cfg2 p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>q. x (cfg2 q) = x (cfg2 p)

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
hence "\<forall>q. vote (cfg3 q) = Some ?v"
[PROOF STATE]
proof (prove)
using this:
\<forall>q. x (cfg2 q) = x (cfg2 p)

goal (1 subgoal):
 1. \<forall>q. vote (cfg3 q) = Some (x (cfg2 p))
[PROOF STEP]
by(simp add: vote_origin[OF send2 step2 step_r2])
[PROOF STATE]
proof (state)
this:
\<forall>q. vote (cfg3 q) = Some (x (cfg2 p))

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
hence "decide (cfg4 p) = Some ?v"
[PROOF STATE]
proof (prove)
using this:
\<forall>q. vote (cfg3 q) = Some (x (cfg2 p))

goal (1 subgoal):
 1. decide (cfg4 p) = Some (x (cfg2 p))
[PROOF STEP]
using send3[THEN spec, of p] step3[THEN spec, of p] HOs_nonempty
[PROOF STATE]
proof (prove)
using this:
\<forall>q. vote (cfg3 q) = Some (x (cfg2 p))
\<mu>3 p \<in> get_msgs (send1 r3) cfg3 (HOs r3) (HOs r3) p
next1 r3 p (cfg3 p) (\<mu>3 p) (cfg4 p)
HOs ?r ?p \<noteq> {}

goal (1 subgoal):
 1. decide (cfg4 p) = Some (x (cfg2 p))
[PROOF STEP]
by(auto simp add: next1_def send1_def get_msgs_benign dec_update_def
      restrict_map_def identicalVoteRcvd_def msgRcvd_def isVote_def)
[PROOF STATE]
proof (state)
this:
decide (cfg4 p) = Some (x (cfg2 p))

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
decide (cfg4 p) = Some (x (cfg2 p))

goal (1 subgoal):
 1. \<exists>r v. decide (rho r p) = Some v
[PROOF STEP]
by(auto simp add: cfg4_def)
[PROOF STATE]
proof (state)
this:
\<exists>r v. decide (rho r p) = Some v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matroid_ax_3_alt:
  assumes "I \<subseteq> X \<inter> Y"
  shows "rk (X \<union> Y) + rk I \<le> rk X + rk Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk (X \<union> Y) + rk I \<le> rk X + rk Y
[PROOF STEP]
by (metis add.commute add_le_cancel_right assms matroid_ax_2 matroid_ax_3 order_trans)


[STATEMENT]
lemma rk_uniqueness:
  assumes "rk {A,B} = 2" and "rk {C,D} = 2" and "rk {A,B,M} \<le> 2" and "rk {C,D,M} \<le> 2" and
  "rk {A,B,P} \<le> 2" and "rk {C,D,P} \<le> 2" and "rk {A,B,C,D} \<ge> 3"
  shows "rk {M,P} = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {M, P} = 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rk {M, P} = 1
[PROOF STEP]
have "{A,B,M} \<union> {A,B,P} = {A,B,M,P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {A, B, M} \<union> {A, B, P} = {A, B, M, P}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{A, B, M} \<union> {A, B, P} = {A, B, M, P}

goal (1 subgoal):
 1. rk {M, P} = 1
[PROOF STEP]
have "rk {A,B,M,P} + rk {A,B} \<le> rk {A,B,M} + rk {A,B,P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A, B, M, P} + rk {A, B} \<le> rk {A, B, M} + rk {A, B, P}
[PROOF STEP]
by (metis (full_types) \<open>{A, B, M} \<union> {A, B, P} = {A, B, M, P}\<close> insert_commute le_inf_iff
        matroid_ax_3_alt subset_insertI)
[PROOF STATE]
proof (state)
this:
rk {A, B, M, P} + rk {A, B} \<le> rk {A, B, M} + rk {A, B, P}

goal (1 subgoal):
 1. rk {M, P} = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rk {A, B, M, P} + rk {A, B} \<le> rk {A, B, M} + rk {A, B, P}
[PROOF STEP]
have "rk {A,B,M,P} = 2"
[PROOF STATE]
proof (prove)
using this:
rk {A, B, M, P} + rk {A, B} \<le> rk {A, B, M} + rk {A, B, P}

goal (1 subgoal):
 1. rk {A, B, M, P} = 2
[PROOF STEP]
by (metis add_diff_cancel_right' antisym assms(1) assms(3) assms(5) insert_commute le_diff_conv matroid_ax_2 subset_insertI)
[PROOF STATE]
proof (state)
this:
rk {A, B, M, P} = 2

goal (1 subgoal):
 1. rk {M, P} = 1
[PROOF STEP]
have "{C,D,M} \<union> {C,D,P} = {C,D,M,P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {C, D, M} \<union> {C, D, P} = {C, D, M, P}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{C, D, M} \<union> {C, D, P} = {C, D, M, P}

goal (1 subgoal):
 1. rk {M, P} = 1
[PROOF STEP]
have "rk {C,D,M,P} + rk {C,D} \<le> rk {C,D,M} + rk {C,D,P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {C, D, M, P} + rk {C, D} \<le> rk {C, D, M} + rk {C, D, P}
[PROOF STEP]
by (metis Un_insert_left Un_upper1 \<open>{C, D, M} \<union> {C, D, P} = {C, D, M, P}\<close> insert_is_Un le_inf_iff
        matroid_ax_3_alt)
[PROOF STATE]
proof (state)
this:
rk {C, D, M, P} + rk {C, D} \<le> rk {C, D, M} + rk {C, D, P}

goal (1 subgoal):
 1. rk {M, P} = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rk {C, D, M, P} + rk {C, D} \<le> rk {C, D, M} + rk {C, D, P}
[PROOF STEP]
have i1:"rk {C,D,M,P} + 2 \<le> 4"
[PROOF STATE]
proof (prove)
using this:
rk {C, D, M, P} + rk {C, D} \<le> rk {C, D, M} + rk {C, D, P}

goal (1 subgoal):
 1. rk {C, D, M, P} + 2 \<le> 4
[PROOF STEP]
using assms(2) assms(4) assms(6)
[PROOF STATE]
proof (prove)
using this:
rk {C, D, M, P} + rk {C, D} \<le> rk {C, D, M} + rk {C, D, P}
rk {C, D} = 2
rk {C, D, M} \<le> 2
rk {C, D, P} \<le> 2

goal (1 subgoal):
 1. rk {C, D, M, P} + 2 \<le> 4
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
rk {C, D, M, P} + 2 \<le> 4

goal (1 subgoal):
 1. rk {M, P} = 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rk {C, D, M, P} + 2 \<le> 4

goal (1 subgoal):
 1. rk {M, P} = 1
[PROOF STEP]
have i2:"rk {C,D,M,P} \<ge> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 \<le> rk {C, D, M, P}
[PROOF STEP]
by (metis assms(2) insertI1 insert_subset matroid_ax_2 subset_insertI)
[PROOF STATE]
proof (state)
this:
2 \<le> rk {C, D, M, P}

goal (1 subgoal):
 1. rk {M, P} = 1
[PROOF STEP]
from i1 and i2
[PROOF STATE]
proof (chain)
picking this:
rk {C, D, M, P} + 2 \<le> 4
2 \<le> rk {C, D, M, P}
[PROOF STEP]
have "rk {C,D,M,P} = 2"
[PROOF STATE]
proof (prove)
using this:
rk {C, D, M, P} + 2 \<le> 4
2 \<le> rk {C, D, M, P}

goal (1 subgoal):
 1. rk {C, D, M, P} = 2
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
rk {C, D, M, P} = 2

goal (1 subgoal):
 1. rk {M, P} = 1
[PROOF STEP]
have "rk {A,B,C,D,M,P} \<ge> 3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3 \<le> rk {A, B, C, D, M, P}
[PROOF STEP]
by (metis Un_insert_right Un_upper2 assms(7) matroid_ax_2 order_trans sup_bot.right_neutral)
[PROOF STATE]
proof (state)
this:
3 \<le> rk {A, B, C, D, M, P}

goal (1 subgoal):
 1. rk {M, P} = 1
[PROOF STEP]
have "{A,B,M,P} \<union> {C,D,M,P} = {A,B,C,D,M,P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {A, B, M, P} \<union> {C, D, M, P} = {A, B, C, D, M, P}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{A, B, M, P} \<union> {C, D, M, P} = {A, B, C, D, M, P}

goal (1 subgoal):
 1. rk {M, P} = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{A, B, M, P} \<union> {C, D, M, P} = {A, B, C, D, M, P}
[PROOF STEP]
have "rk {A,B,C,D,M,P} + rk {M,P} \<le> rk {A,B,M,P} + rk {C,D,M,P}"
[PROOF STATE]
proof (prove)
using this:
{A, B, M, P} \<union> {C, D, M, P} = {A, B, C, D, M, P}

goal (1 subgoal):
 1. rk {A, B, C, D, M, P} + rk {M, P} \<le> rk {A, B, M, P} + rk {C, D, M, P}
[PROOF STEP]
by (smt le_inf_iff matroid_ax_3_alt order_trans subset_insertI)
[PROOF STATE]
proof (state)
this:
rk {A, B, C, D, M, P} + rk {M, P} \<le> rk {A, B, M, P} + rk {C, D, M, P}

goal (1 subgoal):
 1. rk {M, P} = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rk {A, B, C, D, M, P} + rk {M, P} \<le> rk {A, B, M, P} + rk {C, D, M, P}
[PROOF STEP]
have i3:"rk {A,B,C,D,M,P} + rk {M,P} \<le> 4"
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, D, M, P} + rk {M, P} \<le> rk {A, B, M, P} + rk {C, D, M, P}

goal (1 subgoal):
 1. rk {A, B, C, D, M, P} + rk {M, P} \<le> 4
[PROOF STEP]
using \<open>rk {A, B, M, P} = 2\<close> \<open>rk {C, D, M, P} = 2\<close>
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, D, M, P} + rk {M, P} \<le> rk {A, B, M, P} + rk {C, D, M, P}
rk {A, B, M, P} = 2
rk {C, D, M, P} = 2

goal (1 subgoal):
 1. rk {A, B, C, D, M, P} + rk {M, P} \<le> 4
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
rk {A, B, C, D, M, P} + rk {M, P} \<le> 4

goal (1 subgoal):
 1. rk {M, P} = 1
[PROOF STEP]
have i4:"rk {A,B,C,D,M,P} + rk {M,P} \<ge> 3 + rk{M,P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3 + rk {M, P} \<le> rk {A, B, C, D, M, P} + rk {M, P}
[PROOF STEP]
by (simp add: \<open>3 \<le> rk {A, B, C, D, M, P}\<close>)
[PROOF STATE]
proof (state)
this:
3 + rk {M, P} \<le> rk {A, B, C, D, M, P} + rk {M, P}

goal (1 subgoal):
 1. rk {M, P} = 1
[PROOF STEP]
from i3 and i4
[PROOF STATE]
proof (chain)
picking this:
rk {A, B, C, D, M, P} + rk {M, P} \<le> 4
3 + rk {M, P} \<le> rk {A, B, C, D, M, P} + rk {M, P}
[PROOF STEP]
show "rk {M,P} = 1"
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, D, M, P} + rk {M, P} \<le> 4
3 + rk {M, P} \<le> rk {A, B, C, D, M, P} + rk {M, P}

goal (1 subgoal):
 1. rk {M, P} = 1
[PROOF STEP]
by (metis (no_types, lifting) \<open>rk {A, B, C, D, M, P} + rk {M, P} \<le> rk {A, B, M, P} + rk {C, D, M, P}\<close>
        \<open>rk {A, B, M, P} = 2\<close> \<open>rk {C, D, M, P} = 2\<close> add_le_cancel_left add_numeral_left antisym
        insert_absorb2 numeral_Bit1 numeral_One numeral_plus_one one_add_one one_le_numeral
        order_trans rk_ax_couple rk_ax_singleton)
[PROOF STATE]
proof (state)
this:
rk {M, P} = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rk_ax_dim_alt: "\<exists>A B C D. \<forall>M. rk {A,B,M} \<noteq> 2 \<or> rk {C,D,M} \<noteq> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A B C D. \<forall>M. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>A B C D. \<forall>M. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2
[PROOF STEP]
obtain A B C D where f1:"rk {A,B,C,D} \<ge> 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A B C D. 4 \<le> rk {A, B, C, D} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using rk_ax_dim
[PROOF STATE]
proof (prove)
using this:
\<exists>A B C D. 4 \<le> rk {A, B, C, D}

goal (1 subgoal):
 1. (\<And>A B C D. 4 \<le> rk {A, B, C, D} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
4 \<le> rk {A, B, C, D}

goal (1 subgoal):
 1. \<exists>A B C D. \<forall>M. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2
[PROOF STEP]
have "\<forall>M. rk {A,B,M} \<noteq> 2 \<or> rk {C,D,M} \<noteq> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>M. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2
[PROOF STEP]
fix M
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2
[PROOF STEP]
have "{A,B,C,D,M} = {A,B,M} \<union> {C,D,M}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {A, B, C, D, M} = {A, B, M} \<union> {C, D, M}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{A, B, C, D, M} = {A, B, M} \<union> {C, D, M}

goal (1 subgoal):
 1. \<And>M. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{A, B, C, D, M} = {A, B, M} \<union> {C, D, M}
[PROOF STEP]
have "rk {A,B,C,D,M} + rk {M} \<le> rk {A,B,M} + rk {C,D,M}"
[PROOF STATE]
proof (prove)
using this:
{A, B, C, D, M} = {A, B, M} \<union> {C, D, M}

goal (1 subgoal):
 1. rk {A, B, C, D, M} + rk {M} \<le> rk {A, B, M} + rk {C, D, M}
[PROOF STEP]
by (smt le_inf_iff matroid_ax_3_alt order_trans subset_insertI)
[PROOF STATE]
proof (state)
this:
rk {A, B, C, D, M} + rk {M} \<le> rk {A, B, M} + rk {C, D, M}

goal (1 subgoal):
 1. \<And>M. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rk {A, B, C, D, M} + rk {M} \<le> rk {A, B, M} + rk {C, D, M}
[PROOF STEP]
have "rk {A,B,C,D,M} \<le> 3" if "rk {A,B,M} = 2" and "rk {C,D,M} = 2"
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, D, M} + rk {M} \<le> rk {A, B, M} + rk {C, D, M}

goal (1 subgoal):
 1. rk {A, B, C, D, M} \<le> 3
[PROOF STEP]
by (smt (z3) One_nat_def Suc_le_eq Suc_numeral add_Suc_right add_le_same_cancel1 nat_1_add_1 not_less numeral_Bit1 numerals(1) order_trans rk_ax_singleton semiring_norm(2) that(1) that(2))
[PROOF STATE]
proof (state)
this:
\<lbrakk>rk {A, B, M} = 2; rk {C, D, M} = 2\<rbrakk> \<Longrightarrow> rk {A, B, C, D, M} \<le> 3

goal (1 subgoal):
 1. \<And>M. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>rk {A, B, M} = 2; rk {C, D, M} = 2\<rbrakk> \<Longrightarrow> rk {A, B, C, D, M} \<le> 3
[PROOF STEP]
have "rk {A,B,C,D} \<le> 3" if "rk {A,B,M} = 2" and "rk {C,D,M} = 2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>rk {A, B, M} = 2; rk {C, D, M} = 2\<rbrakk> \<Longrightarrow> rk {A, B, C, D, M} \<le> 3

goal (1 subgoal):
 1. rk {A, B, C, D} \<le> 3
[PROOF STEP]
by (smt insert_commute matroid_ax_2 order_trans subset_insertI that(1) that(2))
[PROOF STATE]
proof (state)
this:
\<lbrakk>rk {A, B, M} = 2; rk {C, D, M} = 2\<rbrakk> \<Longrightarrow> rk {A, B, C, D} \<le> 3

goal (1 subgoal):
 1. \<And>M. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2
[PROOF STEP]
thus "rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2 "
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>rk {A, B, M} = 2; rk {C, D, M} = 2\<rbrakk> \<Longrightarrow> rk {A, B, C, D} \<le> 3

goal (1 subgoal):
 1. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2
[PROOF STEP]
using \<open>4 \<le> rk {A, B, C, D}\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>rk {A, B, M} = 2; rk {C, D, M} = 2\<rbrakk> \<Longrightarrow> rk {A, B, C, D} \<le> 3
4 \<le> rk {A, B, C, D}

goal (1 subgoal):
 1. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>M. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2

goal (1 subgoal):
 1. \<exists>A B C D. \<forall>M. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2
[PROOF STEP]
thus "\<exists>A B C D. \<forall>M. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2"
[PROOF STATE]
proof (prove)
using this:
\<forall>M. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2

goal (1 subgoal):
 1. \<exists>A B C D. \<forall>M. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>A B C D. \<forall>M. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rk_empty: "rk {} = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {} = 0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rk {} = 0
[PROOF STEP]
have "rk {} \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> rk {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> rk {}

goal (1 subgoal):
 1. rk {} = 0
[PROOF STEP]
have "rk {} \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {} \<le> 0
[PROOF STEP]
by (metis card.empty matroid_ax_1b)
[PROOF STATE]
proof (state)
this:
rk {} \<le> 0

goal (1 subgoal):
 1. rk {} = 0
[PROOF STEP]
thus "rk {} = 0"
[PROOF STATE]
proof (prove)
using this:
rk {} \<le> 0

goal (1 subgoal):
 1. rk {} = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rk {} = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matroid_ax_2_alt: "rk X \<le> rk (X \<union> {x}) \<and> rk (X \<union> {x}) \<le> rk X + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk X \<le> rk (X \<union> {x}) \<and> rk (X \<union> {x}) \<le> rk X + 1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rk X \<le> rk (X \<union> {x})
 2. rk (X \<union> {x}) \<le> rk X + 1
[PROOF STEP]
have "X \<subseteq> X \<union> {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<subseteq> X \<union> {x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X \<subseteq> X \<union> {x}

goal (2 subgoals):
 1. rk X \<le> rk (X \<union> {x})
 2. rk (X \<union> {x}) \<le> rk X + 1
[PROOF STEP]
thus "rk X \<le> rk (X \<union> {x})"
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> X \<union> {x}

goal (1 subgoal):
 1. rk X \<le> rk (X \<union> {x})
[PROOF STEP]
by (simp add: matroid_ax_2)
[PROOF STATE]
proof (state)
this:
rk X \<le> rk (X \<union> {x})

goal (1 subgoal):
 1. rk (X \<union> {x}) \<le> rk X + 1
[PROOF STEP]
have "rk {x} \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {x} \<le> 1
[PROOF STEP]
by (metis One_nat_def card.empty card_Suc_eq insert_absorb insert_not_empty matroid_ax_1b)
[PROOF STATE]
proof (state)
this:
rk {x} \<le> 1

goal (1 subgoal):
 1. rk (X \<union> {x}) \<le> rk X + 1
[PROOF STEP]
thus "rk (X \<union> {x}) \<le> rk X + 1"
[PROOF STATE]
proof (prove)
using this:
rk {x} \<le> 1

goal (1 subgoal):
 1. rk (X \<union> {x}) \<le> rk X + 1
[PROOF STEP]
by (metis add_leD1 le_antisym matroid_ax_3 rk_ax_singleton)
[PROOF STATE]
proof (state)
this:
rk (X \<union> {x}) \<le> rk X + 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matroid_ax_3_alt': "rk (X \<union> {y}) = rk (X \<union> {z}) \<longrightarrow> rk (X \<union> {z}) = rk X \<longrightarrow> rk X = rk (X \<union> {y,z})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk (X \<union> {y}) = rk (X \<union> {z}) \<longrightarrow> rk (X \<union> {z}) = rk X \<longrightarrow> rk X = rk (X \<union> {y, z})
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rk (X \<union> {y}) = rk (X \<union> {z}) \<longrightarrow> rk (X \<union> {z}) = rk X \<longrightarrow> rk X = rk (X \<union> {y, z})
[PROOF STEP]
have i1:"rk X \<le> rk (X \<union> {y,z})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk X \<le> rk (X \<union> {y, z})
[PROOF STEP]
using matroid_ax_2
[PROOF STATE]
proof (prove)
using this:
?X \<subseteq> ?Y \<longrightarrow> rk ?X \<le> rk ?Y

goal (1 subgoal):
 1. rk X \<le> rk (X \<union> {y, z})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rk X \<le> rk (X \<union> {y, z})

goal (1 subgoal):
 1. rk (X \<union> {y}) = rk (X \<union> {z}) \<longrightarrow> rk (X \<union> {z}) = rk X \<longrightarrow> rk X = rk (X \<union> {y, z})
[PROOF STEP]
have i2:"rk X \<ge> rk (X \<union> {y,z})" if "rk (X \<union> {y}) = rk (X \<union> {z})" and "rk (X \<union> {z}) = rk X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk (X \<union> {y, z}) \<le> rk X
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rk (X \<union> {y, z}) \<le> rk X
[PROOF STEP]
have "(X \<union> {y}) \<union> (X \<union> {z}) = X \<union> {y,z}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<union> {y} \<union> (X \<union> {z}) = X \<union> {y, z}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
X \<union> {y} \<union> (X \<union> {z}) = X \<union> {y, z}

goal (1 subgoal):
 1. rk (X \<union> {y, z}) \<le> rk X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<union> {y} \<union> (X \<union> {z}) = X \<union> {y, z}
[PROOF STEP]
have "rk (X \<union> {y,z}) + rk X \<le> rk X + rk X"
[PROOF STATE]
proof (prove)
using this:
X \<union> {y} \<union> (X \<union> {z}) = X \<union> {y, z}

goal (1 subgoal):
 1. rk (X \<union> {y, z}) + rk X \<le> rk X + rk X
[PROOF STEP]
by (metis \<open>rk (X \<union> {y}) = rk (X \<union> {z})\<close> \<open>rk (X \<union> {z}) = rk X\<close> inf_sup_ord(3) le_inf_iff
          matroid_ax_3_alt)
[PROOF STATE]
proof (state)
this:
rk (X \<union> {y, z}) + rk X \<le> rk X + rk X

goal (1 subgoal):
 1. rk (X \<union> {y, z}) \<le> rk X
[PROOF STEP]
thus "rk (X \<union> {y,z}) \<le> rk X"
[PROOF STATE]
proof (prove)
using this:
rk (X \<union> {y, z}) + rk X \<le> rk X + rk X

goal (1 subgoal):
 1. rk (X \<union> {y, z}) \<le> rk X
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rk (X \<union> {y, z}) \<le> rk X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>rk (X \<union> {y}) = rk (X \<union> {z}); rk (X \<union> {z}) = rk X\<rbrakk> \<Longrightarrow> rk (X \<union> {y, z}) \<le> rk X

goal (1 subgoal):
 1. rk (X \<union> {y}) = rk (X \<union> {z}) \<longrightarrow> rk (X \<union> {z}) = rk X \<longrightarrow> rk X = rk (X \<union> {y, z})
[PROOF STEP]
thus "rk (X \<union> {y}) = rk (X \<union> {z}) \<longrightarrow> rk (X \<union> {z}) = rk X \<longrightarrow> rk X = rk (X \<union> {y, z})"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>rk (X \<union> {y}) = rk (X \<union> {z}); rk (X \<union> {z}) = rk X\<rbrakk> \<Longrightarrow> rk (X \<union> {y, z}) \<le> rk X

goal (1 subgoal):
 1. rk (X \<union> {y}) = rk (X \<union> {z}) \<longrightarrow> rk (X \<union> {z}) = rk X \<longrightarrow> rk X = rk (X \<union> {y, z})
[PROOF STEP]
using antisym i1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>rk (X \<union> {y}) = rk (X \<union> {z}); rk (X \<union> {z}) = rk X\<rbrakk> \<Longrightarrow> rk (X \<union> {y, z}) \<le> rk X
\<lbrakk>?a \<le> ?b; ?b \<le> ?a\<rbrakk> \<Longrightarrow> ?a = ?b
rk X \<le> rk (X \<union> {y, z})

goal (1 subgoal):
 1. rk (X \<union> {y}) = rk (X \<union> {z}) \<longrightarrow> rk (X \<union> {z}) = rk X \<longrightarrow> rk X = rk (X \<union> {y, z})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rk (X \<union> {y}) = rk (X \<union> {z}) \<longrightarrow> rk (X \<union> {z}) = rk X \<longrightarrow> rk X = rk (X \<union> {y, z})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rk_ext:
  assumes "rk X \<le> 3"
  shows "\<exists>P. rk(X \<union> {P}) = rk X + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. rk (X \<union> {P}) = rk X + 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P. rk (X \<union> {P}) = rk X + 1
[PROOF STEP]
obtain A B C D where "rk {A,B,C,D} \<ge> 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A B C D. 4 \<le> rk {A, B, C, D} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using rk_ax_dim
[PROOF STATE]
proof (prove)
using this:
\<exists>A B C D. 4 \<le> rk {A, B, C, D}

goal (1 subgoal):
 1. (\<And>A B C D. 4 \<le> rk {A, B, C, D} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
4 \<le> rk {A, B, C, D}

goal (1 subgoal):
 1. \<exists>P. rk (X \<union> {P}) = rk X + 1
[PROOF STEP]
have f1:"rk (X \<union> {A, B, C, D}) \<ge> 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4 \<le> rk (X \<union> {A, B, C, D})
[PROOF STEP]
by (metis Un_upper2 \<open>4 \<le> rk {A, B, C, D}\<close> matroid_ax_2 sup.coboundedI2 sup.orderE)
[PROOF STATE]
proof (state)
this:
4 \<le> rk (X \<union> {A, B, C, D})

goal (1 subgoal):
 1. \<exists>P. rk (X \<union> {P}) = rk X + 1
[PROOF STEP]
have "rk (X \<union> {A, B, C, D}) = rk X" if "rk(X \<union> {A}) = rk(X \<union> {B})" and "rk(X \<union> {B}) = rk(X \<union> {C})"
    and "rk(X \<union> {C}) = rk(X \<union> {D})" and "rk(X \<union> {D}) = rk X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk (X \<union> {A, B, C, D}) = rk X
[PROOF STEP]
using matroid_ax_3_alt' that(1) that(2) that(3) that(4)
[PROOF STATE]
proof (prove)
using this:
rk (?X \<union> {?y}) = rk (?X \<union> {?z}) \<longrightarrow> rk (?X \<union> {?z}) = rk ?X \<longrightarrow> rk ?X = rk (?X \<union> {?y, ?z})
rk (X \<union> {A}) = rk (X \<union> {B})
rk (X \<union> {B}) = rk (X \<union> {C})
rk (X \<union> {C}) = rk (X \<union> {D})
rk (X \<union> {D}) = rk X

goal (1 subgoal):
 1. rk (X \<union> {A, B, C, D}) = rk X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>rk (X \<union> {A}) = rk (X \<union> {B}); rk (X \<union> {B}) = rk (X \<union> {C}); rk (X \<union> {C}) = rk (X \<union> {D}); rk (X \<union> {D}) = rk X\<rbrakk> \<Longrightarrow> rk (X \<union> {A, B, C, D}) = rk X

goal (1 subgoal):
 1. \<exists>P. rk (X \<union> {P}) = rk X + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>rk (X \<union> {A}) = rk (X \<union> {B}); rk (X \<union> {B}) = rk (X \<union> {C}); rk (X \<union> {C}) = rk (X \<union> {D}); rk (X \<union> {D}) = rk X\<rbrakk> \<Longrightarrow> rk (X \<union> {A, B, C, D}) = rk X
[PROOF STEP]
have f2:"rk (X \<union> {A, B, C, D}) \<le> 3" if "rk(X \<union> {A}) = rk(X \<union> {B})" and "rk(X \<union> {B}) = rk(X \<union> {C})"
    and "rk(X \<union> {C}) = rk(X \<union> {D})" and "rk(X \<union> {D}) = rk X"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>rk (X \<union> {A}) = rk (X \<union> {B}); rk (X \<union> {B}) = rk (X \<union> {C}); rk (X \<union> {C}) = rk (X \<union> {D}); rk (X \<union> {D}) = rk X\<rbrakk> \<Longrightarrow> rk (X \<union> {A, B, C, D}) = rk X

goal (1 subgoal):
 1. rk (X \<union> {A, B, C, D}) \<le> 3
[PROOF STEP]
using assms that(1) that(2) that(3) that(4)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>rk (X \<union> {A}) = rk (X \<union> {B}); rk (X \<union> {B}) = rk (X \<union> {C}); rk (X \<union> {C}) = rk (X \<union> {D}); rk (X \<union> {D}) = rk X\<rbrakk> \<Longrightarrow> rk (X \<union> {A, B, C, D}) = rk X
rk X \<le> 3
rk (X \<union> {A}) = rk (X \<union> {B})
rk (X \<union> {B}) = rk (X \<union> {C})
rk (X \<union> {C}) = rk (X \<union> {D})
rk (X \<union> {D}) = rk X

goal (1 subgoal):
 1. rk (X \<union> {A, B, C, D}) \<le> 3
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<lbrakk>rk (X \<union> {A}) = rk (X \<union> {B}); rk (X \<union> {B}) = rk (X \<union> {C}); rk (X \<union> {C}) = rk (X \<union> {D}); rk (X \<union> {D}) = rk X\<rbrakk> \<Longrightarrow> rk (X \<union> {A, B, C, D}) \<le> 3

goal (1 subgoal):
 1. \<exists>P. rk (X \<union> {P}) = rk X + 1
[PROOF STEP]
from f1 and f2
[PROOF STATE]
proof (chain)
picking this:
4 \<le> rk (X \<union> {A, B, C, D})
\<lbrakk>rk (X \<union> {A}) = rk (X \<union> {B}); rk (X \<union> {B}) = rk (X \<union> {C}); rk (X \<union> {C}) = rk (X \<union> {D}); rk (X \<union> {D}) = rk X\<rbrakk> \<Longrightarrow> rk (X \<union> {A, B, C, D}) \<le> 3
[PROOF STEP]
have "False" if "rk(X \<union> {A}) = rk(X \<union> {B})" and "rk(X \<union> {B}) = rk(X \<union> {C})"
    and "rk(X \<union> {C}) = rk(X \<union> {D})" and "rk(X \<union> {D}) = rk X"
[PROOF STATE]
proof (prove)
using this:
4 \<le> rk (X \<union> {A, B, C, D})
\<lbrakk>rk (X \<union> {A}) = rk (X \<union> {B}); rk (X \<union> {B}) = rk (X \<union> {C}); rk (X \<union> {C}) = rk (X \<union> {D}); rk (X \<union> {D}) = rk X\<rbrakk> \<Longrightarrow> rk (X \<union> {A, B, C, D}) \<le> 3

goal (1 subgoal):
 1. False
[PROOF STEP]
using that(1) that(2) that(3) that(4)
[PROOF STATE]
proof (prove)
using this:
4 \<le> rk (X \<union> {A, B, C, D})
\<lbrakk>rk (X \<union> {A}) = rk (X \<union> {B}); rk (X \<union> {B}) = rk (X \<union> {C}); rk (X \<union> {C}) = rk (X \<union> {D}); rk (X \<union> {D}) = rk X\<rbrakk> \<Longrightarrow> rk (X \<union> {A, B, C, D}) \<le> 3
rk (X \<union> {A}) = rk (X \<union> {B})
rk (X \<union> {B}) = rk (X \<union> {C})
rk (X \<union> {C}) = rk (X \<union> {D})
rk (X \<union> {D}) = rk X

goal (1 subgoal):
 1. False
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<lbrakk>rk (X \<union> {A}) = rk (X \<union> {B}); rk (X \<union> {B}) = rk (X \<union> {C}); rk (X \<union> {C}) = rk (X \<union> {D}); rk (X \<union> {D}) = rk X\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<exists>P. rk (X \<union> {P}) = rk X + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>rk (X \<union> {A}) = rk (X \<union> {B}); rk (X \<union> {B}) = rk (X \<union> {C}); rk (X \<union> {C}) = rk (X \<union> {D}); rk (X \<union> {D}) = rk X\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "rk (X \<union> {A}) = rk X + 1 \<or> rk (X \<union> {B}) = rk X + 1 \<or> rk (X \<union> {C}) = rk X + 1 \<or>
    rk (X \<union> {D}) = rk X + 1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>rk (X \<union> {A}) = rk (X \<union> {B}); rk (X \<union> {B}) = rk (X \<union> {C}); rk (X \<union> {C}) = rk (X \<union> {D}); rk (X \<union> {D}) = rk X\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. rk (X \<union> {A}) = rk X + 1 \<or> rk (X \<union> {B}) = rk X + 1 \<or> rk (X \<union> {C}) = rk X + 1 \<or> rk (X \<union> {D}) = rk X + 1
[PROOF STEP]
by (smt One_nat_def Suc_le_eq Suc_numeral Un_upper2 \<open>4 \<le> rk {A, B, C, D}\<close>
        \<open>\<lbrakk>rk (X \<union> {A}) = rk (X \<union> {B}); rk (X \<union> {B}) = rk (X \<union> {C}); rk (X \<union> {C}) = rk (X \<union> {D}); rk (X \<union> {D}) = rk X\<rbrakk> \<Longrightarrow> rk (X \<union> {A, B, C, D}) = rk X\<close>
        add.right_neutral add_Suc_right assms antisym_conv1 matroid_ax_2 matroid_ax_2_alt
        not_less semiring_norm(2) semiring_norm(8) sup.coboundedI2 sup.orderE)
[PROOF STATE]
proof (state)
this:
rk (X \<union> {A}) = rk X + 1 \<or> rk (X \<union> {B}) = rk X + 1 \<or> rk (X \<union> {C}) = rk X + 1 \<or> rk (X \<union> {D}) = rk X + 1

goal (1 subgoal):
 1. \<exists>P. rk (X \<union> {P}) = rk X + 1
[PROOF STEP]
thus "\<exists>P . rk (X \<union> {P}) = rk X + 1"
[PROOF STATE]
proof (prove)
using this:
rk (X \<union> {A}) = rk X + 1 \<or> rk (X \<union> {B}) = rk X + 1 \<or> rk (X \<union> {C}) = rk X + 1 \<or> rk (X \<union> {D}) = rk X + 1

goal (1 subgoal):
 1. \<exists>P. rk (X \<union> {P}) = rk X + 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P. rk (X \<union> {P}) = rk X + 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rk_singleton : "\<forall>P. rk {P} = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P. rk {P} = 1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. rk {P} = 1
[PROOF STEP]
fix P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. rk {P} = 1
[PROOF STEP]
have f1:"rk {P} \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {P} \<le> 1
[PROOF STEP]
by (metis One_nat_def card.empty card_Suc_eq insert_absorb insert_not_empty matroid_ax_1b)
[PROOF STATE]
proof (state)
this:
rk {P} \<le> 1

goal (1 subgoal):
 1. \<And>P. rk {P} = 1
[PROOF STEP]
have f2:"rk {P} \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> rk {P}
[PROOF STEP]
using rk_ax_singleton
[PROOF STATE]
proof (prove)
using this:
1 \<le> rk {?P}

goal (1 subgoal):
 1. 1 \<le> rk {P}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 \<le> rk {P}

goal (1 subgoal):
 1. \<And>P. rk {P} = 1
[PROOF STEP]
from f1 and f2
[PROOF STATE]
proof (chain)
picking this:
rk {P} \<le> 1
1 \<le> rk {P}
[PROOF STEP]
show "rk {P} = 1"
[PROOF STATE]
proof (prove)
using this:
rk {P} \<le> 1
1 \<le> rk {P}

goal (1 subgoal):
 1. rk {P} = 1
[PROOF STEP]
using antisym
[PROOF STATE]
proof (prove)
using this:
rk {P} \<le> 1
1 \<le> rk {P}
\<lbrakk>?a \<le> ?b; ?b \<le> ?a\<rbrakk> \<Longrightarrow> ?a = ?b

goal (1 subgoal):
 1. rk {P} = 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rk {P} = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rk_singleton_bis :
  assumes "A = B"
  shows "rk {A, B} = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A, B} = 1
[PROOF STEP]
by (simp add: assms rk_singleton)


[STATEMENT]
lemma rk_couple :
  assumes "A \<noteq> B"
  shows "rk {A, B} = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A, B} = 2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rk {A, B} = 2
[PROOF STEP]
have f1:"rk {A, B} \<le> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A, B} \<le> 2
[PROOF STEP]
by (metis insert_is_Un matroid_ax_2_alt one_add_one rk_singleton)
[PROOF STATE]
proof (state)
this:
rk {A, B} \<le> 2

goal (1 subgoal):
 1. rk {A, B} = 2
[PROOF STEP]
have f2:"rk {A, B} \<ge> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 \<le> rk {A, B}
[PROOF STEP]
by (simp add: assms rk_ax_couple)
[PROOF STATE]
proof (state)
this:
2 \<le> rk {A, B}

goal (1 subgoal):
 1. rk {A, B} = 2
[PROOF STEP]
from f1 and f2
[PROOF STATE]
proof (chain)
picking this:
rk {A, B} \<le> 2
2 \<le> rk {A, B}
[PROOF STEP]
show "?thesis"
[PROOF STATE]
proof (prove)
using this:
rk {A, B} \<le> 2
2 \<le> rk {A, B}

goal (1 subgoal):
 1. rk {A, B} = 2
[PROOF STEP]
by (simp add: f1 le_antisym)
[PROOF STATE]
proof (state)
this:
rk {A, B} = 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rk_triple_le : "rk {A, B, C} \<le> 3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A, B, C} \<le> 3
[PROOF STEP]
by (metis Suc_numeral Un_commute insert_absorb2 insert_is_Un linear matroid_ax_2_alt numeral_2_eq_2
      numeral_3_eq_3 numeral_le_one_iff numeral_plus_one rk_couple rk_singleton semiring_norm(70))


[STATEMENT]
lemma rk_couple_to_singleton :
  assumes "rk {A, B} = 1"
  shows "A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = B
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A = B
[PROOF STEP]
have "rk {A, B} = 2" if "A \<noteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A, B} = 2
[PROOF STEP]
using rk_couple
[PROOF STATE]
proof (prove)
using this:
?A \<noteq> ?B \<Longrightarrow> rk {?A, ?B} = 2

goal (1 subgoal):
 1. rk {A, B} = 2
[PROOF STEP]
by (simp add: that)
[PROOF STATE]
proof (state)
this:
A \<noteq> B \<Longrightarrow> rk {A, B} = 2

goal (1 subgoal):
 1. A = B
[PROOF STEP]
thus "A = B"
[PROOF STATE]
proof (prove)
using this:
A \<noteq> B \<Longrightarrow> rk {A, B} = 2

goal (1 subgoal):
 1. A = B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<noteq> B \<Longrightarrow> rk {A, B} = 2
rk {A, B} = 1

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rk_triple_to_rk_couple :
  assumes "rk {A, B, C} = 3"
  shows "rk {A, B} = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A, B} = 2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rk {A, B} = 2
[PROOF STEP]
have "rk {A, B} \<le> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A, B} \<le> 2
[PROOF STEP]
using matroid_ax_1b
[PROOF STATE]
proof (prove)
using this:
rk ?X \<le> card ?X

goal (1 subgoal):
 1. rk {A, B} \<le> 2
[PROOF STEP]
by (metis one_le_numeral rk_ax_couple rk_couple rk_singleton_bis)
[PROOF STATE]
proof (state)
this:
rk {A, B} \<le> 2

goal (1 subgoal):
 1. rk {A, B} = 2
[PROOF STEP]
have "rk {A, B, C} \<le> 2" if "rk {A, B} = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A, B, C} \<le> 2
[PROOF STEP]
using matroid_ax_2_alt[of "{A, B}" C]
[PROOF STATE]
proof (prove)
using this:
rk {A, B} \<le> rk ({A, B} \<union> {C}) \<and> rk ({A, B} \<union> {C}) \<le> rk {A, B} + 1

goal (1 subgoal):
 1. rk {A, B, C} \<le> 2
[PROOF STEP]
by (simp add: insert_commute that)
[PROOF STATE]
proof (state)
this:
rk {A, B} = 1 \<Longrightarrow> rk {A, B, C} \<le> 2

goal (1 subgoal):
 1. rk {A, B} = 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rk {A, B} = 1 \<Longrightarrow> rk {A, B, C} \<le> 2
[PROOF STEP]
have "rk {A, B} \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
rk {A, B} = 1 \<Longrightarrow> rk {A, B, C} \<le> 2

goal (1 subgoal):
 1. 2 \<le> rk {A, B}
[PROOF STEP]
using assms rk_ax_couple rk_singleton_bis
[PROOF STATE]
proof (prove)
using this:
rk {A, B} = 1 \<Longrightarrow> rk {A, B, C} \<le> 2
rk {A, B, C} = 3
?P \<noteq> ?Q \<longrightarrow> 2 \<le> rk {?P, ?Q}
?A = ?B \<Longrightarrow> rk {?A, ?B} = 1

goal (1 subgoal):
 1. 2 \<le> rk {A, B}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
2 \<le> rk {A, B}

goal (1 subgoal):
 1. rk {A, B} = 2
[PROOF STEP]
thus "rk {A, B} = 2"
[PROOF STATE]
proof (prove)
using this:
2 \<le> rk {A, B}

goal (1 subgoal):
 1. rk {A, B} = 2
[PROOF STEP]
by (simp add: \<open>rk {A, B} \<le> 2\<close> le_antisym)
[PROOF STATE]
proof (state)
this:
rk {A, B} = 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma del_undirected: "del_unEdge v e v' g = delete_edge v' e v (delete_edge v e v' g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. del_unEdge v e v' g = delete_edge v' e v (delete_edge v e v' g)
[PROOF STEP]
unfolding del_unEdge_def delete_edge_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>nodes = nodes g, edges = edges g - {(v, e, v'), (v', e, v)}\<rparr> = \<lparr>nodes = nodes \<lparr>nodes = nodes g, edges = edges g - {(v, e, v')}\<rparr>, edges = edges \<lparr>nodes = nodes g, edges = edges g - {(v, e, v')}\<rparr> - {(v', e, v)}\<rparr>
[PROOF STEP]
by auto


[STATEMENT]
lemma delete_edge_sym: "del_unEdge v e v' g = del_unEdge v' e v g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. del_unEdge v e v' g = del_unEdge v' e v g
[PROOF STEP]
unfolding del_unEdge_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>nodes = nodes g, edges = edges g - {(v, e, v'), (v', e, v)}\<rparr> = \<lparr>nodes = nodes g, edges = edges g - {(v', e, v), (v, e, v')}\<rparr>
[PROOF STEP]
by auto


[STATEMENT]
lemma del_unEdge_valid[simp]: assumes "valid_unMultigraph g"
    shows "valid_unMultigraph (del_unEdge v e v' g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph (del_unEdge v e v' g)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valid_unMultigraph (del_unEdge v e v' g)
[PROOF STEP]
interpret valid_unMultigraph g
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph g
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valid_unMultigraph (del_unEdge v e v' g)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph (del_unEdge v e v' g)
[PROOF STEP]
unfolding del_unEdge_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph \<lparr>nodes = V, edges = E - {(v, e, v'), (v', e, v)}\<rparr>
[PROOF STEP]
by unfold_locales (auto dest: E_validD)
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (del_unEdge v e v' g)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_compre_diff:"{x \<in> A - B. P x}={x \<in> A. P x} - {x \<in> B . P x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> A - B. P x} = {x \<in> A. P x} - {x \<in> B. P x}
[PROOF STEP]
by blast


[STATEMENT]
lemma set_compre_subset: "B \<subseteq> A \<Longrightarrow> {x \<in> B. P x} \<subseteq> {x \<in> A. P x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<subseteq> A \<Longrightarrow> {x \<in> B. P x} \<subseteq> {x \<in> A. P x}
[PROOF STEP]
by blast


[STATEMENT]
lemma del_edge_undirected_degree_plus: "finite (edges g) \<Longrightarrow> (v,e,v') \<in> edges g
    \<Longrightarrow> (v',e,v) \<in> edges g  \<Longrightarrow> degree v (del_unEdge v e v' g) + 1=degree v g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite (edges g); (v, e, v') \<in> edges g; (v', e, v) \<in> edges g\<rbrakk> \<Longrightarrow> degree v (del_unEdge v e v' g) + 1 = degree v g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>finite (edges g); (v, e, v') \<in> edges g; (v', e, v) \<in> edges g\<rbrakk> \<Longrightarrow> degree v (del_unEdge v e v' g) + 1 = degree v g
[PROOF STEP]
assume assms: "finite (edges g)" "(v,e,v') \<in> edges g" "(v',e,v) \<in> edges g "
[PROOF STATE]
proof (state)
this:
finite (edges g)
(v, e, v') \<in> edges g
(v', e, v) \<in> edges g

goal (1 subgoal):
 1. \<lbrakk>finite (edges g); (v, e, v') \<in> edges g; (v', e, v) \<in> edges g\<rbrakk> \<Longrightarrow> degree v (del_unEdge v e v' g) + 1 = degree v g
[PROOF STEP]
have "degree v (del_unEdge v e v' g) + 1
          = card ({ea \<in>  edges g - {(v, e, v'), (v', e, v)}. fst ea = v}) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree v (del_unEdge v e v' g) + 1 = card {ea \<in> edges g - {(v, e, v'), (v', e, v)}. fst ea = v} + 1
[PROOF STEP]
unfolding del_unEdge_def degree_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {ea \<in> edges \<lparr>nodes = nodes g, edges = edges g - {(v, e, v'), (v', e, v)}\<rparr>. fst ea = v} + 1 = card {ea \<in> edges g - {(v, e, v'), (v', e, v)}. fst ea = v} + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree v (del_unEdge v e v' g) + 1 = card {ea \<in> edges g - {(v, e, v'), (v', e, v)}. fst ea = v} + 1

goal (1 subgoal):
 1. \<lbrakk>finite (edges g); (v, e, v') \<in> edges g; (v', e, v) \<in> edges g\<rbrakk> \<Longrightarrow> degree v (del_unEdge v e v' g) + 1 = degree v g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree v (del_unEdge v e v' g) + 1 = card {ea \<in> edges g - {(v, e, v'), (v', e, v)}. fst ea = v} + 1

goal (1 subgoal):
 1. \<lbrakk>finite (edges g); (v, e, v') \<in> edges g; (v', e, v) \<in> edges g\<rbrakk> \<Longrightarrow> degree v (del_unEdge v e v' g) + 1 = degree v g
[PROOF STEP]
have "...=card ({ea \<in>  edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}.
      fst ea = v})+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {ea \<in> edges g - {(v, e, v'), (v', e, v)}. fst ea = v} + 1 = card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}) + 1
[PROOF STEP]
by (metis set_compre_diff)
[PROOF STATE]
proof (state)
this:
card {ea \<in> edges g - {(v, e, v'), (v', e, v)}. fst ea = v} + 1 = card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}) + 1

goal (1 subgoal):
 1. \<lbrakk>finite (edges g); (v, e, v') \<in> edges g; (v', e, v) \<in> edges g\<rbrakk> \<Longrightarrow> degree v (del_unEdge v e v' g) + 1 = degree v g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {ea \<in> edges g - {(v, e, v'), (v', e, v)}. fst ea = v} + 1 = card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}) + 1

goal (1 subgoal):
 1. \<lbrakk>finite (edges g); (v, e, v') \<in> edges g; (v', e, v) \<in> edges g\<rbrakk> \<Longrightarrow> degree v (del_unEdge v e v' g) + 1 = degree v g
[PROOF STEP]
have "...=card ({ea \<in>  edges g. fst ea = v}) - card({ea \<in> {(v, e, v'), (v', e, v)}.
      fst ea = v})+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}) + 1 = card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}) + 1 = card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1
[PROOF STEP]
have "{(v, e, v'), (v', e, v)} \<subseteq> edges g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(v, e, v'), (v', e, v)} \<subseteq> edges g
[PROOF STEP]
using \<open>(v,e,v') \<in> edges g\<close> \<open>(v',e,v) \<in> edges g\<close>
[PROOF STATE]
proof (prove)
using this:
(v, e, v') \<in> edges g
(v', e, v) \<in> edges g

goal (1 subgoal):
 1. {(v, e, v'), (v', e, v)} \<subseteq> edges g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(v, e, v'), (v', e, v)} \<subseteq> edges g

goal (1 subgoal):
 1. card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}) + 1 = card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1
[PROOF STEP]
hence "{ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} \<subseteq> {ea \<in>  edges g. fst ea = v}"
[PROOF STATE]
proof (prove)
using this:
{(v, e, v'), (v', e, v)} \<subseteq> edges g

goal (1 subgoal):
 1. {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} \<subseteq> {ea \<in> edges g. fst ea = v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} \<subseteq> {ea \<in> edges g. fst ea = v}

goal (1 subgoal):
 1. card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}) + 1 = card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} \<subseteq> {ea \<in> edges g. fst ea = v}

goal (1 subgoal):
 1. card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}) + 1 = card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1
[PROOF STEP]
have "finite {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}

goal (1 subgoal):
 1. card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}) + 1 = card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} \<subseteq> {ea \<in> edges g. fst ea = v}
finite {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}
[PROOF STEP]
have "card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}.
          fst ea = v})=card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}.
          fst ea = v}"
[PROOF STATE]
proof (prove)
using this:
{ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} \<subseteq> {ea \<in> edges g. fst ea = v}
finite {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}

goal (1 subgoal):
 1. card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}) = card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}
[PROOF STEP]
using card_Diff_subset
[PROOF STATE]
proof (prove)
using this:
{ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} \<subseteq> {ea \<in> edges g. fst ea = v}
finite {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}
\<lbrakk>finite ?B; ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> card (?A - ?B) = card ?A - card ?B

goal (1 subgoal):
 1. card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}) = card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}) = card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}

goal (1 subgoal):
 1. card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}) + 1 = card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}) = card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}

goal (1 subgoal):
 1. card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}) + 1 = card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}) + 1 = card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}) + 1 = card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1

goal (1 subgoal):
 1. \<lbrakk>finite (edges g); (v, e, v') \<in> edges g; (v', e, v) \<in> edges g\<rbrakk> \<Longrightarrow> degree v (del_unEdge v e v' g) + 1 = degree v g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ({ea \<in> edges g. fst ea = v} - {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}) + 1 = card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1

goal (1 subgoal):
 1. \<lbrakk>finite (edges g); (v, e, v') \<in> edges g; (v', e, v) \<in> edges g\<rbrakk> \<Longrightarrow> degree v (del_unEdge v e v' g) + 1 = degree v g
[PROOF STEP]
have "...=card ({ea \<in>  edges g. fst ea = v})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1 = card {ea \<in> edges g. fst ea = v}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1 = card {ea \<in> edges g. fst ea = v}
[PROOF STEP]
have "{ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v}={(v,e,v')}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} = {(v, e, v')}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} = {(v, e, v')}

goal (1 subgoal):
 1. card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1 = card {ea \<in> edges g. fst ea = v}
[PROOF STEP]
hence "card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} = 1"
[PROOF STATE]
proof (prove)
using this:
{ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} = {(v, e, v')}

goal (1 subgoal):
 1. card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} = 1

goal (1 subgoal):
 1. card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1 = card {ea \<in> edges g. fst ea = v}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} = 1

goal (1 subgoal):
 1. card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1 = card {ea \<in> edges g. fst ea = v}
[PROOF STEP]
have "card {ea \<in> edges g. fst ea = v}\<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {ea \<in> edges g. fst ea = v} \<noteq> 0
[PROOF STEP]
by (metis (lifting, mono_tags) Collect_empty_eq assms(1) assms(2)
          card_eq_0_iff fst_conv mem_Collect_eq rev_finite_subset subsetI)
[PROOF STATE]
proof (state)
this:
card {ea \<in> edges g. fst ea = v} \<noteq> 0

goal (1 subgoal):
 1. card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1 = card {ea \<in> edges g. fst ea = v}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} = 1
card {ea \<in> edges g. fst ea = v} \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} = 1
card {ea \<in> edges g. fst ea = v} \<noteq> 0

goal (1 subgoal):
 1. card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1 = card {ea \<in> edges g. fst ea = v}
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1 = card {ea \<in> edges g. fst ea = v}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card {ea \<in> edges g. fst ea = v} - card {ea \<in> {(v, e, v'), (v', e, v)}. fst ea = v} + 1 = card {ea \<in> edges g. fst ea = v}

goal (1 subgoal):
 1. \<lbrakk>finite (edges g); (v, e, v') \<in> edges g; (v', e, v) \<in> edges g\<rbrakk> \<Longrightarrow> degree v (del_unEdge v e v' g) + 1 = degree v g
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree v (del_unEdge v e v' g) + 1 = card {ea \<in> edges g. fst ea = v}
[PROOF STEP]
have "degree v (del_unEdge v e v' g) + 1=card ({ea \<in>  edges g. fst ea = v})"
[PROOF STATE]
proof (prove)
using this:
degree v (del_unEdge v e v' g) + 1 = card {ea \<in> edges g. fst ea = v}

goal (1 subgoal):
 1. degree v (del_unEdge v e v' g) + 1 = card {ea \<in> edges g. fst ea = v}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
degree v (del_unEdge v e v' g) + 1 = card {ea \<in> edges g. fst ea = v}

goal (1 subgoal):
 1. \<lbrakk>finite (edges g); (v, e, v') \<in> edges g; (v', e, v) \<in> edges g\<rbrakk> \<Longrightarrow> degree v (del_unEdge v e v' g) + 1 = degree v g
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
degree v (del_unEdge v e v' g) + 1 = card {ea \<in> edges g. fst ea = v}

goal (1 subgoal):
 1. degree v (del_unEdge v e v' g) + 1 = degree v g
[PROOF STEP]
unfolding degree_def
[PROOF STATE]
proof (prove)
using this:
card {ea \<in> edges (del_unEdge v e v' g). fst ea = v} + 1 = card {ea \<in> edges g. fst ea = v}

goal (1 subgoal):
 1. card {ea \<in> edges (del_unEdge v e v' g). fst ea = v} + 1 = card {e \<in> edges g. fst e = v}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
degree v (del_unEdge v e v' g) + 1 = degree v g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma del_edge_undirected_degree_plus': "finite (edges g) \<Longrightarrow> (v,e,v') \<in> edges g
    \<Longrightarrow> (v',e,v) \<in> edges g \<Longrightarrow> degree v' (del_unEdge v e v' g) + 1=degree v' g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite (edges g); (v, e, v') \<in> edges g; (v', e, v) \<in> edges g\<rbrakk> \<Longrightarrow> degree v' (del_unEdge v e v' g) + 1 = degree v' g
[PROOF STEP]
by (metis del_edge_undirected_degree_plus delete_edge_sym)


[STATEMENT]
lemma del_edge_undirected_degree_minus[simp]: "finite (edges g) \<Longrightarrow> (v,e,v') \<in> edges g
    \<Longrightarrow> (v',e,v) \<in> edges g \<Longrightarrow> degree v (del_unEdge v e v' g) =degree v g- (1::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite (edges g); (v, e, v') \<in> edges g; (v', e, v) \<in> edges g\<rbrakk> \<Longrightarrow> degree v (del_unEdge v e v' g) = degree v g - 1
[PROOF STEP]
using del_edge_undirected_degree_plus
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite (edges ?g); (?v, ?e, ?v') \<in> edges ?g; (?v', ?e, ?v) \<in> edges ?g\<rbrakk> \<Longrightarrow> degree ?v (del_unEdge ?v ?e ?v' ?g) + 1 = degree ?v ?g

goal (1 subgoal):
 1. \<lbrakk>finite (edges g); (v, e, v') \<in> edges g; (v', e, v) \<in> edges g\<rbrakk> \<Longrightarrow> degree v (del_unEdge v e v' g) = degree v g - 1
[PROOF STEP]
by (metis add_diff_cancel_left' add.commute)


[STATEMENT]
lemma del_edge_undirected_degree_minus'[simp]: "finite (edges g) \<Longrightarrow> (v,e,v') \<in> edges g
    \<Longrightarrow> (v',e,v) \<in> edges g \<Longrightarrow> degree v' (del_unEdge v e v' g) =degree v' g- (1::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite (edges g); (v, e, v') \<in> edges g; (v', e, v) \<in> edges g\<rbrakk> \<Longrightarrow> degree v' (del_unEdge v e v' g) = degree v' g - 1
[PROOF STEP]
by (metis del_edge_undirected_degree_minus delete_edge_sym)


[STATEMENT]
lemma del_unEdge_com: "del_unEdge v w v' (del_unEdge n e n' g)
          = del_unEdge n e n' (del_unEdge v w v' g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. del_unEdge v w v' (del_unEdge n e n' g) = del_unEdge n e n' (del_unEdge v w v' g)
[PROOF STEP]
unfolding del_unEdge_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>nodes = nodes \<lparr>nodes = nodes g, edges = edges g - {(n, e, n'), (n', e, n)}\<rparr>, edges = edges \<lparr>nodes = nodes g, edges = edges g - {(n, e, n'), (n', e, n)}\<rparr> - {(v, w, v'), (v', w, v)}\<rparr> = \<lparr>nodes = nodes \<lparr>nodes = nodes g, edges = edges g - {(v, w, v'), (v', w, v)}\<rparr>, edges = edges \<lparr>nodes = nodes g, edges = edges g - {(v, w, v'), (v', w, v)}\<rparr> - {(n, e, n'), (n', e, n)}\<rparr>
[PROOF STEP]
by auto


[STATEMENT]
lemma rem_unPath_com: "rem_unPath ps (del_unEdge v w v' g)
            = del_unEdge v w v' (rem_unPath ps g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rem_unPath ps (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath ps g)
[PROOF STEP]
proof (induct ps arbitrary: g)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>g. rem_unPath [] (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath [] g)
 2. \<And>a ps g. (\<And>g. rem_unPath ps (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath ps g)) \<Longrightarrow> rem_unPath (a # ps) (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath (a # ps) g)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>g. rem_unPath [] (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath [] g)
 2. \<And>a ps g. (\<And>g. rem_unPath ps (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath ps g)) \<Longrightarrow> rem_unPath (a # ps) (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath (a # ps) g)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rem_unPath [] (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath [] g)
[PROOF STEP]
by (metis rem_unPath.simps(1))
[PROOF STATE]
proof (state)
this:
rem_unPath [] (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath [] g)

goal (1 subgoal):
 1. \<And>a ps g. (\<And>g. rem_unPath ps (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath ps g)) \<Longrightarrow> rem_unPath (a # ps) (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath (a # ps) g)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps g. (\<And>g. rem_unPath ps (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath ps g)) \<Longrightarrow> rem_unPath (a # ps) (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath (a # ps) g)
[PROOF STEP]
case (Cons a ps')
[PROOF STATE]
proof (state)
this:
rem_unPath ps' (del_unEdge v w v' ?g) = del_unEdge v w v' (rem_unPath ps' ?g)

goal (1 subgoal):
 1. \<And>a ps g. (\<And>g. rem_unPath ps (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath ps g)) \<Longrightarrow> rem_unPath (a # ps) (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath (a # ps) g)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
rem_unPath ps' (del_unEdge v w v' ?g) = del_unEdge v w v' (rem_unPath ps' ?g)

goal (1 subgoal):
 1. rem_unPath (a # ps') (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath (a # ps') g)
[PROOF STEP]
using del_unEdge_com
[PROOF STATE]
proof (prove)
using this:
rem_unPath ps' (del_unEdge v w v' ?g) = del_unEdge v w v' (rem_unPath ps' ?g)
del_unEdge ?v ?w ?v' (del_unEdge ?n ?e ?n' ?g) = del_unEdge ?n ?e ?n' (del_unEdge ?v ?w ?v' ?g)

goal (1 subgoal):
 1. rem_unPath (a # ps') (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath (a # ps') g)
[PROOF STEP]
by (metis prod_cases3 rem_unPath.simps(1) rem_unPath.simps(2))
[PROOF STATE]
proof (state)
this:
rem_unPath (a # ps') (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath (a # ps') g)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rem_unPath_valid[intro]:
  "valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath ps g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath ps g)
[PROOF STEP]
proof (induct ps )
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath [] g)
 2. \<And>a ps. \<lbrakk>valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath ps g); valid_unMultigraph g\<rbrakk> \<Longrightarrow> valid_unMultigraph (rem_unPath (a # ps) g)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
valid_unMultigraph g

goal (2 subgoals):
 1. valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath [] g)
 2. \<And>a ps. \<lbrakk>valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath ps g); valid_unMultigraph g\<rbrakk> \<Longrightarrow> valid_unMultigraph (rem_unPath (a # ps) g)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph g

goal (1 subgoal):
 1. valid_unMultigraph (rem_unPath [] g)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (rem_unPath [] g)

goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath ps g); valid_unMultigraph g\<rbrakk> \<Longrightarrow> valid_unMultigraph (rem_unPath (a # ps) g)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath ps g); valid_unMultigraph g\<rbrakk> \<Longrightarrow> valid_unMultigraph (rem_unPath (a # ps) g)
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath xs g)
valid_unMultigraph g

goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath ps g); valid_unMultigraph g\<rbrakk> \<Longrightarrow> valid_unMultigraph (rem_unPath (a # ps) g)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath xs g)
valid_unMultigraph g

goal (1 subgoal):
 1. valid_unMultigraph (rem_unPath (x # xs) g)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath xs g); valid_unMultigraph g\<rbrakk> \<Longrightarrow> valid_unMultigraph (rem_unPath (x # xs) g)
[PROOF STEP]
have "valid_unMultigraph (rem_unPath (x # xs) g) = valid_unMultigraph
         (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph (rem_unPath (x # xs) g) = valid_unMultigraph (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs g))
[PROOF STEP]
using rem_unPath_com
[PROOF STATE]
proof (prove)
using this:
rem_unPath ?ps (del_unEdge ?v ?w ?v' ?g) = del_unEdge ?v ?w ?v' (rem_unPath ?ps ?g)

goal (1 subgoal):
 1. valid_unMultigraph (rem_unPath (x # xs) g) = valid_unMultigraph (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs g))
[PROOF STEP]
by (metis prod.collapse rem_unPath.simps(2))
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (rem_unPath (x # xs) g) = valid_unMultigraph (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs g))

goal (1 subgoal):
 1. \<lbrakk>valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath xs g); valid_unMultigraph g\<rbrakk> \<Longrightarrow> valid_unMultigraph (rem_unPath (x # xs) g)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (rem_unPath (x # xs) g) = valid_unMultigraph (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs g))

goal (1 subgoal):
 1. \<lbrakk>valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath xs g); valid_unMultigraph g\<rbrakk> \<Longrightarrow> valid_unMultigraph (rem_unPath (x # xs) g)
[PROOF STEP]
have "...=valid_unMultigraph (rem_unPath xs g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs g)) = valid_unMultigraph (rem_unPath xs g)
[PROOF STEP]
by (metis Cons.hyps Cons.prems del_unEdge_valid)
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs g)) = valid_unMultigraph (rem_unPath xs g)

goal (1 subgoal):
 1. \<lbrakk>valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath xs g); valid_unMultigraph g\<rbrakk> \<Longrightarrow> valid_unMultigraph (rem_unPath (x # xs) g)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs g)) = valid_unMultigraph (rem_unPath xs g)

goal (1 subgoal):
 1. \<lbrakk>valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath xs g); valid_unMultigraph g\<rbrakk> \<Longrightarrow> valid_unMultigraph (rem_unPath (x # xs) g)
[PROOF STEP]
have "...=True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph (rem_unPath xs g) = True
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath xs g)
valid_unMultigraph g

goal (1 subgoal):
 1. valid_unMultigraph (rem_unPath xs g) = True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (rem_unPath xs g) = True

goal (1 subgoal):
 1. \<lbrakk>valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath xs g); valid_unMultigraph g\<rbrakk> \<Longrightarrow> valid_unMultigraph (rem_unPath (x # xs) g)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
valid_unMultigraph (rem_unPath (x # xs) g) = True
[PROOF STEP]
have "?case=True"
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph (rem_unPath (x # xs) g) = True

goal (1 subgoal):
 1. valid_unMultigraph (rem_unPath (x # xs) g) = True
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (rem_unPath (x # xs) g) = True

goal (1 subgoal):
 1. \<lbrakk>valid_unMultigraph g \<Longrightarrow> valid_unMultigraph (rem_unPath xs g); valid_unMultigraph g\<rbrakk> \<Longrightarrow> valid_unMultigraph (rem_unPath (x # xs) g)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph (rem_unPath (x # xs) g) = True

goal (1 subgoal):
 1. valid_unMultigraph (rem_unPath (x # xs) g)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (rem_unPath (x # xs) g)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (rem_unPath (x # xs) g)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in valid_unMultigraph) degree_frame:
    assumes "finite (edges G)"  "x \<notin> {v, v'}"
    shows "degree x (del_unEdge v w v' G) = degree x G" (is "?L=?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
proof (cases "(v,w,v') \<in> edges G")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (v, w, v') \<in> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
 2. (v, w, v') \<notin> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(v, w, v') \<in> E

goal (2 subgoals):
 1. (v, w, v') \<in> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
 2. (v, w, v') \<notin> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
have "?L=card({e. e\<in>edges G - {(v,w,v'),(v',w,v)} \<and> fst e=x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree x (del_unEdge v w v' G) = card {e \<in> E - {(v, w, v'), (v', w, v)}. fst e = x}
[PROOF STEP]
by (simp add:del_unEdge_def degree_def)
[PROOF STATE]
proof (state)
this:
degree x (del_unEdge v w v' G) = card {e \<in> E - {(v, w, v'), (v', w, v)}. fst e = x}

goal (2 subgoals):
 1. (v, w, v') \<in> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
 2. (v, w, v') \<notin> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree x (del_unEdge v w v' G) = card {e \<in> E - {(v, w, v'), (v', w, v)}. fst e = x}

goal (2 subgoals):
 1. (v, w, v') \<in> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
 2. (v, w, v') \<notin> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
have "...=card({e. e\<in>edges G \<and> fst e=x}-{e. e\<in>{(v,w,v'),(v',w,v)} \<and> fst e=x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {e \<in> E - {(v, w, v'), (v', w, v)}. fst e = x} = card ({e \<in> E. fst e = x} - {e \<in> {(v, w, v'), (v', w, v)}. fst e = x})
[PROOF STEP]
by (metis  set_compre_diff)
[PROOF STATE]
proof (state)
this:
card {e \<in> E - {(v, w, v'), (v', w, v)}. fst e = x} = card ({e \<in> E. fst e = x} - {e \<in> {(v, w, v'), (v', w, v)}. fst e = x})

goal (2 subgoals):
 1. (v, w, v') \<in> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
 2. (v, w, v') \<notin> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {e \<in> E - {(v, w, v'), (v', w, v)}. fst e = x} = card ({e \<in> E. fst e = x} - {e \<in> {(v, w, v'), (v', w, v)}. fst e = x})

goal (2 subgoals):
 1. (v, w, v') \<in> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
 2. (v, w, v') \<notin> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
have "...=card({e. e\<in>edges G \<and> fst e=x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({e \<in> E. fst e = x} - {e \<in> {(v, w, v'), (v', w, v)}. fst e = x}) = card {e \<in> E. fst e = x}
[PROOF STEP]
using \<open>x \<notin> {v, v'}\<close>
[PROOF STATE]
proof (prove)
using this:
x \<notin> {v, v'}

goal (1 subgoal):
 1. card ({e \<in> E. fst e = x} - {e \<in> {(v, w, v'), (v', w, v)}. fst e = x}) = card {e \<in> E. fst e = x}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> card ({e \<in> E. fst e = x} - {e \<in> {(v, w, v'), (v', w, v)}. fst e = x}) = card {e \<in> E. fst e = x}
[PROOF STEP]
have "x\<noteq>v \<and> x\<noteq> v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> v \<and> x \<noteq> v'
[PROOF STEP]
using \<open>x\<notin>{v,v'}\<close>
[PROOF STATE]
proof (prove)
using this:
x \<notin> {v, v'}

goal (1 subgoal):
 1. x \<noteq> v \<and> x \<noteq> v'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<noteq> v \<and> x \<noteq> v'

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> card ({e \<in> E. fst e = x} - {e \<in> {(v, w, v'), (v', w, v)}. fst e = x}) = card {e \<in> E. fst e = x}
[PROOF STEP]
hence "{e. e\<in>{(v,w,v'),(v',w,v)} \<and> fst e=x}={}"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> v \<and> x \<noteq> v'

goal (1 subgoal):
 1. {e \<in> {(v, w, v'), (v', w, v)}. fst e = x} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{e \<in> {(v, w, v'), (v', w, v)}. fst e = x} = {}

goal (1 subgoal):
 1. x \<notin> {v, v'} \<Longrightarrow> card ({e \<in> E. fst e = x} - {e \<in> {(v, w, v'), (v', w, v)}. fst e = x}) = card {e \<in> E. fst e = x}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{e \<in> {(v, w, v'), (v', w, v)}. fst e = x} = {}

goal (1 subgoal):
 1. card ({e \<in> E. fst e = x} - {e \<in> {(v, w, v'), (v', w, v)}. fst e = x}) = card {e \<in> E. fst e = x}
[PROOF STEP]
by (metis Diff_empty)
[PROOF STATE]
proof (state)
this:
card ({e \<in> E. fst e = x} - {e \<in> {(v, w, v'), (v', w, v)}. fst e = x}) = card {e \<in> E. fst e = x}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card ({e \<in> E. fst e = x} - {e \<in> {(v, w, v'), (v', w, v)}. fst e = x}) = card {e \<in> E. fst e = x}

goal (2 subgoals):
 1. (v, w, v') \<in> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
 2. (v, w, v') \<notin> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ({e \<in> E. fst e = x} - {e \<in> {(v, w, v'), (v', w, v)}. fst e = x}) = card {e \<in> E. fst e = x}

goal (2 subgoals):
 1. (v, w, v') \<in> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
 2. (v, w, v') \<notin> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
have "...=?R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {e \<in> E. fst e = x} = degree x G
[PROOF STEP]
by (simp add:degree_def)
[PROOF STATE]
proof (state)
this:
card {e \<in> E. fst e = x} = degree x G

goal (2 subgoals):
 1. (v, w, v') \<in> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
 2. (v, w, v') \<notin> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
degree x (del_unEdge v w v' G) = degree x G

goal (1 subgoal):
 1. degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
degree x (del_unEdge v w v' G) = degree x G

goal (1 subgoal):
 1. (v, w, v') \<notin> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (v, w, v') \<notin> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
(v, w, v') \<notin> E

goal (1 subgoal):
 1. (v, w, v') \<notin> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(v, w, v') \<notin> E

goal (1 subgoal):
 1. (v, w, v') \<notin> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
hence "(v',w,v)\<notin>E"
[PROOF STATE]
proof (prove)
using this:
(v, w, v') \<notin> E

goal (1 subgoal):
 1. (v', w, v) \<notin> E
[PROOF STEP]
using corres
[PROOF STATE]
proof (prove)
using this:
(v, w, v') \<notin> E
((?v, ?w, ?u') \<in> E) = ((?u', ?w, ?v) \<in> E)

goal (1 subgoal):
 1. (v', w, v) \<notin> E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v', w, v) \<notin> E

goal (1 subgoal):
 1. (v, w, v') \<notin> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(v, w, v') \<notin> E
(v', w, v) \<notin> E
[PROOF STEP]
have "E- {(v,w,v'),(v',w,v)}=E"
[PROOF STATE]
proof (prove)
using this:
(v, w, v') \<notin> E
(v', w, v) \<notin> E

goal (1 subgoal):
 1. E - {(v, w, v'), (v', w, v)} = E
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
E - {(v, w, v'), (v', w, v)} = E

goal (1 subgoal):
 1. (v, w, v') \<notin> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
hence "del_unEdge v w v' G=G"
[PROOF STATE]
proof (prove)
using this:
E - {(v, w, v'), (v', w, v)} = E

goal (1 subgoal):
 1. del_unEdge v w v' G = G
[PROOF STEP]
by (auto simp add:del_unEdge_def)
[PROOF STATE]
proof (state)
this:
del_unEdge v w v' G = G

goal (1 subgoal):
 1. (v, w, v') \<notin> E \<Longrightarrow> degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
del_unEdge v w v' G = G

goal (1 subgoal):
 1. degree x (del_unEdge v w v' G) = degree x G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree x (del_unEdge v w v' G) = degree x G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [simp]: "rev_path [] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev_path [] = []
[PROOF STEP]
unfolding rev_path_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>(a, b, c). (c, b, a)) (rev []) = []
[PROOF STEP]
by simp


[STATEMENT]
lemma rev_path_append[simp]: "rev_path (xs@ys) = (rev_path ys) @ (rev_path xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev_path (xs @ ys) = rev_path ys @ rev_path xs
[PROOF STEP]
unfolding rev_path_def rev_append
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>(a, b, c). (c, b, a)) (rev ys @ rev xs) = map (\<lambda>(a, b, c). (c, b, a)) (rev ys) @ map (\<lambda>(a, b, c). (c, b, a)) (rev xs)
[PROOF STEP]
by auto


[STATEMENT]
lemma rev_path_double[simp]: "rev_path(rev_path xs)=xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev_path (rev_path xs) = xs
[PROOF STEP]
unfolding rev_path_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>(a, b, c). (c, b, a)) (rev (map (\<lambda>(a, b, c). (c, b, a)) (rev xs))) = xs
[PROOF STEP]
by (induct xs,auto)


[STATEMENT]
lemma del_UnEdge_node[simp]: "v\<in>nodes (del_unEdge u e u' G) \<longleftrightarrow> v\<in>nodes G  "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v \<in> nodes (del_unEdge u e u' G)) = (v \<in> nodes G)
[PROOF STEP]
by (metis del_unEdge_def select_convs(1))


[STATEMENT]
lemma [intro!]: "finite (edges G) \<Longrightarrow> finite (edges (del_unEdge u e u' G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (edges G) \<Longrightarrow> finite (edges (del_unEdge u e u' G))
[PROOF STEP]
by (metis del_unEdge_def finite_Diff select_convs(2))


[STATEMENT]
lemma [intro!]: "finite (nodes G) \<Longrightarrow> finite (nodes (del_unEdge u e u' G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (nodes G) \<Longrightarrow> finite (nodes (del_unEdge u e u' G))
[PROOF STEP]
by (metis del_unEdge_def select_convs(1))