Theory Blockchain

(*
  Title:      Blockchain.thy
  Author:     Diego Marmsoler
*)
section "Blockchain Architectures"

theory Blockchain imports Auxiliary DynamicArchitectures.Dynamic_Architecture_Calculus RF_LTL
begin

subsection "Blockchains"
text ‹
  A blockchain itself is modeled as a simple list.
›

type_synonym 'a BC = "'a list"

abbreviation max_cond:: "('a BC) set ⇒ 'a BC ⇒ bool"
  where "max_cond B b ≡ b ∈ B ∧ (∀b'∈B. length b' ≤ length b)"

no_syntax 
  "_MAX1"     :: "pttrns ⇒ 'b ⇒ 'b"           ("(3MAX _./ _)" [0, 10] 10)
  "_MAX"      :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b"  ("(3MAX _:_./ _)" [0, 0, 10] 10)
  "_MAX1"     :: "pttrns ⇒ 'b ⇒ 'b"           ("(3MAX _./ _)" [0, 10] 10)
  "_MAX"      :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b"  ("(3MAX _∈_./ _)" [0, 0, 10] 10)

definition MAX:: "('a BC) set ⇒ 'a BC"
  where "MAX B = (SOME b. max_cond B b)"

lemma max_ex:
  fixes XS::"('a BC) set"
  assumes "XS ≠ {}"
    and "finite XS"
  shows "∃xs∈XS. (∀ys∈XS. length ys ≤ length xs)"
proof (rule Finite_Set.finite_ne_induct)
  show "finite XS" using assms by simp
next
  from assms show "XS ≠ {}" by simp
next
  fix x::"'a BC"
  show "∃xs∈{x}. ∀ys∈{x}. length ys ≤ length xs" by simp
next
  fix zs::"'a BC" and F::"('a BC) set"
  assume "finite F" and "F ≠ {}" and "zs ∉ F" and "∃xs∈F. ∀ys∈F. length ys ≤ length xs"
  then obtain xs where "xs∈F" and "∀ys∈F. length ys ≤ length xs" by auto
  show "∃xs∈insert zs F. ∀ys∈insert zs F. length ys ≤ length xs"
  proof (cases)
    assume "length zs ≥ length xs"
    with ‹∀ys∈F. length ys ≤ length xs› show ?thesis by auto
  next
    assume "¬ length zs ≥ length xs"
    hence "length zs ≤ length xs" by simp
    with ‹xs ∈ F› show ?thesis using ‹∀ys∈F. length ys ≤ length xs› by auto
  qed
qed

lemma max_prop:
  fixes XS::"('a BC) set"
  assumes "XS ≠ {}"
    and "finite XS"
  shows "MAX XS ∈ XS"
    and "∀b'∈XS. length b' ≤ length (MAX XS)"
proof -
  from assms have "∃xs∈XS. ∀ys∈XS. length ys ≤ length xs" using max_ex[of XS] by auto
  with MAX_def[of XS] show "MAX XS ∈ XS" and "∀b'∈XS. length b' ≤ length (MAX XS)"
    using someI_ex[of "λb. b ∈ XS ∧ (∀b'∈XS. length b' ≤ length b)"] by auto
qed

lemma max_less:
  fixes b::"'a BC" and b'::"'a BC" and B::"('a BC) set"
  assumes "b∈B"
    and "finite B"
    and "length b > length b'"
  shows "length (MAX B) > length b'"
proof -
  from assms have "∃xs∈B. ∀ys∈B. length ys ≤ length xs" using max_ex[of B] by auto
  with MAX_def[of B] have "∀b'∈B. length b' ≤ length (MAX B)"
    using someI_ex[of "λb. b ∈ B ∧ (∀b'∈B. length b' ≤ length b)"] by auto
  with ‹b∈B› have "length b ≤ length (MAX B)" by simp
  with ‹length b > length b'› show ?thesis by simp
qed

subsection "Blockchain Architectures"
text ‹
  In the following we describe the locale for blockchain architectures.
›

locale Blockchain = dynamic_component cmp active
  for active :: "'nid ⇒ cnf ⇒ bool" ("∥_∥⇘_⇙" [0,110]60)
    and cmp :: "'nid ⇒ cnf ⇒ 'ND" ("σ⇘_⇙(_)" [0,110]60) +
  fixes pin :: "'ND ⇒ ('nid BC) set"
    and pout :: "'ND ⇒ 'nid BC"
    and bc :: "'ND ⇒ 'nid BC"
    and mining :: "'ND ⇒ bool"
    and honest :: "'nid ⇒ bool"
    and actHn :: "cnf ⇒ 'nid set"
    and actDn :: "cnf ⇒ 'nid set"
    and PoW:: "trace ⇒ nat ⇒ nat"
    and hmining:: "trace ⇒ nat ⇒ bool"
    and dmining:: "trace ⇒ nat ⇒ bool"
    and cb:: nat
  defines "actHn k ≡ {nid. ∥nid∥⇘k⇙ ∧ honest nid}"
    and "actDn k ≡ {nid. ∥nid∥⇘k⇙ ∧ ¬ honest nid}"
    and "PoW t n ≡ (LEAST x. ∀nid∈actHn (t n). length (bc (σ⇘nid⇙(t n))) ≤ x)"
    and "hmining t ≡ (λn. ∃nid∈actHn (t n). mining (σ⇘nid⇙(t n)))"
    and "dmining t ≡ (λn. ∃nid∈actDn (t n). mining (σ⇘nid⇙(t n)))"
  assumes consensus: "⋀nid t t' bc'::('nid BC). ⟦honest nid⟧ ⟹ eval nid t t' 0
    (□⇩b ([λnd. bc' = (if (∃b∈pin nd. length b > length (bc nd)) then (MAX (pin nd)) else (bc nd))]⇩b
      ⟶⇧b ○⇩b [λnd.(¬ mining nd ∧ bc nd = bc' ∨ mining nd ∧ (∃b. bc nd = bc' @ [b]))]⇩b))"
    and attacker: "⋀nid t t' bc'. ⟦¬ honest nid⟧ ⟹ eval nid t t' 0
    (□⇩b ([λnd. bc' = (SOME b. b ∈ (pin nd ∪ {bc nd}))]⇩b ⟶⇧b
      ○⇩b [λnd.(¬ mining nd ∧ prefix (bc nd) bc' ∨ mining nd ∧ (∃b. bc nd = bc' @ [b]))]⇩b))"
    and forward: "⋀nid t t'. eval nid t t' 0 (□⇩b [λnd. pout nd = bc nd]⇩b)"
    ― ‹At each time point a node will forward its blockchain to the network›
    and init: "⋀nid t t'. eval nid t t' 0 [λnd. bc nd=[]]⇩b"
    and conn: "⋀k nid. ⟦∥nid∥⇘k⇙; honest nid⟧
      ⟹ pin (cmp nid k) = (⋃nid'∈actHn k. {pout (cmp nid' k)})"
    and act: "⋀t n::nat. finite {nid::'nid. ∥nid∥⇘t n⇙}"
    and actHn: "⋀t n::nat. ∃nid. honest nid ∧ ∥nid∥⇘t n⇙ ∧ ∥nid∥⇘t (Suc n)⇙"
    and fair: "⋀n n'. ccard n n' (dmining t) > cb ⟹ ccard n n' (hmining t) > cb"
    and closed: "⋀t nid b n::nat. ⟦∥nid∥⇘t n⇙; b ∈ pin (σ⇘nid⇙(t n))⟧ ⟹ ∃nid'. ∥nid'∥⇘t n⇙ ∧ bc (σ⇘nid'⇙(t n)) = b"
    and mine: "⋀t nid n::nat. ⟦honest nid; ∥nid∥⇘t (Suc n)⇙; mining (σ⇘nid⇙(t (Suc n)))⟧ ⟹ ∥nid∥⇘t n⇙"
begin

lemma init_model:
  assumes "¬ (∃n'. latestAct_cond nid t n n')"
    and "∥nid∥⇘t n⇙"
  shows "bc (σ⇘nid⇙t n) = []"
proof -
  from assms(2) have "∃i≥0. ∥nid∥⇘t i⇙" by auto
  with init have "bc (σ⇘nid⇙t ⟨nid → t⟩⇘0⇙) = []" using baEA[of 0 nid t] by blast
  moreover from assms have "n=⟨nid → t⟩⇘0⇙" using nxtAct_eq by simp
  ultimately show ?thesis by simp
qed

