Commit 2023-05-11 05:53 c8947716

View on Github →

feat: port Computability.TMToPartrec (#3864)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Computability/TMToPartrec.lean

added def Turing.PartrecToTM2.Cfg'

added inductive Turing.PartrecToTM2.Cont'

added def Turing.PartrecToTM2.K'.elim

added theorem Turing.PartrecToTM2.K'.elim_aux

added theorem Turing.PartrecToTM2.K'.elim_main

added theorem Turing.PartrecToTM2.K'.elim_rev

added theorem Turing.PartrecToTM2.K'.elim_stack

added theorem Turing.PartrecToTM2.K'.elim_update_aux

added theorem Turing.PartrecToTM2.K'.elim_update_main

added theorem Turing.PartrecToTM2.K'.elim_update_rev

added theorem Turing.PartrecToTM2.K'.elim_update_stack

added inductive Turing.PartrecToTM2.K'

added def Turing.PartrecToTM2.Stmt'

added def Turing.PartrecToTM2.Supports

added def Turing.PartrecToTM2.TrCfg

added theorem Turing.PartrecToTM2.clear_ok

added def Turing.PartrecToTM2.codeSupp'

added theorem Turing.PartrecToTM2.codeSupp'_self

added theorem Turing.PartrecToTM2.codeSupp'_supports

added def Turing.PartrecToTM2.codeSupp

added theorem Turing.PartrecToTM2.codeSupp_case

added theorem Turing.PartrecToTM2.codeSupp_comp

added theorem Turing.PartrecToTM2.codeSupp_cons

added theorem Turing.PartrecToTM2.codeSupp_fix

added theorem Turing.PartrecToTM2.codeSupp_self

added theorem Turing.PartrecToTM2.codeSupp_succ

added theorem Turing.PartrecToTM2.codeSupp_supports

added theorem Turing.PartrecToTM2.codeSupp_tail

added theorem Turing.PartrecToTM2.codeSupp_zero

added def Turing.PartrecToTM2.contStack

added def Turing.PartrecToTM2.contSupp

added theorem Turing.PartrecToTM2.contSupp_comp

added theorem Turing.PartrecToTM2.contSupp_cons₁

added theorem Turing.PartrecToTM2.contSupp_cons₂

added theorem Turing.PartrecToTM2.contSupp_fix

added theorem Turing.PartrecToTM2.contSupp_halt

added theorem Turing.PartrecToTM2.contSupp_supports

added theorem Turing.PartrecToTM2.copy_ok

added def Turing.PartrecToTM2.halt

added def Turing.PartrecToTM2.head

added theorem Turing.PartrecToTM2.head_main_ok

added theorem Turing.PartrecToTM2.head_stack_ok

added theorem Turing.PartrecToTM2.head_supports

added def Turing.PartrecToTM2.init

added def Turing.PartrecToTM2.moveExcl

added theorem Turing.PartrecToTM2.move_ok

added def Turing.PartrecToTM2.move₂

added theorem Turing.PartrecToTM2.move₂_ok

added def Turing.PartrecToTM2.natEnd

added def Turing.PartrecToTM2.peek'

added def Turing.PartrecToTM2.pop'

added theorem Turing.PartrecToTM2.pred_ok

added def Turing.PartrecToTM2.push'

added theorem Turing.PartrecToTM2.ret_supports

added def Turing.PartrecToTM2.splitAtPred

added theorem Turing.PartrecToTM2.splitAtPred_eq

added theorem Turing.PartrecToTM2.splitAtPred_false

added theorem Turing.PartrecToTM2.succ_ok

added theorem Turing.PartrecToTM2.supports_bunionᵢ

added theorem Turing.PartrecToTM2.supports_insert

added theorem Turing.PartrecToTM2.supports_singleton

added theorem Turing.PartrecToTM2.supports_union

added def Turing.PartrecToTM2.tr

added def Turing.PartrecToTM2.trCont

added def Turing.PartrecToTM2.trContStack

added def Turing.PartrecToTM2.trLList

added def Turing.PartrecToTM2.trList

added theorem Turing.PartrecToTM2.trList_ne_consₗ

added def Turing.PartrecToTM2.trNat

added theorem Turing.PartrecToTM2.trNat_default

added theorem Turing.PartrecToTM2.trNat_natEnd

added theorem Turing.PartrecToTM2.trNat_zero

added def Turing.PartrecToTM2.trNormal

added theorem Turing.PartrecToTM2.trNormal_respects

added theorem Turing.PartrecToTM2.trNormal_supports

added def Turing.PartrecToTM2.trNum

added theorem Turing.PartrecToTM2.trNum_natEnd

added def Turing.PartrecToTM2.trPosNum

added theorem Turing.PartrecToTM2.trPosNum_natEnd

added def Turing.PartrecToTM2.trStmts₁

added theorem Turing.PartrecToTM2.trStmts₁_self

added theorem Turing.PartrecToTM2.trStmts₁_supports'

added theorem Turing.PartrecToTM2.trStmts₁_supports

added theorem Turing.PartrecToTM2.trStmts₁_trans

added theorem Turing.PartrecToTM2.tr_clear

added theorem Turing.PartrecToTM2.tr_copy

added theorem Turing.PartrecToTM2.tr_eval

added theorem Turing.PartrecToTM2.tr_init

added theorem Turing.PartrecToTM2.tr_move

added theorem Turing.PartrecToTM2.tr_pred

added theorem Turing.PartrecToTM2.tr_push

added theorem Turing.PartrecToTM2.tr_read

added theorem Turing.PartrecToTM2.tr_respects

added theorem Turing.PartrecToTM2.tr_ret_comp

added theorem Turing.PartrecToTM2.tr_ret_cons₁

added theorem Turing.PartrecToTM2.tr_ret_cons₂

added theorem Turing.PartrecToTM2.tr_ret_fix

added theorem Turing.PartrecToTM2.tr_ret_halt

added theorem Turing.PartrecToTM2.tr_ret_respects

added theorem Turing.PartrecToTM2.tr_succ

added theorem Turing.PartrecToTM2.tr_supports

added def Turing.PartrecToTM2.unrev

added theorem Turing.PartrecToTM2.unrev_ok

added inductive Turing.PartrecToTM2.Γ'

added def Turing.PartrecToTM2.Λ'.Supports

added inductive Turing.PartrecToTM2.Λ'

added def Turing.ToPartrec.Cfg.then

added inductive Turing.ToPartrec.Cfg

added theorem Turing.ToPartrec.Code.Ok.zero

added def Turing.ToPartrec.Code.Ok

added theorem Turing.ToPartrec.Code.case_eval

added theorem Turing.ToPartrec.Code.comp_eval

added theorem Turing.ToPartrec.Code.cons_eval

added def Turing.ToPartrec.Code.eval

added theorem Turing.ToPartrec.Code.exists_code.comp

added theorem Turing.ToPartrec.Code.exists_code

added theorem Turing.ToPartrec.Code.fix_eval

added def Turing.ToPartrec.Code.head

added theorem Turing.ToPartrec.Code.head_eval

added def Turing.ToPartrec.Code.id

added theorem Turing.ToPartrec.Code.id_eval

added def Turing.ToPartrec.Code.nil

added theorem Turing.ToPartrec.Code.nil_eval

added def Turing.ToPartrec.Code.prec

added def Turing.ToPartrec.Code.pred

added theorem Turing.ToPartrec.Code.pred_eval

added def Turing.ToPartrec.Code.rfind

added theorem Turing.ToPartrec.Code.succ_eval

added theorem Turing.ToPartrec.Code.tail_eval

added theorem Turing.ToPartrec.Code.zero'_eval

added def Turing.ToPartrec.Code.zero

added theorem Turing.ToPartrec.Code.zero_eval

added inductive Turing.ToPartrec.Code

added def Turing.ToPartrec.Cont.eval

added def Turing.ToPartrec.Cont.then

added theorem Turing.ToPartrec.Cont.then_eval

added inductive Turing.ToPartrec.Cont

added theorem Turing.ToPartrec.code_is_ok

added theorem Turing.ToPartrec.cont_eval_fix

added def Turing.ToPartrec.step

added theorem Turing.ToPartrec.stepNormal.is_ret

added def Turing.ToPartrec.stepNormal

added theorem Turing.ToPartrec.stepNormal_eval

added theorem Turing.ToPartrec.stepNormal_then

added def Turing.ToPartrec.stepRet

added theorem Turing.ToPartrec.stepRet_eval

added theorem Turing.ToPartrec.stepRet_then