[STATEMENT]
lemma update_trans:
  assumes "greater_mask \<pi> \<pi>'"
      and "greater_mask \<pi>' \<pi>''"
  shows "update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' = update_dm dm \<pi> \<pi>''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' = update_dm dm \<pi> \<pi>''
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' x = update_dm dm \<pi> \<pi>'' x
[PROOF STEP]
fix hl
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' x = update_dm dm \<pi> \<pi>'' x
[PROOF STEP]
show "update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = update_dm dm \<pi> \<pi>'' hl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = update_dm dm \<pi> \<pi>'' hl
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = update_dm dm \<pi> \<pi>'' hl
[PROOF STEP]
have "update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl \<longleftrightarrow> (update_dm dm \<pi> \<pi>') hl \<or> pgt (\<pi>' hl) (\<pi>'' hl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = (update_dm dm \<pi> \<pi>' hl \<or> pgt (\<pi>' hl) (\<pi>'' hl))
[PROOF STEP]
using update_dm_def
[PROOF STATE]
proof (prove)
using this:
update_dm ?dm ?\<pi> ?\<pi>' ?hl = (?dm ?hl \<or> pgt (?\<pi> ?hl) (?\<pi>' ?hl))

goal (1 subgoal):
 1. update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = (update_dm dm \<pi> \<pi>' hl \<or> pgt (\<pi>' hl) (\<pi>'' hl))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = (update_dm dm \<pi> \<pi>' hl \<or> pgt (\<pi>' hl) (\<pi>'' hl))

goal (1 subgoal):
 1. update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = update_dm dm \<pi> \<pi>'' hl
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = (update_dm dm \<pi> \<pi>' hl \<or> pgt (\<pi>' hl) (\<pi>'' hl))

goal (1 subgoal):
 1. update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = update_dm dm \<pi> \<pi>'' hl
[PROOF STEP]
have "... \<longleftrightarrow> dm hl \<or> pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (update_dm dm \<pi> \<pi>' hl \<or> pgt (\<pi>' hl) (\<pi>'' hl)) = (dm hl \<or> pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl))
[PROOF STEP]
using update_dm_def
[PROOF STATE]
proof (prove)
using this:
update_dm ?dm ?\<pi> ?\<pi>' ?hl = (?dm ?hl \<or> pgt (?\<pi> ?hl) (?\<pi>' ?hl))

goal (1 subgoal):
 1. (update_dm dm \<pi> \<pi>' hl \<or> pgt (\<pi>' hl) (\<pi>'' hl)) = (dm hl \<or> pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(update_dm dm \<pi> \<pi>' hl \<or> pgt (\<pi>' hl) (\<pi>'' hl)) = (dm hl \<or> pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl))

goal (1 subgoal):
 1. update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = update_dm dm \<pi> \<pi>'' hl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(update_dm dm \<pi> \<pi>' hl \<or> pgt (\<pi>' hl) (\<pi>'' hl)) = (dm hl \<or> pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl))

goal (1 subgoal):
 1. update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = update_dm dm \<pi> \<pi>'' hl
[PROOF STEP]
have "update_dm dm \<pi> \<pi>'' hl \<longleftrightarrow> dm hl \<or> pgt (\<pi> hl) (\<pi>'' hl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. update_dm dm \<pi> \<pi>'' hl = (dm hl \<or> pgt (\<pi> hl) (\<pi>'' hl))
[PROOF STEP]
using update_dm_def
[PROOF STATE]
proof (prove)
using this:
update_dm ?dm ?\<pi> ?\<pi>' ?hl = (?dm ?hl \<or> pgt (?\<pi> ?hl) (?\<pi>' ?hl))

goal (1 subgoal):
 1. update_dm dm \<pi> \<pi>'' hl = (dm hl \<or> pgt (\<pi> hl) (\<pi>'' hl))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
update_dm dm \<pi> \<pi>'' hl = (dm hl \<or> pgt (\<pi> hl) (\<pi>'' hl))

goal (1 subgoal):
 1. update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = update_dm dm \<pi> \<pi>'' hl
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
update_dm dm \<pi> \<pi>'' hl = (dm hl \<or> pgt (\<pi> hl) (\<pi>'' hl))

goal (1 subgoal):
 1. update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = update_dm dm \<pi> \<pi>'' hl
[PROOF STEP]
have "pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl) \<longleftrightarrow> pgt (\<pi> hl) (\<pi>'' hl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl)) = pgt (\<pi> hl) (\<pi>'' hl)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl) \<Longrightarrow> pgt (\<pi> hl) (\<pi>'' hl)
 2. pgt (\<pi> hl) (\<pi>'' hl) \<Longrightarrow> pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl)
[PROOF STEP]
show "pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl) \<Longrightarrow> pgt (\<pi> hl) (\<pi>'' hl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl) \<Longrightarrow> pgt (\<pi> hl) (\<pi>'' hl)
[PROOF STEP]
by (metis assms(1) assms(2) greater_mask_equiv_def greater_mask_properties(2) not_pgte_charact pgte_antisym)
[PROOF STATE]
proof (state)
this:
pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl) \<Longrightarrow> pgt (\<pi> hl) (\<pi>'' hl)

goal (1 subgoal):
 1. pgt (\<pi> hl) (\<pi>'' hl) \<Longrightarrow> pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl)
[PROOF STEP]
show "pgt (\<pi> hl) (\<pi>'' hl) \<Longrightarrow> pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pgt (\<pi> hl) (\<pi>'' hl) \<Longrightarrow> pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl)
[PROOF STEP]
by (metis assms(1) greater_mask_equiv_def not_pgte_charact pgte_antisym)
[PROOF STATE]
proof (state)
this:
pgt (\<pi> hl) (\<pi>'' hl) \<Longrightarrow> pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl)) = pgt (\<pi> hl) (\<pi>'' hl)

goal (1 subgoal):
 1. update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = update_dm dm \<pi> \<pi>'' hl
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = (update_dm dm \<pi> \<pi>' hl \<or> pgt (\<pi>' hl) (\<pi>'' hl))
(update_dm dm \<pi> \<pi>' hl \<or> pgt (\<pi>' hl) (\<pi>'' hl)) = (dm hl \<or> pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl))
update_dm dm \<pi> \<pi>'' hl = (dm hl \<or> pgt (\<pi> hl) (\<pi>'' hl))
(pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl)) = pgt (\<pi> hl) (\<pi>'' hl)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = (update_dm dm \<pi> \<pi>' hl \<or> pgt (\<pi>' hl) (\<pi>'' hl))
(update_dm dm \<pi> \<pi>' hl \<or> pgt (\<pi>' hl) (\<pi>'' hl)) = (dm hl \<or> pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl))
update_dm dm \<pi> \<pi>'' hl = (dm hl \<or> pgt (\<pi> hl) (\<pi>'' hl))
(pgt (\<pi> hl) (\<pi>' hl) \<or> pgt (\<pi>' hl) (\<pi>'' hl)) = pgt (\<pi> hl) (\<pi>'' hl)

