Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-02 07:22 ff4eeed7

View on Github →

feat(computability/turing_machine): reduce to 2-symbol TMs

Estimated changes

Modified computability/turing_machine.lean

added def turing.TM0.cfg.map

modified def turing.TM0.init

added def turing.TM0.machine.map

added theorem turing.TM0.machine.map_respects

added theorem turing.TM0.machine.map_step

added theorem turing.TM0.map_init

modified theorem turing.TM0.step_supports

added def turing.TM0.stmt.map

modified def turing.TM0.supports

added theorem turing.TM0.univ_supports

added def turing.TM0to1.tr

added def turing.TM0to1.tr_cfg

added theorem turing.TM0to1.tr_respects

added inductive turing.TM0to1.Λ'

modified def turing.TM1.init

modified def turing.TM1.step_aux

modified def turing.TM1to0.tr_cfg

modified theorem turing.TM1to0.tr_supports

added theorem turing.TM1to1.exists_enc_dec

added def turing.TM1to1.move

added def turing.TM1to1.read

added def turing.TM1to1.read_aux

added theorem turing.TM1to1.step_aux_move

added theorem turing.TM1to1.step_aux_read

added theorem turing.TM1to1.step_aux_write

added theorem turing.TM1to1.supports_stmt_move

added theorem turing.TM1to1.supports_stmt_read

added theorem turing.TM1to1.supports_stmt_write

added def turing.TM1to1.tr

added def turing.TM1to1.tr_cfg

added def turing.TM1to1.tr_normal

added theorem turing.TM1to1.tr_respects

added theorem turing.TM1to1.tr_supports

added def turing.TM1to1.tr_tape'

added theorem turing.TM1to1.tr_tape'_move_left

added theorem turing.TM1to1.tr_tape'_move_right

added def turing.TM1to1.tr_tape

added theorem turing.TM1to1.tr_tape_drop_right

added theorem turing.TM1to1.tr_tape_take_right

added def turing.TM1to1.write

added inductive turing.TM1to1.Λ'

modified def turing.TM2.init

modified def turing.TM2.step_aux

modified theorem turing.TM2to1.tr_respects_aux₃

deleted def turing.TM2to1.Λ'_inh

added def turing.pointed_map

added theorem turing.reaches.to₀

added theorem turing.reaches₀.head

added theorem turing.reaches₀.refl

added theorem turing.reaches₀.single

added theorem turing.reaches₀.tail'

added theorem turing.reaches₀.tail

added theorem turing.reaches₀.trans

added def turing.reaches₀

added theorem turing.reaches₀_eq

added theorem turing.reaches₁.to₀

added theorem turing.reaches₁_fwd

added def turing.tape.map

added theorem turing.tape.map_fst

added theorem turing.tape.map_mk

added theorem turing.tape.map_move

added theorem turing.tape.map_write

added def turing.tape.mk'

Modified data/bool.lean

added theorem bool.default_bool

added theorem bool.to_bool_eq

Modified data/fin.lean

added def fin.add_nat

Modified data/finset.lean

added theorem finset.coe_empty

added theorem finset.coe_erase

added theorem finset.coe_filter

added theorem finset.coe_image

added theorem finset.coe_inj

added theorem finset.coe_insert

added theorem finset.coe_inter

added theorem finset.coe_sdiff

added theorem finset.coe_singleton

added theorem finset.coe_subset

added theorem finset.coe_union

added theorem finset.mem_coe

added def finset.to_set

Modified data/fintype.lean

Modified data/list/basic.lean

added theorem list.bind_append

added theorem list.drop_add

added theorem list.drop_left'

added theorem list.drop_left

added theorem list.drop_one

added theorem list.ne_nil_of_mem

added theorem list.reverse_repeat

added def list.take'

added theorem list.take'_eq_take

added theorem list.take'_left'

added theorem list.take'_left

added theorem list.take'_length

added theorem list.take'_nil

added theorem list.take_left'

added theorem list.take_left

Modified data/set/finite.lean

deleted theorem finset.coe_empty

deleted theorem finset.coe_eq_coe

deleted theorem finset.coe_erase

deleted theorem finset.coe_filter

deleted theorem finset.coe_image

deleted theorem finset.coe_insert

deleted theorem finset.coe_inter

deleted theorem finset.coe_sdiff

deleted theorem finset.coe_singleton

deleted theorem finset.coe_subseteq_coe

deleted theorem finset.coe_union

deleted theorem finset.mem_coe

deleted def finset.to_set

Modified data/vector2.lean

modified theorem vector.mk_to_list

added def vector.reverse

Modified linear_algebra/basic.lean

Modified logic/embedding.lean

added theorem function.embedding.set_value_eq