Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-06-02 10:36 56035953

View on Github →

feat(computability/turing_machine): proving the TM reductions

Estimated changes

Modified data/computability/turing_machine.lean

added structure turing.TM0.cfg

added def turing.TM0.eval

added def turing.TM0.machine

deleted structure turing.TM0.machine

added def turing.TM0.reaches

deleted structure turing.TM0.state

modified def turing.TM0.step

added structure turing.TM1.cfg

added def turing.TM1.eval

added def turing.TM1.reaches

deleted structure turing.TM1.state

modified def turing.TM1.step

modified theorem turing.TM1.step_supports

added theorem turing.TM1.stmts_supports_stmt

added theorem turing.TM1.stmts_trans

modified theorem turing.TM1.stmts₁_self

added theorem turing.TM1.stmts₁_supports_stmt_mono

added theorem turing.TM1.stmts₁_trans

modified def turing.TM1.supports

modified def turing.TM1.supports_stmt

added def turing.TM1to0.tr'

added def turing.TM1to0.tr

added def turing.TM1to0.tr_cfg

added theorem turing.TM1to0.tr_reaches

added theorem turing.TM1to0.tr_supports

deleted def turing.TM1to0.trans

deleted def turing.TM1to0.translate

added def turing.TM1to0.Λ'

added structure turing.TM2.cfg

added def turing.TM2.eval

added theorem turing.TM2.move_until_left_reaches

added theorem turing.TM2.move_until_right_reaches

added def turing.TM2.reaches

deleted structure turing.TM2.state

modified def turing.TM2.step

modified def turing.TM2.step_aux

added theorem turing.TM2.step_supports

added theorem turing.TM2.stmts_supports_stmt

added theorem turing.TM2.stmts_trans

added theorem turing.TM2.stmts₁_self

added theorem turing.TM2.stmts₁_supports_stmt_mono

added theorem turing.TM2.stmts₁_trans

added def turing.TM2.supports

added def turing.TM2.supports_stmt

added def turing.TM2to1.tr'

added def turing.TM2to1.tr

added def turing.TM2to1.tr_cfg

added theorem turing.TM2to1.tr_reaches

added theorem turing.TM2to1.tr_supports

deleted def turing.TM2to1.translate'

deleted def turing.TM2to1.translate

added def turing.TM2to1.Λ'

added structure turing.TM3.cfg

added def turing.TM3.eval

deleted structure turing.TM3.machine

added def turing.TM3.reaches

deleted structure turing.TM3.state

modified def turing.TM3.step

modified def turing.TM3.step_aux

added theorem turing.TM3.step_supports

added theorem turing.TM3.stmts_supports_stmt

added theorem turing.TM3.stmts_trans

added theorem turing.TM3.stmts₁_self

added theorem turing.TM3.stmts₁_supports_stmt_mono

added theorem turing.TM3.stmts₁_trans

added def turing.TM3.supports

added def turing.TM3.supports_stmt

deleted structure turing.TM3to2.alph

added theorem turing.TM3to2.at_stack_supports

added def turing.TM3to2.stack_val

added def turing.TM3to2.tr

added inductive turing.TM3to2.tr_cfg

added theorem turing.TM3to2.tr_supports

added def turing.TM3to2.tr_tape

deleted def turing.TM3to2.translate

added def turing.TM3to2.Γ'.write_stack

added structure turing.TM3to2.Γ'

added def turing.TM3to2.Γ'_equiv

added def turing.TM3to2.Λ'

added def turing.eval

deleted def turing.move_tape

added def turing.tape.mk

added def turing.tape.move

added theorem turing.tape.move_left_nth

added theorem turing.tape.move_right_nth

added def turing.tape.nth

added def turing.tape.write

added theorem turing.tape.write_nth

added theorem turing.tape.write_self

added def turing.tape

Modified data/equiv.lean

modified def equiv.d_array_equiv_fin

Modified data/finset.lean

modified theorem finset.pi_insert

Modified data/fintype.lean

added theorem fintype.card_option

Modified data/multiset.lean

Modified logic/basic.lean

deleted theorem exists_eq'

modified theorem exists_eq

added theorem exists_eq_left'

added theorem exists_eq_left

Modified logic/relation.lean

added theorem relation.refl_trans_gen_closed

added theorem relation.refl_trans_gen_eq_self

added theorem relation.refl_trans_gen_idem

added theorem relation.refl_trans_gen_lift'

deleted theorem relation.refl_trans_gen_refl_trans_gen