# Theory Aux_TM_Reducing

chapter ‹Auxiliary Turing machines for reducing $\NP$ languages to \SAT{}\label{s:Aux_TM}›

theory Aux_TM_Reducing
imports Reducing
begin

text ‹
In the previous chapter we have seen how to reduce a language $L\in\NP$ to
\SAT{} by constructing for every string $x$ a CNF formula $\Phi$ that is
satisfiable iff.\ $x\in L$. To complete the Cook-Levin theorem it remains to
show that there is a polynomial-time Turing machine that on input $x$ outputs
$\Phi$.  Constructing such a TM will be the subject of the rest of this article
and conclude in the next chapter. This chapter introduces several TMs used in
the construction.
›

section ‹Generating literals›

text ‹
Our representation of CNF formulas as lists of lists of numbers is based on a
representation of literals as numbers. Our function @{const literal_n} encodes
the positive literal $v_i$ as the number $2i + 1$ and the negative literal $\bar v_i$ as $2i$. We already have the Turing machine @{const tm_times2} to cover the
second case. Now we build a TM for the first case, that is, for doubling and
incrementing.

\null
›

definition tm_times2incr :: "tapeidx ⇒ machine" where
"tm_times2incr j ≡ tm_times2 j ;; tm_incr j"

lemma tm_times2incr_tm:
assumes "0 < j" and "j < k" and "G ≥ 4"
shows "turing_machine k G (tm_times2incr j)"
unfolding tm_times2incr_def using tm_times2_tm tm_incr_tm assms by simp

lemma transforms_tm_times2incrI [transforms_intros]:
fixes j :: tapeidx
fixes k :: nat and tps tps' :: "tape list"
assumes "k ≥ 2" and "j > 0" and "j < k" and "length tps = k"
assumes "tps ! j = (⌊n⌋⇩N, 1)"
assumes "t = 12 + 4 * nlength n"
assumes "tps' = tps[j := (⌊Suc (2 * n)⌋⇩N, 1)]"
shows "transforms (tm_times2incr j) tps t tps'"
proof -
define tt where "tt = 10 + (2 * nlength n + 2 * nlength (2 * n))"
have "transforms (tm_times2incr j) tps tt tps'"
unfolding tm_times2incr_def by (tform tps: tt_def assms)
moreover have "tt ≤ t"
proof -
have "tt = 10 + 2 * nlength n + 2 * nlength (2 * n)"
using tt_def by simp
also have "... ≤ 10 + 2 * nlength n + 2 * (Suc (nlength n))"
proof -
have "nlength (2 * n) ≤ Suc (nlength n)"
by (metis eq_imp_le gr0I le_SucI nat_0_less_mult_iff nlength_even_le)
then show ?thesis
by simp
qed
also have "... = 12 + 4 * nlength n"
by simp
finally show ?thesis
using assms(6) by simp
qed
ultimately show ?thesis
using transforms_monotone by simp
qed

lemma literal_n_rename:
assumes "v div 2 < length σ"
shows "2 * σ ! (v div 2) + v mod 2 = (literal_n ∘ rename σ) (n_literal v)"
proof (cases "even v")
case True
then show ?thesis
using n_literal_def assms by simp
next
case False
then show ?thesis
using n_literal_def assms by simp presburger
qed

text ‹
Combining @{const tm_times2} and @{const tm_times2incr}, the next Turing machine
accepts a variable index $i$ on tape $j_1$ and a flag $b$ on tape $j_2$ and
outputs on tape $j_1$ the encoding of the positive literal $v_i$ or the negative
literal $\bar v_i$ if $b$ is positive or zero, respectively.
›

definition tm_to_literal :: "tapeidx ⇒ tapeidx ⇒ machine" where
"tm_to_literal j1 j2 ≡
IF λrs. rs ! j2 = □ THEN
tm_times2 j1
ELSE
tm_times2incr j1
ENDIF"

lemma tm_to_literal_tm:
assumes "k ≥ 2" and "G ≥ 4" and "0 < j1" and "j1 < k" and "j2 < k"
shows "turing_machine k G (tm_to_literal j1 j2)"
unfolding tm_to_literal_def
using assms tm_times2_tm tm_times2incr_tm turing_machine_branch_turing_machine
by simp

lemma transforms_tm_to_literalI [transforms_intros]:
fixes j1 j2 :: tapeidx
fixes tps tps' :: "tape list" and ttt k i b :: nat
assumes "0 < j1" "j1 < k" "j2 < k" "2 ≤ k" "length tps = k"
assumes
"tps ! j1 = (⌊i⌋⇩N, 1)"
"tps ! j2 = (⌊b⌋⇩N, 1)"
assumes "ttt = 13 + 4 * nlength i"
assumes "tps' = tps
[j1 := (⌊2 * i + (if b = 0 then 0 else 1)⌋⇩N, 1)]"
shows "transforms (tm_to_literal j1 j2) tps ttt tps'"
unfolding tm_to_literal_def
proof (tform tps: assms read_ncontents_eq_0)
show "5 + 2 * nlength i + 2 ≤ ttt" and "12 + 4 * nlength i + 1 ≤ ttt"
using assms(8) by simp_all
qed

section ‹A Turing machine for relabeling formulas›

text ‹
In order to construct $\Phi_9$, we must construct CNF formulas $\chi_t$, which
have the form $\rho(\psi)$ or $\rho'(\psi')$. So we need a Turing machine for
relabeling formulas. In this section we devise a Turing machine that gets a
substitution $\sigma$ and a CNF formula $\phi$ and outputs $\sigma(\phi)$. In
order to bound its running time we first prove some bounds on the length of
relabeled formulas.
›

subsection ‹The length of relabeled formulas›

text ‹
First we bound the length of the representation of a single relabeled clause.
In the following lemma the assumption ensures that the substitution $\sigma$ has
a value for every variable in the clause.
›

lemma nllength_rename:
assumes "∀v∈set clause. v div 2 < length σ"
shows "nllength (map (literal_n ∘ rename σ) (n_clause clause)) ≤ length clause * Suc (nllength σ)"
proof (cases "σ = []")
case True
then show ?thesis
using assms n_clause_def by simp
next
case False
let ?f = "literal_n ∘ rename σ ∘ n_literal"
have *: "map (literal_n ∘ rename σ) (n_clause clause) = map ?f clause"
using n_clause_def by simp

have "nlength (2 * n + 1) ≤ Suc (nlength n)" for n
using nlength_times2plus1 by simp
then have "nlength (2 * Max (set σ) + 1) ≤ Suc (nlength (Max (set σ)))"
by simp
moreover have "nlength (Max (set σ)) ≤ nllength σ - 1"
using False member_le_nllength_1 by simp
ultimately have "nlength (2 * Max (set σ) + 1) ≤ Suc (nllength σ - 1)"
by simp
then have **: "nlength (2 * Max (set σ) + 1) ≤ nllength σ"
using nllength_gr_0 False by simp

have "?f n ≤ 2 * (σ ! (n div 2)) + 1" if "n div 2 < length σ" for n
using n_literal_def by (cases "even n") simp_all
then have "?f v ≤ 2 * (σ ! (v div 2)) + 1" if "v ∈ set clause" for v
using assms that by simp
moreover have "σ ! (v div 2) ≤ Max (set σ)" if "v ∈ set clause" for v
using that assms by simp
ultimately have "?f v ≤ 2 * Max (set σ) + 1" if "v ∈ set clause" for v
using that by fastforce
then have "n ≤ 2 * Max (set σ) + 1" if "n ∈ set (map ?f clause)" for n
using that by auto
then have "nllength (map ?f clause) ≤ Suc (nlength (2 * Max (set σ) + 1)) * length (map ?f clause)"
using nllength_le_len_mult_max by blast
also have "... = Suc (nlength (2 * Max (set σ) + 1)) * length clause"
by simp
also have "... ≤ Suc (nllength σ) * length clause"
using ** by simp
finally have "nllength (map ?f clause) ≤ Suc (nllength σ) * length clause" .
then show ?thesis
using * by (metis mult.commute)
qed

text ‹
Our upper bound for the length of the symbol representation of a relabeled
formula is fairly crude. It is basically the length of the string resulting from
replacing every symbol of the original formula by the entire substitution.
›

