Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1667 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (35 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (412 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (41 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (450 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (42 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (15 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (7 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (104 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (50 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (9 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (499 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (3 entries)

Global Index

A

ACom [inductive, in ProgrammingTuringMachines.TM.LM.Alphabets]
ACom_inhab [instance, in ProgrammingTuringMachines.TM.LM.Alphabets]
ACom_finType [instance, in ProgrammingTuringMachines.TM.LM.Alphabets]
ACom_eq_dec [instance, in ProgrammingTuringMachines.TM.LM.Alphabets]
Add [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
AddTapes [section, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
AddTapes.n [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
add_tapes_select_nth [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
add_tapes_dupfree [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
add_tapes [definition, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Add_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.NatTM]
Add_steps [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Main_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Main_steps [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Loop_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Loop_steps [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Computes [lemma, in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Main_Realise [lemma, in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Main_Rel [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Loop_Realise [lemma, in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Loop_Rel [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Step_Sem [lemma, in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Step_Rel [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Main [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Loop [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Step [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Alphabets [library]
App [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
appAT [constructor, in ProgrammingTuringMachines.TM.LM.Alphabets]
Append [section, in ProgrammingTuringMachines.TM.Code.ListTM]
Append.cX [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Append.defX [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Append.sigX [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Append.stop [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Append.X [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
appT [constructor, in ProgrammingTuringMachines.TM.LM.Semantics]
App_Com_Terminates [lemma, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Com_T [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Com_steps [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Com_Realise [lemma, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Com_Rel [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Com [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_ACom_Terminates [lemma, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_ACom_T [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_ACom_steps [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_ACom_Realise [lemma, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_ACom_Rel [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_ACom [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Comens_Terminates [lemma, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Comens_T [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Comens_steps [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Comens_Realise [lemma, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Comens_Rel [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Comens [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
App_T [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
App_steps [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
App_Computes [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
app_or_nil [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
app_tapes_select_nth [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
app_tapes_dupfree [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
app_tapes [definition, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
App' [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
App'_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
App'_T [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
App'_steps [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
App'_Realise [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
App'_Rel [definition, in ProgrammingTuringMachines.TM.Code.ListTM]


B

Basic [library]
boundary [inductive, in ProgrammingTuringMachines.TM.Code.CodeTM]
boundary_fin [instance, in ProgrammingTuringMachines.TM.Code.CodeTM]
boundary_eq [instance, in ProgrammingTuringMachines.TM.Code.CodeTM]


C

Canonical_TerminatesIn [lemma, in ProgrammingTuringMachines.TM.TM]
Canonical_T [definition, in ProgrammingTuringMachines.TM.TM]
Canonical_Realise [lemma, in ProgrammingTuringMachines.TM.TM]
Canonical_Rel [definition, in ProgrammingTuringMachines.TM.TM]
CaseCom [definition, in ProgrammingTuringMachines.TM.LM.CaseCom]
CaseCom [library]
CaseCom_Sem [lemma, in ProgrammingTuringMachines.TM.LM.CaseCom]
CaseCom_steps [definition, in ProgrammingTuringMachines.TM.LM.CaseCom]
CaseCom_Rel [definition, in ProgrammingTuringMachines.TM.LM.CaseCom]
CaseFin [definition, in ProgrammingTuringMachines.TM.Code.CaseFin]
CaseFin [section, in ProgrammingTuringMachines.TM.Code.CaseFin]
CaseFin [library]
CaseFin_Sem [lemma, in ProgrammingTuringMachines.TM.Code.CaseFin]
CaseFin_Rel [definition, in ProgrammingTuringMachines.TM.Code.CaseFin]
CaseFin.defSig [variable, in ProgrammingTuringMachines.TM.Code.CaseFin]
CaseFin.sig [variable, in ProgrammingTuringMachines.TM.Code.CaseFin]
CaseList [definition, in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList [section, in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList [library]
CaseList_steps_comp [lemma, in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList_steps_cons_comp [lemma, in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList_steps [definition, in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList_steps_nil [definition, in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList_steps_cons [definition, in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList_Realise [lemma, in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList_Rel [definition, in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList.cX [variable, in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList.sigX [variable, in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList.X [variable, in ProgrammingTuringMachines.TM.Code.CaseList]
CaseNat [definition, in ProgrammingTuringMachines.TM.Code.CaseNat]
CaseNat [section, in ProgrammingTuringMachines.TM.Code.CaseNat]
CaseNat [library]
CaseNat_Sem [lemma, in ProgrammingTuringMachines.TM.Code.CaseNat]
CaseNat_steps [definition, in ProgrammingTuringMachines.TM.Code.CaseNat]
CaseNat_Rel [definition, in ProgrammingTuringMachines.TM.Code.CaseNat]
CaseNat.NatConstructor [section, in ProgrammingTuringMachines.TM.Code.CaseNat]
CaseOption [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseOption [section, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseOption_Sem [lemma, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseOption_steps [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseOption_Rel [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseOption.codX [variable, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseOption.sig [variable, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseOption.sigX [variable, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseOption.tau [variable, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseOption.X [variable, in ProgrammingTuringMachines.TM.Code.CaseSum]
CasePair [definition, in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair [section, in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair [library]
CasePair_steps_comp [lemma, in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair_T [definition, in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair_steps [definition, in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair_Realise [lemma, in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair_Rel [definition, in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair.cX [variable, in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair.cY [variable, in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair.sigX [variable, in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair.sigY [variable, in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair.X [variable, in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair.Y [variable, in ProgrammingTuringMachines.TM.Code.CasePair]
CaseSum [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum [section, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum [library]
CaseSum_Sem [lemma, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum_steps [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum_Rel [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum.codX [variable, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum.codY [variable, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum.sigX [variable, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum.sigY [variable, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum.SumConstr [section, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum.X [variable, in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum.Y [variable, in ProgrammingTuringMachines.TM.Code.CaseSum]
ChangeAlphabet [definition, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet [section, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet [library]
ChangeAlphabet_Terminates2 [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet_Computes2 [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet_Computes [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet.F [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet.n [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet.pM [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet.retr [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet.sig [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet.tau [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
codable [record, in ProgrammingTuringMachines.TM.Code.Code]
Code [library]
CodeTM [library]
Com [inductive, in ProgrammingTuringMachines.TM.LM.Semantics]
Combinators [library]
Composition [section, in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
Composition.F1 [variable, in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
Composition.F2 [variable, in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
Composition.n [variable, in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
Composition.pM1 [variable, in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
Composition.pM2 [variable, in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
Composition.sig [variable, in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
Computes_Monotone [lemma, in ProgrammingTuringMachines.TM.Code.CodeTM]
Computes_ext [lemma, in ProgrammingTuringMachines.TM.Code.CodeTM]
Computes_T [definition, in ProgrammingTuringMachines.TM.Code.CodeTM]
Computes_Rel [definition, in ProgrammingTuringMachines.TM.Code.CodeTM]
Computes_ChangeAlphabet2.func [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.cZ [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.cY [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.cX [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.Z [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.Y [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.X [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.retr [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.pM [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.F [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.n_tapes [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.tau [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.sig [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2 [section, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.func [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.cY [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.cX [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.Y [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.X [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.retr [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.pM [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.F [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.n_tapes [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.tau [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.sig [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet [section, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes2_Monotone [lemma, in ProgrammingTuringMachines.TM.Code.CodeTM]
Computes2_ext [lemma, in ProgrammingTuringMachines.TM.Code.CodeTM]
Computes2_T [definition, in ProgrammingTuringMachines.TM.Code.CodeTM]
Computes2_Rel [definition, in ProgrammingTuringMachines.TM.Code.CodeTM]
ConsClos [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
ConsClos_Terminates [lemma, in ProgrammingTuringMachines.TM.LM.StepTM]
ConsClos_T [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
ConsClos_steps [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
ConsClos_Realise [lemma, in ProgrammingTuringMachines.TM.LM.StepTM]
ConsClos_Rel [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Constr_varT_Sem [lemma, in ProgrammingTuringMachines.TM.LM.CaseCom]
Constr_varT_steps [definition, in ProgrammingTuringMachines.TM.LM.CaseCom]
Constr_varT_Rel [definition, in ProgrammingTuringMachines.TM.LM.CaseCom]
Constr_varT [definition, in ProgrammingTuringMachines.TM.LM.CaseCom]
Constr_ACom_Sem [lemma, in ProgrammingTuringMachines.TM.LM.CaseCom]
Constr_ACom_steps [definition, in ProgrammingTuringMachines.TM.LM.CaseCom]
Constr_ACom_Rel [definition, in ProgrammingTuringMachines.TM.LM.CaseCom]
Constr_ACom [definition, in ProgrammingTuringMachines.TM.LM.CaseCom]
Constr_cons_steps_comp [lemma, in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_cons_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_cons_steps [definition, in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_cons_Realise [lemma, in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_cons_Rel [definition, in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_cons [definition, in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_nil_Sem [lemma, in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_nil_steps [definition, in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_nil_Rel [definition, in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_nil [definition, in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_None_Sem [lemma, in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_None_steps [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_None [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_None_Rel [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_Some_Sem [lemma, in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_Some_steps [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_Some [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_Some_Rel [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_inr_Sem [lemma, in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_inr_steps [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_inl_Sem [lemma, in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_inl_steps [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_inr [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_inl [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_inr_Rel [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_inl_Rel [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_pair_steps_comp [lemma, in ProgrammingTuringMachines.TM.Code.CasePair]
Constr_pair_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.CasePair]
Constr_pair_T [definition, in ProgrammingTuringMachines.TM.Code.CasePair]
Constr_pair_steps [definition, in ProgrammingTuringMachines.TM.Code.CasePair]
Constr_pair_Realise [lemma, in ProgrammingTuringMachines.TM.Code.CasePair]
Constr_pair [definition, in ProgrammingTuringMachines.TM.Code.CasePair]
Constr_pair_Rel [definition, in ProgrammingTuringMachines.TM.Code.CasePair]
Constr_O_Sem [lemma, in ProgrammingTuringMachines.TM.Code.CaseNat]
Constr_O_steps [definition, in ProgrammingTuringMachines.TM.Code.CaseNat]
Constr_O [definition, in ProgrammingTuringMachines.TM.Code.CaseNat]
Constr_S_Sem [lemma, in ProgrammingTuringMachines.TM.Code.CaseNat]
Constr_S_steps [definition, in ProgrammingTuringMachines.TM.Code.CaseNat]
Constr_S [definition, in ProgrammingTuringMachines.TM.Code.CaseNat]
contains_translate_eq [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
contains_translate_tau [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
contains_translate_tau2 [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
contains_translate_tau1 [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
contains_translate_sig [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Copy [section, in ProgrammingTuringMachines.TM.Code.Copy]
Copy [section, in ProgrammingTuringMachines.TM.Compound.Multi]
Copy [library]
CopyChar [definition, in ProgrammingTuringMachines.TM.Compound.Multi]
CopyChar_Sem [lemma, in ProgrammingTuringMachines.TM.Compound.Multi]
CopyChar_Rel [definition, in ProgrammingTuringMachines.TM.Compound.Multi]
CopySymbols [definition, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols [section, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols [library]
CopySymbols_L_steps_moveleft [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_L_steps_midtape [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_L_steps_local [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_steps_moveright [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_steps_midtape [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_steps_local [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_L_correct_moveleft [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_L_correct_midtape [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_L_correct [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_correct_moveright [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_correct_midtape [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_correct [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_L_Terminates [lemma, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_steps_mirror [lemma, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_L_Realise [lemma, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_L_Rel [definition, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_mirror' [lemma, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_mirror [lemma, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_L [definition, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_Terminates [lemma, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_Realise [lemma, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_true [lemma, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_false [lemma, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_Rel [definition, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_Step_Sem [lemma, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_Step_Rel [definition, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_Step [definition, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols.f [variable, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols.sig [variable, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopyValue [definition, in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue [section, in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_steps_comp [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_steps_comp.I [variable, in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_steps_comp.cX [variable, in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_steps_comp.X [variable, in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_steps_comp.tau [variable, in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_steps_comp.sig [variable, in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_steps_comp [section, in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_steps [definition, in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_Realise [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_Rel [definition, in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue.cX [variable, in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue.sig [variable, in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue.X [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Copy.f [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Copy.f [variable, in ProgrammingTuringMachines.TM.Compound.Multi]
Copy.sig [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Copy.sig [variable, in ProgrammingTuringMachines.TM.Compound.Multi]
Copy.stop [variable, in ProgrammingTuringMachines.TM.Code.Copy]
countMap_zero [lemma, in ProgrammingTuringMachines.TM.Code.Code]
countMap_injective [lemma, in ProgrammingTuringMachines.TM.Code.Code]
cstate [projection, in ProgrammingTuringMachines.TM.TM]
ctapes [projection, in ProgrammingTuringMachines.TM.TM]
current [definition, in ProgrammingTuringMachines.TM.TM]
current_chars [definition, in ProgrammingTuringMachines.TM.TM]
current_chars_mirror_tapes [lemma, in ProgrammingTuringMachines.TM.Combinators.Mirror]
current_chars_select [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
current_chars_surjectTapes [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]


D

Diverge [definition, in ProgrammingTuringMachines.TM.Compound.Multi]
Diverge [section, in ProgrammingTuringMachines.TM.Compound.Multi]
Diverge_Realise [lemma, in ProgrammingTuringMachines.TM.Compound.Multi]
Diverge_Rel [definition, in ProgrammingTuringMachines.TM.Compound.Multi]
Diverge.n [variable, in ProgrammingTuringMachines.TM.Compound.Multi]
Diverge.sig [variable, in ProgrammingTuringMachines.TM.Compound.Multi]
doAct [definition, in ProgrammingTuringMachines.TM.TM]
DoAct [definition, in ProgrammingTuringMachines.TM.Basic.Mono]
DoAct [section, in ProgrammingTuringMachines.TM.Basic.Mono]
doAct_nop [lemma, in ProgrammingTuringMachines.TM.TM]
doAct_multi [definition, in ProgrammingTuringMachines.TM.TM]
doAct_mirror_multi [lemma, in ProgrammingTuringMachines.TM.Combinators.Mirror]
doAct_mirror [lemma, in ProgrammingTuringMachines.TM.Combinators.Mirror]
DoAct_Derived.D [variable, in ProgrammingTuringMachines.TM.Basic.Mono]
DoAct_Derived.c [variable, in ProgrammingTuringMachines.TM.Basic.Mono]
DoAct_Derived.sig [variable, in ProgrammingTuringMachines.TM.Basic.Mono]
DoAct_Derived [section, in ProgrammingTuringMachines.TM.Basic.Mono]
DoAct_Sem [lemma, in ProgrammingTuringMachines.TM.Basic.Mono]
DoAct_Rel [definition, in ProgrammingTuringMachines.TM.Basic.Mono]
DoAct_TM [definition, in ProgrammingTuringMachines.TM.Basic.Mono]
doAct_select [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
doAct_surject [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
DoAct.act [variable, in ProgrammingTuringMachines.TM.Basic.Mono]
DoAct.c [variable, in ProgrammingTuringMachines.TM.Basic.Mono]
DoAct.sig [variable, in ProgrammingTuringMachines.TM.Basic.Mono]


E

encode [projection, in ProgrammingTuringMachines.TM.Code.Code]
Encode_Heap [instance, in ProgrammingTuringMachines.TM.LM.Alphabets]
Encode_HEntr [instance, in ProgrammingTuringMachines.TM.LM.Alphabets]
Encode_HEntr' [instance, in ProgrammingTuringMachines.TM.LM.Alphabets]
Encode_HClos [instance, in ProgrammingTuringMachines.TM.LM.Alphabets]
Encode_Prog [instance, in ProgrammingTuringMachines.TM.LM.Alphabets]
Encode_Com_hasSize [lemma, in ProgrammingTuringMachines.TM.LM.Alphabets]
Encode_Com_size [definition, in ProgrammingTuringMachines.TM.LM.Alphabets]
Encode_Com [instance, in ProgrammingTuringMachines.TM.LM.Alphabets]
Encode_ACom [instance, in ProgrammingTuringMachines.TM.LM.Alphabets]
Encode_nat_eq_nil [lemma, in ProgrammingTuringMachines.TM.Code.Code]
Encode_nat_hasSize [lemma, in ProgrammingTuringMachines.TM.Code.Code]
Encode_nat [instance, in ProgrammingTuringMachines.TM.Code.Code]
Encode_nat [section, in ProgrammingTuringMachines.TM.Code.Code]
Encode_list_hasSize [lemma, in ProgrammingTuringMachines.TM.Code.Code]
Encode_list_size [definition, in ProgrammingTuringMachines.TM.Code.Code]
Encode_list_neq_nil [lemma, in ProgrammingTuringMachines.TM.Code.Code]
encode_list_neq_nil [lemma, in ProgrammingTuringMachines.TM.Code.Code]
Encode_list_app [lemma, in ProgrammingTuringMachines.TM.Code.Code]
encode_list_app [lemma, in ProgrammingTuringMachines.TM.Code.Code]
Encode_list [instance, in ProgrammingTuringMachines.TM.Code.Code]
encode_list [definition, in ProgrammingTuringMachines.TM.Code.Code]
Encode_list.cX [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_list.X [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_list.sigX [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_list [section, in ProgrammingTuringMachines.TM.Code.Code]
Encode_option_hasSize [lemma, in ProgrammingTuringMachines.TM.Code.Code]
Encode_option_size [definition, in ProgrammingTuringMachines.TM.Code.Code]
Encode_option [instance, in ProgrammingTuringMachines.TM.Code.Code]
Encode_option.cX [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_option.X [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_option.sigX [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_option [section, in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair_hasSize [lemma, in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair_size [definition, in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair [instance, in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair.cY [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair.cX [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair.Y [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair.X [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair.sigY [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair.sigX [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair [section, in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum_hasSize [lemma, in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum_size [definition, in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum [instance, in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum.cY [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum.cX [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum.sigY [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum.sigX [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum.Y [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum.X [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum [section, in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_comp [lemma, in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_comp.I2 [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_comp.I1 [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_comp.cX [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_comp.sig3 [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_comp.sig2 [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_comp.sig1 [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_comp.X [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_comp [section, in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_hasSize [lemma, in ProgrammingTuringMachines.TM.Code.Code]
Encode_map [instance, in ProgrammingTuringMachines.TM.Code.Code]
Encode_map.inj [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_map.cX [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_map.tau [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_map.sig [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_map.X [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_map [section, in ProgrammingTuringMachines.TM.Code.Code]
Encode_Finite_hasSize [lemma, in ProgrammingTuringMachines.TM.Code.Code]
Encode_Finite [instance, in ProgrammingTuringMachines.TM.Code.Code]
Encode_Finite.sig [variable, in ProgrammingTuringMachines.TM.Code.Code]
Encode_Finite [section, in ProgrammingTuringMachines.TM.Code.Code]
Encode_Fin_hasSize [lemma, in ProgrammingTuringMachines.TM.Code.Code]
Encode_Fin [instance, in ProgrammingTuringMachines.TM.Code.Code]
Encode_bool_hasSize [lemma, in ProgrammingTuringMachines.TM.Code.Code]
Encode_bool [instance, in ProgrammingTuringMachines.TM.Code.Code]
Encode_unit_hasSize [lemma, in ProgrammingTuringMachines.TM.Code.Code]
Encode_unit [instance, in ProgrammingTuringMachines.TM.Code.Code]
eqrel [definition, in ProgrammingTuringMachines.TM.Relations]
eqrel_eq [instance, in ProgrammingTuringMachines.TM.Relations]
eqrel_pre [instance, in ProgrammingTuringMachines.TM.Relations]
Eq_in_equivalence [instance, in ProgrammingTuringMachines.TM.Relations]
Eq_in [definition, in ProgrammingTuringMachines.TM.Relations]
execTM [definition, in ProgrammingTuringMachines.TM.TM]
execTM_p [definition, in ProgrammingTuringMachines.TM.TM]


F

fill [definition, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Fill [section, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
fill_default_not_index [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
fill_default [definition, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
fill_not_index [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
fill_correct_nth [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Fill.m [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Fill.n [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Fill.X [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
FinR [definition, in ProgrammingTuringMachines.TM.Prelim]
Fin_R_fillive [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Fin_L_fillive [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Fix_Sig.Computes2.Computes2_Ext.mon [variable, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes2.Computes2_Ext.r2 [variable, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes2.Computes2_Ext.r1 [variable, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes2.Computes2_Ext.ext_fun [variable, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes2.Computes2_Ext.f' [variable, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes2.Computes2_Ext.f [variable, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes2.Computes2_Ext [section, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes2.F [variable, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes2.n [variable, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes2 [section, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes.Computes_Ext.mon [variable, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes.Computes_Ext.r2 [variable, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes.Computes_Ext.r1 [variable, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes.Computes_Ext.ext_fun [variable, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes.Computes_Ext.f' [variable, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes.Computes_Ext.f [variable, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes.Computes_Ext [section, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes.F [variable, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes.n [variable, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes [section, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.InitTape [section, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Encodes_Ext [section, in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ≂( _ ) _ [notation, in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ≂ _ [notation, in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ≃( _ ) _ [notation, in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ≃ _ [notation, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Tape_Contains [section, in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ^+ (type_scope) [notation, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.sig [variable, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig [section, in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sigma.sig [variable, in ProgrammingTuringMachines.TM.TM]
Fix_Sigma [section, in ProgrammingTuringMachines.TM.TM]
V _ [notation, in ProgrammingTuringMachines.TM.Relations]
Fix_X2.n [variable, in ProgrammingTuringMachines.TM.Relations]
Fix_X2.Z [variable, in ProgrammingTuringMachines.TM.Relations]
Fix_X2.Y [variable, in ProgrammingTuringMachines.TM.Relations]
Fix_X2.X [variable, in ProgrammingTuringMachines.TM.Relations]
Fix_X2 [section, in ProgrammingTuringMachines.TM.Relations]
functional [definition, in ProgrammingTuringMachines.TM.Relations]


H

HAdd [definition, in ProgrammingTuringMachines.TM.LM.Semantics]
halt [projection, in ProgrammingTuringMachines.TM.TM]
haltConf [definition, in ProgrammingTuringMachines.TM.TM]
HaltingProblem [lemma, in ProgrammingTuringMachines.TM.LM.HaltingProblem]
HaltingProblem [library]
Halts [definition, in ProgrammingTuringMachines.TM.LM.HaltingProblem]
halts [definition, in ProgrammingTuringMachines.TM.LM.Semantics]
halts_k [definition, in ProgrammingTuringMachines.TM.LM.Semantics]
halt_state_steps_k [lemma, in ProgrammingTuringMachines.TM.LM.Semantics]
halt_state_steps [lemma, in ProgrammingTuringMachines.TM.LM.Semantics]
halt_state_dec [instance, in ProgrammingTuringMachines.TM.LM.Semantics]
halt_state_is_halt_state [lemma, in ProgrammingTuringMachines.TM.LM.Semantics]
halt_state [definition, in ProgrammingTuringMachines.TM.LM.Semantics]
halt_comp [lemma, in ProgrammingTuringMachines.TM.Combinators.While]
halt_conf_liftL [lemma, in ProgrammingTuringMachines.TM.Combinators.Switch]
halt_liftL [definition, in ProgrammingTuringMachines.TM.Combinators.Switch]
HClos [definition, in ProgrammingTuringMachines.TM.LM.Semantics]
Heap [definition, in ProgrammingTuringMachines.TM.LM.Semantics]
HEntr [definition, in ProgrammingTuringMachines.TM.LM.Semantics]


I

Id [definition, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Id [section, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Id.F [variable, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Id.n [variable, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Id.pM [variable, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Id.sig [variable, in ProgrammingTuringMachines.TM.Combinators.Combinators]
If [definition, in ProgrammingTuringMachines.TM.Combinators.If]
If [section, in ProgrammingTuringMachines.TM.Combinators.If]
If [library]
If_RealiseIn [lemma, in ProgrammingTuringMachines.TM.Combinators.If]
If_TerminatesIn [lemma, in ProgrammingTuringMachines.TM.Combinators.If]
If_Realise [lemma, in ProgrammingTuringMachines.TM.Combinators.If]
If.F [variable, in ProgrammingTuringMachines.TM.Combinators.If]
If.n [variable, in ProgrammingTuringMachines.TM.Combinators.If]
If.pM1 [variable, in ProgrammingTuringMachines.TM.Combinators.If]
If.pM2 [variable, in ProgrammingTuringMachines.TM.Combinators.If]
If.pM3 [variable, in ProgrammingTuringMachines.TM.Combinators.If]
If.sig [variable, in ProgrammingTuringMachines.TM.Combinators.If]
ignoreParam [definition, in ProgrammingTuringMachines.TM.Relations]
initc [definition, in ProgrammingTuringMachines.TM.TM]
initRight [definition, in ProgrammingTuringMachines.TM.Code.CodeTM]
initRight_isRight [lemma, in ProgrammingTuringMachines.TM.Code.CodeTM]
initTapes [definition, in ProgrammingTuringMachines.TM.LM.HaltingProblem]
initValue [definition, in ProgrammingTuringMachines.TM.Code.CodeTM]
initValue_contains [lemma, in ProgrammingTuringMachines.TM.Code.CodeTM]
InjectSurject [section, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
InjectSurject.def [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
InjectSurject.inj [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
InjectSurject.sig [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
InjectSurject.tau [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
injectSymbols [definition, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
injectTape [abbreviation, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
injectTape [definition, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
InjectTape [section, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
injectTapes [definition, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
InjectTape.f [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
InjectTape.sig [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
InjectTape.tau [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
inject_surject [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
in_encode_retract [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
IsNil [definition, in ProgrammingTuringMachines.TM.Code.CaseList]
IsNil_Sem [lemma, in ProgrammingTuringMachines.TM.Code.CaseList]
IsNil_steps [definition, in ProgrammingTuringMachines.TM.Code.CaseList]
IsNil_Rel [definition, in ProgrammingTuringMachines.TM.Code.CaseList]
isRight [definition, in ProgrammingTuringMachines.TM.Code.CodeTM]
IsRight [section, in ProgrammingTuringMachines.TM.Code.CodeTM]
isRight_isRight_size [lemma, in ProgrammingTuringMachines.TM.Code.CodeTM]
isRight_size_right [lemma, in ProgrammingTuringMachines.TM.Code.CodeTM]
isRight_size_left [lemma, in ProgrammingTuringMachines.TM.Code.CodeTM]
isRight_right [lemma, in ProgrammingTuringMachines.TM.Code.CodeTM]
isRight_size_monotone [lemma, in ProgrammingTuringMachines.TM.Code.CodeTM]
isRight_size_isRight [lemma, in ProgrammingTuringMachines.TM.Code.CodeTM]
isRight_size [definition, in ProgrammingTuringMachines.TM.Code.CodeTM]
isStart [definition, in ProgrammingTuringMachines.TM.Code.Copy]
isStop [definition, in ProgrammingTuringMachines.TM.Code.Copy]
is_halt_state_correct [lemma, in ProgrammingTuringMachines.TM.LM.Semantics]
is_halt_state_halt [lemma, in ProgrammingTuringMachines.TM.LM.Semantics]
is_halt_state [definition, in ProgrammingTuringMachines.TM.LM.Semantics]


J

JumpTarget [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
jumpTarget [definition, in ProgrammingTuringMachines.TM.LM.Semantics]
JumpTargetTM [library]
JumpTarget_Terminates [lemma, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_T [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_steps [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Realise [lemma, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Rel [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Loop_Terminates [lemma, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Loop_T [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Loop_steps [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Loop_Realise [lemma, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Loop_Rel [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Loop [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
jumpTarget_k [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Step_Terminates [lemma, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Step_T [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Step_steps [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Step_steps_CaseList [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Step_steps_CaseCom [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Step_Realise [lemma, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Step_Rel [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Step [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]


L

L [constructor, in ProgrammingTuringMachines.TM.TM]
lamAT [constructor, in ProgrammingTuringMachines.TM.LM.Alphabets]
lamT [constructor, in ProgrammingTuringMachines.TM.LM.Semantics]
left [definition, in ProgrammingTuringMachines.TM.TM]
leftof [constructor, in ProgrammingTuringMachines.TM.TM]
Lenght [section, in ProgrammingTuringMachines.TM.Code.ListTM]
Lenght.cX [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Lenght.retr1 [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Lenght.retr2 [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Lenght.sig [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Lenght.sigX [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Lenght.X [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Length [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
Length_T [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Length_steps [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Computes [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Loop_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Loop_T [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Loop_steps [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Loop_Realise [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Loop_Rel [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Loop [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Step_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Step_T [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Step_steps [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Step_Realise [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Step_Rel [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Step [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
LiftAlphabet [definition, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet [section, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet [library]
LiftAlphabet_RealiseIn [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet_TerminatesIn [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet_unlift [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet_Realise [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet_lift [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet_comp_step [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet_TM [definition, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet.def [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet.F [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet.Inj [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet.n [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet.pMSig [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet.sig [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet.tau [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
Lifting [library]
LiftNM [section, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftNM.F [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftNM.I [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftNM.I_dupfree [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftNM.m [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftNM.n [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftNM.pM [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftNM.sig [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes [definition, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes [library]
LiftTapes_RealiseIn [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Terminates [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_unlift [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Realise [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_eq [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_comp_eq [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_lift [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_comp_step [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_TM [definition, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_trans [definition, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_T [definition, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Rel.T [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Rel [definition, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_eq_Rel [definition, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_select_Rel [definition, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Rel.R [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Rel.I [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Rel.n [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Rel.m [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Rel.F [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Rel.sig [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Rel [section, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
lift_initc [lemma, in ProgrammingTuringMachines.TM.Combinators.Switch]
lift_confR [definition, in ProgrammingTuringMachines.TM.Combinators.Switch]
lift_confL [definition, in ProgrammingTuringMachines.TM.Combinators.Switch]
lift_trans [definition, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
lift_sigma_tau_T [definition, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
lift_sigma_tau_Rel [definition, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
lift_sigma_tau.F [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
lift_sigma_tau.def [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
lift_sigma_tau.g [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
lift_sigma_tau.tau [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
lift_sigma_tau.sig [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
lift_sigma_tau.n [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
lift_sigma_tau [section, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
ListStuff [section, in ProgrammingTuringMachines.TM.Code.ListTM]
ListStuff.X [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
ListTM [library]
llength [definition, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
llength [definition, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
llength' [definition, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
lookup [definition, in ProgrammingTuringMachines.TM.LM.Semantics]
Lookup [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup [section, in ProgrammingTuringMachines.TM.LM.LookupTM]
LookupTM [library]
lookup_eq [lemma, in ProgrammingTuringMachines.TM.LM.Semantics]
Lookup_Terminates [lemma, in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_T [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_steps [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Realise [lemma, in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Rel [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Step_Terminates [lemma, in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Step_T [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Step_steps [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Step_steps_Nth' [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Step_steps_CaseOption [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Step_steps_CaseNat [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Step_Realise [lemma, in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Step_Rel [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Step [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup.retr_heap_lookup [variable, in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup.retr_clos_lookup [variable, in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup.sigLookup [variable, in ProgrammingTuringMachines.TM.LM.LookupTM]
Loop [definition, in ProgrammingTuringMachines.TM.LM.HaltingProblem]
loop [definition, in ProgrammingTuringMachines.TM.Prelim]
Loop [section, in ProgrammingTuringMachines.TM.Prelim]
LoopLift [section, in ProgrammingTuringMachines.TM.Prelim]
LoopLift.A [variable, in ProgrammingTuringMachines.TM.Prelim]
LoopLift.B [variable, in ProgrammingTuringMachines.TM.Prelim]
LoopLift.f [variable, in ProgrammingTuringMachines.TM.Prelim]
LoopLift.f' [variable, in ProgrammingTuringMachines.TM.Prelim]
LoopLift.h [variable, in ProgrammingTuringMachines.TM.Prelim]
LoopLift.halt_lift_comp [variable, in ProgrammingTuringMachines.TM.Prelim]
LoopLift.h' [variable, in ProgrammingTuringMachines.TM.Prelim]
LoopLift.lift [variable, in ProgrammingTuringMachines.TM.Prelim]
LoopLift.step_lift_comp [variable, in ProgrammingTuringMachines.TM.Prelim]
loopM [definition, in ProgrammingTuringMachines.TM.TM]
LoopMerge [section, in ProgrammingTuringMachines.TM.Prelim]
LoopMerge.A [variable, in ProgrammingTuringMachines.TM.Prelim]
LoopMerge.f [variable, in ProgrammingTuringMachines.TM.Prelim]
LoopMerge.h [variable, in ProgrammingTuringMachines.TM.Prelim]
LoopMerge.halt_comp [variable, in ProgrammingTuringMachines.TM.Prelim]
LoopMerge.h' [variable, in ProgrammingTuringMachines.TM.Prelim]
Loop_Terminates [lemma, in ProgrammingTuringMachines.TM.LM.HaltingProblem]
Loop_T [definition, in ProgrammingTuringMachines.TM.LM.HaltingProblem]
Loop_steps [definition, in ProgrammingTuringMachines.TM.LM.HaltingProblem]
Loop_Realise [lemma, in ProgrammingTuringMachines.TM.LM.HaltingProblem]
Loop_Rel [definition, in ProgrammingTuringMachines.TM.LM.HaltingProblem]
loop_split [lemma, in ProgrammingTuringMachines.TM.Prelim]
loop_merge [lemma, in ProgrammingTuringMachines.TM.Prelim]
loop_unlift [lemma, in ProgrammingTuringMachines.TM.Prelim]
loop_lift [lemma, in ProgrammingTuringMachines.TM.Prelim]
loop_monotone [lemma, in ProgrammingTuringMachines.TM.Prelim]
loop_eq_0 [lemma, in ProgrammingTuringMachines.TM.Prelim]
loop_0 [lemma, in ProgrammingTuringMachines.TM.Prelim]
loop_fulfills [lemma, in ProgrammingTuringMachines.TM.Prelim]
loop_injective [lemma, in ProgrammingTuringMachines.TM.Prelim]
loop_step [lemma, in ProgrammingTuringMachines.TM.Prelim]
loop_map [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
loop_map.step_map_comp [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
loop_map.g [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
loop_map.h [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
loop_map.f [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
loop_map.B [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
loop_map.A [variable, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
loop_map [section, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Loop.A [variable, in ProgrammingTuringMachines.TM.Prelim]
Loop.f [variable, in ProgrammingTuringMachines.TM.Prelim]
Loop.p [variable, in ProgrammingTuringMachines.TM.Prelim]


M

Map [section, in ProgrammingTuringMachines.TM.Prelim]
MapCode [section, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
MapCode.retr [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
MapCode.sig [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
MapCode.tau [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
f' [notation, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
g' [notation, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
MapSum [definition, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum [section, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum_steps [definition, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum_Computes [lemma, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.codX [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.codY [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.codZ [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.f [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.g [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.M1 [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.M1_Terminates [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.M1_steps [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.M1_Computes [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.M2 [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.M2_Terminates [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.M2_steps [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.M2_Computes [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.n [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.retr_sigSum_sigMap [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.retr_sigM_sigMap [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.retr_sigZ_sigM [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.retr_sigY_sigM [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.retr_sigX_sigM [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.sigM [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.sigMap [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.sigX [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.sigY [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.sigZ [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.X [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.Y [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.Z [variable, in ProgrammingTuringMachines.TM.Code.SumTM]
mapTape [definition, in ProgrammingTuringMachines.TM.TM]
MapTape [section, in ProgrammingTuringMachines.TM.TM]
mapTapes [definition, in ProgrammingTuringMachines.TM.TM]
mapTape_isRight [lemma, in ProgrammingTuringMachines.TM.Code.CodeTM]
mapTape_local [lemma, in ProgrammingTuringMachines.TM.TM]
mapTape_id [lemma, in ProgrammingTuringMachines.TM.TM]
mapTape_ext [lemma, in ProgrammingTuringMachines.TM.TM]
mapTape_mapTape [lemma, in ProgrammingTuringMachines.TM.TM]
mapTape_inv_midtape [lemma, in ProgrammingTuringMachines.TM.TM]
mapTape_inv_leftof [lemma, in ProgrammingTuringMachines.TM.TM]
mapTape_inv_rightof [lemma, in ProgrammingTuringMachines.TM.TM]
mapTape_inv_niltap [lemma, in ProgrammingTuringMachines.TM.TM]
mapTape_move_right [lemma, in ProgrammingTuringMachines.TM.TM]
mapTape_move_left [lemma, in ProgrammingTuringMachines.TM.TM]
mapTape_right [lemma, in ProgrammingTuringMachines.TM.TM]
mapTape_left [lemma, in ProgrammingTuringMachines.TM.TM]
mapTape_current [lemma, in ProgrammingTuringMachines.TM.TM]
MapTape.g [variable, in ProgrammingTuringMachines.TM.TM]
MapTape.sig [variable, in ProgrammingTuringMachines.TM.TM]
MapTape.tau [variable, in ProgrammingTuringMachines.TM.TM]
map_snd [definition, in ProgrammingTuringMachines.TM.Prelim]
map_fst [definition, in ProgrammingTuringMachines.TM.Prelim]
map_inr [definition, in ProgrammingTuringMachines.TM.Prelim]
map_inl [definition, in ProgrammingTuringMachines.TM.Prelim]
map_opt [definition, in ProgrammingTuringMachines.TM.Prelim]
map_length_eq [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
map_removelast [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
map_sum [definition, in ProgrammingTuringMachines.TM.Code.SumTM]
map_act [definition, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
Map.X [variable, in ProgrammingTuringMachines.TM.Prelim]
Map.Y [variable, in ProgrammingTuringMachines.TM.Prelim]
Map.Z [variable, in ProgrammingTuringMachines.TM.Prelim]
Match [abbreviation, in ProgrammingTuringMachines.TM.Combinators.Switch]
MATCH [abbreviation, in ProgrammingTuringMachines.TM.Combinators.Switch]
MatchTapes [section, in ProgrammingTuringMachines.TM.TM]
MatchTapes.sig [variable, in ProgrammingTuringMachines.TM.TM]
mconfig [record, in ProgrammingTuringMachines.TM.TM]
midtape [constructor, in ProgrammingTuringMachines.TM.TM]
midtape_tape_local_l_cons_right [lemma, in ProgrammingTuringMachines.TM.TM]
midtape_tape_local_l_cons [lemma, in ProgrammingTuringMachines.TM.TM]
midtape_tape_local_cons_left [lemma, in ProgrammingTuringMachines.TM.TM]
midtape_tape_local_cons [lemma, in ProgrammingTuringMachines.TM.TM]
Mirror [definition, in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mirror [section, in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mirror [library]
mirrorConf [definition, in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirrorConf_injective [lemma, in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirrorConf_involution [lemma, in ProgrammingTuringMachines.TM.Combinators.Mirror]
MirrorTape [section, in ProgrammingTuringMachines.TM.TM]
MirrorTape.n [variable, in ProgrammingTuringMachines.TM.TM]
MirrorTape.sig [variable, in ProgrammingTuringMachines.TM.TM]
MirrorTM [definition, in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirror_tape_move_right' [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tape_move_left' [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tapes_nth [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_move_involution [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_move [definition, in ProgrammingTuringMachines.TM.TM]
mirror_tapes_injective [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tapes_involution [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tapes [definition, in ProgrammingTuringMachines.TM.TM]
mirror_tape_inv_niltape' [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tape_inv_rightof' [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tape_inv_leftof' [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tape_inv_midtape' [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tape_inv_niltape [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tape_inv_rightof [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tape_inv_leftof [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tape_inv_midtape [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tape_move_right [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tape_move_left [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tape_injective [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tape_involution [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tape_current [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tape_right [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tape_left [lemma, in ProgrammingTuringMachines.TM.TM]
mirror_tape [definition, in ProgrammingTuringMachines.TM.TM]
Mirror_RealiseIn [lemma, in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mirror_Terminates [lemma, in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mirror_T [definition, in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mirror_Realise [lemma, in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mirror_Rel [definition, in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirror_unlift [lemma, in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirror_lift [lemma, in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirror_step [lemma, in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mirror_trans [definition, in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirror_acts_involution [lemma, in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirror_act_involution [lemma, in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirror_acts [definition, in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirror_act [definition, in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mirror.F [variable, in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mirror.n [variable, in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mirror.pM [variable, in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mirror.sig [variable, in ProgrammingTuringMachines.TM.Combinators.Mirror]
mk_mconfig [constructor, in ProgrammingTuringMachines.TM.TM]
Mk_R_p [definition, in ProgrammingTuringMachines.TM.Basic.Mono]
Mk_Mono.R [variable, in ProgrammingTuringMachines.TM.Basic.Mono]
Mk_Mono.F [variable, in ProgrammingTuringMachines.TM.Basic.Mono]
Mk_Mono_TM [definition, in ProgrammingTuringMachines.TM.Basic.Mono]
Mk_Mono.fin [variable, in ProgrammingTuringMachines.TM.Basic.Mono]
Mk_Mono.init [variable, in ProgrammingTuringMachines.TM.Basic.Mono]
Mk_Mono.mono_trans [variable, in ProgrammingTuringMachines.TM.Basic.Mono]
Mk_Mono.states [variable, in ProgrammingTuringMachines.TM.Basic.Mono]
Mk_Mono.sig [variable, in ProgrammingTuringMachines.TM.Basic.Mono]
Mk_Mono [section, in ProgrammingTuringMachines.TM.Basic.Mono]
Mono [library]
Mono_Nop.sig [variable, in ProgrammingTuringMachines.TM.Basic.Null]
Mono_Nop [section, in ProgrammingTuringMachines.TM.Basic.Null]
move [inductive, in ProgrammingTuringMachines.TM.TM]
Move [section, in ProgrammingTuringMachines.TM.Code.Copy]
Move [definition, in ProgrammingTuringMachines.TM.Basic.Mono]
MoveLeft [definition, in ProgrammingTuringMachines.TM.Code.Copy]
MoveLeft_steps_comp [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveLeft_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveLeft_steps [definition, in ProgrammingTuringMachines.TM.Code.Copy]
MoveLeft_Realise [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveLeft_Rel [definition, in ProgrammingTuringMachines.TM.Code.Copy]
MovePar [definition, in ProgrammingTuringMachines.TM.Compound.Multi]
MovePar [section, in ProgrammingTuringMachines.TM.Compound.Multi]
MovePar_Sem [lemma, in ProgrammingTuringMachines.TM.Compound.Multi]
MovePar_R [definition, in ProgrammingTuringMachines.TM.Compound.Multi]
MovePar.D1 [variable, in ProgrammingTuringMachines.TM.Compound.Multi]
MovePar.D2 [variable, in ProgrammingTuringMachines.TM.Compound.Multi]
MovePar.sig [variable, in ProgrammingTuringMachines.TM.Compound.Multi]
MoveRight [definition, in ProgrammingTuringMachines.TM.Code.Copy]
MoveRight_steps_comp [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveRight_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveRight_steps [definition, in ProgrammingTuringMachines.TM.Code.Copy]
MoveRight_Realise [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveRight_Rel [definition, in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol [definition, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol [section, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol [library]
MoveToSymbol_L_steps_moveleft [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_L_steps_midtape [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_L_steps_local [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_steps_moveright [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_steps_midtape [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_steps_local [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_L_correct_moveleft [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_L_correct_midtape [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_L_correct [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_correct_moveright [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_correct_midtape [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_correct [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_L_Terminates [lemma, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_steps_mirror [lemma, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_L_Realise [lemma, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_L_Rel [definition, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_mirror' [lemma, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_mirror [lemma, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_L [definition, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Terminates [lemma, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Realise [lemma, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Rel [definition, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_skip [lemma, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Step_Fun_M2_true [lemma, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Step_false [lemma, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Step_true [lemma, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Step_None [lemma, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Step_Fun_M2_None [lemma, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Step_Sem [lemma, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Step_Rel [definition, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Step_Fun [definition, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Step [definition, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol.f [variable, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol.g [variable, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol.sig [variable, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveValue [definition, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue [section, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps_comp [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps_comp.I2 [variable, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps_comp.I1 [variable, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps_comp.cY [variable, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps_comp.cX [variable, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps_comp.Y [variable, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps_comp.X [variable, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps_comp.tau [variable, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps_comp.sig [variable, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps_comp [section, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps [definition, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_Realise [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_Rel [definition, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue.cX [variable, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue.cY [variable, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue.sig [variable, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue.X [variable, in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue.Y [variable, in ProgrammingTuringMachines.TM.Code.Copy]
move_finC [instance, in ProgrammingTuringMachines.TM.TM]
move_eq_dec [instance, in ProgrammingTuringMachines.TM.TM]
Move_steps_comp.I [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Move_steps_comp.cX [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Move_steps_comp.X [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Move_steps_comp.tau [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Move_steps_comp.sig [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Move_steps_comp [section, in ProgrammingTuringMachines.TM.Code.Copy]
Move_Sem [lemma, in ProgrammingTuringMachines.TM.Basic.Mono]
Move_Rel [definition, in ProgrammingTuringMachines.TM.Basic.Mono]
Move.cX [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Move.sig [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Move.X [variable, in ProgrammingTuringMachines.TM.Code.Copy]
mTM [record, in ProgrammingTuringMachines.TM.TM]
Mult [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Multi [library]
Mult_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_steps [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Main_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Main_steps [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Loop_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Loop_steps [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Step_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Step_steps [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Computes [lemma, in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Main_Realise [lemma, in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Main_Rel [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Loop_Realise [lemma, in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Loop_Rel [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Step_Realise [lemma, in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Step_Rel [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Main [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Loop [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Step [definition, in ProgrammingTuringMachines.TM.Code.NatTM]
M1 [definition, in ProgrammingTuringMachines.TM.Code.CaseList]
M1 [abbreviation, in ProgrammingTuringMachines.TM.Combinators.Switch]
M1_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.CaseList]
M1_Realise [lemma, in ProgrammingTuringMachines.TM.Code.CaseList]
M1_Rel [definition, in ProgrammingTuringMachines.TM.Code.CaseList]


N

N [constructor, in ProgrammingTuringMachines.TM.TM]
NatTM [library]
niltape [constructor, in ProgrammingTuringMachines.TM.TM]
Nop [definition, in ProgrammingTuringMachines.TM.Compound.Multi]
Nop [section, in ProgrammingTuringMachines.TM.Compound.Multi]
nop_action [definition, in ProgrammingTuringMachines.TM.TM]
Nop_Action.sig [variable, in ProgrammingTuringMachines.TM.TM]
Nop_Action.n [variable, in ProgrammingTuringMachines.TM.TM]
Nop_Action [section, in ProgrammingTuringMachines.TM.TM]
Nop_Sem [lemma, in ProgrammingTuringMachines.TM.Compound.Multi]
Nop_Rel [definition, in ProgrammingTuringMachines.TM.Compound.Multi]
Nop.n [variable, in ProgrammingTuringMachines.TM.Compound.Multi]
Nop.sig [variable, in ProgrammingTuringMachines.TM.Compound.Multi]
not_index [definition, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Nth [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth [section, in ProgrammingTuringMachines.TM.Code.ListTM]
nth_map2' [lemma, in ProgrammingTuringMachines.TM.TM]
nth_map' [lemma, in ProgrammingTuringMachines.TM.TM]
Nth_Computes [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth_Loop_Realise [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth_Loop [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth_Loop_Rel [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth_Step_Realise [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth_Step [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth_Step_Rel [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth' [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth' [section, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_T [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_steps [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Realise [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Rel [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Loop_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Loop_T [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Loop_steps [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Loop_Realise [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Loop [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Loop_Rel [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Step_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Step_T [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Step_steps [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Step_Realise [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Step [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Step_Rel [definition, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'.cX [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'.retr1 [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'.retr2 [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'.sig [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'.sigX [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'.X [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth.cX [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth.retr1 [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth.retr2 [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth.retr3 [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth.sig [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth.sigX [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Nth.X [variable, in ProgrammingTuringMachines.TM.Code.ListTM]
Null [definition, in ProgrammingTuringMachines.TM.Basic.Null]
Null [library]
NullTM [definition, in ProgrammingTuringMachines.TM.Basic.Null]
Null_Sem [lemma, in ProgrammingTuringMachines.TM.Basic.Null]
Null_Rel [definition, in ProgrammingTuringMachines.TM.Basic.Null]


O

opt_to_sum [definition, in ProgrammingTuringMachines.TM.Code.CaseSum]
OtherWhileRel [section, in ProgrammingTuringMachines.TM.Combinators.While]
OtherWhileRel.F [variable, in ProgrammingTuringMachines.TM.Combinators.While]
OtherWhileRel.n [variable, in ProgrammingTuringMachines.TM.Combinators.While]
OtherWhileRel.R [variable, in ProgrammingTuringMachines.TM.Combinators.While]
OtherWhileRel.sig [variable, in ProgrammingTuringMachines.TM.Combinators.While]
O_Rel [definition, in ProgrammingTuringMachines.TM.Code.CaseNat]


P

pair_eq [lemma, in ProgrammingTuringMachines.TM.Code.CasePair]
pair_eq [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
plus' [definition, in ProgrammingTuringMachines.TM.Prelim]
pow [inductive, in ProgrammingTuringMachines.TM.Relations]
pow_plus [lemma, in ProgrammingTuringMachines.TM.Relations]
pow_S [constructor, in ProgrammingTuringMachines.TM.Relations]
pow_0 [constructor, in ProgrammingTuringMachines.TM.Relations]
pRel [definition, in ProgrammingTuringMachines.TM.TM]
Prelim [library]
Pro [definition, in ProgrammingTuringMachines.TM.LM.Semantics]
ProgrammingTools [library]
pTM [definition, in ProgrammingTuringMachines.TM.TM]
put [definition, in ProgrammingTuringMachines.TM.LM.Semantics]
Put [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Put_Terminates [lemma, in ProgrammingTuringMachines.TM.LM.StepTM]
Put_T [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Put_steps [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Put_Realise [lemma, in ProgrammingTuringMachines.TM.LM.StepTM]
Put_Rel [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
p1 [abbreviation, in ProgrammingTuringMachines.TM.Combinators.Switch]


R

R [constructor, in ProgrammingTuringMachines.TM.TM]
rcomp [definition, in ProgrammingTuringMachines.TM.Relations]
ReadChar [section, in ProgrammingTuringMachines.TM.Compound.Multi]
ReadChar [definition, in ProgrammingTuringMachines.TM.Basic.Mono]
ReadChar [section, in ProgrammingTuringMachines.TM.Basic.Mono]
ReadChar_at_Sem [lemma, in ProgrammingTuringMachines.TM.Compound.Multi]
ReadChar_at_Rel [definition, in ProgrammingTuringMachines.TM.Compound.Multi]
ReadChar_at [definition, in ProgrammingTuringMachines.TM.Compound.Multi]
ReadChar_Sem [definition, in ProgrammingTuringMachines.TM.Basic.Mono]
ReadChar_Rel [definition, in ProgrammingTuringMachines.TM.Basic.Mono]
ReadChar_TM [definition, in ProgrammingTuringMachines.TM.Basic.Mono]
ReadChar.k [variable, in ProgrammingTuringMachines.TM.Compound.Multi]
ReadChar.n [variable, in ProgrammingTuringMachines.TM.Compound.Multi]
ReadChar.sig [variable, in ProgrammingTuringMachines.TM.Compound.Multi]
ReadChar.sig [variable, in ProgrammingTuringMachines.TM.Basic.Mono]
Realise [definition, in ProgrammingTuringMachines.TM.TM]
RealiseIn [definition, in ProgrammingTuringMachines.TM.TM]
RealiseIn_TerminatesIn [lemma, in ProgrammingTuringMachines.TM.TM]
RealiseIn_Realise [lemma, in ProgrammingTuringMachines.TM.TM]
RealiseIn_split [lemma, in ProgrammingTuringMachines.TM.TM]
RealiseIn_monotone' [lemma, in ProgrammingTuringMachines.TM.TM]
RealiseIn_monotone [lemma, in ProgrammingTuringMachines.TM.TM]
Realise_strengthen [lemma, in ProgrammingTuringMachines.TM.TM]
Realise_total [lemma, in ProgrammingTuringMachines.TM.TM]
Realise_monotone [lemma, in ProgrammingTuringMachines.TM.TM]
Rel [definition, in ProgrammingTuringMachines.TM.Relations]
Relabel [definition, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Relabel [section, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Relabel_Terminates [lemma, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Relabel_RealiseIn [lemma, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Relabel_Realise [lemma, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Relabel.F [variable, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Relabel.F' [variable, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Relabel.n [variable, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Relabel.p [variable, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Relabel.pM [variable, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Relabel.sig [variable, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Relations [library]
removelast_length [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
removelast_app_singleton [lemma, in ProgrammingTuringMachines.TM.Code.ListTM]
Reset [definition, in ProgrammingTuringMachines.TM.Code.Copy]
ResetEmpty [definition, in ProgrammingTuringMachines.TM.Code.Copy]
ResetEmpty_Sem [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
ResetEmpty_steps [definition, in ProgrammingTuringMachines.TM.Code.Copy]
ResetEmpty_Rel [definition, in ProgrammingTuringMachines.TM.Code.Copy]
ResetEmpty1 [definition, in ProgrammingTuringMachines.TM.Code.Copy]
ResetEmpty1_Sem [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
ResetEmpty1_steps [definition, in ProgrammingTuringMachines.TM.Code.Copy]
ResetEmpty1_Rel [definition, in ProgrammingTuringMachines.TM.Code.Copy]
Reset_steps_comp [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
Reset_Terminates [definition, in ProgrammingTuringMachines.TM.Code.Copy]
Reset_steps [definition, in ProgrammingTuringMachines.TM.Code.Copy]
Reset_Realise [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
Reset_Rel [definition, in ProgrammingTuringMachines.TM.Code.Copy]
restrict [definition, in ProgrammingTuringMachines.TM.Relations]
retAT [constructor, in ProgrammingTuringMachines.TM.LM.Alphabets]
Retract_sigOption_sigSum [instance, in ProgrammingTuringMachines.TM.Code.CaseSum]
Retract_plus [instance, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Retract_sigList_X [instance, in ProgrammingTuringMachines.TM.Code.Code]
Retract_sigOption_X [instance, in ProgrammingTuringMachines.TM.Code.Code]
Retract_sigPair_Y [instance, in ProgrammingTuringMachines.TM.Code.Code]
Retract_sigPair_X [instance, in ProgrammingTuringMachines.TM.Code.Code]
Retract_sigSum_Y [instance, in ProgrammingTuringMachines.TM.Code.Code]
Retract_sigSum_X [instance, in ProgrammingTuringMachines.TM.Code.Code]
retr_closures_step [definition, in ProgrammingTuringMachines.TM.LM.HaltingProblem]
retr_heap_step [definition, in ProgrammingTuringMachines.TM.LM.HaltingProblem]
retr_nat_prog [definition, in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
retr_X_list' [instance, in ProgrammingTuringMachines.TM.Code.ListTM]
retr_X_opt [instance, in ProgrammingTuringMachines.TM.Code.ListTM]
retr_X_list [instance, in ProgrammingTuringMachines.TM.Code.ListTM]
retr_sigY_sigMap' [definition, in ProgrammingTuringMachines.TM.Code.SumTM]
retr_sigY_sigMap [definition, in ProgrammingTuringMachines.TM.Code.SumTM]
retr_sigX_sigMap' [definition, in ProgrammingTuringMachines.TM.Code.SumTM]
retr_sigX_sigMap [definition, in ProgrammingTuringMachines.TM.Code.SumTM]
retr_hent'_lookup [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_hent'_heap [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_hent_lookup [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_hent_heap [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_clos_lookup_heap [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_clos_heap [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_nat_lookup_entry [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_nat_heap_entry [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_nat_lookup_clos_var [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_nat_clos_var [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_nat_lookup_clos_ad [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_nat_clos_ad [definition, in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_closure_step [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
retr_hent_step [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
retr_hent'_step [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
retr_clos_step_hent [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
retr_nat_step_hent [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
retr_nat_step_clos_var [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
retr_nat_clos_var [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
retr_nat_step_clos_ad [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
retr_nat_clos_ad [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
retr_tok_step [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
retr_pro_step [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
retr_pro_clos [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
retr_clos_step [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
retT [constructor, in ProgrammingTuringMachines.TM.LM.Semantics]
Return [definition, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return [section, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return_Terminates [lemma, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return_RealiseIn [lemma, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return_Realise [lemma, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return.F [variable, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return.F' [variable, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return.n [variable, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return.p [variable, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return.pM [variable, in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return.sig [variable, in ProgrammingTuringMachines.TM.Combinators.Combinators]
rfix [definition, in ProgrammingTuringMachines.TM.Relations]
right [definition, in ProgrammingTuringMachines.TM.TM]
rightof [constructor, in ProgrammingTuringMachines.TM.TM]
rimplication [definition, in ProgrammingTuringMachines.TM.Relations]
rIntersection [definition, in ProgrammingTuringMachines.TM.Relations]
rintersection [definition, in ProgrammingTuringMachines.TM.Relations]
rlength [definition, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
rlength [definition, in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
rlength' [definition, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
rUnion [definition, in ProgrammingTuringMachines.TM.Relations]
runion [definition, in ProgrammingTuringMachines.TM.Relations]
R_canonical_functional [lemma, in ProgrammingTuringMachines.TM.TM]


S

select [definition, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
selectConf [definition, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
select_nth [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Semantics [section, in ProgrammingTuringMachines.TM.TM]
Semantics [section, in ProgrammingTuringMachines.TM.LM.Semantics]
Semantics [library]
Semantics.Canonical_Termination.M [variable, in ProgrammingTuringMachines.TM.TM]
Semantics.Canonical_Termination.n [variable, in ProgrammingTuringMachines.TM.TM]
Semantics.Canonical_Termination [section, in ProgrammingTuringMachines.TM.TM]
Semantics.Canonical_Correctness.pM [variable, in ProgrammingTuringMachines.TM.TM]
Semantics.Canonical_Correctness.F [variable, in ProgrammingTuringMachines.TM.TM]
Semantics.Canonical_Correctness.n [variable, in ProgrammingTuringMachines.TM.TM]
Semantics.Canonical_Correctness [section, in ProgrammingTuringMachines.TM.TM]
Semantics.sig [variable, in ProgrammingTuringMachines.TM.TM]
_ ⊨c( _ ) _ [notation, in ProgrammingTuringMachines.TM.TM]
_ ↓ _ [notation, in ProgrammingTuringMachines.TM.TM]
_ ⊨ _ [notation, in ProgrammingTuringMachines.TM.TM]
Seq [definition, in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
SequentialComposition [library]
Seq_RealiseIn [lemma, in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
Seq_TerminatesIn [lemma, in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
Seq_Realise [lemma, in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
sigCom [definition, in ProgrammingTuringMachines.TM.LM.Alphabets]
sigCom_fin [definition, in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHAdd [definition, in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHAdd_fin [definition, in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHClos [definition, in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHClos_fin [definition, in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHeap [definition, in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHeap_fin [definition, in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHEntr [definition, in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHEntr_fin [definition, in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHEntr' [definition, in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHEntr'_fin [definition, in ProgrammingTuringMachines.TM.LM.Alphabets]
sigList [abbreviation, in ProgrammingTuringMachines.TM.Code.ListTM]
sigList [inductive, in ProgrammingTuringMachines.TM.Code.Code]
sigList_fin [instance, in ProgrammingTuringMachines.TM.Code.Code]
sigList_dec [instance, in ProgrammingTuringMachines.TM.Code.Code]
sigList_cons [constructor, in ProgrammingTuringMachines.TM.Code.Code]
sigList_nil [constructor, in ProgrammingTuringMachines.TM.Code.Code]
sigList_X [constructor, in ProgrammingTuringMachines.TM.Code.Code]
sigNat [inductive, in ProgrammingTuringMachines.TM.Code.Code]
sigNat_fin [instance, in ProgrammingTuringMachines.TM.Code.Code]
sigNat_eq [instance, in ProgrammingTuringMachines.TM.Code.Code]
sigNat_S [constructor, in ProgrammingTuringMachines.TM.Code.Code]
sigNat_O [constructor, in ProgrammingTuringMachines.TM.Code.Code]
sigOption [inductive, in ProgrammingTuringMachines.TM.Code.Code]
sigOption_fin [instance, in ProgrammingTuringMachines.TM.Code.Code]
sigOption_dec [instance, in ProgrammingTuringMachines.TM.Code.Code]
sigOption_Some [constructor, in ProgrammingTuringMachines.TM.Code.Code]
sigOption_None [constructor, in ProgrammingTuringMachines.TM.Code.Code]
sigOption_X [constructor, in ProgrammingTuringMachines.TM.Code.Code]
sigPair [abbreviation, in ProgrammingTuringMachines.TM.Code.CasePair]
sigPair [inductive, in ProgrammingTuringMachines.TM.Code.Code]
sigPair_fin [instance, in ProgrammingTuringMachines.TM.Code.Code]
sigPair_dec [instance, in ProgrammingTuringMachines.TM.Code.Code]
sigPair_Y [constructor, in ProgrammingTuringMachines.TM.Code.Code]
sigPair_X [constructor, in ProgrammingTuringMachines.TM.Code.Code]
sigPro [definition, in ProgrammingTuringMachines.TM.LM.Alphabets]
sigPro_fin [definition, in ProgrammingTuringMachines.TM.LM.Alphabets]
sigStep [definition, in ProgrammingTuringMachines.TM.LM.HaltingProblem]
sigSum [inductive, in ProgrammingTuringMachines.TM.Code.Code]
sigSum_fin [instance, in ProgrammingTuringMachines.TM.Code.Code]
sigSum_dec [instance, in ProgrammingTuringMachines.TM.Code.Code]
sigSum_inr [constructor, in ProgrammingTuringMachines.TM.Code.Code]
sigSum_inl [constructor, in ProgrammingTuringMachines.TM.Code.Code]
sigSum_Y [constructor, in ProgrammingTuringMachines.TM.Code.Code]
sigSum_X [constructor, in ProgrammingTuringMachines.TM.Code.Code]
size [definition, in ProgrammingTuringMachines.TM.Code.Code]
sizeOfmTapes [definition, in ProgrammingTuringMachines.TM.TM]
sizeOfTape [definition, in ProgrammingTuringMachines.TM.TM]
skipn_tl [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
skipn_0 [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
Skip_cons_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.CaseList]
Skip_cons_Realise [lemma, in ProgrammingTuringMachines.TM.Code.CaseList]
Skip_cons_Rel [definition, in ProgrammingTuringMachines.TM.Code.CaseList]
Skip_cons [definition, in ProgrammingTuringMachines.TM.Code.CaseList]
smpl_dupfree_helper2 [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
smpl_dupfree_helper1 [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Snd [definition, in ProgrammingTuringMachines.TM.Code.CasePair]
Snd_steps_comp [lemma, in ProgrammingTuringMachines.TM.Code.CasePair]
Snd_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.CasePair]
Snd_T [definition, in ProgrammingTuringMachines.TM.Code.CasePair]
Snd_steps [definition, in ProgrammingTuringMachines.TM.Code.CasePair]
Snd_Realise [lemma, in ProgrammingTuringMachines.TM.Code.CasePair]
Snd_Rel [definition, in ProgrammingTuringMachines.TM.Code.CasePair]
star [inductive, in ProgrammingTuringMachines.TM.Relations]
starC [constructor, in ProgrammingTuringMachines.TM.Relations]
starR [constructor, in ProgrammingTuringMachines.TM.Relations]
START [constructor, in ProgrammingTuringMachines.TM.Code.CodeTM]
start [projection, in ProgrammingTuringMachines.TM.TM]
start_not_in [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
star_pow [lemma, in ProgrammingTuringMachines.TM.Relations]
star_preorder [instance, in ProgrammingTuringMachines.TM.Relations]
star_trans [lemma, in ProgrammingTuringMachines.TM.Relations]
Star_Pow.R [variable, in ProgrammingTuringMachines.TM.Relations]
Star_Pow.X [variable, in ProgrammingTuringMachines.TM.Relations]
Star_Pow [section, in ProgrammingTuringMachines.TM.Relations]
state [definition, in ProgrammingTuringMachines.TM.LM.Semantics]
states [projection, in ProgrammingTuringMachines.TM.TM]
step [definition, in ProgrammingTuringMachines.TM.TM]
step [inductive, in ProgrammingTuringMachines.TM.LM.Semantics]
Step [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
StepMachine [section, in ProgrammingTuringMachines.TM.LM.StepTM]
StepMachine.retr_heap_step [variable, in ProgrammingTuringMachines.TM.LM.StepTM]
StepMachine.retr_closures_step [variable, in ProgrammingTuringMachines.TM.LM.StepTM]
StepMachine.sigStep [variable, in ProgrammingTuringMachines.TM.LM.StepTM]
steps [definition, in ProgrammingTuringMachines.TM.LM.Semantics]
steps_steps_k [lemma, in ProgrammingTuringMachines.TM.LM.Semantics]
steps_k_steps [lemma, in ProgrammingTuringMachines.TM.LM.Semantics]
steps_k [definition, in ProgrammingTuringMachines.TM.LM.Semantics]
Steps_comp.I [variable, in ProgrammingTuringMachines.TM.Code.CaseList]
Steps_comp.cX [variable, in ProgrammingTuringMachines.TM.Code.CaseList]
Steps_comp.X [variable, in ProgrammingTuringMachines.TM.Code.CaseList]
Steps_comp.tau [variable, in ProgrammingTuringMachines.TM.Code.CaseList]
Steps_comp.sig [variable, in ProgrammingTuringMachines.TM.Code.CaseList]
Steps_comp [section, in ProgrammingTuringMachines.TM.Code.CaseList]
Steps_comp.I [variable, in ProgrammingTuringMachines.TM.Code.CasePair]
Steps_comp.cX [variable, in ProgrammingTuringMachines.TM.Code.CasePair]
Steps_comp.Y [variable, in ProgrammingTuringMachines.TM.Code.CasePair]
Steps_comp.X [variable, in ProgrammingTuringMachines.TM.Code.CasePair]
Steps_comp.tau [variable, in ProgrammingTuringMachines.TM.Code.CasePair]
Steps_comp.sig [variable, in ProgrammingTuringMachines.TM.Code.CasePair]
Steps_comp [section, in ProgrammingTuringMachines.TM.Code.CasePair]
StepTM [library]
step_is_halt_state [lemma, in ProgrammingTuringMachines.TM.LM.Semantics]
step_functional [lemma, in ProgrammingTuringMachines.TM.LM.Semantics]
step_iff [lemma, in ProgrammingTuringMachines.TM.LM.Semantics]
step_fun_step [lemma, in ProgrammingTuringMachines.TM.LM.Semantics]
step_step_fun [lemma, in ProgrammingTuringMachines.TM.LM.Semantics]
step_fun [definition, in ProgrammingTuringMachines.TM.LM.Semantics]
step_load [constructor, in ProgrammingTuringMachines.TM.LM.Semantics]
step_beta [constructor, in ProgrammingTuringMachines.TM.LM.Semantics]
step_pushVal [constructor, in ProgrammingTuringMachines.TM.LM.Semantics]
step_comp [lemma, in ProgrammingTuringMachines.TM.Combinators.While]
step_nop_split [lemma, in ProgrammingTuringMachines.TM.Combinators.Switch]
step_nop_transition [lemma, in ProgrammingTuringMachines.TM.Combinators.Switch]
step_comp_liftR [lemma, in ProgrammingTuringMachines.TM.Combinators.Switch]
step_comp_liftL [lemma, in ProgrammingTuringMachines.TM.Combinators.Switch]
Step_Terminates [lemma, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_T [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_steps [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_steps_CaseList [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_steps_CaseList' [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_steps_CaseCom [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_Realise [lemma, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_Rel [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_var_Terminates [lemma, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_var_T [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_var_steps [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_var_steps_Lookup [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_var_Realise [lemma, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_var [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_var_Rel [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_app_Terminates [lemma, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_app_T [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_app_steps [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_app_steps_CaseList [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_app_steps_CaseList' [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_app_Realise [lemma, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_app [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_app_Rel [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_lam_Terminates [lemma, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_lam_T [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_lam_steps [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_lam_steps_JumpTarget [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_lam_Realise [lemma, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_lam [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_lam_Rel [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
Step_Lookup [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
STOP [constructor, in ProgrammingTuringMachines.TM.Code.CodeTM]
stop [definition, in ProgrammingTuringMachines.TM.Code.CaseList]
stopAfterFirst [definition, in ProgrammingTuringMachines.TM.Code.CasePair]
stopAtStart [definition, in ProgrammingTuringMachines.TM.Code.CasePair]
stop_not_in [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
stop_lemma [lemma, in ProgrammingTuringMachines.TM.Code.CaseList]
subrel [definition, in ProgrammingTuringMachines.TM.Relations]
subrel_or2 [lemma, in ProgrammingTuringMachines.TM.Relations]
subrel_and2 [lemma, in ProgrammingTuringMachines.TM.Relations]
subrel_or [lemma, in ProgrammingTuringMachines.TM.Relations]
subrel_and [lemma, in ProgrammingTuringMachines.TM.Relations]
SujectTape [section, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
SujectTape.def [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
SujectTape.g [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
SujectTape.sig [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
SujectTape.tau [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
SumTM [library]
surject [definition, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
surjectConf [definition, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
SurjectInject [section, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
SurjectInject.def [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
SurjectInject.retr [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
SurjectInject.sig [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
SurjectInject.tau [variable, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
surjective [definition, in ProgrammingTuringMachines.TM.Relations]
surjectReadSymbols [definition, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
surjectSymbols [definition, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
surjectTape [abbreviation, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
surjectTape [definition, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
surjectTapes [definition, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
surjectTapes_nth [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
surjectTape_isRight' [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
surjectTape_isRight [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
surjectTape_injectTape [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
surject_inject_inr [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
surject_app [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
surject_cons [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
surject_inject [lemma, in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
surject_inject_tape [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
surject_inject' [lemma, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
Switch [definition, in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch [section, in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch [library]
SwitchTM [definition, in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch_RealiseIn [lemma, in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch_TerminatesIn [lemma, in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch_Realise [lemma, in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch_split [lemma, in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch_merge [lemma, in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch_p [definition, in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch_halt [definition, in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch_trans [definition, in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch.F [variable, in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch.F' [variable, in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch.n [variable, in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch.pMf [variable, in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch.pM1 [variable, in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch.sig [variable, in ProgrammingTuringMachines.TM.Combinators.Switch]
Mf _ [notation, in ProgrammingTuringMachines.TM.Combinators.Switch]
p2 _ [notation, in ProgrammingTuringMachines.TM.Combinators.Switch]
S_Rel [definition, in ProgrammingTuringMachines.TM.Code.CaseNat]


T

TailRec [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
tailRecursion [definition, in ProgrammingTuringMachines.TM.LM.Semantics]
TailRec_Terminates [lemma, in ProgrammingTuringMachines.TM.LM.StepTM]
TailRec_T [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
TailRec_steps [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
TailRec_Realise [lemma, in ProgrammingTuringMachines.TM.LM.StepTM]
TailRec_Rel [definition, in ProgrammingTuringMachines.TM.LM.StepTM]
tape [inductive, in ProgrammingTuringMachines.TM.TM]
tapes [definition, in ProgrammingTuringMachines.TM.TM]
tapeToList [definition, in ProgrammingTuringMachines.TM.TM]
tapeToList_move_L [lemma, in ProgrammingTuringMachines.TM.TM]
tapeToList_move_R [lemma, in ProgrammingTuringMachines.TM.TM]
tapeToList_move [lemma, in ProgrammingTuringMachines.TM.TM]
tape_contains_rev_ext [lemma, in ProgrammingTuringMachines.TM.Code.CodeTM]
tape_contains_ext [lemma, in ProgrammingTuringMachines.TM.Code.CodeTM]
tape_contains_rev_isRight [lemma, in ProgrammingTuringMachines.TM.Code.CodeTM]
tape_contains_rev [definition, in ProgrammingTuringMachines.TM.Code.CodeTM]
tape_contains_rev' [definition, in ProgrammingTuringMachines.TM.Code.CodeTM]
tape_contains [definition, in ProgrammingTuringMachines.TM.Code.CodeTM]
tape_contains' [definition, in ProgrammingTuringMachines.TM.Code.CodeTM]
tape_local_l_move_left' [lemma, in ProgrammingTuringMachines.TM.TM]
tape_local_move_right' [lemma, in ProgrammingTuringMachines.TM.TM]
tape_left_move_left' [lemma, in ProgrammingTuringMachines.TM.TM]
tape_right_move_right' [lemma, in ProgrammingTuringMachines.TM.TM]
tape_left_move_right' [lemma, in ProgrammingTuringMachines.TM.TM]
tape_right_move_left' [lemma, in ProgrammingTuringMachines.TM.TM]
tape_right_move_left [lemma, in ProgrammingTuringMachines.TM.TM]
tape_left_move_right [lemma, in ProgrammingTuringMachines.TM.TM]
tape_local_l_move_left [lemma, in ProgrammingTuringMachines.TM.TM]
tape_local_move_right [lemma, in ProgrammingTuringMachines.TM.TM]
tape_local_nil [lemma, in ProgrammingTuringMachines.TM.TM]
tape_local_l_cons_iff [lemma, in ProgrammingTuringMachines.TM.TM]
tape_local_cons_iff [lemma, in ProgrammingTuringMachines.TM.TM]
tape_local_l_left [lemma, in ProgrammingTuringMachines.TM.TM]
tape_local_right [lemma, in ProgrammingTuringMachines.TM.TM]
tape_local_l_current_cons [lemma, in ProgrammingTuringMachines.TM.TM]
tape_local_current_cons [lemma, in ProgrammingTuringMachines.TM.TM]
tape_local_mirror' [lemma, in ProgrammingTuringMachines.TM.TM]
tape_local_mirror [lemma, in ProgrammingTuringMachines.TM.TM]
tape_local_l [definition, in ProgrammingTuringMachines.TM.TM]
tape_local [definition, in ProgrammingTuringMachines.TM.TM]
Tape_Local.sig [variable, in ProgrammingTuringMachines.TM.TM]
Tape_Local [section, in ProgrammingTuringMachines.TM.TM]
tape_write [definition, in ProgrammingTuringMachines.TM.TM]
tape_move_left_right [lemma, in ProgrammingTuringMachines.TM.TM]
tape_move_right_left [lemma, in ProgrammingTuringMachines.TM.TM]
tape_move [definition, in ProgrammingTuringMachines.TM.TM]
tape_move_left [definition, in ProgrammingTuringMachines.TM.TM]
tape_move_left' [definition, in ProgrammingTuringMachines.TM.TM]
tape_move_right [definition, in ProgrammingTuringMachines.TM.TM]
tape_move_right' [definition, in ProgrammingTuringMachines.TM.TM]
tape_is_midtape [lemma, in ProgrammingTuringMachines.TM.TM]
tape_midtape_current_left [lemma, in ProgrammingTuringMachines.TM.TM]
tape_midtape_current_right [lemma, in ProgrammingTuringMachines.TM.TM]
tape_destruct2' [lemma, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
tape_destruct2 [lemma, in ProgrammingTuringMachines.TM.Compound.CopySymbols]
tape_local_contains [lemma, in ProgrammingTuringMachines.TM.Code.WriteValue]
TerminatesIn [definition, in ProgrammingTuringMachines.TM.TM]
TerminatesIn_extend [lemma, in ProgrammingTuringMachines.TM.TM]
TerminatesIn_monotone [lemma, in ProgrammingTuringMachines.TM.TM]
test [section, in ProgrammingTuringMachines.TM.Compound.TMTac]
test.dec_P [variable, in ProgrammingTuringMachines.TM.Compound.TMTac]
test.P [variable, in ProgrammingTuringMachines.TM.Compound.TMTac]
TM [library]
TMTac [library]
trans [projection, in ProgrammingTuringMachines.TM.TM]
Translate [definition, in ProgrammingTuringMachines.TM.Code.Copy]
translate [definition, in ProgrammingTuringMachines.TM.Code.Copy]
Translate [section, in ProgrammingTuringMachines.TM.Code.Copy]
TranslateAct [section, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
TranslateAct.X [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
TranslateAct.Y [variable, in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
Translate_steps_comp [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
Translate_steps_comp.I [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Translate_steps_comp.cX [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Translate_steps_comp.X [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Translate_steps_comp.tau [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Translate_steps_comp.sig [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Translate_steps_comp [section, in ProgrammingTuringMachines.TM.Code.Copy]
Translate_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
Translate_T [definition, in ProgrammingTuringMachines.TM.Code.Copy]
Translate_steps [definition, in ProgrammingTuringMachines.TM.Code.Copy]
Translate_Realise [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
Translate_Rel [definition, in ProgrammingTuringMachines.TM.Code.Copy]
Translate' [definition, in ProgrammingTuringMachines.TM.Code.Copy]
Translate'_Terminates [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
Translate'_steps [definition, in ProgrammingTuringMachines.TM.Code.Copy]
Translate'_Realise [lemma, in ProgrammingTuringMachines.TM.Code.Copy]
Translate'_Rel [definition, in ProgrammingTuringMachines.TM.Code.Copy]
Translate.cX [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Translate.retr1 [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Translate.retr2 [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Translate.sig [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Translate.tau [variable, in ProgrammingTuringMachines.TM.Code.Copy]
Translate.X [variable, in ProgrammingTuringMachines.TM.Code.Copy]
tRel [definition, in ProgrammingTuringMachines.TM.TM]


U

UNKNOWN [constructor, in ProgrammingTuringMachines.TM.Code.CodeTM]


V

Var [definition, in ProgrammingTuringMachines.TM.LM.Semantics]
varT [constructor, in ProgrammingTuringMachines.TM.LM.Semantics]


W

WHILE [abbreviation, in ProgrammingTuringMachines.TM.Combinators.While]
While [definition, in ProgrammingTuringMachines.TM.Combinators.While]
While [section, in ProgrammingTuringMachines.TM.Combinators.While]
While [library]
WhileCoInduction [lemma, in ProgrammingTuringMachines.TM.Combinators.While]
WhileCoInduction [section, in ProgrammingTuringMachines.TM.Combinators.While]
WhileCoInduction.F [variable, in ProgrammingTuringMachines.TM.Combinators.While]
WhileCoInduction.n [variable, in ProgrammingTuringMachines.TM.Combinators.While]
WhileCoInduction.R [variable, in ProgrammingTuringMachines.TM.Combinators.While]
WhileCoInduction.sig [variable, in ProgrammingTuringMachines.TM.Combinators.While]
WhileCoInduction.T [variable, in ProgrammingTuringMachines.TM.Combinators.While]
WhileCoInduction.T' [variable, in ProgrammingTuringMachines.TM.Combinators.While]
WhileInduction [lemma, in ProgrammingTuringMachines.TM.Combinators.While]
WhileInduction [section, in ProgrammingTuringMachines.TM.Combinators.While]
WhileInduction.F [variable, in ProgrammingTuringMachines.TM.Combinators.While]
WhileInduction.n [variable, in ProgrammingTuringMachines.TM.Combinators.While]
WhileInduction.R1 [variable, in ProgrammingTuringMachines.TM.Combinators.While]
WhileInduction.R2 [variable, in ProgrammingTuringMachines.TM.Combinators.While]
WhileInduction.sig [variable, in ProgrammingTuringMachines.TM.Combinators.While]
WhileTM [definition, in ProgrammingTuringMachines.TM.Combinators.While]
While_Rel' [definition, in ProgrammingTuringMachines.TM.Combinators.While]
While_TerminatesIn [lemma, in ProgrammingTuringMachines.TM.Combinators.While]
While_T_intro [constructor, in ProgrammingTuringMachines.TM.Combinators.While]
While_T [inductive, in ProgrammingTuringMachines.TM.Combinators.While]
While_TerminatesIn_ind [lemma, in ProgrammingTuringMachines.TM.Combinators.While]
While_Realise [lemma, in ProgrammingTuringMachines.TM.Combinators.While]
While_Rel''_loop [constructor, in ProgrammingTuringMachines.TM.Combinators.While]
While_Rel''_one [constructor, in ProgrammingTuringMachines.TM.Combinators.While]
While_Rel [inductive, in ProgrammingTuringMachines.TM.Combinators.While]
While_merge_term [lemma, in ProgrammingTuringMachines.TM.Combinators.While]
While_merge_repeat [lemma, in ProgrammingTuringMachines.TM.Combinators.While]
While_split_term [lemma, in ProgrammingTuringMachines.TM.Combinators.While]
While_split_repeat [lemma, in ProgrammingTuringMachines.TM.Combinators.While]
While_split [lemma, in ProgrammingTuringMachines.TM.Combinators.While]
While_trans_repeat [lemma, in ProgrammingTuringMachines.TM.Combinators.While]
While_part [definition, in ProgrammingTuringMachines.TM.Combinators.While]
While_trans [definition, in ProgrammingTuringMachines.TM.Combinators.While]
While.defF [variable, in ProgrammingTuringMachines.TM.Combinators.While]
While.F [variable, in ProgrammingTuringMachines.TM.Combinators.While]
While.n [variable, in ProgrammingTuringMachines.TM.Combinators.While]
While.pM [variable, in ProgrammingTuringMachines.TM.Combinators.While]
While.R [variable, in ProgrammingTuringMachines.TM.Combinators.While]
While.sig [variable, in ProgrammingTuringMachines.TM.Combinators.While]
While.While_TerminatesIn_coind.T [variable, in ProgrammingTuringMachines.TM.Combinators.While]
While.While_TerminatesIn_coind [section, in ProgrammingTuringMachines.TM.Combinators.While]
While.While_TerminatesIn.T' [variable, in ProgrammingTuringMachines.TM.Combinators.While]
While.While_TerminatesIn.T [variable, in ProgrammingTuringMachines.TM.Combinators.While]
While.While_TerminatesIn [section, in ProgrammingTuringMachines.TM.Combinators.While]
Write [definition, in ProgrammingTuringMachines.TM.Basic.Mono]
WriteMove [definition, in ProgrammingTuringMachines.TM.Basic.Mono]
WriteMove_Sem [lemma, in ProgrammingTuringMachines.TM.Basic.Mono]
WriteMove_Rel [definition, in ProgrammingTuringMachines.TM.Basic.Mono]
WriteString [definition, in ProgrammingTuringMachines.TM.Compound.WriteString]
WriteString [library]
WriteString_Sem [lemma, in ProgrammingTuringMachines.TM.Compound.WriteString]
WriteString_Rel [definition, in ProgrammingTuringMachines.TM.Compound.WriteString]
WriteString_fix_Sem [lemma, in ProgrammingTuringMachines.TM.Compound.WriteString]
WriteString_steps [definition, in ProgrammingTuringMachines.TM.Compound.WriteString]
WriteString_sem_fix [definition, in ProgrammingTuringMachines.TM.Compound.WriteString]
WriteString_Fun [definition, in ProgrammingTuringMachines.TM.Compound.WriteString]
WriteString_L_local [lemma, in ProgrammingTuringMachines.TM.Code.WriteValue]
WriteValue [definition, in ProgrammingTuringMachines.TM.Code.WriteValue]
WriteValue [section, in ProgrammingTuringMachines.TM.Code.WriteValue]
WriteValue [library]
WriteValue_Sem [lemma, in ProgrammingTuringMachines.TM.Code.WriteValue]
WriteValue_steps [definition, in ProgrammingTuringMachines.TM.Code.WriteValue]
WriteValue_Rel [definition, in ProgrammingTuringMachines.TM.Code.WriteValue]
WriteValue.cX [variable, in ProgrammingTuringMachines.TM.Code.WriteValue]
WriteValue.sig [variable, in ProgrammingTuringMachines.TM.Code.WriteValue]
WriteValue.X [variable, in ProgrammingTuringMachines.TM.Code.WriteValue]
Write_String_nil [lemma, in ProgrammingTuringMachines.TM.Compound.WriteString]
Write_String.D [variable, in ProgrammingTuringMachines.TM.Compound.WriteString]
Write_String.sig [variable, in ProgrammingTuringMachines.TM.Compound.WriteString]
Write_String [section, in ProgrammingTuringMachines.TM.Compound.WriteString]
Write_Sem [lemma, in ProgrammingTuringMachines.TM.Basic.Mono]
Write_Rel [definition, in ProgrammingTuringMachines.TM.Basic.Mono]


other

_ ^+ (type_scope) [notation, in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ≂( _ ) _ [notation, in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ≂ _ [notation, in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ≃( _ ) _ [notation, in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ≃ _ [notation, in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ↓ _ [notation, in ProgrammingTuringMachines.TM.TM]
_ ⊨c( _ ) _ [notation, in ProgrammingTuringMachines.TM.TM]
_ ⊨ _ [notation, in ProgrammingTuringMachines.TM.TM]
_ ;; _ [notation, in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
_ ⇑ _ [notation, in ProgrammingTuringMachines.TM.Code.ProgrammingTools]
_ @ _ [notation, in ProgrammingTuringMachines.TM.Code.ProgrammingTools]
_ ||_ _ [notation, in ProgrammingTuringMachines.TM.Relations]
_ |_ _ [notation, in ProgrammingTuringMachines.TM.Relations]
_ =2 _ [notation, in ProgrammingTuringMachines.TM.Relations]
_ <<=2 _ [notation, in ProgrammingTuringMachines.TM.Relations]
_ ⊂ _ [notation, in ProgrammingTuringMachines.TM.Relations]
_ ∩ _ [notation, in ProgrammingTuringMachines.TM.Relations]
_ ∪ _ [notation, in ProgrammingTuringMachines.TM.Relations]
_ ∘ _ [notation, in ProgrammingTuringMachines.TM.Relations]
( _ ; _ ) [notation, in ProgrammingTuringMachines.TM.TM]
â‹‚_ _ _ [notation, in ProgrammingTuringMachines.TM.Relations]
⋃_ _ _ [notation, in ProgrammingTuringMachines.TM.Relations]



Notation Index

F

_ ≂( _ ) _ [in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ≂ _ [in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ≃( _ ) _ [in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ≃ _ [in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ^+ (type_scope) [in ProgrammingTuringMachines.TM.Code.CodeTM]
V _ [in ProgrammingTuringMachines.TM.Relations]


M

f' [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
g' [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]


S

_ ⊨c( _ ) _ [in ProgrammingTuringMachines.TM.TM]
_ ↓ _ [in ProgrammingTuringMachines.TM.TM]
_ ⊨ _ [in ProgrammingTuringMachines.TM.TM]
Mf _ [in ProgrammingTuringMachines.TM.Combinators.Switch]
p2 _ [in ProgrammingTuringMachines.TM.Combinators.Switch]


other

_ ^+ (type_scope) [in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ≂( _ ) _ [in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ≂ _ [in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ≃( _ ) _ [in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ≃ _ [in ProgrammingTuringMachines.TM.Code.CodeTM]
_ ↓ _ [in ProgrammingTuringMachines.TM.TM]
_ ⊨c( _ ) _ [in ProgrammingTuringMachines.TM.TM]
_ ⊨ _ [in ProgrammingTuringMachines.TM.TM]
_ ;; _ [in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
_ ⇑ _ [in ProgrammingTuringMachines.TM.Code.ProgrammingTools]
_ @ _ [in ProgrammingTuringMachines.TM.Code.ProgrammingTools]
_ ||_ _ [in ProgrammingTuringMachines.TM.Relations]
_ |_ _ [in ProgrammingTuringMachines.TM.Relations]
_ =2 _ [in ProgrammingTuringMachines.TM.Relations]
_ <<=2 _ [in ProgrammingTuringMachines.TM.Relations]
_ ⊂ _ [in ProgrammingTuringMachines.TM.Relations]
_ ∩ _ [in ProgrammingTuringMachines.TM.Relations]
_ ∪ _ [in ProgrammingTuringMachines.TM.Relations]
_ ∘ _ [in ProgrammingTuringMachines.TM.Relations]
( _ ; _ ) [in ProgrammingTuringMachines.TM.TM]
â‹‚_ _ _ [in ProgrammingTuringMachines.TM.Relations]
⋃_ _ _ [in ProgrammingTuringMachines.TM.Relations]



Variable Index

A

AddTapes.n [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Append.cX [in ProgrammingTuringMachines.TM.Code.ListTM]
Append.defX [in ProgrammingTuringMachines.TM.Code.ListTM]
Append.sigX [in ProgrammingTuringMachines.TM.Code.ListTM]
Append.stop [in ProgrammingTuringMachines.TM.Code.ListTM]
Append.X [in ProgrammingTuringMachines.TM.Code.ListTM]


C

CaseFin.defSig [in ProgrammingTuringMachines.TM.Code.CaseFin]
CaseFin.sig [in ProgrammingTuringMachines.TM.Code.CaseFin]
CaseList.cX [in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList.sigX [in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList.X [in ProgrammingTuringMachines.TM.Code.CaseList]
CaseOption.codX [in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseOption.sig [in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseOption.sigX [in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseOption.tau [in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseOption.X [in ProgrammingTuringMachines.TM.Code.CaseSum]
CasePair.cX [in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair.cY [in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair.sigX [in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair.sigY [in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair.X [in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair.Y [in ProgrammingTuringMachines.TM.Code.CasePair]
CaseSum.codX [in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum.codY [in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum.sigX [in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum.sigY [in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum.X [in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum.Y [in ProgrammingTuringMachines.TM.Code.CaseSum]
ChangeAlphabet.F [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet.n [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet.pM [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet.retr [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet.sig [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet.tau [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Composition.F1 [in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
Composition.F2 [in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
Composition.n [in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
Composition.pM1 [in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
Composition.pM2 [in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
Composition.sig [in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
Computes_ChangeAlphabet2.func [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.cZ [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.cY [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.cX [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.Z [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.Y [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.X [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.retr [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.pM [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.F [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.n_tapes [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.tau [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet2.sig [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.func [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.cY [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.cX [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.Y [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.X [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.retr [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.pM [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.F [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.n_tapes [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.tau [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet.sig [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
CopySymbols.f [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols.sig [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopyValue_steps_comp.I [in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_steps_comp.cX [in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_steps_comp.X [in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_steps_comp.tau [in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_steps_comp.sig [in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue.cX [in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue.sig [in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue.X [in ProgrammingTuringMachines.TM.Code.Copy]
Copy.f [in ProgrammingTuringMachines.TM.Code.Copy]
Copy.f [in ProgrammingTuringMachines.TM.Compound.Multi]
Copy.sig [in ProgrammingTuringMachines.TM.Code.Copy]
Copy.sig [in ProgrammingTuringMachines.TM.Compound.Multi]
Copy.stop [in ProgrammingTuringMachines.TM.Code.Copy]


D

Diverge.n [in ProgrammingTuringMachines.TM.Compound.Multi]
Diverge.sig [in ProgrammingTuringMachines.TM.Compound.Multi]
DoAct_Derived.D [in ProgrammingTuringMachines.TM.Basic.Mono]
DoAct_Derived.c [in ProgrammingTuringMachines.TM.Basic.Mono]
DoAct_Derived.sig [in ProgrammingTuringMachines.TM.Basic.Mono]
DoAct.act [in ProgrammingTuringMachines.TM.Basic.Mono]
DoAct.c [in ProgrammingTuringMachines.TM.Basic.Mono]
DoAct.sig [in ProgrammingTuringMachines.TM.Basic.Mono]


E

Encode_list.cX [in ProgrammingTuringMachines.TM.Code.Code]
Encode_list.X [in ProgrammingTuringMachines.TM.Code.Code]
Encode_list.sigX [in ProgrammingTuringMachines.TM.Code.Code]
Encode_option.cX [in ProgrammingTuringMachines.TM.Code.Code]
Encode_option.X [in ProgrammingTuringMachines.TM.Code.Code]
Encode_option.sigX [in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair.cY [in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair.cX [in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair.Y [in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair.X [in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair.sigY [in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair.sigX [in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum.cY [in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum.cX [in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum.sigY [in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum.sigX [in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum.Y [in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum.X [in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_comp.I2 [in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_comp.I1 [in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_comp.cX [in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_comp.sig3 [in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_comp.sig2 [in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_comp.sig1 [in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_comp.X [in ProgrammingTuringMachines.TM.Code.Code]
Encode_map.inj [in ProgrammingTuringMachines.TM.Code.Code]
Encode_map.cX [in ProgrammingTuringMachines.TM.Code.Code]
Encode_map.tau [in ProgrammingTuringMachines.TM.Code.Code]
Encode_map.sig [in ProgrammingTuringMachines.TM.Code.Code]
Encode_map.X [in ProgrammingTuringMachines.TM.Code.Code]
Encode_Finite.sig [in ProgrammingTuringMachines.TM.Code.Code]


F

Fill.m [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Fill.n [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Fill.X [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Fix_Sig.Computes2.Computes2_Ext.mon [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes2.Computes2_Ext.r2 [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes2.Computes2_Ext.r1 [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes2.Computes2_Ext.ext_fun [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes2.Computes2_Ext.f' [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes2.Computes2_Ext.f [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes2.F [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes2.n [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes.Computes_Ext.mon [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes.Computes_Ext.r2 [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes.Computes_Ext.r1 [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes.Computes_Ext.ext_fun [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes.Computes_Ext.f' [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes.Computes_Ext.f [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes.F [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes.n [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.sig [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sigma.sig [in ProgrammingTuringMachines.TM.TM]
Fix_X2.n [in ProgrammingTuringMachines.TM.Relations]
Fix_X2.Z [in ProgrammingTuringMachines.TM.Relations]
Fix_X2.Y [in ProgrammingTuringMachines.TM.Relations]
Fix_X2.X [in ProgrammingTuringMachines.TM.Relations]


I

Id.F [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Id.n [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Id.pM [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Id.sig [in ProgrammingTuringMachines.TM.Combinators.Combinators]
If.F [in ProgrammingTuringMachines.TM.Combinators.If]
If.n [in ProgrammingTuringMachines.TM.Combinators.If]
If.pM1 [in ProgrammingTuringMachines.TM.Combinators.If]
If.pM2 [in ProgrammingTuringMachines.TM.Combinators.If]
If.pM3 [in ProgrammingTuringMachines.TM.Combinators.If]
If.sig [in ProgrammingTuringMachines.TM.Combinators.If]
InjectSurject.def [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
InjectSurject.inj [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
InjectSurject.sig [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
InjectSurject.tau [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
InjectTape.f [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
InjectTape.sig [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
InjectTape.tau [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]


L

Lenght.cX [in ProgrammingTuringMachines.TM.Code.ListTM]
Lenght.retr1 [in ProgrammingTuringMachines.TM.Code.ListTM]
Lenght.retr2 [in ProgrammingTuringMachines.TM.Code.ListTM]
Lenght.sig [in ProgrammingTuringMachines.TM.Code.ListTM]
Lenght.sigX [in ProgrammingTuringMachines.TM.Code.ListTM]
Lenght.X [in ProgrammingTuringMachines.TM.Code.ListTM]
LiftAlphabet.def [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet.F [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet.Inj [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet.n [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet.pMSig [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet.sig [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet.tau [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftNM.F [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftNM.I [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftNM.I_dupfree [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftNM.m [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftNM.n [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftNM.pM [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftNM.sig [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Rel.T [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Rel.R [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Rel.I [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Rel.n [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Rel.m [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Rel.F [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Rel.sig [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
lift_sigma_tau.F [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
lift_sigma_tau.def [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
lift_sigma_tau.g [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
lift_sigma_tau.tau [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
lift_sigma_tau.sig [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
lift_sigma_tau.n [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
ListStuff.X [in ProgrammingTuringMachines.TM.Code.ListTM]
Lookup.retr_heap_lookup [in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup.retr_clos_lookup [in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup.sigLookup [in ProgrammingTuringMachines.TM.LM.LookupTM]
LoopLift.A [in ProgrammingTuringMachines.TM.Prelim]
LoopLift.B [in ProgrammingTuringMachines.TM.Prelim]
LoopLift.f [in ProgrammingTuringMachines.TM.Prelim]
LoopLift.f' [in ProgrammingTuringMachines.TM.Prelim]
LoopLift.h [in ProgrammingTuringMachines.TM.Prelim]
LoopLift.halt_lift_comp [in ProgrammingTuringMachines.TM.Prelim]
LoopLift.h' [in ProgrammingTuringMachines.TM.Prelim]
LoopLift.lift [in ProgrammingTuringMachines.TM.Prelim]
LoopLift.step_lift_comp [in ProgrammingTuringMachines.TM.Prelim]
LoopMerge.A [in ProgrammingTuringMachines.TM.Prelim]
LoopMerge.f [in ProgrammingTuringMachines.TM.Prelim]
LoopMerge.h [in ProgrammingTuringMachines.TM.Prelim]
LoopMerge.halt_comp [in ProgrammingTuringMachines.TM.Prelim]
LoopMerge.h' [in ProgrammingTuringMachines.TM.Prelim]
loop_map.step_map_comp [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
loop_map.g [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
loop_map.h [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
loop_map.f [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
loop_map.B [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
loop_map.A [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Loop.A [in ProgrammingTuringMachines.TM.Prelim]
Loop.f [in ProgrammingTuringMachines.TM.Prelim]
Loop.p [in ProgrammingTuringMachines.TM.Prelim]


M

MapCode.retr [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
MapCode.sig [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
MapCode.tau [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
MapSum.codX [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.codY [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.codZ [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.f [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.g [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.M1 [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.M1_Terminates [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.M1_steps [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.M1_Computes [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.M2 [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.M2_Terminates [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.M2_steps [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.M2_Computes [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.n [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.retr_sigSum_sigMap [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.retr_sigM_sigMap [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.retr_sigZ_sigM [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.retr_sigY_sigM [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.retr_sigX_sigM [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.sigM [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.sigMap [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.sigX [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.sigY [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.sigZ [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.X [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.Y [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum.Z [in ProgrammingTuringMachines.TM.Code.SumTM]
MapTape.g [in ProgrammingTuringMachines.TM.TM]
MapTape.sig [in ProgrammingTuringMachines.TM.TM]
MapTape.tau [in ProgrammingTuringMachines.TM.TM]
Map.X [in ProgrammingTuringMachines.TM.Prelim]
Map.Y [in ProgrammingTuringMachines.TM.Prelim]
Map.Z [in ProgrammingTuringMachines.TM.Prelim]
MatchTapes.sig [in ProgrammingTuringMachines.TM.TM]
MirrorTape.n [in ProgrammingTuringMachines.TM.TM]
MirrorTape.sig [in ProgrammingTuringMachines.TM.TM]
Mirror.F [in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mirror.n [in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mirror.pM [in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mirror.sig [in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mk_Mono.R [in ProgrammingTuringMachines.TM.Basic.Mono]
Mk_Mono.F [in ProgrammingTuringMachines.TM.Basic.Mono]
Mk_Mono.fin [in ProgrammingTuringMachines.TM.Basic.Mono]
Mk_Mono.init [in ProgrammingTuringMachines.TM.Basic.Mono]
Mk_Mono.mono_trans [in ProgrammingTuringMachines.TM.Basic.Mono]
Mk_Mono.states [in ProgrammingTuringMachines.TM.Basic.Mono]
Mk_Mono.sig [in ProgrammingTuringMachines.TM.Basic.Mono]
Mono_Nop.sig [in ProgrammingTuringMachines.TM.Basic.Null]
MovePar.D1 [in ProgrammingTuringMachines.TM.Compound.Multi]
MovePar.D2 [in ProgrammingTuringMachines.TM.Compound.Multi]
MovePar.sig [in ProgrammingTuringMachines.TM.Compound.Multi]
MoveToSymbol.f [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol.g [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol.sig [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveValue_steps_comp.I2 [in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps_comp.I1 [in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps_comp.cY [in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps_comp.cX [in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps_comp.Y [in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps_comp.X [in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps_comp.tau [in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps_comp.sig [in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue.cX [in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue.cY [in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue.sig [in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue.X [in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue.Y [in ProgrammingTuringMachines.TM.Code.Copy]
Move_steps_comp.I [in ProgrammingTuringMachines.TM.Code.Copy]
Move_steps_comp.cX [in ProgrammingTuringMachines.TM.Code.Copy]
Move_steps_comp.X [in ProgrammingTuringMachines.TM.Code.Copy]
Move_steps_comp.tau [in ProgrammingTuringMachines.TM.Code.Copy]
Move_steps_comp.sig [in ProgrammingTuringMachines.TM.Code.Copy]
Move.cX [in ProgrammingTuringMachines.TM.Code.Copy]
Move.sig [in ProgrammingTuringMachines.TM.Code.Copy]
Move.X [in ProgrammingTuringMachines.TM.Code.Copy]


N

Nop_Action.sig [in ProgrammingTuringMachines.TM.TM]
Nop_Action.n [in ProgrammingTuringMachines.TM.TM]
Nop.n [in ProgrammingTuringMachines.TM.Compound.Multi]
Nop.sig [in ProgrammingTuringMachines.TM.Compound.Multi]
Nth'.cX [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'.retr1 [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'.retr2 [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'.sig [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'.sigX [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'.X [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth.cX [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth.retr1 [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth.retr2 [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth.retr3 [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth.sig [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth.sigX [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth.X [in ProgrammingTuringMachines.TM.Code.ListTM]


O

OtherWhileRel.F [in ProgrammingTuringMachines.TM.Combinators.While]
OtherWhileRel.n [in ProgrammingTuringMachines.TM.Combinators.While]
OtherWhileRel.R [in ProgrammingTuringMachines.TM.Combinators.While]
OtherWhileRel.sig [in ProgrammingTuringMachines.TM.Combinators.While]


R

ReadChar.k [in ProgrammingTuringMachines.TM.Compound.Multi]
ReadChar.n [in ProgrammingTuringMachines.TM.Compound.Multi]
ReadChar.sig [in ProgrammingTuringMachines.TM.Compound.Multi]
ReadChar.sig [in ProgrammingTuringMachines.TM.Basic.Mono]
Relabel.F [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Relabel.F' [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Relabel.n [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Relabel.p [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Relabel.pM [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Relabel.sig [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return.F [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return.F' [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return.n [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return.p [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return.pM [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return.sig [in ProgrammingTuringMachines.TM.Combinators.Combinators]


S

Semantics.Canonical_Termination.M [in ProgrammingTuringMachines.TM.TM]
Semantics.Canonical_Termination.n [in ProgrammingTuringMachines.TM.TM]
Semantics.Canonical_Correctness.pM [in ProgrammingTuringMachines.TM.TM]
Semantics.Canonical_Correctness.F [in ProgrammingTuringMachines.TM.TM]
Semantics.Canonical_Correctness.n [in ProgrammingTuringMachines.TM.TM]
Semantics.sig [in ProgrammingTuringMachines.TM.TM]
Star_Pow.R [in ProgrammingTuringMachines.TM.Relations]
Star_Pow.X [in ProgrammingTuringMachines.TM.Relations]
StepMachine.retr_heap_step [in ProgrammingTuringMachines.TM.LM.StepTM]
StepMachine.retr_closures_step [in ProgrammingTuringMachines.TM.LM.StepTM]
StepMachine.sigStep [in ProgrammingTuringMachines.TM.LM.StepTM]
Steps_comp.I [in ProgrammingTuringMachines.TM.Code.CaseList]
Steps_comp.cX [in ProgrammingTuringMachines.TM.Code.CaseList]
Steps_comp.X [in ProgrammingTuringMachines.TM.Code.CaseList]
Steps_comp.tau [in ProgrammingTuringMachines.TM.Code.CaseList]
Steps_comp.sig [in ProgrammingTuringMachines.TM.Code.CaseList]
Steps_comp.I [in ProgrammingTuringMachines.TM.Code.CasePair]
Steps_comp.cX [in ProgrammingTuringMachines.TM.Code.CasePair]
Steps_comp.Y [in ProgrammingTuringMachines.TM.Code.CasePair]
Steps_comp.X [in ProgrammingTuringMachines.TM.Code.CasePair]
Steps_comp.tau [in ProgrammingTuringMachines.TM.Code.CasePair]
Steps_comp.sig [in ProgrammingTuringMachines.TM.Code.CasePair]
SujectTape.def [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
SujectTape.g [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
SujectTape.sig [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
SujectTape.tau [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
SurjectInject.def [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
SurjectInject.retr [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
SurjectInject.sig [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
SurjectInject.tau [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Switch.F [in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch.F' [in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch.n [in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch.pMf [in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch.pM1 [in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch.sig [in ProgrammingTuringMachines.TM.Combinators.Switch]


T

Tape_Local.sig [in ProgrammingTuringMachines.TM.TM]
test.dec_P [in ProgrammingTuringMachines.TM.Compound.TMTac]
test.P [in ProgrammingTuringMachines.TM.Compound.TMTac]
TranslateAct.X [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
TranslateAct.Y [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
Translate_steps_comp.I [in ProgrammingTuringMachines.TM.Code.Copy]
Translate_steps_comp.cX [in ProgrammingTuringMachines.TM.Code.Copy]
Translate_steps_comp.X [in ProgrammingTuringMachines.TM.Code.Copy]
Translate_steps_comp.tau [in ProgrammingTuringMachines.TM.Code.Copy]
Translate_steps_comp.sig [in ProgrammingTuringMachines.TM.Code.Copy]
Translate.cX [in ProgrammingTuringMachines.TM.Code.Copy]
Translate.retr1 [in ProgrammingTuringMachines.TM.Code.Copy]
Translate.retr2 [in ProgrammingTuringMachines.TM.Code.Copy]
Translate.sig [in ProgrammingTuringMachines.TM.Code.Copy]
Translate.tau [in ProgrammingTuringMachines.TM.Code.Copy]
Translate.X [in ProgrammingTuringMachines.TM.Code.Copy]


W

WhileCoInduction.F [in ProgrammingTuringMachines.TM.Combinators.While]
WhileCoInduction.n [in ProgrammingTuringMachines.TM.Combinators.While]
WhileCoInduction.R [in ProgrammingTuringMachines.TM.Combinators.While]
WhileCoInduction.sig [in ProgrammingTuringMachines.TM.Combinators.While]
WhileCoInduction.T [in ProgrammingTuringMachines.TM.Combinators.While]
WhileCoInduction.T' [in ProgrammingTuringMachines.TM.Combinators.While]
WhileInduction.F [in ProgrammingTuringMachines.TM.Combinators.While]
WhileInduction.n [in ProgrammingTuringMachines.TM.Combinators.While]
WhileInduction.R1 [in ProgrammingTuringMachines.TM.Combinators.While]
WhileInduction.R2 [in ProgrammingTuringMachines.TM.Combinators.While]
WhileInduction.sig [in ProgrammingTuringMachines.TM.Combinators.While]
While.defF [in ProgrammingTuringMachines.TM.Combinators.While]
While.F [in ProgrammingTuringMachines.TM.Combinators.While]
While.n [in ProgrammingTuringMachines.TM.Combinators.While]
While.pM [in ProgrammingTuringMachines.TM.Combinators.While]
While.R [in ProgrammingTuringMachines.TM.Combinators.While]
While.sig [in ProgrammingTuringMachines.TM.Combinators.While]
While.While_TerminatesIn_coind.T [in ProgrammingTuringMachines.TM.Combinators.While]
While.While_TerminatesIn.T' [in ProgrammingTuringMachines.TM.Combinators.While]
While.While_TerminatesIn.T [in ProgrammingTuringMachines.TM.Combinators.While]
WriteValue.cX [in ProgrammingTuringMachines.TM.Code.WriteValue]
WriteValue.sig [in ProgrammingTuringMachines.TM.Code.WriteValue]
WriteValue.X [in ProgrammingTuringMachines.TM.Code.WriteValue]
Write_String.D [in ProgrammingTuringMachines.TM.Compound.WriteString]
Write_String.sig [in ProgrammingTuringMachines.TM.Compound.WriteString]



Library Index

A

Alphabets


B

Basic


C

CaseCom
CaseFin
CaseList
CaseNat
CasePair
CaseSum
ChangeAlphabet
Code
CodeTM
Combinators
Copy
CopySymbols


H

HaltingProblem


I

If


J

JumpTargetTM


L

LiftAlphabet
Lifting
LiftTapes
ListTM
LookupTM


M

Mirror
Mono
MoveToSymbol
Multi


N

NatTM
Null


P

Prelim
ProgrammingTools


R

Relations


S

Semantics
SequentialComposition
StepTM
SumTM
Switch


T

TM
TMTac


W

While
WriteString
WriteValue



Lemma Index

A

add_tapes_select_nth [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
add_tapes_dupfree [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Add_Terminates [in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Main_Terminates [in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Loop_Terminates [in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Computes [in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Main_Realise [in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Loop_Realise [in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Step_Sem [in ProgrammingTuringMachines.TM.Code.NatTM]
App_Com_Terminates [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Com_Realise [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_ACom_Terminates [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_ACom_Realise [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Comens_Terminates [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Comens_Realise [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Terminates [in ProgrammingTuringMachines.TM.Code.ListTM]
App_Computes [in ProgrammingTuringMachines.TM.Code.ListTM]
app_or_nil [in ProgrammingTuringMachines.TM.Code.ListTM]
app_tapes_select_nth [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
app_tapes_dupfree [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
App'_Terminates [in ProgrammingTuringMachines.TM.Code.ListTM]
App'_Realise [in ProgrammingTuringMachines.TM.Code.ListTM]


C

Canonical_TerminatesIn [in ProgrammingTuringMachines.TM.TM]
Canonical_Realise [in ProgrammingTuringMachines.TM.TM]
CaseCom_Sem [in ProgrammingTuringMachines.TM.LM.CaseCom]
CaseFin_Sem [in ProgrammingTuringMachines.TM.Code.CaseFin]
CaseList_steps_comp [in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList_steps_cons_comp [in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList_Terminates [in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList_Realise [in ProgrammingTuringMachines.TM.Code.CaseList]
CaseNat_Sem [in ProgrammingTuringMachines.TM.Code.CaseNat]
CaseOption_Sem [in ProgrammingTuringMachines.TM.Code.CaseSum]
CasePair_steps_comp [in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair_Terminates [in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair_Realise [in ProgrammingTuringMachines.TM.Code.CasePair]
CaseSum_Sem [in ProgrammingTuringMachines.TM.Code.CaseSum]
ChangeAlphabet_Terminates2 [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet_Computes2 [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet_Terminates [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
ChangeAlphabet_Computes [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_Monotone [in ProgrammingTuringMachines.TM.Code.CodeTM]
Computes_ext [in ProgrammingTuringMachines.TM.Code.CodeTM]
Computes2_Monotone [in ProgrammingTuringMachines.TM.Code.CodeTM]
Computes2_ext [in ProgrammingTuringMachines.TM.Code.CodeTM]
ConsClos_Terminates [in ProgrammingTuringMachines.TM.LM.StepTM]
ConsClos_Realise [in ProgrammingTuringMachines.TM.LM.StepTM]
Constr_varT_Sem [in ProgrammingTuringMachines.TM.LM.CaseCom]
Constr_ACom_Sem [in ProgrammingTuringMachines.TM.LM.CaseCom]
Constr_cons_steps_comp [in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_cons_Terminates [in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_cons_Realise [in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_nil_Sem [in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_None_Sem [in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_Some_Sem [in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_inr_Sem [in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_inl_Sem [in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_pair_steps_comp [in ProgrammingTuringMachines.TM.Code.CasePair]
Constr_pair_Terminates [in ProgrammingTuringMachines.TM.Code.CasePair]
Constr_pair_Realise [in ProgrammingTuringMachines.TM.Code.CasePair]
Constr_O_Sem [in ProgrammingTuringMachines.TM.Code.CaseNat]
Constr_S_Sem [in ProgrammingTuringMachines.TM.Code.CaseNat]
contains_translate_eq [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
contains_translate_tau [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
contains_translate_tau2 [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
contains_translate_tau1 [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
contains_translate_sig [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
CopyChar_Sem [in ProgrammingTuringMachines.TM.Compound.Multi]
CopySymbols_L_steps_moveleft [in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_L_steps_midtape [in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_L_steps_local [in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_steps_moveright [in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_steps_midtape [in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_steps_local [in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_L_correct_moveleft [in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_L_correct_midtape [in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_L_correct [in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_correct_moveright [in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_correct_midtape [in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_correct [in ProgrammingTuringMachines.TM.Code.Copy]
CopySymbols_L_Terminates [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_steps_mirror [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_L_Realise [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_mirror' [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_mirror [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_Terminates [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_Realise [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_true [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_false [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_Step_Sem [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopyValue_steps_comp [in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_Terminates [in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_Realise [in ProgrammingTuringMachines.TM.Code.Copy]
countMap_zero [in ProgrammingTuringMachines.TM.Code.Code]
countMap_injective [in ProgrammingTuringMachines.TM.Code.Code]
current_chars_mirror_tapes [in ProgrammingTuringMachines.TM.Combinators.Mirror]
current_chars_select [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
current_chars_surjectTapes [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]


D

Diverge_Realise [in ProgrammingTuringMachines.TM.Compound.Multi]
doAct_nop [in ProgrammingTuringMachines.TM.TM]
doAct_mirror_multi [in ProgrammingTuringMachines.TM.Combinators.Mirror]
doAct_mirror [in ProgrammingTuringMachines.TM.Combinators.Mirror]
DoAct_Sem [in ProgrammingTuringMachines.TM.Basic.Mono]
doAct_select [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
doAct_surject [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]


E

Encode_Com_hasSize [in ProgrammingTuringMachines.TM.LM.Alphabets]
Encode_nat_eq_nil [in ProgrammingTuringMachines.TM.Code.Code]
Encode_nat_hasSize [in ProgrammingTuringMachines.TM.Code.Code]
Encode_list_hasSize [in ProgrammingTuringMachines.TM.Code.Code]
Encode_list_neq_nil [in ProgrammingTuringMachines.TM.Code.Code]
encode_list_neq_nil [in ProgrammingTuringMachines.TM.Code.Code]
Encode_list_app [in ProgrammingTuringMachines.TM.Code.Code]
encode_list_app [in ProgrammingTuringMachines.TM.Code.Code]
Encode_option_hasSize [in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair_hasSize [in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum_hasSize [in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_comp [in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_hasSize [in ProgrammingTuringMachines.TM.Code.Code]
Encode_Finite_hasSize [in ProgrammingTuringMachines.TM.Code.Code]
Encode_Fin_hasSize [in ProgrammingTuringMachines.TM.Code.Code]
Encode_bool_hasSize [in ProgrammingTuringMachines.TM.Code.Code]
Encode_unit_hasSize [in ProgrammingTuringMachines.TM.Code.Code]


F

fill_default_not_index [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
fill_not_index [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
fill_correct_nth [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Fin_R_fillive [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Fin_L_fillive [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]


H

HaltingProblem [in ProgrammingTuringMachines.TM.LM.HaltingProblem]
halt_state_steps_k [in ProgrammingTuringMachines.TM.LM.Semantics]
halt_state_steps [in ProgrammingTuringMachines.TM.LM.Semantics]
halt_state_is_halt_state [in ProgrammingTuringMachines.TM.LM.Semantics]
halt_comp [in ProgrammingTuringMachines.TM.Combinators.While]
halt_conf_liftL [in ProgrammingTuringMachines.TM.Combinators.Switch]


I

If_RealiseIn [in ProgrammingTuringMachines.TM.Combinators.If]
If_TerminatesIn [in ProgrammingTuringMachines.TM.Combinators.If]
If_Realise [in ProgrammingTuringMachines.TM.Combinators.If]
initRight_isRight [in ProgrammingTuringMachines.TM.Code.CodeTM]
initValue_contains [in ProgrammingTuringMachines.TM.Code.CodeTM]
inject_surject [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
in_encode_retract [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
IsNil_Sem [in ProgrammingTuringMachines.TM.Code.CaseList]
isRight_isRight_size [in ProgrammingTuringMachines.TM.Code.CodeTM]
isRight_size_right [in ProgrammingTuringMachines.TM.Code.CodeTM]
isRight_size_left [in ProgrammingTuringMachines.TM.Code.CodeTM]
isRight_right [in ProgrammingTuringMachines.TM.Code.CodeTM]
isRight_size_monotone [in ProgrammingTuringMachines.TM.Code.CodeTM]
isRight_size_isRight [in ProgrammingTuringMachines.TM.Code.CodeTM]
is_halt_state_correct [in ProgrammingTuringMachines.TM.LM.Semantics]
is_halt_state_halt [in ProgrammingTuringMachines.TM.LM.Semantics]


J

JumpTarget_Terminates [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Realise [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Loop_Terminates [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Loop_Realise [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Step_Terminates [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Step_Realise [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]


L

Length_Terminates [in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Computes [in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Loop_Terminates [in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Loop_Realise [in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Step_Terminates [in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Step_Realise [in ProgrammingTuringMachines.TM.Code.ListTM]
LiftAlphabet_RealiseIn [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet_TerminatesIn [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet_unlift [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet_Realise [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet_lift [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet_comp_step [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftTapes_RealiseIn [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Terminates [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_unlift [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Realise [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_eq [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_comp_eq [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_lift [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_comp_step [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
lift_initc [in ProgrammingTuringMachines.TM.Combinators.Switch]
lookup_eq [in ProgrammingTuringMachines.TM.LM.Semantics]
Lookup_Terminates [in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Realise [in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Step_Terminates [in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Step_Realise [in ProgrammingTuringMachines.TM.LM.LookupTM]
Loop_Terminates [in ProgrammingTuringMachines.TM.LM.HaltingProblem]
Loop_Realise [in ProgrammingTuringMachines.TM.LM.HaltingProblem]
loop_split [in ProgrammingTuringMachines.TM.Prelim]
loop_merge [in ProgrammingTuringMachines.TM.Prelim]
loop_unlift [in ProgrammingTuringMachines.TM.Prelim]
loop_lift [in ProgrammingTuringMachines.TM.Prelim]
loop_monotone [in ProgrammingTuringMachines.TM.Prelim]
loop_eq_0 [in ProgrammingTuringMachines.TM.Prelim]
loop_0 [in ProgrammingTuringMachines.TM.Prelim]
loop_fulfills [in ProgrammingTuringMachines.TM.Prelim]
loop_injective [in ProgrammingTuringMachines.TM.Prelim]
loop_step [in ProgrammingTuringMachines.TM.Prelim]
loop_map [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]


M

MapSum_Terminates [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum_Computes [in ProgrammingTuringMachines.TM.Code.SumTM]
mapTape_isRight [in ProgrammingTuringMachines.TM.Code.CodeTM]
mapTape_local [in ProgrammingTuringMachines.TM.TM]
mapTape_id [in ProgrammingTuringMachines.TM.TM]
mapTape_ext [in ProgrammingTuringMachines.TM.TM]
mapTape_mapTape [in ProgrammingTuringMachines.TM.TM]
mapTape_inv_midtape [in ProgrammingTuringMachines.TM.TM]
mapTape_inv_leftof [in ProgrammingTuringMachines.TM.TM]
mapTape_inv_rightof [in ProgrammingTuringMachines.TM.TM]
mapTape_inv_niltap [in ProgrammingTuringMachines.TM.TM]
mapTape_move_right [in ProgrammingTuringMachines.TM.TM]
mapTape_move_left [in ProgrammingTuringMachines.TM.TM]
mapTape_right [in ProgrammingTuringMachines.TM.TM]
mapTape_left [in ProgrammingTuringMachines.TM.TM]
mapTape_current [in ProgrammingTuringMachines.TM.TM]
map_length_eq [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
map_removelast [in ProgrammingTuringMachines.TM.Code.ListTM]
midtape_tape_local_l_cons_right [in ProgrammingTuringMachines.TM.TM]
midtape_tape_local_l_cons [in ProgrammingTuringMachines.TM.TM]
midtape_tape_local_cons_left [in ProgrammingTuringMachines.TM.TM]
midtape_tape_local_cons [in ProgrammingTuringMachines.TM.TM]
mirrorConf_injective [in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirrorConf_involution [in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirror_tape_move_right' [in ProgrammingTuringMachines.TM.TM]
mirror_tape_move_left' [in ProgrammingTuringMachines.TM.TM]
mirror_tapes_nth [in ProgrammingTuringMachines.TM.TM]
mirror_move_involution [in ProgrammingTuringMachines.TM.TM]
mirror_tapes_injective [in ProgrammingTuringMachines.TM.TM]
mirror_tapes_involution [in ProgrammingTuringMachines.TM.TM]
mirror_tape_inv_niltape' [in ProgrammingTuringMachines.TM.TM]
mirror_tape_inv_rightof' [in ProgrammingTuringMachines.TM.TM]
mirror_tape_inv_leftof' [in ProgrammingTuringMachines.TM.TM]
mirror_tape_inv_midtape' [in ProgrammingTuringMachines.TM.TM]
mirror_tape_inv_niltape [in ProgrammingTuringMachines.TM.TM]
mirror_tape_inv_rightof [in ProgrammingTuringMachines.TM.TM]
mirror_tape_inv_leftof [in ProgrammingTuringMachines.TM.TM]
mirror_tape_inv_midtape [in ProgrammingTuringMachines.TM.TM]
mirror_tape_move_right [in ProgrammingTuringMachines.TM.TM]
mirror_tape_move_left [in ProgrammingTuringMachines.TM.TM]
mirror_tape_injective [in ProgrammingTuringMachines.TM.TM]
mirror_tape_involution [in ProgrammingTuringMachines.TM.TM]
mirror_tape_current [in ProgrammingTuringMachines.TM.TM]
mirror_tape_right [in ProgrammingTuringMachines.TM.TM]
mirror_tape_left [in ProgrammingTuringMachines.TM.TM]
Mirror_RealiseIn [in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mirror_Terminates [in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mirror_Realise [in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirror_unlift [in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirror_lift [in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirror_step [in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirror_acts_involution [in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirror_act_involution [in ProgrammingTuringMachines.TM.Combinators.Mirror]
MoveLeft_steps_comp [in ProgrammingTuringMachines.TM.Code.Copy]
MoveLeft_Terminates [in ProgrammingTuringMachines.TM.Code.Copy]
MoveLeft_Realise [in ProgrammingTuringMachines.TM.Code.Copy]
MovePar_Sem [in ProgrammingTuringMachines.TM.Compound.Multi]
MoveRight_steps_comp [in ProgrammingTuringMachines.TM.Code.Copy]
MoveRight_Terminates [in ProgrammingTuringMachines.TM.Code.Copy]
MoveRight_Realise [in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_L_steps_moveleft [in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_L_steps_midtape [in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_L_steps_local [in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_steps_moveright [in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_steps_midtape [in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_steps_local [in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_L_correct_moveleft [in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_L_correct_midtape [in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_L_correct [in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_correct_moveright [in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_correct_midtape [in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_correct [in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol_L_Terminates [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_steps_mirror [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_L_Realise [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_mirror' [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_mirror [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Terminates [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Realise [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_skip [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Step_Fun_M2_true [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Step_false [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Step_true [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Step_None [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Step_Fun_M2_None [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Step_Sem [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveValue_steps_comp [in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_Terminates [in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_Realise [in ProgrammingTuringMachines.TM.Code.Copy]
Move_Sem [in ProgrammingTuringMachines.TM.Basic.Mono]
Mult_Terminates [in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Main_Terminates [in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Loop_Terminates [in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Step_Terminates [in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Computes [in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Main_Realise [in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Loop_Realise [in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Step_Realise [in ProgrammingTuringMachines.TM.Code.NatTM]
M1_Terminates [in ProgrammingTuringMachines.TM.Code.CaseList]
M1_Realise [in ProgrammingTuringMachines.TM.Code.CaseList]


N

Nop_Sem [in ProgrammingTuringMachines.TM.Compound.Multi]
nth_map2' [in ProgrammingTuringMachines.TM.TM]
nth_map' [in ProgrammingTuringMachines.TM.TM]
Nth_Computes [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth_Loop_Realise [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth_Step_Realise [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Terminates [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Realise [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Loop_Terminates [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Loop_Realise [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Step_Terminates [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Step_Realise [in ProgrammingTuringMachines.TM.Code.ListTM]
Null_Sem [in ProgrammingTuringMachines.TM.Basic.Null]


P

pair_eq [in ProgrammingTuringMachines.TM.Code.CasePair]
pair_eq [in ProgrammingTuringMachines.TM.Code.ListTM]
pow_plus [in ProgrammingTuringMachines.TM.Relations]
Put_Terminates [in ProgrammingTuringMachines.TM.LM.StepTM]
Put_Realise [in ProgrammingTuringMachines.TM.LM.StepTM]


R

ReadChar_at_Sem [in ProgrammingTuringMachines.TM.Compound.Multi]
RealiseIn_TerminatesIn [in ProgrammingTuringMachines.TM.TM]
RealiseIn_Realise [in ProgrammingTuringMachines.TM.TM]
RealiseIn_split [in ProgrammingTuringMachines.TM.TM]
RealiseIn_monotone' [in ProgrammingTuringMachines.TM.TM]
RealiseIn_monotone [in ProgrammingTuringMachines.TM.TM]
Realise_strengthen [in ProgrammingTuringMachines.TM.TM]
Realise_total [in ProgrammingTuringMachines.TM.TM]
Realise_monotone [in ProgrammingTuringMachines.TM.TM]
Relabel_Terminates [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Relabel_RealiseIn [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Relabel_Realise [in ProgrammingTuringMachines.TM.Combinators.Combinators]
removelast_length [in ProgrammingTuringMachines.TM.Code.ListTM]
removelast_app_singleton [in ProgrammingTuringMachines.TM.Code.ListTM]
ResetEmpty_Sem [in ProgrammingTuringMachines.TM.Code.Copy]
ResetEmpty1_Sem [in ProgrammingTuringMachines.TM.Code.Copy]
Reset_steps_comp [in ProgrammingTuringMachines.TM.Code.Copy]
Reset_Realise [in ProgrammingTuringMachines.TM.Code.Copy]
Return_Terminates [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return_RealiseIn [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return_Realise [in ProgrammingTuringMachines.TM.Combinators.Combinators]
R_canonical_functional [in ProgrammingTuringMachines.TM.TM]


S

select_nth [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Seq_RealiseIn [in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
Seq_TerminatesIn [in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
Seq_Realise [in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
skipn_tl [in ProgrammingTuringMachines.TM.Code.Copy]
skipn_0 [in ProgrammingTuringMachines.TM.Code.Copy]
Skip_cons_Terminates [in ProgrammingTuringMachines.TM.Code.CaseList]
Skip_cons_Realise [in ProgrammingTuringMachines.TM.Code.CaseList]
smpl_dupfree_helper2 [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
smpl_dupfree_helper1 [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Snd_steps_comp [in ProgrammingTuringMachines.TM.Code.CasePair]
Snd_Terminates [in ProgrammingTuringMachines.TM.Code.CasePair]
Snd_Realise [in ProgrammingTuringMachines.TM.Code.CasePair]
start_not_in [in ProgrammingTuringMachines.TM.Code.Copy]
star_pow [in ProgrammingTuringMachines.TM.Relations]
star_trans [in ProgrammingTuringMachines.TM.Relations]
steps_steps_k [in ProgrammingTuringMachines.TM.LM.Semantics]
steps_k_steps [in ProgrammingTuringMachines.TM.LM.Semantics]
step_is_halt_state [in ProgrammingTuringMachines.TM.LM.Semantics]
step_functional [in ProgrammingTuringMachines.TM.LM.Semantics]
step_iff [in ProgrammingTuringMachines.TM.LM.Semantics]
step_fun_step [in ProgrammingTuringMachines.TM.LM.Semantics]
step_step_fun [in ProgrammingTuringMachines.TM.LM.Semantics]
step_comp [in ProgrammingTuringMachines.TM.Combinators.While]
step_nop_split [in ProgrammingTuringMachines.TM.Combinators.Switch]
step_nop_transition [in ProgrammingTuringMachines.TM.Combinators.Switch]
step_comp_liftR [in ProgrammingTuringMachines.TM.Combinators.Switch]
step_comp_liftL [in ProgrammingTuringMachines.TM.Combinators.Switch]
Step_Terminates [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_Realise [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_var_Terminates [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_var_Realise [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_app_Terminates [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_app_Realise [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_lam_Terminates [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_lam_Realise [in ProgrammingTuringMachines.TM.LM.StepTM]
stop_not_in [in ProgrammingTuringMachines.TM.Code.Copy]
stop_lemma [in ProgrammingTuringMachines.TM.Code.CaseList]
subrel_or2 [in ProgrammingTuringMachines.TM.Relations]
subrel_and2 [in ProgrammingTuringMachines.TM.Relations]
subrel_or [in ProgrammingTuringMachines.TM.Relations]
subrel_and [in ProgrammingTuringMachines.TM.Relations]
surjectTapes_nth [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
surjectTape_isRight' [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
surjectTape_isRight [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
surjectTape_injectTape [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
surject_inject_inr [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
surject_app [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
surject_cons [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
surject_inject [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
surject_inject_tape [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
surject_inject' [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
Switch_RealiseIn [in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch_TerminatesIn [in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch_Realise [in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch_split [in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch_merge [in ProgrammingTuringMachines.TM.Combinators.Switch]


T

TailRec_Terminates [in ProgrammingTuringMachines.TM.LM.StepTM]
TailRec_Realise [in ProgrammingTuringMachines.TM.LM.StepTM]
tapeToList_move_L [in ProgrammingTuringMachines.TM.TM]
tapeToList_move_R [in ProgrammingTuringMachines.TM.TM]
tapeToList_move [in ProgrammingTuringMachines.TM.TM]
tape_contains_rev_ext [in ProgrammingTuringMachines.TM.Code.CodeTM]
tape_contains_ext [in ProgrammingTuringMachines.TM.Code.CodeTM]
tape_contains_rev_isRight [in ProgrammingTuringMachines.TM.Code.CodeTM]
tape_local_l_move_left' [in ProgrammingTuringMachines.TM.TM]
tape_local_move_right' [in ProgrammingTuringMachines.TM.TM]
tape_left_move_left' [in ProgrammingTuringMachines.TM.TM]
tape_right_move_right' [in ProgrammingTuringMachines.TM.TM]
tape_left_move_right' [in ProgrammingTuringMachines.TM.TM]
tape_right_move_left' [in ProgrammingTuringMachines.TM.TM]
tape_right_move_left [in ProgrammingTuringMachines.TM.TM]
tape_left_move_right [in ProgrammingTuringMachines.TM.TM]
tape_local_l_move_left [in ProgrammingTuringMachines.TM.TM]
tape_local_move_right [in ProgrammingTuringMachines.TM.TM]
tape_local_nil [in ProgrammingTuringMachines.TM.TM]
tape_local_l_cons_iff [in ProgrammingTuringMachines.TM.TM]
tape_local_cons_iff [in ProgrammingTuringMachines.TM.TM]
tape_local_l_left [in ProgrammingTuringMachines.TM.TM]
tape_local_right [in ProgrammingTuringMachines.TM.TM]
tape_local_l_current_cons [in ProgrammingTuringMachines.TM.TM]
tape_local_current_cons [in ProgrammingTuringMachines.TM.TM]
tape_local_mirror' [in ProgrammingTuringMachines.TM.TM]
tape_local_mirror [in ProgrammingTuringMachines.TM.TM]
tape_move_left_right [in ProgrammingTuringMachines.TM.TM]
tape_move_right_left [in ProgrammingTuringMachines.TM.TM]
tape_is_midtape [in ProgrammingTuringMachines.TM.TM]
tape_midtape_current_left [in ProgrammingTuringMachines.TM.TM]
tape_midtape_current_right [in ProgrammingTuringMachines.TM.TM]
tape_destruct2' [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
tape_destruct2 [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
tape_local_contains [in ProgrammingTuringMachines.TM.Code.WriteValue]
TerminatesIn_extend [in ProgrammingTuringMachines.TM.TM]
TerminatesIn_monotone [in ProgrammingTuringMachines.TM.TM]
Translate_steps_comp [in ProgrammingTuringMachines.TM.Code.Copy]
Translate_Terminates [in ProgrammingTuringMachines.TM.Code.Copy]
Translate_Realise [in ProgrammingTuringMachines.TM.Code.Copy]
Translate'_Terminates [in ProgrammingTuringMachines.TM.Code.Copy]
Translate'_Realise [in ProgrammingTuringMachines.TM.Code.Copy]


W

WhileCoInduction [in ProgrammingTuringMachines.TM.Combinators.While]
WhileInduction [in ProgrammingTuringMachines.TM.Combinators.While]
While_TerminatesIn [in ProgrammingTuringMachines.TM.Combinators.While]
While_TerminatesIn_ind [in ProgrammingTuringMachines.TM.Combinators.While]
While_Realise [in ProgrammingTuringMachines.TM.Combinators.While]
While_merge_term [in ProgrammingTuringMachines.TM.Combinators.While]
While_merge_repeat [in ProgrammingTuringMachines.TM.Combinators.While]
While_split_term [in ProgrammingTuringMachines.TM.Combinators.While]
While_split_repeat [in ProgrammingTuringMachines.TM.Combinators.While]
While_split [in ProgrammingTuringMachines.TM.Combinators.While]
While_trans_repeat [in ProgrammingTuringMachines.TM.Combinators.While]
WriteMove_Sem [in ProgrammingTuringMachines.TM.Basic.Mono]
WriteString_Sem [in ProgrammingTuringMachines.TM.Compound.WriteString]
WriteString_fix_Sem [in ProgrammingTuringMachines.TM.Compound.WriteString]
WriteString_L_local [in ProgrammingTuringMachines.TM.Code.WriteValue]
WriteValue_Sem [in ProgrammingTuringMachines.TM.Code.WriteValue]
Write_String_nil [in ProgrammingTuringMachines.TM.Compound.WriteString]
Write_Sem [in ProgrammingTuringMachines.TM.Basic.Mono]



Constructor Index

A

appAT [in ProgrammingTuringMachines.TM.LM.Alphabets]
appT [in ProgrammingTuringMachines.TM.LM.Semantics]


L

L [in ProgrammingTuringMachines.TM.TM]
lamAT [in ProgrammingTuringMachines.TM.LM.Alphabets]
lamT [in ProgrammingTuringMachines.TM.LM.Semantics]
leftof [in ProgrammingTuringMachines.TM.TM]


M

midtape [in ProgrammingTuringMachines.TM.TM]
mk_mconfig [in ProgrammingTuringMachines.TM.TM]


N

N [in ProgrammingTuringMachines.TM.TM]
niltape [in ProgrammingTuringMachines.TM.TM]


P

pow_S [in ProgrammingTuringMachines.TM.Relations]
pow_0 [in ProgrammingTuringMachines.TM.Relations]


R

R [in ProgrammingTuringMachines.TM.TM]
retAT [in ProgrammingTuringMachines.TM.LM.Alphabets]
retT [in ProgrammingTuringMachines.TM.LM.Semantics]
rightof [in ProgrammingTuringMachines.TM.TM]


S

sigList_cons [in ProgrammingTuringMachines.TM.Code.Code]
sigList_nil [in ProgrammingTuringMachines.TM.Code.Code]
sigList_X [in ProgrammingTuringMachines.TM.Code.Code]
sigNat_S [in ProgrammingTuringMachines.TM.Code.Code]
sigNat_O [in ProgrammingTuringMachines.TM.Code.Code]
sigOption_Some [in ProgrammingTuringMachines.TM.Code.Code]
sigOption_None [in ProgrammingTuringMachines.TM.Code.Code]
sigOption_X [in ProgrammingTuringMachines.TM.Code.Code]
sigPair_Y [in ProgrammingTuringMachines.TM.Code.Code]
sigPair_X [in ProgrammingTuringMachines.TM.Code.Code]
sigSum_inr [in ProgrammingTuringMachines.TM.Code.Code]
sigSum_inl [in ProgrammingTuringMachines.TM.Code.Code]
sigSum_Y [in ProgrammingTuringMachines.TM.Code.Code]
sigSum_X [in ProgrammingTuringMachines.TM.Code.Code]
starC [in ProgrammingTuringMachines.TM.Relations]
starR [in ProgrammingTuringMachines.TM.Relations]
START [in ProgrammingTuringMachines.TM.Code.CodeTM]
step_load [in ProgrammingTuringMachines.TM.LM.Semantics]
step_beta [in ProgrammingTuringMachines.TM.LM.Semantics]
step_pushVal [in ProgrammingTuringMachines.TM.LM.Semantics]
STOP [in ProgrammingTuringMachines.TM.Code.CodeTM]


U

UNKNOWN [in ProgrammingTuringMachines.TM.Code.CodeTM]


V

varT [in ProgrammingTuringMachines.TM.LM.Semantics]


W

While_T_intro [in ProgrammingTuringMachines.TM.Combinators.While]
While_Rel''_loop [in ProgrammingTuringMachines.TM.Combinators.While]
While_Rel''_one [in ProgrammingTuringMachines.TM.Combinators.While]



Inductive Index

A

ACom [in ProgrammingTuringMachines.TM.LM.Alphabets]


B

boundary [in ProgrammingTuringMachines.TM.Code.CodeTM]


C

Com [in ProgrammingTuringMachines.TM.LM.Semantics]


M

move [in ProgrammingTuringMachines.TM.TM]


P

pow [in ProgrammingTuringMachines.TM.Relations]


S

sigList [in ProgrammingTuringMachines.TM.Code.Code]
sigNat [in ProgrammingTuringMachines.TM.Code.Code]
sigOption [in ProgrammingTuringMachines.TM.Code.Code]
sigPair [in ProgrammingTuringMachines.TM.Code.Code]
sigSum [in ProgrammingTuringMachines.TM.Code.Code]
star [in ProgrammingTuringMachines.TM.Relations]
step [in ProgrammingTuringMachines.TM.LM.Semantics]


T

tape [in ProgrammingTuringMachines.TM.TM]


W

While_T [in ProgrammingTuringMachines.TM.Combinators.While]
While_Rel [in ProgrammingTuringMachines.TM.Combinators.While]



Projection Index

C

cstate [in ProgrammingTuringMachines.TM.TM]
ctapes [in ProgrammingTuringMachines.TM.TM]


E

encode [in ProgrammingTuringMachines.TM.Code.Code]


H

halt [in ProgrammingTuringMachines.TM.TM]


S

start [in ProgrammingTuringMachines.TM.TM]
states [in ProgrammingTuringMachines.TM.TM]


T

trans [in ProgrammingTuringMachines.TM.TM]



Section Index

A

AddTapes [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Append [in ProgrammingTuringMachines.TM.Code.ListTM]


C

CaseFin [in ProgrammingTuringMachines.TM.Code.CaseFin]
CaseList [in ProgrammingTuringMachines.TM.Code.CaseList]
CaseNat [in ProgrammingTuringMachines.TM.Code.CaseNat]
CaseNat.NatConstructor [in ProgrammingTuringMachines.TM.Code.CaseNat]
CaseOption [in ProgrammingTuringMachines.TM.Code.CaseSum]
CasePair [in ProgrammingTuringMachines.TM.Code.CasePair]
CaseSum [in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum.SumConstr [in ProgrammingTuringMachines.TM.Code.CaseSum]
ChangeAlphabet [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Composition [in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
Computes_ChangeAlphabet2 [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_ChangeAlphabet [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Copy [in ProgrammingTuringMachines.TM.Code.Copy]
Copy [in ProgrammingTuringMachines.TM.Compound.Multi]
CopySymbols [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopyValue [in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_steps_comp [in ProgrammingTuringMachines.TM.Code.Copy]


D

Diverge [in ProgrammingTuringMachines.TM.Compound.Multi]
DoAct [in ProgrammingTuringMachines.TM.Basic.Mono]
DoAct_Derived [in ProgrammingTuringMachines.TM.Basic.Mono]


E

Encode_nat [in ProgrammingTuringMachines.TM.Code.Code]
Encode_list [in ProgrammingTuringMachines.TM.Code.Code]
Encode_option [in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair [in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum [in ProgrammingTuringMachines.TM.Code.Code]
Encode_map_comp [in ProgrammingTuringMachines.TM.Code.Code]
Encode_map [in ProgrammingTuringMachines.TM.Code.Code]
Encode_Finite [in ProgrammingTuringMachines.TM.Code.Code]


F

Fill [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Fix_Sig.Computes2.Computes2_Ext [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes2 [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes.Computes_Ext [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Computes [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.InitTape [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Encodes_Ext [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig.Tape_Contains [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sig [in ProgrammingTuringMachines.TM.Code.CodeTM]
Fix_Sigma [in ProgrammingTuringMachines.TM.TM]
Fix_X2 [in ProgrammingTuringMachines.TM.Relations]


I

Id [in ProgrammingTuringMachines.TM.Combinators.Combinators]
If [in ProgrammingTuringMachines.TM.Combinators.If]
InjectSurject [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
InjectTape [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
IsRight [in ProgrammingTuringMachines.TM.Code.CodeTM]


L

Lenght [in ProgrammingTuringMachines.TM.Code.ListTM]
LiftAlphabet [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftNM [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Rel [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
lift_sigma_tau [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
ListStuff [in ProgrammingTuringMachines.TM.Code.ListTM]
Lookup [in ProgrammingTuringMachines.TM.LM.LookupTM]
Loop [in ProgrammingTuringMachines.TM.Prelim]
LoopLift [in ProgrammingTuringMachines.TM.Prelim]
LoopMerge [in ProgrammingTuringMachines.TM.Prelim]
loop_map [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]


M

Map [in ProgrammingTuringMachines.TM.Prelim]
MapCode [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
MapSum [in ProgrammingTuringMachines.TM.Code.SumTM]
MapTape [in ProgrammingTuringMachines.TM.TM]
MatchTapes [in ProgrammingTuringMachines.TM.TM]
Mirror [in ProgrammingTuringMachines.TM.Combinators.Mirror]
MirrorTape [in ProgrammingTuringMachines.TM.TM]
Mk_Mono [in ProgrammingTuringMachines.TM.Basic.Mono]
Mono_Nop [in ProgrammingTuringMachines.TM.Basic.Null]
Move [in ProgrammingTuringMachines.TM.Code.Copy]
MovePar [in ProgrammingTuringMachines.TM.Compound.Multi]
MoveToSymbol [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveValue [in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps_comp [in ProgrammingTuringMachines.TM.Code.Copy]
Move_steps_comp [in ProgrammingTuringMachines.TM.Code.Copy]


N

Nop [in ProgrammingTuringMachines.TM.Compound.Multi]
Nop_Action [in ProgrammingTuringMachines.TM.TM]
Nth [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth' [in ProgrammingTuringMachines.TM.Code.ListTM]


O

OtherWhileRel [in ProgrammingTuringMachines.TM.Combinators.While]


R

ReadChar [in ProgrammingTuringMachines.TM.Compound.Multi]
ReadChar [in ProgrammingTuringMachines.TM.Basic.Mono]
Relabel [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Return [in ProgrammingTuringMachines.TM.Combinators.Combinators]


S

Semantics [in ProgrammingTuringMachines.TM.TM]
Semantics [in ProgrammingTuringMachines.TM.LM.Semantics]
Semantics.Canonical_Termination [in ProgrammingTuringMachines.TM.TM]
Semantics.Canonical_Correctness [in ProgrammingTuringMachines.TM.TM]
Star_Pow [in ProgrammingTuringMachines.TM.Relations]
StepMachine [in ProgrammingTuringMachines.TM.LM.StepTM]
Steps_comp [in ProgrammingTuringMachines.TM.Code.CaseList]
Steps_comp [in ProgrammingTuringMachines.TM.Code.CasePair]
SujectTape [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
SurjectInject [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Switch [in ProgrammingTuringMachines.TM.Combinators.Switch]


T

Tape_Local [in ProgrammingTuringMachines.TM.TM]
test [in ProgrammingTuringMachines.TM.Compound.TMTac]
Translate [in ProgrammingTuringMachines.TM.Code.Copy]
TranslateAct [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
Translate_steps_comp [in ProgrammingTuringMachines.TM.Code.Copy]


W

While [in ProgrammingTuringMachines.TM.Combinators.While]
WhileCoInduction [in ProgrammingTuringMachines.TM.Combinators.While]
WhileInduction [in ProgrammingTuringMachines.TM.Combinators.While]
While.While_TerminatesIn_coind [in ProgrammingTuringMachines.TM.Combinators.While]
While.While_TerminatesIn [in ProgrammingTuringMachines.TM.Combinators.While]
WriteValue [in ProgrammingTuringMachines.TM.Code.WriteValue]
Write_String [in ProgrammingTuringMachines.TM.Compound.WriteString]



Instance Index

A

ACom_inhab [in ProgrammingTuringMachines.TM.LM.Alphabets]
ACom_finType [in ProgrammingTuringMachines.TM.LM.Alphabets]
ACom_eq_dec [in ProgrammingTuringMachines.TM.LM.Alphabets]


B

boundary_fin [in ProgrammingTuringMachines.TM.Code.CodeTM]
boundary_eq [in ProgrammingTuringMachines.TM.Code.CodeTM]


E

Encode_Heap [in ProgrammingTuringMachines.TM.LM.Alphabets]
Encode_HEntr [in ProgrammingTuringMachines.TM.LM.Alphabets]
Encode_HEntr' [in ProgrammingTuringMachines.TM.LM.Alphabets]
Encode_HClos [in ProgrammingTuringMachines.TM.LM.Alphabets]
Encode_Prog [in ProgrammingTuringMachines.TM.LM.Alphabets]
Encode_Com [in ProgrammingTuringMachines.TM.LM.Alphabets]
Encode_ACom [in ProgrammingTuringMachines.TM.LM.Alphabets]
Encode_nat [in ProgrammingTuringMachines.TM.Code.Code]
Encode_list [in ProgrammingTuringMachines.TM.Code.Code]
Encode_option [in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair [in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum [in ProgrammingTuringMachines.TM.Code.Code]
Encode_map [in ProgrammingTuringMachines.TM.Code.Code]
Encode_Finite [in ProgrammingTuringMachines.TM.Code.Code]
Encode_Fin [in ProgrammingTuringMachines.TM.Code.Code]
Encode_bool [in ProgrammingTuringMachines.TM.Code.Code]
Encode_unit [in ProgrammingTuringMachines.TM.Code.Code]
eqrel_eq [in ProgrammingTuringMachines.TM.Relations]
eqrel_pre [in ProgrammingTuringMachines.TM.Relations]
Eq_in_equivalence [in ProgrammingTuringMachines.TM.Relations]


H

halt_state_dec [in ProgrammingTuringMachines.TM.LM.Semantics]


M

move_finC [in ProgrammingTuringMachines.TM.TM]
move_eq_dec [in ProgrammingTuringMachines.TM.TM]


R

Retract_sigOption_sigSum [in ProgrammingTuringMachines.TM.Code.CaseSum]
Retract_plus [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Retract_sigList_X [in ProgrammingTuringMachines.TM.Code.Code]
Retract_sigOption_X [in ProgrammingTuringMachines.TM.Code.Code]
Retract_sigPair_Y [in ProgrammingTuringMachines.TM.Code.Code]
Retract_sigPair_X [in ProgrammingTuringMachines.TM.Code.Code]
Retract_sigSum_Y [in ProgrammingTuringMachines.TM.Code.Code]
Retract_sigSum_X [in ProgrammingTuringMachines.TM.Code.Code]
retr_X_list' [in ProgrammingTuringMachines.TM.Code.ListTM]
retr_X_opt [in ProgrammingTuringMachines.TM.Code.ListTM]
retr_X_list [in ProgrammingTuringMachines.TM.Code.ListTM]


S

sigList_fin [in ProgrammingTuringMachines.TM.Code.Code]
sigList_dec [in ProgrammingTuringMachines.TM.Code.Code]
sigNat_fin [in ProgrammingTuringMachines.TM.Code.Code]
sigNat_eq [in ProgrammingTuringMachines.TM.Code.Code]
sigOption_fin [in ProgrammingTuringMachines.TM.Code.Code]
sigOption_dec [in ProgrammingTuringMachines.TM.Code.Code]
sigPair_fin [in ProgrammingTuringMachines.TM.Code.Code]
sigPair_dec [in ProgrammingTuringMachines.TM.Code.Code]
sigSum_fin [in ProgrammingTuringMachines.TM.Code.Code]
sigSum_dec [in ProgrammingTuringMachines.TM.Code.Code]
star_preorder [in ProgrammingTuringMachines.TM.Relations]



Abbreviation Index

I

injectTape [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]


M

Match [in ProgrammingTuringMachines.TM.Combinators.Switch]
MATCH [in ProgrammingTuringMachines.TM.Combinators.Switch]
M1 [in ProgrammingTuringMachines.TM.Combinators.Switch]


P

p1 [in ProgrammingTuringMachines.TM.Combinators.Switch]


S

sigList [in ProgrammingTuringMachines.TM.Code.ListTM]
sigPair [in ProgrammingTuringMachines.TM.Code.CasePair]
surjectTape [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]


W

WHILE [in ProgrammingTuringMachines.TM.Combinators.While]



Definition Index

A

Add [in ProgrammingTuringMachines.TM.Code.NatTM]
add_tapes [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Add_steps [in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Main_steps [in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Loop_steps [in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Main_Rel [in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Loop_Rel [in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Step_Rel [in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Main [in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Loop [in ProgrammingTuringMachines.TM.Code.NatTM]
Add_Step [in ProgrammingTuringMachines.TM.Code.NatTM]
App [in ProgrammingTuringMachines.TM.Code.ListTM]
App_Com_T [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Com_steps [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Com_Rel [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Com [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_ACom_T [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_ACom_steps [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_ACom_Rel [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_ACom [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Comens_T [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Comens_steps [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Comens_Rel [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_Comens [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
App_T [in ProgrammingTuringMachines.TM.Code.ListTM]
App_steps [in ProgrammingTuringMachines.TM.Code.ListTM]
app_tapes [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
App' [in ProgrammingTuringMachines.TM.Code.ListTM]
App'_T [in ProgrammingTuringMachines.TM.Code.ListTM]
App'_steps [in ProgrammingTuringMachines.TM.Code.ListTM]
App'_Rel [in ProgrammingTuringMachines.TM.Code.ListTM]


C

Canonical_T [in ProgrammingTuringMachines.TM.TM]
Canonical_Rel [in ProgrammingTuringMachines.TM.TM]
CaseCom [in ProgrammingTuringMachines.TM.LM.CaseCom]
CaseCom_steps [in ProgrammingTuringMachines.TM.LM.CaseCom]
CaseCom_Rel [in ProgrammingTuringMachines.TM.LM.CaseCom]
CaseFin [in ProgrammingTuringMachines.TM.Code.CaseFin]
CaseFin_Rel [in ProgrammingTuringMachines.TM.Code.CaseFin]
CaseList [in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList_steps [in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList_steps_nil [in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList_steps_cons [in ProgrammingTuringMachines.TM.Code.CaseList]
CaseList_Rel [in ProgrammingTuringMachines.TM.Code.CaseList]
CaseNat [in ProgrammingTuringMachines.TM.Code.CaseNat]
CaseNat_steps [in ProgrammingTuringMachines.TM.Code.CaseNat]
CaseNat_Rel [in ProgrammingTuringMachines.TM.Code.CaseNat]
CaseOption [in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseOption_steps [in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseOption_Rel [in ProgrammingTuringMachines.TM.Code.CaseSum]
CasePair [in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair_T [in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair_steps [in ProgrammingTuringMachines.TM.Code.CasePair]
CasePair_Rel [in ProgrammingTuringMachines.TM.Code.CasePair]
CaseSum [in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum_steps [in ProgrammingTuringMachines.TM.Code.CaseSum]
CaseSum_Rel [in ProgrammingTuringMachines.TM.Code.CaseSum]
ChangeAlphabet [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
Computes_T [in ProgrammingTuringMachines.TM.Code.CodeTM]
Computes_Rel [in ProgrammingTuringMachines.TM.Code.CodeTM]
Computes2_T [in ProgrammingTuringMachines.TM.Code.CodeTM]
Computes2_Rel [in ProgrammingTuringMachines.TM.Code.CodeTM]
ConsClos [in ProgrammingTuringMachines.TM.LM.StepTM]
ConsClos_T [in ProgrammingTuringMachines.TM.LM.StepTM]
ConsClos_steps [in ProgrammingTuringMachines.TM.LM.StepTM]
ConsClos_Rel [in ProgrammingTuringMachines.TM.LM.StepTM]
Constr_varT_steps [in ProgrammingTuringMachines.TM.LM.CaseCom]
Constr_varT_Rel [in ProgrammingTuringMachines.TM.LM.CaseCom]
Constr_varT [in ProgrammingTuringMachines.TM.LM.CaseCom]
Constr_ACom_steps [in ProgrammingTuringMachines.TM.LM.CaseCom]
Constr_ACom_Rel [in ProgrammingTuringMachines.TM.LM.CaseCom]
Constr_ACom [in ProgrammingTuringMachines.TM.LM.CaseCom]
Constr_cons_steps [in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_cons_Rel [in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_cons [in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_nil_steps [in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_nil_Rel [in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_nil [in ProgrammingTuringMachines.TM.Code.CaseList]
Constr_None_steps [in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_None [in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_None_Rel [in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_Some_steps [in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_Some [in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_Some_Rel [in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_inr_steps [in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_inl_steps [in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_inr [in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_inl [in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_inr_Rel [in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_inl_Rel [in ProgrammingTuringMachines.TM.Code.CaseSum]
Constr_pair_T [in ProgrammingTuringMachines.TM.Code.CasePair]
Constr_pair_steps [in ProgrammingTuringMachines.TM.Code.CasePair]
Constr_pair [in ProgrammingTuringMachines.TM.Code.CasePair]
Constr_pair_Rel [in ProgrammingTuringMachines.TM.Code.CasePair]
Constr_O_steps [in ProgrammingTuringMachines.TM.Code.CaseNat]
Constr_O [in ProgrammingTuringMachines.TM.Code.CaseNat]
Constr_S_steps [in ProgrammingTuringMachines.TM.Code.CaseNat]
Constr_S [in ProgrammingTuringMachines.TM.Code.CaseNat]
CopyChar [in ProgrammingTuringMachines.TM.Compound.Multi]
CopyChar_Rel [in ProgrammingTuringMachines.TM.Compound.Multi]
CopySymbols [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_L_Rel [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_L [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_Rel [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_Step_Rel [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopySymbols_Step [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
CopyValue [in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_steps [in ProgrammingTuringMachines.TM.Code.Copy]
CopyValue_Rel [in ProgrammingTuringMachines.TM.Code.Copy]
current [in ProgrammingTuringMachines.TM.TM]
current_chars [in ProgrammingTuringMachines.TM.TM]


D

Diverge [in ProgrammingTuringMachines.TM.Compound.Multi]
Diverge_Rel [in ProgrammingTuringMachines.TM.Compound.Multi]
doAct [in ProgrammingTuringMachines.TM.TM]
DoAct [in ProgrammingTuringMachines.TM.Basic.Mono]
doAct_multi [in ProgrammingTuringMachines.TM.TM]
DoAct_Rel [in ProgrammingTuringMachines.TM.Basic.Mono]
DoAct_TM [in ProgrammingTuringMachines.TM.Basic.Mono]


E

Encode_Com_size [in ProgrammingTuringMachines.TM.LM.Alphabets]
Encode_list_size [in ProgrammingTuringMachines.TM.Code.Code]
encode_list [in ProgrammingTuringMachines.TM.Code.Code]
Encode_option_size [in ProgrammingTuringMachines.TM.Code.Code]
Encode_pair_size [in ProgrammingTuringMachines.TM.Code.Code]
Encode_sum_size [in ProgrammingTuringMachines.TM.Code.Code]
eqrel [in ProgrammingTuringMachines.TM.Relations]
Eq_in [in ProgrammingTuringMachines.TM.Relations]
execTM [in ProgrammingTuringMachines.TM.TM]
execTM_p [in ProgrammingTuringMachines.TM.TM]


F

fill [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
fill_default [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
FinR [in ProgrammingTuringMachines.TM.Prelim]
functional [in ProgrammingTuringMachines.TM.Relations]


H

HAdd [in ProgrammingTuringMachines.TM.LM.Semantics]
haltConf [in ProgrammingTuringMachines.TM.TM]
Halts [in ProgrammingTuringMachines.TM.LM.HaltingProblem]
halts [in ProgrammingTuringMachines.TM.LM.Semantics]
halts_k [in ProgrammingTuringMachines.TM.LM.Semantics]
halt_state [in ProgrammingTuringMachines.TM.LM.Semantics]
halt_liftL [in ProgrammingTuringMachines.TM.Combinators.Switch]
HClos [in ProgrammingTuringMachines.TM.LM.Semantics]
Heap [in ProgrammingTuringMachines.TM.LM.Semantics]
HEntr [in ProgrammingTuringMachines.TM.LM.Semantics]


I

Id [in ProgrammingTuringMachines.TM.Combinators.Combinators]
If [in ProgrammingTuringMachines.TM.Combinators.If]
ignoreParam [in ProgrammingTuringMachines.TM.Relations]
initc [in ProgrammingTuringMachines.TM.TM]
initRight [in ProgrammingTuringMachines.TM.Code.CodeTM]
initTapes [in ProgrammingTuringMachines.TM.LM.HaltingProblem]
initValue [in ProgrammingTuringMachines.TM.Code.CodeTM]
injectSymbols [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
injectTape [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
injectTapes [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
IsNil [in ProgrammingTuringMachines.TM.Code.CaseList]
IsNil_steps [in ProgrammingTuringMachines.TM.Code.CaseList]
IsNil_Rel [in ProgrammingTuringMachines.TM.Code.CaseList]
isRight [in ProgrammingTuringMachines.TM.Code.CodeTM]
isRight_size [in ProgrammingTuringMachines.TM.Code.CodeTM]
isStart [in ProgrammingTuringMachines.TM.Code.Copy]
isStop [in ProgrammingTuringMachines.TM.Code.Copy]
is_halt_state [in ProgrammingTuringMachines.TM.LM.Semantics]


J

JumpTarget [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
jumpTarget [in ProgrammingTuringMachines.TM.LM.Semantics]
JumpTarget_T [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_steps [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Rel [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Loop_T [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Loop_steps [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Loop_Rel [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Loop [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
jumpTarget_k [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Step_T [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Step_steps [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Step_steps_CaseList [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Step_steps_CaseCom [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Step_Rel [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
JumpTarget_Step [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]


L

left [in ProgrammingTuringMachines.TM.TM]
Length [in ProgrammingTuringMachines.TM.Code.ListTM]
Length_T [in ProgrammingTuringMachines.TM.Code.ListTM]
Length_steps [in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Loop_T [in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Loop_steps [in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Loop_Rel [in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Loop [in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Step_T [in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Step_steps [in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Step_Rel [in ProgrammingTuringMachines.TM.Code.ListTM]
Length_Step [in ProgrammingTuringMachines.TM.Code.ListTM]
LiftAlphabet [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftAlphabet_TM [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
LiftTapes [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_TM [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_trans [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_T [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_Rel [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_eq_Rel [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
LiftTapes_select_Rel [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
lift_confR [in ProgrammingTuringMachines.TM.Combinators.Switch]
lift_confL [in ProgrammingTuringMachines.TM.Combinators.Switch]
lift_trans [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
lift_sigma_tau_T [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
lift_sigma_tau_Rel [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
llength [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
llength [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
llength' [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
lookup [in ProgrammingTuringMachines.TM.LM.Semantics]
Lookup [in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_T [in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_steps [in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Rel [in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Step_T [in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Step_steps [in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Step_steps_Nth' [in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Step_steps_CaseOption [in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Step_steps_CaseNat [in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Step_Rel [in ProgrammingTuringMachines.TM.LM.LookupTM]
Lookup_Step [in ProgrammingTuringMachines.TM.LM.LookupTM]
Loop [in ProgrammingTuringMachines.TM.LM.HaltingProblem]
loop [in ProgrammingTuringMachines.TM.Prelim]
loopM [in ProgrammingTuringMachines.TM.TM]
Loop_T [in ProgrammingTuringMachines.TM.LM.HaltingProblem]
Loop_steps [in ProgrammingTuringMachines.TM.LM.HaltingProblem]
Loop_Rel [in ProgrammingTuringMachines.TM.LM.HaltingProblem]


M

MapSum [in ProgrammingTuringMachines.TM.Code.SumTM]
MapSum_steps [in ProgrammingTuringMachines.TM.Code.SumTM]
mapTape [in ProgrammingTuringMachines.TM.TM]
mapTapes [in ProgrammingTuringMachines.TM.TM]
map_snd [in ProgrammingTuringMachines.TM.Prelim]
map_fst [in ProgrammingTuringMachines.TM.Prelim]
map_inr [in ProgrammingTuringMachines.TM.Prelim]
map_inl [in ProgrammingTuringMachines.TM.Prelim]
map_opt [in ProgrammingTuringMachines.TM.Prelim]
map_sum [in ProgrammingTuringMachines.TM.Code.SumTM]
map_act [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
Mirror [in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirrorConf [in ProgrammingTuringMachines.TM.Combinators.Mirror]
MirrorTM [in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirror_move [in ProgrammingTuringMachines.TM.TM]
mirror_tapes [in ProgrammingTuringMachines.TM.TM]
mirror_tape [in ProgrammingTuringMachines.TM.TM]
Mirror_T [in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mirror_Rel [in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mirror_trans [in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirror_acts [in ProgrammingTuringMachines.TM.Combinators.Mirror]
mirror_act [in ProgrammingTuringMachines.TM.Combinators.Mirror]
Mk_R_p [in ProgrammingTuringMachines.TM.Basic.Mono]
Mk_Mono_TM [in ProgrammingTuringMachines.TM.Basic.Mono]
Move [in ProgrammingTuringMachines.TM.Basic.Mono]
MoveLeft [in ProgrammingTuringMachines.TM.Code.Copy]
MoveLeft_steps [in ProgrammingTuringMachines.TM.Code.Copy]
MoveLeft_Rel [in ProgrammingTuringMachines.TM.Code.Copy]
MovePar [in ProgrammingTuringMachines.TM.Compound.Multi]
MovePar_R [in ProgrammingTuringMachines.TM.Compound.Multi]
MoveRight [in ProgrammingTuringMachines.TM.Code.Copy]
MoveRight_steps [in ProgrammingTuringMachines.TM.Code.Copy]
MoveRight_Rel [in ProgrammingTuringMachines.TM.Code.Copy]
MoveToSymbol [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_L_Rel [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_L [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Rel [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Step_Rel [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Step_Fun [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveToSymbol_Step [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
MoveValue [in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_steps [in ProgrammingTuringMachines.TM.Code.Copy]
MoveValue_Rel [in ProgrammingTuringMachines.TM.Code.Copy]
Move_Rel [in ProgrammingTuringMachines.TM.Basic.Mono]
Mult [in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_steps [in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Main_steps [in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Loop_steps [in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Step_steps [in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Main_Rel [in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Loop_Rel [in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Step_Rel [in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Main [in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Loop [in ProgrammingTuringMachines.TM.Code.NatTM]
Mult_Step [in ProgrammingTuringMachines.TM.Code.NatTM]
M1 [in ProgrammingTuringMachines.TM.Code.CaseList]
M1_Rel [in ProgrammingTuringMachines.TM.Code.CaseList]


N

Nop [in ProgrammingTuringMachines.TM.Compound.Multi]
nop_action [in ProgrammingTuringMachines.TM.TM]
Nop_Rel [in ProgrammingTuringMachines.TM.Compound.Multi]
not_index [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Nth [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth_Loop [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth_Loop_Rel [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth_Step [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth_Step_Rel [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth' [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_T [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_steps [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Rel [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Loop_T [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Loop_steps [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Loop [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Loop_Rel [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Step_T [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Step_steps [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Step [in ProgrammingTuringMachines.TM.Code.ListTM]
Nth'_Step_Rel [in ProgrammingTuringMachines.TM.Code.ListTM]
Null [in ProgrammingTuringMachines.TM.Basic.Null]
NullTM [in ProgrammingTuringMachines.TM.Basic.Null]
Null_Rel [in ProgrammingTuringMachines.TM.Basic.Null]


O

opt_to_sum [in ProgrammingTuringMachines.TM.Code.CaseSum]
O_Rel [in ProgrammingTuringMachines.TM.Code.CaseNat]


P

plus' [in ProgrammingTuringMachines.TM.Prelim]
pRel [in ProgrammingTuringMachines.TM.TM]
Pro [in ProgrammingTuringMachines.TM.LM.Semantics]
pTM [in ProgrammingTuringMachines.TM.TM]
put [in ProgrammingTuringMachines.TM.LM.Semantics]
Put [in ProgrammingTuringMachines.TM.LM.StepTM]
Put_T [in ProgrammingTuringMachines.TM.LM.StepTM]
Put_steps [in ProgrammingTuringMachines.TM.LM.StepTM]
Put_Rel [in ProgrammingTuringMachines.TM.LM.StepTM]


R

rcomp [in ProgrammingTuringMachines.TM.Relations]
ReadChar [in ProgrammingTuringMachines.TM.Basic.Mono]
ReadChar_at_Rel [in ProgrammingTuringMachines.TM.Compound.Multi]
ReadChar_at [in ProgrammingTuringMachines.TM.Compound.Multi]
ReadChar_Sem [in ProgrammingTuringMachines.TM.Basic.Mono]
ReadChar_Rel [in ProgrammingTuringMachines.TM.Basic.Mono]
ReadChar_TM [in ProgrammingTuringMachines.TM.Basic.Mono]
Realise [in ProgrammingTuringMachines.TM.TM]
RealiseIn [in ProgrammingTuringMachines.TM.TM]
Rel [in ProgrammingTuringMachines.TM.Relations]
Relabel [in ProgrammingTuringMachines.TM.Combinators.Combinators]
Reset [in ProgrammingTuringMachines.TM.Code.Copy]
ResetEmpty [in ProgrammingTuringMachines.TM.Code.Copy]
ResetEmpty_steps [in ProgrammingTuringMachines.TM.Code.Copy]
ResetEmpty_Rel [in ProgrammingTuringMachines.TM.Code.Copy]
ResetEmpty1 [in ProgrammingTuringMachines.TM.Code.Copy]
ResetEmpty1_steps [in ProgrammingTuringMachines.TM.Code.Copy]
ResetEmpty1_Rel [in ProgrammingTuringMachines.TM.Code.Copy]
Reset_Terminates [in ProgrammingTuringMachines.TM.Code.Copy]
Reset_steps [in ProgrammingTuringMachines.TM.Code.Copy]
Reset_Rel [in ProgrammingTuringMachines.TM.Code.Copy]
restrict [in ProgrammingTuringMachines.TM.Relations]
retr_closures_step [in ProgrammingTuringMachines.TM.LM.HaltingProblem]
retr_heap_step [in ProgrammingTuringMachines.TM.LM.HaltingProblem]
retr_nat_prog [in ProgrammingTuringMachines.TM.LM.JumpTargetTM]
retr_sigY_sigMap' [in ProgrammingTuringMachines.TM.Code.SumTM]
retr_sigY_sigMap [in ProgrammingTuringMachines.TM.Code.SumTM]
retr_sigX_sigMap' [in ProgrammingTuringMachines.TM.Code.SumTM]
retr_sigX_sigMap [in ProgrammingTuringMachines.TM.Code.SumTM]
retr_hent'_lookup [in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_hent'_heap [in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_hent_lookup [in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_hent_heap [in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_clos_lookup_heap [in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_clos_heap [in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_nat_lookup_entry [in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_nat_heap_entry [in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_nat_lookup_clos_var [in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_nat_clos_var [in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_nat_lookup_clos_ad [in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_nat_clos_ad [in ProgrammingTuringMachines.TM.LM.LookupTM]
retr_closure_step [in ProgrammingTuringMachines.TM.LM.StepTM]
retr_hent_step [in ProgrammingTuringMachines.TM.LM.StepTM]
retr_hent'_step [in ProgrammingTuringMachines.TM.LM.StepTM]
retr_clos_step_hent [in ProgrammingTuringMachines.TM.LM.StepTM]
retr_nat_step_hent [in ProgrammingTuringMachines.TM.LM.StepTM]
retr_nat_step_clos_var [in ProgrammingTuringMachines.TM.LM.StepTM]
retr_nat_clos_var [in ProgrammingTuringMachines.TM.LM.StepTM]
retr_nat_step_clos_ad [in ProgrammingTuringMachines.TM.LM.StepTM]
retr_nat_clos_ad [in ProgrammingTuringMachines.TM.LM.StepTM]
retr_tok_step [in ProgrammingTuringMachines.TM.LM.StepTM]
retr_pro_step [in ProgrammingTuringMachines.TM.LM.StepTM]
retr_pro_clos [in ProgrammingTuringMachines.TM.LM.StepTM]
retr_clos_step [in ProgrammingTuringMachines.TM.LM.StepTM]
Return [in ProgrammingTuringMachines.TM.Combinators.Combinators]
rfix [in ProgrammingTuringMachines.TM.Relations]
right [in ProgrammingTuringMachines.TM.TM]
rimplication [in ProgrammingTuringMachines.TM.Relations]
rIntersection [in ProgrammingTuringMachines.TM.Relations]
rintersection [in ProgrammingTuringMachines.TM.Relations]
rlength [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
rlength [in ProgrammingTuringMachines.TM.Compound.MoveToSymbol]
rlength' [in ProgrammingTuringMachines.TM.Compound.CopySymbols]
rUnion [in ProgrammingTuringMachines.TM.Relations]
runion [in ProgrammingTuringMachines.TM.Relations]


S

select [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
selectConf [in ProgrammingTuringMachines.TM.Lifting.LiftTapes]
Seq [in ProgrammingTuringMachines.TM.Combinators.SequentialComposition]
sigCom [in ProgrammingTuringMachines.TM.LM.Alphabets]
sigCom_fin [in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHAdd [in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHAdd_fin [in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHClos [in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHClos_fin [in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHeap [in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHeap_fin [in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHEntr [in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHEntr_fin [in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHEntr' [in ProgrammingTuringMachines.TM.LM.Alphabets]
sigHEntr'_fin [in ProgrammingTuringMachines.TM.LM.Alphabets]
sigPro [in ProgrammingTuringMachines.TM.LM.Alphabets]
sigPro_fin [in ProgrammingTuringMachines.TM.LM.Alphabets]
sigStep [in ProgrammingTuringMachines.TM.LM.HaltingProblem]
size [in ProgrammingTuringMachines.TM.Code.Code]
sizeOfmTapes [in ProgrammingTuringMachines.TM.TM]
sizeOfTape [in ProgrammingTuringMachines.TM.TM]
Skip_cons_Rel [in ProgrammingTuringMachines.TM.Code.CaseList]
Skip_cons [in ProgrammingTuringMachines.TM.Code.CaseList]
Snd [in ProgrammingTuringMachines.TM.Code.CasePair]
Snd_T [in ProgrammingTuringMachines.TM.Code.CasePair]
Snd_steps [in ProgrammingTuringMachines.TM.Code.CasePair]
Snd_Rel [in ProgrammingTuringMachines.TM.Code.CasePair]
state [in ProgrammingTuringMachines.TM.LM.Semantics]
step [in ProgrammingTuringMachines.TM.TM]
Step [in ProgrammingTuringMachines.TM.LM.StepTM]
steps [in ProgrammingTuringMachines.TM.LM.Semantics]
steps_k [in ProgrammingTuringMachines.TM.LM.Semantics]
step_fun [in ProgrammingTuringMachines.TM.LM.Semantics]
Step_T [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_steps [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_steps_CaseList [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_steps_CaseList' [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_steps_CaseCom [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_Rel [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_var_T [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_var_steps [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_var_steps_Lookup [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_var [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_var_Rel [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_app_T [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_app_steps [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_app_steps_CaseList [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_app_steps_CaseList' [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_app [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_app_Rel [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_lam_T [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_lam_steps [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_lam_steps_JumpTarget [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_lam [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_lam_Rel [in ProgrammingTuringMachines.TM.LM.StepTM]
Step_Lookup [in ProgrammingTuringMachines.TM.LM.StepTM]
stop [in ProgrammingTuringMachines.TM.Code.CaseList]
stopAfterFirst [in ProgrammingTuringMachines.TM.Code.CasePair]
stopAtStart [in ProgrammingTuringMachines.TM.Code.CasePair]
subrel [in ProgrammingTuringMachines.TM.Relations]
surject [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
surjectConf [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
surjective [in ProgrammingTuringMachines.TM.Relations]
surjectReadSymbols [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
surjectSymbols [in ProgrammingTuringMachines.TM.Code.ChangeAlphabet]
surjectTape [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
surjectTapes [in ProgrammingTuringMachines.TM.Lifting.LiftAlphabet]
Switch [in ProgrammingTuringMachines.TM.Combinators.Switch]
SwitchTM [in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch_p [in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch_halt [in ProgrammingTuringMachines.TM.Combinators.Switch]
Switch_trans [in ProgrammingTuringMachines.TM.Combinators.Switch]
S_Rel [in ProgrammingTuringMachines.TM.Code.CaseNat]


T

TailRec [in ProgrammingTuringMachines.TM.LM.StepTM]
tailRecursion [in ProgrammingTuringMachines.TM.LM.Semantics]
TailRec_T [in ProgrammingTuringMachines.TM.LM.StepTM]
TailRec_steps [in ProgrammingTuringMachines.TM.LM.StepTM]
TailRec_Rel [in ProgrammingTuringMachines.TM.LM.StepTM]
tapes [in ProgrammingTuringMachines.TM.TM]
tapeToList [in ProgrammingTuringMachines.TM.TM]
tape_contains_rev [in ProgrammingTuringMachines.TM.Code.CodeTM]
tape_contains_rev' [in ProgrammingTuringMachines.TM.Code.CodeTM]
tape_contains [in ProgrammingTuringMachines.TM.Code.CodeTM]
tape_contains' [in ProgrammingTuringMachines.TM.Code.CodeTM]
tape_local_l [in ProgrammingTuringMachines.TM.TM]
tape_local [in ProgrammingTuringMachines.TM.TM]
tape_write [in ProgrammingTuringMachines.TM.TM]
tape_move [in ProgrammingTuringMachines.TM.TM]
tape_move_left [in ProgrammingTuringMachines.TM.TM]
tape_move_left' [in ProgrammingTuringMachines.TM.TM]
tape_move_right [in ProgrammingTuringMachines.TM.TM]
tape_move_right' [in ProgrammingTuringMachines.TM.TM]
TerminatesIn [in ProgrammingTuringMachines.TM.TM]
Translate [in ProgrammingTuringMachines.TM.Code.Copy]
translate [in ProgrammingTuringMachines.TM.Code.Copy]
Translate_T [in ProgrammingTuringMachines.TM.Code.Copy]
Translate_steps [in ProgrammingTuringMachines.TM.Code.Copy]
Translate_Rel [in ProgrammingTuringMachines.TM.Code.Copy]
Translate' [in ProgrammingTuringMachines.TM.Code.Copy]
Translate'_steps [in ProgrammingTuringMachines.TM.Code.Copy]
Translate'_Rel [in ProgrammingTuringMachines.TM.Code.Copy]
tRel [in ProgrammingTuringMachines.TM.TM]


V

Var [in ProgrammingTuringMachines.TM.LM.Semantics]


W

While [in ProgrammingTuringMachines.TM.Combinators.While]
WhileTM [in ProgrammingTuringMachines.TM.Combinators.While]
While_Rel' [in ProgrammingTuringMachines.TM.Combinators.While]
While_part [in ProgrammingTuringMachines.TM.Combinators.While]
While_trans [in ProgrammingTuringMachines.TM.Combinators.While]
Write [in ProgrammingTuringMachines.TM.Basic.Mono]
WriteMove [in ProgrammingTuringMachines.TM.Basic.Mono]
WriteMove_Rel [in ProgrammingTuringMachines.TM.Basic.Mono]
WriteString [in ProgrammingTuringMachines.TM.Compound.WriteString]
WriteString_Rel [in ProgrammingTuringMachines.TM.Compound.WriteString]
WriteString_steps [in ProgrammingTuringMachines.TM.Compound.WriteString]
WriteString_sem_fix [in ProgrammingTuringMachines.TM.Compound.WriteString]
WriteString_Fun [in ProgrammingTuringMachines.TM.Compound.WriteString]
WriteValue [in ProgrammingTuringMachines.TM.Code.WriteValue]
WriteValue_steps [in ProgrammingTuringMachines.TM.Code.WriteValue]
WriteValue_Rel [in ProgrammingTuringMachines.TM.Code.WriteValue]
Write_Rel [in ProgrammingTuringMachines.TM.Basic.Mono]



Record Index

C

codable [in ProgrammingTuringMachines.TM.Code.Code]


M

mconfig [in ProgrammingTuringMachines.TM.TM]
mTM [in ProgrammingTuringMachines.TM.TM]



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1667 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (35 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (412 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (41 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (450 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (42 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (15 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (7 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (104 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (50 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (9 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (499 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (3 entries)