Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-31 03:00 b3752640

View on Github →

feat(computability/turing_machine): add TMs and reductions

Estimated changes

Modified data/array/lemmas.lean

Modified data/computability/halting.lean

Created data/computability/turing_machine.lean

added structure turing.TM0.machine

added structure turing.TM0.state

added def turing.TM0.step

added theorem turing.TM0.step_supports

added inductive turing.TM0.stmt

added def turing.TM0.supports

added structure turing.TM1.state

added def turing.TM1.step

added theorem turing.TM1.step_supports

added inductive turing.TM1.stmt

added theorem turing.TM1.stmts₁_self

added def turing.TM1.supports

added def turing.TM1.supports_stmt

added def turing.TM1to0.trans

added def turing.TM1to0.translate

added structure turing.TM2.state

added def turing.TM2.step

added def turing.TM2.step_aux

added inductive turing.TM2.stmt

added def turing.TM2to1.translate'

added def turing.TM2to1.translate

added structure turing.TM3.machine

added structure turing.TM3.state

added def turing.TM3.step

added def turing.TM3.step_aux

added inductive turing.TM3.stmt

added structure turing.TM3to2.alph

added def turing.TM3to2.at_stack

added def turing.TM3to2.pop

added def turing.TM3to2.push

added def turing.TM3to2.stackel.get

added def turing.TM3to2.stackel.is_bottom

added def turing.TM3to2.stackel.is_top

added inductive turing.TM3to2.stackel

added def turing.TM3to2.stackel_equiv

added def turing.TM3to2.translate

added def turing.dir.rev

added inductive turing.dir

added def turing.move_tape

Modified data/fintype.lean

Modified data/real/basic.lean

modified def real

Modified data/sum.lean