lemma nlllength_relabel:
assumes "∀clause∈set φ. ∀v∈set (clause_n clause). v div 2 < length σ"
shows "nlllength (formula_n (relabel σ φ)) ≤ Suc (nllength σ) * nlllength (formula_n φ)"
using assms
proof (induction φ)
case Nil
then show ?case
by (simp add: relabel_def)
next
case (Cons clause φ)
let ?nclause = "clause_n clause"
have "∀v∈set ?nclause. v div 2 < length σ"
using Cons.prems by simp
then have "nllength (map (literal_n ∘ rename σ) (n_clause ?nclause)) ≤ length ?nclause * Suc (nllength σ)"
using nllength_rename by simp
then have "nllength (map (literal_n ∘ rename σ) clause) ≤ length clause * Suc (nllength σ)"
using clause_n_def n_clause_n by simp
moreover have "map (literal_n ∘ rename σ) clause = clause_n (map (rename σ) clause)"
using clause_n_def by simp
ultimately have *: "nllength (clause_n (map (rename σ) clause)) ≤ length clause * Suc (nllength σ)"
by simp

have "formula_n (relabel σ (clause # φ)) = clause_n (map (rename σ) clause) # formula_n (relabel σ φ)"
by (simp add: formula_n_def relabel_def)
then have "nlllength (formula_n (relabel σ (clause # φ))) =
nllength (clause_n (map (rename σ) clause)) + 1 + nlllength (formula_n (relabel σ φ))"
using nlllength_Cons by simp
also have "... ≤ length clause * Suc (nllength σ) + 1 + nlllength (formula_n (relabel σ φ))"
using * by simp
also have "... ≤ length clause * Suc (nllength σ) + 1 + Suc (nllength σ) * nlllength (formula_n φ)"
using Cons by (metis add_mono_thms_linordered_semiring(2) insert_iff list.set(2))
also have "... = 1 + Suc (nllength σ) * (length clause + nlllength (formula_n φ))"
by algebra
also have "... ≤ Suc (nllength σ) * (1 + length clause + nlllength (formula_n φ))"
by simp
also have "... ≤ Suc (nllength σ) * (1 + nllength (clause_n clause) + nlllength (formula_n φ))"
using length_le_nllength n_clause_def n_clause_n
by (metis add_Suc_shift add_le_cancel_right length_map mult_le_mono2 plus_1_eq_Suc)
also have "... = Suc (nllength σ) * (nlllength (formula_n (clause # φ)))"
using formula_n_def nlllength_Cons by simp
finally show ?case .
qed

text ‹
A simple sufficient condition for the assumption in the previous lemma.
›

lemma variables_σ:
assumes "variables φ ⊆ {..<length σ}"
shows "∀clause∈set φ.∀v∈set (clause_n clause). v div 2 < length σ"
proof standard+
fix clause :: clause and v :: nat
assume clause: "clause ∈ set φ" and v: "v ∈ set (clause_n clause)"

obtain i where i: "i < length clause" "v = literal_n (clause ! i)"
using v clause_n_def by (metis in_set_conv_nth length_map nth_map)
then have clause_i: "clause ! i = n_literal v"
using n_literal_n by simp

show "v div 2 < length σ"
proof (cases "even v")
case True
then have "clause ! i = Neg (v div 2)"
using clause_i n_literal_def by simp
then have "∃c∈set φ. Neg (v div 2) ∈ set c"
using clause i(1) by (metis nth_mem)
then have "v div 2 ∈ variables φ"
using variables_def by auto
then show ?thesis
using assms by auto
next
case False
then have "clause ! i = Pos (v div 2)"
using clause_i n_literal_def by simp
then have "∃c∈set φ. Pos (v div 2) ∈ set c"
using clause i(1) by (metis nth_mem)
then have "v div 2 ∈ variables φ"
using variables_def by auto
then show ?thesis
using assms by auto
qed
qed

text ‹
Combining the previous two lemmas yields this upper bound:
›

lemma nlllength_relabel_variables:
assumes "variables φ ⊆ {..<length σ}"
shows "nlllength (formula_n (relabel σ φ)) ≤ Suc (nllength σ) * nlllength (formula_n φ)"
using assms variables_σ nlllength_relabel by blast

subsection ‹Relabeling clauses›

text ‹
Relabeling a CNF formula is accomplished by relabeling each of its clauses. In
this section we devise a Turing machine for relabeling clauses. The TM accepts
on tape $j$ a list of numbers representing a substitution $\sigma$ and on tape
$j + 1$ a clause represented as a list of numbers. It outputs on tape $j + 2$
the relabeled clause, consuming the original clause on tape $j + 1$ in the
process.
›

definition tm_relabel_clause :: "tapeidx ⇒ machine" where
"tm_relabel_clause j ≡
WHILE [] ; λrs. rs ! (j + 1) ≠ □ DO
tm_nextract ¦ (j + 1) (j + 3) ;;
tm_mod2 (j + 3) (j + 4) ;;
tm_div2 (j + 3) ;;
tm_nth_inplace j (j + 3) ¦ ;;
tm_to_literal (j + 3) (j + 4) ;;
tm_append (j + 2) (j + 3) ;;
tm_setn (j + 3) 0 ;;
tm_setn (j + 4) 0
DONE ;;
tm_cr (j + 2) ;;
tm_erase_cr (j + 1)"

lemma tm_relabel_clause_tm:
assumes "G ≥ 5" and "j + 4 < k" and "0 < j"
shows "turing_machine k G (tm_relabel_clause j)"
unfolding tm_relabel_clause_def
using assms tm_nextract_tm tm_mod2_tm tm_div2_tm tm_nth_inplace_tm tm_to_literal_tm tm_append_tm tm_setn_tm
tm_cr_tm tm_erase_cr_tm Nil_tm turing_machine_loop_turing_machine
by simp

locale turing_machine_relabel_clause =
fixes j :: tapeidx
begin

definition "tm1 ≡ tm_nextract ¦ (j + 1) (j + 3)"
definition "tm2 ≡ tm1 ;; tm_mod2 (j + 3) (j + 4)"
definition "tm3 ≡ tm2 ;; tm_div2 (j + 3)"
definition "tm4 ≡ tm3 ;; tm_nth_inplace j (j + 3) ¦"
definition "tm5 ≡ tm4 ;; tm_to_literal (j + 3) (j + 4)"
definition "tm6 ≡ tm5 ;; tm_append (j + 2) (j + 3)"
definition "tm7 = tm6 ;; tm_setn (j + 3) 0"
definition "tm8 ≡ tm7 ;; tm_setn (j + 4) 0"
definition "tmL ≡ WHILE [] ; λrs. rs ! (j + 1) ≠ □ DO tm8 DONE"
definition "tm9 ≡ tmL ;; tm_cr (j + 2)"
definition "tm10 ≡ tm9 ;; tm_erase_cr (j + 1)"

lemma tm10_eq_tm_relabel_clause: "tm10 = tm_relabel_clause j"
unfolding tm_relabel_clause_def tm3_def tmL_def tm5_def tm4_def tm1_def tm2_def tm6_def tm7_def tm8_def tm9_def tm10_def
by simp

context
fixes tps0 :: "tape list" and k :: nat and σ clause :: "nat list"
assumes clause: "∀v∈set clause. v div 2 < length σ"
assumes jk: "0 < j" "j + 4 < k" "length tps0 = k"
assumes tps0:
"tps0 ! j = (⌊σ⌋⇩N⇩L, 1)"
"tps0 ! (j + 1) = (⌊clause⌋⇩N⇩L, 1)"
"tps0 ! (j + 2) = (⌊[]⌋⇩N⇩L, 1)"
"tps0 ! (j + 3) = (⌊0⌋⇩N, 1)"
"tps0 ! (j + 4) = (⌊0⌋⇩N, 1)"
begin

definition "tpsL t ≡ tps0
[j + 1 := nltape' clause t,
j + 2 := nltape (take t (map literal_n (map (rename σ) (n_clause clause))))]"

lemma tpsL_eq_tps0: "tpsL 0 = tps0"
using tpsL_def tps0 jk nllength_Nil by (metis One_nat_def list_update_id take0)

definition "tps1 t ≡ tps0
[j + 1 := nltape' clause (Suc t),
j + 2 := nltape (take t (map literal_n (map (rename σ) (n_clause clause)))),
j + 3 := (⌊clause ! t⌋⇩N, 1)]"

lemma tm1 [transforms_intros]:
assumes "t < length clause"
and "ttt = 12 + 2 * nlength (clause ! t)"
shows "transforms tm1 (tpsL t) ttt (tps1 t)"
unfolding tm1_def
proof (tform tps: assms(1) tpsL_def tps1_def tps0 jk)
show "ttt = 12 + 2 * nlength 0 + 2 * nlength (clause ! t)"
using assms(2) by simp
qed

