Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-06-16 17:39 85bc56ad

View on Github →

feat(computability/turing_machine): finish stack machine proof

Estimated changes

Modified algebra/group_power.lean

Modified computability/turing_machine.lean

deleted theorem turing.TM2.move_until_left_reaches

added theorem turing.TM2.move_until_left_reaches₁

deleted theorem turing.TM2.move_until_right_reaches

added theorem turing.TM2.move_until_right_reaches₁

added def turing.TM2.reaches₁

added theorem turing.TM2.reaches₁_step

modified def turing.TM3.eval

modified def turing.TM3to2.at_stack

deleted theorem turing.TM3to2.at_stack_supports

deleted def turing.TM3to2.pop

deleted def turing.TM3to2.push

deleted def turing.TM3to2.stack_val

modified def turing.TM3to2.stackel.get

modified def turing.TM3to2.stackel.is_bottom

modified def turing.TM3to2.stackel.is_top

modified inductive turing.TM3to2.stackel

modified def turing.TM3to2.stackel_equiv

added theorem turing.TM3to2.tr_reaches

added def turing.TM3to2.tr_stk

deleted def turing.TM3to2.tr_tape

deleted def turing.TM3to2.Γ'.write_stack

added def turing.TM3to2.Γ'

deleted structure turing.TM3to2.Γ'

deleted def turing.TM3to2.Γ'_equiv

added def turing.dwrite

added theorem turing.dwrite_eq

added theorem turing.dwrite_ne

added theorem turing.dwrite_self

modified theorem turing.tape.move_left_nth

modified theorem turing.tape.move_right_nth

added theorem turing.tape.nth_zero

modified theorem turing.tape.write_nth

Modified data/list/basic.lean

added theorem list.map_eq_append_split

added theorem list.repeat_add

Modified group_theory/free_group.lean

Modified logic/relation.lean

added theorem relation.refl_trans_gen_iff_eq_or_trans_gen

added theorem relation.trans_gen.head'

added theorem relation.trans_gen.head'_iff

added theorem relation.trans_gen.head

added theorem relation.trans_gen.tail'

added theorem relation.trans_gen.tail'_iff

added theorem relation.trans_gen.to_refl

added theorem relation.trans_gen.trans

added theorem relation.trans_gen.trans_left

added theorem relation.trans_gen.trans_right

added inductive relation.trans_gen