lemma fwd_bc:
  fixes nid and t::"nat ⇒ cnf" and t'::"nat ⇒ 'ND"
  assumes "∥nid∥⇘t n⇙"
  shows "pout (σ⇘nid⇙t n) = bc (σ⇘nid⇙t n)"
  using assms forward globEANow[THEN baEANow[of nid t t' n]] by blast

lemma finite_input:
  fixes t n nid
  assumes "∥nid∥⇘t n⇙"
  defines "dep nid' ≡ pout (σ⇘nid'⇙(t n))"
  shows "finite (pin (cmp nid (t n)))"
proof -
  have "finite {nid'. ∥nid'∥⇘t n⇙}" using act by auto
  moreover have "pin (cmp nid (t n)) ⊆ dep ` {nid'. ∥nid'∥⇘t n⇙}"
  proof
    fix x assume "x ∈ pin (cmp nid (t n))"
    show "x ∈ dep ` {nid'. ∥nid'∥⇘t n⇙}"
    proof -
      from assms obtain nid' where "∥nid'∥⇘t n⇙" and "bc (σ⇘nid'⇙(t n)) = x"
        using closed ‹x ∈ pin (cmp nid (t n))› by blast
      hence "pout (σ⇘nid'⇙(t n)) = x" using fwd_bc by auto
      hence "x=dep nid'" using dep_def by simp
      moreover from ‹∥nid'∥⇘t n⇙› have "nid' ∈ {nid'. ∥nid'∥⇘t n⇙}" by simp
      ultimately show ?thesis using image_eqI by simp
    qed
  qed
  ultimately show ?thesis using finite_surj by metis
qed

lemma nempty_input:
  fixes t n nid
  assumes "∥nid∥⇘t n⇙"
    and "honest nid"
  shows "pin (cmp nid (t n))≠{}" using conn[of nid "t n"] act assms actHn_def by auto

lemma onlyone:
  assumes "∃n'≥n. ∥tid∥⇘t n'⇙"
    and "∃n'<n. ∥tid∥⇘t n'⇙"
  shows "∃!i. ⟨tid ← t⟩⇘n⇙ ≤ i ∧ i < ⟨tid → t⟩⇘n⇙ ∧ ∥tid∥⇘t i⇙"
proof
  show "⟨tid ← t⟩⇘n⇙ ≤ ⟨tid ← t⟩⇘n⇙ ∧ ⟨tid ← t⟩⇘n⇙ < ⟨tid → t⟩⇘n⇙ ∧ ∥tid∥⇘t ⟨tid ← t⟩⇘n⇙⇙"
    by (metis assms dynamic_component.nxtActI latestAct_prop(1) latestAct_prop(2) less_le_trans order_refl)
next
  fix i
  show "⟨tid ← t⟩⇘n⇙ ≤ i ∧ i < ⟨tid → t⟩⇘n⇙ ∧ ∥tid∥⇘t i⇙ ⟹ i = ⟨tid ← t⟩⇘n⇙"
    by (metis latestActless(1) leI le_less_Suc_eq le_less_trans nxtActI order_refl)
qed

subsubsection "Component Behavior"

lemma bhv_hn_ex:
  fixes t and t'::"nat ⇒ 'ND" and tid
  assumes "honest tid"
    and "∃n'≥n. ∥tid∥⇘t n'⇙"
    and "∃n'<n. ∥tid∥⇘t n'⇙"
    and "∃b∈pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙). length b > length (bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙))"
  shows "¬ mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ bc (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) =
    Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) ∨ mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧
    (∃b. bc (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) = Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) @ [b])"
proof -
  let ?cond = "λnd. MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) =
    (if (∃b∈pin nd. length b > length (bc nd)) then (MAX (pin nd)) else (bc nd))"
  let ?check = "λnd. ¬ mining nd ∧ bc nd = MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) ∨ mining nd ∧
    (∃b. bc nd = MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) @ [b])"
  from ‹honest tid› have "eval tid t t' 0 (□⇩b([?cond]⇩b ⟶⇧b ○⇩b [?check]⇩b))"
    using consensus[of tid _ _ "MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙))"] by simp
  moreover from assms have "∃i≥0. ∥tid∥⇘t i⇙" by auto
  moreover have "⟨tid ⇐ t⟩⇘0⇙ ≤ ⟨tid ← t⟩⇘n⇙" by simp
  ultimately have "eval tid t t' ⟨tid ← t⟩⇘n⇙ ([?cond]⇩b ⟶⇧b ○⇩b [?check]⇩b)"
    using globEA[of 0 tid t t' "([?cond]⇩b ⟶⇧b ○⇩b [?check]⇩b)" "⟨tid ← t⟩⇘n⇙"] by fastforce
  moreover have "eval tid t t' ⟨tid ← t⟩⇘n⇙ [?cond]⇩b"
  proof (rule baIA)
    from ‹∃n'<n. ∥tid∥⇘t n'⇙› show "∃i≥⟨tid ← t⟩⇘n⇙. ∥tid∥⇘t i⇙" using latestAct_prop(1) by blast
    from assms(3) assms(4) show "?cond (σ⇘tid⇙t ⟨tid → t⟩⇘⟨tid ← t⟩⇘n⇙⇙)" using latestActNxt by simp
  qed
  ultimately have "eval tid t t' ⟨tid ← t⟩⇘n⇙ (○⇩b [?check]⇩b)"
    using impE[of tid t t' _ "[?cond]⇩b" "○⇩b [?check]⇩b"] by simp
  moreover have "∃i>⟨tid → t⟩⇘⟨tid ← t⟩⇘n⇙⇙. ∥tid∥⇘t i⇙"
  proof -
    from assms have "⟨tid → t⟩⇘n⇙>⟨tid ← t⟩⇘n⇙" using latestActNxtAct by simp
    with assms(3) have "⟨tid → t⟩⇘n⇙>⟨tid → t⟩⇘⟨tid ← t⟩⇘n⇙⇙" using latestActNxt by simp
    moreover from ‹∃n'≥n. ∥tid∥⇘t n'⇙› have "∥tid∥⇘t ⟨tid → t⟩⇘n⇙⇙"  using nxtActI by simp
    ultimately show ?thesis by auto
  qed
  moreover from assms have "⟨tid ← t⟩⇘n⇙ ≤ ⟨tid → t⟩⇘n⇙"
    using latestActNxtAct by (simp add: order.strict_implies_order)
  moreover from assms have "∃!i. ⟨tid ← t⟩⇘n⇙ ≤ i ∧ i < ⟨tid → t⟩⇘n⇙ ∧ ∥tid∥⇘t i⇙"
    using onlyone by simp
  ultimately have "eval tid t t' ⟨tid → t⟩⇘n⇙ [?check]⇩b"
    using nxtEA1[of tid t "⟨tid ← t⟩⇘n⇙" t' "[?check]⇩b" "⟨tid → t⟩⇘n⇙"] by simp
  moreover from ‹∃n'≥n. ∥tid∥⇘t n'⇙› have "∥tid∥⇘t ⟨tid → t⟩⇘n⇙⇙" using nxtActI by simp
  ultimately show ?thesis using baEANow[of tid t t' "⟨tid → t⟩⇘n⇙" ?check] by simp
qed

lemma bhv_hn_in:
  fixes t and t'::"nat ⇒ 'ND" and tid
  assumes "honest tid"
    and "∃n'≥n. ∥tid∥⇘t n'⇙"
    and "∃n'<n. ∥tid∥⇘t n'⇙"
    and "¬ (∃b∈pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙). length b > length (bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)))"
  shows "¬ mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ bc (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) = bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙) ∨
    mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ (∃b. bc (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) = bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙) @ [b])"
proof -
  let ?cond = "λnd. bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙) = (if (∃b∈pin nd. length b > length (bc nd)) then (MAX (pin nd)) else (bc nd))"
  let ?check = "λnd. ¬ mining nd ∧ bc nd = bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙) ∨ mining nd ∧ (∃b. bc nd = bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙) @ [b])"
  from ‹honest tid› have "eval tid t t' 0 ((□⇩b([?cond]⇩b ⟶⇧b ○⇩b [?check]⇩b)))"
    using consensus[of tid _ _ "bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)"] by simp
  moreover from assms have "∃i≥0. ∥tid∥⇘t i⇙" by auto
  moreover have "⟨tid ⇐ t⟩⇘0⇙ ≤ ⟨tid ← t⟩⇘n⇙" by simp
  ultimately have "eval tid t t' ⟨tid ← t⟩⇘n⇙ ([?cond]⇩b ⟶⇧b ○⇩b [?check]⇩b)"
    using globEA[of 0 tid t t' "[?cond]⇩b ⟶⇧b ○⇩b [?check]⇩b" "⟨tid ← t⟩⇘n⇙"] by fastforce
  moreover have "eval tid t t' ⟨tid ← t⟩⇘n⇙ [?cond]⇩b"
  proof (rule baIA)
    from ‹∃n'<n. ∥tid∥⇘t n'⇙› show "∃i≥⟨tid ← t⟩⇘n⇙. ∥tid∥⇘t i⇙" using latestAct_prop(1) by blast
    from assms(3) assms(4) show "?cond (σ⇘tid⇙t ⟨tid → t⟩⇘⟨tid ← t⟩⇘n⇙⇙)" using latestActNxt by simp
  qed
  ultimately have "eval tid t t' ⟨tid ← t⟩⇘n⇙ (○⇩b [?check]⇩b)"
    using impE[of tid t t' _ "[?cond]⇩b" "○⇩b [?check]⇩b"] by simp
  moreover have "∃i>⟨tid → t⟩⇘⟨tid ← t⟩⇘n⇙⇙. ∥tid∥⇘t i⇙"
  proof -
    from assms have "⟨tid → t⟩⇘n⇙>⟨tid ← t⟩⇘n⇙" using latestActNxtAct by simp
    with assms(3) have "⟨tid → t⟩⇘n⇙>⟨tid → t⟩⇘⟨tid ← t⟩⇘n⇙⇙" using latestActNxt by simp
    moreover from ‹∃n'≥n. ∥tid∥⇘t n'⇙› have "∥tid∥⇘t ⟨tid → t⟩⇘n⇙⇙"  using nxtActI by simp
    ultimately show ?thesis by auto
  qed
  moreover from assms have "⟨tid ← t⟩⇘n⇙ ≤ ⟨tid → t⟩⇘n⇙"
    using latestActNxtAct by (simp add: order.strict_implies_order)
  moreover from assms have "∃!i. ⟨tid ← t⟩⇘n⇙ ≤ i ∧ i < ⟨tid → t⟩⇘n⇙ ∧ ∥tid∥⇘t i⇙"
    using onlyone by simp
  ultimately have "eval tid t t' ⟨tid → t⟩⇘n⇙ [?check]⇩b"
    using nxtEA1[of tid t "⟨tid ← t⟩⇘n⇙" t' "[?check]⇩b" "⟨tid → t⟩⇘n⇙"] by simp
  moreover from ‹∃n'≥n. ∥tid∥⇘t n'⇙› have "∥tid∥⇘t ⟨tid → t⟩⇘n⇙⇙" using nxtActI by simp
  ultimately show ?thesis using baEANow[of tid t t' "⟨tid → t⟩⇘n⇙" ?check] by simp
qed

lemma bhv_hn_context:
  assumes "honest tid"
      and "∥tid∥⇘t n⇙"
      and "∃n'<n. ∥tid∥⇘t n'⇙"
    shows "∃nid'. ∥nid'∥⇘t ⟨tid ← t⟩⇘n⇙⇙ ∧ (mining (σ⇘tid⇙t n) ∧ (∃b. bc (σ⇘tid⇙t n) = bc (σ⇘nid'⇙t ⟨tid ← t⟩⇘n⇙) @ [b]) ∨
      ¬ mining (σ⇘tid⇙t n) ∧ bc (σ⇘tid⇙t n) = bc (σ⇘nid'⇙t ⟨tid ← t⟩⇘n⇙))"
proof cases
  assume casmp: "∃b∈pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙). length b > length (bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙))"
  moreover from assms(2) have "∃n'≥n. ∥tid∥⇘t n'⇙" by auto
  moreover from assms(3) have "∃n'<n. ∥tid∥⇘t n'⇙" by auto
  ultimately have "¬ mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ bc (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) = Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) ∨
    mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ (∃b. bc (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) = Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) @ [b])"
    using assms(1) bhv_hn_ex by auto
  moreover from assms(2) have "⟨tid → t⟩⇘n⇙ = n" using nxtAct_active by simp
  ultimately have "¬ mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ bc (σ⇘tid⇙t n) = Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) ∨
    mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ (∃b. bc (σ⇘tid⇙t n) = Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) @ [b])" by simp
  moreover from assms(2) have "⟨tid → t⟩⇘n⇙ = n" using nxtAct_active by simp
  ultimately have "¬ mining (σ⇘tid⇙t n) ∧ bc (σ⇘tid⇙t n) = Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) ∨
    mining (σ⇘tid⇙t n) ∧ (∃b. bc (σ⇘tid⇙t n) = Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) @ [b])" by simp
  moreover have "Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)) ∈ pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)"
  proof -
    from ‹∃n'<n. ∥tid∥⇘t n'⇙› have "∥tid∥⇘t ⟨tid ← t⟩⇘n⇙⇙" using latestAct_prop(1) by simp
    hence "finite (pin (σ⇘tid⇙(t ⟨tid ← t⟩⇘n⇙)))" using finite_input[of tid t "⟨tid ← t⟩⇘n⇙"] by simp
    moreover from casmp obtain b where "b ∈ pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)" and "length b > length (bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙))" by auto
    ultimately show ?thesis using max_prop(1) by auto
  qed
  with ‹∃n'<n. ∥tid∥⇘t n'⇙›  obtain nid where "∥nid∥⇘t ⟨tid ← t⟩⇘n⇙⇙"
    and "bc (σ⇘nid⇙t ⟨tid ← t⟩⇘n⇙) = Blockchain.MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙))" using
    closed[of tid t "⟨tid ← t⟩⇘n⇙" "MAX (pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙))"] latestAct_prop(1) by auto
  ultimately show ?thesis by auto
next
  assume "¬ (∃b∈pin (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙). length b > length (bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙)))"
  moreover from assms(2) have "∃n'≥n. ∥tid∥⇘t n'⇙" by auto
  moreover from assms(3) have "∃n'<n. ∥tid∥⇘t n'⇙" by auto
  ultimately have "¬ mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ bc (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) = bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙) ∨
    mining (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) ∧ (∃b. bc (σ⇘tid⇙t ⟨tid → t⟩⇘n⇙) = bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙) @ [b])"
    using assms(1) bhv_hn_in[of tid n t] by auto
  moreover from assms(2) have "⟨tid → t⟩⇘n⇙ = n" using nxtAct_active by simp
  ultimately have "¬ mining (σ⇘tid⇙t n) ∧ bc (σ⇘tid⇙t n) = bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙) ∨
    mining (σ⇘tid⇙t n) ∧ (∃b. bc (σ⇘tid⇙t n) = bc (σ⇘tid⇙t ⟨tid ← t⟩⇘n⇙) @ [b])" by simp
  moreover from ‹∃n'. latestAct_cond tid t n n'› have "∥tid∥⇘t ⟨tid ← t⟩⇘n⇙⇙"
    using latestAct_prop(1) by simp
  ultimately show ?thesis by auto
qed

lemma bhv_dn:
  fixes t and t'::"nat ⇒ 'ND" and uid
  assumes "¬ honest uid"
    and "∃n'≥n. ∥uid∥⇘t n'⇙"
    and "∃n'<n. ∥uid∥⇘t n'⇙"
  shows "¬ mining (σ⇘uid⇙t ⟨uid → t⟩⇘n⇙) ∧ prefix (bc (σ⇘uid⇙t ⟨uid → t⟩⇘n⇙)) (SOME b. b ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∪ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)})
         ∨ mining (σ⇘uid⇙t ⟨uid → t⟩⇘n⇙) ∧ (∃b. bc (σ⇘uid⇙t ⟨uid → t⟩⇘n⇙) = (SOME b. b ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∪ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)}) @ [b])"
proof -
  let ?cond = "λnd. (SOME b. b ∈ (pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∪ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)})) = (SOME b. b ∈ pin nd ∪ {bc nd})"
  let ?check = "λnd. ¬ mining nd ∧ prefix (bc nd) (SOME b. b ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∪ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)})
    ∨ mining nd ∧ (∃b. bc nd = (SOME b. b ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∪ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)}) @ [b])"
  from ‹¬ honest uid› have "eval uid t t' 0 ((□⇩b([?cond]⇩b ⟶⇧b ○⇩b [?check]⇩b)))"
    using attacker[of uid _ _ "(SOME b. b ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∪ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)})"]
    by simp
  moreover from assms have "∃i≥0. ∥uid∥⇘t i⇙" by auto
  moreover have "⟨uid ⇐ t⟩⇘0⇙ ≤ ⟨uid ← t⟩⇘n⇙" by simp
  ultimately have "eval uid t t' ⟨uid ← t⟩⇘n⇙ ([?cond]⇩b ⟶⇧b ○⇩b[?check]⇩b)"
    using globEA[of 0 uid t t' "([?cond]⇩b ⟶⇧b ○⇩b[?check]⇩b)" "⟨uid ← t⟩⇘n⇙"] by fastforce
  moreover have "eval uid t t' ⟨uid ← t⟩⇘n⇙ [?cond]⇩b"
  proof (rule baIA)
    from ‹∃n'<n. ∥uid∥⇘t n'⇙› show "∃i≥⟨uid ← t⟩⇘n⇙. ∥uid∥⇘t i⇙" using latestAct_prop(1) by blast
    with assms(3) show "?cond (σ⇘uid⇙t ⟨uid → t⟩⇘⟨uid ← t⟩⇘n⇙⇙)" using latestActNxt by simp
  qed
  ultimately have "eval uid t t' ⟨uid ← t⟩⇘n⇙ (○⇩b [?check]⇩b)"
    using impE[of uid t t' _ "[?cond]⇩b" "○⇩b [?check]⇩b"] by simp
  moreover have "∃i>⟨uid → t⟩⇘⟨uid ← t⟩⇘n⇙⇙. ∥uid∥⇘t i⇙"
  proof -
    from assms have "⟨uid → t⟩⇘n⇙>⟨uid ← t⟩⇘n⇙" using latestActNxtAct by simp
    with assms(3) have "⟨uid → t⟩⇘n⇙>⟨uid → t⟩⇘⟨uid ← t⟩⇘n⇙⇙" using latestActNxt by simp
    moreover from ‹∃n'≥n. ∥uid∥⇘t n'⇙› have "∥uid∥⇘t ⟨uid → t⟩⇘n⇙⇙"  using nxtActI by simp
    ultimately show ?thesis by auto
  qed
  moreover from assms have "⟨uid ← t⟩⇘n⇙ ≤ ⟨uid → t⟩⇘n⇙"
    using latestActNxtAct by (simp add: order.strict_implies_order)
  moreover from assms have "∃!i. ⟨uid ← t⟩⇘n⇙ ≤ i ∧ i < ⟨uid → t⟩⇘n⇙ ∧ ∥uid∥⇘t i⇙"
    using onlyone by simp
  ultimately have "eval uid t t' ⟨uid → t⟩⇘n⇙ [?check]⇩b"
    using nxtEA1[of uid t "⟨uid ← t⟩⇘n⇙" t' "[?check]⇩b" "⟨uid → t⟩⇘n⇙"] by simp
  moreover from ‹∃n'≥n. ∥uid∥⇘t n'⇙› have "∥uid∥⇘t ⟨uid → t⟩⇘n⇙⇙" using nxtActI by simp
  ultimately show ?thesis using baEANow[of uid t t' "⟨uid → t⟩⇘n⇙" ?check] by simp
qed

lemma bhv_dn_context:
  assumes "¬ honest uid"
      and "∥uid∥⇘t n⇙"
      and "∃n'<n. ∥uid∥⇘t n'⇙"
  shows "∃nid'. ∥nid'∥⇘t ⟨uid ← t⟩⇘n⇙⇙ ∧ (mining (σ⇘uid⇙t n) ∧ (∃b. prefix (bc (σ⇘uid⇙t n)) (bc (σ⇘nid'⇙t ⟨uid ← t⟩⇘n⇙) @ [b]))
  ∨ ¬ mining (σ⇘uid⇙t n) ∧ prefix (bc (σ⇘uid⇙t n)) (bc (σ⇘nid'⇙t ⟨uid ← t⟩⇘n⇙)))"
proof -
  let ?bc="SOME b. b ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∪ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)}"
  have bc_ex: "?bc ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∨ ?bc ∈ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)}"
  proof -
    have "∃b. b∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∪ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)}" by auto
    hence "?bc ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∪ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)}" using someI_ex by simp
    thus ?thesis by auto
  qed

  from assms(2) have "∃n'≥n. ∥uid∥⇘t n'⇙" by auto
  moreover from assms(3) have "∃n'<n. ∥uid∥⇘t n'⇙" by auto
  ultimately have "¬ mining (σ⇘uid⇙t ⟨uid → t⟩⇘n⇙) ∧ prefix (bc (σ⇘uid⇙t ⟨uid → t⟩⇘n⇙)) ?bc ∨
    mining (σ⇘uid⇙t ⟨uid → t⟩⇘n⇙) ∧ (∃b. bc (σ⇘uid⇙t ⟨uid → t⟩⇘n⇙) = ?bc @ [b])"
    using bhv_dn[of uid n t] assms(1) by simp
  moreover from assms(2) have "⟨uid → t⟩⇘n⇙ = n" using nxtAct_active by simp
  ultimately have casmp: "¬ mining (σ⇘uid⇙t n) ∧ prefix (bc (σ⇘uid⇙t n)) ?bc ∨
    mining (σ⇘uid⇙t n) ∧ (∃b. bc (σ⇘uid⇙t n) = ?bc @ [b])" by simp

  from bc_ex have "?bc ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙) ∨ ?bc ∈ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)}" .
  thus ?thesis
  proof
    assume "?bc ∈ pin (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)"
    moreover from ‹∃n'<n. ∥uid∥⇘t n'⇙› have "∥uid∥⇘t ⟨uid ← t⟩⇘n⇙⇙" using latestAct_prop(1) by simp
    ultimately obtain nid where "∥nid∥⇘t ⟨uid ← t⟩⇘n⇙⇙" and "bc (σ⇘nid⇙t ⟨uid ← t⟩⇘n⇙) = ?bc"
      using closed by blast
    with casmp have "¬ mining (σ⇘uid⇙t n) ∧ prefix (bc (σ⇘uid⇙t n)) (bc (σ⇘nid⇙t ⟨uid ← t⟩⇘n⇙)) ∨
      mining (σ⇘uid⇙t n) ∧ (∃b. bc (σ⇘uid⇙t n) = (bc (σ⇘nid⇙t ⟨uid ← t⟩⇘n⇙)) @ [b])" by simp
    with ‹∥nid∥⇘t ⟨uid ← t⟩⇘n⇙⇙› show ?thesis by auto
  next
    assume "?bc ∈ {bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)}"
    hence "?bc = bc (σ⇘uid⇙t ⟨uid ← t⟩⇘n⇙)" by simp
    moreover from ‹∃n'. latestAct_cond uid t n n'› have "∥uid∥⇘t ⟨uid ← t⟩⇘n⇙⇙"
      using latestAct_prop(1) by simp
    ultimately show ?thesis using casmp by auto
  qed
qed

subsubsection "Maximal Honest Blockchains"

abbreviation mbc_cond:: "trace ⇒ nat ⇒ 'nid ⇒ bool"
  where "mbc_cond t n nid ≡ nid∈actHn (t n) ∧ (∀nid'∈actHn (t n). length (bc (σ⇘nid'⇙(t n))) ≤ length (bc (σ⇘nid⇙(t n))))"

lemma mbc_ex:
  fixes t n
  shows "∃x. mbc_cond t n x"
proof -
  let ?ALL="{b. ∃nid∈actHn (t n). b = bc (σ⇘nid⇙(t n))}"
  have "MAX ?ALL ∈ ?ALL"
  proof (rule max_prop)
    from actHn have "actHn (t n) ≠ {}" using actHn_def by blast
    thus "?ALL≠{}" by auto
    from act have "finite (actHn (t n))" using actHn_def by simp
    thus "finite ?ALL" by simp
  qed
  then obtain nid where "nid ∈ actHn (t n) ∧ bc (σ⇘nid⇙(t n)) = MAX ?ALL" by auto
  moreover have "∀nid'∈actHn (t n). length (bc (σ⇘nid'⇙(t n))) ≤ length (MAX ?ALL)"
  proof
    fix nid
    assume "nid ∈ actHn (t n)"
    hence "bc (σ⇘nid⇙(t n)) ∈ ?ALL" by auto
    moreover have "∀b'∈?ALL. length b' ≤ length (MAX ?ALL)"
    proof (rule max_prop)
      from ‹bc (σ⇘nid⇙(t n)) ∈ ?ALL› show "?ALL≠{}" by auto
      from act have "finite (actHn (t n))" using actHn_def by simp
      thus "finite ?ALL" by simp
    qed
    ultimately show "length (bc (σ⇘nid⇙t n)) ≤ length (Blockchain.MAX {b. ∃nid∈actHn (t n). b = bc (σ⇘nid⇙t n)})" by simp
  qed
  ultimately show ?thesis by auto
qed

definition MBC:: "trace ⇒ nat ⇒ 'nid"
  where "MBC t n = (SOME b. mbc_cond t n b)"

lemma mbc_prop[simp]:
  shows "mbc_cond t n (MBC t n)"
  using someI_ex[OF mbc_ex] MBC_def by simp

subsubsection "Honest Proof of Work"
text ‹
  An important construction is the maximal proof of work available in the honest community.
  The construction was already introduces in the locale itself since it was used to express some of the locale assumptions.
›

abbreviation pow_cond:: "trace ⇒ nat ⇒ nat ⇒ bool"
  where "pow_cond t n n' ≡ ∀nid∈actHn (t n). length (bc (σ⇘nid⇙(t n))) ≤ n'"

lemma pow_ex:
  fixes t n
  shows "pow_cond t n (length (bc (σ⇘MBC t n⇙(t n))))"
    and "∀x'. pow_cond t n x' ⟶ x'≥length (bc (σ⇘MBC t n⇙(t n)))"
  using mbc_prop by auto

lemma pow_prop:
  "pow_cond t n (PoW t n)"
proof -
  from pow_ex have "pow_cond t n (LEAST x. pow_cond t n x)" using LeastI_ex[of "pow_cond t n"] by blast
  thus ?thesis using PoW_def by simp
qed 

lemma pow_eq:
  fixes n
  assumes "∃tid∈actHn (t n). length (bc (σ⇘tid⇙(t n))) = x"
    and "∀tid∈actHn (t n). length (bc (σ⇘tid⇙(t n))) ≤ x"
  shows "PoW t n = x"
proof -
  have "(LEAST x. pow_cond t n x) = x"
  proof (rule Least_equality)
    from assms(2) show "∀nid∈actHn (t n). length (bc (σ⇘nid⇙t n)) ≤ x" by simp
  next
    fix y
    assume "∀nid∈actHn (t n). length (bc (σ⇘nid⇙t n)) ≤ y"
    thus "x ≤ y" using assms(1) by auto
  qed
  with PoW_def show ?thesis by simp
qed

lemma pow_mbc:
  shows "length (bc (σ⇘MBC t n⇙t n)) = PoW t n"
  by (metis mbc_prop pow_eq)

lemma pow_less:
  fixes t n nid
  assumes "pow_cond t n x"
  shows "PoW t n ≤ x"
proof -
  from pow_ex assms have "(LEAST x. pow_cond t n x) ≤ x" using Least_le[of "pow_cond t n"] by blast
  thus ?thesis using PoW_def by simp
qed

lemma pow_le_max:
  assumes "honest tid"
    and "∥tid∥⇘t n⇙"
  shows "PoW t n ≤ length (MAX (pin (σ⇘tid⇙t n)))"
proof -
  from mbc_prop have "honest (MBC t n)" and "∥MBC t n∥⇘t n⇙" using actHn_def by auto
  hence "pout (σ⇘MBC t n⇙t n) = bc (σ⇘MBC t n⇙t n)"
    using forward globEANow[THEN baEANow[of "MBC t n" t t' n "λnd. pout nd = bc nd"]] by auto
  with assms ‹∥MBC t n∥⇘t n⇙› ‹honest (MBC t n)› have "bc (σ⇘MBC t n⇙t n) ∈ pin (σ⇘tid⇙t n)"
    using conn actHn_def by auto
  moreover from assms (2) have "finite (pin (σ⇘tid⇙t n))" using finite_input[of tid t n] by simp
  ultimately have "length (bc (σ⇘MBC t n⇙t n)) ≤ length (MAX (pin (σ⇘tid⇙t n)))"
    using max_prop(2) by auto
  with pow_mbc show ?thesis by simp
qed

lemma pow_ge_lgth:
  assumes "honest tid"
    and "∥tid∥⇘t n⇙"
  shows "length (bc (σ⇘tid⇙t n)) ≤ PoW t n"
proof -
  from assms have "tid ∈ actHn (t n)" using actHn_def by simp
  thus ?thesis using pow_prop by simp
qed

lemma pow_le_lgth:
  assumes "honest tid"
    and "∥tid∥⇘t n⇙"
    and "¬(∃b∈pin (σ⇘tid⇙t n). length b > length (bc (σ⇘tid⇙t n)))"
  shows "length (bc (σ⇘tid⇙t n)) ≥ PoW t n"
proof -
  from assms (3) have "∀b∈pin (σ⇘tid⇙t n). length b ≤ length (bc (σ⇘tid⇙t n))" by auto
  moreover from assms nempty_input[of tid t n] finite_input[of tid t n]
  have "MAX (pin (σ⇘tid⇙t n)) ∈ pin (σ⇘tid⇙t n)" using max_prop(1)[of "pin (σ⇘tid⇙t n)"] by simp
  ultimately have "length (MAX (pin (σ⇘tid⇙t n))) ≤ length (bc (σ⇘tid⇙t n))" by simp
  moreover from assms have "PoW t n ≤ length (MAX (pin (σ⇘tid⇙t n)))" using pow_le_max by simp
  ultimately show ?thesis by simp
qed

lemma pow_mono:
  shows "n'≥n ⟹ PoW t n' ≥ PoW t n"
proof (induction n' rule: dec_induct)
  case base
  then show ?case by simp
next
  case (step n')
  hence "PoW t n ≤ PoW t n'" by simp
  moreover have "PoW t (Suc n') ≥ PoW t n'"
  proof -
    from actHn obtain tid where "honest tid" and "∥tid∥⇘t n'⇙" and "∥tid∥⇘t (Suc n')⇙" by auto
    show ?thesis
    proof cases
      assume "∃b∈pin (σ⇘tid⇙t n'). length b > length (bc (σ⇘tid⇙t n'))"
      moreover from ‹∥tid∥⇘t (Suc n')⇙› have "⟨tid → t⟩⇘Suc n'⇙ = Suc n'"
        using nxtAct_active by simp
      moreover from ‹∥tid∥⇘t n'⇙› have "⟨tid ← t⟩⇘Suc n'⇙ = n'"
        using latestAct_prop(2) latestActless le_less_Suc_eq by blast
      moreover from ‹∥tid∥⇘t n'⇙› have "∃n''<Suc n'. ∥tid∥⇘t n''⇙" by blast
      moreover from ‹∥tid∥⇘t (Suc n')⇙› have "∃n''≥Suc n'. ∥tid∥⇘t n''⇙" by auto
      ultimately have "bc (σ⇘tid⇙t (Suc n')) = Blockchain.MAX (pin (σ⇘tid⇙t n')) ∨
        (∃b. bc (σ⇘tid⇙t (Suc n')) = Blockchain.MAX (pin (σ⇘tid⇙t n')) @ b)"
        using ‹honest tid› bhv_hn_ex[of tid "Suc n'" t] by auto
      hence "length (bc (σ⇘tid⇙t (Suc n'))) ≥ length (Blockchain.MAX (pin (σ⇘tid⇙t n')))" by auto
      moreover from ‹honest tid› ‹∥tid∥⇘t n'⇙›
        have "length (Blockchain.MAX (pin (σ⇘tid⇙t n'))) ≥ PoW t n'" using pow_le_max by simp
      ultimately have "PoW t n' ≤ length (bc (σ⇘tid⇙t (Suc n')))" by simp
      moreover from ‹honest tid› ‹∥tid∥⇘t (Suc n')⇙›
        have "length (bc (σ⇘tid⇙t (Suc n'))) ≤ PoW t (Suc n')" using pow_ge_lgth by simp
      ultimately show ?thesis by simp
    next
      assume asmp: "¬(∃b∈pin (σ⇘tid⇙t n'). length b > length (bc (σ⇘tid⇙t n')))"
      moreover from ‹∥tid∥⇘t (Suc n')⇙› have "⟨tid → t⟩⇘Suc n'⇙ = Suc n'"
        using nxtAct_active by simp
      moreover from ‹∥tid∥⇘t n'⇙› have "⟨tid ← t⟩⇘Suc n'⇙ = n'"
        using latestAct_prop(2) latestActless le_less_Suc_eq by blast
      moreover from ‹∥tid∥⇘t n'⇙› have "∃n''<Suc n'. ∥tid∥⇘t n''⇙" by blast
      moreover from ‹∥tid∥⇘t (Suc n')⇙› have "∃n''≥Suc n'. ∥tid∥⇘t n''⇙" by auto
      ultimately have "bc (σ⇘tid⇙t (Suc n')) = bc (σ⇘tid⇙t n') ∨
        (∃b. bc (σ⇘tid⇙t (Suc n')) = bc (σ⇘tid⇙t n') @ b)"
        using ‹honest tid› bhv_hn_in[of tid "Suc n'" t] by auto
      hence "length (bc (σ⇘tid⇙t (Suc n'))) ≥ length (bc (σ⇘tid⇙t n'))" by auto
      moreover from ‹honest tid› ‹∥tid∥⇘t n'⇙› asmp have "length (bc (σ⇘tid⇙t n')) ≥ PoW t n'"
        using pow_le_lgth by simp
      moreover from ‹honest tid› ‹∥tid∥⇘t (Suc n')⇙›
      have "length (bc (σ⇘tid⇙t (Suc n'))) ≤ PoW t (Suc n')" using pow_ge_lgth by simp
      ultimately show ?thesis by simp
    qed
  qed
  ultimately show ?case by auto
qed

lemma pow_equals:
  assumes "PoW t n = PoW t n'"
  and "n'≥n"
  and "n''≥n"
  and "n''≤n'"
shows "PoW t n = PoW t n''" by (metis pow_mono assms(1) assms(3) assms(4) eq_iff)

lemma pow_mining_suc:
    assumes "hmining t (Suc n)"
    shows "PoW t n < PoW t (Suc n)"
proof -
  from assms obtain nid where "nid∈actHn (t (Suc n))" and "mining (σ⇘nid⇙(t (Suc n)))"
    using hmining_def by auto
  show ?thesis
  proof cases
    assume asmp: "(∃b∈pin (σ⇘nid⇙t ⟨nid ← t⟩⇘Suc n⇙). length b > length (bc (σ⇘nid⇙t ⟨nid ← t⟩⇘Suc n⇙)))"
    moreover from ‹nid∈actHn (t (Suc n))› have "honest nid" and "∥nid∥⇘t (Suc n)⇙"
      using actHn_def by auto
    moreover from ‹honest nid› ‹mining (σ⇘nid⇙(t (Suc n)))› ‹∥nid∥⇘t (Suc n)⇙› have "∥nid∥⇘t n⇙"
      using mine by simp
    hence "∃n'. latestAct_cond nid t (Suc n) n'" by auto
    ultimately have "¬ mining (σ⇘nid⇙t ⟨nid → t⟩⇘Suc n⇙) ∧ bc (σ⇘nid⇙t ⟨nid → t⟩⇘Suc n⇙) = MAX (pin (σ⇘nid⇙t ⟨nid ← t⟩⇘Suc n⇙)) ∨
    mining (σ⇘nid⇙t ⟨nid → t⟩⇘Suc n⇙) ∧ (∃b. bc (σ⇘nid⇙t ⟨nid → t⟩⇘Suc n⇙) = MAX (pin (σ⇘nid⇙t ⟨nid ← t⟩⇘Suc n⇙)) @ [b])" using bhv_hn_ex[of nid "Suc n"] by auto
    moreover from ‹∥nid∥⇘t (Suc n)⇙› have "⟨nid → t⟩⇘Suc n⇙ = Suc n" using nxtAct_active by simp
    moreover have "⟨nid ← t⟩⇘Suc n⇙ = n"
    proof (rule latestActEq)
      from ‹∥nid∥⇘t n⇙› show "∥nid∥⇘t n⇙" by simp
      show "¬ (∃n''>n. n'' < Suc n ∧ ∥nid∥⇘t n⇙)" by simp
      show "n < Suc n" by simp
    qed
    hence "⟨nid ← t⟩⇘Suc n⇙ = n" using latestAct_def by simp
    ultimately have "¬ mining (σ⇘nid⇙t (Suc n)) ∧ bc (σ⇘nid⇙t (Suc n)) = MAX (pin (σ⇘nid⇙t n)) ∨
    mining (σ⇘nid⇙t (Suc n)) ∧ (∃b. bc (σ⇘nid⇙t (Suc n)) = MAX (pin (σ⇘nid⇙t n)) @ [b])" by simp
    with ‹mining (σ⇘nid⇙(t (Suc n)))›
      have "∃b. bc (σ⇘nid⇙t (Suc n)) = MAX (pin (σ⇘nid⇙t n)) @ [b]" by auto
    moreover from ‹honest nid› ‹∥nid∥⇘t (Suc n)⇙› have "length (bc (σ⇘nid⇙t (Suc n))) ≤ PoW t (Suc n)"
      using pow_ge_lgth[of nid t "Suc n"] by simp
    ultimately have "length (MAX (pin (σ⇘nid⇙t n))) < PoW t (Suc n)" by auto
    moreover from ‹honest nid› ‹∥nid∥⇘t n⇙› have "length (MAX (pin (σ⇘nid⇙t n))) ≥ PoW t n"
      using pow_le_max by simp
    ultimately show ?thesis by simp
  next
    assume asmp: "¬ (∃b∈pin (σ⇘nid⇙t ⟨nid ← t⟩⇘Suc n⇙). length b > length (bc (σ⇘nid⇙t ⟨nid ← t⟩⇘Suc n⇙)))"
    moreover from ‹nid∈actHn (t (Suc n))› have "honest nid" and "∥nid∥⇘t (Suc n)⇙"
      using actHn_def by auto
    moreover from ‹honest nid› ‹mining (σ⇘nid⇙(t (Suc n)))› ‹∥nid∥⇘t (Suc n)⇙› have "∥nid∥⇘t n⇙"
      using mine by simp
    hence "∃n'. latestAct_cond nid t (Suc n) n'" by auto
    ultimately have "¬ mining (σ⇘nid⇙t ⟨nid → t⟩⇘Suc n⇙) ∧ bc (σ⇘nid⇙t ⟨nid → t⟩⇘Suc n⇙) = bc (σ⇘nid⇙t ⟨nid ← t⟩⇘Suc n⇙) ∨
    mining (σ⇘nid⇙t ⟨nid → t⟩⇘Suc n⇙) ∧ (∃b. bc (σ⇘nid⇙t ⟨nid → t⟩⇘Suc n⇙) = bc (σ⇘nid⇙t ⟨nid ← t⟩⇘Suc n⇙) @ [b])"
      using bhv_hn_in[of nid "Suc n"] by auto
    moreover from ‹∥nid∥⇘t (Suc n)⇙› have "⟨nid → t⟩⇘Suc n⇙ = Suc n" using nxtAct_active by simp
    moreover have "⟨nid ← t⟩⇘Suc n⇙ = n"
    proof (rule latestActEq)
      from ‹∥nid∥⇘t n⇙› show "∥nid∥⇘t n⇙" by simp
      show "¬ (∃n''>n. n'' < Suc n ∧ ∥nid∥⇘t n⇙)" by simp
      show "n < Suc n" by simp
    qed
    hence "⟨nid ← t⟩⇘Suc n⇙ = n" using latestAct_def by simp
    ultimately have "¬ mining (σ⇘nid⇙t (Suc n)) ∧ bc (σ⇘nid⇙t (Suc n)) = bc (σ⇘nid⇙t n) ∨
    mining (σ⇘nid⇙t (Suc n)) ∧ (∃b. bc (σ⇘nid⇙t (Suc n)) = bc (σ⇘nid⇙t n) @ [b])" by simp
    with ‹mining (σ⇘nid⇙(t (Suc n)))› have "∃b. bc (σ⇘nid⇙t (Suc n)) = bc (σ⇘nid⇙t n) @ [b]" by simp
    moreover from ‹⟨nid ← t⟩⇘Suc n⇙ = n›
      have "¬ (∃b∈pin (σ⇘nid⇙t n). length (bc (σ⇘nid⇙t n)) < length b)"
      using asmp by simp
    with ‹honest nid› ‹∥nid∥⇘t n⇙› have "length (bc (σ⇘nid⇙t n)) ≥ PoW t n"
      using pow_le_lgth[of nid t n] by simp
    moreover from ‹honest nid› ‹∥nid∥⇘t (Suc n)⇙› have "length (bc (σ⇘nid⇙t (Suc n))) ≤ PoW t (Suc n)"
      using pow_ge_lgth[of nid t "Suc n"] by simp
    ultimately show ?thesis by auto
  qed
qed

subsubsection "History"
text ‹
  In the following we introduce an operator which extracts the development of a blockchain up to a time point @{term n}.
›

abbreviation "his_prop t n nid n' nid' x ≡
  (∃n. latestAct_cond nid' t n' n) ∧ ∥snd x∥⇘t (fst x)⇙ ∧ fst x = ⟨nid' ← t⟩⇘n'⇙ ∧
  (prefix (bc (σ⇘nid'⇙(t n'))) (bc (σ⇘snd x⇙(t (fst x)))) ∨
    (∃b. bc (σ⇘nid'⇙(t n')) = (bc (σ⇘snd x⇙(t (fst x)))) @ [b] ∧ mining (σ⇘nid'⇙(t n'))))"

inductive_set 
his:: "trace ⇒ nat ⇒ 'nid ⇒ (nat × 'nid) set"
  for t::trace and n::nat and nid::'nid 
  where "⟦∥nid∥⇘t n⇙⟧ ⟹ (n,nid) ∈ his t n nid"
  | "⟦(n',nid') ∈ his t n nid; ∃x. his_prop t n nid n' nid' x⟧ ⟹ (SOME x. his_prop t n nid n' nid' x) ∈ his t n nid"

lemma his_act:
  assumes "(n',nid') ∈ his t n nid"
  shows "∥nid'∥⇘t n'⇙"
  using assms
proof (rule his.cases)
  assume "(n', nid') = (n, nid)" and "∥nid∥⇘t n⇙"
  thus "∥nid'∥⇘t n'⇙" by simp
next
  fix n'' nid'' assume asmp: "(n', nid') = (SOME x. his_prop t n nid n'' nid'' x)"
  and "(n'', nid'') ∈ his t n nid" and "∃x. his_prop t n nid n'' nid'' x"
  hence "his_prop t n nid n'' nid'' (SOME x. his_prop t n nid n'' nid'' x)"
    using someI_ex[of "λx. his_prop t n nid n'' nid'' x"] by auto
  hence "∥snd (SOME x. his_prop t n nid n'' nid'' x)∥⇘t (fst (SOME x. his_prop t n nid n'' nid'' x))⇙"
    by blast
  moreover from asmp have "fst (SOME x. his_prop t n nid n'' nid'' x) = fst (n', nid')" by simp
  moreover from asmp have "snd (SOME x. his_prop t n nid n'' nid'' x) = snd (n', nid')" by simp
  ultimately show ?thesis by simp
qed

text ‹
  In addition we also introduce an operator to obtain the predecessor of a blockchains development.
›

definition "hisPred"
  where "hisPred t n nid n' ≡ (GREATEST n''. ∃nid'. (n'',nid')∈ his t n nid ∧ n'' < n')"

lemma hisPrev_prop:
  assumes "∃n''<n'. ∃nid'. (n'',nid')∈ his t n nid"
  shows "hisPred t n nid n' < n'" and "∃nid'. (hisPred t n nid n',nid')∈ his t n nid"
proof -
  from assms obtain n'' where "∃nid'. (n'',nid')∈ his t n nid ∧ n''<n'" by auto
  moreover from ‹∃nid'. (n'',nid')∈ his t n nid ∧ n''<n'›
    have "∃i'≤n'. (∃nid'. (i', nid') ∈ his t n nid ∧ i' < n') ∧ (∀n'a. (∃nid'. (n'a, nid') ∈ his t n nid ∧ n'a < n') ⟶ n'a ≤ i')"
    using boundedGreatest[of "λn''. ∃nid'. (n'',nid')∈ his t n nid ∧ n'' < n'" n'' n'] by simp
  then obtain i' where "∀n'a. (∃nid'. (n'a, nid') ∈ his t n nid ∧ n'a < n') ⟶ n'a ≤ i'" by auto
  ultimately show "hisPred t n nid n' < n'" and "∃nid'. (hisPred t n nid n',nid')∈ his t n nid"
    using GreatestI_nat[of "λn''. ∃nid'. (n'',nid')∈ his t n nid ∧ n'' < n'" n'' i'] hisPred_def by auto
qed

lemma hisPrev_nex_less:
  assumes "∃n''<n'. ∃nid'. (n'',nid')∈ his t n nid"
  shows "¬(∃x∈his t n nid. fst x < n' ∧ fst x>hisPred t n nid n')"
proof (rule ccontr)
  assume "¬¬(∃x∈his t n nid. fst x < n' ∧ fst x>hisPred t n nid n')"
  then obtain n'' nid'' where "(n'',nid'')∈his t n nid" and "n''< n'" and "n''>hisPred t n nid n'" by auto
  moreover have "n''≤hisPred t n nid n'"
  proof -
    from ‹(n'',nid'')∈his t n nid› ‹n''< n'› have "∃nid'. (n'',nid')∈ his t n nid ∧ n''<n'" by auto
    moreover from ‹∃nid'. (n'',nid')∈ his t n nid ∧ n''<n'› have "∃i'≤n'. (∃nid'. (i', nid') ∈ his t n nid ∧ i' < n') ∧ (∀n'a. (∃nid'. (n'a, nid') ∈ his t n nid ∧ n'a < n') ⟶ n'a ≤ i')"
      using boundedGreatest[of "λn''. ∃nid'. (n'',nid')∈ his t n nid ∧ n'' < n'" n'' n'] by simp
    then obtain i' where "∀n'a. (∃nid'. (n'a, nid') ∈ his t n nid ∧ n'a < n') ⟶ n'a ≤ i'" by auto
    ultimately show ?thesis using Greatest_le_nat[of "λn''. ∃nid'. (n'',nid')∈ his t n nid ∧ n'' < n'" n'' i'] hisPred_def by simp
  qed
  ultimately show False by simp
qed

lemma his_le:
  assumes "x ∈ his t n nid"
  shows "fst x≤n"
using assms
proof (induction rule: his.induct)
  case 1
  then show ?case by simp
next
  case (2 n' nid')
  moreover have "fst (SOME x. his_prop t n nid n' nid' x) ≤ n'"
  proof -
    from "2.hyps" have "∃x. his_prop t n nid n' nid' x" by simp
    hence "his_prop t n nid n' nid' (SOME x. his_prop t n nid n' nid' x)"
      using someI_ex[of "λx. his_prop t n nid n' nid' x"] by auto
    hence "fst (SOME x. his_prop t n nid n' nid' x) = ⟨nid' ← t⟩⇘n'⇙" by force
    moreover from ‹his_prop t n nid n' nid' (SOME x. his_prop t n nid n' nid' x)›
    have "∃n. latestAct_cond nid' t n' n" by simp
    ultimately show ?thesis using latestAct_prop(2)[of n' nid' t] by simp
  qed
  ultimately show ?case by simp
qed

lemma his_determ_base:
  shows "(n, nid') ∈ his t n nid ⟹ nid'=nid"
proof (rule his.cases)
  assume "(n, nid') = (n, nid)"
  thus ?thesis by simp
next
  fix n' nid'a
  assume "(n, nid') ∈ his t n nid" and "(n, nid') = (SOME x. his_prop t n nid n' nid'a x)"
    and "(n', nid'a) ∈ his t n nid" and "∃x. his_prop t n nid n' nid'a x"
  hence "his_prop t n nid n' nid'a (SOME x. his_prop t n nid n' nid'a x)"
    using someI_ex[of "λx. his_prop t n nid n' nid'a x"] by auto
  hence "fst (SOME x. his_prop t n nid n' nid'a x) = ⟨nid'a ← t⟩⇘n'⇙" by force
  moreover from ‹his_prop t n nid n' nid'a (SOME x. his_prop t n nid n' nid'a x)›
    have "∃n. latestAct_cond nid'a t n' n" by simp
  ultimately have "fst (SOME x. his_prop t n nid n' nid'a x) < n'"
    using latestAct_prop(2)[of n' nid'a t] by simp
  with ‹(n, nid') = (SOME x. his_prop t n nid n' nid'a x)› have "fst (n, nid')<n'" by simp
  hence "n<n'" by simp
  moreover from ‹(n', nid'a) ∈ his t n nid› have "n'≤n" using his_le by auto
  ultimately show "nid' = nid" by simp
qed

lemma hisPrev_same:
  assumes "∃n'<n''. ∃nid'. (n',nid')∈ his t n nid"
  and "∃n''<n'. ∃nid'. (n'',nid')∈ his t n nid"
  and "(n',nid')∈ his t n nid"
  and "(n'',nid'')∈ his t n nid"
  and "hisPred t n nid n'=hisPred t n nid n''"
  shows "n'=n''"
proof (rule ccontr)
  assume "¬ n'=n''"
  hence "n'>n'' ∨ n'<n''" by auto
  thus False
  proof
    assume "n'<n''"
    hence "fst (n',nid')<n''" by simp
    moreover from assms(2) have "hisPred t n nid n'<n'" using hisPrev_prop(1) by simp
    with assms have "hisPred t n nid n''<n'" by simp
    hence "hisPred t n nid n''<fst (n',nid')" by simp
    ultimately show False using hisPrev_nex_less[of n'' t n nid] assms by auto
  next (*Symmetric*)
    assume "n'>n''"
    hence "fst (n'',nid')<n'" by simp
    moreover from assms(1) have "hisPred t n nid n''<n''" using hisPrev_prop(1) by simp
    with assms have "hisPred t n nid n'<n''" by simp
    hence "hisPred t n nid n'<fst (n'',nid')" by simp
    ultimately show False using hisPrev_nex_less[of n' t n nid] assms by auto
  qed
qed

lemma his_determ_ext:
  shows "n'≤n ⟹ (∃nid'. (n',nid')∈his t n nid) ⟹ (∃!nid'. (n',nid')∈his t n nid) ∧
    ((∃n''<n'. ∃nid'. (n'',nid')∈ his t n nid) ⟶ (∃x. his_prop t n nid n' (THE nid'. (n',nid')∈his t n nid) x) ∧
    (hisPred t n nid n', (SOME nid'. (hisPred t n nid n', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n' (THE nid'. (n',nid')∈his t n nid) x))"
proof (induction n' rule: my_induct)
  case base
  then obtain nid' where "(n, nid') ∈ his t n nid" by auto
  hence "∃!nid'. (n, nid') ∈ his t n nid"
  proof
    fix nid'' assume "(n, nid'') ∈ his t n nid"
    with his_determ_base have "nid''=nid" by simp
    moreover from ‹(n, nid') ∈ his t n nid› have "nid'=nid" using his_determ_base by simp
    ultimately show "nid'' = nid'" by simp
  qed
  moreover have "(∃n''<n. ∃nid'. (n'',nid')∈ his t n nid) ⟶ (∃x. his_prop t n nid n (THE nid'. (n,nid')∈his t n nid) x) ∧ (hisPred t n nid n, (SOME nid'. (hisPred t n nid n, nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n (THE nid'. (n,nid')∈his t n nid) x)"
  proof
    assume "∃n''<n. ∃nid'. (n'',nid')∈ his t n nid"
    hence "∃nid'. (hisPred t n nid n, nid')∈ his t n nid" using hisPrev_prop(2) by simp
    hence "(hisPred t n nid n, (SOME nid'. (hisPred t n nid n, nid') ∈ his t n nid)) ∈ his t n nid"
      using someI_ex[of "λnid'. (hisPred t n nid n, nid') ∈ his t n nid"] by simp
    thus "(∃x. his_prop t n nid n (THE nid'. (n,nid')∈his t n nid) x) ∧
      (hisPred t n nid n, (SOME nid'. (hisPred t n nid n, nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n (THE nid'. (n,nid')∈his t n nid) x)"
    proof (rule his.cases)
      assume "(hisPred t n nid n, SOME nid'. (hisPred t n nid n, nid') ∈ his t n nid) = (n, nid)"
      hence "hisPred t n nid n=n" by simp
      with ‹∃n''<n. ∃nid'. (n'',nid')∈ his t n nid› show ?thesis using hisPrev_prop(1)[of n t n nid] by force
    next
      fix n'' nid'' assume asmp: "(hisPred t n nid n, SOME nid'. (hisPred t n nid n, nid') ∈ his t n nid) = (SOME x. his_prop t n nid n'' nid'' x)"
      and "(n'', nid'') ∈ his t n nid" and "∃x. his_prop t n nid n'' nid'' x"
      moreover have "n''=n"
      proof (rule antisym)
        show "n''≥n"
        proof (rule ccontr)
          assume "(¬n''≥n)"
          hence "n''<n" by simp
          moreover have "n''>hisPred t n nid n"
          proof -
            let ?x="λx. his_prop t n nid n'' nid'' x"
            from ‹∃x. his_prop t n nid n'' nid'' x› have "his_prop t n nid n'' nid'' (SOME x. ?x x)"
              using someI_ex[of ?x] by auto
            hence "n''>fst (SOME x. ?x x)" using latestAct_prop(2)[of n'' nid'' t] by force
            moreover from asmp have "fst (hisPred t n nid n, SOME nid'. (hisPred t n nid n, nid') ∈ his t n nid) = fst (SOME x. ?x x)" by simp
            ultimately show ?thesis by simp
          qed
          moreover from ‹∃n''<n. ∃nid'. (n'',nid')∈ his t n nid›
            have "¬(∃x∈his t n nid. fst x < n ∧ fst x > hisPred t n nid n)"
            using hisPrev_nex_less by simp
          ultimately show False using ‹(n'', nid'') ∈ his t n nid› by auto
        qed
      next
        from ‹(n'', nid'') ∈ his t n nid› show "n'' ≤ n" using his_le by auto
      qed
      ultimately have "(hisPred t n nid n, SOME nid'. (hisPred t n nid n, nid') ∈ his t n nid) = (SOME x. his_prop t n nid n nid'' x)" by simp
      moreover from ‹n''=n› ‹(n'', nid'') ∈ his t n nid› have "(n, nid'') ∈ his t n nid" by simp
      with ‹∃!nid'. (n,nid') ∈ his t n nid› have "nid''=(THE nid'. (n,nid')∈his t n nid)"
        using the1_equality[of "λnid'. (n, nid') ∈ his t n nid"] by simp
      moreover from ‹∃x. his_prop t n nid n'' nid'' x› ‹n''=n› ‹nid''=(THE nid'. (n,nid')∈his t n nid)›
        have "∃x. his_prop t n nid n (THE nid'. (n,nid')∈his t n nid) x" by simp
      ultimately show ?thesis by simp
    qed
  qed
  ultimately show ?case by simp
next
  case (step n')
  then obtain nid' where "(n', nid') ∈ his t n nid" by auto
  hence "∃!nid'. (n', nid') ∈ his t n nid"
  proof (rule his.cases)
    assume "(n', nid') = (n, nid)"
    hence "n'=n" by simp
    with step.hyps show ?thesis by simp
  next
    fix n'''' nid''''
    assume "(n'''', nid'''') ∈ his t n nid"
      and n'nid': "(n', nid') = (SOME x. his_prop t n nid n'''' nid'''' x)"
      and "(n'''', nid'''') ∈ his t n nid" and "∃x. his_prop t n nid n'''' nid'''' x"
    from ‹(n', nid') ∈ his t n nid› show ?thesis
    proof
      fix nid'' assume "(n', nid'') ∈ his t n nid"
      thus "nid'' = nid'"
      proof (rule his.cases)
        assume "(n', nid'') = (n, nid)"
        hence "n'=n" by simp
        with step.hyps show ?thesis by simp
      next
        fix n''' nid'''
        assume "(n''', nid''') ∈ his t n nid"
          and n'nid'': "(n', nid'') = (SOME x. his_prop t n nid n''' nid''' x)"
          and "(n''', nid''') ∈ his t n nid" and "∃x. his_prop t n nid n''' nid''' x"
        moreover have "n'''=n''''"
        proof -
          have "hisPred t n nid n''' = n'"
          proof -
            from n'nid'' ‹∃x. his_prop t n nid n''' nid''' x›
              have "his_prop t n nid n''' nid''' (n',nid'')"
              using someI_ex[of "λx. his_prop t n nid n''' nid''' x"] by auto
            hence "n'''>n'" using latestAct_prop(2) by simp
            moreover from ‹(n''', nid''') ∈ his t n nid› have "n'''≤ n" using his_le by auto
            moreover from ‹(n''', nid''') ∈ his t n nid›
              have "∃nid'. (n''', nid') ∈ his t n nid" by auto
            ultimately have "(∃n'<n'''. ∃nid'. (n',nid')∈ his t n nid) ⟶ (∃!nid'. (n''',nid') ∈ his t n nid) ∧ (hisPred t n nid n''', (SOME nid'. (hisPred t n nid n''', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n''' (THE nid'. (n''',nid')∈his t n nid) x)" using step.IH by auto
            with ‹n'''>n'› ‹(n', nid') ∈ his t n nid› have "∃!nid'. (n''',nid') ∈ his t n nid" and "(hisPred t n nid n''', (SOME nid'. (hisPred t n nid n''', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n''' (THE nid'. (n''',nid')∈his t n nid) x)" by auto
            moreover from ‹∃!nid'. (n''',nid') ∈ his t n nid› ‹(n''', nid''') ∈ his t n nid› have "nid'''=(THE nid'. (n''',nid')∈his t n nid)" using the1_equality[of "λnid'. (n''', nid') ∈ his t n nid"] by simp
            ultimately have "(hisPred t n nid n''', (SOME nid'. (hisPred t n nid n''', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n''' nid''' x)" by simp
            with n'nid'' have "(n', nid'') = (hisPred t n nid n''', (SOME nid'. (hisPred t n nid n''', nid') ∈ his t n nid))" by simp
            thus ?thesis by simp
          qed
          moreover have "hisPred t n nid n'''' = n'" (*Symmetric*)
          proof -
            from n'nid' ‹∃x. his_prop t n nid n'''' nid'''' x› have "his_prop t n nid n'''' nid'''' (n',nid')"
              using someI_ex[of "λx. his_prop t n nid n'''' nid'''' x"] by auto
            hence "n''''>n'" using latestAct_prop(2) by simp
            moreover from ‹(n'''', nid'''') ∈ his t n nid› have "n''''≤ n" using his_le by auto
            moreover from ‹(n'''', nid'''') ∈ his t n nid›
              have "∃nid'. (n'''', nid') ∈ his t n nid" by auto
            ultimately have "(∃n'<n''''. ∃nid'. (n',nid')∈ his t n nid) ⟶ (∃!nid'. (n'''',nid') ∈ his t n nid) ∧ (hisPred t n nid n'''', (SOME nid'. (hisPred t n nid n'''', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n'''' (THE nid'. (n'''',nid')∈his t n nid) x)" using step.IH by auto
            with ‹n''''>n'› ‹(n', nid') ∈ his t n nid› have "∃!nid'. (n'''',nid') ∈ his t n nid" and "(hisPred t n nid n'''', (SOME nid'. (hisPred t n nid n'''', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n'''' (THE nid'. (n'''',nid')∈his t n nid) x)" by auto
            moreover from ‹∃!nid'. (n'''',nid') ∈ his t n nid› ‹(n'''', nid'''') ∈ his t n nid› have "nid''''=(THE nid'. (n'''',nid')∈his t n nid)" using the1_equality[of "λnid'. (n'''', nid') ∈ his t n nid"] by simp
            ultimately have "(hisPred t n nid n'''', (SOME nid'. (hisPred t n nid n'''', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n'''' nid'''' x)" by simp
            with n'nid' have "(n', nid') = (hisPred t n nid n'''', (SOME nid'. (hisPred t n nid n'''', nid') ∈ his t n nid))" by simp
            thus ?thesis by simp
          qed
          ultimately have "hisPred t n nid n'''=hisPred t n nid n''''" ..
          moreover have "∃n'<n'''. ∃nid'. (n',nid')∈ his t n nid"
          proof -
            from n'nid'' ‹∃x. his_prop t n nid n''' nid''' x› have "his_prop t n nid n''' nid''' (n',nid'')"
              using someI_ex[of "λx. his_prop t n nid n''' nid''' x"] by auto
            hence "n'''>n'" using latestAct_prop(2) by simp
            with ‹(n', nid') ∈ his t n nid› show ?thesis by auto
          qed
          moreover have "∃n'<n''''. ∃nid'. (n',nid')∈ his t n nid"
          proof -
            from n'nid' ‹∃x. his_prop t n nid n'''' nid'''' x› have "his_prop t n nid n'''' nid'''' (n',nid')"
              using someI_ex[of "λx. his_prop t n nid n'''' nid'''' x"] by auto
            hence "n''''>n'" using latestAct_prop(2) by simp
            with ‹(n', nid') ∈ his t n nid› show ?thesis by auto
          qed
          ultimately show ?thesis
            using hisPrev_same ‹(n''', nid''') ∈ his t n nid› ‹(n'''', nid'''') ∈ his t n nid›
            by blast
        qed
        moreover have "nid'''=nid''''"
        proof -
          from n'nid'' ‹∃x. his_prop t n nid n''' nid''' x›
            have "his_prop t n nid n''' nid''' (n',nid'')"
            using someI_ex[of "λx. his_prop t n nid n''' nid''' x"] by auto
          hence "n'''>n'" using latestAct_prop(2) by simp
          moreover from ‹(n''', nid''') ∈ his t n nid› have "n'''≤ n" using his_le by auto
          moreover from ‹(n''', nid''') ∈ his t n nid›
            have "∃nid'. (n''', nid') ∈ his t n nid" by auto
          ultimately have "∃!nid'. (n''', nid') ∈ his t n nid" using step.IH by auto
          with ‹(n''', nid''') ∈ his t n nid› ‹(n'''', nid'''') ∈ his t n nid› ‹n'''=n''''›
            show ?thesis by auto
        qed
        ultimately have "(n', nid') = (n', nid'')" using n'nid' by simp
        thus "nid'' = nid'" by simp
      qed
    qed
  qed
  moreover have "(∃n''<n'. ∃nid'. (n'',nid')∈ his t n nid) ⟶ (∃x. his_prop t n nid n' (THE nid'. (n',nid')∈his t n nid) x) ∧ (hisPred t n nid n', (SOME nid'. (hisPred t n nid n', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n' (THE nid'. (n',nid')∈his t n nid) x)"
  proof
    assume "∃n''<n'. ∃nid'. (n'',nid')∈ his t n nid"
    hence "∃nid'. (hisPred t n nid n', nid')∈ his t n nid" using hisPrev_prop(2) by simp
    hence "(hisPred t n nid n', (SOME nid'. (hisPred t n nid n', nid') ∈ his t n nid)) ∈ his t n nid"
      using someI_ex[of "λnid'. (hisPred t n nid n', nid') ∈ his t n nid"] by simp
    thus "(∃x. his_prop t n nid n' (THE nid'. (n',nid')∈his t n nid) x) ∧ (hisPred t n nid n', (SOME nid'. (hisPred t n nid n', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n' (THE nid'. (n',nid')∈his t n nid) x)"
    proof (rule his.cases)
      assume "(hisPred t n nid n', SOME nid'. (hisPred t n nid n', nid') ∈ his t n nid) = (n, nid)"
      hence "hisPred t n nid n'=n" by simp
      moreover from ‹∃n''<n'. ∃nid'. (n'',nid')∈ his t n nid› have "hisPred t n nid n'<n'"
        using hisPrev_prop(1)[of n'] by force
      ultimately show ?thesis using step.hyps by simp
    next
      fix n'' nid'' assume asmp: "(hisPred t n nid n', SOME nid'. (hisPred t n nid n', nid') ∈ his t n nid) = (SOME x. his_prop t n nid n'' nid'' x)"
      and "(n'', nid'') ∈ his t n nid" and "∃x. his_prop t n nid n'' nid'' x"
      moreover have "n''=n'"
      proof (rule antisym)
        show "n''≥n'"
        proof (rule ccontr)
          assume "(¬n''≥n')"
          hence "n''<n'" by simp
          moreover have "n''>hisPred t n nid n'"
          proof -
            let ?x="λx. his_prop t n nid n'' nid'' x"
            from ‹∃x. his_prop t n nid n'' nid'' x› have "his_prop t n nid n'' nid'' (SOME x. ?x x)"
              using someI_ex[of ?x] by auto
            hence "n''>fst (SOME x. ?x x)" using latestAct_prop(2)[of n'' nid'' t] by force
            moreover from asmp have "fst (hisPred t n nid n', SOME nid'. (hisPred t n nid n', nid') ∈ his t n nid) = fst (SOME x. ?x x)" by simp
            ultimately show ?thesis by simp
          qed
          moreover from ‹∃n''<n'. ∃nid'. (n'',nid')∈ his t n nid›
            have "¬(∃x∈his t n nid. fst x < n' ∧ fst x > hisPred t n nid n')"
            using hisPrev_nex_less by simp
          ultimately show False using ‹(n'', nid'') ∈ his t n nid› by auto
        qed
      next
        show "n'≥n''"
        proof (rule ccontr)
          assume "(¬n'≥n'')"
          hence "n'<n''" by simp
          moreover from ‹(n'', nid'') ∈ his t n nid› have "n''≤ n" using his_le by auto
          moreover from ‹(n'', nid'') ∈ his t n nid› have "∃nid'. (n'', nid') ∈ his t n nid" by auto
          ultimately have "(∃n'<n''. ∃nid'. (n',nid')∈ his t n nid) ⟶ (∃!nid'. (n'',nid') ∈ his t n nid) ∧ (hisPred t n nid n'', (SOME nid'. (hisPred t n nid n'', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n'' (THE nid'. (n'',nid')∈his t n nid) x)" using step.IH by auto
          with ‹n'<n''› ‹(n', nid') ∈ his t n nid› have "∃!nid'. (n'',nid') ∈ his t n nid" and "(hisPred t n nid n'', (SOME nid'. (hisPred t n nid n'', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n'' (THE nid'. (n'',nid')∈his t n nid) x)" by auto
          moreover from ‹∃!nid'. (n'',nid') ∈ his t n nid› ‹(n'', nid'') ∈ his t n nid›
            have "nid'' = (THE nid'. (n'',nid')∈his t n nid)"
            using the1_equality[of "λnid'. (n'', nid') ∈ his t n nid"] by simp
          ultimately have "(hisPred t n nid n'', (SOME nid'. (hisPred t n nid n'', nid') ∈ his t n nid)) = (SOME x. his_prop t n nid n'' nid'' x)" by simp
          with asmp have "(hisPred t n nid n', SOME nid'. (hisPred t n nid n', nid') ∈ his t n nid)=(hisPred t n nid n'', SOME nid'. (hisPred t n nid n'', nid') ∈ his t n nid)" by simp
          hence "hisPred t n nid n' = hisPred t n nid n''" by simp
          with ‹∃n''<n'. ∃nid'. (n'', nid') ∈ his t n nid› ‹n'<n''› ‹(n', nid') ∈ his t n nid› ‹(n'', nid'') ∈ his t n nid› ‹(n', nid') ∈ his t n nid› have "n'=n''" using hisPrev_same by blast
          with ‹n'<n''› show False by simp
        qed
      qed
      ultimately have "(hisPred t n nid n', SOME nid'. (hisPred t n nid n', nid') ∈ his t n nid) = (SOME x. his_prop t n nid n' nid'' x)" by simp
      moreover from ‹(n'', nid'') ∈ his t n nid› ‹n''=n'› have "(n', nid'') ∈ his t n nid" by simp
      with ‹∃!nid'. (n',nid') ∈ his t n nid› have "nid''=(THE nid'. (n',nid')∈his t n nid)"
        using the1_equality[of "λnid'. (n', nid') ∈ his t n nid"] by simp
      moreover from ‹∃x. his_prop t n nid n'' nid'' x› ‹n''=n'› ‹nid''=(THE nid'. (n',nid')∈his t n nid)›
        have "∃x. his_prop t n nid n' (THE nid'. (n',nid')∈his t n nid) x" by simp
      ultimately show ?thesis by simp
    qed
  qed
  ultimately show ?case by simp
qed

corollary his_determ_ex:
  assumes "(n',nid')∈his t n nid"
  shows "∃!nid'. (n',nid')∈his t n nid"
  using assms his_le his_determ_ext[of n' n t nid] by force

corollary his_determ:
  assumes "(n',nid')∈his t n nid"
    and "(n',nid'')∈his t n nid"
  shows "nid'=nid''" using assms his_le his_determ_ext[of n' n t nid] by force

corollary his_determ_the:
  assumes "(n',nid')∈his t n nid"
  shows "(THE nid'. (n', nid')∈his t n nid) = nid'"
  using assms his_determ theI'[of "λnid'. (n', nid')∈his t n nid"] his_determ_ex by simp

subsubsection "Blockchain Development"

definition devBC::"trace ⇒ nat ⇒ 'nid ⇒ nat ⇒ 'nid option"
  where "devBC t n nid n' ≡
    (if (∃nid'. (n', nid')∈ his t n nid) then (Some (THE nid'. (n', nid')∈his t n nid))
    else Option.None)"

lemma devBC_some[simp]: assumes "∥nid∥⇘t n⇙" shows "devBC t n nid n = Some nid"
proof -
  from assms have "(n, nid)∈ his t n nid" using his.intros(1) by simp
  hence "devBC t n nid n = (Some (THE nid'. (n, nid')∈his t n nid))" using devBC_def by auto
  moreover have "(THE nid'. (n, nid')∈his t n nid) = nid"
  proof
    from ‹(n, nid)∈ his t n nid› show "(n, nid)∈ his t n nid" .
  next
    fix nid' assume "(n, nid') ∈ his t n nid"
    thus "nid' = nid" using his_determ_base by simp
  qed
  ultimately show ?thesis by simp
qed

lemma devBC_act: assumes "¬ Option.is_none (devBC t n nid n')" shows "∥the (devBC t n nid n')∥⇘t n'⇙"
proof -
  from assms have "¬ devBC t n nid n'=Option.None" by (metis is_none_simps(1))
  then obtain nid' where "(n', nid')∈ his t n nid" and "devBC t n nid n' = (Some (THE nid'. (n', nid')∈his t n nid))"
    using devBC_def[of t n nid] by metis
  hence "nid'= (THE nid'. (n', nid')∈his t n nid)" using his_determ_the by simp
  with ‹devBC t n nid n' = (Some (THE nid'. (n', nid')∈his t n nid))› have "the (devBC t n nid n') = nid'" by simp
  with ‹(n', nid')∈ his t n nid› show ?thesis using his_act by simp
qed

lemma his_ex:
  assumes "¬Option.is_none (devBC t n nid n')"
  shows "∃nid'. (n',nid')∈his t n nid"
proof (rule ccontr)
  assume "¬(∃nid'. (n',nid')∈his t n nid)"
  with devBC_def have "Option.is_none (devBC t n nid n')" by simp
  with assms show False by simp
qed

lemma devExt_nopt_leq:
  assumes "¬Option.is_none (devBC t n nid n')"
  shows "n'≤n"
proof -
  from assms have "∃nid'. (n',nid')∈his t n nid" using his_ex by simp
  then obtain nid' where "(n',nid')∈his t n nid" by auto
  with his_le[of "(n',nid')"] show ?thesis by simp
qed

text ‹
  An extended version of the development in which deactivations are filled with the last value.
›

function devExt::"trace ⇒ nat ⇒ 'nid ⇒ nat ⇒ nat ⇒ 'nid BC"
  where "⟦∃n'<n⇩s. ¬Option.is_none (devBC t n nid n'); Option.is_none (devBC t n nid n⇩s)⟧ ⟹ devExt t n nid n⇩s 0 = bc (σ⇘the (devBC t n nid (GREATEST n'. n'<n⇩s ∧ ¬Option.is_none (devBC t n nid n')))⇙(t (GREATEST n'. n'<n⇩s ∧ ¬Option.is_none (devBC t n nid n'))))"
  | "⟦¬ (∃n'<n⇩s. ¬Option.is_none (devBC t n nid n')); Option.is_none (devBC t n nid n⇩s)⟧ ⟹ devExt t n nid n⇩s 0 = []"
  | "¬ Option.is_none (devBC t n nid n⇩s) ⟹ devExt t n nid n⇩s 0 = bc (σ⇘the (devBC t n nid n⇩s)⇙(t n⇩s))"
  | "¬ Option.is_none (devBC t n nid (n⇩s + Suc n')) ⟹ devExt t n nid n⇩s (Suc n') = bc (σ⇘the (devBC t n nid (n⇩s + Suc n'))⇙(t (n⇩s + Suc n')))"
  | "Option.is_none (devBC t n nid (n⇩s + Suc n')) ⟹ devExt t n nid n⇩s (Suc n') = devExt t n nid n⇩s n'"
proof -
  show "⋀n⇩s t n nid n⇩s' ta na nida.
       ∃n'<n⇩s. ¬ Option.is_none (devBC t n nid n') ⟹
       Option.is_none (devBC t n nid n⇩s) ⟹
       ∃n'<n⇩s'. ¬ Option.is_none (devBC ta na nida n') ⟹
       Option.is_none (devBC ta na nida n⇩s') ⟹
       (t, n, nid, n⇩s, 0) = (ta, na, nida, n⇩s', 0) ⟹
       bc (σ⇘the (devBC t n nid (GREATEST n'. n' < n⇩s ∧ ¬ Option.is_none (devBC t n nid n')))⇙t (GREATEST n'. n' < n⇩s ∧ ¬ Option.is_none (devBC t n nid n'))) =
       bc (σ⇘the (devBC ta na nida
                    (GREATEST n'. n' < n⇩s' ∧ ¬ Option.is_none (devBC ta na nida n')))⇙ta (GREATEST n'. n' < n⇩s' ∧ ¬ Option.is_none (devBC ta na nida n')))" by auto
  show "⋀n⇩s t n nid n⇩s' ta na nida.
       ∃n'<n⇩s. ¬ Option.is_none (devBC t n nid n') ⟹
       Option.is_none (devBC t n nid n⇩s) ⟹
       ¬ (∃n'<n⇩s'. ¬ Option.is_none (devBC ta na nida n')) ⟹
       Option.is_none (devBC ta na nida n⇩s') ⟹
       (t, n, nid, n⇩s, 0) = (ta, na, nida, n⇩s', 0) ⟹
       bc (σ⇘the (devBC t n nid (GREATEST n'. n' < n⇩s ∧ ¬ Option.is_none (devBC t n nid n')))⇙t (GREATEST n'. n' < n⇩s ∧ ¬ Option.is_none (devBC t n nid n'))) = []" by auto
  show "⋀n⇩s t n nid ta na nida n⇩s'.
       ∃n'<n⇩s. ¬ Option.is_none (devBC t n nid n') ⟹
       Option.is_none (devBC t n nid n⇩s) ⟹
       ¬ Option.is_none (devBC ta na nida n⇩s') ⟹
       (t, n, nid, n⇩s, 0) = (ta, na, nida, n⇩s', 0) ⟹
       bc (σ⇘the (devBC t n nid (GREATEST n'. n' < n⇩s ∧ ¬ Option.is_none (devBC t n nid n')))⇙t (GREATEST n'. n' < n⇩s ∧ ¬ Option.is_none (devBC t n nid n'))) =
       bc (σ⇘the (devBC ta na nida n⇩s')⇙ta n⇩s')" by auto
  show "⋀n⇩s t n nid ta na nida n⇩s' n'.
       ∃n'<n⇩s. ¬ Option.is_none (devBC t n nid n') ⟹
       Option.is_none (devBC t n nid n⇩s) ⟹
       ¬ Option.is_none (devBC ta na nida (n⇩s' + Suc n')) ⟹
       (t, n, nid, n⇩s, 0) = (ta, na, nida, n⇩s', Suc n') ⟹
       bc (σ⇘the (devBC t n nid (GREATEST n'. n' < n⇩s ∧ ¬ Option.is_none (devBC t n nid n')))⇙t (GREATEST n'. n' < n⇩s ∧ ¬ Option.is_none (devBC t n nid n'))) =
       bc (σ⇘the (devBC ta na nida (n⇩s' + Suc n'))⇙ta (n⇩s' + Suc n'))" by auto
  show "⋀n⇩s t n nid ta na nida n⇩s' n'.
       ∃n'<n⇩s. ¬ Option.is_none (devBC t n nid n') ⟹
       Option.is_none (devBC t n nid n⇩s) ⟹
       Option.is_none (devBC ta na nida (n⇩s' + Suc n')) ⟹
       (t, n, nid, n⇩s, 0) = (ta, na, nida, n⇩s', Suc n') ⟹
       bc (σ⇘the (devBC t n nid (GREATEST n'. n' < n⇩s ∧ ¬ Option.is_none (devBC t n nid n')))⇙t (GREATEST n'. n' < n⇩s ∧ ¬ Option.is_none (devBC t n nid n'))) =
       devExt_sumC (ta, na, nida, n⇩s', n')" by auto
  show"⋀n⇩s t n nid n⇩s' ta na nida.
       ¬ (∃n'<n⇩s. ¬ Option.is_none (devBC t n nid n')) ⟹
       Option.is_none (devBC t n nid n⇩s) ⟹
       ¬ (∃n'<n⇩s'. ¬ Option.is_none (devBC ta na nida n')) ⟹
       Option.is_none (devBC ta na nida n⇩s') ⟹ (t, n, nid, n⇩s, 0) = (ta, na, nida, n⇩s', 0) ⟹ [] = []" by auto
  show "⋀n⇩s t n nid ta na nida n⇩s'.
       ¬ (∃n'<n⇩s. ¬ Option.is_none (devBC t n nid n')) ⟹
       Option.is_none (devBC t n nid n⇩s) ⟹
       ¬ Option.is_none (devBC ta na nida n⇩s') ⟹ (t, n, nid, n⇩s, 0) = (ta, na, nida, n⇩s', 0) ⟹ [] = bc (σ⇘the (devBC ta na nida n⇩s')⇙ta n⇩s')" by auto
  show "⋀n⇩s t n nid ta na nida n⇩s' n'.
       ¬ (∃n'<n⇩s. ¬ Option.is_none (devBC t n nid n')) ⟹
       Option.is_none (devBC t n nid n⇩s) ⟹
       ¬ Option.is_none (devBC ta na nida (n⇩s' + Suc n')) ⟹
       (t, n, nid, n⇩s, 0) = (ta, na, nida, n⇩s', Suc n') ⟹ [] = bc (σ⇘the (devBC ta na nida (n⇩s' + Suc n'))⇙ta (n⇩s' + Suc n'))" by auto
  show "⋀n⇩s t n nid ta na nida n⇩s' n'.
       ¬ (∃n'<n⇩s. ¬ Option.is_none (devBC t n nid n')) ⟹
       Option.is_none (devBC t n nid n⇩s) ⟹
       Option.is_none (devBC ta na nida (n⇩s' + Suc n')) ⟹ (t, n, nid, n⇩s, 0) = (ta, na, nida, n⇩s', Suc n') ⟹ [] = devExt_sumC (ta, na, nida, n⇩s', n')" by auto
  show "⋀t n nid n⇩s ta na nida n⇩s'.
       ¬ Option.is_none (devBC t n nid n⇩s) ⟹
       ¬ Option.is_none (devBC ta na nida n⇩s') ⟹
       (t, n, nid, n⇩s, 0) = (ta, na, nida, n⇩s', 0) ⟹ bc (σ⇘the (devBC t n nid n⇩s)⇙t n⇩s) = bc (σ⇘the (devBC ta na nida n⇩s')⇙ta n⇩s')" by auto
  show "⋀t n nid n⇩s ta na nida n⇩s' n'.
        ¬ Option.is_none (devBC t n nid n⇩s) ⟹
        ¬ Option.is_none (devBC ta na nida (n⇩s' + Suc n')) ⟹
        (t, n, nid, n⇩s, 0) = (ta, na, nida, n⇩s', Suc n') ⟹ bc (σ⇘the (devBC t n nid n⇩s)⇙t n⇩s) = bc (σ⇘the (devBC ta na nida (n⇩s' + Suc n'))⇙ta (n⇩s' + Suc n'))" by auto
  show "⋀t n nid n⇩s ta na nida n⇩s' n'.
       ¬ Option.is_none (devBC t n nid n⇩s) ⟹
       Option.is_none (devBC ta na nida (n⇩s' + Suc n')) ⟹
       (t, n, nid, n⇩s, 0) = (ta, na, nida, n⇩s', Suc n') ⟹ bc (σ⇘the (devBC t n nid n⇩s)⇙t n⇩s) = devExt_sumC (ta, na, nida, n⇩s', n')" by auto
  show "⋀t n nid n⇩s n' ta na nida n⇩s' n'a.
       ¬ Option.is_none (devBC t n nid (n⇩s + Suc n')) ⟹
       ¬ Option.is_none (devBC ta na nida (n⇩s' + Suc n'a)) ⟹
       (t, n, nid, n⇩s, Suc n') = (ta, na, nida, n⇩s', Suc n'a) ⟹
       bc (σ⇘the (devBC t n nid (n⇩s + Suc n'))⇙t (n⇩s + Suc n')) = bc (σ⇘the (devBC ta na nida (n⇩s' + Suc n'a))⇙ta (n⇩s' + Suc n'a))" by auto
  show "⋀t n nid n⇩s n' ta na nida n⇩s' n'a.
       ¬ Option.is_none (devBC t n nid (n⇩s + Suc n')) ⟹
       Option.is_none (devBC ta na nida (n⇩s' + Suc n'a)) ⟹
       (t, n, nid, n⇩s, Suc n') = (ta, na, nida, n⇩s', Suc n'a) ⟹ bc (σ⇘the (devBC t n nid (n⇩s + Suc n'))⇙t (n⇩s + Suc n')) = devExt_sumC (ta, na, nida, n⇩s', n'a)" by auto
  show "⋀t n nid n⇩s n' ta na nida n⇩s' n'a.
       Option.is_none (devBC t n nid (n⇩s + Suc n')) ⟹
       Option.is_none (devBC ta na nida (n⇩s' + Suc n'a)) ⟹
       (t, n, nid, n⇩s, Suc n') = (ta, na, nida, n⇩s', Suc n'a) ⟹ devExt_sumC (t, n, nid, n⇩s, n') = devExt_sumC (ta, na, nida, n⇩s', n'a)" by auto
  show "⋀P x. (⋀n⇩s t n nid. ∃n'<n⇩s. ¬ Option.is_none (devBC t n nid n') ⟹ Option.is_none (devBC t n nid n⇩s) ⟹ x = (t, n, nid, n⇩s, 0) ⟹ P) ⟹
           (⋀n⇩s t n nid. ¬ (∃n'<n⇩s. ¬ Option.is_none (devBC t n nid n')) ⟹ Option.is_none (devBC t n nid n⇩s) ⟹ x = (t, n, nid, n⇩s, 0) ⟹ P) ⟹
           (⋀t n nid n⇩s. ¬ Option.is_none (devBC t n nid n⇩s) ⟹ x = (t, n, nid, n⇩s, 0) ⟹ P) ⟹
           (⋀t n nid n⇩s n'. ¬ Option.is_none (devBC t n nid (n⇩s + Suc n')) ⟹ x = (t, n, nid, n⇩s, Suc n') ⟹ P) ⟹
           (⋀t n nid n⇩s n'. Option.is_none (devBC t n nid (n⇩s + Suc n')) ⟹ x = (t, n, nid, n⇩s, Suc n') ⟹ P) ⟹ P"
  proof -
    fix P::bool and x::"trace ×nat×'nid×nat×nat"
    assume a1:"(⋀n⇩s t n nid. ∃n'<n⇩s. ¬ Option.is_none (devBC t n nid n') ⟹ Option.is_none (devBC t n nid n⇩s) ⟹ x = (t, n, nid, n⇩s, 0) ⟹ P)" and
           a2:"(⋀n⇩s t n nid. ¬ (∃n'<n⇩s. ¬ Option.is_none (devBC t n nid n')) ⟹ Option.is_none (devBC t n nid n⇩s) ⟹ x = (t, n, nid, n⇩s, 0) ⟹ P)" and
           a3:"(⋀t n nid n⇩s. ¬ Option.is_none (devBC t n nid n⇩s) ⟹ x = (t, n, nid, n⇩s, 0) ⟹ P)" and
           a4:"(⋀t n nid n⇩s n'. ¬ Option.is_none (devBC t n nid (n⇩s + Suc n')) ⟹ x = (t, n, nid, n⇩s, Suc n') ⟹ P)" and
           a5:"(⋀t n nid n⇩s n'. Option.is_none (devBC t n nid (n⇩s + Suc n')) ⟹ x = (t, n, nid, n⇩s, Suc n') ⟹ P)"
    show P
    proof (cases x)
      case (fields t n nid n⇩s n')
      then show ?thesis
      proof (cases n')
        case 0
        then show ?thesis
        proof cases
          assume "Option.is_none (devBC t n nid n⇩s)"
          thus ?thesis
          proof cases
            assume "∃n'<n⇩s. ¬ Option.is_none (devBC t n nid n')"
            with ‹x = (t, n , nid, n⇩s, n')› ‹Option.is_none (devBC t n nid n⇩s)› ‹n'=0› show ?thesis using a1 by simp
          next
            assume "¬ (∃n'<n⇩s. ¬ Option.is_none (devBC t n nid n'))"
            with ‹x = (t, n , nid, n⇩s, n')› ‹Option.is_none (devBC t n nid n⇩s)› ‹n'=0› show ?thesis using a2 by simp
          qed
        next
          assume "¬ Option.is_none (devBC t n nid n⇩s)"
          with ‹x = (t, n , nid, n⇩s, n')› ‹n'=0› show ?thesis using a3 by simp
        qed
      next
        case (Suc n'')
        then show ?thesis
        proof cases
          assume "Option.is_none (devBC t n nid (n⇩s + Suc n''))"
          with ‹x = (t, n , nid, n⇩s, n')› ‹n'=Suc n''› show ?thesis using a5[of t n nid n⇩s n''] by simp
        next
          assume "¬ Option.is_none (devBC t n nid (n⇩s + Suc n''))"
          with ‹x = (t, n , nid, n⇩s, n')› ‹n'=Suc n''› show ?thesis using a4[of t n nid n⇩s n''] by simp
        qed
      qed
    qed
  qed
qed
termination by lexicographic_order

lemma devExt_same:
  assumes "∀n'''>n'. n'''≤n'' ⟶ Option.is_none (devBC t n nid n''')"
    and "n'≥n⇩s"
    and "n'''≤n''"
  shows "n'''≥n'⟹devExt t n nid n⇩s (n'''-n⇩s) = devExt t n nid n⇩s (n'-n⇩s)"
proof (induction n''' rule: dec_induct)
  case base
  then show ?case by simp
next
  case (step n'''')
  hence "Suc n''''>n'" by simp
  moreover from step.hyps assms(3) have "Suc n''''≤n''" by simp
  ultimately have "Option.is_none (devBC t n nid (Suc n''''))" using assms(1) by simp
  moreover from assms(2) step.hyps have "n''''≥n⇩s" by simp
  hence "Suc n'''' = n⇩s + Suc (n''''-n⇩s)" by simp
  ultimately have "Option.is_none (devBC t n nid (n⇩s + Suc (n''''-n⇩s)))" by metis
  hence "devExt t n nid n⇩s (Suc (n''''-n⇩s)) = devExt t n nid n⇩s (n''''-n⇩s)" by simp
  moreover from ‹n''''≥n⇩s› have "Suc (n''''-n⇩s) = Suc n''''-n⇩s" by simp
  ultimately have "devExt t n nid n⇩s (Suc n''''-n⇩s) = devExt t n nid n⇩s (n''''-n⇩s)" by simp
  with step.IH show ?case by simp
qed

lemma devExt_bc[simp]:
  assumes "¬ Option.is_none (devBC t n nid (n'+n''))"
  shows "devExt t n nid n' n'' = bc (σ⇘the (devBC t n nid (n'+n''))⇙(t (n'+n'')))"
proof (cases n'')
  case 0
  with assms show ?thesis by simp
next
  case (Suc nat)
  with assms show ?thesis by simp
qed

lemma devExt_greatest:
  assumes "∃n'''<n'+n''. ¬ Option.is_none (devBC t n nid n''')"
    and "Option.is_none (devBC t n nid (n'+n''))" and "¬ n''=0"
  shows "devExt t n nid n' n'' = bc (σ⇘the (devBC t n nid (GREATEST n'''. n'''<(n'+n'') ∧ ¬Option.is_none (devBC t n nid n''')))⇙(t (GREATEST n'''. n'''<(n'+n'') ∧ ¬Option.is_none (devBC t n nid n'''))))"
proof -
  let ?P="λn'''. n'''<(n'+n'') ∧ ¬Option.is_none (devBC t n nid n''')"
  let ?G="GREATEST n'''. ?P n'''"
  have "∀n'''>n'+n''. ¬ ?P n'''" by simp
  with ‹∃n'''<n'+n''. ¬ Option.is_none (devBC t n nid n''')› have "∃n'''. ?P n''' ∧ (∀n''''. ?P n'''' ⟶ n''''≤n''')" using boundedGreatest[of ?P] by blast
  hence "?P ?G" using GreatestI_ex_nat[of ?P] by auto
  hence "¬Option.is_none (devBC t n nid ?G)" by simp
  show ?thesis
  proof cases
    assume "?G>n'"
    hence "?G-n'+n' = ?G" by simp
    with ‹¬Option.is_none (devBC t n nid ?G)› have "¬Option.is_none (devBC t n nid (?G-n'+n'))" by simp
    moreover from ‹?G>n'› have "?G-n'≠0" by auto
    hence "∃nat. Suc nat = ?G - n'" by presburger
    then obtain nat where "Suc nat = ?G-n'" by auto
    ultimately have "¬Option.is_none (devBC t n nid (n'+Suc nat))" by simp
    hence "devExt t n nid n' (Suc nat) = bc (σ⇘the (devBC t n nid (n' + Suc nat))⇙t (n' + Suc nat))" by simp
    with ‹Suc nat = ?G - n'› have "devExt t n nid n' (?G - n') = bc (σ⇘the (devBC t n nid (?G-n'+n'))⇙(t (?G-n'+n')))" by simp
    with ‹?G-n'+n' = ?G› have "devExt t n nid n' (?G - n') = bc (σ⇘the (devBC t n nid ?G)⇙(t ?G))" by simp
    moreover have "devExt t n nid n' (n' + n'' - n') = devExt t n nid n' (?G - n')"
    proof -
      from ‹∃n'''. ?P n''' ∧ (∀n''''. ?P n'''' ⟶ n''''≤n''')› have "∀n'''. ?P n''' ⟶ n'''≤?G"
        using Greatest_le_nat[of ?P] by blast
      hence "∀n'''>?G. n'''<n'+n'' ⟶ Option.is_none (devBC t n nid n''')" by auto
      with ‹Option.is_none (devBC t n nid (n'+n''))›
        have "∀n'''>?G. n'''≤n'+n'' ⟶ Option.is_none (devBC t n nid n''')" by auto
      moreover from ‹?P ?G› have "?G≤n'+n''" by simp
      moreover from ‹?G>n'› have "?G≥n'" by simp
      ultimately show ?thesis using ‹?G>n'› devExt_same[of ?G "n'+n''" t n nid n' "n'+n''"] by blast
    qed
    ultimately show ?thesis by simp
  next
    assume "¬?G>n'"
    thus ?thesis
    proof cases
      assume "?G=n'"
      with ‹¬Option.is_none (devBC t n nid ?G)› have "¬ Option.is_none (devBC t n nid n')" by simp
      with ‹¬Option.is_none (devBC t n nid ?G)› have "devExt t n nid n' 0 = bc (σ⇘the (devBC t n nid n')⇙(t n'))" by simp
      moreover have "devExt t n nid n' n'' = devExt t n nid n' 0"
      proof -
        from ‹∃n'''. ?P n''' ∧ (∀n''''. ?P n'''' ⟶ n''''≤n''')› have "∀n'''>?G. ?P n''' ⟶ n'''≤?G"
          using Greatest_le_nat[of ?P] by blast
        with ‹?G=n'› have "∀n'''>n'. n''' < n' + n'' ⟶ Option.is_none (devBC t n nid n''')" by simp
        with ‹Option.is_none (devBC t n nid (n'+n''))›
          have "∀n'''>n'. n'''≤n'+n'' ⟶ Option.is_none (devBC t n nid n''')" by auto
        moreover from ‹¬ n''=0› have "n'<n'+n''" by simp
        ultimately show ?thesis using devExt_same[of n' "n'+n''" t n nid n' "n'+n''"] by simp
      qed
      ultimately show ?thesis using ‹?G=n'› by simp
    next
      assume "¬?G=n'"
      with ‹¬?G>n'› have "?G<n'" by simp
      hence "devExt t n nid n' n'' = devExt t n nid n' 0"
      proof -
        from ‹∃n'''. ?P n''' ∧ (∀n''''. ?P n'''' ⟶ n''''≤n''')› have "∀n'''>?G. ?P n''' ⟶ n'''≤?G"
          using Greatest_le_nat[of ?P] by blast
        with ‹¬?G>n'› have "∀n'''>n'. n'''<n'+n'' ⟶ Option.is_none (devBC t n nid n''')" by auto
        with ‹Option.is_none (devBC t n nid (n'+n''))›
          have "∀n'''>n'. n'''≤n'+n'' ⟶ Option.is_none (devBC t n nid n''')" by auto
        moreover from ‹?P ?G› have "?G<n'+n''" by simp
        moreover from ‹¬ n''=0› have "n'<n'+n''" by simp
        ultimately show ?thesis using devExt_same[of n' "n'+n''" t n nid n' "n'+n''"] by simp
      qed
      moreover have "devExt t n nid n' 0 = bc (σ⇘the (devBC t n nid (GREATEST n'''. n'''<n' ∧ ¬Option.is_none (devBC t n nid n''')))⇙(t (GREATEST n'''. n'''<n' ∧ ¬Option.is_none (devBC t n nid n'''))))"
      proof -
        from ‹¬ n''=0› have "n'<n'+n''" by simp
        moreover from ‹∃n'''. ?P n''' ∧ (∀n''''. ?P n'''' ⟶ n''''≤n''')› have "∀n'''>?G. ?P n''' ⟶ n'''≤?G" using Greatest_le_nat[of ?P] by blast
        ultimately have "Option.is_none (devBC t n nid n')" using ‹?G<n'› by simp
        moreover from ‹∀n'''>?G. ?P n''' ⟶ n'''≤?G› ‹?G<n'› ‹n'<n'+n''› have "∀n'''≥n'. n'''<n'+n'' ⟶ Option.is_none (devBC t n nid n''')" by auto
        have "∃n'''<n'. ¬ Option.is_none (devBC t n nid n''')"
        proof -
          from ‹∃n'''<n'+n''. ¬ Option.is_none (devBC t n nid n''')› obtain n'''
            where "n'''<n'+n''" and "¬ Option.is_none (devBC t n nid n''')" by auto
          moreover have "n'''<n'"
          proof (rule ccontr)
            assume "¬n'''<n'"
            hence "n'''≥n'" by simp
            with ‹∀n'''≥n'. n'''<n'+n'' ⟶ Option.is_none (devBC t n nid n''')› ‹n'''<n'+n''›
              ‹¬ Option.is_none (devBC t n nid n''')› show False by simp
          qed
          ultimately show ?thesis by auto
        qed
        ultimately show ?thesis by simp
      qed
      moreover have "(GREATEST n'''. n'''<n' ∧ ¬Option.is_none (devBC t n nid n''')) = ?G"
      proof(rule Greatest_equality)
        from ‹?P ?G› have "?G < n'+n''" and "¬Option.is_none (devBC t n nid ?G)" by auto
        with ‹?G<n'› show "?G < n' ∧ ¬ Option.is_none (devBC t n nid ?G)" by simp
      next
        fix y assume "y < n' ∧ ¬ Option.is_none (devBC t n nid y)"
        moreover from ‹∃n'''. ?P n''' ∧ (∀n''''. ?P n'''' ⟶ n''''≤n''')›
          have "∀n'''. ?P n''' ⟶ n'''≤?G" using Greatest_le_nat[of ?P] by blast
        ultimately show "y ≤ ?G" by simp
      qed
      ultimately show ?thesis by simp
    qed
  qed
qed

lemma devExt_shift: "devExt t n nid (n'+n'') 0 = devExt t n nid n' n''"
proof (cases)
  assume "n''=0"
  thus ?thesis by simp
next
  assume "¬ (n''=0)"
  thus ?thesis
  proof (cases)
    assume "Option.is_none (devBC t n nid (n'+n''))"
    thus ?thesis
    proof cases
      assume "∃n'''<n'+n''. ¬ Option.is_none (devBC t n nid n''')"
      with ‹Option.is_none (devBC t n nid (n'+n''))› have "devExt t n nid (n'+n'') 0 = bc (σ⇘the (devBC t n nid (GREATEST n'''. n'''<(n'+n'') ∧ ¬Option.is_none (devBC t n nid n''')))⇙(t (GREATEST n'''. n'''<(n'+n'') ∧ ¬Option.is_none (devBC t n nid n'''))))" by simp
      moreover from ‹¬ (n''=0)› ‹Option.is_none (devBC t n nid (n'+n''))› ‹∃n'''<n'+n''. ¬ Option.is_none (devBC t n nid n''')› have "devExt t n nid n' n'' = bc (σ⇘the (devBC t n nid (GREATEST n'''. n'''<(n'+n'') ∧ ¬Option.is_none (devBC t n nid n''')))⇙(t (GREATEST n'''. n'''<(n'+n'') ∧ ¬Option.is_none (devBC t n nid n'''))))" using devExt_greatest by simp
      ultimately show ?thesis by simp
    next
      assume "¬ (∃n'''<n'+n''. ¬ Option.is_none (devBC t n nid n'''))"
      with ‹Option.is_none (devBC t n nid (n'+n''))› have "devExt t n nid (n'+n'') 0=[]" by simp
      moreover have "devExt t n nid n' n''=[]"
      proof -
        from ‹¬ (∃n'''<n'+n''. ¬ Option.is_none (devBC t n nid n'''))› ‹n''≠0›
          have "Option.is_none (devBC t n nid n')" by simp
        moreover from ‹¬ (∃n'''<n'+n''. ¬ Option.is_none (devBC t n nid n'''))›
          have "¬ (∃n'''<n'. ¬ Option.is_none (devBC t n nid n'''))" by simp
        ultimately have "devExt t n nid n' 0=[]" by simp
        moreover have "devExt t n nid n' n''=devExt t n nid n' 0"
        proof -
          from ‹¬ (∃n'''<n'+n''. ¬ Option.is_none (devBC t n nid n'''))›
            have "∀n'''>n'. n''' < n' + n'' ⟶ Option.is_none (devBC t n nid n''')" by simp
          with ‹Option.is_none (devBC t n nid (n'+n''))› 
            have "∀n'''>n'. n'''≤n'+n'' ⟶ Option.is_none (devBC t n nid n''')" by auto
          moreover from ‹¬ n''=0› have "n'<n'+n''" by simp
          ultimately show ?thesis using devExt_same[of n' "n'+n''" t n nid n' "n'+n''"] by simp
        qed
        ultimately show ?thesis by simp
      qed
      ultimately show ?thesis by simp
    qed
  next
    assume "¬ Option.is_none (devBC t n nid (n'+n''))"
    hence "devExt t n nid (n'+n'') 0 = bc (σ⇘the (devBC t n nid (n'+n''))⇙(t (n'+n'')))" by simp
    moreover from ‹¬ Option.is_none (devBC t n nid (n'+n''))›
      have "devExt t n nid n' n'' = bc (σ⇘the (devBC t n nid (n'+n''))⇙(t (n'+n'')))" by simp
    ultimately show ?thesis by simp
  qed
qed

lemma devExt_bc_geq:
  assumes "¬ Option.is_none (devBC t n nid n')" and "n'≥n⇩s"
  shows "devExt t n nid n⇩s (n'-n⇩s) = bc (σ⇘the (devBC t n nid n')⇙(t n'))" (is "?LHS = ?RHS")
proof -
  have "devExt t n nid n⇩s (n'-n⇩s) = devExt t n nid (n⇩s+(n'-n⇩s)) 0" using devExt_shift by auto
  moreover from assms(2) have "n⇩s+(n'-n⇩s) = n'" by simp
  ultimately have "devExt t n nid n⇩s (n'-n⇩s) = devExt t n nid n' 0" by simp
  with assms(1) show ?thesis by simp
qed

lemma his_bc_empty:
  assumes "(n',nid')∈ his t n nid" and "¬(∃n''<n'. ∃nid''. (n'',nid'')∈ his t n nid)"
  shows "bc (σ⇘nid'⇙(t n')) = []"
proof -
  have "¬ (∃x. his_prop t n nid n' nid' x)"
  proof (rule ccontr)
    assume "¬ ¬ (∃x. his_prop t n nid n' nid' x)"
    hence "∃x. his_prop t n nid n' nid' x" by simp
    with ‹(n',nid')∈ his t n nid› have "(SOME x. his_prop t n nid n' nid' x) ∈ his t n nid"
      using his.intros by simp
    moreover from ‹∃x. his_prop t n nid n' nid' x› have "his_prop t n nid n' nid' (SOME x. his_prop t n nid n' nid' x)"
      using someI_ex[of "λx. his_prop t n nid n' nid' x"] by auto
    hence "(∃n. latestAct_cond nid' t n' n) ∧ fst (SOME x. his_prop t n nid n' nid' x) = ⟨nid' ← t⟩⇘n'⇙"
      by force
    hence "fst (SOME x. his_prop t n nid n' nid' x) < n'" using latestAct_prop(2)[of n' nid' t] by force
    ultimately have "fst (SOME x. his_prop t n nid n' nid' x)<n' ∧
      (fst (SOME x. his_prop t n nid n' nid' x),snd (SOME x. his_prop t n nid n' nid' x))∈ his t n nid" by simp
    thus False using assms(2) by blast
  qed
  hence "∀x. ¬ (∃n. latestAct_cond nid' t n' n) ∨ ¬ ∥snd x∥⇘t (fst x)⇙ ∨ ¬ fst x = ⟨nid' ← t⟩⇘n'⇙ ∨ ¬ (prefix (bc (σ⇘nid'⇙(t n'))) (bc (σ⇘snd x⇙(t (fst x)))) ∨ (∃b. bc (σ⇘nid'⇙(t n')) = (bc (σ⇘snd x⇙(t (fst x)))) @ [b] ∧ mining (σ⇘nid'⇙(t n'))))" by auto
  hence "¬ (∃n. latestAct_cond nid' t n' n) ∨ (∃n. latestAct_cond nid' t n' n) ∧ (∀x. ¬ ∥snd x∥⇘t (fst x)⇙ ∨ ¬ fst x = ⟨nid' ← t⟩⇘n'⇙ ∨ ¬ (prefix (bc (σ⇘nid'⇙(t n'))) (bc (σ⇘snd x⇙(t (fst x)))) ∨ (∃b. bc (σ⇘nid'⇙(t n')) = (bc (σ⇘snd x⇙(t (fst x)))) @ [b] ∧ mining (σ⇘nid'⇙(t n')))))" by auto
  thus ?thesis
  proof
    assume "¬ (∃n. latestAct_cond nid' t n' n)"
    moreover from assms(1) have "∥nid'∥⇘t n'⇙" using his_act by simp
    ultimately show ?thesis using init_model by simp
  next
    assume "(∃n. latestAct_cond nid' t n' n) ∧ (∀x. ¬ ∥snd x∥⇘t (fst x)⇙ ∨ ¬ fst x = ⟨nid' ← t⟩⇘n'⇙ ∨ ¬ (prefix (bc (σ⇘nid'⇙(t n'))) (bc (σ⇘snd x⇙(t (fst x)))) ∨ (∃b. bc (σ⇘nid'⇙(t n')) = (bc (σ⇘snd x⇙(t (fst x)))) @ [b] ∧ mining (σ⇘nid'⇙(t n')))))"
    hence "∃n. latestAct_cond nid' t n' n" and "∀x. ¬ ∥snd x∥⇘t (fst x)⇙ ∨ ¬ fst x = ⟨nid' ← t⟩⇘n'⇙ ∨ ¬ (prefix (bc (σ⇘nid'⇙(t n'))) (bc (σ⇘snd x⇙(t (fst x)))) ∨ (∃b. bc (σ⇘nid'⇙(t n')) = (bc (σ⇘snd x⇙(t (fst x)))) @ [b] ∧ mining (σ⇘nid'⇙(t n'))))" by auto
    hence asmp: "∀x. ∥snd x∥⇘t (fst x)⇙ ⟶ fst x = ⟨nid' ← t⟩⇘n'⇙ ⟶ ¬ (prefix (bc (σ⇘nid'⇙(t n'))) (bc (σ⇘snd x⇙(t (fst x)))) ∨ (∃b. bc (σ⇘nid'⇙(t n')) = (bc (σ⇘snd x⇙(t (fst x)))) @ [b] ∧ mining (σ⇘nid'⇙(t n'))))" by auto
    show ?thesis
    proof cases
      assume "honest nid'"
      moreover from assms(1) have "∥nid'∥⇘t n'⇙" using his_act by simp
      ultimately obtain nid'' where "∥nid''∥⇘t ⟨nid' ← t⟩⇘n'⇙⇙" and "mining (σ⇘nid'⇙t n') ∧ (∃b. bc (σ⇘nid'⇙t n') = bc (σ⇘nid''⇙t ⟨nid' ← t⟩⇘n'⇙) @ [b]) ∨ ¬ mining (σ⇘nid'⇙t n') ∧ bc (σ⇘nid'⇙t n') = bc (σ⇘nid''⇙t ⟨nid' ← t⟩⇘n'⇙)" using ‹∃n. latestAct_cond nid' t n' n› bhv_hn_context[of nid' t n'] by auto
      moreover from ‹∥nid''∥⇘t ⟨nid' ← t⟩⇘n'⇙⇙› have "¬ (prefix (bc (σ⇘nid'⇙(t n'))) (bc (σ⇘nid''⇙(t (⟨nid' ← t⟩⇘n'⇙)))) ∨ (∃b. bc (σ⇘nid'⇙(t n')) = (bc (σ⇘nid''⇙(t (⟨nid' ← t⟩⇘n'⇙)))) @ [b] ∧ mining (σ⇘nid'⇙(t n'))))" using asmp by auto
      ultimately have False by auto
      thus ?thesis ..
    next
      assume "¬ honest nid'"
      moreover from assms(1) have "∥nid'∥⇘t n'⇙" using his_act by simp
      ultimately obtain nid'' where "∥nid''∥⇘t ⟨nid' ← t⟩⇘n'⇙⇙" and "(mining (σ⇘nid'⇙t n') ∧ (∃b. prefix (bc (σ⇘nid'⇙t n')) (bc (σ⇘nid''⇙t ⟨nid' ← t⟩⇘n'⇙) @ [b])) ∨ ¬ mining (σ⇘nid'⇙t n') ∧ prefix (bc (σ⇘nid'⇙t n')) (bc (σ⇘nid''⇙t ⟨nid' ← t⟩⇘n'⇙)))" using ‹∃n. latestAct_cond nid' t n' n› bhv_dn_context[of nid' t n'] by auto
      moreover from ‹∥nid''∥⇘t ⟨nid' ← t⟩⇘n'⇙⇙› have "¬ (prefix (bc (σ⇘nid'⇙(t n'))) (bc (σ⇘nid''⇙(t (⟨nid' ← t⟩⇘n'⇙)))) ∨ (∃b. bc (σ⇘nid'⇙(t n')) = (bc (σ⇘nid''⇙(t (⟨nid' ← t⟩⇘n'⇙)))) @ [b] ∧ mining (σ⇘nid'⇙(t n'))))" using asmp by auto
      ultimately have False by auto
      thus ?thesis ..
    qed
  qed
qed

lemma devExt_devop:
  "prefix (devExt t n nid n⇩s (Suc n')) (devExt t n nid n⇩s n') ∨ (∃b. devExt t n nid n⇩s (Suc n') = devExt t n nid n⇩s n' @ [b]) ∧ ¬ Option.is_none (devBC t n nid (n⇩s + Suc n')) ∧ ∥the (devBC t n nid (n⇩s + Suc n'))∥⇘t (n⇩s + Suc n')⇙ ∧ n⇩s + Suc n' ≤ n ∧ mining (σ⇘the (devBC t n nid (n⇩s + Suc n'))⇙(t (n⇩s + Suc n')))"
proof cases
  assume "n⇩s + Suc n' > n"
  hence "¬(∃nid'. (n⇩s + Suc n', nid') ∈ his t n nid)" using his_le by fastforce
  hence "Option.is_none (devBC t n nid (n⇩s + Suc n'))" using devBC_def by simp
  hence "devExt t n nid n⇩s (Suc n') = devExt t n nid n⇩s n'" by simp
  thus ?thesis by simp
next
  assume "¬n⇩s + Suc n' > n"
  hence "n⇩s + Suc n' ≤ n" by simp
  show ?thesis
  proof cases
    assume "Option.is_none (devBC t n nid (n⇩s + Suc n'))"
    hence "devExt t n nid n⇩s (Suc n') = devExt t n nid n⇩s n'" by simp
    thus ?thesis by simp
  next
    assume "¬ Option.is_none (devBC t n nid (n⇩s + Suc n'))"
    hence "devExt t n nid n⇩s (Suc n') = bc (σ⇘the (devBC t n nid (n⇩s + Suc n'))⇙(t (n⇩s + Suc n')))" by simp
    moreover have "prefix (bc (σ⇘the (devBC t n nid (n⇩s + Suc n'))⇙(t (n⇩s + Suc n')))) (devExt t n nid n⇩s n') ∨ (∃b. bc (σ⇘the (devBC t n nid (n⇩s + Suc n'))⇙(t (n⇩s + Suc n'))) = devExt t n nid n⇩s n' @ [b] ∧ ¬ Option.is_none (devBC t n nid (n⇩s + Suc n')) ∧ ∥the (devBC t n nid (n⇩s + Suc n'))∥⇘t (n⇩s + Suc n')⇙ ∧ n⇩s + Suc n' ≤ n ∧ mining (σ⇘the (devBC t n nid (n⇩s + Suc n'))⇙(t (n⇩s + Suc n'))))"
    proof cases
      assume "∃n''<n⇩s + Suc n'. ∃nid'. (n'',nid')∈ his t n nid"
      let ?nid="(THE nid'. (n⇩s + Suc n',nid')∈his t n nid)"
      let ?x="SOME x. his_prop t n nid (n⇩s + Suc n') ?nid x"
      from ‹¬ Option.is_none (devBC t n nid (n⇩s + Suc n'))›
        have "n⇩s + Suc n'≤n" using devExt_nopt_leq by simp
      moreover from ‹¬ Option.is_none (devBC t n nid (n⇩s + Suc n'))›
        have "∃nid'. (n⇩s + Suc n',nid')∈his t n nid" using his_ex by simp
      ultimately have "∃x. his_prop t n nid (n⇩s + Suc n') (THE nid'. ((n⇩s + Suc n'),nid')∈his t n nid) x"
        and "(hisPred t n nid (n⇩s + Suc n'), (SOME nid'. (hisPred t n nid (n⇩s + Suc n'), nid') ∈ his t n nid)) = ?x"
        using ‹∃n''<n⇩s + Suc n'. ∃nid'. (n'',nid')∈ his t n nid›
        his_determ_ext[of "n⇩s + Suc n'" n t nid] by auto
      moreover have "bc (σ⇘(SOME nid'. (hisPred t n nid (n⇩s + Suc n'), nid') ∈ his t n nid)⇙(t (hisPred t n nid (n⇩s + Suc n')))) = devExt t n nid n⇩s n'"
      proof cases
        assume "Option.is_none (devBC t n nid (n⇩s+n'))"
        have "devExt t n nid n⇩s n' = bc (σ⇘the (devBC t n nid (GREATEST n''. n''<n⇩s+n' ∧ ¬Option.is_none (devBC t n nid n'')))⇙(t (GREATEST n''. n''<n⇩s+n' ∧ ¬Option.is_none (devBC t n nid n''))))"
        proof cases
          assume "n'=0"
          moreover have "∃n''<n⇩s+n'. ¬Option.is_none (devBC t n nid n'')"
          proof -
            from ‹∃n''<n⇩s + Suc n'. ∃nid'. (n'',nid')∈ his t n nid› obtain n''
              where "n''<Suc n⇩s + n'" and "∃nid'. (n'',nid')∈ his t n nid" by auto
            hence "¬ Option.is_none (devBC t n nid n'')" using devBC_def by simp
            moreover from ‹¬ Option.is_none (devBC t n nid n'')›
              ‹Option.is_none (devBC t n nid (n⇩s+n'))› have "¬ n''=n⇩s+n'" by auto
            with ‹n''<Suc n⇩s+n'› have "n''<n⇩s+n'" by simp
            ultimately show ?thesis by auto
          qed
          ultimately show ?thesis using ‹Option.is_none (devBC t n nid (n⇩s+n'))› by simp
        next
          assume "¬ n'=0"
          moreover have "∃n''<n⇩s + n'. ¬ Option.is_none (devBC t n nid n'')"
          proof -
            from ‹∃n''<n⇩s + Suc n'. ∃nid'. (n'',nid')∈ his t n nid› obtain n''
              where "n''<Suc n⇩s + n'" and "∃nid'. (n'',nid')∈ his t n nid" by auto
            hence "¬ Option.is_none (devBC t n nid n'')" using devBC_def by simp
            moreover from ‹¬ Option.is_none (devBC t n nid n'')› ‹Option.is_none (devBC t n nid (n⇩s+n'))›
              have "¬ n''=n⇩s+n'" by auto
            with ‹n''<Suc n⇩s+n'› have "n''<n⇩s+n'" by simp
            ultimately show ?thesis by auto
          qed
          with ‹¬ (n'=0)› ‹Option.is_none (devBC t n nid (n⇩s+n'))› show ?thesis
            using devExt_greatest[of n⇩s n' t n nid] by simp
        qed
        moreover have "(GREATEST n''. n''<n⇩s+n' ∧ ¬Option.is_none (devBC t n nid n''))=hisPred t n nid (n⇩s + Suc n')"
        proof -
          have "(λn''. n''<n⇩s+n' ∧ ¬Option.is_none (devBC t n nid n'')) = (λn''. ∃nid'. (n'',nid')∈ his t n nid ∧ n'' < n⇩s + Suc n')"
          proof
            fix n''
            show "(n'' < n⇩s + n' ∧ ¬ Option.is_none (devBC t n nid n'')) = (∃nid'. (n'', nid') ∈ his t n nid ∧ n'' < n⇩s + Suc n')"
            proof
              assume "n'' < n⇩s + n' ∧ ¬ Option.is_none (devBC t n nid n'')"
              thus "(∃nid'. (n'', nid') ∈ his t n nid ∧ n'' < n⇩s + Suc n')" using his_ex by simp
            next
              assume "(∃nid'. (n'', nid') ∈ his t n nid ∧ n'' < n⇩s + Suc n')"
              hence "∃nid'. (n'', nid') ∈ his t n nid" and "n'' < n⇩s + Suc n'" by auto
              hence "¬ Option.is_none (devBC t n nid n'')" using devBC_def by simp
              moreover from ‹¬ Option.is_none (devBC t n nid n'')› ‹Option.is_none (devBC t n nid (n⇩s+n'))›
              have "n''≠n⇩s+n'" by auto
              with ‹n'' < n⇩s + Suc n'› have "n'' < n⇩s + n'" by simp
              ultimately show "n'' < n⇩s + n' ∧ ¬ Option.is_none (devBC t n nid n'')" by simp
            qed
          qed
          hence "(GREATEST n''. n''<n⇩s+n' ∧ ¬Option.is_none (devBC t n nid n''))= (GREATEST n''. ∃nid'. (n'',nid')∈ his t n nid ∧ n'' < n⇩s + Suc n')" using arg_cong[of "λn''. n''<n⇩s+n' ∧ ¬Option.is_none (devBC t n nid n'')" "(λn''. ∃nid'. (n'',nid')∈ his t n nid ∧ n'' < n⇩s + Suc n')"] by simp
          with hisPred_def show ?thesis by simp
        qed
        moreover have "the (devBC t n nid (hisPred t n nid (n⇩s + Suc n')))=(SOME nid'. (hisPred t n nid (n⇩s + Suc n'), nid') ∈ his t n nid)"
        proof -
          from ‹∃n''<n⇩s + Suc n'. ∃nid'. (n'',nid')∈ his t n nid›
            have "∃nid'. (hisPred t n nid (n⇩s + Suc n'), nid')∈ his t n nid"
            using hisPrev_prop(2) by simp
          hence "the (devBC t n nid (hisPred t n nid (n⇩s + Suc n'))) = (THE nid'. (hisPred t n nid (n⇩s + Suc n'), nid')∈his t n nid)"
            using devBC_def by simp
          moreover from ‹∃nid'. (hisPred t n nid (n⇩s + Suc n'), nid')∈ his t n nid›
            have "(hisPred t n nid (n⇩s + Suc n'), SOME nid'. (hisPred t n nid (n⇩s + Suc n'), nid') ∈ his t n nid) ∈ his t n nid"
            using someI_ex[of "λnid'. (hisPred t n nid (n⇩s + Suc n'), nid')∈his t n nid"] by simp
          hence "(THE nid'. (hisPred t n nid (n⇩s + Suc n'), nid')∈his t n nid) = (SOME nid'. (hisPred t n nid (n⇩s + Suc n'), nid') ∈ his t n nid)"
            using his_determ_the by simp
          ultimately show ?thesis by simp
        qed
        ultimately show ?thesis by simp
      next
        assume "¬ Option.is_none (devBC t n nid (n⇩s+n'))"
        hence "devExt t n nid n⇩s n' = bc (σ⇘the (devBC t n nid (n⇩s+n'))⇙(t (n⇩s+n')))"
        proof cases
          assume "n'=0"
          with ‹¬ Option.is_none (devBC t n nid (n⇩s+n'))› show ?thesis by simp
        next
          assume "¬ n'=0"
          hence "∃nat. n' = Suc nat" by presburger
          then obtain nat where "n' = Suc nat" by auto
          with ‹¬ Option.is_none (devBC t n nid (n⇩s+n'))› have "devExt t n nid n⇩s (Suc nat) = bc (σ⇘the (devBC t n nid (n⇩s + Suc nat))⇙(t (n⇩s + Suc nat)))" by simp
          with ‹n' = Suc nat›  show ?thesis by simp
        qed
        moreover have "hisPred t n nid (n⇩s + Suc n') = n⇩s+n'"
        proof -
          have "(GREATEST n''. ∃nid'. (n'',nid')∈ his t n nid ∧ n'' < (n⇩s + Suc n')) = n⇩s+n'"
          proof (rule Greatest_equality)
            from ‹¬ Option.is_none (devBC t n nid (n⇩s+n'))› have "∃nid'. (n⇩s + n', nid') ∈ his t n nid" using his_ex by simp
            thus "∃nid'. (n⇩s + n', nid') ∈ his t n nid ∧ n⇩s + n' < n⇩s + Suc n'" by simp
          next
            fix y assume "∃nid'. (y, nid') ∈ his t n nid ∧ y < n⇩s + Suc n'"
            thus "y ≤ n⇩s + n'" by simp
          qed
          thus ?thesis using hisPred_def by simp
        qed
        moreover have "the (devBC t n nid (hisPred t n nid (n⇩s + Suc n')))=(SOME nid'. (hisPred t n nid (n⇩s + Suc n'), nid') ∈ his t n nid)"
        proof -
          from ‹∃n''<n⇩s + Suc n'. ∃nid'. (n'',nid')∈ his t n nid›
            have "∃nid'. (hisPred t n nid (n⇩s + Suc n'), nid')∈ his t n nid"
            using hisPrev_prop(2) by simp
          hence "the (devBC t n nid (hisPred t n nid (n⇩s + Suc n'))) = (THE nid'. (hisPred t n nid (n⇩s + Suc n'), nid')∈his t n nid)"
            using devBC_def by simp
          moreover from ‹∃nid'. (hisPred t n nid (n⇩s + Suc n'), nid')∈ his t n nid›
            have "(hisPred t n nid (n⇩s + Suc n'), SOME nid'. (hisPred t n nid (n⇩s + Suc n'), nid') ∈ his t n nid) ∈ his t n nid"
            using someI_ex[of "λnid'. (hisPred t n nid (n⇩s + Suc n'), nid')∈his t n nid"] by simp
          hence "(THE nid'. (hisPred t n nid (n⇩s + Suc n'), nid')∈his t n nid) = (SOME nid'. (hisPred t n nid (n⇩s + Suc n'), nid') ∈ his t n nid)"
            using his_determ_the by simp
          ultimately show ?thesis by simp
        qed
        ultimately show ?thesis by simp
      qed
      ultimately have "bc (σ⇘snd ?x⇙(t (fst ?x))) = devExt t n nid n⇩s n'"
        using fst_conv[of "hisPred t n nid (n⇩s + Suc n')"
        "(SOME nid'. (hisPred t n nid (n⇩s + Suc n'), nid') ∈ his t n nid)"]
        snd_conv[of "hisPred t n nid (n⇩s + Suc n')"
        "(SOME nid'. (hisPred t n nid (n⇩s + Suc n'), nid') ∈ his t n nid)"] by simp
      moreover from ‹∃x. his_prop t n nid (n⇩s + Suc n') ?nid x›
        have "his_prop t n nid (n⇩s + Suc n') ?nid ?x"
        using someI_ex[of "λx. his_prop t n nid (n⇩s + Suc n') ?nid x"] by blast
      hence "prefix (bc (σ⇘?nid⇙(t (n⇩s + Suc n')))) (bc (σ⇘snd ?x⇙(t (fst ?x)))) ∨ (∃b. bc (σ⇘?nid⇙(t (n⇩s + Suc n'))) = (bc (σ⇘snd ?x⇙(t (fst ?x)))) @ [b] ∧ mining (σ⇘?nid⇙(t (n⇩s + Suc n'))))" by blast
      ultimately have "prefix (bc (σ⇘?nid⇙(t (n⇩s + Suc n')))) (devExt t n nid n⇩s n') ∨ (∃b. bc (σ⇘?nid⇙(t (n⇩s + Suc n'))) = (devExt t n nid n⇩s n') @ [b] ∧ mining (σ⇘?nid⇙(t (n⇩s + Suc n'))))" by simp
      moreover from ‹∃nid'. (n⇩s + Suc n',nid')∈ his t n nid›
        have "?nid=the (devBC t n nid (n⇩s + Suc n'))" using devBC_def by simp
      moreover have "∥the (devBC t n nid (n⇩s + Suc n'))∥⇘t (n⇩s + Suc n')⇙"
      proof -
        from ‹∃nid'. (n⇩s + Suc n',nid')∈his t n nid› obtain nid'
          where "(n⇩s + Suc n',nid')∈his t n nid" by auto
        with his_determ_the have "nid' = (THE nid'. (n⇩s + Suc n', nid') ∈ his t n nid)" by simp
        with ‹?nid=the (devBC t n nid (n⇩s + Suc n'))›
          have "the (devBC t n nid (n⇩s + Suc n')) = nid'" by simp
        with ‹(n⇩s + Suc n',nid')∈his t n nid› show ?thesis using his_act by simp
      qed
      ultimately show ?thesis
        using ‹¬ Option.is_none (devBC t n nid (n⇩s+Suc n'))› ‹n⇩s + Suc n' ≤ n› by simp
    next
      assume "¬ (∃n''<n⇩s + Suc n'. ∃nid'. (n'',nid')∈ his t n nid)"
      moreover have "(n⇩s + Suc n', the (devBC t n nid (n⇩s + Suc n'))) ∈ his t n nid"
      proof -
        from ‹¬ Option.is_none (devBC t n nid (n⇩s + Suc n'))›
          have "∃nid'. (n⇩s + Suc n',nid')∈his t n nid" using his_ex by simp
        hence "the (devBC t n nid (n⇩s + Suc n')) = (THE nid'. (n⇩s + Suc n', nid') ∈ his t n nid)"
          using devBC_def by simp
        moreover from ‹∃nid'. (n⇩s + Suc n',nid')∈his t n nid› obtain nid'
          where "(n⇩s + Suc n',nid')∈his t n nid" by auto
        with his_determ_the have "nid' = (THE nid'. (n⇩s + Suc n', nid') ∈ his t n nid)" by simp
        ultimately have "the (devBC t n nid (n⇩s + Suc n')) = nid'" by simp
        with ‹(n⇩s + Suc n',nid')∈his t n nid› show ?thesis by simp
      qed
      ultimately have "bc (σ⇘the (devBC t n nid (n⇩s + Suc n'))⇙(t (n⇩s + Suc n'))) = []"
        using his_bc_empty by simp
      thus ?thesis by simp
    qed
    ultimately show ?thesis by simp
  qed
qed

abbreviation devLgthBC where "devLgthBC t n nid n⇩s ≡ (λn'. length (devExt t n nid n⇩s n'))"

theorem blockchain_save:
  fixes t::"nat⇒cnf" and n⇩s and sbc and n
  assumes "∀nid. honest nid ⟶ prefix sbc (bc (σ⇘nid⇙(t (⟨nid → t⟩⇘n⇩s⇙))))"
    and "∀nid∈actDn (t n⇩s). length (bc (σ⇘nid⇙(t n⇩s))) < length sbc"
    and "PoW t n⇩s≥length sbc + cb"
    and "∀n'<n⇩s. ∀nid. ∥nid∥⇘t n'⇙ ⟶ length (bc (σ⇘nid⇙t n')) < length sbc ∨ prefix sbc (bc (σ⇘nid⇙(t n')))"
    and "n≥n⇩s"
  shows "∀nid ∈ actHn (t n). prefix sbc (bc (σ⇘nid⇙(t n)))"
proof (cases)
  assume "sbc=[]"
  thus ?thesis by simp
next
  assume "¬ sbc=[]"
  have "n≥n⇩s ⟹ ∀nid ∈ actHn (t n). prefix sbc (bc (σ⇘nid⇙(t n)))"
  proof (induction n rule: ge_induct)
    case (step n)
    show ?case
    proof
      fix nid assume "nid ∈ actHn (t n)"
      hence "∥nid∥⇘t n⇙" and "honest nid" using actHn_def by auto
      show "prefix sbc (bc (σ⇘nid⇙t n))"
      proof cases
        assume lAct: "∃n' < n. n' ≥ n⇩s ∧ ∥nid∥⇘t n'⇙"    
        show ?thesis
        proof cases
          assume "∃b∈pin (σ⇘nid⇙t ⟨nid ← t⟩⇘n⇙). length b > length (bc (σ⇘nid⇙t ⟨nid ← t⟩⇘n⇙))"
          moreover from ‹∥nid∥⇘t n⇙› have "∃n'≥n. ∥nid∥⇘t n'⇙" by auto
          moreover from lAct have "∃n'. latestAct_cond nid t n n'" by auto
          ultimately have "¬ mining (σ⇘nid⇙t ⟨nid → t⟩⇘n⇙) ∧ bc (σ⇘nid⇙t ⟨nid → t⟩⇘n⇙) = MAX (pin (σ⇘nid⇙t ⟨nid ← t⟩⇘n⇙)) ∨
            mining (σ⇘nid⇙t ⟨nid → t⟩⇘n⇙) ∧ (∃b. bc (σ⇘nid⇙t ⟨nid → t⟩⇘n⇙) = MAX (pin (σ⇘nid⇙t ⟨nid ← t⟩⇘n⇙)) @ [b])"
            using ‹honest nid› bhv_hn_ex[of nid n t] by simp
          moreover have "prefix sbc (MAX (pin (σ⇘nid⇙t ⟨nid ← t⟩⇘n⇙)))"
          proof -
            from ‹∃n'. latestAct_cond nid t n n'› have "∥nid∥⇘t ⟨nid ← t⟩⇘n⇙⇙"
              using latestAct_prop(1) by simp
            hence "pin (σ⇘nid⇙t ⟨nid ← t⟩⇘n⇙) ≠ {}" and "finite (pin (σ⇘nid⇙t ⟨nid ← t⟩⇘n⇙))"
              using nempty_input[of nid t "⟨nid ← t⟩⇘n⇙"] finite_input[of nid t "⟨nid ← t⟩⇘n⇙"] ‹honest nid› by auto
            hence "MAX (pin (σ⇘nid⇙t ⟨nid ← t⟩⇘n⇙)) ∈ pin (σ⇘nid⇙t ⟨nid ← t⟩⇘n⇙)" using max_prop(1) by auto
            with ‹∥nid∥⇘t ⟨nid ← t⟩⇘n⇙⇙› obtain nid' where "∥nid'∥⇘t ⟨nid ← t⟩⇘n⇙⇙"
              and "bc (σ⇘nid'⇙(t ⟨nid ← t⟩⇘n⇙)) = MAX (pin (σ⇘nid⇙t ⟨nid ← t⟩⇘n⇙))"
              using closed[where b="MAX (pin (σ⇘nid⇙t ⟨nid ← t⟩⇘n⇙))"] by blast
            moreover have "prefix sbc (bc (σ⇘nid'⇙(t ⟨nid ← t⟩⇘n⇙)))"
            proof cases
              assume "honest nid'"
              with ‹∥nid'∥⇘t ⟨nid ← t⟩⇘n⇙⇙› have "nid' ∈ actHn (t ⟨nid ← t⟩⇘n⇙)"
                using actHn_def by simp
              moreover from ‹∃n'. latestAct_cond nid t n n'› have "⟨nid ← t⟩⇘n⇙ < n"
                using latestAct_prop(2) by simp
              moreover from lAct have "⟨nid ← t⟩⇘n⇙ ≥ n⇩s" using latestActless by blast
              ultimately show ?thesis using ‹∥nid'∥⇘t ⟨nid ← t⟩⇘n⇙⇙› step.IH by simp
            next
              assume "¬ honest nid'"
              show ?thesis
              proof (rule ccontr)
                assume "¬ prefix sbc (bc (σ⇘nid'⇙(t ⟨nid ← t⟩⇘n⇙)))"
                moreover have "∃n'≤⟨nid ← t⟩⇘n⇙. n'≥n⇩s ∧ length (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' 0) < length sbc ∧ (∀n''>n'. n''≤⟨nid ← t⟩⇘n⇙ ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'') ⟶ ¬ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'')))"
                proof cases
                  assume "∃n'≤⟨nid ← t⟩⇘n⇙. n'≥n⇩s ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n') ∧ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'))"
                  hence "∃n'≤⟨nid ← t⟩⇘n⇙. n'≥n⇩s ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n') ∧ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n')) ∧ (∀n''>n'. n''≤⟨nid ← t⟩⇘n⇙ ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'') ⟶ ¬ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'')))"
                  proof -
                    let ?P="λn'. n'≤⟨nid ← t⟩⇘n⇙ ∧ n'≥n⇩s  ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n') ∧ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'))"
                    from ‹∃n'≤⟨nid ← t⟩⇘n⇙. n'≥n⇩s  ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n') ∧ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'))› have "∃n'. ?P n'" by simp
                    moreover have "∀n'>⟨nid ← t⟩⇘n⇙. ¬ ?P n'" by simp
                    ultimately obtain n' where "?P n'" and "∀n''. ?P n'' ⟶ n''≤n'" using boundedGreatest[of ?P _ "⟨nid ← t⟩⇘n⇙"] by auto
                    hence "∀n''>n'. n''≤⟨nid ← t⟩⇘n⇙ ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'') ⟶ ¬ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n''))" by auto
                    thus ?thesis using ‹?P n'› by auto
                  qed
                  then obtain n' where "n'≤⟨nid ← t⟩⇘n⇙" and "¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n')"
                    and "n'≥n⇩s" and "honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'))"
                    and "∀n''>n'. n''≤⟨nid ← t⟩⇘n⇙ ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'') ⟶ ¬ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n''))" by auto
                  hence "n'≥n⇩s" and dishonest: "∀n''>n'. n''≤⟨nid ← t⟩⇘n⇙ ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'') ⟶ ¬ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n''))" by auto
                  moreover have "⟨nid ← t⟩⇘n⇙<n" using ‹∃n'. latestAct_cond nid t n n'› latestAct_prop(2) by blast
                  with ‹n'≤⟨nid ← t⟩⇘n⇙› have "n'<n" by simp
                  moreover from ‹¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n')›
                    have "∥the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n')∥⇘t n'⇙" using devBC_act by simp
                  with ‹honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'))›
                    have "the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n') ∈actHn (t n')" using actHn_def by simp
                  ultimately have "prefix sbc (bc (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n')⇙t n'))"
                    using step.IH by simp
  
                  interpret ut: dishonest "devExt t ⟨nid ← t⟩⇘n⇙ nid' n'" "λn. dmining t (n' + n)"
                  proof
                    fix n''
                    from devExt_devop[of t "⟨nid ← t⟩⇘n⇙" nid' n'] have "prefix (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' (Suc n'')) (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' n'') ∨ (∃b. devExt t ⟨nid ← t⟩⇘n⇙ nid' n' (Suc n'') = devExt t ⟨nid ← t⟩⇘n⇙ nid' n' n'' @ [b]) ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n'')) ∧ ∥the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))∥⇘t (n' + Suc n'')⇙ ∧ n' + Suc n'' ≤ ⟨nid ← t⟩⇘n⇙ ∧ mining (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))⇙t (n' + Suc n''))" .
                    thus "prefix (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' (Suc n'')) (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' n'') ∨ (∃b. devExt t ⟨nid ← t⟩⇘n⇙ nid' n' (Suc n'') = devExt t ⟨nid ← t⟩⇘n⇙ nid' n' n'' @ [b]) ∧ dmining t (n' + Suc n'')"
                    proof
                      assume "prefix (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' (Suc n'')) (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' n'')"
                      thus ?thesis by simp
                    next
                      assume "(∃b. devExt t ⟨nid ← t⟩⇘n⇙ nid' n' (Suc n'') = devExt t ⟨nid ← t⟩⇘n⇙ nid' n' n'' @ [b]) ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n'')) ∧ ∥the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))∥⇘t (n' + Suc n'')⇙ ∧ n' + Suc n'' ≤ ⟨nid ← t⟩⇘n⇙ ∧ mining (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))⇙t (n' + Suc n''))"
                      hence "∃b. devExt t ⟨nid ← t⟩⇘n⇙ nid' n' (Suc n'') = devExt t ⟨nid ← t⟩⇘n⇙ nid' n' n'' @ [b]" and "¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))" and "∥the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))∥⇘t (n' + Suc n'')⇙" and "n' + Suc n'' ≤ ⟨nid ← t⟩⇘n⇙" and "mining (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))⇙t (n' + Suc n''))" by auto
                      moreover from ‹n' + Suc n'' ≤ ⟨nid ← t⟩⇘n⇙› ‹¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))› have "¬ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n'')))" using dishonest by simp
                      with ‹∥the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))∥⇘t (n' + Suc n'')⇙› have "the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))∈actDn (t (n' + Suc n''))" using actDn_def by simp
                      ultimately show ?thesis using dmining_def by auto
                    qed
                  qed
                  from ‹¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n')› have "bc (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n')⇙t n') = devExt t ⟨nid ← t⟩⇘n⇙ nid' n' 0"
                    using devExt_bc_geq[of t "⟨nid ← t⟩⇘n⇙" nid' n'] by simp
                  moreover from ‹n'≤⟨nid ← t⟩⇘n⇙› ‹∥nid'∥⇘t ⟨nid ← t⟩⇘n⇙⇙› have "bc (σ⇘nid'⇙t ⟨nid ← t⟩⇘n⇙) = devExt t ⟨nid ← t⟩⇘n⇙ nid' n' (⟨nid ← t⟩⇘n⇙-n')"
                    using devExt_bc_geq by simp
                  with ‹¬ prefix sbc (bc (σ⇘nid'⇙(t ⟨nid ← t⟩⇘n⇙)))› have "¬ prefix sbc (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' (⟨nid ← t⟩⇘n⇙-n'))" by simp
                  ultimately have "∃n'''. n''' ≤ ⟨nid ← t⟩⇘n⇙-n' ∧ length (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' n''') < length sbc"
                    using ‹prefix sbc (bc (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n')⇙(t n')))›
                    ut.prefix_length[of sbc 0 "⟨nid ← t⟩⇘n⇙-n'"] by auto
                  then obtain n⇩p where "n⇩p ≤ ⟨nid ← t⟩⇘n⇙-n'"
                    and "length (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' n⇩p) < length sbc" by auto
                  hence "length (devExt t ⟨nid ← t⟩⇘n⇙ nid' (n' + n⇩p) 0) < length sbc" using devExt_shift[of t "⟨nid ← t⟩⇘n⇙" nid' n' n⇩p] by simp
                  moreover from ‹⟨nid ← t⟩⇘n⇙≥n'› ‹n⇩p ≤ ⟨nid ← t⟩⇘n⇙-n'› have "(n' + n⇩p) ≤ ⟨nid ← t⟩⇘n⇙" by simp
                  ultimately show ?thesis using ‹n'≥n⇩s› dishonest by auto
                next
                  assume "¬(∃n'≤⟨nid ← t⟩⇘n⇙. n'≥n⇩s ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n') ∧ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n')))"
                  hence cas: "∀n'≤⟨nid ← t⟩⇘n⇙. n'≥n⇩s ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n') ⟶ ¬ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'))" by auto
                  show ?thesis
                  proof cases
                    assume "Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n⇩s)"
                    thus ?thesis
                    proof cases
                      assume "∀n'<n⇩s. Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n')"
                      with ‹Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n⇩s)› have "devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s 0 = []" by simp
                      with ‹¬ sbc=[]› have "length (devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s 0) < length sbc" by simp
                      moreover from lAct have "⟨nid ← t⟩⇘n⇙≥n⇩s" using latestActless by blast
                      moreover from cas have "∀n''>n⇩s. n''≤⟨nid ← t⟩⇘n⇙ ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'') ⟶ ¬ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n''))" by simp
                      ultimately show ?thesis by auto
                    next
                      let ?P="λn'. n'<n⇩s ∧ ¬Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n')"
                      let ?n'="GREATEST n'. ?P n'"
                      assume "¬ (∀n'<n⇩s. Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'))"
                      moreover have "∀n'>n⇩s. ¬ ?P n'" by simp
                      ultimately have exists: "∃n'. ?P n' ∧ (∀n''. ?P n''⟶ n''≤n')"
                        using boundedGreatest[of ?P] by blast
                      hence "?P ?n'" using GreatestI_ex_nat[of ?P] by auto
                      moreover from ‹?P ?n'› have "∥the (devBC t ⟨nid ← t⟩⇘n⇙ nid' ?n')∥⇘t ?n'⇙" using devBC_act by simp
                      ultimately have "length (bc (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' ?n')⇙t ?n')) < length sbc ∨ prefix sbc (bc (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' ?n')⇙(t ?n')))" using assms(4) by simp
                      thus ?thesis
                      proof
                        assume "length (bc (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' ?n')⇙t ?n')) < length sbc"
                        moreover from exists have "¬(∃n'>?n'. ?P n')" using Greatest_ex_le_nat[of ?P] by simp
                        moreover from ‹?P ?n'› have "∃n'<n⇩s. ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n')" by blast
                        with ‹Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n⇩s)›
                          have "devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s 0 = bc (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' ?n')⇙(t ?n'))" by simp
                        ultimately have "length (devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s 0) < length sbc" by simp
                        moreover from lAct have "⟨nid ← t⟩⇘n⇙≥n⇩s" using latestActless by blast
                        moreover from cas have "∀n''>n⇩s. n''≤⟨nid ← t⟩⇘n⇙ ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'') ⟶ ¬ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n''))" by simp
                        ultimately show ?thesis by auto
                      next
                        interpret ut: dishonest "devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s" "λn. dmining t (n⇩s + n)"
                        proof
                          fix n''
                          from devExt_devop[of t "⟨nid ← t⟩⇘n⇙" nid' n⇩s] have "prefix (devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s (Suc n'')) (devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s n'') ∨ (∃b. devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s (Suc n'') = devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s n'' @ [b]) ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n⇩s + Suc n'')) ∧ ∥the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n⇩s + Suc n''))∥⇘t (n⇩s + Suc n'')⇙ ∧ n⇩s + Suc n'' ≤ ⟨nid ← t⟩⇘n⇙ ∧ mining (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n⇩s + Suc n''))⇙t (n⇩s + Suc n''))" .
                          thus "prefix (devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s (Suc n'')) (devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s n'') ∨ (∃b. devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s (Suc n'') = devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s n'' @ [b]) ∧ dmining t (n⇩s + Suc n'')"
                          proof
                            assume "prefix (devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s (Suc n'')) (devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s n'')" thus ?thesis by simp
                          next
                            assume "(∃b. devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s (Suc n'') = devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s n'' @ [b]) ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n⇩s + Suc n'')) ∧ ∥the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n⇩s + Suc n''))∥⇘t (n⇩s + Suc n'')⇙ ∧ n⇩s + Suc n'' ≤ ⟨nid ← t⟩⇘n⇙ ∧ mining (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n⇩s + Suc n''))⇙t (n⇩s + Suc n''))"
                            hence "∃b. devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s (Suc n'') = devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s n'' @ [b]"
                              and "¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n⇩s + Suc n''))"
                              and "∥the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n⇩s + Suc n''))∥⇘t (n⇩s + Suc n'')⇙"
                              and "n⇩s + Suc n'' ≤ ⟨nid ← t⟩⇘n⇙"
                              and "mining (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n⇩s + Suc n''))⇙t (n⇩s + Suc n''))"
                              by auto
                            moreover from ‹n⇩s + Suc n'' ≤ ⟨nid ← t⟩⇘n⇙› ‹¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n⇩s + Suc n''))›
                              have "¬ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n⇩s + Suc n'')))"
                              using cas by simp
                            with ‹∥the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n⇩s + Suc n''))∥⇘t (n⇩s + Suc n'')⇙›
                              have "the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n⇩s + Suc n''))∈actDn (t (n⇩s + Suc n''))" using actDn_def by simp
                            ultimately show ?thesis using dmining_def by auto
                          qed
                        qed
  
                        assume "prefix sbc (bc (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' ?n')⇙(t ?n')))"
                        moreover from exists have "¬(∃n'>?n'. ?P n')" using Greatest_ex_le_nat[of ?P] by simp
                        moreover from ‹?P ?n'› have "∃n'<n⇩s. ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n')" by blast
                        with ‹Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n⇩s)› have "devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s 0 = bc (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' ?n')⇙(t ?n'))" by simp
                        ultimately have "prefix sbc (devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s 0)" by simp
                        moreover from lAct have "⟨nid ← t⟩⇘n⇙≥n⇩s" using latestActless by blast
                        with ‹∥nid'∥⇘t ⟨nid ← t⟩⇘n⇙⇙› have "bc (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' ⟨nid ← t⟩⇘n⇙)⇙t ⟨nid ← t⟩⇘n⇙) = devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s (⟨nid ← t⟩⇘n⇙-n⇩s)" using devExt_bc_geq by simp
                        with ‹¬ prefix sbc (bc (σ⇘nid'⇙(t ⟨nid ← t⟩⇘n⇙)))› ‹∥nid'∥⇘t ⟨nid ← t⟩⇘n⇙⇙› have "¬ prefix sbc (devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s (⟨nid ← t⟩⇘n⇙-n⇩s))" by simp
                        ultimately have "∃n'''>0. n''' ≤ ⟨nid ← t⟩⇘n⇙-n⇩s ∧ length (devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s n''') < length sbc" using ut.prefix_length[of sbc 0 "⟨nid ← t⟩⇘n⇙-n⇩s"] by simp
                        then obtain n⇩p where "n⇩p>0" and "n⇩p ≤ ⟨nid ← t⟩⇘n⇙-n⇩s" and "length (devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s n⇩p) < length sbc" by auto
                        hence "length (devExt t ⟨nid ← t⟩⇘n⇙ nid' (n⇩s + n⇩p) 0) < length sbc" using devExt_shift by simp
                        moreover from lAct have "⟨nid ← t⟩⇘n⇙≥n⇩s" using latestActless by blast
                        with ‹n⇩p ≤ ⟨nid ← t⟩⇘n⇙-n⇩s› have "(n⇩s + n⇩p) ≤ ⟨nid ← t⟩⇘n⇙" by simp
                        moreover from ‹n⇩p ≤ ⟨nid ← t⟩⇘n⇙-n⇩s› have "n⇩p ≤ ⟨nid ← t⟩⇘n⇙" by simp
                        moreover have "∀n''>n⇩s + n⇩p. n'' ≤ ⟨nid ← t⟩⇘n⇙ ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'') ⟶ ¬ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n''))" using cas by simp
                        ultimately show ?thesis by auto
                      qed
                    qed
                  next
                    assume asmp: "¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n⇩s)"
                    moreover from lAct have "n⇩s≤⟨nid ← t⟩⇘n⇙" using latestActless by blast
                    ultimately have "¬ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n⇩s))" using cas by simp
                    moreover from asmp have "∥the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n⇩s)∥⇘t n⇩s⇙"
                      using devBC_act by simp
                    ultimately have "the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n⇩s)∈actDn (t n⇩s)"
                      using actDn_def by simp
                    hence "length (bc (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n⇩s)⇙(t n⇩s))) < length sbc"
                      using assms(2) by simp
                    moreover from asmp have
                      "devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s 0 = bc (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n⇩s)⇙(t n⇩s))"
                      by simp
                    ultimately have "length (devExt t ⟨nid ← t⟩⇘n⇙ nid' n⇩s 0) < length sbc" by simp
                    moreover from lAct have "⟨nid ← t⟩⇘n⇙≥n⇩s" using latestActless by blast
                    moreover from cas have "∀n''>n⇩s. n''≤⟨nid ← t⟩⇘n⇙ ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'') ⟶ ¬ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n''))" by simp
                    ultimately show ?thesis by auto
                  qed
                qed
                then obtain n' where "⟨nid ← t⟩⇘n⇙≥n'" and "n'≥n⇩s"
                  and "length (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' 0) < length sbc"
                  and dishonest: "∀n''>n'. n''≤⟨nid ← t⟩⇘n⇙ ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' n'') ⟶ ¬ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' n''))" by auto
                interpret ut: dishonest "devExt t ⟨nid ← t⟩⇘n⇙ nid' n'" "λn. dmining t (n' + n)"
                proof
                  fix n''
                  from devExt_devop[of t "⟨nid ← t⟩⇘n⇙" nid' n']
                  have "prefix (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' (Suc n'')) (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' n'') ∨
                    (∃b. devExt t ⟨nid ← t⟩⇘n⇙ nid' n' (Suc n'') = devExt t ⟨nid ← t⟩⇘n⇙ nid' n' n'' @ [b]) ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n'')) ∧ ∥the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))∥⇘t (n' + Suc n'')⇙ ∧ n' + Suc n'' ≤ ⟨nid ← t⟩⇘n⇙ ∧ mining (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))⇙t (n' + Suc n''))" .
                  thus "prefix (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' (Suc n'')) (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' n'')
                    ∨ (∃b. devExt t ⟨nid ← t⟩⇘n⇙ nid' n' (Suc n'') = devExt t ⟨nid ← t⟩⇘n⇙ nid' n' n'' @ [b]) ∧ dmining t (n' + Suc n'')"
                  proof
                    assume "prefix (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' (Suc n'')) (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' n'')"
                    thus ?thesis by simp
                  next
                    assume "(∃b. devExt t ⟨nid ← t⟩⇘n⇙ nid' n' (Suc n'') = devExt t ⟨nid ← t⟩⇘n⇙ nid' n' n'' @ [b]) ∧ ¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n'')) ∧ ∥the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))∥⇘t (n' + Suc n'')⇙ ∧ n' + Suc n'' ≤ ⟨nid ← t⟩⇘n⇙ ∧ mining (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))⇙t (n' + Suc n''))"
                    hence "∃b. devExt t ⟨nid ← t⟩⇘n⇙ nid' n' (Suc n'') = devExt t ⟨nid ← t⟩⇘n⇙ nid' n' n'' @ [b]"
                      and "¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))"
                      and "∥the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))∥⇘t (n' + Suc n'')⇙"
                      and "n' + Suc n'' ≤ ⟨nid ← t⟩⇘n⇙"
                      and "mining (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))⇙t (n' + Suc n''))"
                      by auto
                    moreover from ‹n' + Suc n'' ≤ ⟨nid ← t⟩⇘n⇙› ‹¬ Option.is_none (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))›
                      have "¬ honest (the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n'')))" using dishonest by simp
                    with ‹∥the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))∥⇘t (n' + Suc n'')⇙›
                      have "the (devBC t ⟨nid ← t⟩⇘n⇙ nid' (n' + Suc n''))∈actDn (t (n' + Suc n''))"
                      using actDn_def by simp
                    ultimately show ?thesis using dmining_def by auto
                  qed
                qed
                interpret dishonest_growth "devLgthBC t ⟨nid ← t⟩⇘n⇙ nid' n'" "λn. dmining t (n' + n)"
                  by unfold_locales
                interpret honest_growth "λn. PoW t (n' + n)" "λn. hmining t (n' + n)"
                proof
                  show "⋀n. PoW t (n' + n) ≤ PoW t (n' + Suc n)" using pow_mono by simp
                  show "⋀n. hmining t (n' + Suc n) ⟹ PoW t (n' + n) < PoW t (n' + Suc n)"
                    using pow_mining_suc by simp
                qed
                interpret bg: bounded_growth "length sbc" "λn. PoW t (n' + n)" "devLgthBC t ⟨nid ← t⟩⇘n⇙ nid' n'" "λn. hmining t (n' + n)" "λn. dmining t (n' + n)" "length sbc" cb
                proof
                  from assms(3) ‹n'≥n⇩s› show "length sbc + cb ≤ PoW t (n' + 0)" using pow_mono[of n⇩s n' t] by simp
                next
                  from ‹length (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' 0) < length sbc› show "length (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' 0) < length sbc" .
                next
                  fix n'' n'''
                  assume "cb < card {i. n'' < i ∧ i ≤ n''' ∧ dmining t (n' + i)}"
                  hence "cb < card {i. n'' + n' < i ∧ i ≤ n''' + n' ∧ dmining t i}"
                    using cardshift[of n'' n''' "dmining t" n'] by simp
                  with fair[of "n'' + n'" "n''' + n'" t]
                  have "cb < card {i. n'' + n' < i ∧ i ≤ n''' + n' ∧ hmining t i}" by simp
                  thus "cb < card {i. n'' < i ∧ i ≤ n''' ∧ hmining t (n' + i)}"
                    using cardshift[of n'' n''' "hmining t" n'] by simp
                qed
                from ‹⟨nid ← t⟩⇘n⇙≥n'› have "length (devExt t ⟨nid ← t⟩⇘n⇙ nid' n' (⟨nid ← t⟩⇘n⇙-n')) < PoW t ⟨nid ← t⟩⇘n⇙"
                  using bg.hn_upper_bound[of "⟨nid ← t⟩⇘n⇙-n'"] by simp
                moreover from ‹∥nid'∥⇘t ⟨nid ← t⟩⇘n⇙⇙› ‹⟨nid ← t⟩⇘n⇙≥n'›
                  have "bc (σ⇘the (devBC t ⟨nid ← t⟩⇘n⇙ nid' ⟨nid ← t⟩⇘n⇙)⇙t ⟨nid ← t⟩⇘n⇙) = devExt t ⟨nid ← t⟩⇘n⇙ nid' n' (⟨nid ← t⟩⇘n⇙-n')"
                  using devExt_bc_geq[of t "⟨nid ← t⟩⇘n⇙" nid' "⟨nid ← t⟩⇘n⇙" n'] by simp
                ultimately have "length (bc (σ⇘nid'⇙(t ⟨nid ← t⟩⇘n⇙))) < PoW t ⟨nid ← t⟩⇘n⇙"
                  using ‹∥nid'∥⇘t ⟨nid ← t⟩⇘n⇙⇙› by simp
                moreover have "PoW t ⟨nid ← t⟩⇘n⇙ ≤ length (bc (σ⇘nid'⇙(t ⟨nid ← t⟩⇘n⇙)))" (is "?lhs ≤ ?rhs")
                proof -
                  from ‹honest nid› ‹∥nid∥⇘t ⟨nid ← t⟩⇘n⇙⇙›
                    have "?lhs ≤ length (MAX (pin (σ⇘nid⇙t ⟨nid ← t⟩⇘n⇙)))" using pow_le_max by simp
                  also from ‹bc (σ⇘nid'⇙(t ⟨nid ← t⟩⇘n⇙)) = MAX (pin (σ⇘nid⇙t ⟨nid ← t⟩⇘n⇙))›
                    have "… = length (bc (σ⇘nid'⇙(t ⟨nid ← t⟩⇘n⇙)))" by simp
                  finally show ?thesis .
                qed
                ultimately show False by simp
              qed
            qed
            moreover from ‹∥nid∥⇘t n⇙› have "⟨nid → t⟩⇘n⇙=n" using nxtAct_active by simp
            ultimately show ?thesis by auto
          qed
          moreover from ‹∥nid∥⇘t n⇙› have "⟨nid → t⟩⇘n⇙=n" using nxtAct_active by simp
          ultimately show ?thesis by auto
        next
          assume "¬ (∃b∈pin (σ⇘nid⇙t ⟨nid ← t⟩⇘n⇙). length b > length (bc (σ⇘nid⇙t ⟨nid ← t⟩⇘n⇙)))"
          moreover from ‹∥nid∥⇘t n⇙› have "∃n'≥n. ∥nid∥⇘t n'⇙" by auto
          moreover from lAct have "∃n'. latestAct_cond nid t n n'" by auto
          ultimately have "¬ mining (σ⇘nid⇙t ⟨nid → t⟩⇘n⇙) ∧ bc (σ⇘nid⇙t ⟨nid → t⟩⇘n⇙) = bc (σ⇘nid⇙t ⟨nid ← t⟩⇘n⇙) ∨
            mining (σ⇘nid⇙t ⟨nid → t⟩⇘n⇙) ∧ (∃b. bc (σ⇘nid⇙t ⟨nid → t⟩⇘n⇙) = bc (σ⇘nid⇙t ⟨nid ← t⟩⇘n⇙) @ [b])"
            using ‹honest nid› bhv_hn_in[of nid n t] by simp
          moreover have "prefix sbc (bc (σ⇘nid⇙t ⟨nid ← t⟩⇘n⇙))"
          proof -
            from ‹∃n'. latestAct_cond nid t n n'› have "⟨nid ← t⟩⇘n⇙ < n" using latestAct_prop(2) by simp
            moreover from lAct have "⟨nid ← t⟩⇘n⇙ ≥ n⇩s" using latestActless by blast
            moreover from ‹∃n'. latestAct_cond nid t n n'› have "∥nid∥⇘t ⟨nid ← t⟩⇘n⇙⇙"
              using latestAct_prop(1) by simp
            with ‹honest nid› have "nid ∈ actHn (t ⟨nid ← t⟩⇘n⇙)" using actHn_def by simp
            ultimately show ?thesis using step.IH by auto
          qed
          moreover from ‹∥nid∥⇘t n⇙› have "⟨nid → t⟩⇘n⇙=n" using nxtAct_active by simp
          ultimately show ?thesis by auto
        qed
      next
        assume nAct: "¬ (∃n' < n. n' ≥ n⇩s ∧ ∥nid∥⇘t n'⇙)"
        moreover from step.hyps have "n⇩s ≤ n" by simp
        ultimately have "⟨nid → t⟩⇘n⇩s⇙ = n" using ‹∥nid∥⇘t n⇙› nxtAct_eq[of n⇩s n nid t] by simp
        with ‹honest nid› show ?thesis using assms(1) by auto
      qed
    qed
  qed
  with assms(5) show ?thesis by simp
qed

end

end