definition "tps2 t ≡ tps0
[j + 1 := nltape' clause (Suc t),
j + 2 := nltape (take t (map literal_n (map (rename σ) (n_clause clause)))),
j + 3 := (⌊clause ! t⌋⇩N, 1),
j + 4 := (⌊(clause ! t) mod 2⌋⇩N, 1)]"

lemma tm2 [transforms_intros]:
assumes "t < length clause"
and "ttt = 13 + 2 * nlength (clause ! t)"
shows "transforms tm2 (tpsL t) ttt (tps2 t)"
unfolding tm2_def by (tform tps: assms tps1_def tps2_def tps0 jk)

definition "tps3 t ≡ tps0
[j + 1 := nltape' clause (Suc t),
j + 2 := nltape (take t (map literal_n (map (rename σ) (n_clause clause)))),
j + 3 := (⌊clause ! t div 2⌋⇩N, 1),
j + 4 := (⌊clause ! t mod 2⌋⇩N, 1)]"

lemma tm3 [transforms_intros]:
assumes "t < length clause"
and "ttt = 16 + 4 * nlength (clause ! t)"
shows "transforms tm3 (tpsL t) ttt (tps3 t)"
unfolding tm3_def by (tform tps: assms(1) tps2_def tps3_def jk time: assms(2))

definition "tps4 t ≡ tps0
[j + 1 := nltape' clause (Suc t),
j + 2 := nltape (take t (map literal_n (map (rename σ) (n_clause clause)))),
j + 3 := (⌊σ ! (clause ! t div 2)⌋⇩N, 1),
j + 4 := (⌊clause ! t mod 2⌋⇩N, 1)]"

lemma tm4 [transforms_intros]:
assumes "t < length clause"
and "ttt = 28 + 4 * nlength (clause ! t) + 18 * (nllength σ)⇧2"
shows "transforms tm4 (tpsL t) ttt (tps4 t)"
unfolding tm4_def
proof (tform tps: assms(1) tps0 tps3_def tps4_def jk clause time: assms(2))
show "tps4 t = (tps3 t)[j + 3 := (⌊σ ! (clause ! t div 2)⌋⇩N, 1)]"
unfolding tps4_def tps3_def by (simp add: list_update_swap[of "j + 3"])
qed

definition "tps5 t ≡ tps0
[j + 1 := nltape' clause (Suc t),
j + 2 := nltape (take t (map literal_n (map (rename σ) (n_clause clause)))),
j + 3 := (⌊2 * (σ ! (clause ! t div 2)) + clause ! t mod 2⌋⇩N, 1),
j + 4 := (⌊clause ! t mod 2⌋⇩N, 1)]"

lemma tm5 [transforms_intros]:
assumes "t < length clause"
and "ttt = 41 + 4 * nlength (clause ! t) + 18 * (nllength σ)⇧2 +
4 * nlength (σ ! (clause ! t div 2))"
shows "transforms tm5 (tpsL t) ttt (tps5 t)"
unfolding tm5_def by (tform tps: assms(1) tps0 tps4_def tps5_def jk time: assms(2))

definition "tps6 t ≡ tps0
[j + 1 := nltape' clause (Suc t),
j + 2 := nltape (take (Suc t) (map literal_n (map (rename σ) (n_clause clause)))),
j + 3 := (⌊2 * (σ ! (clause ! t div 2)) + clause ! t mod 2⌋⇩N, 1),
j + 4 := (⌊clause ! t mod 2⌋⇩N, 1)]"

lemma tm6:
assumes "t < length clause"
and "ttt = 47 + 4 * nlength (clause ! t) + 18 * (nllength σ)⇧2 +
4 * nlength (σ ! (clause ! t div 2)) +
2 * nlength (2 * σ ! (clause ! t div 2) + clause ! t mod 2)"
shows "transforms tm6 (tpsL t) ttt (tps6 t)"
unfolding tm6_def
proof (tform tps: assms(1) tps0 tps5_def tps6_def jk)
have "2 * σ ! (clause ! t div 2) + clause ! t mod 2 =
(literal_n ∘ rename σ) (n_literal (clause ! t))"
using clause assms(1) literal_n_rename by simp
then have "2 * σ ! (clause ! t div 2) + clause ! t mod 2 =
(map (literal_n ∘ rename σ) (n_clause clause)) ! t"
using assms(1) by (simp add: n_clause_def)
then have "take t (map (literal_n ∘ rename σ) (n_clause clause)) @
[2 * σ ! (clause ! t div 2) + clause ! t mod 2] =
take (Suc t) (map (literal_n ∘ rename σ) (n_clause clause))"
by (simp add: assms(1) n_clause_def take_Suc_conv_app_nth)
then show "tps6 t = (tps5 t)
[j + 2 := nltape
(take t (map (literal_n ∘ rename σ) (n_clause clause)) @
[2 * σ ! (clause ! t div 2) + clause ! t mod 2])]"
unfolding tps5_def tps6_def
by (simp only: list_update_overwrite list_update_swap_less[of "j + 2"]) simp
show "ttt = 41 + 4 * nlength (clause ! t) + 18 * (nllength σ)⇧2 +
4 * nlength (σ ! (clause ! t div 2)) +
(7 + nllength (take t (map (literal_n ∘ rename σ) (n_clause clause))) -
Suc (nllength (take t (map (literal_n ∘ rename σ) (n_clause clause)))) +
2 * nlength (2 * σ ! (clause ! t div 2) + clause ! t mod 2))"
using assms(2) by simp
qed

lemma nlength_σ1:
assumes "t < length clause"
shows "nlength (clause ! t) ≤ nllength σ"
proof -
have "clause ! t div 2 < length σ"
using clause assms(1) by simp
then have "nlength (clause ! t div 2) < length σ"
using nlength_le_n by (meson leD le_less_linear order.trans)
then have "nlength (clause ! t) ≤ length σ"
using canrepr_div_2 by simp
then show "nlength (clause ! t) ≤ nllength σ"
using length_le_nllength by (meson dual_order.trans mult_le_mono2)
qed

lemma nlength_σ2:
assumes "t < length clause"
shows "nlength (σ ! (clause ! t div 2)) ≤ nllength σ"
using assms clause member_le_nllength nth_mem by simp

lemma nlength_σ3:
assumes "t < length clause"
shows "nlength (2 * σ ! (clause ! t div 2) + clause ! t mod 2) ≤ Suc (nllength σ)"
proof -
have "nlength (2 * σ ! (clause ! t div 2) + clause ! t mod 2) ≤ nlength (2 * σ ! (clause ! t div 2) + 1)"
using nlength_mono by simp
also have "... ≤ Suc (nlength (σ ! (clause ! t div 2)))"
using nlength_times2plus1 by (meson dual_order.trans)
finally show ?thesis
using nlength_σ2 assms by fastforce
qed

lemma tm6' [transforms_intros]:
assumes "t < length clause"
and "ttt = 49 + 28 * nllength σ ^ 2"
shows "transforms tm6 (tpsL t) ttt (tps6 t)"
proof -
let ?ttt = "47 + 4 * nlength (clause ! t) + 18 * (nllength σ)⇧2 +
4 * nlength (σ ! (clause ! t div 2)) +
2 * nlength (2 * σ ! (clause ! t div 2) + clause ! t mod 2)"

have "?ttt ≤ 47 + 4 * nllength σ + 18 * (nllength σ)⇧2 +
4 * nllength σ + 2 * Suc (nllength σ)"
using nlength_σ1 nlength_σ3 nlength_σ2 assms(1) by fastforce
also have "... = 49 + 10 * nllength σ + 18 * (nllength σ)⇧2"
by simp
also have "... ≤ 49 + 10 * nllength σ ^ 2 + 18 * (nllength σ)⇧2"
using linear_le_pow by simp
also have "... = 49 + 28 * nllength σ ^ 2"
by simp
finally have "?ttt ≤ 49 + 28 * nllength σ ^ 2" .
then show ?thesis
using tm6 assms transforms_monotone by blast
qed

definition "tps7 t ≡ tps0
[j + 1 := nltape' clause (Suc t),
j + 2 := nltape (take (Suc t) (map literal_n (map (rename σ) (n_clause clause)))),
j + 4 := (⌊clause ! t mod 2⌋⇩N, 1)]"

lemma tm7:
assumes "t < length clause"
and "ttt = 59 + 28 * nllength σ ^ 2 +
2 * nlength (2 * σ ! (clause ! t div 2) + clause ! t mod 2)"
shows "transforms tm7 (tpsL t) ttt (tps7 t)"
unfolding tm7_def
proof (tform tps: assms(1) tps0 tps6_def tps7_def jk time: assms(2))
show "tps7 t = (tps6 t)[j + 3 := (⌊0⌋⇩N, 1)]"
using tps6_def tps7_def tps0 jk
by (smt (verit) add_left_cancel list_update_id list_update_overwrite list_update_swap num.simps(8)
numeral_eq_iff one_eq_numeral_iff semiring_norm(84))
qed

