Quelle  FLPTheorem.thy

section ‹FLPTheorem›

text ‹
 \file{FLPTheorem} combines the results of \file{FLPSystem} with the concept
 of fair infinite executions and culminates in showing the impossibility
 of a consensus algorithm in the proposed setting.
 ›

theory FLPTheorem
imports Execution FLPSystem
begin

locale flpPseudoConsensus =
  flpSystem trans sends start
for
  trans :: "'p ==> 's ==> 'v messageValue ==>'s" and
  sends :: "'p ==> 's ==> 'v messageValue ==> ('p, 'v) message multiset" and
  start :: "'p ==> 's" +
assumes
  Agreement: "∧ i c . agreementInit i c" and
  PseudoTermination: "∧cc Q . terminationPseudo 1 cc Q"
begin

subsection ‹Obtaining non-uniform executions›

text ‹
 Executions which end with a \isb{nonUniform} configuration can be expanded
 to a strictly longer execution consuming a particular message.

 This lemma connects the previous results to the world of executions,
 thereby paving the way to the final contradiction. It covers a big part of
 the original proof of the theorem, i.e.\ finding the expansion to a longer
 execution where the decision for both values is still possible.
 \voelzer{constructing executions using Lemma 2}
 ›
lemma NonUniformExecutionsConstructable:
fixes
  exec :: "('p, 'v, 's ) configuration list " and
  trace :: "('p, 'v) message list" and 
  msg :: "('p, 'v) message" and
  p :: 'p  
assumes
  MsgEnabled: "enabled (last exec) msg" and
  PisReceiverOf: "isReceiverOf p msg" and
  ExecIsExecution: "execution trans sends start exec trace" and
  NonUniformLexec: "nonUniform (last exec)" and
  Agree: "∧ cfg . reachable (last exec) cfg ⟶ agreement cfg"
