Library Timestamp
Require Import Nat.
Require Import Bool.
Require Import Omega.
Require Import List.
Require Import Permutation.
Require Import Tact.
Require Import Decide.
Require Import Relation.
Require Import Majority.
Require Import Weight.
Require Import HashgraphFacts.
Require Import Sees.
Require Import Round.
Require Import Progress.
Require Import Vote.
Require Import Decision.
Require Import Consensus.
Require Import Famous.
Require Import Fairness.
Require Import Received.
Require Import Median.
Require Import Order.
Lemma ufwitness_fun :
forall s W i x y,
creator x = creator y
-> ufwitness s W i x
-> ufwitness s W i y
-> x = y.
Lemma list_minimum :
forall (T : Type) (R : T -> T -> Prop) l,
transitive T R
-> (forall x y, R x y \/ R y x)
-> l = nil \/ exists x, In x l /\ forall y, In y l -> R x y.
Lemma obtain_ufwitness :
forall s W i x,
finite (fwitness s W i)
-> fwitness s W i x
-> exists y,
creator x = creator y
/\ ufwitness s W i y.
Lemma earliest_observer_fun :
forall x y y' z,
earliest_observer x y z
-> earliest_observer x y' z
-> y = y'.
Lemma earliest_observer_defined :
forall x z,
x @= z
-> exists y,
earliest_observer x y z.
Corollary honest_timestamp :
forall s x t,
time_received s (global s) x t
-> exists i y y' w w',
received s (global s) i x
/\ honest (creator y)
/\ honest (creator y')
/\ ufwitness s (global s) i w
/\ ufwitness s (global s) i w'
/\ earliest_observer x y w
/\ earliest_observer x y' w'
/\ timestamp y <= t <= timestamp y'.