lemma tm7' [transforms_intros]:
assumes "t < length clause"
and "ttt = 61 + 30 * nllength σ ^ 2"
shows "transforms tm7 (tpsL t) ttt (tps7 t)"
proof -
let ?ttt = "59 + 28 * nllength σ ^ 2 +
2 * nlength (2 * σ ! (clause ! t div 2) + clause ! t mod 2)"
have "?ttt ≤ 59 + 28 * nllength σ ^ 2 + 2 * Suc (nllength σ)"
using nlength_σ3 assms(1) by fastforce
also have "... = 61 + 28 * nllength σ ^ 2 + 2 * nllength σ"
by simp
also have "... ≤ 61 + 30 * nllength σ ^ 2"
using linear_le_pow by simp
finally have "?ttt ≤ 61 + 30 * nllength σ ^ 2" .
then show ?thesis
using assms tm7 transforms_monotone by blast
qed

definition "tps8 t ≡ tps0
[j + 1 := nltape' clause (Suc t),
j + 2 := nltape (take (Suc t) (map literal_n (map (rename σ) (n_clause clause))))]"

lemma tm8:
assumes "t < length clause"
and "ttt = 61 + 30 * (nllength σ)⇧2 + (10 + 2 * nlength (clause ! t mod 2))"
shows "transforms tm8 (tpsL t) ttt (tps8 t)"
unfolding tm8_def
proof (tform tps: assms(1) tps0 tps7_def tps8_def jk time: assms(2))
show "tps8 t = (tps7 t)[j + 4 := (⌊0⌋⇩N, 1)]"
using tps7_def tps8_def tps0 jk
by (smt (verit) add_left_imp_eq list_update_id list_update_overwrite list_update_swap numeral_eq_iff
numeral_eq_one_iff semiring_norm(85) semiring_norm(87))
qed

lemma tm8' [transforms_intros]:
assumes "t < length clause"
and "ttt = 71 + 32 * (nllength σ)⇧2"
shows "transforms tm8 (tpsL t) ttt (tpsL (Suc t))"
proof -
have "nlength (clause ! t mod 2) ≤ nllength σ"
using assms(1) nlength_σ1 by (meson mod_less_eq_dividend nlength_mono order.trans)
then have "nlength (clause ! t mod 2) ≤ nllength σ ^ 2"
using linear_le_pow by (metis nat_le_linear power2_nat_le_imp_le verit_la_disequality)
then have "61 + 30 * (nllength σ)⇧2 + (10 + 2 * nlength (clause ! t mod 2)) ≤ ttt"
using assms(2) by simp
then have "transforms tm8 (tpsL t) ttt (tps8 t)"
using assms(1) tm8 transforms_monotone by blast
moreover have "tps8 t = tpsL (Suc t)"
using tps8_def tpsL_def by simp
ultimately show ?thesis
by simp
qed

lemma tmL [transforms_intros]:
assumes "ttt = length clause * (73 + 32 * (nllength σ)⇧2) + 1"
shows "transforms tmL (tpsL 0) ttt (tpsL (length clause))"
unfolding tmL_def
proof (tform)
let ?t = "71 + 32 * (nllength σ)⇧2"
show "read (tpsL t) ! (j + 1) ≠ □" if "t < length clause" for t
proof -
have "tpsL t ! (j + 1) = nltape' clause t"
using tpsL_def jk by simp
then show ?thesis
using nltape'_tape_read that tapes_at_read' tpsL_def jk
by (smt (verit) Suc_eq_plus1 leD length_list_update less_add_same_cancel1 less_trans_Suc zero_less_numeral)
qed
show "¬ read (tpsL (length clause)) ! (j + 1) ≠ □"
proof -
have "tpsL (length clause) ! (j + 1) = nltape' clause (length clause)"
using tpsL_def jk by simp
then show ?thesis
using nltape'_tape_read tapes_at_read' tpsL_def jk
by (smt (verit) Suc_eq_plus1 length_list_update less_add_same_cancel1 less_or_eq_imp_le less_trans_Suc zero_less_numeral)
qed
show "length clause * (71 + 32 * (nllength σ)⇧2 + 2) + 1 ≤ ttt"
using assms(1) by simp
qed

lemma tpsL_length: "tpsL (length clause) = tps0
[j + 1 := nltape' clause (length clause),
j + 2 := nltape (map literal_n (map (rename σ) (n_clause clause)))]"
using tpsL_def by (simp add: n_clause_def)

definition "tps9 ≡ tps0
[j + 1 := nltape' clause (length clause),
j + 2 := (⌊map literal_n (map (rename σ) (n_clause clause))⌋⇩N⇩L, 1)]"