goal (1 subgoal):
 1. update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = update_dm dm \<pi> \<pi>'' hl
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = update_dm dm \<pi> \<pi>'' hl

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
update_dm (update_dm dm \<pi> \<pi>') \<pi>' \<pi>'' hl = update_dm dm \<pi> \<pi>'' hl

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma equal_on_bmask_greater:
  assumes "equal_on_bmask \<pi>' h h'"
      and "greater_bmask \<pi>' \<pi>"
    shows "equal_on_bmask \<pi> h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equal_on_bmask \<pi> h h'
[PROOF STEP]
by (metis (mono_tags, lifting) assms(1) assms(2) equal_on_bmask_def greater_bmask_def)


[STATEMENT]
lemma update_dm_equal_bmask:
  assumes "\<pi> = add_masks \<pi>' m"
  shows "equal_on_bmask (update_dm dm \<pi> \<pi>') h' h \<longleftrightarrow> equal_on_mask m h h' \<and> equal_on_bmask dm h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equal_on_bmask (update_dm dm \<pi> \<pi>') h' h = (equal_on_mask m h h' \<and> equal_on_bmask dm h h')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. equal_on_bmask (update_dm dm \<pi> \<pi>') h' h = (equal_on_mask m h h' \<and> equal_on_bmask dm h h')
[PROOF STEP]
have "equal_on_bmask (update_dm dm \<pi> \<pi>') h' h \<longleftrightarrow> (\<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equal_on_bmask (update_dm dm \<pi> \<pi>') h' h = (\<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl)
[PROOF STEP]
by (simp add: equal_on_bmask_def)
[PROOF STATE]
proof (state)
this:
equal_on_bmask (update_dm dm \<pi> \<pi>') h' h = (\<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl)

goal (1 subgoal):
 1. equal_on_bmask (update_dm dm \<pi> \<pi>') h' h = (equal_on_mask m h h' \<and> equal_on_bmask dm h h')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
equal_on_bmask (update_dm dm \<pi> \<pi>') h' h = (\<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl)

goal (1 subgoal):
 1. equal_on_bmask (update_dm dm \<pi> \<pi>') h' h = (equal_on_mask m h h' \<and> equal_on_bmask dm h h')
[PROOF STEP]
have "\<And>hl. update_dm dm \<pi> \<pi>' hl \<longleftrightarrow> dm hl \<or> pgt (\<pi> hl) (\<pi>' hl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>hl. update_dm dm \<pi> \<pi>' hl = (dm hl \<or> pgt (\<pi> hl) (\<pi>' hl))
[PROOF STEP]
by (simp add: update_dm_def)
[PROOF STATE]
proof (state)
this:
update_dm dm \<pi> \<pi>' ?hl = (dm ?hl \<or> pgt (\<pi> ?hl) (\<pi>' ?hl))

goal (1 subgoal):
 1. equal_on_bmask (update_dm dm \<pi> \<pi>') h' h = (equal_on_mask m h h' \<and> equal_on_bmask dm h h')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
update_dm dm \<pi> \<pi>' ?hl = (dm ?hl \<or> pgt (\<pi> ?hl) (\<pi>' ?hl))

goal (1 subgoal):
 1. equal_on_bmask (update_dm dm \<pi> \<pi>') h' h = (equal_on_mask m h h' \<and> equal_on_bmask dm h h')
[PROOF STEP]
have "(\<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl) \<longleftrightarrow> equal_on_mask m h h' \<and> equal_on_bmask dm h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl) = (equal_on_mask m h h' \<and> equal_on_bmask dm h h')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl \<Longrightarrow> equal_on_mask m h h' \<and> equal_on_bmask dm h h'
 2. equal_on_mask m h h' \<and> equal_on_bmask dm h h' \<Longrightarrow> \<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl
[PROOF STEP]
show "\<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl \<Longrightarrow> equal_on_mask m h h' \<and> equal_on_bmask dm h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl \<Longrightarrow> equal_on_mask m h h' \<and> equal_on_bmask dm h h'
[PROOF STEP]
by (simp add: assms equal_on_bmask_def equal_on_mask_def padd.rep_eq pgt.rep_eq ppos.rep_eq update_dm_def)
[PROOF STATE]
proof (state)
this:
\<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl \<Longrightarrow> equal_on_mask m h h' \<and> equal_on_bmask dm h h'

goal (1 subgoal):
 1. equal_on_mask m h h' \<and> equal_on_bmask dm h h' \<Longrightarrow> \<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl
[PROOF STEP]
assume "equal_on_mask m h h' \<and> equal_on_bmask dm h h'"
[PROOF STATE]
proof (state)
this:
equal_on_mask m h h' \<and> equal_on_bmask dm h h'

goal (1 subgoal):
 1. equal_on_mask m h h' \<and> equal_on_bmask dm h h' \<Longrightarrow> \<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
equal_on_mask m h h' \<and> equal_on_bmask dm h h'
[PROOF STEP]
have "\<And>hl. update_dm dm \<pi> \<pi>' hl \<Longrightarrow> h' hl = h hl"
[PROOF STATE]
proof (prove)
using this:
equal_on_mask m h h' \<and> equal_on_bmask dm h h'

goal (1 subgoal):
 1. \<And>hl. update_dm dm \<pi> \<pi>' hl \<Longrightarrow> h' hl = h hl
[PROOF STEP]
by (metis (full_types) add.right_neutral add_masks.simps assms dual_order.strict_iff_order equal_on_bmask_def equal_on_mask_def padd.rep_eq pgt.rep_eq pnone.rep_eq ppos_eq_pnone update_dm_def)
[PROOF STATE]
proof (state)
this:
update_dm dm \<pi> \<pi>' ?hl \<Longrightarrow> h' ?hl = h ?hl

goal (1 subgoal):
 1. equal_on_mask m h h' \<and> equal_on_bmask dm h h' \<Longrightarrow> \<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
update_dm dm \<pi> \<pi>' ?hl \<Longrightarrow> h' ?hl = h ?hl
[PROOF STEP]
show "\<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl"
[PROOF STATE]
proof (prove)
using this:
update_dm dm \<pi> \<pi>' ?hl \<Longrightarrow> h' ?hl = h ?hl

goal (1 subgoal):
 1. \<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl) = (equal_on_mask m h h' \<and> equal_on_bmask dm h h')

goal (1 subgoal):
 1. equal_on_bmask (update_dm dm \<pi> \<pi>') h' h = (equal_on_mask m h h' \<and> equal_on_bmask dm h h')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl) = (equal_on_mask m h h' \<and> equal_on_bmask dm h h')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<forall>hl. update_dm dm \<pi> \<pi>' hl \<longrightarrow> h' hl = h hl) = (equal_on_mask m h h' \<and> equal_on_bmask dm h h')

goal (1 subgoal):
 1. equal_on_bmask (update_dm dm \<pi> \<pi>') h' h = (equal_on_mask m h h' \<and> equal_on_bmask dm h h')
[PROOF STEP]
by (simp add: calculation)
[PROOF STATE]
proof (state)
this:
equal_on_bmask (update_dm dm \<pi> \<pi>') h' h = (equal_on_mask m h h' \<and> equal_on_bmask dm h h')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma const_sum_mask_greater:
  assumes "add_masks a b = add_masks c d"
      and "greater_mask a c"
    shows "greater_mask d b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. greater_mask d b
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> greater_mask d b \<Longrightarrow> False
[PROOF STEP]
assume "\<not> greater_mask d b"
[PROOF STATE]
proof (state)
this:
\<not> greater_mask d b

goal (1 subgoal):
 1. \<not> greater_mask d b \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> greater_mask d b
[PROOF STEP]
obtain hl where "\<not> pgte (d hl) (b hl)"
[PROOF STATE]
proof (prove)
using this:
\<not> greater_mask d b

goal (1 subgoal):
 1. (\<And>hl. \<not> pgte (d hl) (b hl) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using greater_mask_equiv_def
[PROOF STATE]
proof (prove)
using this:
\<not> greater_mask d b
greater_mask ?\<pi>' ?\<pi> = (\<forall>hl. pgte (?\<pi>' hl) (?\<pi> hl))

goal (1 subgoal):
 1. (\<And>hl. \<not> pgte (d hl) (b hl) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> pgte (d hl) (b hl)

goal (1 subgoal):
 1. \<not> greater_mask d b \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> pgte (d hl) (b hl)
[PROOF STEP]
have "pgt (b hl) (d hl)"
[PROOF STATE]
proof (prove)
using this:
\<not> pgte (d hl) (b hl)

goal (1 subgoal):
 1. pgt (b hl) (d hl)
[PROOF STEP]
using not_pgte_charact
[PROOF STATE]
proof (prove)
using this:
\<not> pgte (d hl) (b hl)
(\<not> pgte ?a ?b) = pgt ?b ?a

goal (1 subgoal):
 1. pgt (b hl) (d hl)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pgt (b hl) (d hl)

goal (1 subgoal):
 1. \<not> greater_mask d b \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pgt (b hl) (d hl)
[PROOF STEP]
have "pgt (padd (a hl) (b hl)) (padd (c hl) (d hl))"
[PROOF STATE]
proof (prove)
using this:
pgt (b hl) (d hl)

goal (1 subgoal):
 1. pgt (padd (a hl) (b hl)) (padd (c hl) (d hl))
[PROOF STEP]
by (metis assms(2) greater_mask_equiv_def padd_comm pgte_pgt)
[PROOF STATE]
proof (state)
this:
pgt (padd (a hl) (b hl)) (padd (c hl) (d hl))

goal (1 subgoal):
 1. \<not> greater_mask d b \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pgt (padd (a hl) (b hl)) (padd (c hl) (d hl))
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
pgt (padd (a hl) (b hl)) (padd (c hl) (d hl))

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis add_masks.simps assms(1) not_pgte_charact order_refl pgte.rep_eq)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_masks_cancellative:
  assumes "add_masks b c = add_masks b d"
    shows "c = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c = d
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. c x = d x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. c x = d x
[PROOF STEP]
show "c x = d x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c x = d x
[PROOF STEP]
by (metis assms(1) const_sum_mask_greater greater_mask_properties(1) greater_mask_properties(3))
[PROOF STATE]
proof (state)
this:
c x = d x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma equal_on_maskI:
  assumes "\<And>hl. ppos (\<pi> hl) \<Longrightarrow> h hl = h' hl"
  shows "equal_on_mask \<pi> h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equal_on_mask \<pi> h h'
[PROOF STEP]
by (simp add: assms equal_on_mask_def)


[STATEMENT]
lemma greater_equal_on_mask:
  assumes "equal_on_mask \<pi>' h h'"
      and "greater_mask \<pi>' \<pi>"
    shows "equal_on_mask \<pi> h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equal_on_mask \<pi> h h'
[PROOF STEP]
proof (rule equal_on_maskI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>hl. ppos (\<pi> hl) \<Longrightarrow> h hl = h' hl
[PROOF STEP]
fix hl
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>hl. ppos (\<pi> hl) \<Longrightarrow> h hl = h' hl
[PROOF STEP]
assume asm: "ppos (\<pi> hl)"
[PROOF STATE]
proof (state)
this:
ppos (\<pi> hl)

goal (1 subgoal):
 1. \<And>hl. ppos (\<pi> hl) \<Longrightarrow> h hl = h' hl
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ppos (\<pi> hl)
[PROOF STEP]
show "h hl = h' hl"
[PROOF STATE]
proof (prove)
using this:
ppos (\<pi> hl)

goal (1 subgoal):
 1. h hl = h' hl
[PROOF STEP]
by (metis assms(1) assms(2) equal_on_mask_def greater_mask_equiv_def less_le_trans pgte.rep_eq ppos.rep_eq)
[PROOF STATE]
proof (state)
this:
h hl = h' hl

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma equal_on_mask_sum:
  "equal_on_mask \<pi>1 h h' \<and> equal_on_mask \<pi>2 h h' \<longleftrightarrow> equal_on_mask (add_masks \<pi>1 \<pi>2) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (equal_on_mask \<pi>1 h h' \<and> equal_on_mask \<pi>2 h h') = equal_on_mask (add_masks \<pi>1 \<pi>2) h h'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. equal_on_mask \<pi>1 h h' \<and> equal_on_mask \<pi>2 h h' \<Longrightarrow> equal_on_mask (add_masks \<pi>1 \<pi>2) h h'
 2. equal_on_mask (add_masks \<pi>1 \<pi>2) h h' \<Longrightarrow> equal_on_mask \<pi>1 h h' \<and> equal_on_mask \<pi>2 h h'
[PROOF STEP]
show "equal_on_mask (add_masks \<pi>1 \<pi>2) h h' \<Longrightarrow> equal_on_mask \<pi>1 h h' \<and> equal_on_mask \<pi>2 h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equal_on_mask (add_masks \<pi>1 \<pi>2) h h' \<Longrightarrow> equal_on_mask \<pi>1 h h' \<and> equal_on_mask \<pi>2 h h'
[PROOF STEP]
using add_masks_comm greater_equal_on_mask greater_mask_def
[PROOF STATE]
proof (prove)
using this:
add_masks ?a ?b = add_masks ?b ?a
\<lbrakk>equal_on_mask ?\<pi>' ?h ?h'; greater_mask ?\<pi>' ?\<pi>\<rbrakk> \<Longrightarrow> equal_on_mask ?\<pi> ?h ?h'
greater_mask ?\<pi>' ?\<pi> = (\<exists>r. ?\<pi>' = add_masks ?\<pi> r)

goal (1 subgoal):
 1. equal_on_mask (add_masks \<pi>1 \<pi>2) h h' \<Longrightarrow> equal_on_mask \<pi>1 h h' \<and> equal_on_mask \<pi>2 h h'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
equal_on_mask (add_masks \<pi>1 \<pi>2) h h' \<Longrightarrow> equal_on_mask \<pi>1 h h' \<and> equal_on_mask \<pi>2 h h'

goal (1 subgoal):
 1. equal_on_mask \<pi>1 h h' \<and> equal_on_mask \<pi>2 h h' \<Longrightarrow> equal_on_mask (add_masks \<pi>1 \<pi>2) h h'
[PROOF STEP]
assume asm0: "equal_on_mask \<pi>1 h h' \<and> equal_on_mask \<pi>2 h h'"
[PROOF STATE]
proof (state)
this:
equal_on_mask \<pi>1 h h' \<and> equal_on_mask \<pi>2 h h'

goal (1 subgoal):
 1. equal_on_mask \<pi>1 h h' \<and> equal_on_mask \<pi>2 h h' \<Longrightarrow> equal_on_mask (add_masks \<pi>1 \<pi>2) h h'
[PROOF STEP]
show "equal_on_mask (add_masks \<pi>1 \<pi>2) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equal_on_mask (add_masks \<pi>1 \<pi>2) h h'
[PROOF STEP]
proof (rule equal_on_maskI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>hl. ppos (add_masks \<pi>1 \<pi>2 hl) \<Longrightarrow> h hl = h' hl
[PROOF STEP]
fix hl
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>hl. ppos (add_masks \<pi>1 \<pi>2 hl) \<Longrightarrow> h hl = h' hl
[PROOF STEP]
assume "ppos (add_masks \<pi>1 \<pi>2 hl)"
[PROOF STATE]
proof (state)
this:
ppos (add_masks \<pi>1 \<pi>2 hl)

goal (1 subgoal):
 1. \<And>hl. ppos (add_masks \<pi>1 \<pi>2 hl) \<Longrightarrow> h hl = h' hl
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ppos (add_masks \<pi>1 \<pi>2 hl)
[PROOF STEP]
show "h hl = h' hl"
[PROOF STATE]
proof (prove)
using this:
ppos (add_masks \<pi>1 \<pi>2 hl)

goal (1 subgoal):
 1. h hl = h' hl
[PROOF STEP]
proof (cases "ppos (\<pi>1 hl)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>ppos (add_masks \<pi>1 \<pi>2 hl); ppos (\<pi>1 hl)\<rbrakk> \<Longrightarrow> h hl = h' hl
 2. \<lbrakk>ppos (add_masks \<pi>1 \<pi>2 hl); \<not> ppos (\<pi>1 hl)\<rbrakk> \<Longrightarrow> h hl = h' hl
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ppos (\<pi>1 hl)

goal (2 subgoals):
 1. \<lbrakk>ppos (add_masks \<pi>1 \<pi>2 hl); ppos (\<pi>1 hl)\<rbrakk> \<Longrightarrow> h hl = h' hl
 2. \<lbrakk>ppos (add_masks \<pi>1 \<pi>2 hl); \<not> ppos (\<pi>1 hl)\<rbrakk> \<Longrightarrow> h hl = h' hl
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ppos (\<pi>1 hl)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ppos (\<pi>1 hl)

goal (1 subgoal):
 1. h hl = h' hl
[PROOF STEP]
by (meson asm0 equal_on_mask_def)
[PROOF STATE]
proof (state)
this:
h hl = h' hl

goal (1 subgoal):
 1. \<lbrakk>ppos (add_masks \<pi>1 \<pi>2 hl); \<not> ppos (\<pi>1 hl)\<rbrakk> \<Longrightarrow> h hl = h' hl
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>ppos (add_masks \<pi>1 \<pi>2 hl); \<not> ppos (\<pi>1 hl)\<rbrakk> \<Longrightarrow> h hl = h' hl
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> ppos (\<pi>1 hl)

goal (1 subgoal):
 1. \<lbrakk>ppos (add_masks \<pi>1 \<pi>2 hl); \<not> ppos (\<pi>1 hl)\<rbrakk> \<Longrightarrow> h hl = h' hl
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> ppos (\<pi>1 hl)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> ppos (\<pi>1 hl)

goal (1 subgoal):
 1. h hl = h' hl
[PROOF STEP]
by (metis asm0 \<open>ppos (add_masks \<pi>1 \<pi>2 hl)\<close> add_masks.simps equal_on_mask_def padd_zero ppos_eq_pnone)
[PROOF STATE]
proof (state)
this:
h hl = h' hl

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
h hl = h' hl

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
equal_on_mask (add_masks \<pi>1 \<pi>2) h h'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_larger_mask:
  "valid_mask \<pi> \<longleftrightarrow> greater_mask full_mask \<pi> "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_mask \<pi> = greater_mask full_mask \<pi>
[PROOF STEP]
by (metis fst_eqD full_mask_def greater_maskI greater_mask_def not_one_le_zero not_pgte_charact pgt_implies_pgte pgte.rep_eq pnone.rep_eq pwrite.rep_eq surjective_pairing upper_valid_aux valid_mask.elims(1))


[STATEMENT]
lemma valid_mask_full_mask:
  "valid_mask full_mask"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_mask full_mask
[PROOF STEP]
using greater_mask_properties(1) valid_larger_mask
[PROOF STATE]
proof (prove)
using this:
greater_mask ?\<pi> ?\<pi>
valid_mask ?\<pi> = greater_mask full_mask ?\<pi>

goal (1 subgoal):
 1. valid_mask full_mask
[PROOF STEP]
by blast


[STATEMENT]
lemma mult_greater:
  assumes "greater_mask a b"
  shows "greater_mask (multiply_mask p a) (multiply_mask p b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. greater_mask (multiply_mask p a) (multiply_mask p b)
[PROOF STEP]
by (metis (full_types) assms greater_mask_equiv_def multiply_mask_def p_greater_exists pmult_distr)


[STATEMENT]
lemma mult_write_mask:
  "multiply_mask pwrite \<pi> = \<pi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiply_mask pwrite \<pi> = \<pi>
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. multiply_mask pwrite \<pi> x = \<pi> x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. multiply_mask pwrite \<pi> x = \<pi> x
[PROOF STEP]
show "multiply_mask pwrite \<pi> x = \<pi> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiply_mask pwrite \<pi> x = \<pi> x
[PROOF STEP]
by (simp add: multiply_mask_def pmult_special(1))
[PROOF STATE]
proof (state)
this:
multiply_mask pwrite \<pi> x = \<pi> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_distr_masks:
  "multiply_mask a (add_masks b c) = add_masks (multiply_mask a b) (multiply_mask a c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiply_mask a (add_masks b c) = add_masks (multiply_mask a b) (multiply_mask a c)
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. multiply_mask a (add_masks b c) x = add_masks (multiply_mask a b) (multiply_mask a c) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. multiply_mask a (add_masks b c) x = add_masks (multiply_mask a b) (multiply_mask a c) x
[PROOF STEP]
show "multiply_mask a (add_masks b c) x = add_masks (multiply_mask a b) (multiply_mask a c) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiply_mask a (add_masks b c) x = add_masks (multiply_mask a b) (multiply_mask a c) x
[PROOF STEP]
by (simp add: multiply_mask_def pmult_distr)
[PROOF STATE]
proof (state)
this:
multiply_mask a (add_masks b c) x = add_masks (multiply_mask a b) (multiply_mask a c) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_add_states:
  "multiply_mask (padd a b) \<pi> = add_masks (multiply_mask a \<pi>) (multiply_mask b \<pi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiply_mask (padd a b) \<pi> = add_masks (multiply_mask a \<pi>) (multiply_mask b \<pi>)
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. multiply_mask (padd a b) \<pi> x = add_masks (multiply_mask a \<pi>) (multiply_mask b \<pi>) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. multiply_mask (padd a b) \<pi> x = add_masks (multiply_mask a \<pi>) (multiply_mask b \<pi>) x
[PROOF STEP]
show "multiply_mask (padd a b) \<pi> x = add_masks (multiply_mask a \<pi>) (multiply_mask b \<pi>) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiply_mask (padd a b) \<pi> x = add_masks (multiply_mask a \<pi>) (multiply_mask b \<pi>) x
[PROOF STEP]
by (simp add: multiply_mask_def pmult_comm pmult_distr)
[PROOF STATE]
proof (state)
this:
multiply_mask (padd a b) \<pi> x = add_masks (multiply_mask a \<pi>) (multiply_mask b \<pi>) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma upper_boundedI:
  assumes "\<And>hl. pgte p (\<pi> hl)"
  shows "upper_bounded \<pi> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_bounded \<pi> p
[PROOF STEP]
by (simp add: assms upper_bounded_def)


[STATEMENT]
lemma upper_bounded_smaller:
  assumes "upper_bounded \<pi> a"
  shows "upper_bounded (multiply_mask p \<pi>) (pmult p a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_bounded (multiply_mask p \<pi>) (pmult p a)
[PROOF STEP]
by (metis assms multiply_mask_def p_greater_exists pmult_distr upper_bounded_def)


[STATEMENT]
lemma upper_bounded_bigger:
  assumes "upper_bounded \<pi> a"
      and "pgte b a"
    shows "upper_bounded \<pi> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_bounded \<pi> b
[PROOF STEP]
by (meson assms(1) assms(2) order_trans pgte.rep_eq upper_bounded_def)


[STATEMENT]
lemma valid_mult:
  assumes "valid_mask \<pi>"
      and "pgte pwrite p"
    shows "valid_mask (multiply_mask p \<pi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_mask (multiply_mask p \<pi>)
[PROOF STEP]
proof (rule valid_maskI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>hl. pgte pwrite (multiply_mask p \<pi> hl)
 2. \<And>f. multiply_mask p \<pi> (null, f) = pnone
[PROOF STEP]
have "upper_bounded \<pi> pwrite"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_bounded \<pi> pwrite
[PROOF STEP]
using assms(1) upper_bounded_def
[PROOF STATE]
proof (prove)
using this:
valid_mask \<pi>
upper_bounded ?\<pi> ?p = (\<forall>hl. pgte ?p (?\<pi> hl))

goal (1 subgoal):
 1. upper_bounded \<pi> pwrite
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
upper_bounded \<pi> pwrite

goal (2 subgoals):
 1. \<And>hl. pgte pwrite (multiply_mask p \<pi> hl)
 2. \<And>f. multiply_mask p \<pi> (null, f) = pnone
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
upper_bounded \<pi> pwrite
[PROOF STEP]
have "upper_bounded (multiply_mask p \<pi>) (pmult p pwrite)"
[PROOF STATE]
proof (prove)
using this:
upper_bounded \<pi> pwrite

goal (1 subgoal):
 1. upper_bounded (multiply_mask p \<pi>) (pmult p pwrite)
[PROOF STEP]
by (simp add: upper_bounded_smaller)
[PROOF STATE]
proof (state)
this:
upper_bounded (multiply_mask p \<pi>) (pmult p pwrite)

goal (2 subgoals):
 1. \<And>hl. pgte pwrite (multiply_mask p \<pi> hl)
 2. \<And>f. multiply_mask p \<pi> (null, f) = pnone
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
upper_bounded (multiply_mask p \<pi>) (pmult p pwrite)
[PROOF STEP]
show "\<And>hl. pgte pwrite (multiply_mask p \<pi> hl)"
[PROOF STATE]
proof (prove)
using this:
upper_bounded (multiply_mask p \<pi>) (pmult p pwrite)

goal (1 subgoal):
 1. \<And>hl. pgte pwrite (multiply_mask p \<pi> hl)
[PROOF STEP]
by (metis assms(2) pmult_comm pmult_special(1) upper_bounded_bigger upper_bounded_def)
[PROOF STATE]
proof (state)
this:
pgte pwrite (multiply_mask p \<pi> ?hl)

goal (1 subgoal):
 1. \<And>f. multiply_mask p \<pi> (null, f) = pnone
[PROOF STEP]
show "\<And>f. multiply_mask p \<pi> (null, f) = pnone"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. multiply_mask p \<pi> (null, f) = pnone
[PROOF STEP]
by (metis Rep_prat_inverse add_0_left assms(1) multiply_mask_def padd.rep_eq padd_cancellative pmult_distr pnone.rep_eq valid_mask.elims(1))
[PROOF STATE]
proof (state)
this:
multiply_mask p \<pi> (null, ?f) = pnone

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_sum:
  assumes "valid_mask a"
      and "valid_mask b"
      and "upper_bounded a ma"
      and "upper_bounded b mb"
      and "pgte pwrite (padd ma mb)"
    shows "valid_mask (add_masks a b)"
      and "upper_bounded (add_masks a b) (padd ma mb)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_mask (add_masks a b) &&& upper_bounded (add_masks a b) (padd ma mb)
[PROOF STEP]
proof (rule valid_maskI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>hl. pgte pwrite (add_masks a b hl)
 2. \<And>f. add_masks a b (null, f) = pnone
 3. upper_bounded (add_masks a b) (padd ma mb)
[PROOF STEP]
show "\<And>hl. pgte pwrite (add_masks a b hl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>hl. pgte pwrite (add_masks a b hl)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>hl. pgte pwrite (add_masks a b hl)
[PROOF STEP]
fix hl
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>hl. pgte pwrite (add_masks a b hl)
[PROOF STEP]
have "pgte (padd ma mb) (add_masks a b hl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pgte (padd ma mb) (add_masks a b hl)
[PROOF STEP]
by (metis (mono_tags, lifting) add_masks.simps add_mono_thms_linordered_semiring(1) assms(3) assms(4) padd.rep_eq pgte.rep_eq upper_bounded_def)
[PROOF STATE]
proof (state)
this:
pgte (padd ma mb) (add_masks a b hl)

goal (1 subgoal):
 1. \<And>hl. pgte pwrite (add_masks a b hl)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pgte (padd ma mb) (add_masks a b hl)
[PROOF STEP]
show "pgte pwrite (add_masks a b hl)"
[PROOF STATE]
proof (prove)
using this:
pgte (padd ma mb) (add_masks a b hl)

goal (1 subgoal):
 1. pgte pwrite (add_masks a b hl)
[PROOF STEP]
by (meson assms(5) dual_order.trans pgte.rep_eq)
[PROOF STATE]
proof (state)
this:
pgte pwrite (add_masks a b hl)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pgte pwrite (add_masks a b ?hl)

goal (2 subgoals):
 1. \<And>f. add_masks a b (null, f) = pnone
 2. upper_bounded (add_masks a b) (padd ma mb)
[PROOF STEP]
show "\<And>f. add_masks a b (null, f) = pnone"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. add_masks a b (null, f) = pnone
[PROOF STEP]
by (metis Rep_prat_inverse add_0_left add_masks.simps assms(1) assms(2) padd.rep_eq pnone.rep_eq valid_mask.simps)
[PROOF STATE]
proof (state)
this:
add_masks a b (null, ?f) = pnone

goal (1 subgoal):
 1. upper_bounded (add_masks a b) (padd ma mb)
[PROOF STEP]
show "upper_bounded (add_masks a b) (padd ma mb)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_bounded (add_masks a b) (padd ma mb)
[PROOF STEP]
using add_mono_thms_linordered_semiring(1) assms(3) assms(4) padd.rep_eq pgte.rep_eq upper_bounded_def
[PROOF STATE]
proof (prove)
using this:
?i \<le> ?j \<and> ?k \<le> ?l \<Longrightarrow> ?i + ?k \<le> ?j + ?l
upper_bounded a ma
upper_bounded b mb
Rep_prat (padd ?x ?xa) = Rep_prat ?x + Rep_prat ?xa
pgte ?x ?xa = (Rep_prat ?xa \<le> Rep_prat ?x)
upper_bounded ?\<pi> ?p = (\<forall>hl. pgte ?p (?\<pi> hl))

goal (1 subgoal):
 1. upper_bounded (add_masks a b) (padd ma mb)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
upper_bounded (add_masks a b) (padd ma mb)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_multiply:
  assumes "valid_mask a"
      and "upper_bounded a ma"
      and "pgte pwrite (pmult ma p)"
    shows "valid_mask (multiply_mask p a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_mask (multiply_mask p a)
[PROOF STEP]
by (metis (no_types, opaque_lifting) assms(1) assms(2) assms(3) multiply_mask_def pmult_comm pmult_special(2) upper_bounded_bigger upper_bounded_def upper_bounded_smaller valid_mask.elims(1))


[STATEMENT]
lemma greater_mult:
  assumes "greater_mask a b"
  shows "greater_mask (multiply_mask p a) (multiply_mask p b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. greater_mask (multiply_mask p a) (multiply_mask p b)
[PROOF STEP]
by (metis Rep_prat assms greater_mask_equiv_def mem_Collect_eq mult_left_mono multiply_mask_def pgte.rep_eq pmult.rep_eq)


[STATEMENT]
lemma suffix_state_prop[simp]:
  shows "\<lceil>P\<rceil> (\<sigma> |\<^sub>s i) = P (\<sigma> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>P\<rceil> (\<sigma> |\<^sub>s i) = P (\<sigma> i)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ((\<sigma> |\<^sub>s i) 0) = P (\<sigma> i)
[PROOF STEP]
by simp


[STATEMENT]
lemma alwaysI[intro]:
  assumes "\<And>i. P (\<sigma> |\<^sub>s i)"
  shows "(\<box>P) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>P) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. P (\<sigma> |\<^sub>s i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P (\<sigma> |\<^sub>s ?i)

goal (1 subgoal):
 1. \<forall>i. P (\<sigma> |\<^sub>s i)
[PROOF STEP]
by blast


[STATEMENT]
lemma alwaysD:
  assumes "(\<box>P) \<sigma>"
  shows "P (\<sigma> |\<^sub>s i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (\<sigma> |\<^sub>s i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<box>P) \<sigma>

goal (1 subgoal):
 1. P (\<sigma> |\<^sub>s i)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
\<forall>i. P (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. P (\<sigma> |\<^sub>s i)
[PROOF STEP]
by blast


[STATEMENT]
lemma alwaysE: "\<lbrakk>(\<box>P) \<sigma>; P (\<sigma> |\<^sub>s i) \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<box>P) \<sigma>; P (\<sigma> |\<^sub>s i) \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i. P (\<sigma> |\<^sub>s i); P (\<sigma> |\<^sub>s i) \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
[PROOF STEP]
by blast


[STATEMENT]
lemma always_induct:
  assumes "P \<sigma>"
  assumes "(\<box>(P \<^bold>\<longrightarrow> \<circle>P)) \<sigma>"
  shows "(\<box>P) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>P) \<sigma>
[PROOF STEP]
proof(rule alwaysI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. P (\<sigma> |\<^sub>s i)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. P (\<sigma> |\<^sub>s i)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
P \<sigma>
(\<box>(\<lambda>s. P s \<longrightarrow> (\<circle>P) s)) \<sigma>
[PROOF STEP]
show "P (\<sigma> |\<^sub>s i)"
[PROOF STATE]
proof (prove)
using this:
P \<sigma>
(\<box>(\<lambda>s. P s \<longrightarrow> (\<circle>P) s)) \<sigma>

goal (1 subgoal):
 1. P (\<sigma> |\<^sub>s i)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
P \<sigma>
\<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> P (\<sigma> |\<^sub>s i |\<^sub>s 1)

goal (1 subgoal):
 1. P (\<sigma> |\<^sub>s i)
[PROOF STEP]
by (induct i) simp_all
[PROOF STATE]
proof (state)
this:
P (\<sigma> |\<^sub>s i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma seq_comp:
  fixes \<sigma> :: "'a seq"
  fixes P :: "'b seq_pred"
  fixes f :: "'a \<Rightarrow> 'b"
  shows
    "(\<box>P) (f \<circ> \<sigma>) \<longleftrightarrow> (\<box>(\<lambda>\<sigma>. P (f \<circ> \<sigma>))) \<sigma>"
    "(\<diamond>P) (f \<circ> \<sigma>) \<longleftrightarrow> (\<diamond>(\<lambda>\<sigma>. P (f \<circ> \<sigma>))) \<sigma>"
    "(P \<U> Q) (f \<circ> \<sigma>) \<longleftrightarrow> ((\<lambda>\<sigma>. P (f \<circ> \<sigma>)) \<U> (\<lambda>\<sigma>. Q (f \<circ> \<sigma>))) \<sigma>"
    "(P \<W> Q) (f \<circ> \<sigma>) \<longleftrightarrow> ((\<lambda>\<sigma>. P (f \<circ> \<sigma>)) \<W> (\<lambda>\<sigma>. Q (f \<circ> \<sigma>))) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<box>P) (f \<circ> \<sigma>) = (\<box>(\<lambda>\<sigma>. P (f \<circ> \<sigma>))) \<sigma> &&& (\<diamond>P) (f \<circ> \<sigma>) = (\<diamond>(\<lambda>\<sigma>. P (f \<circ> \<sigma>))) \<sigma>) &&& (P \<U> Q) (f \<circ> \<sigma>) = ((\<lambda>\<sigma>. P (f \<circ> \<sigma>)) \<U> (\<lambda>\<sigma>. Q (f \<circ> \<sigma>))) \<sigma> &&& (P \<W> Q) (f \<circ> \<sigma>) = ((\<lambda>\<sigma>. P (f \<circ> \<sigma>)) \<W> (\<lambda>\<sigma>. Q (f \<circ> \<sigma>))) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>i. P ((f \<circ> \<sigma>) |\<^sub>s i)) = (\<forall>i. P (f \<circ> \<sigma> |\<^sub>s i)) &&& (\<exists>i. P ((f \<circ> \<sigma>) |\<^sub>s i) \<and> (\<forall>k<i. True)) = (\<exists>i. P (f \<circ> \<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True))) &&& (\<exists>i. Q ((f \<circ> \<sigma>) |\<^sub>s i) \<and> (\<forall>k<i. P ((f \<circ> \<sigma>) |\<^sub>s k))) = (\<exists>i. Q (f \<circ> \<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (f \<circ> \<sigma> |\<^sub>s k))) &&& ((\<exists>i. Q ((f \<circ> \<sigma>) |\<^sub>s i) \<and> (\<forall>k<i. P ((f \<circ> \<sigma>) |\<^sub>s k))) \<or> (\<forall>i. P ((f \<circ> \<sigma>) |\<^sub>s i))) = ((\<exists>i. Q (f \<circ> \<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (f \<circ> \<sigma> |\<^sub>s k))) \<or> (\<forall>i. P (f \<circ> \<sigma> |\<^sub>s i)))
[PROOF STEP]
by simp_all


[STATEMENT]
lemma nextI[intro]:
  assumes "P (\<sigma> |\<^sub>s Suc 0)"
  shows "(\<circle>P) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<circle>P) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P (\<sigma> |\<^sub>s Suc 0)

goal (1 subgoal):
 1. (\<circle>P) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
P (\<sigma> |\<^sub>s Suc 0)

goal (1 subgoal):
 1. P (\<sigma> |\<^sub>s 1)
[PROOF STEP]
by simp


[STATEMENT]
lemma untilI[intro]:
  assumes "Q (\<sigma> |\<^sub>s i)"
  assumes "\<forall>k<i. P (\<sigma> |\<^sub>s k)"
  shows "(P \<U> Q) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<U> Q) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Q (\<sigma> |\<^sub>s i)
\<forall>k<i. P (\<sigma> |\<^sub>s k)

goal (1 subgoal):
 1. \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))
[PROOF STEP]
by blast


[STATEMENT]
lemma untilE:
  assumes "(P \<U> Q) \<sigma>"
  obtains i where "Q (\<sigma> |\<^sub>s i)" and "\<forall>k<i. P (\<sigma> |\<^sub>s k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(P \<U> Q) \<sigma>

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding until_def
[PROOF STATE]
proof (prove)
using this:
\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>Q (\<sigma> |\<^sub>s i); \<forall>k<i. P (\<sigma> |\<^sub>s k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma eventuallyI[intro]:
  assumes "P (\<sigma> |\<^sub>s i)"
  shows "(\<diamond>P) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<diamond>P) \<sigma>
[PROOF STEP]
unfolding eventually_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. True) \<U> P) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. ((\<lambda>s. True) \<U> P) \<sigma>
[PROOF STEP]
by blast


[STATEMENT]
lemma eventuallyE[elim]:
  assumes "(\<diamond>P) \<sigma>"
  obtains i where "P (\<sigma> |\<^sub>s i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. P (\<sigma> |\<^sub>s i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<diamond>P) \<sigma>

goal (1 subgoal):
 1. (\<And>i. P (\<sigma> |\<^sub>s i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
\<exists>i. P (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True)

goal (1 subgoal):
 1. (\<And>i. P (\<sigma> |\<^sub>s i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast elim: untilE)


[STATEMENT]
lemma unless_alwaysI:
  assumes "(\<box> P) \<sigma>"
  shows "(P \<W> Q) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<W> Q) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<box>P) \<sigma>

goal (1 subgoal):
 1. (P \<W> Q) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
\<forall>i. P (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. (\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) \<or> (\<forall>i. P (\<sigma> |\<^sub>s i))
[PROOF STEP]
by blast


[STATEMENT]
lemma unless_untilI:
  assumes "Q (\<sigma> |\<^sub>s j)"
  assumes "\<And>i. i < j \<Longrightarrow> P (\<sigma> |\<^sub>s i)"
  shows "(P \<W> Q) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<W> Q) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) \<or> (\<forall>i. P (\<sigma> |\<^sub>s i))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Q (\<sigma> |\<^sub>s j)
?i < j \<Longrightarrow> P (\<sigma> |\<^sub>s ?i)

goal (1 subgoal):
 1. (\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) \<or> (\<forall>i. P (\<sigma> |\<^sub>s i))
[PROOF STEP]
by blast


[STATEMENT]
lemma always_imp_refl[iff]:
  shows "(P \<^bold>\<hookrightarrow> P) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<longrightarrow> P s)) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> P (\<sigma> |\<^sub>s i)
[PROOF STEP]
by blast


[STATEMENT]
lemma always_imp_trans:
  assumes "(P \<^bold>\<hookrightarrow> Q) \<sigma>"
  assumes "(Q \<^bold>\<hookrightarrow> R) \<sigma>"
  shows "(P \<^bold>\<hookrightarrow> R) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<longrightarrow> R s)) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. P s \<longrightarrow> Q s)) \<sigma>
(\<box>(\<lambda>s. Q s \<longrightarrow> R s)) \<sigma>

goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<longrightarrow> R s)) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
\<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> Q (\<sigma> |\<^sub>s i)
\<forall>i. Q (\<sigma> |\<^sub>s i) \<longrightarrow> R (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. \<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> R (\<sigma> |\<^sub>s i)
[PROOF STEP]
by blast


[STATEMENT]
lemma always_imp_mp:
  assumes "(P \<^bold>\<hookrightarrow> Q) \<sigma>"
  assumes "P \<sigma>"
  shows "Q \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. P s \<longrightarrow> Q s)) \<sigma>
P \<sigma>

goal (1 subgoal):
 1. Q \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
\<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> Q (\<sigma> |\<^sub>s i)
P \<sigma>

goal (1 subgoal):
 1. Q \<sigma>
[PROOF STEP]
by (metis suffix_zero)


[STATEMENT]
lemma always_imp_mp_suffix:
  assumes "(P \<^bold>\<hookrightarrow> Q) \<sigma>"
  assumes "P (\<sigma> |\<^sub>s i)"
  shows "Q (\<sigma> |\<^sub>s i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q (\<sigma> |\<^sub>s i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. P s \<longrightarrow> Q s)) \<sigma>
P (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. Q (\<sigma> |\<^sub>s i)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
\<forall>i. P (\<sigma> |\<^sub>s i) \<longrightarrow> Q (\<sigma> |\<^sub>s i)
P (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. Q (\<sigma> |\<^sub>s i)
[PROOF STEP]
by metis


[STATEMENT]
lemma necessitation:
  "(\<And>s. P s) \<Longrightarrow> (\<box>P) \<sigma>"
  "(\<And>s. P s) \<Longrightarrow> (\<diamond>P) \<sigma>"
  "(\<And>s. P s) \<Longrightarrow> (P \<W> Q) \<sigma>"
  "(\<And>s. Q s) \<Longrightarrow> (P \<U> Q) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<And>s. P s) \<Longrightarrow> (\<box>P) \<sigma>) &&& ((\<And>s. P s) \<Longrightarrow> (\<diamond>P) \<sigma>)) &&& ((\<And>s. P s) \<Longrightarrow> (P \<W> Q) \<sigma>) &&& ((\<And>s. Q s) \<Longrightarrow> (P \<U> Q) \<sigma>)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<And>s. P s) \<Longrightarrow> \<forall>i. P (\<sigma> |\<^sub>s i)) &&& ((\<And>s. P s) \<Longrightarrow> \<exists>i. P (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True))) &&& ((\<And>s. P s) \<Longrightarrow> (\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) \<or> (\<forall>i. P (\<sigma> |\<^sub>s i))) &&& ((\<And>s. Q s) \<Longrightarrow> \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k)))
[PROOF STEP]
by auto


[STATEMENT]
lemma cong:
  "(\<And>s. P s = P' s) \<Longrightarrow> \<lceil>P\<rceil> = \<lceil>P'\<rceil>"
  "(\<And>\<sigma>. P \<sigma> = P' \<sigma>) \<Longrightarrow> (\<box>P) = (\<box>P')"
  "(\<And>\<sigma>. P \<sigma> = P' \<sigma>) \<Longrightarrow> (\<diamond>P) = (\<diamond>P')"
  "(\<And>\<sigma>. P \<sigma> = P' \<sigma>) \<Longrightarrow> (\<circle>P) = (\<circle>P')"
  "\<lbrakk>\<And>\<sigma>. P \<sigma> = P' \<sigma>; \<And>\<sigma>. Q \<sigma> = Q' \<sigma>\<rbrakk> \<Longrightarrow> (P \<U> Q) = (P' \<U> Q')"
  "\<lbrakk>\<And>\<sigma>. P \<sigma> = P' \<sigma>; \<And>\<sigma>. Q \<sigma> = Q' \<sigma>\<rbrakk> \<Longrightarrow> (P \<W> Q) = (P' \<W> Q')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<And>s. P s = P' s) \<Longrightarrow> \<lceil>P\<rceil> = \<lceil>P'\<rceil>) &&& ((\<And>\<sigma>. P \<sigma> = P' \<sigma>) \<Longrightarrow> \<box>P = \<box>P') &&& ((\<And>\<sigma>. P \<sigma> = P' \<sigma>) \<Longrightarrow> \<diamond>P = \<diamond>P')) &&& ((\<And>\<sigma>. P \<sigma> = P' \<sigma>) \<Longrightarrow> \<circle>P = \<circle>P') &&& (\<lbrakk>\<And>\<sigma>. P \<sigma> = P' \<sigma>; \<And>\<sigma>. Q \<sigma> = Q' \<sigma>\<rbrakk> \<Longrightarrow> (P \<U> Q) = (P' \<U> Q')) &&& (\<lbrakk>\<And>\<sigma>. P \<sigma> = P' \<sigma>; \<And>\<sigma>. Q \<sigma> = Q' \<sigma>\<rbrakk> \<Longrightarrow> (P \<W> Q) = (P' \<W> Q'))
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<And>s. P s = P' s) \<Longrightarrow> (\<lambda>\<sigma>. P (\<sigma> 0)) = (\<lambda>\<sigma>. P' (\<sigma> 0))) &&& ((\<And>\<sigma>. P \<sigma> = P' \<sigma>) \<Longrightarrow> (\<lambda>\<sigma>. \<forall>i. P (\<sigma> |\<^sub>s i)) = (\<lambda>\<sigma>. \<forall>i. P' (\<sigma> |\<^sub>s i))) &&& ((\<And>\<sigma>. P \<sigma> = P' \<sigma>) \<Longrightarrow> (\<lambda>\<sigma>. \<exists>i. P (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True)) = (\<lambda>\<sigma>. \<exists>i. P' (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True)))) &&& ((\<And>\<sigma>. P \<sigma> = P' \<sigma>) \<Longrightarrow> (\<lambda>\<sigma>. P (\<sigma> |\<^sub>s 1)) = (\<lambda>\<sigma>. P' (\<sigma> |\<^sub>s 1))) &&& (\<lbrakk>\<And>\<sigma>. P \<sigma> = P' \<sigma>; \<And>\<sigma>. Q \<sigma> = Q' \<sigma>\<rbrakk> \<Longrightarrow> (\<lambda>\<sigma>. \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) = (\<lambda>\<sigma>. \<exists>i. Q' (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P' (\<sigma> |\<^sub>s k)))) &&& (\<lbrakk>\<And>\<sigma>. P \<sigma> = P' \<sigma>; \<And>\<sigma>. Q \<sigma> = Q' \<sigma>\<rbrakk> \<Longrightarrow> (\<lambda>s. (\<exists>i. Q (s |\<^sub>s i) \<and> (\<forall>k<i. P (s |\<^sub>s k))) \<or> (\<forall>i. P (s |\<^sub>s i))) = (\<lambda>s. (\<exists>i. Q' (s |\<^sub>s i) \<and> (\<forall>k<i. P' (s |\<^sub>s k))) \<or> (\<forall>i. P' (s |\<^sub>s i))))
[PROOF STEP]
by auto


[STATEMENT]
lemma norm[simp]:
  "\<lceil>\<langle>False\<rangle>\<rceil> = \<langle>False\<rangle>"
  "\<lceil>\<langle>True\<rangle>\<rceil> = \<langle>True\<rangle>"
  "(\<^bold>\<not>\<lceil>p\<rceil>) = \<lceil>\<^bold>\<not>p\<rceil>"
  "(\<lceil>p\<rceil> \<^bold>\<and> \<lceil>q\<rceil>) = \<lceil>p \<^bold>\<and> q\<rceil>"
  "(\<lceil>p\<rceil> \<^bold>\<or> \<lceil>q\<rceil>) = \<lceil>p \<^bold>\<or> q\<rceil>"
  "(\<lceil>p\<rceil> \<^bold>\<longrightarrow> \<lceil>q\<rceil>) = \<lceil>p \<^bold>\<longrightarrow> q\<rceil>"
  "(\<lceil>p\<rceil> \<sigma> \<and> \<lceil>q\<rceil> \<sigma>) = \<lceil>p \<^bold>\<and> q\<rceil> \<sigma>"
  "(\<lceil>p\<rceil> \<sigma> \<or> \<lceil>q\<rceil> \<sigma>) = \<lceil>p \<^bold>\<or> q\<rceil> \<sigma>"
  "(\<lceil>p\<rceil> \<sigma> \<longrightarrow> \<lceil>q\<rceil> \<sigma>) = \<lceil>p \<^bold>\<longrightarrow> q\<rceil> \<sigma>"

  "(\<circle>\<langle>False\<rangle>) = \<langle>False\<rangle>"
  "(\<circle>\<langle>True\<rangle>) = \<langle>True\<rangle>"

  "(\<box>\<langle>False\<rangle>) = \<langle>False\<rangle>"
  "(\<box>\<langle>True\<rangle>) = \<langle>True\<rangle>"
  "(\<^bold>\<not>\<box> P) \<sigma> = (\<diamond> (\<^bold>\<not> P)) \<sigma>"
  "(\<box>\<box> P) = (\<box> P)"

  "(\<diamond>\<langle>False\<rangle>) = \<langle>False\<rangle>"
  "(\<diamond>\<langle>True\<rangle>) = \<langle>True\<rangle>"
  "(\<^bold>\<not>\<diamond> P) = (\<box> (\<^bold>\<not> P))"
  "(\<diamond>\<diamond> P) = (\<diamond> P)"

  "(P \<W> \<langle>False\<rangle>) = (\<box> P)"

  "(\<^bold>\<not>(P \<U> Q)) \<sigma> = (\<^bold>\<not>P \<R> \<^bold>\<not>Q) \<sigma>"
  "(\<langle>False\<rangle> \<U> P) = P"
  "(P \<U> \<langle>False\<rangle>) = \<langle>False\<rangle>"
  "(P \<U> \<langle>True\<rangle>) = \<langle>True\<rangle>"
  "(\<langle>True\<rangle> \<U> P) = (\<diamond> P)"
  "(P \<U> (P \<U> Q)) = (P \<U> Q)"

  "(\<^bold>\<not>(P \<R> Q)) \<sigma> = (\<^bold>\<not>P \<U> \<^bold>\<not>Q) \<sigma>"
  "(\<langle>False\<rangle> \<R> P) = (\<box>P)"
  "(P \<R> \<langle>False\<rangle>) = \<langle>False\<rangle>"
  "(\<langle>True\<rangle> \<R> P) = P"
  "(P \<R> \<langle>True\<rangle>) = \<langle>True\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<lceil>\<lambda>s. False\<rceil> = (\<lambda>s. False) &&& \<lceil>\<lambda>s. True\<rceil> = (\<lambda>s. True) &&& (\<lambda>s. \<not> \<lceil>p\<rceil> s) = \<lceil>\<lambda>s. \<not> p s\<rceil>) &&& ((\<lambda>s. \<lceil>p\<rceil> s \<and> \<lceil>q\<rceil> s) = \<lceil>\<lambda>s. p s \<and> q s\<rceil> &&& (\<lambda>s. \<lceil>p\<rceil> s \<or> \<lceil>q\<rceil> s) = \<lceil>\<lambda>s. p s \<or> q s\<rceil>) &&& (\<lambda>s. \<lceil>p\<rceil> s \<longrightarrow> \<lceil>q\<rceil> s) = \<lceil>\<lambda>s. p s \<longrightarrow> q s\<rceil> &&& (\<lceil>p\<rceil> \<sigma> \<and> \<lceil>q\<rceil> \<sigma>) = \<lceil>\<lambda>s. p s \<and> q s\<rceil> \<sigma>) &&& (((\<lceil>p\<rceil> \<sigma> \<or> \<lceil>q\<rceil> \<sigma>) = \<lceil>\<lambda>s. p s \<or> q s\<rceil> \<sigma> &&& (\<lceil>p\<rceil> \<sigma> \<longrightarrow> \<lceil>q\<rceil> \<sigma>) = \<lceil>\<lambda>s. p s \<longrightarrow> q s\<rceil> \<sigma>) &&& \<circle>(\<lambda>s. False) = (\<lambda>s. False) &&& \<circle>(\<lambda>s. True) = (\<lambda>s. True)) &&& (\<box>(\<lambda>s. False) = (\<lambda>s. False) &&& \<box>(\<lambda>s. True) = (\<lambda>s. True)) &&& (\<not> (\<box>P) \<sigma>) = (\<diamond>(\<lambda>s. \<not> P s)) \<sigma> &&& \<box>\<box>P = \<box>P) &&& (((\<diamond>(\<lambda>s. False) = (\<lambda>s. False) &&& \<diamond>(\<lambda>s. True) = (\<lambda>s. True)) &&& (\<lambda>s. \<not> (\<diamond>P) s) = \<box>(\<lambda>s. \<not> P s) &&& \<diamond>\<diamond>P = \<diamond>P) &&& ((P \<W> (\<lambda>s. False)) = \<box>P &&& (\<not> (P \<U> Q) \<sigma>) = ((\<lambda>s. \<not> P s) \<R> (\<lambda>s. \<not> Q s)) \<sigma>) &&& ((\<lambda>s. False) \<U> P) = P &&& (P \<U> (\<lambda>s. False)) = (\<lambda>s. False)) &&& (((P \<U> (\<lambda>s. True)) = (\<lambda>s. True) &&& ((\<lambda>s. True) \<U> P) = \<diamond>P) &&& (P \<U> P \<U> Q) = (P \<U> Q) &&& (\<not> (P \<R> Q) \<sigma>) = ((\<lambda>s. \<not> P s) \<U> (\<lambda>s. \<not> Q s)) \<sigma>) &&& (((\<lambda>s. False) \<R> P) = \<box>P &&& (P \<R> (\<lambda>s. False)) = (\<lambda>s. False)) &&& ((\<lambda>s. True) \<R> P) = P &&& (P \<R> (\<lambda>s. True)) = (\<lambda>s. True)
[PROOF STEP]
(*
  "(P \<U> (P \<U> Q)) \<sigma> = (P \<U> Q) \<sigma>" FIXME for Release
*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<lceil>\<lambda>s. False\<rceil> = (\<lambda>s. False) &&& \<lceil>\<lambda>s. True\<rceil> = (\<lambda>s. True) &&& (\<lambda>s. \<not> \<lceil>p\<rceil> s) = \<lceil>\<lambda>s. \<not> p s\<rceil>) &&& ((\<lambda>s. \<lceil>p\<rceil> s \<and> \<lceil>q\<rceil> s) = \<lceil>\<lambda>s. p s \<and> q s\<rceil> &&& (\<lambda>s. \<lceil>p\<rceil> s \<or> \<lceil>q\<rceil> s) = \<lceil>\<lambda>s. p s \<or> q s\<rceil>) &&& (\<lambda>s. \<lceil>p\<rceil> s \<longrightarrow> \<lceil>q\<rceil> s) = \<lceil>\<lambda>s. p s \<longrightarrow> q s\<rceil> &&& (\<lceil>p\<rceil> \<sigma> \<and> \<lceil>q\<rceil> \<sigma>) = \<lceil>\<lambda>s. p s \<and> q s\<rceil> \<sigma>) &&& (((\<lceil>p\<rceil> \<sigma> \<or> \<lceil>q\<rceil> \<sigma>) = \<lceil>\<lambda>s. p s \<or> q s\<rceil> \<sigma> &&& (\<lceil>p\<rceil> \<sigma> \<longrightarrow> \<lceil>q\<rceil> \<sigma>) = \<lceil>\<lambda>s. p s \<longrightarrow> q s\<rceil> \<sigma>) &&& \<circle>(\<lambda>s. False) = (\<lambda>s. False) &&& \<circle>(\<lambda>s. True) = (\<lambda>s. True)) &&& (\<box>(\<lambda>s. False) = (\<lambda>s. False) &&& \<box>(\<lambda>s. True) = (\<lambda>s. True)) &&& (\<not> (\<box>P) \<sigma>) = (\<diamond>(\<lambda>s. \<not> P s)) \<sigma> &&& \<box>\<box>P = \<box>P) &&& (((\<diamond>(\<lambda>s. False) = (\<lambda>s. False) &&& \<diamond>(\<lambda>s. True) = (\<lambda>s. True)) &&& (\<lambda>s. \<not> (\<diamond>P) s) = \<box>(\<lambda>s. \<not> P s) &&& \<diamond>\<diamond>P = \<diamond>P) &&& ((P \<W> (\<lambda>s. False)) = \<box>P &&& (\<not> (P \<U> Q) \<sigma>) = ((\<lambda>s. \<not> P s) \<R> (\<lambda>s. \<not> Q s)) \<sigma>) &&& ((\<lambda>s. False) \<U> P) = P &&& (P \<U> (\<lambda>s. False)) = (\<lambda>s. False)) &&& (((P \<U> (\<lambda>s. True)) = (\<lambda>s. True) &&& ((\<lambda>s. True) \<U> P) = \<diamond>P) &&& (P \<U> P \<U> Q) = (P \<U> Q) &&& (\<not> (P \<R> Q) \<sigma>) = ((\<lambda>s. \<not> P s) \<U> (\<lambda>s. \<not> Q s)) \<sigma>) &&& (((\<lambda>s. False) \<R> P) = \<box>P &&& (P \<R> (\<lambda>s. False)) = (\<lambda>s. False)) &&& ((\<lambda>s. True) \<R> P) = P &&& (P \<R> (\<lambda>s. True)) = (\<lambda>s. True)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((((\<lambda>\<sigma>. False) = (\<lambda>s. False) &&& (\<lambda>\<sigma>. True) = (\<lambda>s. True) &&& (\<lambda>s. \<not> p (s 0)) = (\<lambda>\<sigma>. \<not> p (\<sigma> 0))) &&& ((\<lambda>s. p (s 0) \<and> q (s 0)) = (\<lambda>\<sigma>. p (\<sigma> 0) \<and> q (\<sigma> 0)) &&& (\<lambda>s. p (s 0) \<or> q (s 0)) = (\<lambda>\<sigma>. p (\<sigma> 0) \<or> q (\<sigma> 0))) &&& (\<lambda>s. p (s 0) \<longrightarrow> q (s 0)) = (\<lambda>\<sigma>. p (\<sigma> 0) \<longrightarrow> q (\<sigma> 0)) &&& (p (\<sigma> 0) \<and> q (\<sigma> 0)) = (p (\<sigma> 0) \<and> q (\<sigma> 0))) &&& (((p (\<sigma> 0) \<or> q (\<sigma> 0)) = (p (\<sigma> 0) \<or> q (\<sigma> 0)) &&& (p (\<sigma> 0) \<longrightarrow> q (\<sigma> 0)) = (p (\<sigma> 0) \<longrightarrow> q (\<sigma> 0))) &&& (\<lambda>\<sigma>. False) = (\<lambda>s. False) &&& (\<lambda>\<sigma>. True) = (\<lambda>s. True)) &&& ((\<lambda>\<sigma>. \<forall>i. False) = (\<lambda>s. False) &&& (\<lambda>\<sigma>. \<forall>i. True) = (\<lambda>s. True)) &&& (\<not> (\<forall>i. P (\<sigma> |\<^sub>s i))) = (\<exists>i. \<not> P (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True)) &&& (\<lambda>\<sigma>. \<forall>i ia. P (\<sigma> |\<^sub>s i |\<^sub>s ia)) = (\<lambda>\<sigma>. \<forall>i. P (\<sigma> |\<^sub>s i))) &&& ((((\<lambda>\<sigma>. \<exists>i. False \<and> (\<forall>k<i. True)) = (\<lambda>s. False) &&& (\<lambda>\<sigma>. \<exists>i. True \<and> (\<forall>k<i. True)) = (\<lambda>s. True)) &&& (\<lambda>s. \<nexists>i. P (s |\<^sub>s i) \<and> (\<forall>k<i. True)) = (\<lambda>\<sigma>. \<forall>i. \<not> P (\<sigma> |\<^sub>s i)) &&& (\<lambda>\<sigma>. \<exists>i. (\<exists>ia. P (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True)) \<and> (\<forall>k<i. True)) = (\<lambda>\<sigma>. \<exists>i. P (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True))) &&& ((\<lambda>s. (\<exists>i. False \<and> (\<forall>k<i. P (s |\<^sub>s k))) \<or> (\<forall>i. P (s |\<^sub>s i))) = (\<lambda>\<sigma>. \<forall>i. P (\<sigma> |\<^sub>s i)) &&& (\<nexists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) = (\<nexists>i. \<not> \<not> Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. \<not> \<not> P (\<sigma> |\<^sub>s k)))) &&& (\<lambda>\<sigma>. \<exists>i. P (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. False)) = P &&& (\<lambda>\<sigma>. \<exists>i. False \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) = (\<lambda>s. False)) &&& (((\<lambda>\<sigma>. \<exists>i. True \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) = (\<lambda>s. True) &&& (\<lambda>\<sigma>. \<exists>i. P (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True)) = (\<lambda>\<sigma>. \<exists>i. P (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True))) &&& (\<lambda>\<sigma>. \<exists>i. (\<exists>ia. Q (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. P (\<sigma> |\<^sub>s i |\<^sub>s k))) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) = (\<lambda>\<sigma>. \<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) &&& (\<not> (\<nexists>i. \<not> Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. \<not> P (\<sigma> |\<^sub>s k)))) = (\<exists>i. \<not> Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. \<not> P (\<sigma> |\<^sub>s k)))) &&& ((\<lambda>s. \<nexists>i. \<not> P (s |\<^sub>s i) \<and> (\<forall>k<i. \<not> False)) = (\<lambda>\<sigma>. \<forall>i. P (\<sigma> |\<^sub>s i)) &&& (\<lambda>s. \<nexists>i. \<not> False \<and> (\<forall>k<i. \<not> P (s |\<^sub>s k))) = (\<lambda>s. False)) &&& (\<lambda>s. \<nexists>i. \<not> P (s |\<^sub>s i) \<and> (\<forall>k<i. \<not> True)) = P &&& (\<lambda>s. \<nexists>i. \<not> True \<and> (\<forall>k<i. \<not> P (s |\<^sub>s k))) = (\<lambda>s. True)
[PROOF STEP]
apply (auto simp: fun_eq_iff)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x i. \<forall>i ia. P (x |\<^sub>s i + ia) \<Longrightarrow> P (x |\<^sub>s i)
 2. \<And>x i. P (x |\<^sub>s i) \<Longrightarrow> \<exists>i ia. P (x |\<^sub>s i + ia)
 3. \<And>x i. \<lbrakk>P (x |\<^sub>s i); \<forall>k. \<not> k < i\<rbrakk> \<Longrightarrow> P x
 4. \<And>x. P x \<Longrightarrow> \<exists>i. P (x |\<^sub>s i) \<and> (\<forall>k. \<not> k < i)
 5. \<And>x i ia. \<lbrakk>\<forall>k<i. P (x |\<^sub>s k); Q (x |\<^sub>s i + ia); \<forall>k<ia. P (x |\<^sub>s i + k)\<rbrakk> \<Longrightarrow> \<exists>i. Q (x |\<^sub>s i) \<and> (\<forall>k<i. P (x |\<^sub>s k))
 6. \<And>x i. \<lbrakk>Q (x |\<^sub>s i); \<forall>k<i. P (x |\<^sub>s k)\<rbrakk> \<Longrightarrow> \<exists>i. (\<exists>ia. Q (x |\<^sub>s i + ia) \<and> (\<forall>k<ia. P (x |\<^sub>s i + k))) \<and> (\<forall>k<i. P (x |\<^sub>s k))
 7. \<And>x. \<forall>i. P (x |\<^sub>s i) \<or> (\<exists>k. k < i) \<Longrightarrow> P x
 8. \<And>x i. \<lbrakk>P x; \<forall>k. \<not> k < i\<rbrakk> \<Longrightarrow> P (x |\<^sub>s i)
[PROOF STEP]
apply (metis suffix_plus suffix_zero)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x i. P (x |\<^sub>s i) \<Longrightarrow> \<exists>i ia. P (x |\<^sub>s i + ia)
 2. \<And>x i. \<lbrakk>P (x |\<^sub>s i); \<forall>k. \<not> k < i\<rbrakk> \<Longrightarrow> P x
 3. \<And>x. P x \<Longrightarrow> \<exists>i. P (x |\<^sub>s i) \<and> (\<forall>k. \<not> k < i)
 4. \<And>x i ia. \<lbrakk>\<forall>k<i. P (x |\<^sub>s k); Q (x |\<^sub>s i + ia); \<forall>k<ia. P (x |\<^sub>s i + k)\<rbrakk> \<Longrightarrow> \<exists>i. Q (x |\<^sub>s i) \<and> (\<forall>k<i. P (x |\<^sub>s k))
 5. \<And>x i. \<lbrakk>Q (x |\<^sub>s i); \<forall>k<i. P (x |\<^sub>s k)\<rbrakk> \<Longrightarrow> \<exists>i. (\<exists>ia. Q (x |\<^sub>s i + ia) \<and> (\<forall>k<ia. P (x |\<^sub>s i + k))) \<and> (\<forall>k<i. P (x |\<^sub>s k))
 6. \<And>x. \<forall>i. P (x |\<^sub>s i) \<or> (\<exists>k. k < i) \<Longrightarrow> P x
 7. \<And>x i. \<lbrakk>P x; \<forall>k. \<not> k < i\<rbrakk> \<Longrightarrow> P (x |\<^sub>s i)
[PROOF STEP]
apply (metis suffix_plus suffix_zero)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x i. \<lbrakk>P (x |\<^sub>s i); \<forall>k. \<not> k < i\<rbrakk> \<Longrightarrow> P x
 2. \<And>x. P x \<Longrightarrow> \<exists>i. P (x |\<^sub>s i) \<and> (\<forall>k. \<not> k < i)
 3. \<And>x i ia. \<lbrakk>\<forall>k<i. P (x |\<^sub>s k); Q (x |\<^sub>s i + ia); \<forall>k<ia. P (x |\<^sub>s i + k)\<rbrakk> \<Longrightarrow> \<exists>i. Q (x |\<^sub>s i) \<and> (\<forall>k<i. P (x |\<^sub>s k))
 4. \<And>x i. \<lbrakk>Q (x |\<^sub>s i); \<forall>k<i. P (x |\<^sub>s k)\<rbrakk> \<Longrightarrow> \<exists>i. (\<exists>ia. Q (x |\<^sub>s i + ia) \<and> (\<forall>k<ia. P (x |\<^sub>s i + k))) \<and> (\<forall>k<i. P (x |\<^sub>s k))
 5. \<And>x. \<forall>i. P (x |\<^sub>s i) \<or> (\<exists>k. k < i) \<Longrightarrow> P x
 6. \<And>x i. \<lbrakk>P x; \<forall>k. \<not> k < i\<rbrakk> \<Longrightarrow> P (x |\<^sub>s i)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. P x \<Longrightarrow> \<exists>i. P (x |\<^sub>s i) \<and> (\<forall>k. \<not> k < i)
 2. \<And>x i ia. \<lbrakk>\<forall>k<i. P (x |\<^sub>s k); Q (x |\<^sub>s i + ia); \<forall>k<ia. P (x |\<^sub>s i + k)\<rbrakk> \<Longrightarrow> \<exists>i. Q (x |\<^sub>s i) \<and> (\<forall>k<i. P (x |\<^sub>s k))
 3. \<And>x i. \<lbrakk>Q (x |\<^sub>s i); \<forall>k<i. P (x |\<^sub>s k)\<rbrakk> \<Longrightarrow> \<exists>i. (\<exists>ia. Q (x |\<^sub>s i + ia) \<and> (\<forall>k<ia. P (x |\<^sub>s i + k))) \<and> (\<forall>k<i. P (x |\<^sub>s k))
 4. \<And>x. \<forall>i. P (x |\<^sub>s i) \<or> (\<exists>k. k < i) \<Longrightarrow> P x
 5. \<And>x i. \<lbrakk>P x; \<forall>k. \<not> k < i\<rbrakk> \<Longrightarrow> P (x |\<^sub>s i)
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x i ia. \<lbrakk>\<forall>k<i. P (x |\<^sub>s k); Q (x |\<^sub>s i + ia); \<forall>k<ia. P (x |\<^sub>s i + k)\<rbrakk> \<Longrightarrow> \<exists>i. Q (x |\<^sub>s i) \<and> (\<forall>k<i. P (x |\<^sub>s k))
 2. \<And>x i. \<lbrakk>Q (x |\<^sub>s i); \<forall>k<i. P (x |\<^sub>s k)\<rbrakk> \<Longrightarrow> \<exists>i. (\<exists>ia. Q (x |\<^sub>s i + ia) \<and> (\<forall>k<ia. P (x |\<^sub>s i + k))) \<and> (\<forall>k<i. P (x |\<^sub>s k))
 3. \<And>x. \<forall>i. P (x |\<^sub>s i) \<or> (\<exists>k. k < i) \<Longrightarrow> P x
 4. \<And>x i. \<lbrakk>P x; \<forall>k. \<not> k < i\<rbrakk> \<Longrightarrow> P (x |\<^sub>s i)
[PROOF STEP]
apply (metis add.commute add_diff_inverse_nat less_diff_conv2 not_le)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x i. \<lbrakk>Q (x |\<^sub>s i); \<forall>k<i. P (x |\<^sub>s k)\<rbrakk> \<Longrightarrow> \<exists>i. (\<exists>ia. Q (x |\<^sub>s i + ia) \<and> (\<forall>k<ia. P (x |\<^sub>s i + k))) \<and> (\<forall>k<i. P (x |\<^sub>s k))
 2. \<And>x. \<forall>i. P (x |\<^sub>s i) \<or> (\<exists>k. k < i) \<Longrightarrow> P x
 3. \<And>x i. \<lbrakk>P x; \<forall>k. \<not> k < i\<rbrakk> \<Longrightarrow> P (x |\<^sub>s i)
[PROOF STEP]
apply (metis add.right_neutral not_less0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>i. P (x |\<^sub>s i) \<or> (\<exists>k. k < i) \<Longrightarrow> P x
 2. \<And>x i. \<lbrakk>P x; \<forall>k. \<not> k < i\<rbrakk> \<Longrightarrow> P (x |\<^sub>s i)
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>P x; \<forall>k. \<not> k < i\<rbrakk> \<Longrightarrow> P (x |\<^sub>s i)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma always_conj_distrib: "(\<box>(P \<^bold>\<and> Q)) = (\<box>P \<^bold>\<and> \<box>Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<box>(\<lambda>s. P s \<and> Q s) = (\<lambda>s. (\<box>P) s \<and> (\<box>Q) s)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<sigma>. \<forall>i. P (\<sigma> |\<^sub>s i) \<and> Q (\<sigma> |\<^sub>s i)) = (\<lambda>s. (\<forall>i. P (s |\<^sub>s i)) \<and> (\<forall>i. Q (s |\<^sub>s i)))
[PROOF STEP]
by auto


[STATEMENT]
lemma eventually_disj_distrib: "(\<diamond>(P \<^bold>\<or> Q)) = (\<diamond>P \<^bold>\<or> \<diamond>Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<diamond>(\<lambda>s. P s \<or> Q s) = (\<lambda>s. (\<diamond>P) s \<or> (\<diamond>Q) s)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<sigma>. \<exists>i. (P (\<sigma> |\<^sub>s i) \<or> Q (\<sigma> |\<^sub>s i)) \<and> (\<forall>k<i. True)) = (\<lambda>s. (\<exists>i. P (s |\<^sub>s i) \<and> (\<forall>k<i. True)) \<or> (\<exists>i. Q (s |\<^sub>s i) \<and> (\<forall>k<i. True)))
[PROOF STEP]
by auto


[STATEMENT]
lemma always_eventually[elim!]:
  assumes "(\<box>P) \<sigma>"
  shows "(\<diamond>P) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<diamond>P) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<box>P) \<sigma>

goal (1 subgoal):
 1. (\<diamond>P) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
\<forall>i. P (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. \<exists>i. P (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True)
[PROOF STEP]
by auto


[STATEMENT]
lemma eventually_imp_conv_disj: "(\<diamond>(P \<^bold>\<longrightarrow> Q)) = (\<diamond>(\<^bold>\<not>P) \<^bold>\<or> \<diamond>Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<diamond>(\<lambda>s. P s \<longrightarrow> Q s) = (\<lambda>s. (\<diamond>(\<lambda>s. \<not> P s)) s \<or> (\<diamond>Q) s)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<sigma>. \<exists>i. (P (\<sigma> |\<^sub>s i) \<longrightarrow> Q (\<sigma> |\<^sub>s i)) \<and> (\<forall>k<i. True)) = (\<lambda>s. (\<exists>i. \<not> P (s |\<^sub>s i) \<and> (\<forall>k<i. True)) \<or> (\<exists>i. Q (s |\<^sub>s i) \<and> (\<forall>k<i. True)))
[PROOF STEP]
by auto


[STATEMENT]
lemma eventually_imp_distrib:
  "(\<diamond>(P \<^bold>\<longrightarrow> Q)) = (\<box>P \<^bold>\<longrightarrow> \<diamond>Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<diamond>(\<lambda>s. P s \<longrightarrow> Q s) = (\<lambda>s. (\<box>P) s \<longrightarrow> (\<diamond>Q) s)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<sigma>. \<exists>i. (P (\<sigma> |\<^sub>s i) \<longrightarrow> Q (\<sigma> |\<^sub>s i)) \<and> (\<forall>k<i. True)) = (\<lambda>s. (\<forall>i. P (s |\<^sub>s i)) \<longrightarrow> (\<exists>i. Q (s |\<^sub>s i) \<and> (\<forall>k<i. True)))
[PROOF STEP]
by auto