shows
  "∃ exec' trace' . (execution trans sends start exec' trace')
    ∧ nonUniform (last exec')
    ∧ prefixList exec exec' ∧ prefixList trace trace'
    ∧ (∀ cfg . reachable (last exec') cfg ⟶ agreement cfg)
    ∧ stepReachable (last exec) msg (last exec')
    ∧ (msg ∈ set (drop (length trace) trace'))"
proof -
  from NonUniformCanReachSilentBivalence[OF NonUniformLexec PseudoTermination Agree]
    obtain c' where C':
      "reachable (last exec) c'" 
      "val[p,c'] = {True, False}"
    by blast
  show ?thesis 
  proof (cases "stepReachable (last exec) msg c'")
    case True
    hence IsStepReachable: "stepReachable (last exec) msg c'" by simp
    hence "∃ exec' trace'. (execution trans sends start exec' trace')
      ∧ prefixList exec exec'
      ∧ prefixList trace trace' ∧ (last exec') = c'
      ∧ msg ∈ set (drop (length trace) trace')" 
      using ExecIsExecution expandExecution
      by auto
    then obtain exec' trace' where NewExec: 
      "(execution trans sends start exec' trace')" 
      "prefixList exec exec'" "(last exec') = c'" "prefixList trace trace'" 
      "msg ∈ set (drop (length trace) trace')" by blast
    hence lastExecExec'Reachable: "reachable (last exec) (last exec')" 
      using C'(1) by simp
    hence InitReachLastExec':  "initReachable (last exec')" 
      using NonUniformLexec 
      by (metis ReachableTrans initReachable_def)
    hence nonUniformC': "nonUniform (last exec')" using C'(2) NewExec(3) 
      by (auto simp add: vUniform_def)
    hence isAgreementPreventing: 
      "(∀ cfg . reachable (last exec') cfg ⟶ agreement cfg)"
      using lastExecExec'Reachable Agree by (metis ReachableTrans)
    with NewExec nonUniformC' IsStepReachable show ?thesis by auto
  next
    case False
    hence NotStepReachable: "¬ (stepReachable (last exec) msg c')" by simp
    from C'(1) obtain exec' trace' where NewExec: 
      "execution trans sends start exec' trace'"
      "(prefixList exec exec' ∧ prefixList trace trace')
      ∨ (exec = exec' ∧ trace = trace')"
      "last exec' = c'"
      using ExecIsExecution expandExecutionReachable by blast
    have lastExecExec'Reachable: "reachable (last exec) (last exec')" 
      using C'(1) NewExec(3) by simp
    with NonUniformLexec have InitReachLastExec': 
      "initReachable (last exec')" 
      by (metis ReachableTrans initReachable_def)
    with C'(2) NewExec(3) have nonUniformC': "nonUniform (last exec')" 
      by (auto simp add: vUniform_def)
    show "∃ exec1 trace1 . (execution trans sends start exec1 trace1)
      ∧ nonUniform (last exec1)
      ∧ prefixList exec exec1 ∧ prefixList trace trace1
      ∧ (∀ cfg . reachable (last exec1) cfg ⟶ agreement cfg)
      ∧ stepReachable (last exec) msg (last exec1)
      ∧ (msg ∈ set (drop (length trace) trace1))"
    proof (cases "enabled (last exec') msg") 
      case True
      hence EnabledMsg: "enabled (last exec') msg" by auto
      hence "∃ cMsg . ((last exec') ⊨ msg ↦ cMsg )"  
      proof (cases msg)
        case (InMsg p' b)
        with PisReceiverOf have MsgIsInMsg: "(msg = <p, inM b>)" by auto
        define cfgInM where "cfgInM = (states = λproc. (
        if proc = p then
          trans p (states (last exec') p) (Bool b)
        else states (last exec') proc),
        msgs = (((sends p (states (last exec') p) (Bool b))
              ∪# (msgs (last exec')-# msg)))) "
          with UniqueReceiverOf MsgIsInMsg EnabledMsg have 
          "((last exec') ⊨ msg ↦ cfgInM)" by auto
        thus "∃ cMsg . ((last exec') ⊨ msg ↦ cMsg )" by blast
      next 
        case (OutMsg b)
        thus "∃ cMsg . ((last exec') ⊨ msg ↦ cMsg )" using PisReceiverOf 
          by auto
      next 
        case (Msg p' v')
        with PisReceiverOf have MsgIsVMsg: "(msg = <p, v'>)" by auto
        define cfgVMsg where "cfgVMsg =
          (states = λproc. (
              if proc = p then
               trans p (states (last exec') p) (Value v')
               else states (last exec') proc),
            msgs = (((sends p (states (last exec') p) (Value v'))
                ∪# (msgs (last exec') -# msg )))) "
        with UniqueReceiverOf MsgIsVMsg EnabledMsg noInSends have 
          "((last exec') ⊨ msg ↦ cfgVMsg)" by auto 
        thus "∃ cMsg . ((last exec') ⊨ msg ↦ cMsg )" by blast
      qed  
      then obtain cMsg where  CMsg:"((last exec') ⊨ msg ↦ cMsg )" by auto
      define execMsg where "execMsg = exec' @ [cMsg]"
      define traceMsg where "traceMsg = trace' @ [msg]"
      from NewExec(1) CMsg obtain execMsg traceMsg where isExecution: 
        "execution trans sends start execMsg traceMsg"
        and ExecMsg: "prefixList exec' execMsg" "prefixList trace' traceMsg"
        "last execMsg = cMsg" "last traceMsg = msg" 
        using expandExecutionStep by blast
      have isPrefixListExec: "prefixList exec execMsg" 
        using PrefixListTransitive NewExec(2) ExecMsg(1) by auto 
      have isPrefixListTrace: "prefixList trace traceMsg" 
        using PrefixListTransitive NewExec(2) ExecMsg(2) by auto
      have cMsgLastReachable: "reachable cMsg (last execMsg)" 
        by (auto simp add: ExecMsg reachable.init) 
      hence isStepReachable: "stepReachable (last exec) msg (last execMsg)" 
        using CMsg lastExecExec'Reachable   
        by (auto simp add: stepReachable_def) 
      have InitReachLastExecMsg: "initReachable (last execMsg)" 
        using CMsg InitReachLastExec' cMsgLastReachable 
        by (metis ReachableTrans initReachable_def step) 
      have "val[p, (last exec')] ⊆ val[p, cMsg]" 
        using CMsg PisReceiverOf InitReachLastExec'
          ActiveProcessSilentDecisionValuesIncrease[of p p "last exec'" msg cMsg]
        by auto
      with ExecMsg C'(2) NewExec(3) have 
        "val[p, (last execMsg)] = {True, False}" by auto
      with InitReachLastExecMsg have isNonUniform: 
        "nonUniform (last execMsg)" by (auto simp add: vUniform_def)
      have "reachable (last exec) (last execMsg)" 
        using lastExecExec'Reachable cMsgLastReachable CMsg 
        by (metis ReachableTrans step)
      hence isAgreementPreventing: 
        "(∀ cfg . reachable (last execMsg) cfg ⟶ agreement cfg)" 
        using Agree by (metis ReachableTrans)
      have "msg ∈ set (drop (length trace) traceMsg)" using ExecMsg(4) 
        isPrefixListTrace 
        by (metis (full_types) PrefixListMonotonicity last_drop last_in_set
          length_0_conv length_drop less_zeroE zero_less_diff)
      thus ?thesis using isExecution isNonUniform isPrefixListExec 
        isPrefixListTrace isAgreementPreventing isStepReachable by blast
    next
      case False
      hence notEnabled: "¬ (enabled (last exec') msg)" by auto
      have isStepReachable: "stepReachable (last exec) msg (last exec')" 
        using MsgEnabled notEnabled lastExecExec'Reachable StepReachable 
          by auto
        with NotStepReachable NewExec(3) show ?thesis by simp
    qed 
  qed 
qed

lemma NonUniformExecutionBase:
fixes
  cfg
assumes
  Cfg: "initial cfg" "nonUniform cfg"
shows 
  "execution trans sends start [cfg] []
  ∧ nonUniform (last [cfg])
  ∧ (∃ cfgList' msgList'. nonUniform (last cfgList')
    ∧ prefixList [cfg] cfgList'
    ∧ prefixList [] msgList'
    ∧ (execution trans sends start cfgList' msgList')
     ∧ (∃ msg'. execution.minimalEnabled [cfg] [] msg'
         ∧ msg' ∈ set msgList'))"
proof -
  have NonUniListCfg: "nonUniform (last [cfg])" using Cfg(2) by auto
  have AgreeCfg': "∀ cfg' .
    reachable (last [cfg]) cfg' ⟶ agreement cfg'" 
    using Agreement Cfg(1) 
    by (auto simp add: agreementInit_def reachable.init agreement_def)
  have StartExec: "execution trans sends start [cfg] []" 
    using Cfg(1) by (unfold_locales, auto)
  hence "∃ msg . execution.minimalEnabled [cfg] [] msg" 
    using Cfg execution.ExistImpliesMinEnabled
    by (metis enabled_def initial_def isReceiverOf.simps(1) 
       last.simps zero_less_one)
  then obtain msg where MinEnabledMsg: 
    "execution.minimalEnabled [cfg] [] msg" by blast
  hence "∃ pMin . isReceiverOf pMin msg" using StartExec 
    by (auto simp add: execution.minimalEnabled_def)
  then obtain pMin where PMin: "isReceiverOf pMin msg" by blast
  hence "enabled (last [cfg]) msg ∧ isReceiverOf pMin msg" 
    using MinEnabledMsg StartExec 
    by (auto simp add: execution.minimalEnabled_def)
  hence Enabled: "enabled (last [cfg]) msg" "isReceiverOf pMin msg" 
    by auto
  from Enabled StartExec NonUniListCfg PseudoTermination AgreeCfg' 
  have "∃ exec' trace' . (execution trans sends start exec' trace')
    ∧ nonUniform (last exec')
    ∧ prefixList [cfg] exec' ∧ prefixList [] trace'
    ∧ (∀ cfg' . reachable (last exec') cfg' ⟶ agreement cfg')
    ∧ stepReachable (last [cfg]) msg (last exec')
    ∧ (msg ∈ set (drop (length []) trace'))" 
  using NonUniformExecutionsConstructable[of "[cfg]" "msg" "pMin"
          "[]::('p,'v) message list"] 
    by simp
  with StartExec NonUniListCfg MinEnabledMsg show ?thesis by auto
qed

lemma NonUniformExecutionStep:
fixes
 cfgList msgList
assumes
  Init: "initial (hd cfgList)" and
  NonUni: "nonUniform (last cfgList)" and
  Execution: "execution trans sends start cfgList msgList"
shows
  "(∃ cfgList' msgList' .
      nonUniform (last cfgList')
      ∧ prefixList cfgList cfgList'
      ∧ prefixList msgList msgList'
      ∧ (execution trans sends start cfgList' msgList')
      ∧ (initial (hd cfgList'))
      ∧ (∃ msg'. execution.minimalEnabled cfgList msgList msg'
        ∧ msg' ∈ (set (drop (length msgList ) msgList')) ))"
proof -
  have ReachImplAgree: "∀ cfg . reachable (last cfgList) cfg
    ⟶ agreement cfg"
    using Agreement Init NonUni ReachableTrans
    unfolding agreementInit_def agreement_def initReachable_def
    by (metis (full_types))
  have "∃ msg p. enabled (last cfgList) msg ∧ isReceiverOf p msg" 
  proof -
    from PseudoTermination NonUni have 
      "∃c'. qReachable (last cfgList) Proc c' ∧ decided c'" 
      using terminationPseudo_def by auto
      then obtain c' where C': "reachable (last cfgList) c'" 
        "decided c'" 
        using QReachImplReach by blast 
    have NoOut: 
      "0 = msgs (last cfgList) <⊥, outM False>"  
      "0 = msgs (last cfgList) <⊥, outM True>" 
      using NonUni ReachImplAgree PseudoTermination 
      by (metis NonUniformImpliesNotDecided neq0_conv)+
    with C'(2) have "(last cfgList) ≠ c'" 
      by (metis (full_types) less_zeroE)
    thus ?thesis using C'(1) ReachableStepFirst by blast
  qed
  then obtain msg p where Enabled: 
    "enabled (last cfgList) msg" "isReceiverOf p msg" by blast
  hence "∃ msg . execution.minimalEnabled cfgList msgList msg" 
    using Init execution.ExistImpliesMinEnabled[OF Execution] by auto        
  then obtain msg' where MinEnabledMsg: 
    "execution.minimalEnabled cfgList msgList msg'" by blast
  hence "∃ p' . isReceiverOf p' msg'"
    using Execution
    by (auto simp add: execution.minimalEnabled_def)
  then obtain p' where
    P': "isReceiverOf p' msg'" by blast
  hence Enabled':
    "enabled (last cfgList) msg'" "isReceiverOf p' msg'" 
    using MinEnabledMsg Execution
    by (auto simp add: execution.minimalEnabled_def)     
  have "∃ exec' trace' . (execution trans sends start exec' trace')
    ∧ nonUniform (last exec')
    ∧ prefixList cfgList exec' ∧ prefixList msgList trace'
    ∧ (∀ cfg . reachable (last exec') cfg ⟶ agreement cfg)
    ∧ stepReachable (last cfgList) msg' (last exec')
    ∧ (msg' ∈ set (drop (length msgList) trace')) "
    using NonUniformExecutionsConstructable[OF Enabled' Execution
          NonUni] ReachImplAgree by auto
  thus ?thesis
    using MinEnabledMsg by (metis execution.base)
qed

subsection ‹Non-uniformity even when demanding fairness›

text ‹
 Using \isb{NonUniformExecutionBase} and \isb{NonUniformExecutionStep} one can obtain
 non-uniform executions which are fair.

 Proving the fairness turned out quite cumbersome.
 ›

text ‹
 These two functions construct infinite series of configurations lists
 and message lists from two extension functions.
 ›
fun infiniteExecutionCfg ::
  "('p, 'v, 's) configuration ==>
   (('p, 'v, 's) configuration list ==> ('p, 'v) message list
    ==> ('p, 'v, 's) configuration list) ==>
   (('p, 'v, 's) configuration list ==> ('p, 'v) message list
    ==>('p, 'v) message list)
  ==> nat
  ==> (('p, 'v, 's) configuration list)"
and  infiniteExecutionMsg ::
  "('p, 'v, 's) configuration ==>
   (('p, 'v, 's) configuration list ==> ('p, 'v) message list
    ==> ('p, 'v, 's) configuration list) ==>
   (('p, 'v, 's) configuration list ==> ('p, 'v) message list
    ==>('p, 'v) message list)
  ==> nat
  ==> ('p, 'v) message list"
where
  "infiniteExecutionCfg cfg fStepCfg fStepMsg 0 = [cfg]"
| "infiniteExecutionCfg cfg fStepCfg fStepMsg (Suc n) =
    fStepCfg (infiniteExecutionCfg cfg fStepCfg fStepMsg n)
             (infiniteExecutionMsg cfg fStepCfg fStepMsg n)"
| "infiniteExecutionMsg cfg fStepCfg fStepMsg 0 = []"
| "infiniteExecutionMsg cfg fStepCfg fStepMsg (Suc n) =
    fStepMsg (infiniteExecutionCfg cfg fStepCfg fStepMsg n)
             (infiniteExecutionMsg cfg fStepCfg fStepMsg n)"

lemma FairNonUniformExecution:
fixes
  cfg
assumes
  Cfg: "initial cfg" "nonUniform cfg"
shows "∃ fe ft.
  (fe 0) = [cfg]
  ∧ fairInfiniteExecution fe ft
  ∧ (∀ n . nonUniform (last (fe n))
       ∧ prefixList (fe n) (fe (n+1))
       ∧ prefixList (ft n) (ft (n+1))
       ∧ (execution trans sends start (fe n) (ft n)))"
proof -
  have BC: 
    "execution trans sends start [cfg] []
    ∧ nonUniform (last [cfg])
    ∧ (∃ cfgList' msgList'. nonUniform (last cfgList')
    ∧ prefixList [cfg] cfgList'
    ∧ prefixList [] msgList'
    ∧ (execution trans sends start cfgList' msgList')
    ∧ (∃ msg'. execution.minimalEnabled [cfg] [] msg'
       ∧ msg' ∈ set msgList'))"
    using NonUniformExecutionBase[OF assms] .
  ― ‹fStep ... a step leading to a fair execution.›
  obtain fStepCfg fStepMsg where FStep: "∀ cfgList msgList . ∃cfgList' msgList' .
          fStepCfg cfgList msgList = cfgList' ∧
          fStepMsg cfgList msgList = msgList' ∧
          (initial (hd cfgList) ∧
          nonUniform (last cfgList) ∧
          execution trans sends start cfgList msgList ⟶
          (nonUniform (last (fStepCfg cfgList msgList))
          ∧ prefixList cfgList (fStepCfg cfgList msgList)
          ∧ prefixList msgList (fStepMsg cfgList msgList)
          ∧ execution trans sends start (fStepCfg cfgList msgList)
              (fStepMsg cfgList msgList)
          ∧ (initial (hd (fStepCfg cfgList msgList)))
          ∧ (∃ msg'. execution.minimalEnabled cfgList msgList msg'
            ∧ msg' ∈ (set (drop (length msgList)
                                (fStepMsg cfgList msgList))))))"
   using NonUniformExecutionStep
      PredicatePairFunctions2[of 
        "λ cfgList msgList cfgList' msgList'.
          (initial (hd cfgList)
          ∧ nonUniform (last cfgList)
          ∧ execution trans sends start cfgList msgList
            ⟶ (nonUniform (last cfgList')
            ∧ prefixList cfgList cfgList'
            ∧ prefixList msgList msgList'
            ∧ execution trans sends start cfgList' msgList'
            ∧ (initial (hd cfgList'))
            ∧ (∃ msg'. execution.minimalEnabled cfgList msgList msg'
              ∧ msg' ∈ (set (drop (length msgList ) msgList')))))" "False"] by auto
  define fe ft
    where "fe = infiniteExecutionCfg cfg fStepCfg fStepMsg"
      and "ft = infiniteExecutionMsg cfg fStepCfg fStepMsg"
  
  have BasicProperties: "(∀n. nonUniform (last (fe n))
    ∧ prefixList (fe n) (fe (n + 1)) ∧ prefixList (ft n) (ft (n + 1))
    ∧ execution trans sends start (fe n) (ft n)
    ∧ initial (hd (fe (n + 1))))"
  proof (clarify)
    fix n
    show "nonUniform (last (fe n)) ∧
          prefixList (fe n) (fe (n + (1::nat)))
          ∧ prefixList (ft n) (ft (n + (1::nat)))
          ∧ execution trans sends start (fe n) (ft n)
          ∧ initial (hd (fe (n + 1)))"
    proof(induct n)
      case 0
      hence "fe 0 = [cfg]" "ft 0 = []" "fe 1 = fStepCfg (fe 0) (ft 0)" 
        "ft 1 = fStepMsg (fe 0) (ft 0)"
        using fe_def ft_def
        by simp_all
      thus ?case
        using BC FStep
        by (simp, metis execution.base)
    next
      case (Suc n)
        thus ?case
        using fe_def ft_def
        by (auto, (metis FStep execution.base)+)
    qed
  qed
  have Fair: "fairInfiniteExecution fe ft" 
    using BasicProperties
    unfolding fairInfiniteExecution_def infiniteExecution_def 
      execution_def flpSystem_def
  proof(auto simp add: finiteProcs minimalProcs finiteSends noInSends) 
    fix n n0 p msg
    assume AssumptionFair: "∀n. initReachable (last (fe n)) ∧
       ¬ vUniform False (last (fe n)) ∧
       ¬ vUniform True (last (fe n)) ∧
       prefixList (fe n) (fe (Suc n)) ∧
       prefixList (ft n) (ft (Suc n)) ∧
       Suc 0 ≤ length (fe n) ∧
       length (fe n) - Suc 0 = length (ft n) ∧
       initial (hd (fe n)) ∧
       (∀i<length (fe n) - Suc 0. ((fe n ! i) ⊨ (ft n ! i)
       ↦ (fe n ! Suc i))) ∧ initial (hd (fe (Suc n)))"
      "n0 < length (fe n)"
      "enabled (fe n ! n0) msg" 
      "isReceiverOf p msg" 
      "correctInfinite fe ft p"
    have MessageStaysOrConsumed: "∧ n n1 n2 msg.
      (n1 ≤ n2 ∧ n2 < length (fe n) ∧ (enabled (fe n ! n1) msg))
      ⟶ (enabled (fe n ! n2) msg)
          ∨ (∃ n0' ≥ n1. n0' < length (ft n) ∧ ft n ! n0' = msg)"
    proof(auto)
      fix n n1 n2 msg
      assume Ass: "n1 ≤ n2" "n2 < length (fe n)" "enabled (fe n ! n1) msg"
        "∀index<length (ft n). n1 ≤ index ⟶ ft n ! index ≠ msg"
      have "∀ k ≤ n2 - n1 .
        msgs (fe n ! n1) msg ≤ msgs (fe n ! (n1 + k)) msg" 
      proof(auto)
        fix k
        show "k ≤ n2 - n1 ==>
          msgs (fe n ! n1) msg ≤ msgs (fe n ! (n1 + k)) msg"
        proof(induct k, auto)
          fix k
          assume IV: "msgs (fe n ! n1) msg ≤ msgs (fe n ! (n1 + k)) msg" 
            "Suc k ≤ n2 - n1"
          from BasicProperties have Exec: 
            "execution trans sends start (fe n) (ft n)" by blast
          have "n2 ≤ length (ft n)"
            using Exec Ass(2)
            execution.length[of trans sends start "fe n" "ft n"]
            by simp
          hence RightIndex: "n1 + k ≥ n1 ∧ n1 + k < length (ft n)"
            using IV(2) by simp
          have  Step: "(fe n ! (n1 + k)) ⊨ (ft n ! (n1 + k))
                      ↦ (fe n ! Suc (n1 + k))" 
            using Exec execution.step[of trans sends start "fe n" "ft n" 
              "n1 + k" "fe n ! (n1 + k)" "fe n ! (n1 + k + 1)"] IV(2) 
              Ass(2) 
            by simp
          hence "msg ≠ (ft n ! (n1 + k))" 
            using Ass(4) Ass(2) IV(2) RightIndex Exec 
            execution.length[of trans sends start "fe n" "ft n"]
            by blast
          thus "msgs (fe n ! n1) msg ≤ msgs (fe n ! Suc (n1 + k)) msg" 
            using Step OtherMessagesOnlyGrowing[of "(fe n ! (n1 + k))" 
              "(ft n ! (n1 + k))" "(fe n ! Suc (n1 + k))" "msg"] IV(1)
            by simp
        qed
      qed
      hence "msgs (fe n ! n1) msg ≤ msgs (fe n ! n2) msg" 
        by (metis Ass(1) le_add_diff_inverse order_refl)
      thus "enabled (fe n ! n2) msg" using Ass(3) enabled_def 
        by (metis gr0I leD)
    qed
    have EnabledOrConsumed: "enabled (fe n ! (length (fe n) - 1)) msg
      ∨ (∃n0'≥n0. n0' < length (ft n) ∧ ft n ! n0' = msg)" 
      using AssumptionFair(3) AssumptionFair(2) 
        MessageStaysOrConsumed[of "n0" "length (fe n) - 1" "n" "msg"] 
      by auto
    have EnabledOrConsumedAtLast: "enabled (last (fe n)) msg ∨
      (∃ n0' . n0' ≥ n0 ∧ n0' < length (ft n) ∧ (ft n) ! n0' = msg )"
      using EnabledOrConsumed last_conv_nth AssumptionFair(2) 
      by (metis length_0_conv less_nat_zero_code)
    have Case2ImplThesis: "(∃ n0' . n0' ≥ n0 ∧ n0' < length (ft n)
      ∧ ft n ! n0' = msg)
      ==> (∃n'≥n. ∃n0'≥n0. n0' < length (ft n') ∧ msg = ft n' ! n0')"
      by auto
    have Case1ImplThesis': "enabled (last (fe n)) msg
      ⟶ (∃n'≥n. ∃n0'≥ (length (ft n)). n0' < length (ft n')
          ∧ msg = ft n' ! n0')" 
    proof(clarify)
      assume AssumptionCase1ImplThesis': "enabled (last (fe n)) msg"
      show "∃n'≥n. ∃n0'≥length (ft n). n0' < length (ft n')
        ∧ msg = ft n' ! n0'" 
      proof(rule ccontr,simp)
        assume AssumptionFairContr: "∀n'≥n. ∀n0'<length (ft n').
          length (ft n) ≤ n0' ⟶ msg ≠ ft n' ! n0'"
        define firstOccSet where "firstOccSet n = { msg1 . ∃ nMsg .
          ∃ n1 ≤ nMsg .
          execution.firstOccurrence (fe n) (ft n) msg1 n1
          ∧ execution.firstOccurrence (fe n) (ft n) msg nMsg }" for n
        have NotEmpty: "fe n ≠ []" using  AssumptionFair(2) 
          by (metis less_nat_zero_code list.size(3))
        have FirstToLast': 
          "∀ n . reachable ((fe n) ! 0) ((fe n) ! (length (fe n) - 1))"
          using execution.ReachableInExecution BasicProperties execution.notEmpty
          by (metis diff_less less_or_eq_imp_le not_gr0 not_one_le_zero)
        hence FirstToLast: "∀ n . reachable (hd (fe n)) (last (fe n))" 
          using NotEmpty hd_conv_nth last_conv_nth AssumptionFair(1) 
          by (metis (full_types) One_nat_def length_0_conv 
            not_one_le_zero)
        hence InitToLast: "∀ n . initReachable (last (fe n))" 
          using BasicProperties by auto
        have "∧ msg n0 . ∀ n .
          (execution.firstOccurrence (fe n) (ft n) msg n0)
          ⟶ 0 < msgs (last (fe n)) msg"
          using BasicProperties execution.firstOccurrence_def 
            enabled_def
          by metis
        hence "∀ n . ∀ msg' ∈ (firstOccSet n) .
          0 < msgs (last (fe n)) msg'" using firstOccSet_def by blast
        hence "∀ n . firstOccSet n ⊆ {msg. 0 < msgs (last (fe n)) msg}"
          by (metis (lifting, full_types) mem_Collect_eq subsetI)
        hence FiniteMsgs: "∀ n . finite (firstOccSet n)" 
          using FiniteMessages[OF finiteProcs finiteSends] InitToLast
          by (metis rev_finite_subset)
        have FirstOccSetDecrOrConsumed: "∀ index .
          (enabled (last (fe index)) msg)
          ⟶ (firstOccSet (Suc index) ⊂ firstOccSet index
          ∧ (enabled (last (fe (Suc index))) msg)
            ∨ msg ∈ (set (drop (length (ft index)) (ft (Suc index)))))"
        proof(clarify)
          fix index
          assume AssumptionFirstOccSetDecrOrConsumed:
            "enabled (last (fe index)) msg" 
            "msg ∉ set (drop (length (ft index)) (ft (Suc index)))"
          have NotEmpty: "fe (Suc index) ≠ []" "fe index ≠ []" 
            using BasicProperties 
            by (metis AssumptionFair(1) One_nat_def list.size(3) 
              not_one_le_zero)+
          have LengthStep: "length (ft (Suc index)) > length (ft index)"
            using AssumptionFair(1) 
            by (metis PrefixListMonotonicity)              
          have IPrefixList:
            "∀ i::nat . prefixList (ft i) (ft (Suc i))" 
            using AssumptionFair(1) by auto
          have IPrefixListEx:
            "∀ i::nat . prefixList (fe i) (fe (Suc i))" 
            using AssumptionFair(1) by auto
          have LastOfIndex:
            "(fe (Suc index) ! (length (fe index) - Suc 0))
            = (last (fe index))"
            using PrefixSameOnLow[of "fe index" "fe (Suc index)"]
              IPrefixListEx[rule_format, of index]
              NotEmpty LengthStep 
            by (auto simp add: last_conv_nth)
          have NotConsumedIntermediate: 
            "∀ i::nat < length (ft (Suc index)) .
              (i ≥ length (ft index)
              ⟶ ft (Suc index) ! i ≠ msg)" 
            using AssumptionFirstOccSetDecrOrConsumed(2) ListLenDrop 
            by auto
          hence 
            "¬(∃i. i < length (ft (Suc index)) ∧ i ≥ length (ft index)
            ∧ msg = (ft (Suc index)) ! i)" 
            using execution.length BasicProperties
            by auto
          hence "¬(∃i. i < length (fe (Suc index)) - 1
            ∧ i ≥ length (fe index) - 1
            ∧ msg = (ft (Suc index)) ! i)"
            using BasicProperties[rule_format, of "Suc index"]
              BasicProperties[rule_format, of "index"]
              execution.length[of trans sends start]
            by auto
          hence EnabledIntermediate: 
            "∀ i < length (fe (Suc index)) . (i ≥ length (fe index) - 1
              ⟶ enabled (fe (Suc index) ! i) msg)" 
            using BasicProperties[rule_format, of "Suc index"]
              BasicProperties[rule_format, of "index"]
              execution.StaysEnabled[of trans sends start
              "fe (Suc index)" "ft (Suc index)" "last (fe index)" msg 
              "length (fe index) - 1 "]
              AssumptionFirstOccSetDecrOrConsumed(1)
            by (auto, metis AssumptionFair(1) LastOfIndex 
              MessageStaysOrConsumed)
          have "length (fe (Suc index)) - 1 ≥ length (fe index) - 1"
            using PrefixListMonotonicity NotEmpty BasicProperties 
            by (metis AssumptionFair(1) diff_le_mono less_imp_le)
          hence "enabled (fe (Suc index)
            ! (length (fe (Suc index)) - 1)) msg"
            using EnabledIntermediate NotEmpty(1) 
            by (metis diff_less length_greater_0_conv zero_less_one)
          hence EnabledInSuc: "enabled (last (fe (Suc index))) msg" 
            using NotEmpty last_conv_nth[of "fe (Suc index)"] by simp
          have IndexIsExec: 
            "execution trans sends start (fe index) (ft index)" 
            using BasicProperties by blast
          have SucIndexIsExec: 
            "execution trans sends start (fe (Suc index))
              (ft (Suc index))" 
            using BasicProperties by blast
          have SameCfgOnLow: "∀ i < length (fe index) . (fe index) ! i
            = (fe (Suc index)) ! i"
            using BasicProperties PrefixSameOnLow by auto
          have SameMsgOnLow: "∀ i < length (ft index) . (ft index) ! i
            = (ft (Suc index)) ! i"
            using BasicProperties PrefixSameOnLow by auto
          have SmallIndex: "∧ nMsg . execution.firstOccurrence
            (fe (Suc index)) (ft (Suc index)) msg nMsg
            ==> nMsg < length (fe index)" 
          proof(-)
            fix nMsg
            assume "execution.firstOccurrence (fe (Suc index))
              (ft (Suc index)) msg nMsg"
            hence AssumptionSubset3: 
              "∃p. isReceiverOf p msg"
                "enabled (last (fe (Suc index))) msg"
                "nMsg < length (fe (Suc index))"
                "enabled (fe (Suc index) ! nMsg) msg"
                "∀n'≥nMsg. n' < length (ft (Suc index))
                ⟶ msg ≠ ft (Suc index) ! n'"
                "nMsg ≠ 0 ⟶ ¬ enabled (fe (Suc index) ! (nMsg - 1))
                msg ∨ msg = ft (Suc index) ! (nMsg - 1)"
              using execution.firstOccurrence_def[of "trans" "sends" 
                "start" "fe (Suc index)" "ft (Suc index)" "msg" "nMsg"]
                SucIndexIsExec by auto
            show "nMsg < length (fe index)"
            proof(rule ccontr)
              assume AssumpSmallIndex: "¬ nMsg < length (fe index)"
              have "fe index ≠ []" using BasicProperties 
                AssumptionFair(1)
                by (metis One_nat_def list.size(3) not_one_le_zero)
              hence "length (fe index) > 0" 
                by (metis length_greater_0_conv)
              hence nMsgNotZero: "nMsg ≠ 0" 
                using AssumpSmallIndex by metis
              hence SucCases: "¬ enabled ((fe (Suc index)) ! (nMsg - 1))
                msg ∨ msg = (ft (Suc index)) ! (nMsg - 1)"
                using AssumptionSubset3(6) by blast
              have Cond1: "nMsg - 1 ≥ length (fe index) - 1"
                using AssumpSmallIndex by (metis diff_le_mono leI)
              hence Enabled: "enabled (fe (Suc index) ! (nMsg - 1)) msg"
                using EnabledIntermediate AssumptionSubset3(3) 
                by (metis less_imp_diff_less)
              have Cond2: "nMsg - 1 ≥ length (ft index) ∧ nMsg - 1
                < length (ft (Suc index))"
                using Cond1 execution.length[of "trans" "sends" "start"
                  "fe index" "ft index"]
                  IndexIsExec AssumptionSubset3(3) 
                  by (simp, metis AssumptionFair(1) One_nat_def Suc_diff_1 
                    Suc_eq_plus1 less_diff_conv nMsgNotZero neq0_conv)
              hence NotConsumed: "ft (Suc index) ! (nMsg - 1) ≠ msg" 
                using NotConsumedIntermediate by simp
              show False using SucCases Enabled NotConsumed
              by blast
            qed
          qed
          have Subset: "∧ msgInSet . msgInSet ∈ firstOccSet (Suc index)
            ==> msgInSet ∈ firstOccSet index" 
          unfolding firstOccSet_def
          proof(auto)
            fix msgInSet nMsg n1
            assume AssumptionSubset: "n1 ≤ nMsg"
              "execution.firstOccurrence (fe (Suc index))
                (ft (Suc index)) msgInSet n1"
              "execution.firstOccurrence (fe (Suc index))
                (ft (Suc index)) msg nMsg"
            have AssumptionSubset2: 
              "∃p. isReceiverOf p msgInSet"
                "enabled (last (fe (Suc index))) msgInSet"
                "n1 < length (fe (Suc index))"
                "enabled (fe (Suc index) ! n1) msgInSet"
                "∀n'≥n1. n' < length (ft (Suc index))
                  ⟶ msgInSet ≠ ft (Suc index) ! n'"
                "n1 ≠ 0 ⟶ ¬ enabled (fe (Suc index) ! (n1 - 1))
                  msgInSet ∨ msgInSet = ft (Suc index) ! (n1 - 1)"
              using execution.firstOccurrence_def[of "trans" "sends" 
                "start" "fe (Suc index)" "ft (Suc index)" "msgInSet" 
                "n1"] AssumptionSubset(2) SucIndexIsExec by auto 
            have AssumptionSubset3: 
              "∃p. isReceiverOf p msg"
                "enabled (last (fe (Suc index))) msg"
                "nMsg < length (fe (Suc index))"
                "enabled (fe (Suc index) ! nMsg) msg"
                "∀n'≥nMsg. n' < length (ft (Suc index))
                  ⟶ msg ≠ ft (Suc index) ! n'"
                "nMsg ≠ 0 ⟶ ¬ enabled (fe (Suc index) ! (nMsg - 1))
                  msg ∨ msg = ft (Suc index) ! (nMsg - 1)"
              using execution.firstOccurrence_def[of "trans" "sends" 
                "start" "fe (Suc index)" "ft (Suc index)" "msg" "nMsg"]
                AssumptionSubset(3) SucIndexIsExec by auto
            have ShorterTrace: "length (ft index)
                                < length (ft (Suc index))" 
              using PrefixListMonotonicity BasicProperties by auto

            have FirstOccurrenceMsg: "execution.firstOccurrence
              (fe index) (ft index) msg nMsg"
            proof-
              have Occ1: "∃ p . isReceiverOf p msg" 
                using AssumptionSubset3(1) by blast
              have Occ2: "enabled (last (fe index)) msg" 
                using AssumptionFirstOccSetDecrOrConsumed by blast

              have "(fe index) ! nMsg = (fe (Suc index)) ! nMsg"
                using SmallIndex AssumptionSubset(3) 
                  PrefixSameOnLow[of "fe index" "fe (Suc index)"] 
                  BasicProperties 
                by simp
              hence Occ4: "enabled ((fe index) ! nMsg) msg" 
                using AssumptionSubset3(4) by simp
              have OccSameMsg: "∀ n' ≥ nMsg . n' < length (ft index)
                ⟶ (ft index) ! n' = (ft (Suc index)) ! n'" 
                using PrefixSameOnLow BasicProperties by auto
              hence Occ5: "∀ n' ≥ nMsg . n' < length (ft index)
                ⟶ msg ≠ ((ft index) ! n')" 
                using AssumptionSubset3(5) ShorterTrace by simp

              have Occ6: "nMsg ≠ 0 ⟶ (¬ enabled ((fe index) !
                (nMsg - 1)) msg ∨ msg = (ft index ) ! (nMsg - 1))" 
              proof(clarify)
                assume AssumpOcc6: "0 < nMsg" "msg ≠ ft index !
                  (nMsg - 1)" "enabled (fe index ! (nMsg - 1)) msg"
                have "nMsg - (Suc 0) < length (fe index) - (Suc 0)" 
                  using SmallIndex AssumptionSubset(3) AssumpOcc6(1) 
                  by (metis Suc_le_eq diff_less_mono)
                hence SmallIndexTrace: "nMsg - 1 < length (ft index)" 
                  using IndexIsExec execution.length 
                  by (metis One_nat_def)
                have "¬ enabled (fe (Suc index) ! (nMsg - 1)) msg
                  ∨ msg = ft (Suc index) ! (nMsg - 1)"
                  using AssumptionSubset3(6) AssumpOcc6(1) by blast
                moreover have "fe (Suc index) ! (nMsg - 1)
                  = fe index ! (nMsg - 1)"
                  using SameCfgOnLow SmallIndex AssumptionSubset(3) 
                  by (metis less_imp_diff_less)
                moreover have "ft (Suc index) ! (nMsg - 1)
                  = ft index ! (nMsg - 1)"
                  using SameMsgOnLow SmallIndexTrace by metis 
                ultimately have "¬ enabled (fe index ! (nMsg - 1)) msg
                  ∨ msg = ft index ! (nMsg - 1)"
                  by simp
                thus False using AssumpOcc6 by blast
              qed

              show ?thesis using IndexIsExec Occ1 Occ2 SmallIndex 
                AssumptionSubset(3) Occ4 Occ5 Occ6
                execution.firstOccurrence_def[of "trans" "sends" "start"
                  "fe index" "ft index"]
                by simp 
            qed

            have "execution.firstOccurrence (fe index) (ft index)
              msgInSet n1" 
              using AssumptionSubset2 AssumptionSubset(1)
            proof-
              have Occ1': "∃p. isReceiverOf p msgInSet" 
                using AssumptionSubset2(1) by blast                 
              have Occ3': "n1 < length (fe index)" 
                using SmallIndex AssumptionSubset(3) AssumptionSubset(1)
                by (metis le_less_trans)
              have "(fe index) ! n1 = (fe (Suc index)) ! n1"
                using Occ3' PrefixSameOnLow[of "fe index" 
                  "fe (Suc index)"] BasicProperties by simp
              hence Occ4': "enabled (fe index ! n1) msgInSet" 
                using AssumptionSubset2(4) by simp
              have OccSameMsg': "∀ n' ≥ n1 . n' < length (ft index)
                ⟶ (ft index) ! n' = (ft (Suc index)) ! n'" 
                using PrefixSameOnLow BasicProperties by auto
              hence Occ5': "∀n' ≥ n1. n' < length (ft index)
                ⟶ msgInSet ≠ ft index ! n'" 
                using AssumptionSubset2(5) ShorterTrace by simp
              have "length (fe index) > 0" using NotEmpty(2) 
                by (metis length_greater_0_conv)
              hence "length (fe index) - 1 < length (fe index)" 
                by (metis One_nat_def diff_Suc_less)                  
              hence 
                "enabled (fe index ! (length (fe index) - 1)) msgInSet
                ∨ (∃n0'≥n1. n0' < length (ft index) ∧ ft index ! n0'
                  = msgInSet)"
                using Occ4' Occ3' MessageStaysOrConsumed[of "n1" 
                  "length (fe index) - 1" "index" "msgInSet"]
                by (metis Suc_pred' ‹0 < length (fe index)›
                  not_le not_less_eq_eq)
              hence "enabled ((fe index) ! (length (fe index) - 1))
                msgInSet" 
                using Occ5' by auto
              hence Occ2': "enabled (last (fe index)) msgInSet" 
                using last_conv_nth[of "fe index"] NotEmpty(2) by simp

              have Occ6': "n1 ≠ 0 ⟶ ¬ enabled (fe index ! (n1 - 1))
                msgInSet ∨ msgInSet = ft index ! (n1 - 1)"
              proof(clarify)
                assume AssumpOcc6': "0 < n1" "msgInSet ≠ ft index !
                  (n1 - 1)" "enabled (fe index ! (n1 - 1)) msgInSet"
                have "n1 - (Suc 0) < length (fe index) - (Suc 0)" 
                  using Occ3' AssumpOcc6'(1) 
                  by (metis Suc_le_eq diff_less_mono)
                hence SmallIndexTrace': "n1 - 1 < length (ft index)" 
                  using IndexIsExec execution.length 
                  by (metis One_nat_def)
                have "¬ enabled (fe (Suc index) ! (n1 - 1)) msgInSet
                  ∨ msgInSet = ft (Suc index) ! (n1 - 1)"
                  using AssumptionSubset2(6) AssumpOcc6'(1) by blast
                moreover have "fe (Suc index) ! (n1 - 1)
                  = fe index ! (n1 - 1)"
                  using SameCfgOnLow Occ3' by (metis less_imp_diff_less)
                moreover have "ft (Suc index) ! (n1 - 1)
                  = ft index ! (n1 - 1)"
                  using SameMsgOnLow SmallIndexTrace' by metis 
                ultimately have "¬ enabled (fe index !
                  (n1 - 1)) msgInSet ∨ msgInSet = ft index ! (n1 - 1)"
                  by simp
                thus False using AssumpOcc6' by blast
              qed

              show ?thesis using IndexIsExec Occ1' Occ2' Occ3' Occ4' 
                Occ5' Occ6'
                execution.firstOccurrence_def[of "trans" "sends" 
                  "start" "fe index" "ft index"]
                by simp  
            qed
            
            thus "∃nMsg' n1'. n1' ≤ nMsg'
              ∧ execution.firstOccurrence (fe index) (ft index)
                msgInSet n1'
              ∧ execution.firstOccurrence (fe index) (ft index)
                msg nMsg'" 
              using FirstOccurrenceMsg AssumptionSubset(1) by blast
          qed

          have ProperSubset: "∃ msg' .msg' ∈ firstOccSet index
            ∧ msg' ∉ firstOccSet (Suc index)"
          proof-               
            have "initial (hd (fe index))" using AssumptionFair(1) 
              by blast
            hence "∃msg'. execution.minimalEnabled (fe index) (ft index)
              msg' ∧ msg' ∈ set (drop (length (ft index))
                (fStepMsg (fe index) (ft index)))" 
              using FStep fe_def ft_def
                BasicProperties by simp
            then obtain consumedMsg where ConsumedMsg: 
              "execution.minimalEnabled (fe index) (ft index)
                consumedMsg"
              "consumedMsg ∈ set (drop (length (ft index))
                (fStepMsg (fe index) (ft index)))" by blast
            hence ConsumedIsInDrop:
              "consumedMsg ∈ set (drop (length (ft index)) (ft (Suc index)))"
              using fe_def ft_def FStep
                BasicProperties[rule_format, of index]
              by auto
            
            have MinImplAllBigger: "∧ msg' . execution.minimalEnabled
            (fe index) (ft index) msg'
             ⟶ (∃ OccM' . (execution.firstOccurrence (fe index)
              (ft index) msg' OccM' )
                ∧ (∀ msg . ∀ OccM . execution.firstOccurrence (fe index)
                  (ft index) msg OccM
                ⟶ OccM' ≤ OccM))" 
            proof(auto)
              fix msg'
              assume AssumpMinImplAllBigger: "execution.minimalEnabled
                (fe index) (ft index) msg'"
              have IsExecIndex: "execution trans sends start
                (fe index) (ft index)" 
                using  BasicProperties[rule_format, of index] by simp
              have "(∃ p . isReceiverOf p msg') ∧
                (enabled (last (fe index)) msg')
                ∧ (∃ n . n < length (fe index)
                  ∧ enabled ( (fe index) ! n) msg'
                  ∧ (∀ n' ≥ n . n' < length (ft index)
                  ⟶ msg' ≠ ((ft index)! n'))
                  ∧ (∀ n' msg' . ((∃ p . isReceiverOf p msg')
                    ∧ (enabled (last (fe index)) msg')
                    ∧ n' < length (ft index)
                    ∧ enabled ((fe index)! n') msg'
                    ∧ (∀ n'' ≥ n' . n'' < length (ft index)
                    ⟶ msg' ≠ ((ft index) ! n''))) ⟶ n' ≥ n))" 
              using execution.minimalEnabled_def[of trans sends start 
                "(fe index)" "(ft index)" msg'] 
                AssumpMinImplAllBigger IsExecIndex by auto
              then obtain OccM' where OccM': 
                "(∃ p . isReceiverOf p msg')" 
                "(enabled (last (fe index)) msg')"
                "OccM' < length (fe index)" 
                "enabled ( (fe index) ! OccM') msg'"  
                "(∀ n' ≥ OccM' . n' < length (ft index)
                ⟶ msg' ≠ ((ft index)! n'))"
                "(∀ n' msg' . ((∃ p . isReceiverOf p msg')
                  ∧ (enabled (last (fe index)) msg')
                  ∧ n' < length (ft index)
                  ∧ enabled ((fe index)! n') msg'
                  ∧ (∀ n'' ≥ n' . n'' < length (ft index)
                  ⟶ msg' ≠ ((ft index) ! n''))) ⟶ n' ≥ OccM')" 
                by blast                  
              have "0 < OccM' ==> enabled (fe index ! (OccM' - Suc 0)) msg'
                      ==> msg' ≠ ft index ! (OccM' - Suc 0) ==> False"
              proof(-)
                fix p
                assume AssumpContr: 
                  "0 < OccM'"
                  "enabled (fe index ! (OccM' - Suc 0)) msg'"
                  "msg' ≠ ft index ! (OccM' - Suc 0)"
                have LengthOccM': "(OccM' - 1) < length (ft index)" 
                using OccM'(3) IndexIsExec AssumpContr(1)   
                  AssumptionFair(1)
                  by (metis  One_nat_def Suc_diff_1 Suc_eq_plus1_left 
                    Suc_less_eq le_add_diff_inverse)
                have BiggerIndices: "(∀n''≥(OccM' - 1).
                  n'' < length (ft index) ⟶ msg' ≠ ft index ! n'')"
                  using OccM'(5) by (metis AssumpContr(3) One_nat_def 
                      Suc_eq_plus1 diff_Suc_1 le_SucE le_diff_conv)
                have "(∃p. isReceiverOf p msg') ∧ enabled (last
                  (fe index)) msg' ∧ (OccM' - 1) < length (ft index)
                    ∧ enabled (fe index ! (OccM' - 1)) msg'
                    ∧ (∀n''≥(OccM' - 1). n'' < length (ft index)
                      ⟶ msg' ≠ ft index ! n'')" 
                  using OccM' LengthOccM' AssumpContr BiggerIndices 
                  by simp
                hence "OccM' ≤ OccM' - 1" using OccM'(6) by blast 
                thus False using AssumpContr(1) diff_less leD zero_less_one by blast
              qed
              hence FirstOccMsg': "execution.firstOccurrence (fe index)
                  (ft index) msg' OccM'"   
                unfolding execution_def
                  execution.firstOccurrence_def[OF IsExecIndex, of msg' OccM']
                by (auto simp add: OccM'(1,2,3,4,5))
              have "∀msg OccM. execution.firstOccurrence (fe index)
                (ft index) msg OccM ⟶ OccM' ≤ OccM" 
              proof clarify
                fix msg OccM
                assume  "execution.firstOccurrence (fe index)
                  (ft index) msg OccM"
                hence AssumpOccMFirstOccurrence: 
                  "∃ p . isReceiverOf p msg" 
                  "enabled (last (fe index)) msg" 
                  "OccM < (length (fe index))"
                  "enabled ((fe index) ! OccM) msg" 
                  "(∀ n' ≥ OccM . n' < length (ft index)
                  ⟶ msg ≠ ((ft index) ! n'))"
                  "(OccM ≠ 0 ⟶ (¬ enabled ((fe index) ! (OccM - 1))
                  msg ∨ msg = (ft index)!(OccM - 1)))"
                  by (auto simp add: execution.firstOccurrence_def[of 
                      trans sends start "(fe index)" "(ft index)" 
                      msg OccM] IsExecIndex)
                hence "(∃p. isReceiverOf p msg) ∧
                  enabled (last (fe index)) msg ∧
                  enabled (fe index ! OccM) msg ∧
                  (∀n''≥ OccM. n'' < length (ft index)
                    ⟶ msg ≠ ft index ! n'')" 
                 by simp
                thus "OccM' ≤ OccM" using OccM' 
                proof(cases "OccM < length (ft index)",auto)
                  assume "¬ OccM < length (ft index)"
                  hence "OccM ≥ length (fe index) - 1" 
                    using AssumptionFair(1) by (metis One_nat_def leI)
                  hence "OccM = length (fe index) - 1"
                    using AssumpOccMFirstOccurrence(3) by simp
                  thus "OccM' ≤ OccM" using OccM'(3) by simp
                qed
              qed
              with FirstOccMsg' show "∃OccM'.
                execution.firstOccurrence (fe index) (ft index)
                  msg' OccM'
                ∧ (∀msg OccM. execution.firstOccurrence (fe index)
                  (ft index) msg OccM ⟶ OccM' ≤ OccM)" by blast
            qed

            have MinImplFirstOcc: "∧ msg' . execution.minimalEnabled
              (fe index) (ft index) msg'
              ==> msg' ∈ firstOccSet index"
            proof -
              fix msg'
              assume AssumpMinImplFirstOcc: 
                "execution.minimalEnabled (fe index) (ft index) msg'"
              then obtain OccM' where OccM': 
                "execution.firstOccurrence (fe index) (ft index)
                  msg' OccM'"
                "∀ msg . ∀ OccM . execution.firstOccurrence
                (fe index) (ft index) msg OccM
              ⟶ OccM' ≤ OccM" using MinImplAllBigger by blast
              thus "msg' ∈ firstOccSet index" using OccM' 
              proof (auto simp add: firstOccSet_def)
                have "enabled (last (fe index)) msg" 
                  using AssumptionFirstOccSetDecrOrConsumed(1) by blast
                hence "∃nMsg . execution.firstOccurrence (fe index)
                  (ft index) msg nMsg"
                  using execution.FirstOccurrenceExists IndexIsExec 
                  AssumptionFair(4) by blast
                then obtain nMsg where NMsg: "execution.firstOccurrence
                  (fe index) (ft index) msg nMsg" by blast
                hence "OccM' ≤ nMsg" using OccM' by simp
                hence "∃nMsg . OccM' ≤ nMsg ∧
                  execution.firstOccurrence (fe index) (ft index) msg'
                    OccM' ∧
                  execution.firstOccurrence (fe index) (ft index) msg
                    nMsg" 
                  using OccM'(1) NMsg by blast 
                thus "∃nMsg n1 . n1 ≤ nMsg ∧
                  execution.firstOccurrence (fe index) (ft index)
                    msg' n1 ∧
                  execution.firstOccurrence (fe index) (ft index)
                    msg nMsg" by blast
              qed
            qed
            hence ConsumedInSet: "consumedMsg ∈ firstOccSet index" 
              using ConsumedMsg by simp
            have GreaterOccurrence: "∧ nMsg n1 .
                execution.firstOccurrence (fe (Suc index))
                  (ft (Suc index)) consumedMsg n1 ∧
                execution.firstOccurrence (fe (Suc index))
                  (ft (Suc index)) msg nMsg
                ==> nMsg < n1" 
            proof(rule ccontr,auto)
              fix nMsg n1
              assume AssumpGreaterOccurrence: "¬ nMsg < n1"
                "execution.firstOccurrence (fe (Suc index))
                  (ft (Suc index)) consumedMsg n1"
                "execution.firstOccurrence (fe (Suc index))
                  (ft (Suc index)) msg nMsg" 
              have "nMsg < length (fe index)" 
                using SmallIndex AssumpGreaterOccurrence(3) by simp
              hence "n1 < length (fe index)" 
                using AssumpGreaterOccurrence(1) 
                by (metis less_trans nat_neq_iff)
              hence N1Small: "n1 ≤ length (ft index)" 
                using IndexIsExec AssumptionFair(1) 
                by (metis  One_nat_def Suc_eq_plus1 le_diff_conv2 
                  not_le not_less_eq_eq)
              have NotConsumed: "∀ i ≥ n1 . i < length (ft (Suc index))
                ⟶ consumedMsg ≠ (ft (Suc index)) ! i" 
                using execution.firstOccurrence_def[of "trans" "sends"
                  "start" "fe (Suc index)" "ft (Suc index)" 
                  "consumedMsg" "n1"]
                  AssumpGreaterOccurrence(2) SucIndexIsExec by auto
              have "∃ i ≥ length (ft index) .
                i < length (ft (Suc index))
                ∧ consumedMsg = (ft (Suc index)) ! i"
                using DropToIndex[of "consumedMsg" "length (ft index)"]
                ConsumedIsInDrop by simp
              then obtain i where IDef: "i ≥ length (ft index)"
                "i < length (ft (Suc index))" 
                "consumedMsg = (ft (Suc index)) ! i" by blast
              thus False using NotConsumed N1Small by simp
            qed
            have "consumedMsg ∉ firstOccSet (Suc index)" 
            proof(clarify)
              assume AssumpConsumedInSucSet: 
                "consumedMsg ∈ firstOccSet (Suc index)"
              hence "∃nMsg n1. n1 ≤ nMsg ∧
                  execution.firstOccurrence (fe (Suc index))
                    (ft (Suc index)) consumedMsg n1 ∧
                  execution.firstOccurrence (fe (Suc index))
                    (ft (Suc index)) msg nMsg" 
                using firstOccSet_def by blast
              thus False using GreaterOccurrence 
                by (metis less_le_trans less_not_refl3)
            qed
            thus ?thesis using ConsumedInSet by blast
          qed

          hence "firstOccSet (Suc index) ⊂ firstOccSet index" 
            using Subset by blast
          thus "firstOccSet (Suc index) ⊂ firstOccSet index
            ∧ enabled (last (fe (Suc index))) msg"
            using EnabledInSuc by blast
        qed

        have NotConsumed: "∀ index ≥ n . ¬ msg ∈
          (set (drop (length (ft index)) (ft (Suc index))))"
        proof(clarify)
          fix index
          assume AssumpMsgNotConsumed: "n ≤ index" 
            "msg ∈ set (drop (length (ft index)) (ft (Suc index)))"

          have "∃ n0' ≥ length (ft index) .
            n0' < length (ft (Suc index))
            ∧ msg = (ft (Suc index)) ! n0'" 
            using AssumpMsgNotConsumed(2) DropToIndex[of "msg" 
              "length (ft index)" "ft (Suc index)"] by auto
          then obtain n0' where MessageIndex: "n0' ≥ length (ft index)" 
            "n0' < length (ft (Suc index))" 
            "msg = (ft (Suc index)) ! n0'" by blast
          have LengthIncreasing: "length (ft n) ≤ length (ft index)" 
            using AssumpMsgNotConsumed(1) 
          proof(induct index,auto)
            fix indexa
            assume AssumpLengthIncreasing: 
              "n ≤ indexa ==> length (ft n) ≤ length (ft indexa)" 
              "n ≤ Suc indexa" "n ≤ index"
            show "length (ft n) ≤ length (ft (Suc indexa))"
            proof(cases "n = Suc indexa",auto)
              assume "n ≠ Suc indexa"
              hence "n ≤ indexa" using AssumpLengthIncreasing(2) 
                by (metis le_SucE)
              hence LengthNA: "length (ft n) ≤ length (ft indexa)" 
                using AssumpLengthIncreasing(1) by blast
              have PrefixIndexA: "prefixList (ft indexa) (ft (Suc indexa))"
                using BasicProperties by simp
              show "length (ft n) ≤ length (ft (Suc indexa))"
                using LengthNA PrefixListMonotonicity[OF PrefixIndexA]
                by (metis (opaque_lifting, no_types) antisym le_cases 
                  less_imp_le less_le_trans)
            qed
          qed
          thus False using AssumptionFairContr MessageIndex 
            AssumpMsgNotConsumed(1) 
            by (metis ‹length (ft index) ≤ n0'› le_SucI le_trans)
        qed

        hence FirstOccSetDecrImpl: 
          "∀ index ≥ n . (enabled (last (fe index)) msg)
          ⟶ firstOccSet (Suc index) ⊂ firstOccSet index
            ∧ (enabled (last (fe (Suc index))) msg)"
          using FirstOccSetDecrOrConsumed by blast
        hence FirstOccSetDecrImpl: "∀ index ≥ n . firstOccSet
          (Suc index) ⊂ firstOccSet index"
          using KeepProperty[of "n" "λx.(enabled (last (fe x)) msg)" 
            "λx.(firstOccSet (Suc x) ⊂ firstOccSet x)"]
            AssumptionCase1ImplThesis' by blast
        hence FirstOccSetDecr': "∀ index ≥ n .
          card (firstOccSet (Suc index)) < card (firstOccSet index)"
          using FiniteMsgs psubset_card_mono by metis
        hence "card (firstOccSet (n + (card (firstOccSet n) + 1)))
          ≤ card (firstOccSet n) - (card (firstOccSet n) + 1)"
          using SmallerMultipleStepsWithLimit[of "n" 
            "λx. card (firstOccSet x)" "card (firstOccSet n) + 1"]
          by blast
        hence IsNegative:"card (firstOccSet (n + (card
          (firstOccSet n) + 1))) < 0" 
          by (metis FirstOccSetDecr' diff_add_zero leD le_add1 
            less_nat_zero_code neq0_conv)
        thus False by (metis less_nat_zero_code)
      qed
    qed

    hence Case1ImplThesis: "enabled (last (fe n)) msg
      ==> (∃n'≥n. ∃n0'≥n0. n0' < length (ft n') ∧ msg = ft n' ! n0')"
      using AssumptionFair(2) execution.length[of trans sends start 
        "fe n" "ft n"] BasicProperties 
      by (metis One_nat_def Suc_eq_plus1 Suc_lessI leI le_less_trans 
        less_asym less_diff_conv)

    show "∃n'≥n. ∃n0'≥n0. n0' < length (ft n') ∧ msg = ft n' ! n0'"
    using disjE[OF EnabledOrConsumedAtLast Case1ImplThesis Case2ImplThesis] .
  qed
  show ?thesis proof (rule exI[of _ fe], rule exI[of _ ft])
    show "fe 0 = [cfg] ∧ fairInfiniteExecution fe ft
      ∧ (∀n. nonUniform (last (fe n)) ∧ prefixList (fe n) (fe (n + 1))
          ∧ prefixList (ft n) (ft (n + 1))
          ∧ execution trans sends start (fe n) (ft n))"
    using Fair fe_def FStep BasicProperties by auto
  qed
qed

subsection ‹Contradiction›

text ‹
 An infinite execution is said to be a terminating FLP execution if each process
 at some point sends a decision message or if it stops, which is expressed
 by the process not processing any further messages.
 ›
definition (in flpSystem) terminationFLP::
  "(nat ==> ('p, 'v, 's) configuration list)
  ==> (nat ==> ('p, 'v) message list) ==> bool"
where
  "terminationFLP fe ft ≡ infiniteExecution fe ft ⟶
  (∀ p . ∃ n .
     (∃ i0 < length (ft n). ∃ b .
      (<⊥, outM b> ∈# sends p (states ((fe n) ! i0) p) (unpackMessage ((ft n) ! i0)))
      ∧ isReceiverOf p ((ft n) ! i0))
  ∨ (∀ n1 > n . ∀ m ∈ set (drop (length (ft n)) (ft n1)) . ¬ isReceiverOf p m))"

theorem ConsensusFails:
assumes 
  Termination:
    "∧ fe ft . (fairInfiniteExecution fe ft ==> terminationFLP fe ft)" and
  Validity: "∀ i c . validity i c" and
  Agreement: "∀ i c . agreementInit i c"
shows
  "False"
proof -
  obtain cfg where Cfg: "initial cfg" "nonUniform cfg"
    using InitialNonUniformCfg[OF PseudoTermination Validity Agreement] 
        by blast
  obtain fe:: "nat ==> ('p, 'v, 's) configuration list" and
              ft:: "nat ==> ('p, 'v) message list"
    where FE: "(fe 0) = [cfg]" "fairInfiniteExecution fe ft"
        "(∀(n::nat) . nonUniform (last (fe n))
          ∧ prefixList (fe n) (fe (n+1))
          ∧ prefixList (ft n) (ft (n+1))
          ∧ (execution trans sends start (fe n) (ft n)))" 
    using FairNonUniformExecution[OF Cfg] 
    by blast

  have AllArePrefixesExec: "∀ m . ∀ n > m . prefixList (fe m) (fe n)"
  proof(clarify)
    fix m::nat and n::nat
    assume MLessN: "m < n"
    have "prefixList (fe m) (fe n)" using MLessN 
    proof(induct n, simp)
      fix n
      assume IA: "(m < n) ==> (prefixList (fe m) (fe n))" "m < (Suc n)"
      have "m = n ∨ m < n" using IA(2) by (metis less_SucE)
      thus "prefixList (fe m) (fe (Suc n))"
      proof(cases "m = n", auto)
        show "prefixList (fe n) (fe (Suc n))" using FE by simp
      next
        assume "m < n"
        hence IA2: "prefixList (fe m) (fe n)" using IA(1) by simp
        have "prefixList (fe n) (fe (n+1))" using FE by simp
        thus "prefixList (fe m) (fe (Suc n))" using PrefixListTransitive 
          IA2 by simp
      qed
    qed
    thus "prefixList (fe m) (fe n)" by simp
  qed

  have AllArePrefixesTrace: "∀ m . ∀ n > m . prefixList (ft m) (ft n)"
  proof(clarify)
    fix m::nat and n::nat
    assume MLessN: "m < n"
    have "prefixList (ft m) (ft n)" using MLessN
    proof(induct n, simp)
      fix n
      assume IA: "(m < n) ==> (prefixList (ft m) (ft n))" "m < (Suc n)"
      have "m = n ∨ m < n" using IA(2) by (metis less_SucE)
      thus "prefixList (ft m) (ft (Suc n))"
      proof(cases "m = n", auto)
        show "prefixList (ft n) (ft (Suc n))" using FE by simp
      next
        assume "m < n"
        hence IA2: "prefixList (ft m) (ft n)" using IA(1) by simp
        have "prefixList (ft n) (ft (n+1))" using FE by simp
        thus "prefixList (ft m) (ft (Suc n))" using PrefixListTransitive 
          IA2 by simp
      qed
    qed
    thus "prefixList (ft m) (ft n)" by simp
  qed

  have Length: "∀ n . length (fe n) ≥ n + 1" 
  proof(clarify)
    fix n
    show "length (fe n) ≥ n + 1" 
    proof(induct n, simp add: FE(1))
      fix n
      assume IH: "(n + (1::nat)) ≤ (length (fe n))"
      have "length (fe (n+1)) ≥ length (fe n) + 1" using FE(3) 
        PrefixListMonotonicity
        by (metis Suc_eq_plus1 Suc_le_eq)
      thus "(Suc n) + (1::nat) ≤ (length (fe (Suc n)))" using IH by auto
    qed
  qed

  have AllExecsFromInit: "∀ n . ∀ n0 < length (fe n) .
    reachable cfg ((fe n) ! n0)"
  proof(clarify)
    fix n::nat and n0::nat
    assume "n0 < length (fe n)"
    thus "reachable cfg ((fe n) ! n0)"
    proof(cases "0 = n", auto)
      assume N0Less: "n0 < length (fe 0)"
      have NoStep: "reachable cfg cfg" using reachable.simps by blast 
      have "length (fe 0) = 1" using FE(1) by simp
      hence N0Zero: "n0 = 0" using N0Less FE by simp
      hence "(fe 0) ! n0 = cfg" using FE(1) by simp
      thus "reachable cfg ((fe 0) ! n0)" using FE(1) NoStep N0Zero by simp
    next
      assume NNotZero: "0 < n" "n0 < (length (fe n))"
      have ZeroCfg: "(fe 0) = [cfg]" using FE by simp
      have "prefixList (fe 0) (fe n)" using AllArePrefixesExec NNotZero 
        by simp
      hence PrList: "prefixList [cfg] (fe n)" using ZeroCfg by simp
      have CfgFirst: "cfg = (fe n) ! 0"
        using prefixList.cases[OF PrList]
        by (metis (full_types) ZeroCfg list.distinct(1) nth_Cons_0)
      have "reachable ((fe n) ! 0) ((fe n) ! n0)"
        using execution.ReachableInExecution FE NNotZero(2) by (metis le0)
      thus "(reachable cfg ((fe n) ! n0))" using assms CfgFirst by simp
    qed
  qed

  have NoDecided: "(∀ n n0 v . (n0 < length (fe n))
                  ⟶ ¬ vDecided v ((fe n) ! n0))" 
  proof(clarify)
    fix n n0 v
    assume AssmNoDecided: "n0 < length (fe n)" 
      "initReachable ((fe n) ! n0)"
      "0 < (msgs ((fe n) ! n0) <⊥, outM v>)"
    have LastNonUniform: "nonUniform (last (fe n))" using FE by simp
    have LastIsLastIndex: "∧ l . l ≠ [] ⟶ last l = l ! ((length l) - 1)" 
      by (metis last_conv_nth)
    have Fou: "n0 ≤ length (fe n) - 1" using AssmNoDecided by simp
    have FeNNotEmpty:"fe n ≠ []" using FE(1) AllArePrefixesExec 
      by (metis AssmNoDecided(1) less_nat_zero_code list.size(3))
    hence Fou2: "length (fe n) - 1 < length (fe n)" by simp
    have "last (fe n) = (fe n) ! (length (fe n) - 1)" 
      using LastIsLastIndex FeNNotEmpty by auto
    have LastNonUniform: "nonUniform (last (fe n))" using FE by simp 
    have "reachable ((fe n) ! n0) ((fe n) ! (length (fe n) - 1))" 
      using FE execution.ReachableInExecution Fou Fou2 by metis
    hence N0ToLast: "reachable ((fe n) ! n0) (last (fe n))" 
      using LastIsLastIndex[of "fe n"] FeNNotEmpty by simp
    hence LastVDecided: "vDecided v (last (fe n))" 
      using NoOutMessageLoss[of "((fe n) ! n0)" "(last (fe n))"] 
        AssmNoDecided
      by (simp,
        metis LastNonUniform le_neq_implies_less less_nat_zero_code neq0_conv)

    have AllAgree: "∀ cfg' . reachable (last (fe n)) cfg'
      ⟶ agreement cfg'" 
    proof(clarify)
      fix cfg'
      assume LastToNext: "reachable (last (fe n)) cfg'"
      hence "reachable cfg ((fe n) ! (length (fe n) - 1))" 
        using AllExecsFromInit AssmNoDecided(1) by auto
      hence "reachable cfg (last (fe n))" using LastIsLastIndex[of "fe n"] 
        FeNNotEmpty by simp
      hence FirstToLast: "reachable cfg cfg'" using initReachable_def Cfg 
        LastToNext ReachableTrans by blast
      hence "agreementInit cfg cfg'" using Agreement by simp
      hence "∀v1. (<⊥, outM v1> ∈# msgs cfg') ⟶ (∀v2. (<⊥, outM v2> ∈#
        msgs cfg') ⟷ v2 = v1)"
        using Cfg FirstToLast
        by (simp add: agreementInit_def)
      thus "agreement cfg'" by (simp add: agreement_def)
    qed
    thus "False" using NonUniformImpliesNotDecided LastNonUniform 
      PseudoTermination LastVDecided by simp
  qed

  have Termination: "terminationFLP fe ft" using assms(1)[OF FE(2)] .

  hence AllDecideOrCrash: 
    "∀p. ∃n .
       (∃ i0 < length (ft n) . ∃b.
          (<⊥, outM b> ∈#
            sends p (states (fe n ! i0) p) (unpackMessage (ft n ! i0)))
          ∧ isReceiverOf p (ft n ! i0))
      ∨ (∀ n1 > n . ∀ m ∈ (set (drop (length (ft n)) (ft n1))) .
          ¬ isReceiverOf p m)"
    using FE(2)
    unfolding terminationFLP_def fairInfiniteExecution_def 
    by blast

  have "∀ p . ∃ n . (∀ n1 > n . ∀ m ∈ (set (drop (length (ft n)) (ft n1))) .
    ¬ isReceiverOf p m)"
  proof(clarify)
    fix p
    from AllDecideOrCrash have
    "∃ n .
       (∃ i0 < length (ft n) . ∃b.
        (<⊥, outM b> ∈# sends p (states (fe n ! i0) p) (unpackMessage (ft n ! i0)))
       ∧ isReceiverOf p (ft n ! i0))
      ∨ (∀ n1 > n . ∀ m ∈ (set (drop (length (ft n)) (ft n1))).
        ¬ isReceiverOf p m)" by simp
    hence "(∃ n . ∃ i0 < length (ft n) .
         (∃b. (<⊥, outM b> ∈#
            sends p (states (fe n ! i0) p) (unpackMessage (ft n ! i0)))
          ∧ isReceiverOf p (ft n ! i0)))
         ∨ (∃ n .∀ n1 > n . ∀ m ∈ (set (drop (length (ft n)) (ft n1))) .
           ¬ isReceiverOf p m)" by blast
    thus "∃n. (∀n1>n. (∀ m ∈ (set (drop (length (ft n)) (ft n1))).
      (¬ (isReceiverOf p m))))"
    proof(elim disjE, auto)
      fix n i0 b
      assume DecidingPoint:
        "i0 < length (ft n)"
        "isReceiverOf p (ft n ! i0)"
        "<⊥, outM b> ∈# sends p (states (fe n ! i0) p) (unpackMessage (ft n ! i0))"
      have "i0 < length (fe n) - 1"
        using DecidingPoint(1)
        by (metis (no_types) FE(3) execution.length) 
      hence StepN0: "((fe n) ! i0) ⊨ ((ft n) ! i0) ↦ ((fe n) ! (i0 + 1))" 
        using FE by (metis execution.step)
      hence "msgs ((fe n) ! (i0 + 1)) <⊥, outM b>
        = (msgs ((fe n) ! i0) <⊥, outM b>) +
        (sends p (states ((fe n) ! i0) p)
        (unpackMessage ((ft n) ! i0)) <⊥, outM b>)" 
        using DecidingPoint(2) OutOnlyGrowing[of "(fe n) ! i0" "(ft n) ! i0"
          "(fe n) ! (i0 + 1)" "p"] 
        by auto
      hence "(sends p (states ((fe n) ! i0) p)
        (unpackMessage ((ft n) ! i0)) <⊥, outM b>)
        ≤ msgs ((fe n) ! (i0 + 1)) <⊥, outM b>" 
        using asynchronousSystem.steps_def by auto
      hence OutMsgEx: "0 < msgs ((fe n) ! (i0 + 1)) <⊥, outM b>" 
        using asynchronousSystem.steps_def DecidingPoint(3) by auto
      have "(i0 + 1) < length (fe n)"
        using DecidingPoint(1) ‹i0 < length (fe n) - 1› by auto
      hence "initReachable ((fe n) ! (i0 + 1))" 
        using AllExecsFromInit Cfg(1) 
        by (metis asynchronousSystem.initReachable_def)
      hence Decided: "vDecided b ((fe n) ! (i0 + 1))" using OutMsgEx 
        by auto
      have "i0 + 1 < length (fe n)" using DecidingPoint(1) 
        by (metis ‹(((i0::nat) + (1::nat)) < (length (
 (fe::(nat ==> ('p, 'v, 's) configuration list)) (n::nat))))›)
      hence "¬ vDecided b ((fe n) ! (i0 + 1))" using NoDecided by auto
      hence "False" using Decided by auto
      thus "∃n. (∀n1>n. (∀ m ∈ (set (drop (length (ft n)) (ft n1))).
        (¬ (isReceiverOf p m))))" by simp
    qed
  qed
  hence "∃ (crashPoint::'p ==> nat) .
    ∀ p . ∃ n . crashPoint p = n ∧ (∀ n1 > n . ∀ m ∈ (set (drop
    (length (ft n)) (ft n1))) . (¬ isReceiverOf p m))" by metis  
  then obtain crashPoint where CrashPoint:
    "∀ p . (∀ n1 > (crashPoint p) . ∀ m ∈ (set (drop (length
    (ft (crashPoint p))) (ft n1))) . (¬ isReceiverOf p m))"
    by blast
  define limitSet where "limitSet = {crashPoint p | p . p ∈ Proc}"
  have "finite {p. p ∈ Proc}" using finiteProcs by simp
  hence "finite limitSet" using limitSet_def finite_image_set[] by blast
  hence "∃ limit . ∀ l ∈ limitSet . l < limit" using 
    finite_nat_set_iff_bounded by auto
  hence "∃ limit . ∀ p . (crashPoint p) < limit" using limitSet_def by auto
  then obtain limit where Limit: "∀ p . (crashPoint p) < limit" by blast
  define lengthLimit where "lengthLimit = length (ft limit) - 1"
  define lateMessage where "lateMessage = last (ft limit)"
  hence "lateMessage = (ft limit) ! (length (ft limit) - 1)" 
    by (metis AllArePrefixesTrace Limit last_conv_nth less_nat_zero_code 
      list.size(3) PrefixListMonotonicity)
  hence LateIsLast: "lateMessage = (ft limit) ! lengthLimit" 
  using lateMessage_def lengthLimit_def by auto

  have "∃ p . isReceiverOf p lateMessage" 
  proof(rule ccontr)
    assume "¬ (∃(p::'p). (isReceiverOf p lateMessage))"
    hence IsOutMsg: "∃ v . lateMessage = <⊥, outM v>"
      by (metis isReceiverOf.simps(1) isReceiverOf.simps(2) message.exhaust)
    have "execution trans sends start (fe limit) (ft limit)" using FE 
      by auto
    hence "length (fe limit) - 1 = length (ft limit)"
      using execution.length by simp
    hence "lengthLimit < length (fe limit) - 1" 
      using lengthLimit_def 
      by (metis (opaque_lifting, no_types) Length Limit One_nat_def Suc_eq_plus1
        Suc_le_eq diff_less 
        diffs0_imp_equal gr_implies_not0 less_Suc0 neq0_conv)
    hence "((fe limit) ! lengthLimit) ⊨ ((ft limit) ! lengthLimit)
      ↦ ((fe limit) ! (lengthLimit + 1))"
      using FE by (metis execution.step)
    hence "((fe limit) ! lengthLimit) ⊨ lateMessage ↦ ((fe limit) !
      (lengthLimit + 1))"
      using LateIsLast by auto
    thus False using IsOutMsg steps_def by auto
  qed

  then obtain p where ReceiverOfLate: "isReceiverOf p lateMessage" by blast
  have "∀ n1 > (crashPoint p) .
    ∀ m ∈ (set (drop (length (ft (crashPoint p))) (ft n1))) .
      (¬ isReceiverOf p m)"
    using CrashPoint
    by simp
  hence NoMsgAfterLimit: "∀ m ∈ (set (drop (length (ft (crashPoint p)))
    (ft limit))) . (¬ isReceiverOf p m)"
    using Limit
    by auto
  have "lateMessage ∈ set (drop (length(ft (crashPoint p))) (ft limit))" 
  proof-
    have "crashPoint p < limit" using Limit by simp
    hence "prefixList (ft (crashPoint p)) (ft limit)" 
      using AllArePrefixesTrace by auto
    hence CrashShorterLimit: "length (ft (crashPoint p))
      < length (ft limit)" using PrefixListMonotonicity by auto
    hence "last (drop (length (ft (crashPoint p))) (ft limit))
      = last (ft limit)" by (metis last_drop)
    hence "lateMessage = last (drop (length (ft (crashPoint p)))
      (ft limit))" using lateMessage_def by auto
    thus "lateMessage ∈ set (drop (length(ft (crashPoint p))) (ft limit))" 
      by (metis CrashShorterLimit drop_eq_Nil last_in_set not_le)
  qed
  
  hence "¬ isReceiverOf p lateMessage" using NoMsgAfterLimit by auto
  thus "False" using ReceiverOfLate by simp
qed

end

end