(*<*)theory Paperimports UTMbegindeclare [[show_question_marks = false]](*>*)section {* Introduction *}text {*We formalised in earlier work the correctness proofs for two algorithms in Isabelle/HOL, one about type-checking in LF and another about deciding requests in access control \cite{UrbanCheneyBerghofer11} [???]: these formalisations uncovered a gap in the informal correctness proof of the former and made us realise that important details were left out in the informal model for the latter. However, in both cases we were unable to formalise computablility arguments for the algorithms. The reason is that both algorithms are formulatedin terms of inductive predicates. Suppose @{text "P"} stands for one such predicate.Decidability of @{text P} usually amounts to showing whether @{term "P \<or> \<not>P"} holds. But this does not work in Isabelle/HOL,since it is a theorem prover based on classical logic wherethe law of excluded midle ensures that @{term "P \<or> \<not>P"} is always provable. These algorithmswere given as inductively defined predicates. inductively defined predicates, but Norrish choose the $\lambda$-calculus as a starting pointfor his formalisation, because of its ``simplicity'' [Norrish]``Turing machines are an even more daunting prospect'' [Norrish]Our formalisation follows XXX\noindent{\bf Contributions:} *}section {* Wang Tiles *}text {* Used in texture mapings - graphics*}section {* Related Work *}text {* The most closely related work is by Norrish. He bases his approach on lambda-terms. For this he introduced a clever rewriting technology based on combinators and de-Bruijn indices for rewriting modulo $\beta$-equivalence (to keep it manageable)*}(*Questions:Can this be done: Ackerman function is not primitive recursive (Nora Szasz)Tape is represented as two lists (finite - usually infinite tape)?*)(*<*)end(*>*)