theorem StateQueue.Computational.real {p : MidgardParameters} {i : InputInfo} {s s' : State.StateQueue} {fp : FraudProofTokens.State.FraudProofTokens} {a : State.Actions} {sch : Scheduler.State.SchedulerDatum} (Step : Relation p sch fp i s a s') : Machine.next p sch fp i a s = ComputationResult.Success s'

theorem StateQueue.Computational.abstract {p : MidgardParameters} {i : InputInfo} {s s' : State.StateQueue} {fp : FraudProofTokens.State.FraudProofTokens} {a : State.Actions} {sch : Scheduler.State.SchedulerDatum} (comp : Machine.next p sch fp i a s = ComputationResult.Success s') : Relation p sch fp i s a s'

structure StateQueue.Computational.Environment : Type

• p : MidgardParameters
• sch : Scheduler.State.SchedulerDatum
• fraudproofs : FraudProofTokens.State.FraudProofTokens

def StateQueue.Computational.RelationFormat (e : Environment) (a : InputInfo × State.Actions) (s s' : State.StateQueue) : Prop

Equations

• StateQueue.Computational.RelationFormat e a s s' = StateQueue.Relation e.p e.sch e.fraudproofs a.1 s a.2 s'

def StateQueue.Computational.computational : ComputationalRel Machine.Err RelationFormat

Equations

• One or more equations did not get rendered due to their size.

def StateQueue.Computational.StateQueueMachine : StepMachines.StepMachine Environment (InputInfo × State.Actions) State.StateQueue

Equations

• StateQueue.Computational.StateQueueMachine = { init := StateQueue.State.StateQueue.init, STS := StateQueue.Computational.RelationFormat }