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"           (‹(‹indent=3 notation=‹binder MAX››MAX _./ _)› [0, 10] 10)
  "_MAX"      :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b"  (‹(‹indent=3 notation=‹binder MAX››MAX _∈_./ _)› [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 ‹