FiniteStateMachines

Difficulty: easy — 2 definitions, 0 abbreviations, 0 lemmas, 0 theorems, 0 examples.

definition
legend
sequential-circuits
structure FiniteStateMachine (State Input Output : Type) [Fintype State] [Fintype Input] [Fintype Output]
  [Nonempty State] [Nonempty Input] [Nonempty Output] : Type
  • step : State → Input → State × Output
Show details

Outer dependencies: (none)

Mathlib dependencies: Fintype

Lean core dependencies: Eq, HEq, Nat, Nonempty, Prod, SizeOf, eq_of_heq

Used by: FiniteStateMachine.Reversible

def FiniteStateMachine.Reversible {State Input Output : Type} [Fintype State] [Fintype Input]
  [Fintype Output] [Nonempty State] [Nonempty Input] [Nonempty Output]
  (fsm : FiniteStateMachine State Input Output) : Prop
Show details 
| fsm.Reversible = Function.Injective fun p => fsm.step p.1 p.2

Complexity: 107 (size of the value term)

Outer dependencies: FiniteStateMachine

Mathlib dependencies: Fintype

Lean core dependencies: Function.Injective, Nonempty, Prod

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitiondeclared elsewheredependencyproof dependency
legend