Library Progress
Copyright (c) 2018 by Swirlds, Inc.
Implemented by Karl Crary.
Require Import Nat.
Require Import Omega.
Require Import List.
Require Import Tact.
Require Import Decide.
Require Import Cardinality.
Require Import Calculate.
Require Import Majority.
Require Import Relation.
Require Import HashgraphFacts.
Require Import Sees.
Require Import Round.
Lemma honest_event_exists :
forall s, exists x, member (global s) x /\ honest (creator x).
Lemma realtime_impl_self_ancestor :
forall s x y,
honest (creator x)
-> creator x = creator y
-> realtime s x y
-> x $= y.
Lemma event_transmit :
forall s x a,
member (global s) x
-> honest (creator x)
-> honest a
-> exists y,
member (global s) y
/\ creator y = a
/\ x @= y.
Lemma event_broadcast :
forall s x,
member (global s) x
-> honest (creator x)
-> exists y,
member (global s) y
/\ honest (creator y)
/\ forall a,
honest a
-> exists w,
creator w = a
/\ x @= w
/\ w @= y.
nil
Lemma round_advanced :
forall x y i j,
round i x
-> round j y
-> supermajority
stake
(fun a =>
exists w,
creator w = a
/\ x @= w
/\ stsees w y)
every
-> i < j.
Lemma global_nonterminating :
forall s, nonterminating (global s).
forall x y i j,
round i x
-> round j y
-> supermajority
stake
(fun a =>
exists w,
creator w = a
/\ x @= w
/\ stsees w y)
every
-> i < j.
Lemma global_nonterminating :
forall s, nonterminating (global s).
0