theorem OperatorDirectory.Computational.real (e : MidgardParameters) (i : State.ODirActs) (s s' : State.OperatorDirectory) (Rel : Relation e i s s') : StateMachine.next e i s = ComputationResult.Success s'

theorem OperatorDirectory.Computational.abstract (p : MidgardParameters) (i : State.ODirActs) (s s' : State.OperatorDirectory) (HStep : StateMachine.next p i s = ComputationResult.Success s') : Relation p i s s'

def OperatorDirectory.Computational.ComputationalRelation : ComputationalRel StateMachine.Err Relation

Equations

• OperatorDirectory.Computational.ComputationalRelation = { compute := OperatorDirectory.StateMachine.next, correct := OperatorDirectory.Computational.ComputationalRelation._proof_1 }

theorem OperatorDirectory.Computational.ExistsState {p : MidgardParameters} {i : State.ODirActs} {s : State.OperatorDirectory} : (∃ (s' : State.OperatorDirectory), Relation p i s s') ↔ ∃ (s' : State.OperatorDirectory), StateMachine.next p i s = ComputationResult.Success s'

def OperatorDirectory.Computational.Relation.StepMachine : StepMachines.StepMachine MidgardParameters State.ODirActs State.OperatorDirectory

Equations

• OperatorDirectory.Computational.Relation.StepMachine = { init := OperatorDirectory.State.OperatorDirectory.init, STS := OperatorDirectory.Relation }