chapter ‹Turing machines for reducing $\NP$ languages to \SAT{}\label{s:Red_TM}› theory Reduction_TM imports Sat_TM_CNF Oblivious_2_Tape begin text ‹ At long last we are going to create a polynomial-time Turing machine that, for a fixed language $L\in\NP$, computes for every string $x$ a CNF formula $\Phi$ such that $x\in L$ iff.\ $\Phi$ is satisfiable. This concludes the proof of the Cook-Levin theorem. The CNF formula $\Phi$ is a conjunction of formulas $\Phi_0, \dots, \Phi_9$, and the previous chapter has provided us with Turing machines @{const tm_PHI0}, @{const tm_PHI1}, etc.\ that are supposed to generate these formulas. But only for $\Phi_9$ has this been proven yet. So our first task is to transfer the Turing machines @{const tm_PHI0}, $\dots$, @{const tm_PHI8} into the locale @{locale reduction_sat_x} and show that they really do generate the CNF formulas $\Phi_0, \dots, \Phi_8$. The TMs require certain values on their tapes prior to starting. Therefore we build a Turing machine that computes these values. Then, in a final effort, we combine all these TMs to create this article's biggest Turing machine. › section ‹Turing machines for parts of $\Phi$ revisited› text ‹ In this section we restate the semantic lemmas @{text "transforms_tm_PHI0"} etc.\ of the Turing machines @{const tm_PHI0} etc.\ in the context of the locale @{locale reduction_sat_x}. This means that the lemmas now have terms like @{term "formula_n Φ⇩_{0}"} in them instead of more complicated expressions. It also means that we more clearly see which values the tapes need to contain initially because they are now expressed in terms of values in the locale, such as $n$, $p(n)$, or $m'$. \null › context reduction_sat_x begin lemma tm_PHI0 [transforms_intros]: fixes tps tps' :: "tape list" and j :: tapeidx and ttt k :: nat assumes "length tps = k" and "1 < j" and "j + 8 < k" assumes "tps ! 1 = (⌊[]⌋, 1)" "tps ! j = (⌊m'⌋⇩_{N}, 1)" "tps ! (j + 1) = (⌊H⌋⇩_{N}, 1)" "tps ! (j + 2) = (⌊[]⌋, 1)" "tps ! (j + 3) = (⌊[]⌋, 1)" "tps ! (j + 4) = (⌊[]⌋, 1)" "tps ! (j + 5) = (⌊[]⌋, 1)" "tps ! (j + 6) = (⌊[]⌋, 1)" "tps ! (j + 7) = (⌊[]⌋, 1)" "tps ! (j + 8) = (⌊[]⌋, 1)" assumes "tps' = tps [j := (⌊Suc (Suc m')⌋⇩_{N}, 1), j + 2 := (⌊0⌋⇩_{N}, 1), j + 6 := (⌊nll_Psi (Suc (Suc m') * H) H 0⌋⇩_{N}⇩_{L}⇩_{L}, 1), 1 := nlltape (formula_n Φ⇩_{0})]" assumes "ttt = 5627 * H ^ 4 * (3 + nlength (3 * H + m' * H))⇧^{2}" shows "transforms (tm_PHI0 j) tps ttt tps'" proof - have "nll_Psi (m' * H) H 1 = formula_n (Ψ (ζ⇩_{0}0) 1)" using nll_Psi zeta0_def m' by simp moreover have "nll_Psi (H + m' * H) H 1 = formula_n (Ψ (ζ⇩_{1}0) 1)" using nll_Psi zeta1_def m' by (smt (verit) ab_semigroup_add_class.add_ac(1) add.commute add_cancel_left_right mult_2 mult_zero_left) moreover have "nll_Psi (Suc (Suc m') * H) H 0 = formula_n (Ψ (ζ⇩_{2}0) 0)" proof - have "Suc (Suc m') * H = N + 2 * H" using m' by simp moreover have "Suc (Suc m') * H + H = N + (Suc 0) * Z" using m' Z_def by simp ultimately have "ζ⇩_{2}0 = [Suc (Suc m') * H..<Suc (Suc m') * H + H]" using zeta2_def by (metis Nat.add_0_right mult_zero_left) then show ?thesis using nll_Psi by simp qed ultimately have "nll_Psi (m' * H) H 1 @ nll_Psi (H + m' * H) H 1 @ nll_Psi (Suc (Suc m') * H) H 0 = formula_n Φ⇩_{0}" using formula_n_def PHI0_def by simp then show ?thesis using transforms_tm_PHI0I[OF assms(1-3) H_ge_3 assms(4-13)] assms(14,15) by simp qed lemma tm_PHI1 [transforms_intros]: fixes tps tps' :: "tape list" and j :: tapeidx and ttt k :: nat and nss :: "nat list list" assumes "length tps = k" and "1 < j" and "j + 7 < k" assumes "tps ! 1 = nlltape nss" "tps ! j = (⌊0⌋⇩_{N}, 1)" "tps ! (j + 1) = (⌊H⌋⇩_{N}, 1)" "tps ! (j + 2) = (⌊[]⌋, 1)" "tps ! (j + 3) = (⌊[]⌋, 1)" "tps ! (j + 4) = (⌊[]⌋, 1)" "tps ! (j + 5) = (⌊[]⌋, 1)" "tps ! (j + 6) = (⌊[]⌋, 1)" "tps ! (j + 7) = (⌊[]⌋, 1)" assumes "tps' = tps [j + 2 := (⌊1⌋⇩_{N}, 1), j + 6 := (⌊nll_Psi 0 H 1⌋⇩_{N}⇩_{L}⇩_{L}, 1), 1 := nlltape (nss @ formula_n Φ⇩_{1})]" assumes "ttt = 1875 * H ^ 4" shows "transforms (tm_PHI1 j) tps ttt tps'" proof - have "nll_Psi 0 H 1 = formula_n (Ψ ([0..<H]) 1)" using nll_Psi by simp then have "nll_Psi 0 H 1 = formula_n (Ψ (γ 0) 1)" using gamma_def by simp then have "nll_Psi 0 H 1 = formula_n Φ⇩_{1}" using PHI1_def by simp then show ?thesis using transforms_tm_PHI1I[OF assms(1-3) H_ge_3 assms(4-12)] assms(13,14) by simp qed lemma tm_PHI2 [transforms_intros]: fixes tps tps' :: "tape list" and j :: tapeidx and ttt k :: nat and nss :: "nat list list" assumes "length tps = k" and "1 < j" and "j + 8 < k" assumes "idx = n " assumes "tps ! 1 = nlltape nss" "tps ! j = (⌊idx⌋⇩_{N}, 1)" "tps ! (j + 1) = (⌊H⌋⇩_{N}, 1)" "tps ! (j + 2) = (⌊[]⌋, 1)" "tps ! (j + 3) = (⌊[]⌋, 1)" "tps ! (j + 4) = (⌊[]⌋, 1)" "tps ! (j + 5) = (⌊[]⌋, 1)" "tps ! (j + 6) = (⌊[]⌋, 1)" "tps ! (j + 7) = (⌊[]⌋, 1)" "tps ! (j + 8) = (⌊[]⌋, 1)" assumes "ttt = 3764 * H ^ 4 * (3 + nlength (3 * H + 2 * idx * H))⇧^{2}" assumes "tps' = tps [j := (⌊2 * idx + 2⌋⇩_{N}, 1), j + 2 := (⌊3⌋⇩_{N}, 1), j + 6 := (⌊nll_Psi (Suc (Suc (2 * idx)) * H) H 3⌋⇩_{N}⇩_{L}⇩_{L}, 1), 1 := nlltape (nss @ formula_n Φ⇩_{2})]" shows "transforms (tm_PHI2 j) tps ttt tps'" proof - have "nll_Psi (H + 2 * idx * H) H 3 @ nll_Psi (2 * H + 2 * idx * H) H 3 = formula_n Φ⇩_{2}" proof - have "γ (2 * n + 1) = [H + 2 * idx * H..<H + 2 * idx * H + H]" using assms(4) gamma_def by simp moreover have "γ (2 * n + 2) = [2 * H + 2 * idx * H..<2 * H + 2 * idx * H + H]" using assms(4) gamma_def by simp ultimately show "nll_Psi (H + 2 * idx * H) H 3 @ nll_Psi (2 * H + 2 * idx * H) H 3 = formula_n Φ⇩_{2}" using nll_Psi PHI2_def formula_n_def by simp qed then show ?thesis using transforms_tm_PHI2I[OF assms(1-3) H_ge_3 assms(5-14)] assms(15,16) by simp qed lemma PHI3_correct: "concat (map (λi. nll_Psi (H * (1 + 2 * i)) H 2) [0..<n]) = formula_n Φ⇩_{3}" proof - have "nll_Psi (H * (1 + 2 * i)) H 2 = formula_n (Ψ (γ (2*i+1)) 2)" for i proof - have "γ (2 * i + 1) = [H * (1 + 2 * i)..<H * (1 + 2 * i) + H]" using gamma_def by (simp add: mult.commute) then show ?thesis using nll_Psi by simp qed then have "concat (map (λi. nll_Psi (H * (1 + 2 * i)) H 2) [0..<n]) = concat (map (λi. formula_n (Ψ (γ (2*i+1)) 2)) [0..<n])" by simp also have "... = formula_n (concat (map (λi. Ψ (γ (2*i+1)) 2) [0..<n]))" using concat_formula_n by simp also have "... = formula_n Φ⇩_{3}" using PHI3_def by simp finally show ?thesis . qed lemma tm_PHI3: fixes tps tps' :: "tape list" and j :: tapeidx and ttt k :: nat and nss :: "nat list list" assumes "length tps = k" and "1 < j" and "j + 8 < k" assumes "tps ! 1 = nlltape nss" "tps ! j = (⌊1⌋⇩_{N}, 1)" "tps ! (j + 1) = (⌊H⌋⇩_{N}, 1)" "tps ! (j + 2) = (⌊2⌋⇩_{N}, 1)" "tps ! (j + 3) = (⌊[]⌋, 1)" "tps ! (j + 4) = (⌊[]⌋, 1)" "tps ! (j + 5) = (⌊[]⌋, 1)" "tps ! (j + 6) = (⌊[]⌋, 1)" "tps ! (j + 7) = (⌊[]⌋, 1)" "tps ! (j + 8) = (⌊1 + 2 * n⌋⇩_{N}, 1)" assumes "ttt = Suc n * (9 + 1897 * (H ^ 4 * (nlength (1 + 2 * n))⇧^{2}))" assumes "tps' = tps [j := (⌊1 + 2 * n⌋⇩_{N}, 1), 1 := nlltape (nss @ formula_n Φ⇩_{3}), j + 3 := (⌊1⌋⇩_{N}, 1)]" shows "transforms (tm_PHI345 2 j) tps ttt tps'" using transforms_tm_PHI345I[OF assms(1,2,3) H_ge_3, of 2 2 nss 1 "n "] H_gr_2 assms PHI3_correct by fastforce lemma PHI4_correct: assumes "idx = 2 * n + 2 + 1" and "kappa = 2" and "step = 2" and "numiter = p n" shows "concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<numiter]) = formula_n Φ⇩_{4}" proof - have "nll_Psi (H * (idx + step * i)) H kappa = formula_n (Ψ (γ (2 * n + 2 + 2 * i + 1)) 2)" for i proof - have "γ (2 * n + 2 + 2 * i + 1) = [H * (idx + step * i)..<H * (idx + step * i) + H]" using assms gamma_def by (simp add: add.commute mult.commute) then show ?thesis using nll_Psi assms by simp qed then have "concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<numiter]) = concat (map (λi. formula_n (Ψ (γ (2 * n + 2 + 2 * i + 1)) 2)) [0..<numiter])" by simp also have "... = formula_n (concat (map (λi. Ψ (γ (2 * n + 2 + 2 * i + 1)) 2) [0..<p n]))" using assms concat_formula_n by simp also have "... = formula_n Φ⇩_{4}" using PHI4_def by simp finally show ?thesis . qed lemma tm_PHI4: fixes tps tps' :: "tape list" and j :: tapeidx and ttt step k :: nat and nss :: "nat list list" assumes "length tps = k" and "1 < j" and "j + 8 < k" assumes "tps ! 1 = nlltape nss" "tps ! j = (⌊2 * n + 2 + 1⌋⇩_{N}, 1)" "tps ! (j + 1) = (⌊H⌋⇩_{N}, 1)" "tps ! (j + 2) = (⌊2⌋⇩_{N}, 1)" "tps ! (j + 3) = (⌊[]⌋, 1)" "tps ! (j + 4) = (⌊[]⌋, 1)" "tps ! (j + 5) = (⌊[]⌋, 1)" "tps ! (j + 6) = (⌊[]⌋, 1)" "tps ! (j + 7) = (⌊[]⌋, 1)" "tps ! (j + 8) = (⌊2 * n + 2 + 1 + 2 * p n⌋⇩_{N}, 1)" assumes "ttt = Suc (p n) * (9 + 1897 * (H ^ 4 * (nlength (2 * n + 2 + 1 + 2 * p n))⇧^{2}))" assumes "tps' = tps [j := (⌊2 * n + 2 + 1 + 2 * p n⌋⇩_{N}, 1), 1 := nlltape (nss @ formula_n Φ⇩_{4}), j + 3 := (⌊1⌋⇩_{N}, 1)]" shows "transforms (tm_PHI345 2 j) tps ttt tps'" using transforms_tm_PHI345I[OF assms(1,2,3) H_ge_3, of 2 2 nss "2 * n + 2 + 1" "p n"] H_gr_2 assms PHI4_correct by fastforce lemma PHI5_correct: assumes "idx = 2 * n + 2 * p n + 3" and "kappa = 0" and "step = 1" and "numiter = T' " shows "concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<numiter]) = formula_n Φ⇩_{5}" proof - have "nll_Psi (H * (idx + step * i)) H kappa = formula_n (Ψ (γ (2 * n + 2 * p n + 3 + i)) 0)" for i proof - have "γ (2 * n + 2 * p n + 3 + i) = [H * (idx + step * i)..<H * (idx + step * i) + H]" using assms gamma_def by (simp add: add.commute mult.commute) then show ?thesis using nll_Psi assms by simp qed then have "concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<numiter]) = concat (map (λi. formula_n (Ψ (γ (2 * n + 2 * p n + 3 + i)) 0)) [0..<numiter])" by simp also have "... = formula_n (concat (map (λi. Ψ (γ (2 * n + 2 * p n + 3 + i)) 0) [0..<T']))" using assms concat_formula_n by simp also have "... = formula_n Φ⇩_{5}" using PHI5_def by simp finally show ?thesis . qed lemma tm_PHI5: fixes tps tps' :: "tape list" and j :: tapeidx and ttt k :: nat and nss :: "nat list list" assumes "length tps = k" and "1 < j" and "j + 8 < k" assumes "tps ! 1 = nlltape nss" "tps ! j = (⌊2 * n + 2 * p n + 3⌋⇩_{N}, 1)" "tps ! (j + 1) = (⌊H⌋⇩_{N}, 1)" "tps ! (j + 2) = (⌊0⌋⇩_{N}, 1)" "tps ! (j + 3) = (⌊[]⌋, 1)" "tps ! (j + 4) = (⌊[]⌋, 1)" "tps ! (j + 5) = (⌊[]⌋, 1)" "tps ! (j + 6) = (⌊[]⌋, 1)" "tps ! (j + 7) = (⌊[]⌋, 1)" "tps ! (j + 8) = (⌊2 * n + 2 * p n + 3 + T'⌋⇩_{N}, 1)" assumes "ttt = Suc T' * (9 + 1891 * (H ^ 4 * (nlength (2 * n + 2 * p n + 3 + T'))⇧^{2}))" assumes "tps' = tps [j := (⌊2 * n + 2 * p n + 3 + T'⌋⇩_{N}, 1), 1 := nlltape (nss @ formula_n Φ⇩_{5}), j + 3 := (⌊1⌋⇩_{N}, 1)]" shows "transforms (tm_PHI345 1 j) tps ttt tps'" using transforms_tm_PHI345I[OF assms(1,2,3) H_ge_3, of 0 1, OF _ _ assms(4-12)] H_gr_2 assms(13-) PHI5_correct by fastforce lemma PHI6_correct: "concat (map (λi. nll_Psi (H * (2 + 2 * i)) H (xs ! i)) [0..<length xs]) = formula_n Φ⇩_{6}" proof - have "nll_Psi (H * (2 + 2 * i)) H (xs ! i) = formula_n (Ψ (γ (2 * i + 2)) (if x ! i then 3 else 2))" if "i < length xs" for i proof - have "γ (2 * i + 2) = [H * (2 + 2 * i)..<H * (2 + 2* i) + H]" using gamma_def by (simp add: mult.commute) then have "nll_Psi (H * (2 + 2 * i)) H (xs ! i) = formula_n (Ψ (γ (2 * i + 2)) (xs ! i))" using nll_Psi by simp moreover have "xs ! i = (if x ! i then 3 else 2)" using that by simp ultimately show ?thesis by simp qed then have "map (λi. nll_Psi (H * (2 + 2 * i)) H (xs ! i)) [0..<length xs] = map (λi. formula_n (Ψ (γ (2 * i + 2)) (if x ! i then 3 else 2))) [0..<length xs]" by simp then have "concat (map (λi. nll_Psi (H * (2 + 2 * i)) H (xs ! i)) [0..<length xs]) = concat (map (λi. formula_n (Ψ (γ (2 * i + 2)) (if x ! i then 3 else 2))) [0..<length xs])" by metis also have "... = formula_n (concat (map (λi. Ψ (γ (2 * i + 2)) (if x ! i then 3 else 2)) [0..<length xs]))" using concat_formula_n by simp also have "... = formula_n (concat (map (λi. Ψ (γ (2 * i + 2)) (if x ! i then 3 else 2)) [0..<n]))" by simp also have "... = formula_n Φ⇩_{6}" using PHI6_def by simp finally show ?thesis . qed lemma tm_PHI6 [transforms_intros]: fixes tps tps' :: "tape list" and j :: tapeidx and ttt k :: nat and nss :: "nat list list" assumes "length tps = k" and "1 < j" and "j + 7 < k" assumes "tps ! 1 = nlltape nss" "tps ! 0 = (⌊xs⌋, 1)" "tps ! j = (⌊2⌋⇩_{N}, 1)" "tps ! (j + 1) = (⌊H⌋⇩_{N}, 1)" "tps ! (j + 2) = (⌊0⌋⇩_{N}, 1)" "tps ! (j + 3) = (⌊[]⌋, 1)" "tps ! (j + 4) = (⌊[]⌋, 1)" "tps ! (j + 5) = (⌊[]⌋, 1)" "tps ! (j + 6) = (⌊[]⌋, 1)" "tps ! (j + 7) = (⌊[]⌋, 1)" assumes "tps' = tps [0 := (⌊xs⌋, Suc n), j := (⌊2 + 2 * n⌋⇩_{N}, 1), 1 := nlltape (nss @ formula_n Φ⇩_{6})]" assumes "ttt = 133650 * H ^ 6 * n ^ 3 + 1" shows "transforms (tm_PHI6 j) tps ttt tps'" using transforms_tm_PHI6I[OF assms(1,2,3) H_ge_3 bs_xs assms(4-13) _] assms(14,15) PHI6_correct by simp lemma PHI7_correct: assumes "idx = 2 * n + 4" and "numiter = p n" shows "concat (map (λi. nll_Upsilon (idx + 2 * i) H) [0..<numiter]) = formula_n Φ⇩_{7}" proof - have "nll_Upsilon (idx + 2 * i) H = formula_n (Υ (γ (2*n + 4 + 2 * i)))" for i proof - have "nll_Upsilon (idx + 2 * i) H = formula_n (Υ [(idx + 2 * i)*H..<(idx + 2 * i)*H+H])" using nll_Upsilon[OF H_ge_3] by simp also have "... = formula_n (Υ (γ (2 * n + 4 + 2 * i)))" using gamma_def assms(1) by (simp add: add.commute) finally show ?thesis . qed then have "concat (map (λi. nll_Upsilon (idx + 2 * i) H) [0..<numiter]) = concat (map (λi. formula_n (Υ (γ (2*n + 4 + 2 * i)))) [0..<numiter])" by simp also have "... = formula_n (concat (map (λi. Υ (γ (2*n + 4 + 2 * i))) [0..<numiter]))" using concat_formula_n by simp also have "... = formula_n (concat (map (λi. Υ (γ (2*n + 4 + 2 * i))) [0..<p n]))" using assms(2) by simp also have "... = formula_n Φ⇩_{7}" using PHI7_def by simp finally show ?thesis . qed lemma tm_PHI7 [transforms_intros]: fixes tps tps' :: "tape list" and j :: tapeidx and ttt numiter k idx :: nat and nss :: "nat list list" assumes "length tps = k" and "1 < j" and "j + 6 < k" assumes "tps ! 1 = nlltape nss" "tps ! j = (⌊2 * n + 4⌋⇩_{N}, 1)" "tps ! (j + 1) = (⌊H⌋⇩_{N}, 1)" "tps ! (j + 2) = (⌊[]⌋, 1)" "tps ! (j + 3) = (⌊[]⌋, 1)" "tps ! (j + 4) = (⌊[]⌋, 1)" "tps ! (j + 5) = (⌊[]⌋, 1)" "tps ! (j + 6) = (⌊p n⌋⇩_{N}, 1)" assumes "ttt = p n * 257 * H * (nlength (2 * n + 4 + 2 * p n) + nlength H)⇧^{2}+ 1" assumes "tps' = tps [j := (⌊2 * n + 4 + 2 * p n⌋⇩_{N}, 1), j + 6 := (⌊0⌋⇩_{N}, 1), 1 := nlltape (nss @ formula_n Φ⇩_{7})]" shows "transforms (tm_PHI7 j) tps ttt tps'" using transforms_tm_PHI7I[OF assms(1,2,3) H_ge_3 assms(4-12)] assms(13) PHI7_correct by simp lemma tm_PHI8 [transforms_intros]: fixes tps tps' :: "tape list" and j :: tapeidx and ttt k idx :: nat and nss :: "nat list list" assumes "length tps = k" and "1 < j" and "j + 7 < k" assumes "idx = 1 + 3 * T' + m' " assumes "tps ! 1 = nlltape nss" "tps ! j = (⌊1 + 3 * T' + m'⌋⇩_{N}, 1)" "tps ! (j + 1) = (⌊H⌋⇩_{N}, 1)" "tps ! (j + 2) = (⌊[]⌋, 1)" "tps ! (j + 3) = (⌊[]⌋, 1)" "tps ! (j + 4) = (⌊[]⌋, 1)" "tps ! (j + 5) = (⌊[]⌋, 1)" "tps ! (j + 6) = (⌊[]⌋, 1)" "tps ! (j + 7) = (⌊[]⌋, 1)" assumes "tps' = tps [1 := nlltape (nss @ formula_n Φ⇩_{8}), j + 2 := (⌊3⌋⇩_{N}, 1), j + 6 := (⌊formula_n Φ⇩_{8}⌋⇩_{N}⇩_{L}⇩_{L}, 1)]" assumes "ttt = 18 + 1861 * H ^ 4 * (nlength (Suc (1 + 3 * T' + m')))⇧^{2}" shows "transforms (tm_PHI8 j) tps ttt tps'" proof - let ?idx = "1 + 3 * T' + m' " have "m' * H + T' * 3 * H + H = ?idx * H" using m' add_mult_distrib by simp then have "ζ⇩_{1}T' = [?idx * H..<?idx * H + H]" using zeta1_def Z_def m' by (metis ab_semigroup_add_class.add_ac(1) mult.assoc mult_2) then have "nll_Psi (?idx * H) H 3 = formula_n Φ⇩_{8}" using PHI8_def nll_Psi by simp then show ?thesis using transforms_tm_PHI8I[OF assms(1-3) H_ge_3 assms(5-13) _ assms(15)] assms(14) by simp qed end (* context reduction_sat_x *) section ‹A Turing machine for initialization› text ‹ As we have seen in the previous section, the Turing machines @{const tm_PHI0} etc.\ expect some tapes to contain certain values that depend on the verifier TM $M$. In this section we construct the TM @{term tm_PHI_init} that computes theses values. The TM expects the string $x$ on the input tape. Then it determines the length $n$ of $x$ and stores it on tape~11. Then it computes the value $p(n)$ and stores it on tape~15. Then it computes $m = 2n + 2p(n) + 2$ and stores it on tape~16. It then writes $\mathbf{0}^m$ to tape~9 and runs @{const tm_list_headpos}, which writes the sequences of head positions for the input and work/output tape of the verifier TM $M$ to tapes~4 and~7, respectively. The length of these lists determines $T'$, which is written to tape~17. From this and $m$ the TM computes $m'$ and writes it to tape~18. It then writes $H$, which is hard-coded, to tape~19 and finally $N = H\cdot m'$ to tape~20. We assume that the TM starts in a configuration where the input tape head and the heads on tapes with index greater than 10 are positioned on cell number~1, whereas all other tapes are on cell number~0 as usual. The TM has no tape parameters, as all tapes are fixed to work with the final TM later. As with other TMs before, we will define and analyze the TM on the theory level and then transfer the semantics to the locale @{locale reduction_sat_x}. › definition tm_PHI_init :: "nat ⇒ machine ⇒ (nat ⇒ nat) ⇒ machine" where "tm_PHI_init G M p ≡ tm_right 9 ;; tm_length_input 11 ;; tm_polynomial p 11 ;; tm_copyn 15 16 ;; tm_add 11 16 ;; tm_incr 16 ;; tm_times2 16 ;; tm_copyn 16 17 ;; tm_write_replicate 2 17 9 ;; tm_left 9 ;; tm_list_headpos G M 2 ;; tm_count 4 17 4 ;; tm_decr 17 ;; tm_copyn 16 18 ;; tm_incr 18 ;; tm_add 17 18 ;; tm_setn 19 (max G (length M)) ;; tm_mult 18 19 20" lemma tm_PHI_init_tm: fixes H k assumes "turing_machine 2 G M" and "k > 20" and "H ≥ Suc (length M)" and "H ≥ G" assumes "H ≥ 5" shows "turing_machine k H (tm_PHI_init G M p)" unfolding tm_PHI_init_def using assms turing_machine_sequential_turing_machine tm_right_tm tm_length_input_tm tm_polynomial_tm tm_copyn_tm tm_add_tm tm_incr_tm tm_times2_tm tm_write_replicate_tm tm_left_tm tm_list_headpos_tm tm_count_tm tm_decr_tm tm_setn_tm tm_mult_tm by simp locale turing_machine_PHI_init = fixes G :: nat and M :: machine and p :: "nat ⇒ nat" begin definition "tm3 ≡ tm_right 9" definition "tm4 ≡ tm3 ;; tm_length_input 11" definition "tm5 ≡ tm4 ;; tm_polynomial p 11" definition "tm6 ≡ tm5 ;; tm_copyn 15 16" definition "tm7 ≡ tm6 ;; tm_add 11 16" definition "tm8 ≡ tm7 ;; tm_incr 16" definition "tm9 ≡ tm8 ;; tm_times2 16" definition "tm10 ≡ tm9 ;; tm_copyn 16 17" definition "tm11 ≡ tm10 ;; tm_write_replicate 2 17 9" definition "tm12 ≡ tm11 ;; tm_left 9" definition "tm13 ≡ tm12 ;; tm_list_headpos G M 2" definition "tm14 ≡ tm13 ;; tm_count 4 17 4" definition "tm15 ≡ tm14 ;; tm_decr 17" definition "tm16 ≡ tm15 ;; tm_copyn 16 18" definition "tm17 ≡ tm16 ;; tm_incr 18" definition "tm18 ≡ tm17 ;; tm_add 17 18" definition "tm19 ≡ tm18 ;; tm_setn 19 (max G (length M))" definition "tm20 ≡ tm19 ;; tm_mult 18 19 20" lemma tm20_eq_tm_PHI_init: "tm20 = tm_PHI_init G M p" unfolding tm20_def tm19_def tm18_def tm17_def tm16_def tm15_def tm14_def tm13_def tm12_def tm11_def unfolding tm10_def tm9_def tm8_def tm7_def tm6_def tm5_def tm4_def tm3_def tm_PHI_init_def by simp context fixes k H thalt :: nat and tps0 :: "tape list" and xs zs :: "symbol list" assumes poly_p: "polynomial p" and M_tm: "turing_machine 2 G M" and k: "k = length tps0" "20 < k" and H: "H = max G (length M)" and xs: "bit_symbols xs" and zs: "zs = 2 # 2 # replicate (2 * length xs + 2 * p (length xs)) 2" assumes thalt: "∀t<thalt. fst (execute M (start_config 2 zs) t) < length M" "fst (execute M (start_config 2 zs) thalt) = length M" assumes tps0: "tps0 ! 0 = (⌊xs⌋, 1)" "⋀i. 0 < i ⟹ i ≤ 10 ⟹ tps0 ! i = (⌊[]⌋, 0)" "⋀i. 10 < i ⟹ i < k ⟹ tps0 ! i = (⌊[]⌋, 1)" begin lemma G: "G ≥ 4" using M_tm turing_machine_def by simp lemma H: "H ≥ length M" "H ≥ G" using H by simp_all definition "tps3 ≡ tps0 [9 := (⌊[]⌋, 1)]" lemma tm3 [transforms_intros]: "transforms tm3 tps0 1 tps3" unfolding tm3_def by (tform tps: tps3_def tps0 k) abbreviation "n ≡ length xs" definition "tps4 ≡ tps0 [9 := (⌊[]⌋, 1), 11 := (⌊n⌋⇩_{N}, 1)]" lemma tm4 [transforms_intros]: assumes "ttt = 5 + 11 * (length xs)⇧^{2}" shows "transforms tm4 tps0 ttt tps4" unfolding tm4_def proof (tform tps: tps3_def tps4_def tps0 k time: assms) show "proper_symbols xs" using xs by auto show "tps3 ! 11 = (⌊0⌋⇩_{N}, 1)" using canrepr_0 tps3_def tps0 k by simp qed definition "tps5 ≡ tps0 [9 := (⌊[]⌋, 1), 11 := (⌊n⌋⇩_{N}, 1), 15 := (⌊p n⌋⇩_{N}, 1)]" lemma tm5 [transforms_intros]: assumes "ttt = 5 + 11 * (length xs)⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength (length xs))⇧^{2})" shows "transforms tm5 tps0 ttt tps5" unfolding tm5_def by (tform tps: canrepr_0 tps4_def tps5_def tps0 k poly_p time: assms) definition "tps6 ≡ tps0 [9 := (⌊[]⌋, 1), 11 := (⌊n⌋⇩_{N}, 1), 15 := (⌊p n⌋⇩_{N}, 1), 16 := (⌊p n⌋⇩_{N}, 1)]" lemma tm6 [transforms_intros]: assumes "ttt = 19 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n)" shows "transforms tm6 tps0 ttt tps6" unfolding tm6_def proof (tform tps: tps5_def tps6_def tps0 k) show "tps5 ! 16 = (⌊0⌋⇩_{N}, 1)" using canrepr_0 k tps0 tps5_def by simp show "ttt = 5 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + (14 + 3 * (nlength (p n) + nlength 0))" using assms by simp qed definition "tps7 ≡ tps0 [9 := (⌊[]⌋, 1), 11 := (⌊n⌋⇩_{N}, 1), 15 := (⌊p n⌋⇩_{N}, 1), 16 := (⌊n + p n⌋⇩_{N}, 1)]" lemma tm7 [transforms_intros]: assumes "ttt = 29 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n))" shows "transforms tm7 tps0 ttt tps7" unfolding tm7_def by (tform tps: tps6_def tps7_def tps0 k assms) definition "tps8 ≡ tps0 [9 := (⌊[]⌋, 1), 11 := (⌊n⌋⇩_{N}, 1), 15 := (⌊p n⌋⇩_{N}, 1), 16 := (⌊Suc (n + p n)⌋⇩_{N}, 1)]" lemma tm8 [transforms_intros]: assumes "ttt = 34 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n)" shows "transforms tm8 tps0 ttt tps8" unfolding tm8_def by (tform tps: tps7_def tps8_def tps0 k assms) definition "tps9 ≡ tps0 [9 := (⌊[]⌋, 1), 11 := (⌊n⌋⇩_{N}, 1), 15 := (⌊p n⌋⇩_{N}, 1), 16 := (⌊2 * Suc (n + p n)⌋⇩_{N}, 1)]" lemma tm9 [transforms_intros]: assumes "ttt = 39 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) + 2 * nlength (Suc (n + p n))" shows "transforms tm9 tps0 ttt tps9" unfolding tm9_def by (tform tps: tps8_def tps9_def tps0 k assms) definition "tps10 ≡ tps0 [9 := (⌊[]⌋, 1), 11 := (⌊n⌋⇩_{N}, 1), 15 := (⌊p n⌋⇩_{N}, 1), 16 := (⌊2 * Suc (n + p n)⌋⇩_{N}, 1), 17 := (⌊2 * Suc (n + p n)⌋⇩_{N}, 1)]" lemma tm10 [transforms_intros]: assumes "ttt = 53 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) + 2 * nlength (Suc (n + p n)) + 3 * nlength (Suc (Suc (2 * n + 2 * p n)))" shows "transforms tm10 tps0 ttt tps10" unfolding tm10_def proof (tform tps: tps9_def tps10_def tps0 k) show "tps9 ! 17 = (⌊0⌋⇩_{N}, 1)" using tps9_def canrepr_0 tps0 k by simp show "ttt = 39 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) + 2 * nlength (Suc (n + p n)) + (14 + 3 * (nlength (Suc (Suc (2 * n + 2 * p n))) + nlength 0))" using assms by simp qed definition "tps11 ≡ tps0 [9 := (⌊zs⌋, 1), 11 := (⌊n⌋⇩_{N}, 1), 15 := (⌊p n⌋⇩_{N}, 1), 16 := (⌊2 * Suc (n + p n)⌋⇩_{N}, 1), 17 := (⌊0⌋⇩_{N}, 1)]" lemma tm11 [transforms_intros]: assumes "ttt = 57 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) + 2 * nlength (Suc (n + p n)) + 3 * nlength (Suc (Suc (2 * n + 2 * p n))) + Suc (Suc (2 * n + 2 * p n)) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n))))" shows "transforms tm11 tps0 ttt tps11" unfolding tm11_def proof (tform tps: tps10_def tps11_def tps0 k time: assms) show "tps11 = tps10 [17 := (⌊0⌋⇩_{N}, 1), 9 := (⌊replicate (Suc (Suc (2 * n + 2 * p n))) 2⌋, 1)]" unfolding tps11_def tps10_def using zs by (simp add: list_update_swap[of _ 9]) qed definition "tps12 ≡ tps0 [9 := (⌊zs⌋, 0), 11 := (⌊n⌋⇩_{N}, 1), 15 := (⌊p n⌋⇩_{N}, 1), 16 := (⌊2 * Suc (n + p n)⌋⇩_{N}, 1), 17 := (⌊0⌋⇩_{N}, 1)]" lemma tm12 [transforms_intros]: assumes "ttt = 82 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) + 2 * nlength (Suc (n + p n)) + 7 * nlength (Suc (Suc (2 * n + 2 * p n))) + (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n))))" shows "transforms tm12 tps0 ttt tps12" unfolding tm12_def proof (tform tps: tps11_def tps12_def tps0 k time: assms) have "tps11 ! 9 |-| 1 = (⌊zs⌋, 0)" using tps11_def k by simp then show "tps12 = tps11[9 := tps11 ! 9 |-| 1]" unfolding tps12_def tps11_def by (simp add: list_update_swap[of _ 9]) qed abbreviation exc :: "nat ⇒ config" where "exc t ≡ execute M (start_config 2 zs) t" definition "tps13 ≡ tps0 [9 := exc thalt <!> 0, 11 := (⌊n⌋⇩_{N}, 1), 15 := (⌊p n⌋⇩_{N}, 1), 16 := (⌊2 * Suc (n + p n)⌋⇩_{N}, 1), 17 := (⌊0⌋⇩_{N}, 1), 3 := (⌊exc thalt <#> 0⌋⇩_{N}, 1), 4 := (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1), 6 := (⌊exc thalt <#> 1⌋⇩_{N}, 1), 7 := (⌊map (λt. exc t <#> 1) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1), 10 := exc thalt <!> 1]" lemma tm13 [transforms_intros]: assumes "ttt = 82 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) + 2 * nlength (Suc (n + p n)) + 7 * nlength (Suc (Suc (2 * n + 2 * p n))) + (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) + (27 + 27 * thalt) * (9 + 2 * nlength thalt)" shows "transforms tm13 tps0 ttt tps13" unfolding tm13_def proof (tform) show "turing_machine 2 G M" using M_tm . show "2 + 9 ≤ length tps12" using tps12_def k by simp show "∀t<thalt. fst (execute M (start_config 2 zs) t) < length M" "fst (execute M (start_config 2 zs) thalt) = length M" using thalt . show "symbols_lt G zs" proof - have "zs = replicate (2 * n + 2 * p n + 2) 2" using zs by simp then have "∀i<length zs. zs ! i = 2" using nth_replicate by (metis length_replicate) then show ?thesis using G by simp qed show "tps13 = tps12 [2 + 1 := (⌊snd (exc thalt) :#: 0⌋⇩_{N}, 1), 2 + 2 := (⌊map (λt. snd (exc t) :#: 0) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1), 2 + 4 := (⌊snd (exc thalt) :#: 1⌋⇩_{N}, 1), 2 + 5 := (⌊map (λt. snd (exc t) :#: 1) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1), 2 + 7 := exc thalt <!> 0, 2 + 8 := exc thalt <!> 1]" unfolding tps13_def tps12_def by (simp add: list_update_swap[of _ 9]) show "tps12 ! 2 = ⌈▹⌉" using tps12_def tps0 onesie_1 by simp show "tps12 ! (2 + 1) = (⌊0⌋⇩_{N}, 0)" using tps12_def tps0 canrepr_0 by simp show "tps12 ! (2 + 2) = (⌊[]⌋⇩_{N}⇩_{L}, 0)" using tps12_def tps0 nlcontents_Nil by simp show "tps12 ! (2 + 3) = ⌈▹⌉" using tps12_def tps0 onesie_1 by simp show "tps12 ! (2 + 4) = (⌊0⌋⇩_{N}, 0)" using tps12_def tps0 canrepr_0 by simp show "tps12 ! (2 + 5) = (⌊[]⌋⇩_{N}⇩_{L}, 0)" using tps12_def tps0 nlcontents_Nil by simp show "tps12 ! (2 + 6) = ⌈▹⌉" using tps12_def tps0 onesie_1 by simp show "tps12 ! (2 + 7) = (⌊zs⌋, 0)" using tps12_def k tps0 by simp show "tps12 ! (2 + 8) = (⌊[]⌋, 0)" using tps12_def tps0 by simp show "ttt = 82 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) + 2 * nlength (Suc (n + p n)) + 7 * nlength (Suc (Suc (2 * n + 2 * p n))) + (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) + 27 * Suc thalt * (9 + 2 * nlength thalt)" using assms by simp qed definition "tpsA ≡ tps0 [9 := exc thalt <!> 0, 3 := (⌊exc thalt <#> 0⌋⇩_{N}, 1), 6 := (⌊exc thalt <#> 1⌋⇩_{N}, 1), 10 := exc thalt <!> 1]" definition "tps14 ≡ tps0 [9 := exc thalt <!> 0, 11 := (⌊n⌋⇩_{N}, 1), 15 := (⌊p n⌋⇩_{N}, 1), 16 := (⌊2 * Suc (n + p n)⌋⇩_{N}, 1), 17 := (⌊Suc thalt⌋⇩_{N}, 1), 3 := (⌊exc thalt <#> 0⌋⇩_{N}, 1), 4 := (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1), 6 := (⌊exc thalt <#> 1⌋⇩_{N}, 1), 7 := (⌊map (λt. exc t <#> 1) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1), 10 := exc thalt <!> 1]" lemma tm14: assumes "ttt = 87 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) + 2 * nlength (Suc (n + p n)) + 7 * nlength (Suc (Suc (2 * n + 2 * p n))) + (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) + (27 + 27 * thalt) * (9 + 2 * nlength thalt) + 14 * (nllength (map (λt. exc t <#> 0) [0..<thalt] @ [exc thalt <#> 0]))⇧^{2}" shows "transforms tm14 tps0 ttt tps14" unfolding tm14_def proof (tform) show "4 < length tps13" "17 < length tps13" using tps13_def k by (simp_all only: length_list_update) show "tps13 ! 4 = (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1)" using tps13_def k by (simp only: length_list_update nth_list_update_neq nth_list_update_eq) show "tps13 ! 17 = (⌊0⌋⇩_{N}, 1)" using tps13_def k by (simp only: length_list_update nth_list_update_neq nth_list_update_eq) show "tps14 = tps13 [17 := (⌊length (map (λt. snd (exc t) :#: 0) [0..<Suc thalt])⌋⇩_{N}, 1)]" unfolding tps14_def tps13_def by (simp add: list_update_swap[of 17]) show "ttt = 82 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) + 2 * nlength (Suc (n + p n)) + 7 * nlength (Suc (Suc (2 * n + 2 * p n))) + (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) + (27 + 27 * thalt) * (9 + 2 * nlength thalt) + (14 * (nllength (map (λt. snd (exc t) :#: 0) [0..<Suc thalt]))⇧^{2}+ 5)" using assms by simp qed definition "tps14' ≡ tpsA [11 := (⌊n⌋⇩_{N}, 1), 15 := (⌊p n⌋⇩_{N}, 1), 16 := (⌊2 * Suc (n + p n)⌋⇩_{N}, 1), 17 := (⌊Suc thalt⌋⇩_{N}, 1), 4 := (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1), 7 := (⌊map (λt. exc t <#> 1) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1)]" lemma tps14': "tps14' = tps14" unfolding tps14'_def tps14_def tpsA_def by (simp add: list_update_swap) lemma len_tpsA: "length tpsA = k" using tpsA_def k by simp lemma tm14' [transforms_intros]: assumes "ttt = 87 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) + 2 * nlength (Suc (n + p n)) + 7 * nlength (Suc (Suc (2 * n + 2 * p n))) + (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) + (27 + 27 * thalt) * (9 + 2 * nlength thalt) + 14 * (nllength (map (λt. exc t <#> 0) [0..<thalt] @ [exc thalt <#> 0]))⇧^{2}" shows "transforms tm14 tps0 ttt tps14'" using tm14 tps14' assms by simp definition "tps15 ≡ tpsA [11 := (⌊n⌋⇩_{N}, 1), 15 := (⌊p n⌋⇩_{N}, 1), 16 := (⌊2 * Suc (n + p n)⌋⇩_{N}, 1), 17 := (⌊thalt⌋⇩_{N}, 1), 4 := (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1), 7 := (⌊map (λt. exc t <#> 1) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1)]" lemma tm15 [transforms_intros]: assumes "ttt = 95 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) + 2 * nlength (Suc (n + p n)) + 7 * nlength (Suc (Suc (2 * n + 2 * p n))) + (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) + (27 + 27 * thalt) * (9 + 2 * nlength thalt) + 14 * (nllength (map (λt. exc t <#> 0) [0..<thalt] @ [exc thalt <#> 0]))⇧^{2}+ 2 * nlength (Suc thalt)" shows "transforms tm15 tps0 ttt tps15" unfolding tm15_def proof (tform tps: tps14'_def len_tpsA k time: assms) show "tps15 = tps14'[17 := (⌊Suc thalt - 1⌋⇩_{N}, 1)]" unfolding tps15_def tps14'_def by (simp add: list_update_swap) qed definition "tps16 ≡ tpsA [11 := (⌊n⌋⇩_{N}, 1), 15 := (⌊p n⌋⇩_{N}, 1), 16 := (⌊2 * Suc (n + p n)⌋⇩_{N}, 1), 17 := (⌊thalt⌋⇩_{N}, 1), 4 := (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1), 7 := (⌊map (λt. exc t <#> 1) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1), 18 := (⌊2 * Suc (n + p n)⌋⇩_{N}, 1)]" lemma tm16 [transforms_intros]: assumes "ttt = 109 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) + 2 * nlength (Suc (n + p n)) + 10 * nlength (Suc (Suc (2 * n + 2 * p n))) + (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) + (27 + 27 * thalt) * (9 + 2 * nlength thalt) + 14 * (nllength (map (λt. exc t <#> 0) [0..<thalt] @ [exc thalt <#> 0]))⇧^{2}+ 2 * nlength (Suc thalt)" shows "transforms tm16 tps0 ttt tps16" unfolding tm16_def proof (tform tps: tps15_def tps16_def k len_tpsA) have "tps15 ! 18 = tpsA ! 18" using tps15_def by simp also have "... = tps0 ! 18" using tpsA_def by simp also have "... = (⌊0⌋⇩_{N}, 1)" using tps0 canrepr_0 k by simp finally show "tps15 ! 18 = (⌊0⌋⇩_{N}, 1)" . show "ttt = 95 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) + 2 * nlength (Suc (n + p n)) + 7 * nlength (Suc (Suc (2 * n + 2 * p n))) + (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) + (27 + 27 * thalt) * (9 + 2 * nlength thalt) + 14 * (nllength (map (λt. snd (exc t) :#: 0) [0..<thalt] @ [snd (exc thalt) :#: 0]))⇧^{2}+ 2 * nlength (Suc thalt) + (14 + 3 * (nlength (Suc (Suc (2 * n + 2 * p n))) + nlength 0))" using assms by simp qed definition "tps17 ≡ tpsA [11 := (⌊n⌋⇩_{N}, 1), 15 := (⌊p n⌋⇩_{N}, 1), 16 := (⌊2 * Suc (n + p n)⌋⇩_{N}, 1), 17 := (⌊thalt⌋⇩_{N}, 1), 4 := (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1), 7 := (⌊map (λt. exc t <#> 1) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1), 18 := (⌊Suc (2 * Suc (n + p n))⌋⇩_{N}, 1)]" lemma tm17 [transforms_intros]: assumes "ttt = 114 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) + 2 * nlength (Suc (n + p n)) + 10 * nlength (Suc (Suc (2 * n + 2 * p n))) + (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) + (27 + 27 * thalt) * (9 + 2 * nlength thalt) + 14 * (nllength (map (λt. exc t <#> 0) [0..<thalt] @ [exc thalt <#> 0]))⇧^{2}+ 2 * nlength (Suc thalt) + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))" shows "transforms tm17 tps0 ttt tps17" unfolding tm17_def by (tform tps: tps16_def tps17_def k len_tpsA time: assms) definition "tps18 ≡ tpsA [11 := (⌊n⌋⇩_{N}, 1), 15 := (⌊p n⌋⇩_{N}, 1), 16 := (⌊2 * Suc (n + p n)⌋⇩_{N}, 1), 17 := (⌊thalt⌋⇩_{N}, 1), 4 := (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1), 7 := (⌊map (λt. exc t <#> 1) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1), 18 := (⌊thalt + Suc (2 * Suc (n + p n))⌋⇩_{N}, 1)]" lemma tm18 [transforms_intros]: assumes "ttt = 124 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) + 2 * nlength (Suc (n + p n)) + 10 * nlength (Suc (Suc (2 * n + 2 * p n))) + (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) + (27 + 27 * thalt) * (9 + 2 * nlength thalt) + 14 * (nllength (map (λt. exc t <#> 0) [0..<thalt] @ [exc thalt <#> 0]))⇧^{2}+ 2 * nlength (Suc thalt) + 2 * nlength (Suc (Suc (2 * n + 2 * p n))) + 3 * max (nlength thalt) (nlength (Suc (Suc (Suc (2 * n + 2 * p n)))))" shows "transforms tm18 tps0 ttt tps18" unfolding tm18_def by (tform tps: tps17_def tps18_def k len_tpsA time: assms) definition "tps19 ≡ tpsA [11 := (⌊n⌋⇩_{N}, 1), 15 := (⌊p n⌋⇩_{N}, 1), 16 := (⌊2 * Suc (n + p n)⌋⇩_{N}, 1), 17 := (⌊thalt⌋⇩_{N}, 1), 4 := (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1), 7 := (⌊map (λt. exc t <#> 1) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1), 18 := (⌊thalt + Suc (2 * Suc (n + p n))⌋⇩_{N}, 1), 19 := (⌊max G (length M)⌋⇩_{N}, 1)]" lemma tm19 [transforms_intros]: assumes "ttt = 134 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) + 2 * nlength (Suc (n + p n)) + 10 * nlength (Suc (Suc (2 * n + 2 * p n))) + (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) + (27 + 27 * thalt) * (9 + 2 * nlength thalt) + 14 * (nllength (map (λt. exc t <#> 0) [0..<thalt] @ [exc thalt <#> 0]))⇧^{2}+ 2 * nlength (Suc thalt) + 2 * nlength (Suc (Suc (2 * n + 2 * p n))) + 3 * max (nlength thalt) (nlength (Suc (Suc (Suc (2 * n + 2 * p n))))) + 2 * nlength (max G (length M))" shows "transforms tm19 tps0 ttt tps19" unfolding tm19_def proof (tform tps: assms nlength_0) have "tps18 ! 19 = tpsA ! 19" using tps18_def by simp also have "... = tps0 ! 19" using tpsA_def by simp also have "... = (⌊0⌋⇩_{N}, 1)" using tps0 canrepr_0 k by simp finally show "tps18 ! 19 = (⌊0⌋⇩_{N}, 1)" . show "19 < length tps18" using tps18_def len_tpsA k by simp show "tps19 = tps18[19 := (⌊max G (length M)⌋⇩_{N}, 1)]" using tps19_def tps18_def len_tpsA k by presburger qed definition "tps20 ≡ tpsA [11 := (⌊n⌋⇩_{N}, 1), 15 := (⌊p n⌋⇩_{N}, 1), 16 := (⌊2 * Suc (n + p n)⌋⇩_{N}, 1), 17 := (⌊thalt⌋⇩_{N}, 1), 4 := (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1), 7 := (⌊map (λt. exc t <#> 1) [0..<Suc thalt]⌋⇩_{N}⇩_{L}, 1), 18 := (⌊thalt + Suc (2 * Suc (n + p n))⌋⇩_{N}, 1), 19 := (⌊max G (length M)⌋⇩_{N}, 1), 20 := (⌊(thalt + Suc (2 * Suc (n + p n))) * max G (length M)⌋⇩_{N}, 1)]" lemma tm20: assumes "ttt = 138 + 11 * n⇧^{2}+ (d_polynomial p + d_polynomial p * (nlength n)⇧^{2}) + 3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) + 2 * nlength (Suc (n + p n)) + 10 * nlength (Suc (Suc (2 * n + 2 * p n))) + (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) + (27 + 27 * thalt) * (9 + 2 * nlength thalt) + 14 * (nllength (map (λt. exc t <#> 0) [0..<thalt] @ [exc thalt <#> 0]))⇧^{2}+ 2 * nlength (Suc thalt) + 2 * nlength (Suc (Suc (2 * n + 2 * p n))) + 3 * max (nlength thalt) (nlength (Suc (Suc (Suc (2 * n + 2 * p n))))) + 2 * nlength (max G (length M)) + 26 * (nlength (Suc (Suc (Suc (thalt + (2 * n + 2 * p n))))) + nlength (max G (length M))) * (nlength (Suc (Suc (Suc (thalt + (2 * n + 2 * p n))))) + nlength (max G (length M)))" shows "transforms tm20 tps0 ttt tps20" unfolding tm20_def proof (tform time: assms) have "tps19 ! 20 = tpsA ! 20" using tps19_def by simp also have "... = tps0 ! 20" using tpsA_def by simp also have "... = (⌊0⌋⇩_{N}, 1)" using tps0 canrepr_0 k by simp finally show "tps19 ! 20 = (⌊0⌋⇩_{N}, 1)" . show "tps20 = tps19 [20 := (⌊Suc (Suc (Suc (thalt + (2 * n + 2 * p n)))) * max G (length M)⌋⇩_{N}, 1)]" unfolding tps20_def tps19_def by (simp add: list_update_swap) show "18 < length tps19" "19 < length tps19" "20 < length tps19" using tps19_def k len_tpsA by (simp_all only: length_list_update) have "tps19 ! 18 = (⌊thalt + Suc (2 * Suc