lemma tm9:
assumes "ttt = 4 + length clause * (73 + 32 * (nllength σ)⇧2) +
nllength (map (literal_n ∘ rename σ) (n_clause clause))"
shows "transforms tm9 (tpsL 0) ttt tps9"
unfolding tm9_def
proof (tform tps: tps0 tps9_def tpsL_def jk tpsL_length)
show "clean_tape (tpsL (length clause) ! (j + 2))"
using tpsL_def jk clean_tape_nlcontents tps0(3) by simp
show "ttt = length clause * (73 + 32 * (nllength σ)⇧2) + 1 +
(tpsL (length clause) :#: (j + 2) + 2)"
using n_clause_def assms jk tpsL_length by fastforce
qed

lemma tm9' [transforms_intros]:
assumes "ttt = 4 + 2 * length clause * (73 + 32 * (nllength σ)⇧2)"
shows "transforms tm9 tps0 ttt tps9"
proof -
let ?ttt = "4 + length clause * (73 + 32 * (nllength σ)⇧2) +
nllength (map (literal_n ∘ rename σ) (n_clause clause))"
have "?ttt ≤ 4 + length clause * (73 + 32 * (nllength σ)⇧2) +
length clause * Suc (nllength σ)"
using clause nllength_rename by simp
also have "... ≤ 4 + length clause * (73 + 32 * (nllength σ)⇧2) +
length clause * (Suc (nllength σ ^ 2))"
by (simp add: linear_le_pow)
also have "... ≤ 4 + length clause * (73 + 32 * (nllength σ)⇧2) +
length clause * (73 + nllength σ ^ 2)"
by (metis One_nat_def Suc_eq_plus1 Suc_leI add.commute add_left_mono mult_le_mono2 zero_less_numeral)
also have "... ≤ 4 + length clause * (73 + 32 * (nllength σ)⇧2) +
length clause * (73 + 32 * nllength σ ^ 2)"
by simp
also have "... = 4 + 2 * length clause * (73 + 32 * (nllength σ)⇧2)"
by simp
finally have "?ttt ≤ 4 + 2 * length clause * (73 + 32 * (nllength σ)⇧2)" .
then show ?thesis
using tm9 assms transforms_monotone tpsL_eq_tps0 by fastforce
qed

definition "tps10 ≡ tps0
[j + 1 := (⌊[]⌋⇩N⇩L, 1),
j + 2 := (⌊map literal_n (map (rename σ) (n_clause clause))⌋⇩N⇩L, 1)]"

lemma tm10:
assumes "ttt = 11 + 2 * length clause * (73 + 32 * (nllength σ)⇧2) + 3 * nllength clause"
shows "transforms tm10 tps0 ttt tps10"
unfolding tm10_def
proof (tform tps: tps0 tps9_def jk)
show "tps9 ::: (j + 1) = ⌊numlist clause⌋"
using tps9_def jk tps0(2) nlcontents_def by simp
show "proper_symbols (numlist clause)"
using proper_symbols_numlist by simp
show "tps10 = tps9[j + 1 := (⌊[]⌋, 1)]"
by (simp add: jk nlcontents_def tps0 tps10_def tps9_def list_update_swap numlist_Nil)
show "ttt = 4 + 2 * length clause * (73 + 32 * (nllength σ)⇧2) +
(tps9 :#: (j + 1) + 2 * length (numlist clause) + 6)"
using assms tps9_def jk nllength_def by simp
qed

lemma tm10':
assumes "ttt = 11 + 64 * nllength clause * (3 + (nllength σ)⇧2)"
shows "transforms tm10 tps0 ttt tps10"
proof -
let ?ttt = "11 + 2 * length clause * (73 + 32 * (nllength σ)⇧2) + 3 * nllength clause"
have "?ttt ≤ 11 + 2 * nllength clause * (73 + 32 * (nllength σ)⇧2) + 3 * nllength clause"
by (simp add: length_le_nllength)
also have "... ≤ 11 + 2 * nllength clause * (73 + 32 * (nllength σ)⇧2) + 2 * 2 * nllength clause"
by simp
also have "... = 11 + 2 * nllength clause * (75 + 32 * (nllength σ)⇧2)"
by algebra
also have "... ≤ 11 + 2 * nllength clause * (96 + 32 * (nllength σ)⇧2)"
by simp
also have "... = 11 + 2 * 32 * nllength clause * (3 + (nllength σ)⇧2)"
by simp
also have "... = 11 + 64 * nllength clause * (3 + (nllength σ)⇧2)"
by simp
finally have "?ttt ≤ 11 + 64 * nllength clause * (3 + (nllength σ)⇧2)" .
then show ?thesis
using tm10 assms transforms_monotone by blast
qed

end

end  (* locale turing_machine_relabel-clause *)

lemma transforms_tm_relabel_clauseI [transforms_intros]:
fixes j :: tapeidx
fixes tps tps' :: "tape list" and ttt k :: nat and σ clause :: "nat list"
assumes "0 < j" "j + 4 < k" "length tps = k"
and "∀v∈set clause. v div 2 < length σ"
assumes
"tps ! j = (⌊σ⌋⇩N⇩L, 1)"
"tps ! (j + 1) = (⌊clause⌋⇩N⇩L, 1)"
"tps ! (j + 2) = (⌊[]⌋⇩N⇩L, 1)"
"tps ! (j + 3) = (⌊0⌋⇩N, 1)"
"tps ! (j + 4) = (⌊0⌋⇩N, 1)"
assumes "ttt = 11 + 64 * nllength clause * (3 + (nllength σ)⇧2)"
assumes "tps' = tps
[j + 1 := (⌊[]⌋⇩N⇩L, 1),
j + 2 := (⌊clause_n (map (rename σ) (n_clause clause))⌋⇩N⇩L, 1)]"
shows "transforms (tm_relabel_clause j) tps ttt tps'"
proof -
interpret loc: turing_machine_relabel_clause j .
show ?thesis
using assms loc.tm10_eq_tm_relabel_clause loc.tps10_def loc.tm10' clause_n_def by simp
qed

subsection ‹Relabeling CNF formulas›

text ‹
A Turing machine can relabel a CNF formula by relabeling each clause using the
TM @{const tm_relabel_clause}. The next TM accepts a CNF formula as a list of
lists of literals on tape $j_1$ and a substitution $\sigma$ as a list of numbers
on tape $j_2 + 1$. It outputs the relabeled formula on tape $j_2$, which
initially must be empty.
›

definition tm_relabel :: "tapeidx ⇒ tapeidx ⇒ machine" where
"tm_relabel j1 j2 ≡
WHILE [] ; λrs. rs ! j1 ≠ □ DO
tm_nextract ♯ j1 (j2 + 2) ;;
tm_relabel_clause (j2 + 1) ;;
tm_appendl j2 (j2 + 3) ;;
tm_erase_cr (j2 + 3)
DONE ;;
tm_cr j1 ;;
tm_cr j2"

lemma tm_relabel_tm:
assumes "G ≥ 6" and "j2 + 5 < k" and "0 < j1" and "j1 < j2"
shows "turing_machine k G (tm_relabel j1 j2)"
unfolding tm_relabel_def
using assms tm_cr_tm tm_nextract_tm tm_appendl_tm tm_relabel_clause_tm Nil_tm tm_erase_cr_tm turing_machine_loop_turing_machine
by simp

locale turing_machine_relabel =
fixes j1 j2 :: tapeidx
begin

definition "tmL1 ≡ tm_nextract ♯ j1 (j2 + 2)"
definition "tmL2 ≡ tmL1 ;; tm_relabel_clause (j2 + 1)"
definition "tmL3 ≡ tmL2 ;; tm_appendl j2 (j2 + 3)"
definition "tmL4 ≡ tmL3 ;; tm_erase_cr (j2 + 3)"
definition "tmL ≡ WHILE [] ; λrs. rs ! j1 ≠ □ DO tmL4 DONE"
definition "tm2 ≡ tmL ;; tm_cr j1"
definition "tm3 ≡ tm2 ;; tm_cr j2"

lemma tm3_eq_tm_relabel: "tm3 = tm_relabel j1 j2"
unfolding tm_relabel_def tm2_def tmL_def tmL4_def tmL3_def tmL2_def tmL1_def tm3_def by simp

context
fixes tps0 :: "tape list" and k :: nat and σ :: "nat list" and φ :: formula
assumes variables: "variables φ ⊆ {..<length σ}"
assumes jk: "0 < j1" "j1 < j2" "j2 + 5 < k" "length tps0 = k"
assumes tps0:
"tps0 ! j1 = (⌊formula_n φ⌋⇩N⇩L⇩L, 1)"
"tps0 ! j2 = (⌊[]⌋⇩N⇩L⇩L, 1)"
"tps0 ! (j2 + 1) = (⌊σ⌋⇩N⇩L, 1)"
"tps0 ! (j2 + 2) = (⌊[]⌋⇩N⇩L, 1)"
"tps0 ! (j2 + 3) = (⌊[]⌋⇩N⇩L, 1)"
"tps0 ! (j2 + 4) = (⌊0⌋⇩N, 1)"
"tps0 ! (j2 + 5) = (⌊0⌋⇩N, 1)"
begin

abbreviation nφ :: "nat list list" where
"nφ ≡ formula_n φ"

definition tpsL :: "nat ⇒ tape list" where
"tpsL t ≡ tps0
[j1 := nlltape' nφ t,
j2 := nlltape (formula_n (take t (relabel σ φ)))]"

lemma tpsL_eq_tps0: "tpsL 0 = tps0"
using tps0 tpsL_def formula_n_def nlllength_def numlist_Nil numlist_def numlistlist_def
by (metis One_nat_def list.map(1) list.size(3) list_update_id take0)

definition tpsL1 :: "nat ⇒ tape list" where
"tpsL1 t ≡ tps0
[j1 := nlltape' nφ (Suc t),
j2 := nlltape (formula_n (take t (relabel σ φ))),
j2 + 2 := (⌊nφ ! t⌋⇩N⇩L, 1)]"

lemma tmL1 [transforms_intros]:
assumes "ttt = 12 + 2 * nllength (nφ ! t)"
and "t < length φ"
shows "transforms tmL1 (tpsL t) ttt (tpsL1 t)"
unfolding tmL1_def
proof (tform tps: tps0 tpsL_def tpsL1_def jk)
show "t < length nφ"
using assms(2) formula_n_def by simp
show "tpsL1 t = (tpsL t)
[j1 := nlltape' nφ (Suc t),
j2 + 2 := (⌊nφ ! t⌋⇩N⇩L, 1)]"
using tpsL1_def tpsL_def by (simp add: jk list_update_swap_less)
show "ttt = 12 + 2 * nllength [] + 2 * nllength (nφ ! t)"
using assms(1) by simp
qed

definition tpsL2 :: "nat ⇒ tape list" where
"tpsL2 t ≡ tps0
[j1 := nlltape' nφ (Suc t),
j2 := nlltape (formula_n (take t (relabel σ φ))),
j2 + 2 := (⌊[]⌋⇩N⇩L, 1),
j2 + 3 := (⌊clause_n (map (rename σ) (n_clause (nφ ! t)))⌋⇩N⇩L, 1)]"

lemma tmL2 [transforms_intros]:
assumes "ttt = 23 + 2 * nllength (nφ ! t) + 64 * nllength (nφ ! t) * (3 + (nllength σ)⇧2)"
and "t < length φ"
shows "transforms tmL2 (tpsL t) ttt (tpsL2 t)"
unfolding tmL2_def
proof (tform tps: assms(2) tps0 tpsL1_def jk)
show "∀v∈set (nφ ! t). v div 2 < length σ"
using variables_σ variables assms(2) by (metis formula_n_def nth_map nth_mem)
have "tpsL1 t ! (j2 + (1 + 2)) = (⌊[]⌋⇩N⇩L, 1)"
using tpsL1_def jk tps0 by (simp add: numeral_3_eq_3)
then show "tpsL1 t ! (j2 + 1 + 2) = (⌊[]⌋⇩N⇩L, 1)"
by (metis add.assoc)
have "tpsL1 t ! (j2 + (1 + 3)) = (⌊0⌋⇩N, 1)"
using tpsL1_def jk tps0 by simp
then show "tpsL1 t ! (j2 + 1 + 3) = (⌊0⌋⇩N, 1)"
by (metis add.assoc)
have "tpsL1 t ! (j2 + (1 + 4)) = (⌊0⌋⇩N, 1)"
using tpsL1_def jk tps0 by simp
then show "tpsL1 t ! (j2 + 1 + 4) = (⌊0⌋⇩N, 1)"
by (metis add.assoc)
have "tpsL2 t = (tpsL1 t)
[j2 + (1 + 1) := (⌊[]⌋⇩N⇩L, 1),
j2 + (1 + 2) := (⌊clause_n (map (rename σ) (n_clause (nφ ! t)))⌋⇩N⇩L, 1)]"
using jk tps0 tpsL1_def tpsL2_def by (simp add: numeral_3_eq_3)
then show "tpsL2 t = (tpsL1 t)
[j2 + 1 + 1 := (⌊[]⌋⇩N⇩L, 1),
j2 + 1 + 2 := (⌊clause_n (map (rename σ) (n_clause (nφ ! t)))⌋⇩N⇩L, 1)]"
by (metis add.assoc)
show "ttt = 12 + 2 * nllength (nφ ! t) +
(11 + 64 * nllength (nφ ! t) * (3 + (nllength σ)⇧2))"
using assms(1) by simp
qed

definition tpsL3 :: "nat ⇒ tape list" where
"tpsL3 t ≡ tps0
[j1 := nlltape' nφ (Suc t),
j2 := nlltape
(formula_n (take t (relabel σ φ)) @ [clause_n (map (rename σ) (n_clause (nφ ! t)))]),
j2 + 2 := (⌊[]⌋⇩N⇩L, 1),
j2 + 3 := (⌊clause_n (map (rename σ) (n_clause (nφ ! t)))⌋⇩N⇩L, 1)]"

lemma tmL3 [transforms_intros]:
assumes "ttt = 29 + 2 * nllength (nφ ! t) +
64 * nllength (nφ ! t) * (3 + (nllength σ)⇧2) +
2 * nllength (clause_n (map (rename σ) (n_clause (nφ ! t))))"
and "t < length φ"
shows "transforms tmL3 (tpsL t) ttt (tpsL3 t)"
unfolding tmL3_def
proof (tform tps: assms(2) tps0 tpsL2_def jk)
show "tpsL3 t = (tpsL2 t)
[j2 := nlltape (formula_n (take t (relabel σ φ)) @ [clause_n (map (rename σ) (n_clause (nφ ! t)))])]"
unfolding tpsL3_def tpsL2_def by (simp add: list_update_swap_less[of j2])
show "ttt = 23 + 2 * nllength (nφ ! t) + 64 * nllength (nφ ! t) * (3 + (nllength σ)⇧2) +
(7 + nlllength (formula_n (take t (relabel σ φ))) - Suc (nlllength (formula_n (take t (relabel σ φ)))) +
2 * nllength (clause_n (map (rename σ) (n_clause (nφ ! t)))))"
using assms(1) by simp
qed

definition tpsL4 :: "nat ⇒ tape list" where
"tpsL4 t ≡ tps0
[j1 := nlltape' nφ (Suc t),
j2 := nlltape
(formula_n (take t (relabel σ φ)) @ [clause_n (map (rename σ) (n_clause (nφ ! t)))]),
j2 + 2 := (⌊[]⌋⇩N⇩L, 1)]"

lemma tmL4:
assumes "ttt = 36 + 2 * nllength (nφ ! t) +
64 * nllength (nφ ! t) * (3 + (nllength σ)⇧2) +
4 * nllength (clause_n (map (rename σ) (n_clause (nφ ! t))))"
and "t < length φ"
shows "transforms tmL4 (tpsL t) ttt (tpsL4 t)"
unfolding tmL4_def
proof (tform tps: assms(2) tps0 tpsL3_def jk)
let ?zs = "numlist (clause_n (map (rename σ) (n_clause (nφ ! t))))"
show "tpsL3 t ::: (j2 + 3) = ⌊?zs⌋"
using tpsL3_def nlcontents_def jk by simp
show "proper_symbols ?zs"
using proper_symbols_numlist by simp
have *: "j1 ≠ j2 + 3"
using jk by simp
have "⌊[]⌋ = ⌊[]⌋⇩N⇩L"
using nlcontents_def numlist_Nil by simp
then show "tpsL4 t = (tpsL3 t)[j2 + 3 := (⌊[]⌋, 1)]"
using tpsL3_def tpsL4_def tps0 jk list_update_id[of tps0 "j2+3"]
by (simp add: list_update_swap[OF *] list_update_swap[of _ "j2 + 3"])
show "ttt = 29 + 2 * nllength (nφ ! t) + 64 * nllength (nφ ! t) * (3 + (nllength σ)⇧2) +
2 * nllength (clause_n (map (rename σ) (n_clause (nφ ! t)))) +
(tpsL3 t :#: (j2 + 3) + 2 * length (numlist (clause_n (map (rename σ) (n_clause (nφ ! t))))) + 6)"
using assms(1) tpsL3_def jk nllength_def by simp
qed

lemma nllength_1:
assumes "t < length φ"
shows "nllength (nφ ! t) ≤ nlllength nφ"
using assms formula_n_def nlllength_take by (metis le_less_linear length_map less_trans not_add_less2)

lemma nllength_2:
assumes "t < length φ"
shows "nllength (clause_n (map (rename σ) (n_clause (nφ ! t)))) ≤ nlllength (formula_n (relabel σ φ))"
(is "?l ≤ ?r")
proof -
have "?l = nllength (clause_n (map (rename σ) (φ ! t)))"
using assms by (simp add: formula_n_def n_clause_n)
moreover have "clause_n (map (rename σ) (φ ! t)) ∈ set (formula_n (relabel σ φ))"
using assms formula_n_def relabel_def by simp
ultimately show ?thesis
using member_le_nlllength_1 by fastforce
qed

definition "tpsL4' t ≡ tps0
[j1 := nlltape' nφ (Suc t),
j2 := nlltape (formula_n (take (Suc t) (relabel σ φ)))]"

lemma tpsL4:
assumes "t < length φ"
shows "tpsL4 t = tpsL4' t"
proof -
have "formula_n (take t (relabel σ φ)) @ [clause_n (map (rename σ) (n_clause (nφ ! t)))] =
formula_n (take (Suc t) (relabel σ φ))"
using assms formula_n_def relabel_def by (simp add: n_clause_n take_Suc_conv_app_nth)
then show ?thesis
using tpsL4_def tpsL4'_def jk tps0
by (smt (verit, del_insts) Suc_1 add_Suc_right add_cancel_left_right less_SucI
list_update_id list_update_swap not_less_eq numeral_1_eq_Suc_0 numeral_One)
qed

lemma tpsL4'_eq_tpsL: "tpsL4' t = tpsL (Suc t)"
using tpsL_def tpsL4'_def by simp

lemma tmL4' [transforms_intros]:
assumes "ttt = 36 + 65 * nlllength nφ * (3 + (nllength σ)⇧2) + 4 * nlllength (formula_n (relabel σ φ))"
and "t < length φ"
shows "transforms tmL4 (tpsL t) ttt (tpsL (Suc t))"
proof -
let ?ttt = "36 + 2 * nllength (nφ ! t) +
64 * nllength (nφ ! t) * (3 + (nllength σ)⇧2) +
4 * nllength (clause_n (map (rename σ) (n_clause (nφ ! t))))"
have "?ttt ≤ 36 + 2 * nlllength nφ +
64 * nlllength nφ * (3 + (nllength σ)⇧2) +
4 * nllength (clause_n (map (rename σ) (n_clause (nφ ! t))))"
using nllength_1 assms(2) add_le_mono add_le_mono1 mult_le_mono1 mult_le_mono2 nat_add_left_cancel_le
by metis
also have "... ≤ 36 + 2 * nlllength nφ +
64 * nlllength nφ * (3 + (nllength σ)⇧2) +
4 * nlllength (formula_n (relabel σ φ))"
using nllength_2 assms(2) by simp
also have "... ≤ 36 + 65 * nlllength nφ * (3 + (nllength σ)⇧2) + 4 * nlllength (formula_n (relabel σ φ))"
by simp
finally have "?ttt ≤ 36 + 65 * nlllength nφ * (3 + (nllength σ)⇧2) + 4 * nlllength (formula_n (relabel σ φ))" .
then have "transforms tmL4 (tpsL t) ttt (tpsL4 t)"
using assms tmL4 transforms_monotone by blast
then show ?thesis
using assms(2) tpsL4'_eq_tpsL tpsL4 by simp
qed

lemma tmL:
assumes "ttt = length φ * (38 + 65 * nlllength nφ * (3 + (nllength σ)⇧2) + 4 * nlllength (formula_n (relabel σ φ))) + 1"
shows "transforms tmL (tpsL 0) ttt (tpsL (length φ))"
unfolding tmL_def
proof (tform)
let ?t = "36 + 65 * nlllength nφ * (3 + (nllength σ)⇧2) + 4 * nlllength (formula_n (relabel σ φ))"
show "¬ read (tpsL (length φ)) ! j1 ≠ □"
proof -
have "tpsL (length φ) ! j1 = nlltape' nφ (length nφ)"
using tpsL_def jk formula_n_def by simp
then show ?thesis
using nlltape'_tape_read[of nφ "length nφ"] tapes_at_read'[of j1 "tpsL (length φ)"] tpsL_def jk
by simp
qed
show "read (tpsL t) ! j1 ≠ □" if "t < length φ" for t
proof -
have "tpsL t ! j1 = nlltape' nφ t"
using tpsL_def jk by simp
then show ?thesis
using that formula_n_def nlltape'_tape_read[of nφ t] tapes_at_read'[of j1 "tpsL t"] tpsL_def jk
by simp
qed
show "length φ * (?t + 2) + 1 ≤ ttt"
using assms(1) by simp
qed

lemma tmL' [transforms_intros]:
assumes "ttt = 107 * nlllength nφ ^ 2 * (3 + nllength σ ^ 2) + 1"
shows "transforms tmL (tpsL 0) ttt (tpsL (length φ))"
proof -
let ?ttt = "length φ * (38 + 65 * nlllength nφ * (3 + (nllength σ)⇧2) + 4 * nlllength (formula_n (relabel σ φ))) + 1"
have "?ttt ≤ length φ * (38 + 65 * nlllength nφ * (3 + (nllength σ)⇧2) + 4 * (Suc (nllength σ) * nlllength nφ)) + 1"
using nlllength_relabel_variables variables by fastforce
also have "... ≤ length φ * (38 + 65 * nlllength nφ * (3 + (nllength σ)⇧2) + 4 * ((3 + nllength σ) * nlllength nφ)) + 1"
proof -
have "Suc (nllength σ) ≤ 3 + nllength σ"
by simp
then show ?thesis
using add_le_mono le_refl mult_le_mono by presburger
qed
also have "... ≤ length φ * (38 + 65 * nlllength nφ * (3 + (nllength σ)⇧2) + 4 * ((3 + nllength σ ^ 2) * nlllength nφ)) + 1"
using linear_le_pow by simp
also have "... = length φ * (38 + 69 * nlllength nφ * (3 + (nllength σ)⇧2)) + 1"
by simp
also have "... ≤ nlllength nφ * (38 + 69 * nlllength nφ * (3 + (nllength σ)⇧2)) + 1"
using length_le_nlllength formula_n_def by (metis add_mono_thms_linordered_semiring(3) length_map mult_le_mono1)
also have "... = 38 * nlllength nφ + (69 * nlllength nφ ^ 2 * (3 + (nllength σ)⇧2)) + 1"
by algebra
also have "... ≤ 38 * nlllength nφ ^ 2 * (3 + nllength σ ^ 2) + (69 * nlllength nφ ^ 2 * (3 + (nllength σ)⇧2)) + 1"
proof -
have "nlllength nφ ≤ nlllength nφ ^ 2 * (3 + nllength σ ^ 2)"
using linear_le_pow by (metis One_nat_def Suc_leI add_gr_0 mult_le_mono nat_mult_1_right zero_less_numeral)
then show ?thesis
by simp
qed
also have "... = 107 * nlllength nφ ^ 2 * (3 + nllength σ ^ 2) + 1"
by simp
finally have "?ttt ≤ 107 * nlllength nφ ^ 2 * (3 + nllength σ ^ 2) + 1" .
then show ?thesis
using tmL assms transforms_monotone by blast
qed

definition tps1 :: "tape list" where
"tps1 ≡ tps0
[j1 := nlltape' nφ (length φ),
j2 := nlltape (formula_n (relabel σ φ))]"

lemma tps1_eq_tpsL: "tps1 = tpsL (length φ)"
using tps1_def tpsL_def jk tps0 relabel_def by simp

definition "tps2 ≡ tps0
[j2 := nlltape (formula_n (relabel σ φ))]"

lemma tm2 [transforms_intros]:
assumes "ttt = Suc (107 * (nlllength nφ)⇧2 * (3 + (nllength σ)⇧2)) +
Suc (Suc (Suc (nlllength nφ)))"
shows "transforms tm2 (tpsL 0) ttt tps2"
unfolding tm2_def
proof (tform tps: tps0 tpsL_def tps1_def jk)
have *: "tpsL (length φ) ! j1 = nlltape' nφ (length φ)"
using tpsL_def jk by simp
then show "clean_tape (tpsL (length φ) ! j1)"
using clean_tape_nllcontents by simp
have "tpsL (length φ) ! j1 |#=| 1 = nlltape' nφ 0"
using * by simp
then show "tps2 = (tpsL (length φ))[j1 := tpsL (length φ) ! j1 |#=| 1]"
using tps0 jk tps2_def tps1_eq_tpsL tps1_def
by (metis (no_types, lifting) One_nat_def list_update_id list_update_overwrite list_update_swap_less nlllength_Nil take0)
show "ttt = 107 * (nlllength nφ)⇧2 * (3 + (nllength σ)⇧2) + 1 +
(tpsL (length φ) :#: j1 + 2)"
using assms tpsL_def jk formula_n_def by simp
qed

definition "tps3 ≡ tps0
[j2 := nlltape' (formula_n (relabel σ φ)) 0]"

lemma tm3:
assumes "ttt = 7 + (107 * (nlllength nφ)⇧2 * (3 + (nllength σ)⇧2)) +
nlllength nφ + nlllength (formula_n (relabel σ φ))"
shows "transforms tm3 (tpsL 0) ttt tps3"
unfolding tm3_def
proof (tform tps: assms tps0 tps2_def tps3_def jk)
show "clean_tape (tps2 ! j2)"
using tps2_def jk clean_tape_nllcontents by simp
qed

lemma tm3' [transforms_intros]:
assumes "ttt = 7 + (108 * (nlllength nφ)⇧2 * (3 + (nllength σ)⇧2))"
shows "transforms tm3 tps0 ttt tps3"
proof -
let ?ttt = "7 + (107 * (nlllength nφ)⇧2 * (3 + (nllength σ)⇧2)) +
nlllength nφ + nlllength (formula_n (relabel σ φ))"
have "?ttt ≤ 7 + (107 * (nlllength nφ)⇧2 * (3 + (nllength σ)⇧2)) +
nlllength nφ + Suc (nllength σ) * nlllength nφ"
using variables nlllength_relabel_variables by simp
also have "... = 7 + (107 * (nlllength nφ)⇧2 * (3 + (nllength σ)⇧2)) +
(2 + nllength σ) * nlllength nφ"
by simp
also have "... ≤ 7 + (107 * (nlllength nφ)⇧2 * (3 + (nllength σ)⇧2)) +
(2 + nllength σ ^ 2) * nlllength nφ"
using linear_le_pow by simp
also have "... ≤ 7 + (107 * (nlllength nφ)⇧2 * (3 + (nllength σ)⇧2)) + (3 + nllength σ ^ 2) * nlllength nφ"
by (metis add_2_eq_Suc add_Suc_shift add_mono_thms_linordered_semiring(2) le_add2 mult.commute mult_le_mono2 numeral_3_eq_3)
also have "... ≤ 7 + (107 * (nlllength nφ)⇧2 * (3 + (nllength σ)⇧2)) +
(3 + nllength σ ^ 2) * nlllength nφ ^ 2"
using linear_le_pow by simp
also have "... = 7 + (108 * (nlllength nφ)⇧2 * (3 + (nllength σ)⇧2))"
by simp
finally have "?ttt ≤ 7 + (108 * (nlllength nφ)⇧2 * (3 + (nllength σ)⇧2))" .
then show ?thesis
using tm3 assms tpsL_eq_tps0 transforms_monotone by simp
qed

end  (* context tps0 *)

end  (* locale turing_machine_relabel *)

lemma transforms_tm_relabelI [transforms_intros]:
fixes j1 j2 :: tapeidx
fixes tps tps' :: "tape list" and ttt k :: nat and σ :: "nat list" and φ :: formula
assumes "0 < j1" and "j1 < j2" and "j2 + 5 < k" and "length tps = k"
and "variables φ ⊆ {..<length σ}"
assumes
"tps ! j1 = (⌊formula_n φ⌋⇩N⇩L⇩L, 1)"
"tps ! j2 = (⌊[]⌋⇩N⇩L⇩L, 1)"
"tps ! (j2 + 1) = (⌊σ⌋⇩N⇩L, 1)"
"tps ! (j2 + 2) = (⌊[]⌋⇩N⇩L, 1)"
"tps ! (j2 + 3) = (⌊[]⌋⇩N⇩L, 1)"
"tps ! (j2 + 4) = (⌊0⌋⇩N, 1)"
"tps ! (j2 + 5) = (⌊0⌋⇩N, 1)"
assumes "tps' = tps
[j2 := nlltape' (formula_n (relabel σ φ)) 0]"
assumes "ttt = 7 + (108 * (nlllength (formula_n φ))⇧2 * (3 + (nllength σ)⇧2))"
shows "transforms (tm_relabel j1 j2) tps ttt tps'"
proof -
interpret loc: turing_machine_relabel j1 j2 .
show ?thesis
using assms loc.tm3_eq_tm_relabel loc.tm3' loc.tps3_def by simp
qed

section ‹Listing the head positions of a Turing machine›

text ‹
The formulas $\chi_t$ used for $\Phi_9$ require the functions $\inputpos$ and
$\prev$, or more precisely the substitutions $\rho_t$ and $\rho'_t$ do.

In this section we build a TM that simulates a two-tape TM $M$ on some input
until it halts. During the simulation it creates two lists: one with the
sequence of head positions on $M$'s input tape and one with the sequence of head
positions on $M$'s output tape. The first list directly provides $\inputpos$;
the second list allows the computation of $\prev$ using the TM @{const tm_prev}.
›

subsection ‹Simulating and logging head movements›

text ‹
At the core of the simulation is the following Turing command. It interprets the
tapes $j + 7$ and $j + 8$ as input tape and output tape of a two-tape Turing
machine $M$ and the symbol in the first cell of tape $j + 6$ as the state of
$M$. It then applies the actions of $M$ in this configuration to the tapes $j + 7$ and $j + 8$ and adapts the state on tape $j + 6$ accordingly. On top of that
it writes (logs'') to tape $j$ the direction in which $M$'s input tape head
has moved and to tape $j + 3$ the direction in which $M$'s work tape head has
moved.

The head movement directions are encoded by the symbols $\Box$,
$\triangleright$, and \textbf{0} for Left, Stay, and Right, respectively.

The command is parameterized by the TM $M$ and its alphabet size $G$ (and as
usual the tape index $j$). The command does nothing if the state on tape $j + 6$
is the halting state or if the symbol read from the simulated tape $j + 7$ or $j + 8$ is outside the alphabet $G$.

\null
›

definition direction_to_symbol :: "direction ⇒ symbol" where
"direction_to_symbol d ≡ (case d of Left ⇒ □ | Stay ⇒ ▹ | Right ⇒ 𝟬)"

lemma direction_to_symbol_less: "direction_to_symbol d < 3"
using direction_to_symbol_def by (cases d) simp_all

definition cmd_simulog :: "nat ⇒ machine ⇒ tapeidx ⇒ command" where
"cmd_simulog G M j rs ≡
(1,
if rs ! (j + 6) ≥ length M ∨ rs ! (j + 7) ≥ G ∨ rs ! (j + 8) ≥ G
then map (λz. (z, Stay)) rs
else
map (λi. let sas = (M ! (rs ! (j + 6))) [rs ! (j + 7), rs ! (j + 8)] in
if i = j then (direction_to_symbol (sas [~] 0), Stay)
else if i = j + 3 then (direction_to_symbol (sas [~] 1), Stay)
else if i = j + 6 then (fst sas, Stay)
else if i = j + 7 then sas [!] 0
else if i = j + 8 then sas [!] 1
else (rs ! i, Stay))
[0..<length rs])"

lemma turing_command_cmd_simulog:
fixes G H :: nat
assumes "turing_machine 2 G M" and "k ≥ j + 9" and "j > 0" and "H ≥ Suc (length M)" and "H ≥ G"
shows "turing_command k 1 H (cmd_simulog G M j)"
proof
show "⋀gs. length gs = k ⟹ length ([!!] cmd_simulog G M j gs) = length gs"
using cmd_simulog_def by simp
have G: "H ≥ 4"
using assms(1,5) turing_machine_def by simp
show "cmd_simulog G M j rs [.] i < H"
if "length rs = k" and "(⋀i. i < length rs ⟹ rs ! i < H)" and "i < length rs"
for rs i
proof (cases "rs ! (j + 6) ≥ length M ∨ rs ! (j + 7) ≥ G ∨ rs ! (j + 8) ≥ G")
case True
then show ?thesis
using assms that cmd_simulog_def by simp
next
case False
then have inbounds: "rs ! (j + 6) < length M"
by simp
let ?cmd = "M ! (rs ! (j + 6))"
let ?gs = "[rs ! (j + 7), rs ! (j + 8)]"
let ?sas = "?cmd ?gs"
have lensas: "length (snd ?sas) = 2"
using assms(1) inbounds turing_commandD(1)
by (metis length_Cons list.size(3) numeral_2_eq_2 turing_machineD(3))
consider
"i = j"
| "i = j + 3"
| "i = j + 6"
| "i = j + 7"
| "i = j + 8"
| "i ≠ j ∧ i ≠ j + 3 ∧ i ≠ j + 6 ∧ i ≠ j + 7 ∧ i ≠ j + 8"
by linarith
then show ?thesis
proof (cases)
case 1
then have "cmd_simulog G M j rs [!] i = (direction_to_symbol (?sas [~] 0), Stay)"
using cmd_simulog_def False that by simp
then have "cmd_simulog G M j rs [.] i < 3"
using direction_to_symbol_less by simp
then show ?thesis
using G by simp
next
case 2
then have "cmd_simulog G M j rs [!] i = (direction_to_symbol (?sas [~] 1), Stay)"
using cmd_simulog_def False that by simp
then have "cmd_simulog G M j rs [.] i < 3"
using direction_to_symbol_less by simp
then show ?thesis
using G by simp
next
case 3
then have "cmd_simulog G M j rs [!] i = (fst ?sas, Stay)"
using cmd_simulog_def False that by simp
then have "cmd_simulog G M j rs [.] i ≤ length M"
using assms inbounds turing_commandD(4) turing_machineD(3)
by (metis One_nat_def Suc_1 fst_conv length_Cons list.size(3))
then show ?thesis
using assms(4) by simp
next
case 4
then have "cmd_simulog G M j rs [!] i = ?sas [!] 0"
using cmd_simulog_def False that by simp
then show ?thesis
using 4 assms inbounds turing_machine_def that lensas turing_commandD(3)
by (metis One_nat_def Suc_1 length_Cons list.size(3) nth_Cons_0 nth_mem zero_less_numeral)
next
case 5
then have *: "cmd_simulog G M j rs [!] i = ?sas [!] 1"
using cmd_simulog_def False that by simp
have "turing_command 2 (length M) G ?cmd"
using assms(1) inbounds turing_machine_def by simp
moreover have "symbols_lt G ?gs"
using False less_2_cases_iff numeral_2_eq_2 by simp
ultimately have "?sas [.] 1 < G"
using turing_commandD(2) by simp
then show ?thesis
using assms * by simp
next
case 6
then have "cmd_simulog G M j rs [!] i = (rs ! i, Stay)"
using cmd_simulog_def False that(3) by simp
then show ?thesis
using that by simp
qed
qed
show "cmd_simulog G M j rs [.] 0 = rs ! 0" if "length rs = k" and "0 < k" for rs
proof (cases "rs ! (j + 6) ≥ length M ∨ rs ! (j + 7) ≥ G ∨ rs ! (j + 8) ≥ G")
case True
then show ?thesis
using assms that cmd_simulog_def by simp
next
case False
then show ?thesis
using assms that cmd_simulog_def by simp
qed
show "⋀gs. length gs = k ⟹ [*] (cmd_simulog G M j gs) ≤ 1"
using cmd_simulog_def by simp
qed

text ‹
The logging Turing machine consists only of the logging command.
›

definition tm_simulog :: "nat ⇒ machine ⇒ tapeidx ⇒ machine" where
"tm_simulog G M j ≡ [cmd_simulog G M j]"

lemma tm_simulog_tm:
fixes H :: nat
assumes "turing_machine 2 G M" and "k ≥ j + 9" and "j > 0" and "H