Theory Sat_TM_CNF
section ‹Turing machines for the parts of $\Phi$\label{s:tmcnf}›
theory Sat_TM_CNF
imports Aux_TM_Reducing
begin
text ‹
In this section we build Turing machines for all parts $\Phi_0,\dots,\Phi_9$ of
the CNF formula $\Phi$. Some of them ($\Phi_0$, $\Phi_1$, $\Phi_2$, and
$\Phi_8$) are just fixed-length sequences of $\Psi$ formulas constructible by
fixed-length sequences of @{const tm_Psigamma} machines. Others ($\Phi_3$,
$\Phi_4$, $\Phi_5$, $\Phi_6$) are variable-length and require looping over a
@{const tm_Psigamma} machine. The TM for $\Phi_7$ is a loop over @{const
tm_Upsilongamma}. Lastly, the TM for $\Phi_9$ is a loop over a TM that generates
the formulas $\chi_t$.
Ideally we would want to prove the semantics of the TMs inside the locale
@{locale reduction_sat}, in which $\Phi$ was defined. However, we use locales to
prove the semantics of TMs, and locales cannot be nested. For this reason we
have to define the TMs on the theory level and prove their semantics there, too,
just as we have done with all TMs until now. In the next chapter the semantics
lemmas will be transferred to the locale @{locale reduction_sat}.
Unlike most TMs so far, the TMs in this section are not meant to be reusable
but serve a special purpose, namely to be combined into one large TM computing
$\Phi$. For this reason the TMs are somewhat peculiar. For example, they write
their output to the fixed tape~$1$ rather than having a parameter for the output
tape. They also often expect the tapes to be initialized in a very special way.
Moreover, the TMs often leave the work tapes in a ``dirty'' state with remnants
of intermediate calculations. The combined TM for all of $\Phi$ will simply
allocate a new batch of work tapes for every individual TM.
›
subsection ‹A Turing machine for $\Phi_0$›
text ‹
The next Turing machine expects a number $i$ on tape $j$ and a number $H$ on
tape $j + 1$ and outputs to tape $1$ the formula $\Psi([i\dots H, (i+1)\dots H),
1) \land \Psi([(i+1)\dots H, (i+2)\dots H), 1) \land \Psi([(i+2)\dots H,
(i+3)\dots H), 0)$, which is just $\Phi_0$ for suitable values of $i$ and $H$.
›
definition tm_PHI0 :: "tapeidx ⇒ machine" where
"tm_PHI0 j ≡
tm_setn (j + 2) 1 ;;
tm_Psigamma j ;;
tm_extendl_erase 1 (j + 6) ;;
tm_incr j ;;
tm_Psigamma j ;;
tm_extendl_erase 1 (j + 6) ;;
tm_incr j ;;
tm_setn (j + 2) 0 ;;
tm_Psigamma j ;;
tm_extendl 1 (j + 6)"
lemma tm_PHI0_tm:
assumes "0 < j" and "j + 8 < k" and "G ≥ 6"
shows "turing_machine k G (tm_PHI0 j)"
unfolding tm_PHI0_def
using assms tm_Psigamma_tm tm_extendl_tm tm_erase_cr_tm tm_times2_tm tm_incr_tm tm_setn_tm tm_cr_tm
tm_extendl_erase_tm
by simp
locale turing_machine_PHI0 =
fixes j :: tapeidx
begin
definition "tm1 ≡ tm_setn (j + 2) 1"
definition "tm2 ≡ tm1 ;; tm_Psigamma j"
definition "tm3 ≡ tm2 ;; tm_extendl_erase 1 (j + 6)"
definition "tm5 ≡ tm3 ;; tm_incr j"
definition "tm6 ≡ tm5 ;; tm_Psigamma j"
definition "tm7 ≡ tm6 ;; tm_extendl_erase 1 (j + 6)"
definition "tm9 ≡ tm7 ;; tm_incr j"
definition "tm10 ≡ tm9 ;; tm_setn (j + 2) 0"
definition "tm11 ≡ tm10 ;; tm_Psigamma j"
definition "tm12 ≡ tm11 ;; tm_extendl 1 (j + 6)"
lemma tm12_eq_tm_PHI0: "tm12 = tm_PHI0 j"
using tm12_def tm11_def tm10_def tm9_def tm7_def tm6_def tm5_def
using tm3_def tm2_def tm1_def tm_PHI0_def
by simp
context
fixes tps0 :: "tape list" and k idx H :: nat
assumes jk: "length tps0 = k" "1 < j" "j + 8 < k"
and H: "H ≥ 3"
assumes tps0:
"tps0 ! 1 = (⌊[]⌋, 1)"
"tps0 ! j = (⌊idx⌋⇩N, 1)"
"tps0 ! (j + 1) = (⌊H⌋⇩N, 1)"
"tps0 ! (j + 2) = (⌊[]⌋, 1)"
"tps0 ! (j + 3) = (⌊[]⌋, 1)"
"tps0 ! (j + 4) = (⌊[]⌋, 1)"
"tps0 ! (j + 5) = (⌊[]⌋, 1)"
"tps0 ! (j + 6) = (⌊[]⌋, 1)"
"tps0 ! (j + 7) = (⌊[]⌋, 1)"
"tps0 ! (j + 8) = (⌊[]⌋, 1)"
begin
definition "tps1 ≡ tps0
[j + 2 := (⌊1⌋⇩N, 1)]"
lemma tm1 [transforms_intros]:
assumes "ttt = 12"
shows "transforms tm1 tps0 ttt tps1"
unfolding tm1_def
proof (tform tps: tps0 tps1_def jk)
show "tps0 ! (j + 2) = (⌊0⌋⇩N, 1)"
using tps0 jk canrepr_0 by simp
show "ttt = 10 + 2 * nlength 0 + 2 * nlength 1"
using assms canrepr_1 by simp
qed
definition "tps2 ≡ tps0
[j + 2 := (⌊1⌋⇩N, 1),
j + 6 := (⌊nll_Psi (idx * H) H 1⌋⇩N⇩L⇩L, 1)]"
lemma tm2 [transforms_intros]:
assumes "ttt = 12 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2"
shows "transforms tm2 tps0 ttt tps2"
unfolding tm2_def by (tform tps: assms tps0 H tps1_def tps2_def jk)
definition "tps3 ≡ tps0
[j + 2 := (⌊1⌋⇩N, 1),
1 := nlltape (nll_Psi (idx * H) H (Suc 0)),
j + 6 := (⌊[]⌋, 1)]"
lemma tm3 [transforms_intros]:
assumes "ttt = 23 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 +
4 * nlllength (nll_Psi (idx * H) H (Suc 0))"
shows "transforms tm3 tps0 ttt tps3"
unfolding tm3_def
proof (tform tps: tps0 H tps2_def tps3_def jk time: assms)
show "tps2 ! 1 = nlltape []"
using tps2_def jk nllcontents_Nil tps0 by simp
show "tps3 = tps2
[1 := nlltape ([] @ nll_Psi (idx * H) H (Suc 0)),
j + 6 := (⌊[]⌋, 1)]"
unfolding tps3_def tps2_def using jk by (simp add: list_update_swap)
qed
definition "tps5 ≡ tps0
[j + 2 := (⌊1⌋⇩N, 1),
1 := nlltape (nll_Psi (idx * H) H (Suc 0)),
j + 6 := (⌊[]⌋, 1),
j := (⌊Suc idx⌋⇩N, 1)]"
lemma tm5 [transforms_intros]:
assumes "ttt = 28 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 +
4 * nlllength (nll_Psi (idx * H) H 1) +
2 * nlength idx"
shows "transforms tm5 tps0 ttt tps5"
unfolding tm5_def by (tform tps: tps0 H tps3_def tps5_def jk time: assms)
definition "tps6 ≡ tps0
[j := (⌊Suc idx⌋⇩N, 1),
j + 2 := (⌊1⌋⇩N, 1),
j + 6 := (⌊nll_Psi (Suc idx * H) H (Suc 0)⌋⇩N⇩L⇩L, 1),
1 := nlltape (nll_Psi (idx * H) H 1)]"
lemma tm6 [transforms_intros]:
assumes "ttt = 28 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 +
4 * nlllength (nll_Psi (idx * H) H 1) + 2 * nlength idx +
1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧2"
shows "transforms tm6 tps0 ttt tps6"
unfolding tm6_def
proof (tform tps: tps0 H tps5_def tps6_def jk time: assms)
show "tps6 = tps5[j + 6 := (⌊nll_Psi (Suc idx * H) H (Suc 0)⌋⇩N⇩L⇩L, 1)]"
unfolding tps5_def tps6_def using jk
by (simp add: list_update_swap[of j] list_update_swap[of _ "j + 6"])
qed
definition "tps7 ≡ tps0
[j := (⌊Suc idx⌋⇩N, 1),
j + 2 := (⌊1⌋⇩N, 1),
j + 6 := (⌊[]⌋, 1),
1 := nlltape (nll_Psi (idx * H) H 1 @ nll_Psi (H + idx * H) H 1)]"
lemma tm7 [transforms_intros]:
assumes "ttt = 39 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 +
4 * nlllength (nll_Psi (idx * H) H 1) +
2 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧2 +
4 * nlllength (nll_Psi (H + idx * H) H 1)"
shows "transforms tm7 tps0 ttt tps7"
unfolding tm7_def by (tform tps: assms tps6_def tps7_def jk)
definition "tps9 ≡ tps0
[j := (⌊Suc (Suc idx)⌋⇩N, 1),
j + 2 := (⌊1⌋⇩N, 1),
j + 6 := (⌊[]⌋, 1),
1 := nlltape (nll_Psi (idx * H) H 1 @ nll_Psi (H + idx * H) H 1)]"
lemma tm9 [transforms_intros]:
assumes "ttt = 44 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 +
4 * nlllength (nll_Psi (idx * H) H 1) + 2 * nlength idx +
1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧2 + 4 * nlllength (nll_Psi (H + idx * H) H 1) +
2 * nlength (Suc idx)"
shows "transforms tm9 tps0 ttt tps9"
unfolding tm9_def
proof (tform tps: tps0 H tps7_def tps9_def jk time: assms)
show "tps9 = tps7[j := (⌊Suc (Suc idx)⌋⇩N, 1)]"
using tps9_def tps7_def jk by (simp add: list_update_swap)
qed
definition "tps10 ≡ tps0
[j := (⌊Suc (Suc idx)⌋⇩N, 1),
j + 2 := (⌊0⌋⇩N, 1),
j + 6 := (⌊[]⌋, 1),
1 := nlltape (nll_Psi (idx * H) H 1 @ nll_Psi (H + idx * H) H 1)]"
lemma tm10 [transforms_intros]:
assumes "ttt = 56 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 +
4 * nlllength (nll_Psi (idx * H) H 1) + 2 * nlength idx +
1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧2 + 4 * nlllength (nll_Psi (H + idx * H) H 1) +
2 * nlength (Suc idx)"
shows "transforms tm10 tps0 ttt tps10"
unfolding tm10_def
proof (tform tps: tps0 H tps9_def tps10_def jk)
show "ttt = 44 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 +
4 * nlllength (nll_Psi (idx * H) H 1) + 2 * nlength idx +
1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧2 + 4 * nlllength (nll_Psi (H + idx * H) H 1) +
2 * nlength (Suc idx) + (10 + 2 * nlength (Suc 0) + 2 * nlength 0) "
using assms canrepr_1 by simp
qed
definition "tps11 ≡ tps0
[j := (⌊Suc (Suc idx)⌋⇩N, 1),
j + 2 := (⌊0⌋⇩N, 1),
j + 6 := (⌊nll_Psi (Suc (Suc idx) * H) H 0⌋⇩N⇩L⇩L, 1),
1 := nlltape (nll_Psi (idx * H) H 1 @ nll_Psi (H + idx * H) H 1)]"
lemma tm11 [transforms_intros]:
assumes "ttt = 56 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 +
4 * nlllength (nll_Psi (idx * H) H 1) + 2 * nlength idx +
1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧2 + 4 * nlllength (nll_Psi (H + idx * H) H 1) +
2 * nlength (Suc idx) + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧2"
shows "transforms tm11 tps0 ttt tps11"
unfolding tm11_def by (tform tps: tps0 H tps10_def tps11_def jk time: assms)
definition "tps12 ≡ tps0
[j := (⌊Suc (Suc idx)⌋⇩N, 1),
j + 2 := (⌊0⌋⇩N, 1),
j + 6 := (⌊nll_Psi (Suc (Suc idx) * H) H 0⌋⇩N⇩L⇩L, 1),
1 := nlltape (nll_Psi (idx * H) H 1 @ nll_Psi (H + idx * H) H 1 @ nll_Psi (Suc (Suc idx) * H) H 0)]"
lemma tm12:
assumes "ttt = 60 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 +
4 * nlllength (nll_Psi (idx * H) H 1) + 2 * nlength idx +
1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧2 + 4 * nlllength (nll_Psi (H + idx * H) H 1) +
2 * nlength (Suc idx) + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧2 +
2 * nlllength (nll_Psi (H + (H + idx * H)) H 0)"
shows "transforms tm12 tps0 ttt tps12"
unfolding tm12_def by (tform tps: tps11_def tps12_def jk assms)
lemma tm12':
assumes "ttt = 5627 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧2"
shows "transforms tm12 tps0 ttt tps12"
proof -
let ?ttt = "60 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 +
4 * nlllength (nll_Psi (idx * H) H 1) + 2 * nlength idx +
1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧2 + 4 * nlllength (nll_Psi (H + idx * H) H 1) +
2 * nlength (Suc idx) + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧2 +
2 * nlllength (nll_Psi (H + (H + idx * H)) H 0)"
have "?ttt ≤ 60 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 +
4 * H * (3 + nlength (3 * H + idx * H)) + 2 * nlength idx +
1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧2 + 4 * nlllength (nll_Psi (H + idx * H) H 1) +
2 * nlength (Suc idx) + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧2 +
2 * nlllength (nll_Psi (H + (H + idx * H)) H 0)"
using nlllength_nll_Psi_le'[of "idx * H" "2 * H + idx * H" "H"] by simp
also have "... ≤ 60 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 +
4 * H * (3 + nlength (3 * H + idx * H)) + 2 * nlength idx +
1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧2 + 4 * H * (3 + nlength (3 * H + idx * H)) +
2 * nlength (Suc idx) + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧2 +
2 * nlllength (nll_Psi (H + (H + idx * H)) H 0)"
using nlllength_nll_Psi_le'[of "H + idx * H" "2 * H + idx * H" "H"] by simp
also have "... ≤ 60 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 +
4 * H * (3 + nlength (3 * H + idx * H)) + 2 * nlength idx +
1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧2 + 4 * H * (3 + nlength (3 * H + idx * H)) +
2 * nlength (Suc idx) + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧2 +
2 * H * (3 + nlength (3 * H + idx * H))"
using nlllength_nll_Psi_le'[of "H + (H + idx * H)" "2 * H + idx * H" "H"] by simp
also have "... = 60 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 +
10 * H * (3 + nlength (3 * H + idx * H)) + 2 * nlength idx +
1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧2 + 2 * nlength (Suc idx) +
1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧2"
by simp
also have "... ≤ 60 + 1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧2 +
10 * H * (3 + nlength (3 * H + idx * H)) + 2 * nlength idx +
1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧2 + 2 * nlength (Suc idx) +
1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧2"
using nlength_mono linear_le_pow by simp
also have "... ≤ 60 + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧2 +
10 * H * (3 + nlength (3 * H + idx * H)) + 2 * nlength idx +
1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧2 + 2 * nlength (Suc idx) +
1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧2"
using nlength_mono linear_le_pow by simp
also have "... = 60 + 5553 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧2 +
10 * H * (3 + nlength (3 * H + idx * H)) + 2 * nlength idx + 2 * nlength (Suc idx)"
by simp
also have "... ≤ 60 + 5553 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧2 +
10 * H * (3 + nlength (3 * H + idx * H)) + 2 * nlength (Suc idx) + 2 * nlength (Suc idx)"
using nlength_mono by simp
also have "... = 60 + 5553 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧2 +
10 * H * (3 + nlength (3 * H + idx * H)) + 4 * nlength (Suc idx)"
by simp
also have "... ≤ 60 + 5553 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧2 +
10 * H * (3 + nlength (3 * H + idx * H)) + 4 * nlength (Suc idx)"
proof -
have "Suc (Suc (Suc idx)) ≤ 3 * H + idx * H"
proof (cases "idx = 0")
case True
then show ?thesis
using H by simp
next
case False
then show ?thesis
using H
by (metis One_nat_def Suc3_eq_add_3 comm_semiring_class.distrib le_Suc_eq less_eq_nat.simps(1) mult.commute
mult_1 mult_le_mono1 nle_le not_numeral_le_zero)
qed
then have "nlength (Suc (Suc (Suc idx))) ≤ 3 + nlength (3 * H + idx * H)"
using nlength_mono trans_le_add2 by presburger
then have "nlength (Suc (Suc (Suc idx))) ^ 2 ≤ (3 + nlength (3 * H + idx * H)) ^ 2"
by simp
then show ?thesis
by simp
qed
also have "... ≤ 60 + 5553 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧2 +
10 * H ^ 4 * (3 + nlength (3 * H + idx * H)) + 4 * nlength (Suc idx)"
using linear_le_pow by simp
also have "... ≤ 60 + 5553 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧2 +
10 * H ^ 4 * (3 + nlength (3 * H + idx * H)) ^ 2 + 4 * nlength (Suc idx)"
using linear_le_pow by simp
also have "... = 60 + 5563 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧2 + 4 * nlength (Suc idx)"
by simp
also have "... ≤ 60 + 5563 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧2 +
4 * H^4 * (3 + nlength (3 * H + idx * H))^2"
proof -
have "idx ≤ idx * H"
using H by simp
then have "Suc idx ≤ 3 * H + idx * H"
using H by linarith
then have "nlength (Suc idx) ≤ 3 + nlength (3 * H + idx * H)"
using nlength_mono trans_le_add2 by presburger
also have "... ≤ (3 + nlength (3 * H + idx * H)) ^ 2"
by (simp add: power2_eq_square)
also have "... ≤ H * (3 + nlength (3 * H + idx * H)) ^ 2"
using H by simp
also have "... ≤ H^4 * (3 + nlength (3 * H + idx * H)) ^ 2"
using linear_le_pow by simp
finally have "nlength (Suc idx) ≤ H^4 * (3 + nlength (3 * H + idx * H)) ^ 2" .
then show ?thesis
by simp
qed
also have "... = 60 + 5567 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧2"
by simp
also have "... ≤ 60 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧2 + 5567 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧2"
using H linear_le_pow by simp
also have "... = 5627 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧2"
by simp
finally have "?ttt ≤ ttt"
using assms by simp
then show ?thesis
using tm12 transforms_monotone by simp
qed
end
end
lemma transforms_tm_PHI0I:
fixes j :: tapeidx
fixes tps tps' :: "tape list" and ttt k idx H :: nat
assumes "length tps = k" and "1 < j" and "j + 8 < k" and "H ≥ 3"
assumes
"tps ! 1 = (⌊[]⌋, 1)"
"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 "tps' = tps
[j := (⌊Suc (Suc idx)⌋⇩N, 1),
j + 2 := (⌊0⌋⇩N, 1),
j + 6 := (⌊nll_Psi (Suc (Suc idx) * H) H 0⌋⇩N⇩L⇩L, 1),
1 := nlltape (nll_Psi (idx * H) H 1 @ nll_Psi (H + idx * H) H 1 @ nll_Psi (Suc (Suc idx) * H) H 0)]"
assumes "ttt = 5627 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧2"
shows "transforms (tm_PHI0 j) tps ttt tps'"
proof -
interpret loc: turing_machine_PHI0 j .
show ?thesis
using loc.tps12_def loc.tm12' loc.tm12_eq_tm_PHI0 assms by metis
qed
subsection ‹A Turing machine for $\Phi_1$›
text ‹
The next TM expects a number $H$ on tape $j + 1$ and appends to the formula on
tape $1$ the formula $\Psi([0, H), 1)$.
›
definition tm_PHI1 :: "tapeidx ⇒ machine" where
"tm_PHI1 j ≡
tm_setn (j + 2) 1 ;;
tm_Psigamma j ;;
tm_extendl 1 (j + 6)"
lemma tm_PHI1_tm:
assumes "0 < j" and "j + 7 < k" and "G ≥ 6"
shows "turing_machine k G (tm_PHI1 j)"
unfolding tm_PHI1_def using assms tm_Psigamma_tm tm_setn_tm tm_extendl_tm by simp
locale turing_machine_PHI1 =
fixes j :: tapeidx
begin
definition "tm1 ≡ tm_setn (j + 2) 1"
definition "tm2 ≡ tm1 ;; tm_Psigamma j"
definition "tm3 ≡ tm2 ;; tm_extendl 1 (j + 6)"
lemma tm3_eq_tm_PHI1: "tm3 = tm_PHI1 j"
using tm3_def tm2_def tm1_def tm_PHI1_def by simp
context
fixes tps0 :: "tape list" and k idx H :: nat and nss :: "nat list list"
assumes jk: "length tps0 = k" "1 < j" "j + 7 < k"
and H: "H ≥ 3"
assumes tps0:
"tps0 ! 1 = nlltape nss"
"tps0 ! j = (⌊0⌋⇩N, 1)"
"tps0 ! (j + 1) = (⌊H⌋⇩N, 1)"
"tps0 ! (j + 2) = (⌊[]⌋, 1)"
"tps0 ! (j + 3) = (⌊[]⌋, 1)"
"tps0 ! (j + 4) = (⌊[]⌋, 1)"
"tps0 ! (j + 5) = (⌊[]⌋, 1)"
"tps0 ! (j + 6) = (⌊[]⌋, 1)"
"tps0 ! (j + 7) = (⌊[]⌋, 1)"
begin
definition "tps1 ≡ tps0
[j + 2 := (⌊1⌋⇩N, 1)]"
lemma tm1 [transforms_intros]:
assumes "ttt = 12"
shows "transforms tm1 tps0 ttt tps1"
unfolding tm1_def
proof (tform tps: tps0 tps1_def jk)
show "tps0 ! (j + 2) = (⌊0⌋⇩N, 1)"
using tps0 jk canrepr_0 by simp
show "ttt = 10 + 2 * nlength 0 + 2 * nlength 1"
using assms canrepr_1 by simp
qed
definition "tps2 ≡ tps0
[j + 2 := (⌊1⌋⇩N, 1),
j + 6 := (⌊nll_Psi 0 H 1⌋⇩N⇩L⇩L, 1)]"
lemma tm2 [transforms_intros]:
assumes "ttt = 12 + 1851 * H ^ 4"
shows "transforms tm2 tps0 ttt tps2"
unfolding tm2_def
proof (tform tps: tps0 H tps1_def tps2_def jk)
show "ttt = 12 + 1851 * H ^ 4 * (nlength (Suc 0))⇧2"
using canrepr_1 assms by simp
qed
definition "tps3 ≡ tps0
[j + 2 := (⌊1⌋⇩N, 1),
j + 6 := (⌊nll_Psi 0 H 1⌋⇩N⇩L⇩L, 1),
1 := nlltape (nss @ nll_Psi 0 H 1)]"
lemma tm3:
assumes "ttt = 16 + 1851 * H ^ 4 + 2 * nlllength (nll_Psi 0 H 1)"
shows "transforms tm3 tps0 ttt tps3"
unfolding tm3_def by (tform tps: tps0 H tps2_def tps3_def jk time: assms)
lemma tm3':
assumes "ttt = 1875 * H ^ 4"
shows "transforms tm3 tps0 ttt tps3"
proof -
let ?ttt = "16 + 1851 * H ^ 4 + 2 * nlllength (nll_Psi 0 H 1)"
have "?ttt ≤ 16 + 1851 * H ^ 4 + 2 * H * (3 + nlength H)"
using nlllength_nll_Psi_le
by (metis (mono_tags, lifting) add_left_mono mult.assoc nat_mult_le_cancel1 plus_nat.add_0 rel_simps(51))
also have "... = 16 + 1851 * H ^ 4 + 6 * H + 2 * H * nlength H"
by algebra
also have "... ≤ 16 + 1851 * H ^ 4 + 6 * H + 2 * H * H"
using nlength_le_n by simp
also have "... ≤ 16 + 1851 * H ^ 4 + 6 * H * H + 2 * H * H"
by simp
also have "... = 16 + 1851 * H ^ 4 + 8 * H^2"
by algebra
also have "... ≤ 16 + 1851 * H ^ 4 + 8 * H^4"
using pow_mono'[of 2 4 H] by simp
also have "... = 16 + 1859 * H ^ 4"
by simp
also have "... ≤ 16 * H^4 + 1859 * H ^ 4"
using H by simp
also have "... = 1875 * H ^ 4"
by simp
finally have "?ttt ≤ 1875 * H ^ 4" .
then show ?thesis
using assms tm3 transforms_monotone by simp
qed
end
end
lemma transforms_tm_PHI1I:
fixes j :: tapeidx
fixes tps tps' :: "tape list" and ttt k H :: nat and nss :: "nat list list"
assumes "length tps = k" and "1 < j" and "j + 7 < k" and "H ≥ 3"
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 @ nll_Psi 0 H 1)]"
assumes "ttt = 1875 * H ^ 4"
shows "transforms (tm_PHI1 j) tps ttt tps'"
proof -
interpret loc: turing_machine_PHI1 j .
show ?thesis
using loc.tps3_def loc.tm3' loc.tm3_eq_tm_PHI1 assms by metis
qed
subsection ‹A Turing machine for $\Phi_2$›
text ‹
The next TM expects a number $i$ on tape $j$ and a number $H$ on tape $j + 1$.
It appends to the formula on tape~$1$ the formula $\Psi([(2i+1)H, (2i+2)H), 3)
\land \Psi([(2i+2)H, (2i+3)H), 3)$.
›
definition tm_PHI2 :: "tapeidx ⇒ machine" where
"tm_PHI2 j ≡
tm_times2 j ;;
tm_incr j ;;
tm_setn (j + 2) 3 ;;
tm_Psigamma j ;;
tm_extendl_erase 1 (j + 6) ;;
tm_incr j ;;
tm_Psigamma j ;;
tm_extendl 1 (j + 6)"
lemma tm_PHI2_tm:
assumes "0 < j" and "j + 8 < k" and "G ≥ 6"
shows "turing_machine k G (tm_PHI2 j)"
unfolding tm_PHI2_def
using assms tm_Psigamma_tm tm_extendl_tm tm_erase_cr_tm tm_times2_tm tm_incr_tm tm_setn_tm tm_cr_tm tm_extendl_erase_tm
by simp
locale turing_machine_PHI2 =
fixes j :: tapeidx
begin
definition "tm1 ≡ tm_times2 j"
definition "tm2 ≡ tm1 ;; tm_incr j"
definition "tm3 ≡ tm2 ;; tm_setn (j + 2) 3"
definition "tm4 ≡ tm3 ;; tm_Psigamma j"
definition "tm5 ≡ tm4 ;; tm_extendl_erase 1 (j + 6)"
definition "tm7 ≡ tm5 ;; tm_incr j"
definition "tm8 ≡ tm7 ;; tm_Psigamma j"
definition "tm9 ≡ tm8 ;; tm_extendl 1 (j + 6)"
lemma tm9_eq_tm_PHI2: "tm9 = tm_PHI2 j"
using tm9_def tm8_def tm7_def tm5_def tm4_def tm3_def tm2_def tm1_def tm_PHI2_def
by simp
context
fixes tps0 :: "tape list" and k idx H :: nat and nss :: "nat list list"
assumes jk: "length tps0 = k" "1 < j" "j + 7 < k"
and H: "H ≥ 3"
assumes tps0:
"tps0 ! 1 = nlltape nss"
"tps0 ! j = (⌊idx⌋⇩N, 1)"
"tps0 ! (j + 1) = (⌊H⌋⇩N, 1)"
"tps0 ! (j + 2) = (⌊[]⌋, 1)"
"tps0 ! (j + 3) = (⌊[]⌋, 1)"
"tps0 ! (j + 4) = (⌊[]⌋, 1)"
"tps0 ! (j + 5) = (⌊[]⌋, 1)"
"tps0 ! (j + 6) = (⌊[]⌋, 1)"
"tps0 ! (j + 7) = (⌊[]⌋, 1)"
begin
definition "tps1 ≡ tps0
[j := (⌊2 * idx⌋⇩N, 1)]"
lemma tm1 [transforms_intros]:
assumes "ttt = 5 + 2 * nlength idx"
shows "transforms tm1 tps0 ttt tps1"
unfolding tm1_def by (tform tps: tps0 tps1_def jk assms)
definition "tps2 ≡ tps0
[j := (⌊2 * idx + 1⌋⇩N, 1)]"
lemma tm2:
assumes "ttt = 10 + 2 * nlength idx + 2 * nlength (2 * idx)"
shows "transforms tm2 tps0 ttt tps2"
unfolding tm2_def by (tform tps: tps0 H tps1_def tps2_def jk assms)
lemma tm2' [transforms_intros]:
assumes "ttt = 12 + 4 * nlength idx"
shows "transforms tm2 tps0 ttt tps2"
proof -
have "10 + 2 * nlength idx + 2 * nlength (2 * idx) ≤ 10 + 2 * nlength idx + 2 * (Suc (nlength idx))"
using nlength_times2 by (meson add_left_mono mult_le_mono2)
then have "10 + 2 * nlength idx + 2 * nlength (2 * idx) ≤ ttt"
using assms by simp
then show ?thesis
using tm2 transforms_monotone by simp
qed
definition "tps3 ≡ tps0
[j := (⌊2 * idx + 1⌋⇩N, 1),
j + 2 := (⌊3⌋⇩N, 1)]"
lemma tm3 [transforms_intros]:
assumes "ttt = 26 + 4 * nlength idx"
shows "transforms tm3 tps0 ttt tps3"
unfolding tm3_def
proof (tform tps: tps0 H tps2_def tps3_def jk)
show "tps2 ! (j + 2) = (⌊0⌋⇩N, 1)"
using tps2_def jk canrepr_0 tps0 by simp
show "ttt = 12 + 4 * nlength idx + (10 + 2 * nlength 0 + 2 * nlength 3)"
using nlength_3 assms by simp
qed
definition "tps4 ≡ tps0
[j := (⌊2 * idx + 1⌋⇩N, 1),
j + 2 := (⌊3⌋⇩N, 1),
j + 6 := (⌊nll_Psi (Suc (2 * idx) * H) H 3⌋⇩N⇩L⇩L, 1)]"
lemma tm4 [transforms_intros]:
assumes "ttt = 26 + 4 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧2"
shows "transforms tm4 tps0 ttt tps4"
unfolding tm4_def by (tform tps: tps0 H tps3_def tps4_def jk time: assms)
definition "tps5 ≡ tps0
[j := (⌊2 * idx + 1⌋⇩N, 1),
j + 2 := (⌊3⌋⇩N, 1),
j + 6 := (⌊[]⌋, 1),
1 := nlltape (nss @ nll_Psi (H + 2 * idx * H) H 3)]"
lemma tm5 [transforms_intros]:
assumes "ttt = 37 + 4 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧2 +
4 * nlllength (nll_Psi (H + 2 * idx * H) H 3)"
shows "transforms tm5 tps0 ttt tps5"
unfolding tm5_def by (tform tps: tps0 H tps4_def tps5_def jk time: assms)
definition "tps7 ≡ tps0
[j := (⌊2 * idx + 2⌋⇩N, 1),
j + 2 := (⌊3⌋⇩N, 1),
j + 6 := (⌊[]⌋, 1),
1 := nlltape (nss @ nll_Psi (H + 2 * idx * H) H 3)]"
lemma tm7:
assumes "ttt = 42 + 4 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧2 +
4 * nlllength (nll_Psi (H + 2 * idx * H) H 3) + 2 * nlength (Suc (2 * idx))"
shows "transforms tm7 tps0 ttt tps7"
unfolding tm7_def
proof (tform tps: tps0 H tps5_def tps7_def jk time: assms)
show "tps7 = tps5[j := (⌊Suc (Suc (2 * idx))⌋⇩N, 1)]"
using tps5_def tps7_def jk by (simp add: list_update_swap)
qed
lemma tm7' [transforms_intros]:
assumes "ttt = 44 + 6 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧2 +
4 * nlllength (nll_Psi (H + 2 * idx * H) H 3)"
shows "transforms tm7 tps0 ttt tps7"
proof -
let ?ttt = "42 + 4 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧2 +
4 * nlllength (nll_Psi (H + 2 * idx * H) H 3) +
2 * nlength (Suc (2 * idx))"
have "?ttt ≤ 42 + 4 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧2 +
4 * nlllength (nll_Psi (H + 2 * idx * H) H 3) +
2 * (Suc (nlength idx))"
using nlength_times2plus1 by (metis add.commute add_left_mono mult_le_mono2 plus_1_eq_Suc)
then have "?ttt ≤ ttt"
using assms by simp
then show ?thesis
using tm7 transforms_monotone by simp
qed
definition "tps8 ≡ tps0
[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 @ nll_Psi (H + 2 * idx * H) H 3)]"
lemma tm8 [transforms_intros]:
assumes "ttt = 44 + 6 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧2 +
4 * nlllength (nll_Psi (H + 2 * idx * H) H 3) +
1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * idx)))))⇧2"
shows "transforms tm8 tps0 ttt tps8"
unfolding tm8_def
proof (tform tps: tps0 H tps7_def tps8_def jk time: assms)
show "tps8 = tps7
[j + 6 := (⌊nll_Psi (Suc (Suc (2 * idx)) * H) H 3⌋⇩N⇩L⇩L, 1)]"
unfolding tps8_def tps7_def by (simp add: list_update_swap[of "j+6"])
qed
definition "tps9 ≡ tps0
[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 @ nll_Psi (H + 2 * idx * H) H 3 @ nll_Psi (2 * H + 2 * idx * H) H 3)]"
lemma tm9:
assumes "ttt = 48 + 6 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧2 +
4 * nlllength (nll_Psi (H + 2 * idx * H) H 3) +
1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * idx)))))⇧2 +
2 * nlllength (nll_Psi (2 * H + 2 * idx * H) H 3)"
shows "transforms tm9 tps0 ttt tps9"
unfolding tm9_def by (tform tps: tps0 H tps9_def tps8_def jk time: assms)
lemma tm9':
assumes "ttt = 3764 * H ^ 4 * (3 + nlength (3 * H + 2 * idx * H))⇧2"
shows "transforms tm9 tps0 ttt tps9"
proof -
let ?ttt = "48 + 6 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧2 +
4 * nlllength (nll_Psi (H + 2 * idx * H) H 3) + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * idx)))))⇧2 +
2 * nlllength (nll_Psi (2 * H + 2 * idx * H) H 3)"
have "?ttt ≤ 48 + 6 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧2 +
4 * H * (3 + nlength (2 * H + 2 * idx * H + H)) + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * idx)))))⇧2 +
2 * nlllength (nll_Psi (2 * H + 2 * idx * H) H 3)"
using nlllength_nll_Psi_le'[of "H + 2 * idx * H" "2 * H + 2 * idx * H" H 3] by simp
also have "... ≤ 48 + 6 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧2 +
5 * H * (3 + nlength (2 * H + 2 * idx * H + H)) + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * idx)))))⇧2 +
3 * H * (3 + nlength (2 * H + 2 * idx * H + H))"
using nlllength_nll_Psi_le'[of "2 * H + 2 * idx * H" "2 * H + 2 * idx * H" H 3] by simp
also have "... = 48 + 6 * nlength idx +
1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧2 +
8 * H * (3 + nlength (2 * H + 2 * idx * H + H)) +
1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * idx)))))⇧2"
by simp
also have "... ≤ 48 + 6 * nlength idx +
1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * idx)))))⇧2 +
8 * H * (3 + nlength (2 * H + 2 * idx * H + H)) +
1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * idx)))))⇧2"
using H4_nlength H by simp
also have "... = 48 + 6 * nlength idx + 3702 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * idx)))))⇧2 +
8 * H * (3 + nlength (3 * H + 2 * idx * H))"
by simp
also have "... ≤ 48 + 6 * nlength idx + 3702 * H ^ 4 * (3 + nlength (3 * H + 2 * idx * H))⇧2 +
8 * H * (3 + nlength (3 * H + 2 * idx * H))"
proof -
have "Suc (Suc (Suc (2 * idx))) ≤ 3 * H + 2 * idx * H"
using H
by (metis One_nat_def Suc3_eq_add_3 Suc_eq_plus1_left add_leD1 comm_monoid_mult_class.mult_1
distrib_right mult.commute mult_le_mono1)
then have "nlength (Suc (Suc (Suc (2 * idx)))) ≤ 3 + nlength (3 * H + 2 * idx * H)"
using nlength_mono trans_le_add2 by blast
then show ?thesis
by simp
qed
also have "... ≤ 48 + 6 * nlength idx + 3702 * H ^ 4 * (3 + nlength (3 * H + 2 * idx * H))⇧2 +
8 * H^4 * (3 + nlength (3 * H + 2 * idx * H))"
using linear_le_pow by simp
also have "... ≤ 48 + 6 * nlength idx + 3702 * H ^ 4 * (3 + nlength (3 * H + 2 * idx * H))⇧2 +
8 * H^4 * (3 + nlength (3 * H + 2 * idx * H))^2"
using linear_le_pow by simp
also have "... = 48 + 6 * nlength idx + 3710 * H ^ 4 * (3 + nlength (3 * H + 2 * idx * H))⇧2"
by simp
also have "... ≤ 48 + 3716 * H ^ 4 * (3 + nlength (3 * H + 2 * idx * H))⇧2"
proof -
have "nlength idx ≤ nlength (3 * H + 2 * idx * H)"
using H by (intro nlength_mono) (simp add: trans_le_add2)
also have "... ≤ 3 + nlength (3 * H + 2 * idx * H)"
by simp
also have "... ≤ (3 + nlength (3 * H + 2 * idx * H)) ^ 2"
using linear_le_pow by simp
also have "... ≤ H ^ 4 * (3 + nlength (3 * H + 2 * idx * H)) ^ 2"
using H by simp
finally have "nlength idx ≤ H ^ 4 * (3 + nlength (3 * H + 2 * idx * H)) ^ 2" .
then show ?thesis
by simp
qed
also have "... ≤ 3764 * H ^ 4 * (3 + nlength (3 * H + 2 * idx * H))⇧2"
proof -
have "1 ≤ nlength (3 * H + 2 * idx * H)"
using H nlength_0
by (metis One_nat_def Suc_leI add_eq_0_iff_both_eq_0 length_0_conv length_greater_0_conv mult_Suc
not_numeral_le_zero numeral_3_eq_3)
also have "... ≤ 3 + nlength (3 * H + 2 * idx * H)"
by simp
also have "... ≤ (3 + nlength (3 * H + 2 * idx * H)) ^ 2"
using linear_le_pow by simp
also have "... ≤ H ^ 4 * (3 + nlength (3 * H + 2 * idx * H)) ^ 2"
using H by simp
finally have "1 ≤ H ^ 4 * (3 + nlength (3 * H + 2 * idx * H)) ^ 2" .
then show ?thesis
by simp
qed
finally have "?ttt ≤ 3764 * H ^ 4 * (3 + nlength (3 * H + 2 * idx * H))⇧2" .
then show ?thesis
using assms tm9 transforms_monotone by simp
qed
end
end
lemma transforms_tm_PHI2I:
fixes j :: tapeidx
fixes tps tps' :: "tape list" and ttt k idx H :: nat and nss :: "nat list list"
assumes "length tps = k" and "1 < j" and "j + 8 < k"
and "H ≥ 3"
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 @ nll_Psi (H + 2 * idx * H) H 3 @ nll_Psi (2 * H + 2 * idx * H) H 3)]"
shows "transforms (tm_PHI2 j) tps ttt tps'"
proof -
interpret loc: turing_machine_PHI2 j .
show ?thesis
using loc.tm9' loc.tps9_def loc.tm9_eq_tm_PHI2 assms by simp
qed
subsection ‹Turing machines for $\Phi_3$, $\Phi_4$, and $\Phi_5$›
text ‹
The CNF formulas $\Phi_3$, $\Phi_4$, and $\Phi_5$ have a similar structure and
can thus be handled by the same Turing machine. The following TM has a parameter
$step$ and the usual tape parameter $j$. It expects on tape $j$ a number $idx$,
on tape $j + 1$ a number $H$, on tape $j + 2$ a number $\kappa$, and on tape $j
+ 8$ the number $idx + step \cdot numiter$ for some number $numiter$. It appends
to the CNF formula on tape~$1$ the formula $\Psi(\gamma_{idx}, \kappa) \land
\Psi(\gamma_{idx + step\cdot (numiter - 1)}, \kappa)$, where $\gamma_i = [iH,
(i+1)H)$.
\null
›
definition tm_PHI345 :: "nat ⇒ tapeidx ⇒ machine" where
"tm_PHI345 step j ≡
WHILE tm_equalsn j (j + 8) (j + 3) ; λrs. rs ! (j + 3) = □ DO
tm_Psigamma j ;;
tm_extendl_erase 1 (j + 6) ;;
tm_plus_const step j
DONE"
lemma tm_PHI345_tm:
assumes "G ≥ 6" and "0 < j" and "j + 8 < k"
shows "turing_machine k G (tm_PHI345 step j)"
unfolding tm_PHI345_def
using assms tm_equalsn_tm tm_Psigamma_tm tm_extendl_erase_tm tm_plus_const_tm
turing_machine_loop_turing_machine
by simp
locale turing_machine_PHI345 =
fixes step :: nat and j :: tapeidx
begin
definition "tmC ≡ tm_equalsn j (j + 8) (j + 3)"
definition "tm1 ≡ tm_Psigamma j"
definition "tm2 ≡ tm1 ;; tm_extendl_erase 1 (j + 6)"
definition "tm4 ≡ tm2 ;; tm_plus_const step j"
definition "tmL ≡ WHILE tmC ; λrs. rs ! (j + 3) = □ DO tm4 DONE"
lemma tmL_eq_tm_PHI345: "tmL = tm_PHI345 step j"
unfolding tmL_def tm4_def tm2_def tm1_def tm_PHI345_def tmC_def by simp
context
fixes tps0 :: "tape list" and numiter H k idx kappa :: nat and nss :: "nat list list"
assumes jk: "length tps0 = k" "1 < j" "j + 8 < k"
and H: "H ≥ 3"
and kappa: "kappa ≤ H"
and step: "step > 0"
assumes tps0:
"tps0 ! 1 = nlltape nss"
"tps0 ! j = (⌊idx⌋⇩N, 1)"
"tps0 ! (j + 1) = (⌊H⌋⇩N, 1)"
"tps0 ! (j + 2) = (⌊kappa⌋⇩N, 1)"
"tps0 ! (j + 3) = (⌊[]⌋, 1)"
"tps0 ! (j + 4) = (⌊[]⌋, 1)"
"tps0 ! (j + 5) = (⌊[]⌋, 1)"
"tps0 ! (j + 6) = (⌊[]⌋, 1)"
"tps0 ! (j + 7) = (⌊[]⌋, 1)"
"tps0 ! (j + 8) = (⌊idx + step * numiter⌋⇩N, 1)"
begin
definition tpsL :: "nat ⇒ tape list" where
"tpsL t ≡ tps0
[j := (⌊idx + step * t⌋⇩N, 1),
1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<t]))]"
lemma tpsL_eq_tps0: "tpsL 0 = tps0"
proof -
have "⌊idx⌋⇩N = ⌊idx + step * 0⌋⇩N"
by simp
moreover have "nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<0])) = nlltape nss"
using nllcontents_Nil by simp
ultimately show ?thesis
using tpsL_def tps0 jk by (metis list_update_id)
qed
definition tpsC :: "nat ⇒ tape list" where
"tpsC t ≡ tps0
[j := (⌊idx + step * t⌋⇩N, 1),
1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<t])),
j + 3 := (⌊t = numiter⌋⇩B, 1)]"
lemma tmC:
assumes "t ≤ numiter"
and "ttt = 3 * nlength (idx + step * t) + 7"
shows "transforms tmC (tpsL t) ttt (tpsC t)"
unfolding tmC_def
proof (tform tps: tps0 tpsL_def jk)
show "tpsL t ! (j + 3) = (⌊0⌋⇩N, 1)"
using canrepr_0 jk tpsL_def tps0 by simp
show "(0::nat) ≤ 1"
by simp
show "tpsC t = (tpsL t)
[j + 3 := (⌊idx + step * t = idx + step * numiter⌋⇩B, 1)]"
using step tpsC_def jk tpsL_def tps0 by simp
show "ttt = 3 * nlength (min (idx + step * t) (idx + step * numiter)) + 7"
using assms by (simp add: min_def)
qed
lemma tmC' [transforms_intros]:
assumes "t ≤ numiter"
and "ttt = 3 * nlength (idx + step * numiter) + 7"
shows "transforms tmC (tpsL t) ttt (tpsC t)"
proof -
have "3 * nlength (idx + step * t) + 7 ≤ ttt"
using assms nlength_mono by simp
then show ?thesis
using assms tmC transforms_monotone by blast
qed
definition tpsL0 :: "nat ⇒ tape list" where
"tpsL0 t ≡ tps0
[j := (⌊idx + step * t⌋⇩N, 1),
1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<t]))]"
lemma tpsL0_eq_tpsC:
assumes "t < numiter"
shows "tpsL0 t = tpsC t"
unfolding tpsL0_def tpsC_def
using assms jk ncontents_0 tps0 list_update_id[of tps0 "j + 3"]
by (simp add: list_update_swap)
definition tpsL1 :: "nat ⇒ tape list" where
"tpsL1 t ≡ tps0
[j := (⌊idx + step * t⌋⇩N, 1),
1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<t])),
j + 6 := (⌊nll_Psi ((idx+step*t) * H) H kappa⌋⇩N⇩L⇩L, 1)]"
lemma tm1 [transforms_intros]:
assumes "t < numiter"
and "ttt = 1851 * H ^ 4 * (nlength (Suc (idx+step*t)))⇧2"
shows "transforms tm1 (tpsL0 t) ttt (tpsL1 t)"
unfolding tm1_def by (tform tps: H kappa tps0 tpsL0_def tpsL1_def jk time: assms(2))
definition tpsL2 :: "nat ⇒ tape list" where
"tpsL2 t ≡ tps0
[j := (⌊idx + step * t⌋⇩N, 1),
1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<t])),
j + 6 := (⌊[]⌋, 1),
1 := nlltape ((nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<t])) @ nll_Psi ((idx+step*t) * H) H kappa)]"
lemma tm2:
assumes "t < numiter"
and "ttt = 1851 * H ^ 4 * (nlength (Suc (idx + step * t)))⇧2 +
(11 + 4 * nlllength (nll_Psi ((idx + step * t) * H) H kappa))"
shows "transforms tm2 (tpsL0 t) ttt (tpsL2 t)"
unfolding tm2_def by (tform tps: assms H kappa tps0 tpsL1_def tpsL2_def jk)
definition tpsL2' :: "nat ⇒ tape list" where
"tpsL2' t ≡ tps0
[j := (⌊idx + step * t⌋⇩N, 1),
j + 6 := (⌊[]⌋, 1),
1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<t]) @ nll_Psi ((idx+step*t) * H) H kappa)]"
lemma tpsL2': "tpsL2 t = tpsL2' t"
unfolding tpsL2_def tpsL2'_def by (simp only: list_update_swap list_update_overwrite) simp
lemma tm2':
assumes "t < numiter"
and "ttt = 1851 * H ^ 4 * (nlength (idx + step * numiter))⇧2 +
(11 + 4 * nlllength (nll_Psi ((idx + step * t) * H) H kappa))"
shows "transforms tm2 (tpsL0 t) ttt (tpsL2' t)"
proof -
let ?ttt = "1851 * H ^ 4 * (nlength (Suc (idx + step * t)))⇧2 +
(11 + 4 * nlllength (nll_Psi ((idx + step * t) * H) H kappa))"
have "?ttt ≤ 1851 * H ^ 4 * (nlength (idx + step * numiter))⇧2 +
(11 + 4 * nlllength (nll_Psi ((idx + step * t) * H) H kappa))"
proof -
have "Suc (idx + step * t) ≤ Suc (idx + step * (numiter - 1))"
using assms(1) step by simp
also have "... = Suc (idx + step * numiter - step)"
by (metis Nat.add_diff_assoc One_nat_def Suc_le_eq add_less_same_cancel1 assms(1) mult.right_neutral
nat_mult_le_cancel_disj nat_neq_iff not_add_less1 right_diff_distrib')
also have "... ≤ idx + step * numiter"
using step Suc_le_eq assms(1) by simp
finally have "Suc (idx + step * t) ≤ idx + step * numiter" .
then have "nlength (Suc (idx + step * t)) ≤ nlength (idx + step * numiter)"
using nlength_mono by simp
then show ?thesis
by simp
qed
then have "transforms tm2 (tpsL0 t) ttt (tpsL2 t)"
using assms tm2 transforms_monotone by blast
then show ?thesis
using tpsL2' by simp
qed
definition tpsL2'' :: "nat ⇒ tape list" where
"tpsL2'' t ≡ tps0
[j := (⌊idx + step * t⌋⇩N, 1),
1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<Suc t])),
j + 6 := (⌊[]⌋, 1)]"
lemma tpsL2'': "tpsL2'' t = tpsL2' t"
proof -
have "nll_Psi ((idx+step*t) * H) H kappa = nll_Psi (H * (idx+step*t)) H kappa"
by (simp add: mult.commute)
then have "concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<t]) @ nll_Psi ((idx+step*t) * H) H kappa =
concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<Suc t])"
by simp
then show "tpsL2'' t = tpsL2' t"
using tpsL2'_def tpsL2''_def by (simp add: list_update_swap)
qed
lemma nlllength_nll_Psi:
assumes "t < numiter"
shows "nlllength (nll_Psi ((idx + step * t) * H) H kappa) ≤ 5 * H ^ 4 * nlength (idx + step * numiter)^2"
proof -
have "nlllength (nll_Psi ((idx + step * t) * H) H kappa) ≤ H * (3 + nlength ((idx + step * t) * H + H))"
using nlllength_nll_Psi_le by simp
also have "... ≤ H * (3 + nlength ((idx + step * numiter) * H))"
proof -
have "(idx + 1 + step * t) ≤ (idx + step * Suc t)"
using step by simp
then have "(idx + 1 + step * t) ≤ (idx + step * numiter)"
using assms(1) Suc_le_eq by auto
then have "(idx + 1 + step * t) * H ≤ (idx + step * numiter) * H"
using mult_le_cancel2 by blast
then show ?thesis
using nlength_mono by simp
qed
also have "... = 3 * H + H * nlength ((idx + step * numiter) * H)"
by algebra
also have "... ≤ 3 * H + H * (nlength (idx + step * numiter) + nlength H)"
using nlength_prod by simp
also have "... ≤ 3 * H + H * (nlength (idx + step * numiter) + H)"
using nlength_le_n by simp
also have "... = 3 * H + H ^ 2 + H * nlength (idx + step * numiter)"
by algebra
also have "... ≤ 3 * H^4 + H ^ 2 + H * nlength (idx + step * numiter)"
using linear_le_pow by simp
also have "... ≤ 3 * H^4 + H ^ 4 + H * nlength (idx + step * numiter)"
using pow_mono' by simp
also have "... ≤ 4 * H^4 + H ^ 4 * nlength (idx + step * numiter)"
using linear_le_pow by simp
also have "... ≤ 4 * H^4 + H ^ 4 * nlength (idx + step * numiter)^2"
using linear_le_pow by simp
also have "... ≤ 5 * H ^ 4 * nlength (idx + step * numiter)^2"
proof -
have "idx + step * numiter > 0"
using assms(1) step by simp
then have "nlength (idx + step * numiter) > 0"
using nlength_0 by simp
then have "nlength (idx + step * numiter) ^ 2 > 0"
by simp
then have "H ^ 4 ≤ H ^ 4 * nlength (idx + step * numiter) ^ 2"
by (metis One_nat_def Suc_leI mult_numeral_1_right nat_mult_le_cancel_disj numerals(1))
then show ?thesis
by simp
qed
finally show ?thesis .
qed
lemma tm2'' [transforms_intros]:
assumes "t < numiter" and "ttt = 1871 * H ^ 4 * (nlength (idx + step * numiter))⇧2 + 11"
shows "transforms tm2 (tpsL0 t) ttt (tpsL2'' t)"
proof -
have "transforms tm2 (tpsL0 t) ttt (tpsL2' t)"
using tm2'[OF assms(1)] nlllength_nll_Psi[OF assms(1)] transforms_monotone assms(2) by simp
then show ?thesis
using tpsL2' tpsL2'' by simp
qed
definition tpsL4 :: "nat ⇒ tape list" where
"tpsL4 t ≡ tps0
[j := (⌊idx + step * Suc t⌋⇩N, 1),
1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<Suc t])),
j + 6 := (⌊[]⌋, 1)]"
lemma tm4:
assumes "t < numiter"
and "ttt = 1871 * H ^ 4 * (nlength (idx + step * numiter))⇧2 + 11 +
step * (5 + 2 * nlength (idx + step * t + step))"
shows "transforms tm4 (tpsL0 t) ttt (tpsL4 t)"
unfolding tm4_def
proof (tform tps: assms(1) H kappa tps0 tpsL2''_def tpsL4_def jk)
have "idx + step * Suc t = idx + step * t + step"
by simp
then show "tpsL4 t = (tpsL2'' t)[j := (⌊idx + step * t + step⌋⇩N, 1)]"
unfolding tpsL4_def tpsL2''_def using jk by (simp only: list_update_swap[of _ j] list_update_overwrite)
show "ttt = 1871 * H ^ 4 * (nlength (idx + step * numiter))⇧2 + 11 +
step * (5 + 2 * nlength (idx + step * t + step))"
using assms(2) .
qed
lemma tm4':
assumes "t < numiter"
and "ttt = (6 * step + 1882) * H ^ 4 * (nlength (idx + step * numiter))⇧2"
shows "transforms tm4 (tpsC t) ttt (tpsL4 t)"
proof -
let ?ttt = "1871 * H ^ 4 * (nlength (idx + step * numiter))⇧2 + 11 +
step * (5 + 2 * nlength (idx + step * t + step))"
have "idx + step * t + step ≤ idx + step * numiter"
using assms(1)
by (metis Suc_le_eq add.assoc add.commute add_le_cancel_left add_mult_distrib2 mult_le_mono2 mult_numeral_1_right numerals(1) plus_1_eq_Suc)
then have "?ttt ≤ 1871 * H ^ 4 * (nlength (idx + step * numiter))⇧2 + 11 +
step * (5 + 2 * nlength (idx + step * numiter))"
using nlength_mono by simp
also have "... = 1871 * H ^ 4 * (nlength (idx + step * numiter))⇧2 + 11 +
step * 5 + step * 2 * nlength (idx + step * numiter)"
by algebra
also have "... ≤ 1871 * H ^ 4 * (nlength (idx + step * numiter))⇧2 + 11 +
step * 5 + step * 2 * nlength (idx + step * numiter)^2"
by (simp add: linear_le_pow)
also have "... ≤ 1871 * H ^ 4 * (nlength (idx + step * numiter))⇧2 + 11 +
step * 5 + step * H^4 * nlength (idx + step * numiter)^2"
proof -
have "2 < H"
using H by simp
then have "2 < H ^ 4"
using linear_le_pow by (meson le_trans not_less zero_less_numeral)
then show ?thesis
by simp
qed
also have "... = (step + 1871) * H ^ 4 * (nlength (idx + step * numiter))⇧2 + (11 + step * 5)"
by algebra
also have "... ≤ (step + 1871) * H ^ 4 * (nlength (idx + step * numiter))⇧2 + (11 + step * 5) * H ^ 4 * (nlength (idx + step * numiter))^2"
proof -
have "H ^ 4 * (nlength (idx + step * numiter))^2 > 0"
using step assms(1) nlength_0 H by auto
then show ?thesis
by (smt (verit) One_nat_def Suc_leI add_mono_thms_linordered_semiring(2) mult.assoc mult_numeral_1_right nat_mult_le_cancel_disj numeral_code(1))
qed
also have "... = (6 * step + 1882) * H ^ 4 * (nlength (idx + step * numiter))⇧2"
by algebra
finally have "?ttt ≤ (6 * step + 1882) * H ^ 4 * (nlength (idx + step * numiter))⇧2" .
then have "transforms tm4 (tpsL0 t) ttt (tpsL4 t)"
using tm4 assms transforms_monotone by blast
then show ?thesis
using tpsL0_eq_tpsC assms(1) by simp
qed
lemma tm4'' [transforms_intros]:
assumes "t < numiter"
and "ttt = (6 * step + 1882) * H ^ 4 * (nlength (idx + step * numiter))⇧2"
shows "transforms tm4 (tpsC t) ttt (tpsL (Suc t))"
proof -
have "tpsL4 t = tpsL (Suc t)"
using tpsL4_def tpsL_def jk tps0 list_update_id[of tps0 "j + 6"]
by (simp add: list_update_swap)
then show ?thesis
using tm4' assms by metis
qed
lemma tmL:
assumes "ttt = Suc numiter * (9 + (6 * step + 1885) * (H ^ 4 * (nlength (idx + step * numiter))⇧2))"
and "nn = numiter"
shows "transforms tmL (tpsL 0) ttt (tpsC nn)"
unfolding tmL_def
proof (tform tps: assms(2))
let ?ttt = "(6 * step + 1882) * H ^ 4 * (nlength (idx + step * numiter))⇧2"
show "⋀t. t < nn ⟹ read (tpsC t) ! (j + 3) = □"
using assms(2) tpsC_def jk read_ncontents_eq_0 by simp
show "read (tpsC nn) ! (j + 3) ≠ □"
using assms(2) tpsC_def jk read_ncontents_eq_0 by simp
show "nn * (3 * nlength (idx + step * numiter) + 7 + ?ttt + 2) + (3 * nlength (idx + step * numiter) + 7) + 1 ≤ ttt"
(is "?lhs ≤ ttt")
proof -
let ?g = "H ^ 4 * (nlength (idx + step * numiter))⇧2"
have "nlength (idx + step * numiter) ≤ nlength (idx + step * numiter)^2"
using linear_le_pow by simp
moreover have "H ^ 4 > 0"
using H by simp
ultimately have *: "nlength (idx + step * numiter) ≤ ?g"
by (metis ab_semigroup_mult_class.mult_ac(1) le_square mult.left_commute nat_mult_le_cancel_disj power2_eq_square)
have "?lhs = numiter * (3 * nlength (idx + step * numiter) + 9 + ?ttt) + 3 * nlength (idx + step * numiter) + 8"
using assms(2) by simp
also have "... ≤ numiter * (3 * nlength (idx + step * numiter) + 9 + ?ttt) + 3 * ?g + 8"
using * by simp
also have "... ≤ numiter * (3 * ?g + 9 + (6 * step + 1882) * ?g) + 3 * ?g + 8"
using * by simp
also have "... = numiter * (9 + (6 * step + 1885) * ?g) + 3 * ?g + 8"
by algebra
also have "... ≤ numiter * (9 + (6 * step + 1885) * ?g) + (6 * step + 1885) * ?g + 8"
by simp
also have "... ≤ numiter * (9 + (6 * step + 1885) * ?g) + (9 + (6 * step + 1885) * ?g)"
by simp
also have "... = Suc numiter * (9 + (6 * step + 1885) * ?g)"
by simp
finally show ?thesis
using assms(1) by simp
qed
qed
lemma tmL':
assumes "ttt = Suc numiter * (9 + (6 * step + 1885) * (H ^ 4 * (nlength (idx + step * numiter))⇧2))"
shows "transforms tmL tps0 ttt (tpsC numiter)"
using assms tmL tpsL_eq_tps0 by simp
end
end
lemma transforms_tm_PHI345I:
fixes j :: tapeidx
fixes tps tps' :: "tape list" and ttt step numiter H k idx kappa :: nat and nss :: "nat list list"
assumes "length tps = k" and "1 < j" and "j + 8 < k"
and "H ≥ 3"
and "kappa ≤ H"
and "step > 0"
assumes
"tps ! 1 = nlltape nss"
"tps ! j = (⌊idx⌋⇩N, 1)"
"tps ! (j + 1) = (⌊H⌋⇩N, 1)"
"tps ! (j + 2) = (⌊kappa⌋⇩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) = (⌊idx + step * numiter⌋⇩N, 1)"
assumes "ttt = Suc numiter * (9 + (6 * step + 1885) * (H ^ 4 * (nlength (idx + step * numiter))⇧2))"
assumes "tps' = tps
[j := (⌊idx + step * numiter⌋⇩N, 1),
1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<numiter])),
j + 3 := (⌊1⌋⇩N, 1)]"
shows "transforms (tm_PHI345 step j) tps ttt tps'"
proof -
interpret loc: turing_machine_PHI345 step j .
show ?thesis
using assms loc.tmL' loc.tpsC_def loc.tmL_eq_tm_PHI345 by simp
qed
subsection ‹A Turing machine for $\Phi_6$›
text ‹
The next Turing machine expects a symbol sequence $zs$ on input tape~$0$, the
number~$2$ on tape $j$, and a number $H$ on tape $j + 1$. It appends to the CNF
formula on tape~$1$ the formula $\bigwedge_{i=0}^{|zs| - 1} \Psi(\gamma_{2+2i},
z_i)$, where $z_i$ is $2$ or $3$ if $zs_i$ is \textbf{0} or \textbf{1},
respectively.
›
definition tm_PHI6 :: "tapeidx ⇒ machine" where
"tm_PHI6 j ≡
WHILE [] ; λrs. rs ! 0 ≠ □ DO
IF λrs. rs ! 0 = 𝟬 THEN
tm_setn (j + 2) 2
ELSE
tm_setn (j + 2) 3
ENDIF ;;
tm_Psigamma j ;;
tm_extendl_erase 1 (j + 6) ;;
tm_setn (j + 2) 0 ;;
tm_right 0 ;;
tm_plus_const 2 j
DONE"
lemma tm_PHI6_tm:
assumes "G ≥ 6" and "0 < j" and "j + 7 < k"
shows "turing_machine k G (tm_PHI6 j)"
unfolding tm_PHI6_def
using assms tm_Psigamma_tm tm_extendl_erase_tm tm_plus_const_tm
turing_machine_loop_turing_machine turing_machine_branch_turing_machine
tm_right_tm tm_setn_tm Nil_tm
by simp
locale turing_machine_PHI6 =
fixes j :: tapeidx
begin
definition "tm1 ≡ IF λrs. rs ! 0 = 𝟬 THEN tm_setn (j + 2) 2 ELSE tm_setn (j + 2) 3 ENDIF"
definition "tm2 ≡ tm1 ;; tm_Psigamma j"
definition "tm3 ≡ tm2 ;; tm_extendl_erase 1 (j + 6)"
definition "tm4 ≡ tm3 ;; tm_setn (j + 2) 0"
definition "tm5 ≡ tm4 ;; tm_right 0"
definition "tm6 ≡ tm5 ;; tm_plus_const 2 j"
definition "tmL ≡ WHILE [] ; λrs. rs ! 0 ≠ □ DO tm6 DONE"
lemma tmL_eq_tm_PHI6: "tmL = tm_PHI6 j"
using tm6_def tm5_def tm4_def tm3_def tm2_def tm1_def tm_PHI6_def tmL_def by simp
context
fixes tps0 :: "tape list" and k H :: nat and zs :: "symbol list" and nss :: "nat list list"
assumes jk: "length tps0 = k" "1 < j" "j + 7 < k"
and H: "H ≥ 3"
and zs: "bit_symbols zs"
assumes tps0:
"tps0 ! 0 = (⌊zs⌋, 1)"
"tps0 ! 1 = nlltape nss"
"tps0 ! j = (⌊2⌋⇩N, 1)"
"tps0 ! (j + 1) = (⌊H⌋⇩N, 1)"
"tps0 ! (j + 2) = (⌊0⌋⇩N, 1)"
"tps0 ! (j + 3) = (⌊[]⌋, 1)"
"tps0 ! (j + 4) = (⌊[]⌋, 1)"
"tps0 ! (j + 5) = (⌊[]⌋, 1)"
"tps0 ! (j + 6) = (⌊[]⌋, 1)"
"tps0 ! (j + 7) = (⌊[]⌋, 1)"
begin
lemma H0: "H > 0"
using H by simp
lemma H_mult: "x ≤ H * x" "x ≤ x * H"
using H by simp_all
definition tpsL :: "nat ⇒ tape list" where
"tpsL t ≡ tps0
[0 := (⌊zs⌋, Suc t),
j := (⌊2 + 2 * t⌋⇩N, 1),
1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (2 + 2 * i)) H (zs ! i)) [0..<t]))]"
lemma tpsL_eq_tps0: "tpsL 0 = tps0"
proof -
have "(⌊zs⌋, 1) = (⌊zs⌋, Suc 0)"
by simp
moreover have "nlltape (concat (map (λi. nll_Psi (H * (2 + 2 * i)) H (zs ! i)) [0..<0])) = (⌊[]⌋, 1)"
using nllcontents_Nil by simp
moreover have "2 = Suc (Suc 0)"
by simp
ultimately show ?thesis
using tpsL_def tps0 jk by simp (metis One_nat_def Suc_1 list_update_id)
qed
definition tpsL1 :: "nat ⇒ tape list" where
"tpsL1 t ≡ tps0
[0 := (⌊zs⌋, Suc t),
j := (⌊2 + 2 * t⌋⇩N, 1),
j + 2 := (⌊zs ! t⌋⇩N, 1),
1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (2 + 2 * i)) H (zs ! i)) [0..<t]))]"
lemma tm1 [transforms_intros]:
assumes "ttt = 16" and "t < length zs"
shows "transforms tm1 (tpsL t) ttt (tpsL1 t)"
unfolding tm1_def
proof (tform tps: tpsL_def tps0 jk)
have *: "read (tpsL t) ! 0 = zs ! t"
using jk tpsL_def tapes_at_read'[of 0 "tpsL t"] assms(2) by simp
show "read (tpsL t) ! 0 = 𝟬 ⟹ tpsL1 t = (tpsL t)[j + 2 := (⌊2⌋⇩N, 1)]"
using * tpsL_def tpsL1_def jk by (simp add: list_update_swap)
show "tpsL1 t = (tpsL t)[j + 2 := (⌊3⌋⇩N, 1)]" if "read (tpsL t) ! □ ≠ 𝟬"
proof -
have "zs ! t = 𝟭"
using * that zs assms(2) by auto
then show ?thesis
using tpsL_def tpsL1_def jk by (simp add: list_update_swap)
qed
show "10 + 2 * nlength 0 + 2 * nlength 2 + 2 ≤ ttt"
using nlength_0 nlength_2 assms(1) by simp
show "10 + 2 * nlength 0 + 2 * nlength 3 + 1 ≤ ttt"
using nlength_0 nlength_3 assms(1) by simp
qed
definition tpsL2 :: "nat ⇒ tape list" where
"tpsL2 t ≡ tps0
[0 := (⌊zs⌋, Suc t),
j := (⌊2 + 2 * t⌋⇩N, 1),
j + 2 := (⌊zs ! t⌋⇩N, 1),
j + 6 := (⌊nll_Psi (2 * H + 2 * t * H) H (zs ! t)⌋⇩N⇩L⇩L, Suc 0),
1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (2 + 2 * i)) H (zs ! i)) [0..<t]))]"
lemma tm2 [transforms_intros]:
assumes "ttt = 16 + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * t)))))⇧2"
and "t < length zs"
shows "transforms tm2 (tpsL t) ttt (tpsL2 t)"
unfolding tm2_def
proof (tform tps: assms(2) tps0 H tpsL1_def tpsL2_def jk time: assms(1))
show "zs ! t ≤ H"
using assms(2) H zs by auto
qed
definition tpsL3 :: "nat ⇒ tape list" where
"tpsL3 t ≡ tps0
[0 := (⌊zs⌋, Suc t),
j := (⌊2 + 2 * t⌋⇩N, 1),
j + 2 := (⌊zs ! t⌋⇩N, 1),
j + 6 := (⌊[]⌋, 1),
1 := nlltape (nss @ concat (map (λi. nll_Psi (2 * H + H * (2 * i)) H (zs ! i)) [0..<Suc t]))]"
lemma tm3 [transforms_intros]:
assumes "ttt = 27 + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * t)))))⇧2 +
4 * nlllength (nll_Psi (2 * H + 2 * t * H) H (zs ! t))"
and "t < length zs"
shows "transforms tm3 (tpsL t) ttt (tpsL3 t)"
unfolding tm3_def
proof (tform tps: assms(2) tps0 H tpsL2_def tpsL3_def jk time: assms(1))
have "nll_Psi (2 * H + H * (2 * t)) H = nll_Psi (2 * H + 2 * t * H) H"
by (simp add: mult.commute)
then have "(nss @ concat (map (λi. nll_Psi (2 * H + H * (2 * i)) H (zs ! i)) [0..<t])) @
nll_Psi (2 * H + 2 * t * H) H (zs ! t) =
nss @ concat (map (λi. nll_Psi (2 * H + H * (2 * i)) H (zs ! i)) [0..<Suc t])"
using assms(2) by simp
then show "tpsL3 t = (tpsL2 t)
[1 := nlltape
((nss @ concat (map (λi. nll_Psi (2 * H + H * (2 * i)) H (zs ! i)) [0..<t])) @
nll_Psi (2 * H + 2 * t * H) H (zs ! t)),
j + 6 := (⌊[]⌋, 1)]"
unfolding tpsL3_def tpsL2_def jk by (simp add: list_update_swap)
qed
definition tpsL4 :: "nat ⇒ tape list" where
"tpsL4 t ≡ tps0
[0 := (⌊zs⌋, Suc t),
j := (⌊2 + 2 * t⌋⇩N, 1),
j + 2 := (⌊0⌋⇩N, 1),
j + 6 := (⌊[]⌋, 1),
1 := nlltape (nss @ concat (map (λi. nll_Psi (2 * H + H * (2 * i)) H (zs ! i)) [0..<Suc t]))]"
lemma tm4 [transforms_intros]:
assumes "ttt = 41 + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * t)))))⇧2 +
4 * nlllength (nll_Psi (2 * H + 2 * t * H) H (zs ! t))"
and "t < length zs"
shows "transforms tm4 (tpsL t) ttt (tpsL4 t)"
unfolding tm4_def
proof (tform tps: assms(2) tpsL3_def tpsL4_def jk)
have "zs ! t = 2 ∨ zs ! t = 3"
using zs assms(2) by auto
then show "ttt = 27 + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * t)))))⇧2 +
4 * nlllength (nll_Psi (2 * H + 2 * t * H) H (zs ! t)) +
(10 + 2 * nlength (zs ! t) + 2 * nlength 0)"
using nlength_2 nlength_3 assms(1) by auto
qed
definition tpsL5 :: "nat ⇒ tape list" where
"tpsL5 t ≡ tps0
[0 := (⌊zs⌋, Suc (Suc t)),
j := (⌊2 + 2 * t⌋⇩N, 1),
j + 2 := (⌊0⌋⇩N, 1),
j + 6 := (⌊[]⌋, 1),
1 := nlltape (nss @ concat (map (λi. nll_Psi (2 * H + H * (2 * i)) H (zs ! i)) [0..<Suc t]))]"
lemma tm5 [transforms_intros]:
assumes "ttt = 42 + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * t)))))⇧2 +
4 * nlllength (nll_Psi (2 * H + 2 * t * H) H (zs ! t))"
and "t < length zs"
shows "transforms tm5 (tpsL t) ttt (tpsL5 t)"
unfolding tm5_def
proof (tform tps: assms(2) tps0 H tpsL4_def tpsL5_def jk time: assms(1))
have neq: "0 ≠ j"
using jk by simp
have "tpsL4 t ! 0 = (⌊zs⌋, Suc t)"
using tpsL4_def jk by simp
then show "tpsL5 t = (tpsL4 t)[0 := tpsL4 t ! 0 |+| 1]"
unfolding tpsL5_def tpsL4_def jk by (simp add: list_update_swap[OF neq] list_update_swap[of _ 0])
qed
definition tpsL6 :: "nat ⇒ tape list" where
"tpsL6 t ≡ tps0
[0 := (⌊zs⌋, Suc (Suc t)),
j := (⌊2 + 2 * (Suc t)⌋⇩N, 1),
j + 2 := (⌊0⌋⇩N, 1),
j + 6 := (⌊[]⌋, 1),
1 := nlltape (nss @ concat (map (λi. nll_Psi (2 * H + H * (2 * i)) H (zs ! i)) [0..<Suc t]))]"
lemma tm6:
assumes "ttt = 52 + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * t)))))⇧2 +
4 * nlllength (nll_Psi (2 * H + 2 * t * H) H (zs ! t)) +
4 * nlength (4 + 2 * t)"
and "t < length zs"
shows "transforms tm6 (tpsL t) ttt (tpsL6 t)"
unfolding tm6_def
proof (tform tps: tps0 H tpsL5_def tpsL6_def jk assms(2))
show "tpsL6 t = (tpsL5 t)[j := (⌊Suc (Suc (2 * t)) + 2⌋⇩N, 1)]"
using tpsL6_def tpsL5_def jk by (simp add: list_update_swap)
have *: "4 + 2 * t = Suc (Suc (Suc (Suc (2 * t))))"
by simp
then show "ttt = 42 + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * t)))))⇧2 +
4 * nlllength (nll_Psi (2 * H + 2 * t * H) H (zs ! t)) +
2 * (5 + 2 * nlength (Suc (Suc (2 * t)) + 2))"
using assms(1) * by simp
qed
lemma tpsL6_eq_tpsL: "tpsL6 t = tpsL (Suc t)"
proof -
have "tpsL (Suc t) ! (j + 6) = (⌊[]⌋, 1)"
using tpsL_def tps0 jk by simp
then have "tpsL (Suc t) = (tpsL (Suc t))[j + 6 := (⌊[]⌋, 1)]"
using list_update_id by metis
moreover have "tpsL (Suc t) ! (j + 2) = (⌊0⌋⇩N, 1)"
using tpsL_def tps0 jk canrepr_0 by simp
ultimately have "tpsL (Suc t) = (tpsL (Suc t))[j + 6 := (⌊[]⌋, 1), j + 2 := (⌊0⌋⇩N, 1)]"
using list_update_id by metis
moreover have "tpsL6 t = (tpsL (Suc t))[j + 6 := (⌊[]⌋, 1), j + 2 := (⌊0⌋⇩N, 1)]"
unfolding tpsL6_def tpsL_def by (simp add: list_update_swap)
ultimately show ?thesis
by simp
qed
lemma tm6':
assumes "ttt = 133648 * H ^ 6 * length zs^2"
and "t < length zs"
shows "transforms tm6 (tpsL t) ttt (tpsL (Suc t))"
proof -
have **: "Suc (2 * length zs)^2 ≤ 9 * length zs ^ 2"
proof -
have "Suc (2 * length zs)^2 = 1 + 2 * 2 * length zs + (2 * length zs)^2"
by (metis add.commute add_Suc_shift mult.assoc nat_mult_1_right one_power2 plus_1_eq_Suc power2_sum)
also have "... = 1 + 4 * length zs + 4 * length zs^2"
by simp
also have "... ≤ length zs + 4 * length zs + 4 * length zs^2"
using assms(2) by simp
also have "... = 5 * length zs + 4 * length zs^2"
by simp
also have "... ≤ 5 * length zs^2 + 4 * length zs^2"
using linear_le_pow by simp
also have "... = 9 * length zs^2"
by simp
finally show ?thesis
by simp
qed
have *: "t ≤ length zs - 1"
using assms(2) by simp
let ?ttt = "52 + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * t)))))⇧2 +
4 * nlllength (nll_Psi (2 * H + 2 * t * H) H (zs ! t)) +
4 * nlength (4 + 2 * t)"
have "?ttt = 52 + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * t)))))⇧2 +
4 * nlllength (nll_Psi (2 * H + H * (2 * t)) H (zs ! t)) +
4 * nlength (4 + 2 * t)"
by (simp add: mult.commute)
also have "... ≤ 52 + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * t)))))⇧2 +
4 * nlllength (nll_Psi (2 * H + H * (2 * t)) H (zs ! t)) +
4 * nlength (2 + 2 * length zs)"
using nlength_mono assms(2) by simp
also have "... ≤ 52 + 1851 * H ^ 4 * (nlength (Suc (2 * length zs)))⇧2 +
4 * nlllength (nll_Psi (2 * H + H * (2 * t)) H (zs ! t)) +
4 * nlength (2 + 2 * length zs)"
using H4_nlength H assms(2) by simp
also have "... ≤ 52 + 1851 * H ^ 4 * (nlength (Suc (2 * length zs)))⇧2 +
4 * H * (3 + nlength (3 * H + H * (2 * (length zs - 1)))) +
4 * nlength (2 + 2 * length zs)"
using nlllength_nll_Psi_le'[of "2 * H + H * (2 * t)" "2 * H + H * (2 * (length zs - 1))" H] *
by simp
also have "... = 52 + 1851 * H ^ 4 * (nlength (Suc (2 * length zs)))⇧2 +
4 * H * (3 + nlength (H * (1 + 2 * length zs))) + 4 * nlength (2 + 2 * length zs)"
proof -
have "3 * H + H * (2 * (length zs - 1)) = H * (3 + 2 * (length zs - 1))"
by algebra
also have "... = H * (3 + 2 * length zs - 2)"
using assms(2)
by (metis Nat.add_diff_assoc Suc_pred add_mono_thms_linordered_semiring(1) le_numeral_extra(4)
length_greater_0_conv list.size(3) mult_2 nat_1_add_1 not_less_zero plus_1_eq_Suc
right_diff_distrib' trans_le_add1)
also have "... = H * (1 + 2 * length zs)"
by simp
finally have "3 * H + H * (2 * (length zs - 1)) = H * (1 + 2 * length zs)" .
then show ?thesis
by metis
qed
also have "... ≤ 52 + 1851 * H ^ 4 * (3 + nlength (Suc (2 * length zs)))⇧2 +
4 * H * (3 + nlength (H * (1 + 2 * length zs))) + 4 * nlength (2 + 2 * length zs)"
by simp
also have "... ≤ 52 + 1851 * H ^ 4 * (3 + nlength (H * Suc (2 * length zs)))⇧2 +
4 * H * (3 + nlength (H * Suc (2 * length zs))) + 4 * nlength (2 + 2 * length zs)"
proof -
have "Suc (2 * length zs) ≤ H * Suc (2 * length zs)"
using H_mult by blast
then have "nlength (Suc (2 * length zs))^2 ≤ nlength (H * Suc (2 * length zs))^2"
using nlength_mono by simp
then show ?thesis
by simp
qed
also have "... ≤ 52 + 1851 * H ^ 4 * (3 + nlength (H * Suc (2 * length zs)))⇧2 +
4 * H * (3 + nlength (H * Suc (2 * length zs)))^2 + 4 * nlength (2 + 2 * length zs)"
using linear_le_pow by simp
also have "... ≤ 52 + 1851 * H ^ 4 * (3 + nlength (H * Suc (2 * length zs)))⇧2 +
4 * H^4 * (3 + nlength (H * Suc (2 * length zs)))^2 + 4 * nlength (2 + 2 * length zs)"
using linear_le_pow by simp
also have "... = 52 + 1855 * H ^ 4 * (3 + nlength (H * Suc (2 * length zs)))⇧2 +
4 * nlength (2 + 2 * length zs)"
by simp
also have "... ≤ 52 + 1855 * H ^ 4 * (3 + nlength (H * Suc (2 * length zs)))⇧2 +
4 * nlength (H * Suc (2 * length zs))"
proof -
have "2 + 2 * m ≤ H * Suc (2 * m)" if "m > 0" for m
using H H_mult(2) by (metis Suc_leD add_mono eval_nat_numeral(3) mult.commute mult_Suc_right)
then have "2 + 2 * length zs ≤ H * Suc (2 * length zs)"
using assms(2) by (metis less_nat_zero_code not_gr_zero)
then show ?thesis
using nlength_mono by simp
qed
also have "... ≤ 52 + 1855 * H ^ 4 * (3 + H * Suc (2 * length zs))⇧2 +
4 * nlength (H * Suc (2 * length zs))"
using nlength_le_n nlength_mono by simp
also have "... ≤ 52 + 1855 * H ^ 4 * (3 + H * Suc (2 * length zs))⇧2 +
4 * (H * Suc (2 * length zs))"
using nlength_le_n nlength_mono by (meson add_left_mono mult_le_cancel1)
also have "... = 52 + 1855 * H ^ 4 * (3^2 + 2 * 3 * H * Suc (2 * length zs) + H^2 * Suc (2 * length zs)^2) +
4 * (H * Suc (2 * length zs))"
by algebra
also have "... ≤ 52 + 1855 * H ^ 4 * (72 * H^2 * length zs^2) + 4 * (H * Suc (2 * length zs))"
proof -
have "3^2 + 2 * 3 * H * Suc (2 * length zs) + H^2 * Suc (2 * length zs)^2 =
9 + 6 * H * Suc (2 * length zs) + H^2 * Suc (2 * length zs)^2"
by simp
also have "... ≤ 9 + 6 * H^2 * Suc (2 * length zs) + H^2 * Suc (2 * length zs)^2"
using H linear_le_pow by (simp add: add_mono)
also have "... ≤ 9 + 6 * H^2 * Suc (2 * length zs)^2 + H^2 * Suc (2 * length zs)^2"
using linear_le_pow by (meson add_le_mono1 add_left_mono le_refl mult_le_mono zero_less_numeral)
also have "... = 9 + 7 * H^2 * Suc (2 * length zs)^2"
by simp
also have "... ≤ 9 + 7 * H^2 * 9 * length zs^2"
using ** by simp
also have "... = 9 + 63 * H^2 * length zs^2"
by simp
also have "... ≤ 9 * H^2 * length zs^2 + 63 * H^2 * length zs^2"
using assms(2) H by simp
also have "... = 72 * H^2 * length zs^2"
by simp
finally have "3^2 + 2 * 3 * H * Suc (2 * length zs) + H^2 * Suc (2 * length zs)^2 ≤ 72 * H^2 * length zs^2" .
then show ?thesis
using add_le_mono le_refl mult_le_mono2 by presburger
qed
also have "... = 52 + 133560 * H ^ 6 * length zs^2 + 4 * (H * Suc (2 * length zs))"
by simp
also have "... ≤ 52 + 133560 * H ^ 6 * length zs^2 + 4 * (H * 9 * length zs ^ 2)"
using ** by (smt (verit) add_left_mono mult.assoc mult_le_cancel1 power2_nat_le_imp_le)
also have "... = 52 + 133560 * H ^ 6 * length zs^2 + 36 * H * length zs ^ 2"
by simp
also have "... ≤ 52 + 133560 * H ^ 6 * length zs^2 + 36 * H^6 * length zs ^ 2"
using linear_le_pow by simp
also have "... = 52 + 133596 * H ^ 6 * length zs^2"
by simp
also have "... ≤ 52 * H ^ 6 * length zs^2 + 133596 * H ^ 6 * length zs^2"
using H assms(2) by simp
also have "... = 133648 * H ^ 6 * length zs^2"
by simp
finally have "?ttt ≤ 133648 * H ^ 6 * length zs^2" .
then have "transforms tm6 (tpsL t) ttt (tpsL6 t)"
using tm6 assms transforms_monotone by blast
then show ?thesis
using tpsL6_eq_tpsL by simp
qed
lemma tmL:
assumes "ttt = 133650 * H ^ 6 * length zs ^ 3 + 1"
shows "transforms tmL (tpsL 0) ttt (tpsL (length zs))"
unfolding tmL_def
proof (tform)
let ?t = "133648 * H ^ 6 * length zs^2"
show "⋀i. i < length zs ⟹ transforms tm6 (tpsL i) ?t (tpsL (Suc i))"
using tm6' by simp
have *: "read (tpsL t) ! 0 = ⌊zs⌋ (Suc t)" for t
using jk tapes_at_read'[symmetric, of 0 "tpsL t"] by (simp add: tpsL_def)
show "read (tpsL t) ! 0 ≠ □" if "t < length zs" for t
proof -
have "read (tpsL t) ! 0 = zs ! t"
using that * by simp
then show ?thesis
using that zs by auto
qed
show "¬ read (tpsL (length zs)) ! 0 ≠ □"
using * by simp
show "length zs * (?t + 2) + 1 ≤ ttt"
proof (cases "length zs = 0")
case True
then show ?thesis
using assms(1) by simp
next
case False
then have "1 ≤ H^6 * length zs ^ 2"
using H linear_le_pow by (simp add: Suc_leI)
then have "?t + 2 ≤ 133650 * H ^ 6 * length zs^2"
by simp
then have "length zs * (?t + 2) ≤ length zs * 133650 * H ^ 6 * length zs^2"
by simp
then have "length zs * (?t + 2) ≤ 133650 * H ^ 6 * length zs^3"
by (simp add: power2_eq_square power3_eq_cube)
then show ?thesis
using assms(1) by simp
qed
qed
lemma tmL':
assumes "ttt = 133650 * H ^ 6 * length zs ^ 3 + 1"
shows "transforms tmL tps0 ttt (tpsL (length zs))"
using assms tmL tpsL_eq_tps0 by simp
end
end
lemma transforms_tm_PHI6I:
fixes j :: tapeidx
fixes tps tps' :: "tape list" and ttt k H :: nat and zs :: "symbol list" and nss :: "nat list list"
assumes "length tps = k" and "1 < j" and "j + 7 < k"
and "H ≥ 3"
and "bit_symbols zs"
assumes
"tps ! 1 = nlltape nss"
"tps ! 0 = (⌊zs⌋, 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 := (⌊zs⌋, Suc (length zs)),
j := (⌊2 + 2 * length zs⌋⇩N, 1),
1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (2 + 2 * i)) H (zs ! i)) [0..<length zs]))]"
assumes "ttt = 133650 * H ^ 6 * length zs ^ 3 + 1"
shows "transforms (tm_PHI6 j) tps ttt tps'"
proof -
interpret loc: turing_machine_PHI6 j .
show ?thesis
using assms loc.tpsL_def loc.tmL' loc.tmL_eq_tm_PHI6 by simp
qed
subsection ‹A Turing machine for $\Phi_7$›
text ‹
The next Turing machine expects a number $idx$ on tape $j$, a number $H$ on tape
$j + 1$, and a number $numiter$ on tape $j + 6$. It appends to the CNF formula
on tape~$1$ the formula $\bigwedge_{t=0}^{numiter} \Upsilon(\gamma_{idx + 2t})$
with $\gamma_i = [iH, (i+1)H)$. This equals $\Phi_7$ if $idx = 2n + 4$ and
$numiter = p(n)$.
›
definition tm_PHI7 :: "tapeidx ⇒ machine" where
"tm_PHI7 j ≡
WHILE [] ; λrs. rs ! (j + 6) ≠ □ DO
tm_Upsilongamma j ;;
tm_extendl_erase 1 (j + 4) ;;
tm_plus_const 2 j ;;
tm_decr (j + 6)
DONE"
lemma tm_PHI7_tm:
assumes "0 < j" and "j + 6 < k" and "6 ≤ G" and "2 ≤ k"
shows "turing_machine k G (tm_PHI7 j)"
unfolding tm_PHI7_def
using tm_Upsilongamma_tm tm_decr_tm Nil_tm tm_extendl_erase_tm tm_plus_const_tm assms turing_machine_loop_turing_machine
by simp
locale turing_machine_tm_PHI7 =
fixes step :: nat and j :: tapeidx
begin
definition "tmL1 ≡ tm_Upsilongamma j"
definition "tmL2 ≡ tmL1 ;; tm_extendl_erase 1 (j + 4)"
definition "tmL4 ≡ tmL2 ;; tm_plus_const 2 j"
definition "tmL5 ≡ tmL4 ;; tm_decr (j + 6)"
definition "tmL ≡ WHILE [] ; λrs. rs ! (j + 6) ≠ □ DO tmL5 DONE"
lemma tmL_eq_tm_PHI7: "tmL = tm_PHI7 j"
unfolding tmL_def tmL5_def tmL4_def tmL2_def tmL1_def tm_PHI7_def by simp
context
fixes tps0 :: "tape list" and numiter H k idx :: nat and nss :: "nat list list"
assumes jk: "length tps0 = k" "1 < j" "j + 6 < k"
and H: "H ≥ 3"
assumes tps0:
"tps0 ! 1 = nlltape nss"
"tps0 ! j = (⌊idx⌋⇩N, 1)"
"tps0 ! (j + 1) = (⌊H⌋⇩N, 1)"
"tps0 ! (j + 2) = (⌊[]⌋, 1)"
"tps0 ! (j + 3) = (⌊[]⌋, 1)"
"tps0 ! (j + 4) = (⌊[]⌋, 1)"
"tps0 ! (j + 5) = (⌊[]⌋, 1)"
"tps0 ! (j + 6) = (⌊numiter⌋⇩N, 1)"
begin
lemma nlength_H: "nlength H ≥ 1"
using nlength_0 H by (metis dual_order.trans nlength_1_simp nlength_mono one_le_numeral)
definition tpsL :: "nat ⇒ tape list" where
"tpsL t ≡ tps0
[j := (⌊idx + 2 * t⌋⇩N, 1),
j + 6 := (⌊numiter - t⌋⇩N, 1),
1 := nlltape (nss @ concat (map (λt. nll_Upsilon (idx + 2 * t) H) [0..<t]))]"
lemma tpsL_eq_tps0: "tpsL 0 = tps0"
using tpsL_def tps0 by auto (metis list_update_id)
definition tpsL1 :: "nat ⇒ tape list" where
"tpsL1 t ≡ tps0
[j := (⌊idx + 2 * t⌋⇩N, 1),
j + 6 := (⌊numiter - t⌋⇩N, 1),
1 := nlltape (nss @ concat (map (λt. nll_Upsilon (idx + 2 * t) H) [0..<t])),
j + 4 := (⌊nll_Upsilon (idx + 2 * t) H⌋⇩N⇩L⇩L, 1)]"
lemma tmL1 [transforms_intros]:
assumes "t < numiter"
and "ttt = 205 * H * (nlength (idx + 2 * t) + nlength H)⇧2"
shows "transforms tmL1 (tpsL t) ttt (tpsL1 t)"
unfolding tmL1_def by (tform tps: H tps0 tpsL_def tpsL1_def jk time: assms(2))
definition tpsL2 :: "nat ⇒ tape list" where
"tpsL2 t ≡ tps0
[j := (⌊idx + 2 * t⌋⇩N, 1),
j + 6 := (⌊numiter - t⌋⇩N, 1),
1 := nlltape (nss @ concat (map (λt. nll_Upsilon (idx + 2 * t) H) [0..<t]) @ (nll_Upsilon (idx + 2 * t) H)),
j + 4 := (⌊[]⌋, 1)]"
lemma tmL2 [transforms_intros]:
assumes "t < numiter"
and "ttt = 11 + 205 * H * (nlength (idx + 2 * t) + nlength H)⇧2 +
4 * nlllength (nll_Upsilon (idx + 2 * t) H)"
shows "transforms tmL2 (tpsL t) ttt (tpsL2 t)"
unfolding tmL2_def by (tform tps: assms(1) H tps0 tpsL1_def tpsL2_def jk time: assms(2))
definition tpsL4 :: "nat ⇒ tape list" where
"tpsL4 t ≡ tps0
[j := (⌊idx + 2 * Suc t⌋⇩N, 1),
j + 6 := (⌊numiter - t⌋⇩N, 1),
1 := nlltape (nss @ concat (map (λt. nll_Upsilon (idx + 2 * t) H) [0..<t]) @ (nll_Upsilon (idx + 2 * t) H)),
j + 4 := (⌊[]⌋, 1)]"
lemma tmL4 [transforms_intros]:
assumes "t < numiter"
and "ttt = 21 + 205 * H * (nlength (idx + 2 * t) + nlength H)⇧2 +
4 * nlllength (nll_Upsilon (idx + 2 * t) H) + 4 * nlength (Suc (Suc (idx + 2 * t)))"
shows "transforms tmL4 (tpsL t) ttt (tpsL4 t)"
unfolding tmL4_def
proof (tform tps: assms(1) H tps0 tpsL2_def tpsL4_def jk time: assms(2))
show "tpsL4 t = (tpsL2 t)[j := (⌊idx + 2 * t + 2⌋⇩N, 1)]"
using tpsL4_def tpsL2_def jk by (simp add: list_update_swap[of j])
qed
definition tpsL5 :: "nat ⇒ tape list" where
"tpsL5 t ≡ tps0
[j := (⌊idx + 2 * Suc t⌋⇩N, 1),
j + 6 := (⌊numiter - Suc t⌋⇩N, 1),
1 := nlltape (nss @ concat (map (λt. nll_Upsilon (idx + 2 * t) H) [0..<t]) @ (nll_Upsilon (idx + 2 * t) H)),
j + 4 := (⌊[]⌋, 1)]"
lemma tmL5:
assumes "t < numiter"
and "ttt = 29 + 205 * H * (nlength (idx + 2 * t) + nlength H)⇧2 +
4 * nlllength (nll_Upsilon (idx + 2 * t) H) + 4 * nlength (Suc (Suc (idx + 2 * t))) +
2 * nlength (numiter - t)"
shows "transforms tmL5 (tpsL t) ttt (tpsL5 t)"
unfolding tmL5_def
proof (tform tps: assms(1) H tps0 tpsL4_def tpsL5_def jk time: assms(2))
show "tpsL5 t = (tpsL4 t)[j + 6 := (⌊numiter - t - 1⌋⇩N, 1)]"
using tpsL5_def tpsL4_def jk by (simp add: list_update_swap[of "j+6"])
qed
lemma tpsL5_eq_tpsL: "tpsL5 t = tpsL (Suc t)"
proof -
define tps where "tps = tps0
[j := (⌊idx + 2 * Suc t⌋⇩N, 1),
j + 6 := (⌊numiter - Suc t⌋⇩N, 1),
1 := nlltape (nss @ concat (map (λt. nll_Upsilon (idx + 2 * t) H) [0..<t]) @ (nll_Upsilon (idx + 2 * t) H))]"
then have "tps = tpsL (Suc t)"
using tpsL_def jk tps0 by simp
moreover have "tps = tpsL5 t"
proof -
have "tps ! (j + 4) = (⌊[]⌋, 1)"
using tps_def jk tps0 by simp
then have "tps[j + 4 := (⌊[]⌋, 1)] = tps"
using list_update_id[of _ "j+4"] by metis
then show ?thesis
unfolding tps_def using tpsL5_def by simp
qed
ultimately show ?thesis
by simp
qed
lemma tmL5' [transforms_intros]:
assumes "t < numiter"
and "ttt = 256 * H * (nlength (idx + 2 * numiter) + nlength H)⇧2"
shows "transforms tmL5 (tpsL t) ttt (tpsL (Suc t))"
proof -
let ?ttt = "29 + 205 * H * (nlength (idx + 2 * t) + nlength H)⇧2 +
4 * nlllength (nll_Upsilon (idx + 2 * t) H) + 4 * nlength (Suc (Suc (idx + 2 * t))) +
2 * nlength (numiter - t)"
have "?ttt ≤ 29 + 205 * H * (nlength (idx + 2 * t) + nlength H)⇧2 +
4 * nlllength (nll_Upsilon (idx + 2 * t) H) + 4 * nlength (Suc (Suc (idx + 2 * t))) +
2 * nlength numiter"
using nlength_mono by simp
also have "... ≤ 29 + 205 * H * (nlength (idx + 2 * t) + nlength H)⇧2 +
4 * H * (4 + nlength (idx + 2 * t) + nlength H) + 4 * nlength (Suc (Suc (idx + 2 * t))) +
2 * nlength numiter"
using nlllength_nll_Upsilon_le H by simp
also have "... ≤ 29 + 205 * H * (nlength (idx + 2 * t) + nlength H)⇧2 +
4 * H * (4 + nlength (idx + 2 * numiter) + nlength H) + 4 * nlength (Suc (Suc (idx + 2 * t))) +
2 * nlength numiter"
using nlength_mono assms(1) by simp
also have "... ≤ 29 + 205 * H * (nlength (idx + 2 * t) + nlength H)⇧2 +
4 * H * (4 + nlength (idx + 2 * numiter) + nlength H) + 4 * nlength (idx + 2 * numiter) +
2 * nlength numiter"
using nlength_mono assms(1) by simp
also have "... ≤ 29 + 205 * H * (nlength (idx + 2 * numiter) + nlength H)⇧2 +
4 * H * (4 + nlength (idx + 2 * numiter) + nlength H) + 4 * nlength (idx + 2 * numiter) +
2 * nlength numiter"
using nlength_mono assms(1) by simp
also have "... ≤ 29 + 205 * H * (nlength (idx + 2 * numiter) + nlength H)⇧2 +
4 * H * (4 + nlength (idx + 2 * numiter) + nlength H) + 6 * nlength (idx + 2 * numiter)"
using nlength_mono by simp
also have "... ≤ 29 + 205 * H * (nlength (idx + 2 * numiter) + nlength H)⇧2 +
4 * H * (4 + nlength (idx + 2 * numiter) + nlength H) + 6 * (nlength (idx + 2 * numiter) + nlength H)"
using nlength_mono by simp
also have "... = 29 + 205 * H * (nlength (idx + 2 * numiter) + nlength H)⇧2 +
16 * H + 4 * H * (nlength (idx + 2 * numiter) + nlength H) + 6 * (nlength (idx + 2 * numiter) + nlength H)"
by algebra
also have "... ≤ 29 + 205 * H * (nlength (idx + 2 * numiter) + nlength H)⇧2 +
16 * H + 4 * H * (nlength (idx + 2 * numiter) + nlength H) + 2 * H * (nlength (idx + 2 * numiter) + nlength H)"
proof -
have "6 ≤ 2 * H"
using H by simp
then show ?thesis
using mult_le_mono1 nat_add_left_cancel_le by presburger
qed
also have "... = 29 + 205 * H * (nlength (idx + 2 * numiter) + nlength H)⇧2 +
16 * H + 6 * H * (nlength (idx + 2 * numiter) + nlength H)"
by simp
also have "... ≤ 29 + 205 * H * (nlength (idx + 2 * numiter) + nlength H)⇧2 +
16 * H + 6 * H * (nlength (idx + 2 * numiter) + nlength H)^2"
using linear_le_pow by simp
also have "... = 29 + 211 * H * (nlength (idx + 2 * numiter) + nlength H)⇧2 + 16 * H"
by simp
also have "... ≤ 29 + 227 * H * (nlength (idx + 2 * numiter) + nlength H)⇧2"
using H nlength_0 by (simp add: Suc_leI)
also have "... ≤ 256 * H * (nlength (idx + 2 * numiter) + nlength H)⇧2"
using H nlength_0 by (simp add: Suc_leI)
finally have "?ttt ≤ ttt"
using assms(2) by simp
then have "transforms tmL5 (tpsL t) ttt (tpsL5 t)"
using assms(1) tmL5 transforms_monotone by blast
then show ?thesis
using tpsL5_eq_tpsL by simp
qed
lemma tmL:
assumes "ttt = numiter * (257 * H * (nlength (idx + 2 * numiter) + nlength H)⇧2) + 1"
shows "transforms tmL (tpsL 0) ttt (tpsL numiter)"
unfolding tmL_def
proof (tform)
show "⋀i. i < numiter ⟹ read (tpsL i) ! (j + 6) ≠ □"
using jk tpsL_def read_ncontents_eq_0 by simp
show "¬ read (tpsL numiter) ! (j + 6) ≠ □"
using jk tpsL_def read_ncontents_eq_0 by simp
show "numiter * (256 * H * (nlength (idx + 2 * numiter) + nlength H)⇧2 + 2) + 1 ≤ ttt"
proof -
have "1 ≤ (nlength (idx + 2 * numiter) + nlength H)⇧2"
using nlength_H by simp
then have "2 ≤ H * (nlength (idx + 2 * numiter) + nlength H)⇧2"
using H by (metis add_leE mult_2 mult_le_mono nat_1_add_1 numeral_Bit1 numerals(1))
then show ?thesis
using assms by simp
qed
qed
lemma tmL':
assumes "ttt = numiter * 257 * H * (nlength (idx + 2 * numiter) + nlength H)⇧2 + 1"
shows "transforms tmL tps0 ttt (tpsL numiter)"
using assms tmL tpsL_eq_tps0 by (simp add: Groups.mult_ac(1))
end
end
lemma transforms_tm_PHI7I:
fixes tps tps' :: "tape list" and ttt numiter H k idx :: nat and nss :: "nat list list" and j :: tapeidx
assumes "length tps = k" and "1 < j" and "j + 6 < k"
and "H ≥ 3"
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) = (⌊numiter⌋⇩N, 1)"
assumes "ttt = numiter * 257 * H * (nlength (idx + 2 * numiter) + nlength H)⇧2 + 1"
assumes "tps' = tps
[j := (⌊idx + 2 * numiter⌋⇩N, 1),
j + 6 := (⌊0⌋⇩N, 1),
1 := nlltape (nss @ concat (map (λt. nll_Upsilon (idx + 2 * t) H) [0..<numiter]))]"
shows "transforms (tm_PHI7 j) tps ttt tps'"
proof -
interpret loc: turing_machine_tm_PHI7 j .
show ?thesis
using assms loc.tmL' loc.tpsL_def loc.tmL_eq_tm_PHI7 by simp
qed
subsection ‹A Turing machine for $\Phi_8$›
text ‹
The next TM expects a number $idx$ on tape $j$ and a number $H$ on tape $j + 1$.
It appends to the formula on tape~$1$ the formula $\Psi([idx\cdot H, (idx+1)H),
3)$.
›
definition tm_PHI8 :: "tapeidx ⇒ machine" where
"tm_PHI8 j ≡
tm_setn (j + 2) 3 ;;
tm_Psigamma j ;;
tm_extendl 1 (j + 6)"
lemma tm_PHI8_tm:
assumes "0 < j" and "j + 7 < k" and "G ≥ 6"
shows "turing_machine k G (tm_PHI8 j)"
unfolding tm_PHI8_def using assms tm_Psigamma_tm tm_setn_tm tm_extendl_tm by simp
locale turing_machine_PHI8 =
fixes j :: tapeidx
begin
definition "tm1 ≡ tm_setn (j + 2) 3"
definition "tm2 ≡ tm1 ;; tm_Psigamma j"
definition "tm3 ≡ tm2 ;; tm_extendl 1 (j + 6)"
lemma tm3_eq_tm_PHI8: "tm3 = tm_PHI8 j"
using tm3_def tm2_def tm1_def tm_PHI8_def by simp
context
fixes tps0 :: "tape list" and k idx H :: nat and nss :: "nat list list"
assumes jk: "length tps0 = k" "1 < j" "j + 7 < k"
and H: "H ≥ 3"
assumes tps0:
"tps0 ! 1 = nlltape nss"
"tps0 ! j = (⌊idx⌋⇩N, 1)"
"tps0 ! (j + 1) = (⌊H⌋⇩N, 1)"
"tps0 ! (j + 2) = (⌊[]⌋, 1)"
"tps0 ! (j + 3) = (⌊[]⌋, 1)"
"tps0 ! (j + 4) = (⌊[]⌋, 1)"
"tps0 ! (j + 5) = (⌊[]⌋, 1)"
"tps0 ! (j + 6) = (⌊[]⌋, 1)"
"tps0 ! (j + 7) = (⌊[]⌋, 1)"
begin
definition "tps1 ≡ tps0
[j + 2 := (⌊3⌋⇩N, 1)]"
lemma tm1 [transforms_intros]:
assumes "ttt = 14"
shows "transforms tm1 tps0 ttt tps1"
unfolding tm1_def
proof (tform tps: tps0 tps1_def jk)
show "tps0 ! (j + 2) = (⌊0⌋⇩N, 1)"
using tps0 jk canrepr_0 by simp
show "ttt = 10 + 2 * nlength 0 + 2 * nlength 3"
using assms nlength_3 by simp
qed
definition "tps2 ≡ tps0
[j + 2 := (⌊3⌋⇩N, 1),
j + 6 := (⌊nll_Psi (idx * H) H 3⌋⇩N⇩L⇩L, 1)]"
lemma tm2 [transforms_intros]:
assumes "ttt = 14 + 1851 * H ^ 4 * nlength (Suc idx) ^ 2"
shows "transforms tm2 tps0 ttt tps2"
unfolding tm2_def by (tform tps: tps0 H tps1_def tps2_def jk time: assms canrepr_1)
definition "tps3 ≡ tps0
[1 := nlltape (nss @ nll_Psi (idx * H) H 3),
j + 2 := (⌊3⌋⇩N, 1),
j + 6 := (⌊nll_Psi (idx * H) H 3⌋⇩N⇩L⇩L, 1)]"
lemma tm3:
assumes "ttt = 18 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 +
2 * nlllength (nll_Psi (idx * H) H 3)"
shows "transforms tm3 tps0 ttt tps3"
unfolding tm3_def by (tform tps: tps0 H tps2_def tps3_def jk time: assms)
lemma tm3':
assumes "ttt = 18 + 1861 * H ^ 4 * (nlength (Suc idx))⇧2"
shows "transforms tm3 tps0 ttt tps3"
proof -
have *: "(nlength (Suc idx))⇧2 ≥ 1"
using nlength_0 by (simp add: Suc_leI)
let ?ttt = "18 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 + 2 * nlllength (nll_Psi (idx * H) H 3)"
have "?ttt ≤ 18 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 + 2 * H * (3 + nlength (idx * H + H))"
using nlllength_nll_Psi_le by simp
also have "... = 18 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 + 2 * H * (3 + nlength (Suc idx * H))"
by (simp add: add.commute)
also have "... ≤ 18 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 + 2 * H * (3 + nlength (Suc idx) + nlength H)"
using nlength_prod by (metis (mono_tags, lifting) ab_semigroup_add_class.add_ac(1) add_left_mono mult_le_cancel1)
also have "... = 18 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 + 6 * H + 2 * H * nlength (Suc idx) + 2 * H * nlength H"
by algebra
also have "... ≤ 18 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 + 6 * H + 2 * H * nlength (Suc idx) + 2 * H * H"
using nlength_le_n by simp
also have "... ≤ 18 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 + 6 * H ^ 4 + 2 * H * nlength (Suc idx) + 2 * H * H"
using linear_le_pow[of 4 H] by simp
also have "... ≤ 18 + 1851 * H ^ 4 * (nlength (Suc idx))⇧2 + 6 * H ^ 4 + 2 * H ^ 4 * nlength (Suc idx) + 2 * H * H"
using linear_le_pow[of 4 H] by simp
also have "... ≤ 18 + 1857 * H ^ 4 * (nlength (Suc idx))⇧2 + 2 * H ^ 4 * nlength (Suc idx) + 2 * H * H"
using * by simp
also have "... ≤ 18 + 1859 * H ^ 4 * (nlength (Suc idx))⇧2 + 2 * H * H"
using linear_le_pow[of 2 "nlength (Suc idx)"] by simp
also have "... = 18 + 1859 * H ^ 4 * (nlength (Suc idx))⇧2 + 2 * H ^ 2"
by algebra
also have "... ≤ 18 + 1859 * H ^ 4 * (nlength (Suc idx))⇧2 + 2 * H ^ 4"
using pow_mono'[of 2 4 H] by simp
also have "... ≤ 18 + 1861 * H ^ 4 * (nlength (Suc idx))⇧2"
using * by simp
finally have "?ttt ≤ 18 + 1861 * H ^ 4 * (nlength (Suc idx))⇧2" .
then show ?thesis
using tm3 assms transforms_monotone by simp
qed
end
end
lemma transforms_tm_PHI8I:
fixes j :: tapeidx
fixes tps tps' :: "tape list" and ttt k idx H :: nat and nss :: "nat list list"
assumes "length tps = k" and "1 < j" and "j + 7 < k"
and "H ≥ 3"
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)"
assumes "tps' = tps
[1 := nlltape (nss @ nll_Psi (idx * H) H 3),
j + 2 := (⌊3⌋⇩N, 1),
j + 6 := (⌊nll_Psi (idx * H) H 3⌋⇩N⇩L⇩L, 1)]"
assumes "ttt = 18 + 1861 * H ^ 4 * (nlength (Suc idx))⇧2"
shows "transforms (tm_PHI8 j) tps ttt tps'"
proof -
interpret loc: turing_machine_PHI8 j .
show ?thesis
using loc.tps3_def loc.tm3' loc.tm3_eq_tm_PHI8 assms by metis
qed
subsection ‹A Turing machine for $\Phi_9$›
text ‹
The CNF formula $\Phi_9 = \bigwedge_{t=1}^{T'}$ is the most complicated part of
$\Phi$. Clearly, the main task here is to generate the formulas $\chi_t$
›
subsubsection ‹A Turing machine for $\chi_t$›
text ‹
A lemma that will help with some time bounds:
›
lemma pow2_le_2pow2: "z ^ 2 ≤ 2 ^ (2*z)" for z :: nat
proof (induction z)
case 0
then show ?case
by simp
next
case (Suc z)
show ?case
proof (cases "z = 0")
case True
then show ?thesis
by simp
next
case False
have "Suc z ^ 2 = z ^ 2 + 2 * z + 1"
by (metis Suc_eq_plus1 ab_semigroup_add_class.add_ac(1) nat_mult_1_right one_power2 plus_1_eq_Suc power2_sum)
also have "... ≤ z ^ 2 + 3 * z"
using False by simp
also have "... ≤ z ^ 2 + 3 * z ^ 2"
by (simp add: linear_le_pow)
also have "... = 2^2 * z ^ 2"
by simp
also have "... ≤ 2^2 * 2 ^ (2 * z)"
using Suc by simp
also have "... = 2 ^ (2 * Suc z)"
by (simp add: power_add)
finally show ?thesis .
qed
qed
text ‹
The next Turing machine can be used to generate $\chi_t$. It expects on tape~1 a
CNF formula, on tape~$j_1$ the list of positions of $M$'s input tape head, on
tape~$j_2$ the list of positions of $M$'s output tape head, on tapes~$j_3,
\dots, j_3+3$ the numbers $N$, $G$, $Z$, and $T$, on tape~$j_3+4$ the formula
$\psi$, on tape~$j_3+5$ the formula $\psi'$, and finally on tape~$j_3+6$ the
number $t$. The TM appends the formula $\chi_t$ to the formula on tape~1, which
should be thought of as an unfinished version of $\Phi$.
The TM first computes $\prev(t)$ using @{const tm_prev} and compares it with
$t$. Depending on the outcome of this comparison it generates either $\rho_t$ or
$\rho'_t$ by concatenating ranges of numbers generated using @{const tm_range}.
Then the TM uses @{const tm_relabel} to compute $\rho_t(\psi)$ or
$\rho'_t(\psi')$. The result equals $\chi_t$ and is appended to tape~1. Finally
$t$ is incremented and $T$ is decremented. This is so the TM can be used inside
a while loop that initializes $T$ with $T'$ and $t$ with $1$.
\null
›
definition tm_chi :: "tapeidx ⇒ tapeidx ⇒ tapeidx ⇒ machine" where
"tm_chi j1 j2 j3 ≡
tm_prev j2 (j3 + 6) ;;
tm_equalsn (j3 + 11) (j3 + 6) (j3 + 13) ;;
tm_decr (j3 + 6) ;;
tm_mult (j3 + 6) (j3 + 2) (j3 + 7) ;;
tm_add j3 (j3 + 7) ;;
tm_range (j3 + 7) (j3 + 2) (j3 + 8) ;;
tm_extend_erase (j3 + 12) (j3 + 8) ;;
tm_setn (j3 + 7) 0 ;;
IF λrs. rs ! (j3 + 13) = □ THEN
tm_mult (j3 + 11) (j3 + 2) (j3 + 7) ;;
tm_add j3 (j3 + 7) ;;
tm_range (j3 + 7) (j3 + 2) (j3 + 8) ;;
tm_extend_erase (j3 + 12) (j3 + 8) ;;
tm_setn (j3 + 7) 0
ELSE
[]
ENDIF ;;
tm_incr (j3 + 6) ;;
tm_mult (j3 + 6) (j3 + 2) (j3 + 7) ;;
tm_add j3 (j3 + 7) ;;
tm_range (j3 + 7) (j3 + 2) (j3 + 8) ;;
tm_extend_erase (j3 + 12) (j3 + 8) ;;
tm_setn (j3 + 11) 0 ;;
tm_nth j1 (j3 + 6) (j3 + 11) 4 ;;
tm_setn (j3 + 7) 0 ;;
tm_mult (j3 + 11) (j3 + 1) (j3 + 7) ;;
tm_range (j3 + 7) (j3 + 1) (j3 + 8) ;;
tm_extend_erase (j3 + 12) (j3 + 8) ;;
tm_setn (j3 + 7) 0 ;;
tm_erase_cr (j3 + 11) ;;
tm_cr (j3 + 12) ;;
IF λrs. rs ! (j3 + 13) = □ THEN
tm_relabel (j3 + 4) (j3 + 11)
ELSE
tm_erase_cr (j3 + 13) ;;
tm_relabel (j3 + 5) (j3 + 11)
ENDIF ;;
tm_erase_cr (j3 + 12) ;;
tm_extendl_erase 1 (j3 + 11) ;;
tm_incr (j3 + 6) ;;
tm_decr (j3 + 3)"
lemma tm_chi_tm:
assumes "0 < j1" and "j1 < j2" and "j2 < j3" and "j3 + 17 < k" and "G ≥ 6"
shows "turing_machine k G (tm_chi j1 j2 j3)"
unfolding tm_chi_def
using tm_prev_tm tm_equalsn_tm tm_decr_tm tm_mult_tm tm_add_tm tm_range_tm tm_extend_erase_tm
tm_setn_tm tm_incr_tm tm_nth_tm tm_erase_cr_tm tm_relabel_tm Nil_tm tm_cr_tm tm_extendl_erase_tm
assms turing_machine_branch_turing_machine
by simp
locale turing_machine_chi =
fixes j1 j2 j3 :: tapeidx
begin
definition "tm1 ≡ tm_prev j2 (j3 + 6)"
definition "tm2 ≡ tm1 ;; tm_equalsn (j3 + 11) (j3 + 6) (j3 + 13)"
definition "tm3 ≡ tm2 ;; tm_decr (j3 + 6)"
definition "tm4 ≡ tm3 ;; tm_mult (j3 + 6) (j3 + 2) (j3 + 7)"
definition "tm5 ≡ tm4 ;; tm_add j3 (j3 + 7)"
definition "tm6 ≡ tm5 ;; tm_range (j3 + 7) (j3 + 2) (j3 + 8)"
definition "tm7 ≡ tm6 ;; tm_extend_erase (j3 + 12) (j3 + 8)"
definition "tm8 ≡ tm7 ;; tm_setn (j3 + 7) 0"
definition "tmT1 ≡ tm_mult (j3 + 11) (j3 + 2) (j3 + 7)"
definition "tmT2 ≡ tmT1 ;; tm_add j3 (j3 + 7)"
definition "tmT3 ≡ tmT2 ;; tm_range (j3 + 7) (j3 + 2) (j3 + 8)"
definition "tmT4 ≡ tmT3 ;; tm_extend_erase (j3 + 12) (j3 + 8)"
definition "tmT5 ≡ tmT4 ;; tm_setn (j3 + 7) 0"
definition "tm89 ≡ IF λrs. rs ! (j3 + 13) = □ THEN tmT5 ELSE [] ENDIF"
definition "tm10 ≡ tm8 ;; tm89"
definition "tm11 ≡ tm10 ;; tm_incr (j3 + 6)"
definition "tm13 ≡ tm11 ;; tm_mult (j3 + 6) (j3 + 2) (j3 + 7)"
definition "tm14 ≡ tm13 ;; tm_add j3 (j3 + 7)"
definition "tm15 ≡ tm14 ;; tm_range (j3 + 7) (j3 + 2) (j3 + 8)"
definition "tm16 ≡ tm15 ;; tm_extend_erase (j3 + 12) (j3 + 8)"
definition "tm17 ≡ tm16 ;; tm_setn (j3 + 11) 0"
definition "tm18 ≡ tm17 ;; tm_nth j1 (j3 + 6) (j3 + 11) 4"
definition "tm19 ≡ tm18 ;; tm_setn (j3 + 7) 0"
definition "tm20 ≡ tm19 ;; tm_mult (j3 + 11) (j3 + 1) (j3 + 7)"
definition "tm21 ≡ tm20 ;; tm_range (j3 + 7) (j3 + 1) (j3 + 8)"
definition "tm22 ≡ tm21 ;; tm_extend_erase (j3 + 12) (j3 + 8)"
definition "tm23 ≡ tm22 ;; tm_setn (j3 + 7) 0"
definition "tm24 ≡ tm23 ;; tm_erase_cr (j3 + 11)"
definition "tm25 ≡ tm24 ;; tm_cr (j3 + 12)"
definition "tmE1 ≡ tm_erase_cr (j3 + 13)"
definition "tmE2 ≡ tmE1 ;; tm_relabel (j3 + 5) (j3 + 11)"
definition "tmTT1 ≡ tm_relabel (j3 + 4) (j3 + 11)"
definition "tm2526 ≡ IF λrs. rs ! (j3 + 13) = □ THEN tmTT1 ELSE tmE2 ENDIF"
definition "tm26 ≡ tm25 ;; tm2526"
definition "tm27 ≡ tm26 ;; tm_erase_cr (j3 + 12)"
definition "tm28 ≡ tm27 ;; tm_extendl_erase 1 (j3 + 11)"
definition "tm29 ≡ tm28 ;; tm_incr (j3 + 6)"
definition "tm30 ≡ tm29 ;; tm_decr (j3 + 3)"
lemma tm30_eq_tm_chi: "tm30 = tm_chi j1 j2 j3"
unfolding tm30_def tm29_def tm28_def tm27_def tm26_def tm25_def tm24_def tm23_def tm22_def tm21_def tm20_def
tm19_def tm18_def tm17_def tm16_def tm15_def tm14_def tm13_def tm11_def tm10_def
tm8_def tm7_def tm6_def tm5_def tm4_def tm3_def tm2_def tm1_def
tm89_def tmE1_def tmE2_def tmTT1_def tm2526_def
tmT5_def tmT4_def tmT3_def tmT2_def tmT1_def
tm_chi_def
by simp
context
fixes tps0 :: "tape list" and k G N Z T' T t :: nat and hp0 hp1 :: "nat list" and ψ ψ' :: formula
fixes nss :: "nat list list"
assumes jk: "length tps0 = k" "1 < j1" "j1 < j2" "j2 < j3" "j3 + 17 < k"
and G: "G ≥ 3"
and Z: "Z = 3 * G"
and N: "N ≥ 1"
and len_hp0: "length hp0 = Suc T'"
and hp0: "∀i<length hp0. hp0 ! i ≤ T'"
and len_hp1: "length hp1 = Suc T'"
and hp1: "∀i<length hp1. hp1 ! i ≤ T'"
and t: "0 < t" "t ≤ T'"
and T: "0 < T" "T ≤ T'"
and T': "T' < N"
and psi: "variables ψ ⊆ {..<3*Z+G}" "fsize ψ ≤ (3*Z+G) * 2 ^ (3*Z+G)" "length ψ ≤ 2 ^ (3*Z+G)"
and psi': "variables ψ' ⊆ {..<2*Z+G}" "fsize ψ' ≤ (2*Z+G) * 2 ^ (2*Z+G)" "length ψ' ≤ 2 ^ (2*Z+G)"
assumes tps0:
"tps0 ! 1 = nlltape nss"
"tps0 ! j1 = (⌊hp0⌋⇩N⇩L, 1)"
"tps0 ! j2 = (⌊hp1⌋⇩N⇩L, 1)"
"tps0 ! j3 = (⌊N⌋⇩N, 1)"
"tps0 ! (j3 + 1) = (⌊G⌋⇩N, 1)"
"tps0 ! (j3 + 2) = (⌊Z⌋⇩N, 1)"
"tps0 ! (j3 + 3) = (⌊T⌋⇩N, 1)"
"tps0 ! (j3 + 4) = (⌊formula_n ψ⌋⇩N⇩L⇩L, 1)"
"tps0 ! (j3 + 5) = (⌊formula_n ψ'⌋⇩N⇩L⇩L, 1)"
"tps0 ! (j3 + 6) = (⌊t⌋⇩N, 1)"
"⋀i. 6 < i ⟹ i < 17 ⟹ tps0 ! (j3 + i) = (⌊[]⌋, 1)"
begin
lemma Z_ge_1: "Z ≥ 1"
using G Z by simp
lemma Z_ge_9: "Z ≥ 9"
using G Z by simp
lemma T'_ge_1: "T' ≥ 1"
using t by simp
lemma tps0': "⋀i. 1 ≤ i ⟹ i < 11 ⟹ tps0 ! (j3 + 6 + i) = (⌊[]⌋, 1)"
proof -
fix i :: nat
assume i: "1 ≤ i" "i < 11"
then have "6 < 6 + i" "6 + i < 17"
by simp_all
then have "tps0 ! (j3 + (6 + i)) = (⌊[]⌋, 1)"
using tps0(11) by simp
then show "tps0 ! (j3 + 6 + i) = (⌊[]⌋, 1)"
by (metis group_cancel.add1)
qed
text ‹The simplifier turns $j3 + 6 + 3$ into $9 + j3$. The next lemma helps with that.›
lemma tps0_sym: "⋀i. 6 < i ⟹ i < 17 ⟹ tps0 ! (i + j3) = (⌊[]⌋, 1)"
using tps0(11) by (simp add: add.commute)
lemma previous_hp1_le: "previous hp1 t ≤ t"
using len_hp1 hp1 t(2) previous_le[of hp1 t] by simp
definition "tps1 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1)]"
lemma tm1 [transforms_intros]:
assumes "ttt = 71 + 153 * nllength hp1 ^ 3"
shows "transforms tm1 tps0 ttt tps1"
unfolding tm1_def
proof (tform tps: canrepr_0 tps0_sym tps0 tps1_def jk t len_hp1 time: assms)
show "tps1 = tps0[j3 + 6 + 5 := (⌊previous hp1 t⌋⇩N, 1)]"
using tps1_def by (simp add: add.commute)
qed
definition "tps2 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1)]"
lemma tm2 [transforms_intros]:
assumes "ttt = 78 + 153 * nllength hp1 ^ 3 + 3 * nlength (min (previous hp1 t) t)"
shows "transforms tm2 tps0 ttt tps2"
unfolding tm2_def
proof (tform tps: tps0 tps1_def tps2_def jk time: assms)
show "tps1 ! (j3 + 13) = (⌊0⌋⇩N, 1)"
using tps1_def tps0(11) canrepr_0 by simp
show "(0::nat) ≤ 1"
by simp
qed
definition "tps3 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t - 1⌋⇩N, 1)]"
lemma tm3 [transforms_intros]:
assumes "ttt = 86 + 153 * nllength hp1 ^ 3 + 3 * nlength (min (previous hp1 t) t) + 2 * nlength t"
shows "transforms tm3 tps0 ttt tps3"
unfolding tm3_def by (tform tps: tps0 tps2_def tps3_def jk assms)
definition "tps4 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t - 1⌋⇩N, 1),
j3 + 7 := (⌊(t - 1) * Z⌋⇩N, 1)]"
lemma tm4 [transforms_intros]:
assumes "ttt = 90 + 153 * nllength hp1 ^ 3 + 3 * nlength (min (previous hp1 t) t) + 2 * nlength t +
26 * (nlength (t - 1) + nlength Z) ^ 2"
shows "transforms tm4 tps0 ttt tps4"
unfolding tm4_def
proof (tform tps: tps0 tps3_def tps4_def jk)
show "tps3 ! (j3 + 7) = (⌊0⌋⇩N, 1)"
using tps3_def jk canrepr_0 tps0 by simp
show "ttt = 86 + 153 * nllength hp1 ^ 3 + 3 * nlength (min (previous hp1 t) t) +
2 * nlength t + (4 + 26 * (nlength (t - Suc 0) + nlength Z) * (nlength (t - Suc 0) + nlength Z))"
proof -
have "(26 * nlength (t - Suc 0) + 26 * nlength Z) * (nlength (t - Suc 0) + nlength Z) =
26 * (nlength (t - Suc 0) + nlength Z) ^ 2"
by algebra
then show ?thesis
using assms by simp
qed
qed
definition "tps5 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t - 1⌋⇩N, 1),
j3 + 7 := (⌊N + (t - 1) * Z⌋⇩N, 1)]"
lemma tm5 [transforms_intros]:
assumes "ttt = 100 + 153 * nllength hp1 ^ 3 + 3 * nlength (min (previous hp1 t) t) + 2 * nlength t +
26 * (nlength (t - 1) + nlength Z) ^ 2 + 3 * max (nlength N) (nlength ((t - 1) * Z))"
shows "transforms tm5 tps0 ttt tps5"
unfolding tm5_def by (tform tps: tps0 tps4_def tps5_def jk time: assms)
definition "tps6 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t - 1⌋⇩N, 1),
j3 + 7 := (⌊N + (t - 1) * Z⌋⇩N, 1),
j3 + 8 := (⌊[N + (t - 1) * Z..<N + (t - 1) * Z + Z]⌋⇩N⇩L, 1)]"
lemma tm6 [transforms_intros]:
assumes "ttt = 100 + 153 * nllength hp1 ^ 3 + 3 * nlength (min (previous hp1 t) t) + 2 * nlength t +
26 * (nlength (t - 1) + nlength Z) ^ 2 + 3 * max (nlength N) (nlength ((t - 1) * Z)) +
Suc Z * (43 + 9 * nlength (N + (t - 1) * Z + Z))"
shows "transforms tm6 tps0 ttt tps6"
unfolding tm6_def
by (tform tps: nlcontents_Nil canrepr_0 tps0_sym tps0 tps5_def tps6_def jk time: assms)
definition "tps7 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t - 1⌋⇩N, 1),
j3 + 7 := (⌊N + (t - 1) * Z⌋⇩N, 1),
j3 + 12 := nltape [N + (t - 1) * Z..<N + (t - 1) * Z + Z]]"
lemma tm7 [transforms_intros]:
assumes "ttt = 111 + 153 * nllength hp1 ^ 3 + 3 * nlength (min (previous hp1 t) t) + 2 * nlength t +
26 * (nlength (t - 1) + nlength Z) ^ 2 + 3 * max (nlength N) (nlength ((t - 1) * Z)) +
Suc Z * (43 + 9 * nlength (N + (t - 1) * Z + Z)) +
4 * nllength [N + (t - Suc 0) * Z..<N + (t - Suc 0) * Z + Z]"
shows "transforms tm7 tps0 ttt tps7"
unfolding tm7_def
proof (tform tps: tps0 tps6_def tps7_def jk time: assms)
show "tps6 ! (j3 + 12) = nltape []"
using tps6_def jk nlcontents_Nil tps0 by force
show "tps7 = tps6
[j3 + 12 := nltape ([] @ [N + (t - Suc 0) * Z..<N + (t - Suc 0) * Z + Z]),
j3 + 8 := (⌊[]⌋, 1)]"
unfolding tps7_def tps6_def
using tps0 jk list_update_id[of tps0 "j3 + 8"]
by (simp add: list_update_swap)
qed
definition "tps8 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t - 1⌋⇩N, 1),
j3 + 7 := (⌊0⌋⇩N, 1),
j3 + 12 := nltape [N + (t - 1) * Z..<N + (t - 1) * Z + Z]]"
lemma tm8:
assumes "ttt = 121 + 153 * nllength hp1 ^ 3 + 3 * nlength (min (previous hp1 t) t) +
2 * nlength t + 26 * (nlength (t - 1) + nlength Z) ^ 2 + 3 * max (nlength N) (nlength ((t - 1) * Z)) +
Suc Z * (43 + 9 * nlength (N + (t - 1) * Z + Z)) + 4 * nllength [N + (t - 1) * Z..<N + (t - 1) * Z + Z] +
2 * nlength (N + (t - 1) * Z)"
shows "transforms tm8 tps0 ttt tps8"
unfolding tm8_def by (tform tps: tps0 tps7_def tps8_def jk time: assms)
text ‹
For the next upper bound we have no scruples replacing $\log T'$, $\log N$, and
$\log Z$ by $T'$, $N$ and $Z$, respectively. All values are polynomial in $n$
($Z$ is even a constant), so the overall polynomiality is not in jeopardy.
›
lemma nllength_le:
fixes nmax :: nat and ns :: "nat list"
assumes "∀n∈set ns. n ≤ nmax"
shows "nllength ns ≤ Suc nmax * length ns"
proof -
have "nllength ns ≤ Suc (nlength nmax) * length ns"
using assms nllength_le_len_mult_max by simp
then show ?thesis
using nlength_le_n by (meson Suc_le_mono dual_order.trans mult_le_mono1)
qed
lemma nllength_upt_le:
fixes a b :: nat
shows "nllength [a..<b] ≤ Suc b * (b - a)"
proof -
have "nllength [a..<b] ≤ Suc (nlength b) * (b - a)"
using nllength_upt_le_len_mult_max by simp
then show ?thesis
using nlength_le_n by (meson Suc_le_mono dual_order.trans mult_le_mono1)
qed
lemma nllength_hp1: "nllength hp1 ≤ Suc T' * Suc T'"
proof -
have "∀n∈set hp1. n ≤ T'"
using hp1 by (metis in_set_conv_nth)
then have "nllength hp1 ≤ Suc T' * Suc T'"
using nllength_le[of hp1 T'] len_hp1 by simp
then show ?thesis
by simp
qed
definition "ttt8 ≡ 168 + 153 * Suc T' ^ 6 + 5 * t + 26 * (t + Z) ^ 2 + 47 * Z + 15 * Z * (N + t * Z)"
lemma tm8' [transforms_intros]: "transforms tm8 tps0 ttt8 tps8"
proof -
let ?s = "88 + 153 * nllength hp1 ^ 3 + 3 * nlength (min (previous hp1 t) t) + 2 * nlength (N + (t - 1) * Z)"
let ?ttt = "121 + 153 * nllength hp1 ^ 3 + 3 * nlength (min (previous hp1 t) t) +
2 * nlength t + 26 * (nlength (t - 1) + nlength Z) ^ 2 + 3 * max (nlength N) (nlength ((t - 1) * Z)) +
Suc Z * (43 + 9 * nlength (N + (t - 1) * Z + Z)) + 4 * nllength [N + (t - 1) * Z..<N + (t - 1) * Z + Z] +
2 * nlength (N + (t - 1) * Z)"
have "?ttt = ?s + 33 + 2 * nlength t + 26 * (nlength (t - 1) + nlength Z) ^ 2 + 3 * max (nlength N) (nlength ((t - 1) * Z)) +
Suc Z * (43 + 9 * nlength (N + (t - 1) * Z + Z)) + 4 * nllength [N + (t - 1) * Z..<N + (t - 1) * Z + Z]"
by simp
also have "... ≤ ?s + 33 + 2 * t + 26 * (nlength (t - 1) + nlength Z) ^ 2 +
3 * max (nlength N) (nlength ((t - 1) * Z)) + Suc Z * (43 + 9 * nlength (N + (t - 1) * Z + Z)) +
4 * nllength [N + (t - 1) * Z..<N + (t - 1) * Z + Z]"
using nlength_le_n by simp
also have "... ≤ ?s + 33 + 2 * t + 26 * ((t - 1) + nlength Z) ^ 2 +
3 * max (nlength N) (nlength ((t - 1) * Z)) + Suc Z * (43 + 9 * nlength (N + (t - 1) * Z + Z)) +
4 * nllength [N + (t - 1) * Z..<N + (t - 1) * Z + Z]"
using nlength_le_n by simp
also have "... ≤ ?s + 33 + 2 * t + 26 * ((t - 1) + Z) ^ 2 +
3 * max (nlength N) (nlength ((t - 1) * Z)) + Suc Z * (43 + 9 * nlength (N + (t - 1) * Z + Z)) +
4 * nllength [N + (t - 1) * Z..<N + (t - 1) * Z + Z]"
using nlength_le_n by simp
also have "... ≤ ?s + 33 + 2 * t + 26 * ((t - 1) + Z) ^ 2 +
3 * max (nlength N) (nlength ((t - 1) * Z)) + Suc Z * (43 + 9 * (N + (t - 1) * Z + Z)) +
4 * nllength [N + (t - 1) * Z..<N + (t - 1) * Z + Z]"
using nlength_le_n add_le_mono le_refl mult_le_mono by presburger
also have "... ≤ ?s + 33 + 2 * t + 26 * ((t - 1) + Z) ^ 2 +
3 * max (nlength N) (nlength ((t - 1) * Z)) + Suc Z * (43 + 9 * (N + (t - 1) * Z + Z)) +
4 * Suc (nlength (N + (t - 1) * Z + Z)) * Z"
proof -
have "nllength [N + (t - 1) * Z..<N + (t - 1) * Z + Z] ≤ Suc (nlength (N + (t - 1) * Z + Z)) * Z"
using nllength_le_len_mult_max[of "[N + (t - 1) * Z..<N + (t - 1) * Z + Z]" "N + (t - 1) * Z + Z"]
by simp
then show ?thesis
by linarith
qed
also have "... = ?s + 33 + 2 * t + 26 * ((t - 1) + Z) ^ 2 +
3 * nlength (max N ((t - 1) * Z)) + Suc Z * (43 + 9 * (N + (t - 1) * Z + Z)) +
4 * Suc (nlength (N + (t - 1) * Z + Z)) * Z"
using max_nlength by simp
also have "... ≤ ?s + 33 + 2 * t + 26 * ((t - 1) + Z) ^ 2 +
3 * max N ((t - 1) * Z) + Suc Z * (43 + 9 * (N + (t - 1) * Z + Z)) +
4 * Suc (nlength (N + (t - 1) * Z + Z)) * Z"
using nlength_le_n by simp
also have "... = ?s + 33 + 2 * t + 26 * ((t - 1) + Z) ^ 2 +
3 * max N ((t - 1) * Z) + Suc Z * (43 + 9 * (N + t * Z)) +
4 * Suc (nlength (N + (t - 1) * Z + Z)) * Z"
using t by (smt (verit) ab_semigroup_add_class.add_ac(1) add.commute diff_Suc_1 gr0_implies_Suc mult_Suc)
also have "... ≤ ?s + 33 + 2 * t + 26 * ((t - 1) + Z) ^ 2 +
3 * max N ((t - 1) * Z) + Suc Z * (43 + 9 * (N + t * Z)) +
4 * Suc (N + (t - 1) * Z + Z) * Z"
using nlength_le_n Suc_le_mono add_le_mono le_refl mult_le_mono by presburger
also have "... = ?s + 33 + 2 * t + 26 * ((t - 1) + Z) ^ 2 +
3 * max N ((t - 1) * Z) + Suc Z * (43 + 9 * (N + t * Z)) +
4 * Suc (N + t * Z) * Z"
by (smt (verit, del_insts) Suc_eq_plus1 Suc_leI add.commute add.left_commute add_leD2 le_add_diff_inverse mult.commute mult_Suc_right t(1))
also have "... ≤ ?s + 33 + 2 * t + 26 * ((t - 1) + Z) ^ 2 +
3 * (N + ((t - 1) * Z)) + Suc Z * (43 + 9 * (N + t * Z)) + 4 * Suc (N + t * Z) * Z"
by simp
also have "... ≤ ?s + 33 + 2 * t + 26 * ((t - 1) + Z) ^ 2 +
3 * (N + t * Z) + Suc Z * (43 + 9 * (N + t * Z)) + 4 * Suc (N + t * Z) * Z"
by simp
also have "... = ?s + 33 + 2 * t + 26 * ((t - 1) + Z) ^ 2 +
3 * (N + t * Z) + Suc Z * (43 + 9 * (N + t * Z)) + (4 + 4 * (N + t * Z)) * Z"
by simp
also have "... ≤ ?s + 33 + 2 * t + 26 * ((t - 1) + Z) ^ 2 +
3 * (N + t * Z) + Suc Z * (43 + 9 * (N + t * Z)) + (4 + 4 * (N + t * Z)) * Suc Z"
by simp
also have "... = ?s + 33 + 2 * t + 26 * ((t - 1) + Z) ^ 2 + 3 * (N + t * Z) + Suc Z * (47 + 13 * (N + t * Z))"
by algebra
also have "... = 121 + 153 * nllength hp1 ^ 3 + 3 * nlength (min (previous hp1 t) t) + 2 * nlength (N + (t - 1) * Z) +
2 * t + 26 * ((t - 1) + Z) ^ 2 + 3 * (N + t * Z) + Suc Z * (47 + 13 * (N + t * Z))"
by simp
also have "... ≤ 121 + 153 * nllength hp1 ^ 3 + 3 * nlength t + 2 * nlength (N + (t - 1) * Z) +
2 * t + 26 * ((t - 1) + Z) ^ 2 + 3 * (N + t * Z) + Suc Z * (47 + 13 * (N + t * Z))"
using previous_hp1_le nlength_mono by simp
also have "... ≤ 121 + 153 * nllength hp1 ^ 3 + 2 * nlength (N + (t - 1) * Z) +
5 * t + 26 * ((t - 1) + Z) ^ 2 + 3 * (N + t * Z) + Suc Z * (47 + 13 * (N + t * Z))"
using nlength_le_n by simp
also have "... ≤ 121 + 153 * nllength hp1 ^ 3 + 2 * (N + (t - 1) * Z) +
5 * t + 26 * ((t - 1) + Z) ^ 2 + 3 * (N + t * Z) + Suc Z * (47 + 13 * (N + t * Z))"
using nlength_le_n add_le_mono1 mult_le_mono2 nat_add_left_cancel_le by presburger
also have "... ≤ 121 + 153 * nllength hp1 ^ 3 + 2 * (N + t * Z) +
5 * t + 26 * ((t - 1) + Z) ^ 2 + 3 * (N + t * Z) + Suc Z * (47 + 13 * (N + t * Z))"
by simp
also have "... = 121 + 153 * nllength hp1 ^ 3 +
5 * t + 26 * ((t - 1) + Z) ^ 2 + 5 * (N + t * Z) + Suc Z * (47 + 13 * (N + t * Z))"
by simp
also have "... ≤ 121 + 153 * (Suc T' * Suc T') ^ 3 +
5 * t + 26 * ((t - 1) + Z) ^ 2 + 5 * (N + t * Z) + Suc Z * (47 + 13 * (N + t * Z))"
using nllength_hp1 by simp
also have "... = 121 + 153 * (Suc T' ^ 2)^3 +
5 * t + 26 * ((t - 1) + Z) ^ 2 + 5 * (N + t * Z) + Suc Z * (47 + 13 * (N + t * Z))"
by algebra
also have "... = 121 + 153 * Suc T' ^ 6 +
5 * t + 26 * ((t - 1) + Z) ^ 2 + 5 * (N + t * Z) + Suc Z * (47 + 13 * (N + t * Z))"
by simp
also have "... ≤ 121 + 153 * Suc T' ^ 6 +
5 * t + 26 * (t + Z) ^ 2 + 5 * (N + t * Z) + Suc Z * (47 + 13 * (N + t * Z))"
by simp
also have "... = 121 + 153 * Suc T' ^ 6 +
5 * t + 26 * (t + Z) ^ 2 + 5 * (N + t * Z) + 47 + 13 * (N + t * Z) + Z * (47 + 13 * (N + t * Z))"
by simp
also have "... = 168 + 153 * Suc T' ^ 6 +
5 * t + 26 * (t + Z) ^ 2 + 18 * (N + t * Z) + Z * (47 + 13 * (N + t * Z))"
by simp
also have "... ≤ 168 + 153 * Suc T' ^ 6 +
5 * t + 26 * (t + Z) ^ 2 + 2 * Z * (N + t * Z) + Z * (47 + 13 * (N + t * Z))"
using Z_ge_9 by (metis add_le_mono add_le_mono1 mult_2 mult_le_mono1 nat_add_left_cancel_le numeral_Bit0)
also have "... = 168 + 153 * Suc T' ^ 6 +
5 * t + 26 * (t + Z) ^ 2 + 2 * Z * (N + t * Z) + 47 * Z + 13 * Z * (N + t * Z)"
by algebra
also have "... = 168 + 153 * Suc T' ^ 6 + 5 * t + 26 * (t + Z) ^ 2 + 47 * Z + 15 * Z * (N + t * Z)"
by simp
finally have "?ttt ≤ ttt8"
using ttt8_def by simp
then show ?thesis
using tm8 transforms_monotone by simp
qed
definition "tpsT1 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t - 1⌋⇩N, 1),
j3 + 7 := (⌊previous hp1 t * Z⌋⇩N, 1),
j3 + 12 := nltape [N + (t - 1) * Z..<N + (t - 1) * Z + Z]]"
lemma tmT1 [transforms_intros]:
assumes "ttt = 4 + 26 * (nlength (previous hp1 t) + nlength Z) ^ 2"
shows "transforms tmT1 tps8 ttt tpsT1"
unfolding tmT1_def
proof (tform tps: tps0 tps8_def tpsT1_def jk)
show "ttt = 4 + 26 * (nlength (previous hp1 t) + nlength Z) * (nlength (previous hp1 t) + nlength Z)"
using assms by algebra
show "tpsT1 = tps8[j3 + 7 := (⌊previous hp1 t * Z⌋⇩N, 1)]"
unfolding tpsT1_def tps8_def by (simp add: list_update_swap[of "j3+7"])
qed
definition "tpsT2 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t - 1⌋⇩N, 1),
j3 + 7 := (⌊N + previous hp1 t * Z⌋⇩N, 1),
j3 + 12 := nltape [N + (t - 1) * Z..<N + (t - 1) * Z + Z]]"
lemma tmT2 [transforms_intros]:
assumes "ttt = 14 + 26 * (nlength (previous hp1 t) + nlength Z) ^ 2 +
3 * max (nlength N) (nlength (previous hp1 t * Z))"
shows "transforms tmT2 tps8 ttt tpsT2"
unfolding tmT2_def by (tform tps: tps0 tpsT1_def tpsT2_def jk assms)
definition "tpsT3 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t - 1⌋⇩N, 1),
j3 + 7 := (⌊N + previous hp1 t * Z⌋⇩N, 1),
j3 + 12 := nltape [N + (t - 1) * Z..<N + (t - 1) * Z + Z],
j3 + 8 := (⌊[N + previous hp1 t * Z..<N + previous hp1 t * Z + Z]⌋⇩N⇩L, 1)]"
lemma tmT3 [transforms_intros]:
assumes "ttt = 14 + 26 * (nlength (previous hp1 t) + nlength Z) ^ 2 +
3 * max (nlength N) (nlength (previous hp1 t * Z)) +
Suc Z * (43 + 9 * nlength (N + previous hp1 t * Z + Z))"
shows "transforms tmT3 tps8 ttt tpsT3"
unfolding tmT3_def
by (tform tps: nlcontents_Nil canrepr_0 tps0_sym tps0 tpsT2_def tpsT3_def jk time: assms)
definition "tpsT4 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t - 1⌋⇩N, 1),
j3 + 7 := (⌊N + previous hp1 t * Z⌋⇩N, 1),
j3 + 12 := nltape
([N + (t - 1) * Z..<N + (t - 1) * Z + Z] @
[N + previous hp1 t * Z..<N + previous hp1 t * Z + Z]),
j3 + 8 := (⌊[]⌋, 1)]"
lemma tmT4 [transforms_intros]:
assumes "ttt = 25 + 26 * (nlength (previous hp1 t) + nlength Z) ^ 2 +
3 * max (nlength N) (nlength (previous hp1 t * Z)) +
Suc Z * (43 + 9 * nlength (N + previous hp1 t * Z + Z)) +
4 * nllength [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z]"
shows "transforms tmT4 tps8 ttt tpsT4"
unfolding tmT4_def by (tform tps: tps0 tpsT3_def tpsT4_def jk time: assms)
definition "tpsT5 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t - 1⌋⇩N, 1),
j3 + 7 := (⌊0⌋⇩N, 1),
j3 + 12 := nltape
([N + (t - 1) * Z..<N + (t - 1) * Z + Z] @
[N + previous hp1 t * Z..<N + previous hp1 t * Z + Z]),
j3 + 8 := (⌊[]⌋, 1)]"
lemma tmT5 [transforms_intros]:
assumes "ttt = 35 + 26 * (nlength (previous hp1 t) + nlength Z) ^ 2 +
3 * max (nlength N) (nlength (previous hp1 t * Z)) +
Suc Z * (43 + 9 * nlength (N + previous hp1 t * Z + Z)) +
4 * nllength [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] +
2 * nlength (N + previous hp1 t * Z)"
shows "transforms tmT5 tps8 ttt tpsT5"
unfolding tmT5_def by (tform tps: tps0 tpsT4_def tpsT5_def jk time: assms)
definition "tps9 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t - 1⌋⇩N, 1),
j3 + 7 := (⌊0⌋⇩N, 1),
j3 + 12 := nltape
([N + (t - 1) * Z..<N + (t - 1) * Z + Z] @
(if previous hp1 t ≠ t then [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] else [])),
j3 + 8 := (⌊[]⌋, 1)]"
lemma tm89 [transforms_intros]:
assumes "ttt = 37 + 26 * (nlength (previous hp1 t) + nlength Z) ^ 2 +
3 * max (nlength N) (nlength (previous hp1 t * Z)) +
Suc Z * (43 + 9 * nlength (N + previous hp1 t * Z + Z)) +
4 * nllength [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] +
2 * nlength (N + previous hp1 t * Z)"
shows "transforms tm89 tps8 ttt tps9"
unfolding tm89_def
proof (tform time: assms)
have "tps8 ! (j3 + 13) = (⌊previous hp1 t = t⌋⇩B, 1)"
using tps8_def jk by simp
then have *: "(previous hp1 t ≠ t) = (read tps8 ! (j3 + 13) = □)"
using jk tps8_def read_ncontents_eq_0 by force
show "read tps8 ! (j3 + 13) = □ ⟹ tps9 = tpsT5"
using * tps9_def tpsT5_def by simp
have "(⌊[]⌋, 1) = tps0 ! (j3 + 8)"
using jk tps0 by simp
then have "tps0[j3 + 8 := (⌊[]⌋, 1)] = tps0"
using jk tps0 by (metis list_update_id)
then have "tps8 = tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t - 1⌋⇩N, 1),
j3 + 7 := (⌊0⌋⇩N, 1),
j3 + 12 := nltape [N + (t - 1) * Z..<N + (t - 1) * Z + Z],
j3 + 8 := (⌊[]⌋, 1)]"
using tps8_def jk tps0 by (simp add: list_update_swap[of _ "j3 + 8"])
then show "read tps8 ! (j3 + 13) ≠ □ ⟹ tps9 = tps8"
using * tps9_def by simp
qed
definition "ttt10 ≡ ttt8 + 37 + 26 * (nlength (previous hp1 t) + nlength Z) ^ 2 +
3 * max (nlength N) (nlength (previous hp1 t * Z)) +
Suc Z * (43 + 9 * nlength (N + previous hp1 t * Z + Z)) +
4 * nllength [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] +
2 * nlength (N + previous hp1 t * Z)"
lemma tm10 [transforms_intros]: "transforms tm10 tps0 ttt10 tps9"
unfolding tm10_def by (tform tps: ttt10_def)
definition "tps11 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊0⌋⇩N, 1),
j3 + 12 := nltape
([N + (t - 1) * Z..<N + (t - 1) * Z + Z] @
(if previous hp1 t ≠ t then [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] else [])),
j3 + 8 := (⌊[]⌋, 1)]"
lemma tm11 [transforms_intros]:
assumes "ttt = ttt10 + 5 + 2 * nlength (t - 1)"
shows "transforms tm11 tps0 ttt tps11"
unfolding tm11_def by (tform tps: t(1) tps0 tps9_def tps11_def jk time: assms)
definition "tps13 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊t * Z⌋⇩N, 1),
j3 + 12 := nltape
([N + (t - 1) * Z..<N + (t - 1) * Z + Z] @
(if previous hp1 t ≠ t then [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] else [])),
j3 + 8 := (⌊[]⌋, 1)]"
lemma tm13 [transforms_intros]:
assumes "ttt = ttt10 + 9 + 2 * nlength (t - 1) + 26 * (nlength t + nlength Z) ^ 2"
shows "transforms tm13 tps0 ttt tps13"
unfolding tm13_def
proof (tform tps: tps0 tps11_def tps13_def jk)
show "ttt = ttt10 + 5 + 2 * nlength (t - 1) + (4 + 26 * (nlength t + nlength Z) * (nlength t + nlength Z))"
using assms by simp (metis Groups.mult_ac(1) distrib_left power2_eq_square)
show "tps13 = tps11[j3 + 7 := (⌊t * Z⌋⇩N, 1)]"
unfolding tps13_def tps11_def by (simp add: list_update_swap[of "j3+7"])
qed
definition "tps14 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊N + t * Z⌋⇩N, 1),
j3 + 12 := nltape
([N + (t - 1) * Z..<N + (t - 1) * Z + Z] @
(if previous hp1 t ≠ t then [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] else [])),
j3 + 8 := (⌊[]⌋, 1)]"
lemma tm14 [transforms_intros]:
assumes "ttt = ttt10 + 19 + 2 * nlength (t - 1) + 26 * (nlength t + nlength Z) ^ 2 +
3 * max (nlength N) (nlength (t * Z))"
shows "transforms tm14 tps0 ttt tps14"
unfolding tm14_def
proof (tform tps: tps0 tps13_def tps14_def jk time: assms)
show "tps14 = tps13[j3 + 7 := (⌊N + t * Z⌋⇩N, 1)]"
unfolding tps14_def tps13_def by (simp add: list_update_swap[of "j3+7"])
qed
definition "tps15 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊N + t * Z⌋⇩N, 1),
j3 + 12 := nltape
([N + (t - 1) * Z..<N + (t - 1) * Z + Z] @
(if previous hp1 t ≠ t then [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] else [])),
j3 + 8 := (⌊[N + t * Z..<N + t * Z + Z]⌋⇩N⇩L, 1)]"
lemma tm15 [transforms_intros]:
assumes "ttt = ttt10 + 19 + 2 * nlength (t - 1) + 26 * (nlength t + nlength Z) ^ 2 +
3 * max (nlength N) (nlength (t * Z)) + Suc Z * (43 + 9 * nlength (N + t * Z + Z))"
shows "transforms tm15 tps0 ttt tps15"
unfolding tm15_def
proof (tform tps: tps0 tps14_def tps15_def jk time: assms)
show "tps14 ! (j3 + 8) = (⌊[]⌋⇩N⇩L, 1)"
using tps14_def jk nlcontents_Nil tps0 by simp
show "tps14 ! (j3 + 8 + 1) = (⌊0⌋⇩N, 1)"
using tps14_def jk canrepr_0 tps0_sym by simp
show "tps14 ! (j3 + 8 + 2) = (⌊0⌋⇩N, 1)"
using tps14_def jk canrepr_0 tps0_sym by simp
qed
definition "tps16 ≡ tps0
[j3 + 11 := (⌊previous hp1 t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊N + t * Z⌋⇩N, 1),
j3 + 12 := nltape
([N + (t - Suc 0) * Z..<N + (t - Suc 0) * Z + Z] @
(if previous hp1 t ≠ t then [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] else []) @
[N + t * Z..<N + t * Z + Z]),
j3 + 8 := (⌊[]⌋, 1)]"
lemma tm16 [transforms_intros]:
assumes "ttt = ttt10 + 30 + 2 * nlength (t - 1) + 26 * (nlength t + nlength Z) ^ 2 +
3 * max (nlength N) (nlength (t * Z)) + Suc Z * (43 + 9 * nlength (N + t * Z + Z)) +
4 * nllength [N + t * Z..<N + t * Z + Z]"
shows "transforms tm16 tps0 ttt tps16"
unfolding tm16_def by (tform tps: tps0 tps15_def tps16_def jk time: assms)
definition "tps17 ≡ tps0
[j3 + 11 := (⌊0⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊N + t * Z⌋⇩N, 1),
j3 + 12 := nltape
([N + (t - Suc 0) * Z..<N + (t - Suc 0) * Z + Z] @
(if previous hp1 t ≠ t then [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] else []) @
[N + t * Z..<N + t * Z + Z]),
j3 + 8 := (⌊[]⌋, 1)]"
lemma tm17 [transforms_intros]:
assumes "ttt = ttt10 + 40 + 2 * nlength (t - 1) + 26 * (nlength t + nlength Z) ^ 2 +
3 * max (nlength N) (nlength (t * Z)) + Suc Z * (43 + 9 * nlength (N + t * Z + Z)) +
4 * nllength [N + t * Z..<N + t * Z + Z] + 2 * nlength (previous hp1 t)"
shows "transforms tm17 tps0 ttt tps17"
unfolding tm17_def by (tform tps: tps0 tps16_def tps17_def jk time: jk assms)
definition "tps18 ≡ tps0
[j3 + 11 := (⌊hp0 ! t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊N + t * Z⌋⇩N, 1),
j3 + 12 := nltape
([N + (t - Suc 0) * Z..<N + (t - Suc 0) * Z + Z] @
(if previous hp1 t ≠ t then [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] else []) @
[N + t * Z..<N + t * Z + Z]),
j3 + 8 := (⌊[]⌋, 1)]"
lemma tm18 [transforms_intros]:
assumes "ttt = ttt10 + 66 + 2 * nlength (t - 1) + 26 * (nlength t + nlength Z) ^ 2 +
3 * max (nlength N) (nlength (t * Z)) + Suc Z * (43 + 9 * nlength (N + t * Z + Z)) +
4 * nllength [N + t * Z..<N + t * Z + Z] + 2 * nlength (previous hp1 t) +
21 * (nllength hp0)⇧2"
shows "transforms tm18 tps0 ttt tps18"
unfolding tm18_def
proof (tform tps: tps0 tps18_def tps17_def jk time: assms)
show "t < length hp0"
using len_hp0 t by simp
qed
definition "tps19 ≡ tps0
[j3 + 11 := (⌊hp0 ! t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊0⌋⇩N, 1),
j3 + 12 := nltape
([N + (t - Suc 0) * Z..<N + (t - Suc 0) * Z + Z] @
(if previous hp1 t ≠ t then [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] else []) @
[N + t * Z..<N + t * Z + Z]),
j3 + 8 := (⌊[]⌋, 1)]"
lemma tm19 [transforms_intros]:
assumes "ttt = ttt10 + 76 + 2 * nlength (t - 1) + 26 * (nlength t + nlength Z) ^ 2 +
3 * max (nlength N) (nlength (t * Z)) + Suc Z * (43 + 9 * nlength (N + t * Z + Z)) +
4 * nllength [N + t * Z..<N + t * Z + Z] + 2 * nlength (previous hp1 t) +
21 * (nllength hp0)⇧2 + 2 * nlength (N + t * Z)"
shows "transforms tm19 tps0 ttt tps19"
unfolding tm19_def
by (tform tps: tps0 tps18_def tps19_def jk time: assms)
definition "tps20 ≡ tps0
[j3 + 11 := (⌊hp0 ! t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊hp0 ! t * G⌋⇩N, 1),
j3 + 12 := nltape
([N + (t - Suc 0) * Z..<N + (t - Suc 0) * Z + Z] @
(if previous hp1 t ≠ t then [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] else []) @
[N + t * Z..<N + t * Z + Z]),
j3 + 8 := (⌊[]⌋, 1)]"
definition "ttt20 ≡ ttt10 + 80 + 2 * nlength (t - 1) + 26 * (nlength t + nlength Z) ^ 2 +
3 * max (nlength N) (nlength (t * Z)) + Suc Z * (43 + 9 * nlength (N + t * Z + Z)) +
4 * nllength [N + t * Z..<N + t * Z + Z] + 2 * nlength (previous hp1 t) +
21 * (nllength hp0)⇧2 + 2 * nlength (N + t * Z) + 26 * (nlength (hp0 ! t) + nlength G) ^ 2"
lemma tm20 [transforms_intros]: "transforms tm20 tps0 ttt20 tps20"
unfolding tm20_def
proof (tform tps: tps0 tps19_def tps20_def jk)
show "tps20 = tps19[j3 + 7 := (⌊hp0 ! t * G⌋⇩N, 1)]"
unfolding tps20_def tps19_def by (simp add: list_update_swap[of "j3 + 7"])
show "ttt20 = ttt10 + 76 + 2 * nlength (t - 1) + 26 * (nlength t + nlength Z)⇧2 +
3 * max (nlength N) (nlength (t * Z)) + Suc Z * (43 + 9 * nlength (N + t * Z + Z)) +
4 * nllength [N + t * Z..<N + t * Z + Z] + 2 * nlength (previous hp1 t) +
21 * (nllength hp0)⇧2 + 2 * nlength (N + t * Z) +
(4 + 26 * (nlength (hp0 ! t) + nlength G) * (nlength (hp0 ! t) + nlength G))"
using ttt20_def by simp (metis Groups.mult_ac(1) distrib_left power2_eq_square)
qed
definition "tps21 ≡ tps0
[j3 + 11 := (⌊hp0 ! t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊hp0 ! t * G⌋⇩N, 1),
j3 + 12 := nltape
([N + (t - Suc 0) * Z..<N + (t - Suc 0) * Z + Z] @
(if previous hp1 t ≠ t then [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] else []) @
[N + t * Z..<N + t * Z + Z]),
j3 + 8 := (⌊[hp0 ! t * G..<hp0 ! t * G + G]⌋⇩N⇩L, 1)]"
lemma tm21 [transforms_intros]:
assumes "ttt = ttt20 + Suc G * (43 + 9 * nlength (hp0 ! t * G + G))"
shows "transforms tm21 tps0 ttt tps21"
unfolding tm21_def
proof (tform tps: tps0 tps20_def tps21_def jk time: assms)
show "tps20 ! (j3 + 8) = (⌊[]⌋⇩N⇩L, 1)"
using tps20_def jk nlcontents_Nil tps0 by simp
show "tps20 ! (j3 + 8 + 1) = (⌊0⌋⇩N, 1)"
using tps20_def jk canrepr_0 tps0_sym by simp
show "tps20 ! (j3 + 8 + 2) = (⌊0⌋⇩N, 1)"
using tps20_def jk canrepr_0 tps0_sym by simp
qed
abbreviation "σ ≡
[N + (t - 1) * Z..<N + (t - 1) * Z + Z] @
(if previous hp1 t ≠ t then [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] else []) @
[N + t * Z..<N + t * Z + Z] @
[hp0 ! t * G..<hp0 ! t * G + G]"
definition "tps22 ≡ tps0
[j3 + 11 := (⌊hp0 ! t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊hp0 ! t * G⌋⇩N, 1),
j3 + 12 := nltape σ,
j3 + 8 := (⌊[]⌋, 1)]"
lemma tm22 [transforms_intros]:
assumes "ttt = ttt20 + 11 + Suc G * (43 + 9 * nlength (hp0 ! t * G + G)) +
4 * nllength [hp0 ! t * G..<hp0 ! t * G + G]"
shows "transforms tm22 tps0 ttt tps22"
unfolding tm22_def by (tform tps: tps0 tps21_def tps22_def jk time: assms)
definition "tps23 ≡ tps0
[j3 + 11 := (⌊hp0 ! t⌋⇩N, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊0⌋⇩N, 1),
j3 + 12 := nltape σ,
j3 + 8 := (⌊[]⌋, 1)]"
lemma tm23 [transforms_intros]:
assumes "ttt = ttt20 + 21 + Suc G * (43 + 9 * nlength (hp0 ! t * G + G)) +
4 * nllength [hp0 ! t * G..<hp0 ! t * G + G] + 2 * nlength (hp0 ! t * G)"
shows "transforms tm23 tps0 ttt tps23"
unfolding tm23_def by (tform tps: tps0 tps22_def tps23_def jk time: assms)
definition "tps24 ≡ tps0
[j3 + 11 := (⌊[]⌋, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊0⌋⇩N, 1),
j3 + 12 := nltape σ,
j3 + 8 := (⌊[]⌋, 1)]"
lemma tm24 [transforms_intros]:
assumes "ttt = ttt20 + 28 + Suc G * (43 + 9 * nlength (hp0 ! t * G + G)) +
4 * nllength [hp0 ! t * G..<hp0 ! t * G + G] + 2 * nlength (hp0 ! t * G) +
2 * nlength (hp0 ! t)"
shows "transforms tm24 tps0 ttt tps24"
unfolding tm24_def
proof (tform tps: tps0 tps23_def tps24_def jk assms)
show "proper_symbols (canrepr (hp0 ! t))"
using proper_symbols_canrepr by simp
qed
definition "tps25 ≡ tps0
[j3 + 11 := (⌊[]⌋, 1),
j3 + 13 := (⌊previous hp1 t = t⌋⇩B, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊0⌋⇩N, 1),
j3 + 12 := (⌊σ⌋⇩N⇩L, 1),
j3 + 8 := (⌊[]⌋, 1)]"
lemma tm25 [transforms_intros]:
assumes "ttt = ttt20 + 31 + Suc G * (43 + 9 * nlength (hp0 ! t * G + G)) +
4 * nllength [hp0 ! t * G..<hp0 ! t * G + G] + 2 * nlength (hp0 ! t * G) +
2 * nlength (hp0 ! t) + nllength σ"
shows "transforms tm25 tps0 ttt tps25"
unfolding tm25_def
proof (tform tps: tps0 tps24_def tps25_def jk assms)
have *: "tps24 ! (j3 + 12) = nltape σ"
using tps24_def jk by simp
then show "clean_tape (tps24 ! (j3 + 12))"
using clean_tape_nlcontents by simp
have "tps25 = tps24[j3 + 12 := nltape σ |#=| 1]"
unfolding tps25_def tps24_def by (simp add: list_update_swap)
then show "tps25 = tps24[j3 + 12 := tps24 ! (j3 + 12) |#=| 1]"
using * by simp
qed
definition "tpsE1 ≡ tps0
[j3 + 11 := (⌊[]⌋, 1),
j3 + 13 := (⌊[]⌋, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊0⌋⇩N, 1),
j3 + 12 := (⌊σ⌋⇩N⇩L, 1),
j3 + 8 := (⌊[]⌋, 1)]"
lemma tmE1:
assumes "ttt = 7 + 2 * nlength (if previous hp1 t = t then 1 else 0)"
shows "transforms tmE1 tps25 ttt tpsE1"
unfolding tmE1_def
proof (tform tps: tps0 tps25_def tpsE1_def jk assms)
show "proper_symbols (canrepr (if previous hp1 t = t then 1 else 0))"
using proper_symbols_canrepr by simp
qed
lemma tmE1' [transforms_intros]:
assumes "ttt = 9"
shows "transforms tmE1 tps25 ttt tpsE1"
using tmE1 assms transforms_monotone by (simp add: nlength_le_n)
definition "tpsE2 ≡ tps0
[j3 + 11 := nlltape' (formula_n (relabel σ ψ')) 0,
j3 + 13 := (⌊[]⌋, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊0⌋⇩N, 1),
j3 + 12 := (⌊σ⌋⇩N⇩L, 1),
j3 + 8 := (⌊[]⌋, 1)]"
lemma tmE2 [transforms_intros]:
assumes "ttt = 16 + 108 * (nlllength (formula_n ψ'))⇧2 * (3 + (nllength σ)⇧2)"
and "previous hp1 t = t"
shows "transforms tmE2 tps25 ttt tpsE2"
unfolding tmE2_def
proof (tform tps: tps0 tpsE1_def tpsE2_def jk assms time: assms(1))
let ?sigma = "[N + (t - Suc 0) * Z..<N + (t - Suc 0) * Z + Z] @
[N + t * Z..<N + t * Z + Z] @ [hp0 ! t * G..<hp0 ! t * G + G]"
show "variables ψ' ⊆ {..<length ?sigma}"
using assms(2) psi'(1) by auto
show "tpsE1 ! (j3 + 11) = (⌊[]⌋⇩N⇩L⇩L, 1)"
using tpsE1_def jk nllcontents_Nil by simp
show "tpsE1 ! (j3 + 11 + 1) = (⌊?sigma⌋⇩N⇩L, 1)"
using assms(2) tpsE1_def jk by (simp add: add.commute[of j3 12])
show "tpsE1 ! (j3 + 11 + 2) = (⌊[]⌋⇩N⇩L, 1)"
using tpsE1_def jk nlcontents_Nil by (simp add: add.commute[of j3 13])
show "tpsE1 ! (j3 + 11 + 3) = (⌊[]⌋⇩N⇩L, 1)"
using tpsE1_def jk tps0_sym nlcontents_Nil by simp
show "tpsE1 ! (j3 + 11 + 4) = (⌊0⌋⇩N, 1)"
using tpsE1_def jk tps0_sym canrepr_0 by simp
show "tpsE1 ! (j3 + 11 + 5) = (⌊0⌋⇩N, 1)"
using tpsE1_def jk tps0_sym canrepr_0 by simp
show "tpsE2 = tpsE1[j3 + 11 := nlltape' (formula_n (relabel ?sigma ψ')) 0]"
unfolding tpsE2_def tpsE1_def using assms(2) by (simp add: list_update_swap[of "j3+11"])
qed
definition "tpsTT1 ≡ tps0
[j3 + 11 := nlltape' (formula_n (relabel σ ψ)) 0,
j3 + 13 := (⌊[]⌋, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊0⌋⇩N, 1),
j3 + 12 := (⌊σ⌋⇩N⇩L, 1),
j3 + 8 := (⌊[]⌋, 1)]"
lemma tmTT1 [transforms_intros]:
assumes "ttt = 7 + 108 * (nlllength (formula_n ψ))⇧2 * (3 + (nllength σ)⇧2)"
and "previous hp1 t ≠ t"
shows "transforms tmTT1 tps25 ttt tpsTT1"
unfolding tmTT1_def
proof (tform tps: tps0 tps25_def tpsTT1_def jk time: assms(1))
let ?sigma = "[N + (t - Suc 0) * Z..<N + (t - Suc 0) * Z + Z] @
(if previous hp1 t ≠ t
then [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z]
else []) @
[N + t * Z..<N + t * Z + Z] @ [hp0 ! t * G..<hp0 ! t * G + G]"
show "variables ψ ⊆ {..<length ?sigma}"
using assms(2) psi(1) by auto
show "tps25 ! (j3 + 11) = (⌊[]⌋⇩N⇩L⇩L, 1)"
using tps25_def jk nllcontents_Nil by simp
show "tps25 ! (j3 + 11 + 1) = (⌊?sigma⌋⇩N⇩L, 1)"
using tps25_def jk by (simp add: add.commute[of j3 12])
show "tps25 ! (j3 + 11 + 2) = (⌊[]⌋⇩N⇩L, 1)"
using tps25_def jk canrepr_0 nlcontents_Nil assms(2) by (simp add: add.commute[of j3 13])
show "tps25 ! (j3 + 11 + 3) = (⌊[]⌋⇩N⇩L, 1)"
using tps25_def jk tps0_sym nlcontents_Nil by simp
show "tps25 ! (j3 + 11 + 4) = (⌊0⌋⇩N, 1)"
using tps25_def jk tps0_sym canrepr_0 by simp
show "tps25 ! (j3 + 11 + 5) = (⌊0⌋⇩N, 1)"
using tps25_def jk tps0_sym canrepr_0 by simp
show "tpsTT1 = tps25[j3 + 11 := nlltape' (formula_n (relabel ?sigma ψ)) 0]"
using tpsTT1_def tps25_def assms(2) canrepr_0 by (simp add: list_update_swap[of "j3+11"])
qed
definition "tps26 ≡ tps0
[j3 + 11 := nlltape' (formula_n (relabel σ (if previous hp1 t = t then ψ' else ψ))) 0,
j3 + 13 := (⌊[]⌋, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊0⌋⇩N, 1),
j3 + 12 := (⌊σ⌋⇩N⇩L, 1),
j3 + 8 := (⌊[]⌋, 1)]"
lemma nlllength_psi: "nlllength (formula_n ψ) ≤ 24 * Z ^ 2 * 2 ^ (4*Z)"
proof -
let ?V = "3 * Z + G"
have "⋀v. v ∈ variables ψ ⟹ v ≤ ?V"
using psi(1) by auto
then have "nlllength (formula_n ψ) ≤ fsize ψ * Suc (Suc (nlength ?V)) + length ψ"
using nlllength_formula_n by simp
also have "... ≤ fsize ψ * Suc (Suc (nlength ?V)) + 2 ^ ?V"
using psi by simp
also have "... ≤ ?V * 2 ^ ?V * Suc (Suc (nlength ?V)) + 2 ^ ?V"
using psi(2) by (metis add_le_mono1 mult.commute mult_le_mono2)
also have "... ≤ 4*Z * 2 ^ ?V * Suc (Suc (nlength ?V)) + 2 ^ ?V"
using Z by simp
also have "... ≤ 4*Z * 2 ^ (4*Z) * Suc (Suc (nlength ?V)) + 2 ^ ?V"
proof -
have "?V ≤ 4 * Z"
using Z by simp
then have "(2::nat) ^ ?V ≤ 2 ^ (4*Z)"
by simp
then show ?thesis
using add_le_mono le_refl mult_le_mono by presburger
qed
also have "... ≤ 4*Z * (2::nat) ^ (4*Z) * Suc (Suc (nlength (4*Z))) + 2 ^ ?V"
using Z nlength_mono by simp
also have "... ≤ 4*Z * (2::nat) ^ (4*Z) * Suc (Suc (4*Z)) + 2 ^ ?V"
using nlength_le_n by simp
also have "... ≤ 4*Z * 2 ^ (4*Z) * Suc (Suc (4*Z)) + 2 ^ (4*Z)"
using Z by simp
also have "... ≤ 4*Z * 2 ^ (4*Z) * (5*Z) + 2 ^ (4*Z)"
using Z G by simp
also have "... ≤ 4*Z * 2 ^ (4*Z) * (6*Z)"
using Z G by simp
also have "... = 24 * Z ^ 2 * 2 ^ (4*Z)"
by algebra
finally show ?thesis .
qed
lemma nlllength_psi': "nlllength (formula_n ψ') ≤ 24 * Z ^ 2 * 2 ^ (4*Z)"
proof -
let ?V = "2 * Z + G"
have "⋀v. v ∈ variables ψ' ⟹ v ≤ ?V"
using psi'(1) by auto
then have "nlllength (formula_n ψ') ≤ fsize ψ' * Suc (Suc (nlength ?V)) + length ψ'"
using nlllength_formula_n by simp
also have "... ≤ fsize ψ' * Suc (Suc (nlength ?V)) + 2 ^ ?V"
using psi' by simp
also have "... ≤ ?V * 2 ^ ?V * Suc (Suc (nlength ?V)) + 2 ^ ?V"
using psi'(2) by (metis add_le_mono1 mult.commute mult_le_mono2)
also have "... ≤ 4*Z * 2 ^ ?V * Suc (Suc (nlength ?V)) + 2 ^ ?V"
using Z by simp
also have "... ≤ 4*Z * 2 ^ (4*Z) * Suc (Suc (nlength ?V)) + 2 ^ ?V"
proof -
have "?V ≤ 4 * Z"
using Z by simp
then have "(2::nat) ^ ?V ≤ 2 ^ (4*Z)"
by simp
then show ?thesis
using add_le_mono le_refl mult_le_mono by presburger
qed
also have "... ≤ 4*Z * (2::nat) ^ (4*Z) * Suc (Suc (nlength (4*Z))) + 2 ^ ?V"
using Z nlength_mono by simp
also have "... ≤ 4*Z * (2::nat) ^ (4*Z) * Suc (Suc (4*Z)) + 2 ^ ?V"
using nlength_le_n by simp
also have "... ≤ 4*Z * 2 ^ (4*Z) * Suc (Suc (4*Z)) + 2 ^ (4*Z)"
using Z by simp
also have "... ≤ 4*Z * 2 ^ (4*Z) * (5*Z) + 2 ^ (4*Z)"
using Z G by simp
also have "... ≤ 4*Z * 2 ^ (4*Z) * (6*Z)"
using Z G by simp
also have "... = 24 * Z ^ 2 * 2 ^ (4*Z)"
by algebra
finally show ?thesis .
qed
lemma tm2526:
assumes "ttt = 17 + 108 * (24 * Z ^ 2 * 2 ^ (4*Z))⇧2 * (3 + (nllength σ)⇧2)"
shows "transforms tm2526 tps25 ttt tps26"
unfolding tm2526_def
proof (tform)
have *: "tps25 ! (j3 + 13) = (⌊previous hp1 t = t⌋⇩B, 1)"
using tps25_def jk by simp
then have **: "(previous hp1 t ≠ t) = (read tps25 ! (j3 + 13) = □)"
using jk tps25_def read_ncontents_eq_0 by force
show "read tps25 ! (j3 + 13) = □ ⟹ previous hp1 t ≠ t"
using ** by simp
show "read tps25 ! (j3 + 13) ≠ □ ⟹ previous hp1 t = t"
using ** by simp
show "read tps25 ! (j3 + 13) = □ ⟹ tps26 = tpsTT1"
using tps26_def tpsTT1_def ** by presburger
show "read tps25 ! (j3 + 13) ≠ □ ⟹ tps26 = tpsE2"
using tps26_def tpsE2_def ** by presburger
let ?tT = "7 + 108 * (nlllength (formula_n ψ))⇧2 * (3 + (nllength σ)⇧2)"
let ?tF = "16 + 108 * (nlllength (formula_n ψ'))⇧2 * (3 + (nllength σ)⇧2)"
have "?tT + 2 ≤ 9 + 108 * (24 * Z ^ 2 * 2 ^ (4*Z))⇧2 * (3 + (nllength σ)⇧2)"
using nlllength_psi linear_le_pow by simp
also have "... ≤ ttt"
using assms by simp
finally show "?tT + 2 ≤ ttt" .
show "?tF + 1 ≤ ttt"
using nlllength_psi' assms linear_le_pow by simp
qed
lemma nllength_σ: "nllength σ ≤ 12 * T' * Z^2 + 4 * Z * N"
proof -
have "n ≤ N + T' * Z + Z" if "n ∈ set σ" for n
proof -
consider
"n ∈ set [N + (t - 1) * Z..<N + (t - 1) * Z + Z]"
| "n ∈ set [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z]"
| "n ∈ set [N + t * Z..<N + t * Z + Z]"
| "n ∈ set [hp0 ! t * G..<hp0 ! t * G + G]"
using `n ∈ set σ` by auto
then show ?thesis
proof (cases)
case 1
then have "n ≤ N + (t - 1) * Z + Z"
by simp
also have "... ≤ N + T' * Z + Z"
using t(2) by auto
finally show ?thesis
by simp
next
case 2
then have "n ≤ N + (previous hp1 t) * Z + Z"
by simp
also have "... ≤ N + t * Z + Z"
by (simp add: previous_hp1_le)
also have "... ≤ N + T' * Z + Z"
using t(2) by simp
finally show ?thesis
by simp
next
case 3
then have "n ≤ N + t * Z + Z"
by simp
also have "... ≤ N + T' * Z + Z"
using t(2) by auto
finally show ?thesis
by simp
next
case 4
then have "n ≤ N + (hp0 ! t) * G + G"
by simp
also have "... ≤ N + T' * G + G"
using t len_hp0 hp0 by simp
also have "... ≤ N + T' * Z + Z"
using Z by simp
finally show ?thesis
by simp
qed
qed
then have "nllength σ ≤ Suc (N + T' * Z + Z) * (length σ)"
using nllength_le[of σ "N + T' * Z + Z"] by simp
also have "... ≤ Suc (N + T' * Z + Z) * (3 * Z + G)"
proof -
have "length σ ≤ 3 * Z + G"
by simp
then show ?thesis
using mult_le_mono2 by presburger
qed
also have "... ≤ Suc (N + T' * Z + Z) * (3 * Z + Z)"
using Z by simp
also have "... = 4 * Z * Suc (N + T' * Z + Z)"
by simp
also have "... = 4 * Z + 4 * Z * (N + T' * Z + Z)"
by simp
also have "... = 4 * Z + 4 * Z * N + 4 * T' * Z^2 + 4 * Z^2"
by algebra
also have "... ≤ 4 * Z^2 + 4 * Z * N + 4 * T' * Z^2 + 4 * Z^2"
using linear_le_pow by simp
also have "... = 8 * Z^2 + 4 * Z * N + 4 * T' * Z^2"
by simp
also have "... ≤ 8 * T' * Z^2 + 4 * Z * N + 4 * T' * Z^2"
using t by simp
also have "... = 12 * T' * Z^2 + 4 * Z * N"
by simp
finally show ?thesis .
qed
lemma tm2526' [transforms_intros]:
assumes "ttt = 17 + 108 * (24 * Z ^ 2 * 2 ^ (4*Z))⇧2 * (3 + (12 * T' * Z^2 + 4 * Z * N)⇧2)"
shows "transforms tm2526 tps25 ttt tps26"
proof -
have "17 + 108 * (24 * Z ^ 2 * 2 ^ (4*Z))⇧2 * (3 + (nllength σ)⇧2) ≤ ttt"
using assms nllength_σ by simp
then show ?thesis
using tm2526 transforms_monotone by simp
qed
lemma tm26 [transforms_intros]:
assumes "ttt = ttt20 + 31 + Suc G * (43 + 9 * nlength (hp0 ! t * G + G)) +
4 * nllength [hp0 ! t * G..<hp0 ! t * G + G] + 2 * nlength (hp0 ! t * G) +
2 * nlength (hp0 ! t) + nllength σ +
17 + 108 * (24 * Z ^ 2 * 2 ^ (4*Z))⇧2 * (3 + (12 * T' * Z^2 + 4 * Z * N)⇧2)"
shows "transforms tm26 tps0 ttt tps26"
unfolding tm26_def by (tform tps: assms)
definition "tps27 ≡ tps0
[j3 + 11 := nlltape' (formula_n (relabel σ (if previous hp1 t = t then ψ' else ψ))) 0,
j3 + 13 := (⌊[]⌋, 1),
j3 + 6 := (⌊t⌋⇩N, 1),
j3 + 7 := (⌊0⌋⇩N, 1),
j3 + 12 := (⌊[]⌋, 1),
j3 + 8 := (⌊[]⌋, 1)]"
lemma tm27:
assumes "ttt = ttt20 + 38 + Suc G * (43 + 9 * nlength (hp0 ! t * G + G)) +
4 * nllength [hp0 ! t * G..<hp0 ! t * G + G] + 2 * nlength (hp0 ! t * G) +
2 * nlength (hp0 ! t) + 3 * nllength σ +
17 + 108 * (24 * Z ^ 2 * 2 ^ (4*Z))⇧2 * (3 + (12 * T' * Z^2 + 4 * Z * N)⇧2)"
shows "transforms tm27 tps0 ttt tps27"
unfolding tm27_def
proof (tform tps: tps0 tps26_def tps27_def jk)
let ?zs = "numlist σ"
show "tps26 ::: (j3 + 12) = ⌊?zs⌋"
using tps26_def jk nlcontents_def by simp
show "proper_symbols ?zs"
using proper_symbols_numlist by simp
show "ttt = ttt20 + 31 + Suc G * (43 + 9 * nlength (hp0 ! t * G + G)) +
4 * nllength [hp0 ! t * G..<hp0 ! t * G + G] + 2 * nlength (hp0 ! t * G) +
2 * nlength (hp0 ! t) + nllength σ +
17 + 108 * (24 * Z⇧2 * 2 ^ (4 * Z))⇧2 * (3 + (12 * T' * Z⇧2 + 4 * Z * N)⇧2) +
(tps26 :#: (j3 + 12) + 2 * length (numlist σ) + 6)"
using tps26_def jk nllength_def assms by simp
qed
definition "tps27' ≡ tps0
[j3 + 11 := nlltape' (formula_n (relabel σ (if previous hp1 t = t then ψ' else ψ))) 0]"
lemma tps27': "tps27 = tps27'"
proof -
have 1: "tps0[j3 + 13 := (⌊[]⌋, Suc 0)] = tps0"
using list_update_id[of tps0 "j3+13"] jk tps0 by simp
have 2: "tps0[j3 + 12 := (⌊[]⌋, Suc 0)] = tps0"
using list_update_id[of tps0 "j3+12"] jk tps0 by simp
have 3: "tps0[j3 + 8 := (⌊[]⌋, Suc 0)] = tps0"
using list_update_id[of tps0 "j3+8"] jk tps0 by simp
have 4: "tps0[j3 + 7 := (⌊0⌋⇩N, Suc 0)] = tps0"
using list_update_id[of tps0 "j3+7"] canrepr_0 jk tps0 by simp
have 5: "tps0[j3 + 6 := (⌊t⌋⇩N, Suc 0)] = tps0"
using list_update_id[of tps0 "j3+6"] jk tps0 by simp
show ?thesis
unfolding tps27_def tps27'_def
using tps0
by (simp split del: if_split add:
list_update_swap[of _ "j3 + 13"] 1
list_update_swap[of _ "j3 + 12"] 2
list_update_swap[of _ "j3 + 8"] 3
list_update_swap[of _ "j3 + 7"] 4
list_update_swap[of _ "j3 + 6"] 5)
qed
definition "ttt27 = ttt20 + 38 + Suc G * (43 + 9 * nlength (hp0 ! t * G + G)) +
4 * nllength [hp0 ! t * G..<hp0 ! t * G + G] + 2 * nlength (hp0 ! t * G) +
2 * nlength (hp0 ! t) + 3 * nllength σ +
17 + 108 * (24 * Z ^ 2 * 2 ^ (4*Z))⇧2 * (3 + (12 * T' * Z^2 + 4 * Z * N)⇧2)"
lemma tm27' [transforms_intros]: "transforms tm27 tps0 ttt27 tps27'"
using ttt27_def tm27 nllength_σ tps27' transforms_monotone by simp
definition "tps28 ≡ tps0
[1 := nlltape (nss @ formula_n (relabel σ (if previous hp1 t = t then ψ' else ψ))),
j3 + 11 := (⌊[]⌋, 1)]"
lemma tm28:
assumes "ttt = ttt27 + (11 + 4 * nlllength (formula_n (relabel σ (if previous hp1 t = t then ψ' else ψ))))"
shows "transforms tm28 tps0 ttt tps28"
unfolding tm28_def by (tform tps: tps0(1) tps0 tps27'_def tps28_def jk time: ttt27_def assms)
lemma nlllength_relabel_chi_t:
"nlllength (formula_n (relabel σ (if previous hp1 t = t then ψ' else ψ))) ≤
Suc (nllength σ) * 24 * Z ^ 2 * 2 ^ (4*Z)"
(is "nlllength (formula_n (relabel σ ?phi)) ≤ _")
proof -
have "variables ?phi ⊆ {..<length σ}"
proof (cases "previous hp1 t = t")
case True
then show ?thesis
using psi'(1) by auto
next
case False
then show ?thesis
using psi(1) by auto
qed
then have "nlllength (formula_n (relabel σ ?phi)) ≤ Suc (nllength σ) * nlllength (formula_n ?phi)"
using nlllength_relabel_variables by simp
moreover have "nlllength (formula_n ?phi) ≤ 24 * Z ^ 2 * 2 ^ (4*Z)"
using nlllength_psi nlllength_psi' by (cases "previous hp1 t = t") simp_all
ultimately have "nlllength (formula_n (relabel σ ?phi)) ≤ Suc (nllength σ) * (24 * Z ^ 2 * 2 ^ (4*Z))"
by (meson le_trans mult_le_mono2)
then show ?thesis
by linarith
qed
definition "tps28' ≡ tps0
[1 := nlltape (nss @ formula_n (relabel σ (if previous hp1 t = t then ψ' else ψ)))]"
lemma tps28': "tps28' = tps28"
unfolding tps28'_def tps28_def using tps0 list_update_id[of tps0 "j3+11"]
by (simp add: list_update_swap[of _ "j3 + 11"])
lemma tm28' [transforms_intros]:
assumes "ttt = ttt27 + (11 + 4 * (Suc (nllength σ) * 24 * Z ^ 2 * 2 ^ (4*Z)))"
shows "transforms tm28 tps0 ttt tps28'"
using assms tm28 tps28' nlllength_relabel_chi_t transforms_monotone by simp
definition "tps29 ≡ tps0
[1 := nlltape (nss @ formula_n (relabel σ (if previous hp1 t = t then ψ' else ψ))),
j3 + 6 := (⌊Suc t⌋⇩N, 1)]"
lemma tm29 [transforms_intros]:
assumes "ttt = ttt27 + 16 + 4 * (Suc (nllength σ) * 24 * Z ^ 2 * 2 ^ (4*Z)) + 2 * nlength t"
shows "transforms tm29 tps0 ttt tps29"
unfolding tm29_def by (tform tps: assms tps0 tps28'_def tps29_def jk)
definition "tps30 ≡ tps0
[1 := nlltape (nss @ formula_n (relabel σ (if previous hp1 t = t then ψ' else ψ))),
j3 + 6 := (⌊Suc t⌋⇩N, 1),
j3 + 3 := (⌊T - 1⌋⇩N, 1)]"
lemma tm30:
assumes "ttt = ttt27 + 24 + 4 * (Suc (nllength σ) * 24 * Z ^ 2 * 2 ^ (4*Z)) + 2 * nlength t + 2 * nlength T"
shows "transforms tm30 tps0 ttt tps30"
unfolding tm30_def by (tform tps: assms tps0 tps29_def tps30_def jk)
text ‹
Some helpers for bounding the running time:
›
lemma pow4_le_2pow4: "z ^ 4 ≤ 2 ^ (4*z)" for z :: nat
proof -
have "z ^ 4 = (z ^ 2) ^ 2"
by simp
also have "... ≤ (2^(2*z)) ^ 2"
using pow2_le_2pow2 power_mono by blast
also have "... = 2^(4*z)"
by (metis mult.commute mult_2_right numeral_Bit0 power_mult)
finally show ?thesis .
qed
lemma pow8_le_2pow8: "z ^ 8 ≤ 2 ^ (8*z)" for z :: nat
proof -
have "z ^ 8 = (z ^ 2) ^ 4"
by simp
also have "... ≤ (2^(2*z)) ^ 4"
using pow2_le_2pow2 power_mono by blast
also have "... = 2^(8*z)"
by (metis mult.commute mult_2_right numeral_Bit0 power_mult)
finally show ?thesis .
qed
lemma Z_sq_le: "Z^2 ≤ 2^(16*Z)"
proof -
have "Z^2 ≤ 2^(2*Z)"
using pow2_le_2pow2[of Z] by simp
also have "... ≤ 2^(16*Z)"
by simp
finally show "Z^2 ≤ 2^(16*Z)" .
qed
lemma time_bound:
"ttt27 + 24 + 4 * (Suc (nllength σ) * 24 * Z ^ 2 * 2 ^ (4*Z)) + 2 * nlength t + 2 * nlength T ≤ 16114765 * 2^(16*Z) * N^6"
proof -
have sum_sq: "(a + b) ^ 2 ≤ Suc (2 * b) * a ^ 2 + b ^ 2" for a b :: nat
proof -
have "(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2"
by algebra
also have "... ≤ a ^ 2 + 2 * a ^ 2 * b + b ^ 2"
using linear_le_pow by simp
also have "... = Suc (2 * b) * a ^ 2 + b ^ 2"
by simp
finally show ?thesis .
qed
have 1: "t < N"
using t T' by simp
then have 15: "t ≤ N"
by simp
have 2: "nlength t < N"
using 1 nlength_le_n dual_order.strict_trans2 by blast
have 25: "nlength T ≤ N"
using T T' nlength_le_n by (meson le_trans order_less_imp_le)
have 27: "nlength (t - 1) < N"
using t(1) nlength_mono 2
by (metis diff_less dual_order.strict_trans2 less_numeral_extra(1) linorder_not_less order.asym)
have 3: "t * Z < N * Z"
using 1 Z_ge_1 by simp
then have 4: "N + t * Z < Suc Z * N"
using 1 by simp
have 41: "N + t * Z + Z ≤ Suc Z * N"
proof -
have "N + t * Z + Z ≤ N + (N - 1) * Z + Z"
using 1 N by auto
then show ?thesis
using N
by (metis One_nat_def Suc_n_not_le_n ab_semigroup_add_class.add_ac(1) add.commute mult.commute mult_eq_if times_nat.simps(2))
qed
have 42: "(t + Z)^2 ≤ (N + Z) ^ 2"
using 1 by simp
have 45: "(N + Z) ^ 2 ≤ 3*Z*N^2 + Z^2"
proof -
have "(N + Z) ^ 2 ≤ Suc (2 * Z) * N^2 + Z^2"
using sum_sq by simp
also have "... ≤ 3*Z * N^2 +Z^2"
using Z_ge_1 by simp
finally show ?thesis .
qed
have 5: "nlength (previous hp1 t) < N"
using previous_hp1_le 1 by (meson dual_order.strict_trans2 nlength_le_n)
then have 51: "nlength (previous hp1 t) ≤ N"
by simp
have 6: "nlength (N + t * Z) < Suc Z * N"
using 4 nlength_le_n by (meson le_trans linorder_not_le)
have "nllength σ ≤ 12 * N * Z^2 + 4 * Z * N"
proof -
have "nllength σ ≤ 12 * T' * Z^2 + 4 * Z * N"
using nllength_σ by simp
also have "... ≤ 12 * N * Z^2 + 4 * Z * N"
using T' by simp
finally show ?thesis .
qed
have 7: "previous hp1 t ≤ N"
using previous_hp1_le 15 by simp
have 65: "(nlength (previous hp1 t) + nlength Z)⇧2 < (N + Z) ^ 2"
proof -
have "nlength (previous hp1 t) + nlength Z < N + Z"
using 7 2 5 by (simp add: add_less_le_mono nlength_le_n)
then show ?thesis
by (simp add: power_strict_mono)
qed
have 66: "N + previous hp1 t * Z + Z ≤ Suc Z * N"
using 41 previous_hp1_le by (meson add_le_mono le_trans less_or_eq_imp_le mult_le_mono)
have 67: "(nlength t + nlength Z)⇧2 ≤ 3 * Z * N^2 + Z^2"
proof -
have "nlength t + nlength Z < N + Z"
using nlength_le_n 2 by (simp add: add_less_le_mono)
then have "(nlength t + nlength Z)^2 < (N + Z) ^ 2"
by (simp add: power_strict_mono)
then show ?thesis
using 45 by simp
qed
have "nlength (previous hp1 t * Z) ≤ N * Z"
using nlength_le_n previous_hp1_le 1 by (meson le_trans less_or_eq_imp_le mult_le_mono)
have 75: "max (nlength N) (nlength (t * Z)) ≤ Suc Z * N"
proof -
have "max (nlength N) (nlength (t * Z)) ≤ nlength (max N (t * Z))"
using max_nlength by simp
also have "... ≤ nlength (N + t * Z)"
by (simp add: nlength_mono)
finally show ?thesis
using 6 by simp
qed
then have 78: "max (nlength N) (nlength (previous hp1 t * Z)) ≤ Suc Z * N"
using previous_hp1_le nlength_mono by (smt (verit, best) Groups.mult_ac(2) le_trans max_def mult_le_mono2)
have 79: "nlength (N + t * Z + Z) ≤ Suc Z * N + Z"
proof -
have "N + t * Z + Z ≤ Suc Z * N + Z"
using previous_le 15 by simp
then show ?thesis
using nlength_le_n le_trans by blast
qed
have 8: "nllength [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] ≤ 2 * Z^2 * N + 2 * Z^2"
proof -
have "nllength [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] ≤
Suc (nlength (N + previous hp1 t * Z + Z)) * Z"
using nllength_upt_le_len_mult_max by (metis diff_add_inverse)
moreover have "nlength (N + previous hp1 t * Z + Z) ≤ Suc Z * N + Z"
proof -
have "N + previous hp1 t * Z + Z ≤ Suc Z * N + Z"
using previous_le 15 7 by simp
then show ?thesis
using nlength_le_n le_trans by blast
qed
ultimately have "nllength [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] ≤ Suc (Suc Z * N + Z) * Z"
by (meson Suc_le_mono le_trans less_or_eq_imp_le mult_le_mono)
also have "... = (Z^2 + Z) * Suc N"
by (metis add.commute mult.commute mult.left_commute mult_Suc nat_arith.suc1 power2_eq_square)
also have "... ≤ (Z^2 + Z^2) * Suc N"
by (meson add_le_cancel_left linear_le_pow mult_le_mono1 rel_simps(51))
also have "... = 2 * Z^2 * Suc N"
by simp
also have "... = 2 * Z^2 * N + 2 * Z^2"
by simp
finally show ?thesis .
qed
have 84: "Z * Suc Z ≤ 2 * Z^2"
by (simp add: power2_eq_square)
have 85: "nlength (N + previous hp1 t * Z) ≤ Suc Z * N"
proof -
have "nlength (N + previous hp1 t * Z) ≤ nlength (N + t * Z)"
using previous_hp1_le nlength_mono by simp
then show ?thesis
using 6 by simp
qed
have 9: "Suc Z ≤ 2*Z"
using Z_ge_1 by simp
then have 91: "Suc Z ^ 2 ≤ 4 * Z^2"
by (metis mult_2_right numeral_Bit0 power2_eq_square power2_nat_le_eq_le power_mult_distrib)
have 99: "Z^2 ≥ 81"
proof -
have "Z * Z ≥ 9 * 9"
using Z_ge_9 mult_le_mono by presburger
moreover have "9 * 9 = (81::nat)"
by simp
ultimately show ?thesis
by (simp add: power2_eq_square)
qed
have part1: "ttt8 ≤ 241 * Z^2 + 266 * Z^2 * N ^ 6"
proof -
have "ttt8 ≤ 168 + 153 * N ^ 6 + 5 * t + 26 * (t + Z)⇧2 + 47 * Z + 15 * Z * (N + t * Z)"
using ttt8_def T' by simp
also have "... ≤ 168 + 153 * N ^ 6 + 5 * N + 26 * (t + Z)⇧2 + 47 * Z + 15 * Z * (N + t * Z)"
using 15 by simp
also have "... ≤ 168 + 153 * N ^ 6 + 5 * N + 26 * (N + Z)⇧2 + 47 * Z + 15 * Z * (N + t * Z)"
using 42 by simp
also have "... ≤ 168 + 153 * N ^ 6 + 5 * N + 26 * (3*Z*N^2 + Z^2) + 47 * Z + 15 * Z * (N + t * Z)"
using 45 by simp
also have "... ≤ 168 + 153 * N ^ 6 + 5 * N + 26 * (3*Z*N^2 + Z^2) + 47 * Z + 15 * Z * Suc Z * N"
using 4 by (metis (mono_tags, lifting) add_left_mono less_or_eq_imp_le mult.assoc mult_le_mono2)
also have "... ≤ 168 + 153 * N ^ 6 + 5 * N + 26 * (3*Z*N^2 + Z^2) + 47 * Z + 30 * Z^2 * N"
using `Z * Suc Z ≤ 2 * Z^2` by simp
also have "... = 168 + 153 * N ^ 6 + 5 * N + 78 * Z * N^2 + 26*Z^2 + 47 * Z + 30 * Z^2 * N"
by simp
also have "... ≤ 168 + 158 * N ^ 6 + 78 * Z * N^2 + 73 * Z^2 + 30 * Z^2 * N"
using linear_le_pow[of 6 N] linear_le_pow[of 2 Z] by simp
also have "... ≤ 168 + 158 * N ^ 6 + 78 * Z^2 * N^2 + 73 * Z^2 + 30 * Z^2 * N^2"
using linear_le_pow
by (metis add_le_mono add_le_mono1 le_square mult_le_mono1 mult_le_mono2 nat_add_left_cancel_le power2_eq_square)
also have "... = 168 + 158 * N ^ 6 + 108 * Z^2 * N^2 + 73 * Z^2"
by simp
also have "... ≤ 168*Z^2 + 158 * N ^ 6 + 108 * Z^2 * N^2 + 73 * Z^2"
using Z_ge_1 by simp
also have "... ≤ 241 * Z^2 + 158 * N ^ 6 + 108 * Z^2 * N^6"
using pow_mono'[of 2 6 N] by simp
also have "... ≤ 241 * Z^2 + 158 * Z^2 * N ^ 6 + 108 * Z^2 * N^6"
using Z_ge_1 by simp
also have "... = 241 * Z^2 + 266 * Z^2 * N ^ 6"
by simp
finally show ?thesis .
qed
have part2: "ttt10 - ttt8 ≤ 63 * Z^2 + 226 * Z^2 * N^6"
proof -
have "ttt10 - ttt8 = 37 + 26 * (nlength (previous hp1 t) + nlength Z)⇧2 +
3 * max (nlength N) (nlength (previous hp1 t * Z)) +
Suc Z * (43 + 9 * nlength (N + previous hp1 t * Z + Z)) +
4 * nllength [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] +
2 * nlength (N + previous hp1 t * Z)"
using ttt10_def ttt8_def by simp
also have "... ≤ 37 + 26 * (nlength (previous hp1 t) + nlength Z)⇧2 +
3 * max (nlength N) (nlength (previous hp1 t * Z)) +
Suc Z * (43 + 9 * nlength (N + previous hp1 t * Z + Z)) +
4 * (2 * Z^2 * N + 2 * Z^2) + 2 * nlength (N + previous hp1 t * Z)"
using 8 by simp
also have "... ≤ 37 + 26 * (N + Z)⇧2 +
3 * max (nlength N) (nlength (previous hp1 t * Z)) +
Suc Z * (43 + 9 * nlength (N + previous hp1 t * Z + Z)) +
4 * (2 * Z^2 * N + 2 * Z^2) + 2 * nlength (N + previous hp1 t * Z)"
using 65 by linarith
also have "... ≤ 37 + 26 * (3*Z*N^2 + Z^2) + 3 * (Suc Z * N) +
Suc Z * (43 + 9 * nlength (N + previous hp1 t * Z + Z)) +
8 * Z^2 * N + 8 * Z^2 + 2 * nlength (N + previous hp1 t * Z)"
using 78 45 by auto
also have "... ≤ 37 + 26 * (3*Z*N^2 + Z^2) + 3 * (Suc Z * N) +
Suc Z * (43 + 9 * nlength (N + previous hp1 t * Z + Z)) +
8 * Z^2 * N + 8 * Z^2 + 2 * Suc Z * N"
using 85 by linarith
also have "... ≤ 37 + 26 * (3*Z*N^2 + Z^2) + 3 * (Suc Z * N) +
Suc Z * (43 + 9 * nlength (Suc Z * N)) +
8 * Z^2 * N + 8 * Z^2 + 2 * Suc Z * N"
using 66 nlength_mono add_le_mono le_refl mult_le_mono by presburger
also have "... ≤ 37 + 26 * (3*Z*N^2 + Z^2) + 3 * (Suc Z * N) +
Suc Z * (43 + 9 * (Suc Z * N)) +
8 * Z^2 * N + 8 * Z^2 + 2 * Suc Z * N"
using nlength_le_n add_le_mono le_refl mult_le_mono by presburger
also have "... = 37 + 26 * (3*Z*N^2 + Z^2) + 3 * (Suc Z * N) +
43 * Suc Z + Suc Z * 9 * Suc Z * N +
8 * Z^2 * N + 8 * Z^2 + 2 * Suc Z * N"
by algebra
also have "... ≤ 37 + 26 * (3*Z*N^2 + Z^2) + 3 * (Suc Z * N) +
43 * 2 * Z + 2 * Z * 9 * Suc Z * N +
8 * Z^2 * N + 8 * Z^2 + 2 * Suc Z * N"
using 9 by (simp add: add_le_mono)
also have "... ≤ 37 + 26 * (3*Z*N^2 + Z^2) + 3 * (Suc Z * N) +
86 * Z + 36 * Z * Z * N + 8 * Z^2 * N + 8 * Z^2 + 2 * Suc Z * N"
by simp
also have "... ≤ 37 + 26 * (3*Z*N^2 + Z^2) + 3 * (Suc Z * N) +
86 * Z + 44 * Z^2 * N + 8 * Z^2 + 2 * Suc Z * N"
by (simp add: power2_eq_square)
also have "... ≤ 37 + 26 * (3*Z*N^2 + Z^2) + 3 * (Suc Z * N) +
86 * Z + 44 * Z^2 * N + 8 * Z^2 + 4 * Z * N"
using 9 by simp
also have "... ≤ 37 + 26 * (3*Z*N^2 + Z^2) + 3 * (Suc Z * N) +
86 * Z + 48 * Z^2 * N + 8 * Z^2"
using linear_le_pow by simp
also have "... ≤ 37 + 26 * (3*Z*N^2 + Z^2) + 3 * 2 * Z * N +
86 * Z + 48 * Z^2 * N + 8 * Z^2"
using 9 by simp
also have "... ≤ 37 + 26 * (3*Z*N^2 + Z^2) + 6 * Z * N +
86 * Z^2 * N + 48 * Z^2 * N + 8 * Z^2"
using linear_le_pow[of 2 Z] N by simp (metis N le_trans mult_le_mono1 nat_mult_1)
also have "... ≤ 37 + 26 * (3*Z*N^2 + Z^2) + 140 * Z^2 * N + 8 * Z^2"
using linear_le_pow[of 2 Z] by simp
also have "... ≤ 37 + 26 * (3*Z*N^2 + Z^2) + 148 * Z^2 * N"
using N by simp
also have "... = 37 + 78 * Z * N^2 + 26 * Z^2 + 148 * Z^2 * N"
by simp
also have "... ≤ 63 * Z^2 + 78 * Z * N^2 + 148 * Z^2 * N"
using Z_ge_1 by simp
also have "... ≤ 63 * Z^2 + 78 * Z^2 * N^2 + 148 * Z^2 * N"
using linear_le_pow by simp
also have "... ≤ 63 * Z^2 + 226 * Z^2 * N^2"
using linear_le_pow by simp
also have "... ≤ 63 * Z^2 + 226 * Z^2 * N^6"
using pow_mono'[of 2 6 N] by simp
finally show ?thesis .
qed
have 10: "nllength hp0 ≤ N ^ 2"
proof -
have "∀n∈set hp0. n ≤ T'"
using hp0 by (metis in_set_conv_nth)
then have "nllength hp0 ≤ Suc T' * Suc T'"
using nllength_le[of hp0 T'] len_hp0 by simp
also have "... ≤ N * N"
using T' Suc_leI mult_le_mono by presburger
also have "... = N ^ 2"
by algebra
finally show ?thesis .
qed
have 11: "nllength [N + t * Z..<N + t * Z + Z] ≤ 2 * Z^2 * N + Z"
proof -
have "nllength [N + t * Z..<N + t * Z + Z] ≤ Suc (N + t * Z + Z) * Z"
using nllength_upt_le[of "N + t * Z" "N + t * Z + Z"] by simp
also have "... ≤ Suc (Suc Z * N) * Z"
using 41 by simp
also have "... = (Z*Z + Z)*N + Z"
by (metis add.commute mult.commute mult.left_commute mult_Suc)
also have "... ≤ 2 * Z^2 * N + Z"
using linear_le_pow[of 2 Z] by (simp add: power2_eq_square)
finally show ?thesis .
qed
have 12: "nlength (hp0 ! t) + nlength G ≤ N + Z"
proof -
have "nlength (hp0 ! t) + nlength G ≤ hp0 ! t + G"
using nlength_le_n by (simp add: add_mono)
also have "... ≤ T' + Z"
using Z by (simp add: add_le_mono hp0 le_imp_less_Suc len_hp0 t(2))
also have "... ≤ N + Z"
using T' by simp
finally show ?thesis .
qed
have part3: "ttt20 - ttt10 ≤ 120 * Z^2 + 206 * Z^2 * N ^ 4"
proof -
have "ttt20 - ttt10 = 80 + 2 * nlength (t - 1) + 26 * (nlength t + nlength Z)⇧2 +
3 * max (nlength N) (nlength (t * Z)) + Suc Z * (43 + 9 * nlength (N + t * Z + Z)) +
4 * nllength [N + t * Z..<N + t * Z + Z] + 2 * nlength (previous hp1 t) +
21 * (nllength hp0)⇧2 + 2 * nlength (N + t * Z) + 26 * (nlength (hp0 ! t) + nlength G)⇧2"
using ttt20_def ttt10_def by simp
also have "... ≤ 80 + 2 * N + 26 * (3 * Z * N^2 + Z^2) +
3 * (Suc Z * N) + Suc Z * (43 + 9 * nlength (N + t * Z + Z)) +
4 * nllength [N + t * Z..<N + t * Z + Z] + 2 * nlength (previous hp1 t) +
21 * (nllength hp0)⇧2 + 2 * nlength (N + t * Z) + 26 * (nlength (hp0 ! t) + nlength G)⇧2"
using 27 67 75 by auto
also have "... ≤ 80 + 2 * N + 26 * (3 * Z * N^2 + Z^2) +
3 * (Suc Z * N) + Suc Z * (43 + 9 * (Suc Z * N + Z)) +
4 * nllength [N + t * Z..<N + t * Z + Z] + 2 * nlength (previous hp1 t) +
21 * (nllength hp0)⇧2 + 2 * nlength (N + t * Z) + 26 * (nlength (hp0 ! t) + nlength G)⇧2"
using 79 add_le_mono le_refl mult_le_mono by presburger
also have "... ≤ 80 + 2 * N + 26 * (3 * Z * N^2 + Z^2) +
3 * (Suc Z * N) + Suc Z * (43 + 9 * (Suc Z * N + Z)) +
4 * nllength [N + t * Z..<N + t * Z + Z] + 2 * N +
21 * (nllength hp0)⇧2 + 2 * nlength (N + t * Z) + 26 * (N + Z)⇧2"
using 51 12
by (metis add_le_cancel_right add_le_mono nat_add_left_cancel_le nat_mult_le_cancel_disj power2_nat_le_eq_le)
also have "... ≤ 80 + 4 * N + 52 * (3 * Z * N^2 + Z^2) + 3 * (Suc Z * N) + Suc Z * (43 + 9 * (Suc Z * N + Z)) +
4 * nllength [N + t * Z..<N + t * Z + Z] + 21 * (nllength hp0)⇧2 + 2 * nlength (N + t * Z)"
using 45 by simp
also have "... ≤ 80 + 4 * N + 52 * (3 * Z * N^2 + Z^2) + 3 * (Suc Z * N) + Suc Z * (43 + 9 * (Suc Z * N + Z)) +
4 * nllength [N + t * Z..<N + t * Z + Z] + 21 * (nllength hp0)⇧2 + 2 * Suc Z * N"
using 6 by linarith
also have "... ≤ 80 + 4 * N + 52 * (3 * Z * N^2 + Z^2) + 3 * (Suc Z * N) + Suc Z * (43 + 9 * (Suc Z * N + Z)) +
4 * (2 * Z^2 * N + Z) + 21 * (N^2)⇧2 + 2 * Suc Z * N"
using 11 10 add_le_mono le_refl mult_le_mono2 power2_nat_le_eq_le by presburger
also have "... = 80 + 4 * N + 156 * Z * N^2 + 52 * Z^2 + 3 * (Suc Z * N) + Suc Z * (43 + 9 * (Suc Z * N + Z)) +
8 * Z^2 * N + 4 * Z + 21 * N ^ 4 + 2 * Suc Z * N"
by simp
also have "... = 80 + 156 * Z * N^2 + 52 * Z^2 + Suc Z * 43 + Suc Z * 9 * Suc Z * N + Suc Z * 9 * Z +
(4 + 5 * Suc Z + 8 * Z^2) * N + 4 * Z + 21 * N ^ 4"
by algebra
also have "... = 123 + 156 * Z * N^2 + 52 * Z^2 + 47 * Z + 9 * Suc Z * Suc Z * N + Suc Z * 9 * Z +
(9 + 5 * Z + 8 * Z^2) * N + 21 * N ^ 4"
by simp
also have "... = 123 + 156 * Z * N^2 + 52 * Z^2 + 47 * Z + 9 * Z * Suc Z +
(9 * Suc Z^2 + 9 + 5 * Z + 8 * Z^2) * N + 21 * N ^ 4"
by algebra
also have "... ≤ 123 + 156 * Z * N^2 + 52 * Z^2 + 47 * Z + 9 * Z * Suc Z +
(44 * Z^2 + 9 + 5 * Z) * N + 21 * N ^ 4"
using 91 by simp
also have "... ≤ 123 + 156 * Z * N^2 + 70 * Z^2 + 47 * Z + (44 * Z^2 + 9 + 5 * Z) * N + 21 * N ^ 4"
using 84 by simp
also have "... ≤ 123 + 156 * Z * N^2 + 70 * Z^2 + 47 * Z^2 + (44 * Z^2 + 9 + 5 * Z^2) * N + 21 * N ^ 4"
using linear_le_pow[of 2 Z] add_le_mono le_refl mult_le_mono power2_nat_le_imp_le
by presburger
also have "... ≤ 123 + 156 * Z * N^2 + 117 * Z^2 + (49 * Z^2 + 9) * N ^ 4 + 21 * N ^ 4"
using linear_le_pow[of 4 N] by simp
also have "... ≤ 123 + 156 * Z * N^4 + 117 * Z^2 + (49 * Z^2 + 9) * N ^ 4 + 21 * N ^ 4"
using pow_mono'[of 2 4 N] by simp
also have "... = 123 + 117 * Z^2 + (156 * Z + 49 * Z^2 + 30) * N ^ 4"
by algebra
also have "... ≤ 123 + 117 * Z^2 + (205 * Z^2 + 30) * N ^ 4"
using linear_le_pow[of 2 Z] by simp
also have "... ≤ 120 * Z^2 + (205 * Z^2 + 30) * N ^ 4"
using 99 by simp
also have "... ≤ 120 * Z^2 + 206 * Z^2 * N ^ 4"
using 99 by simp
finally show ?thesis .
qed
have 12: "hp0 ! t * G + G ≤ Z * N"
proof -
have "hp0 ! t * G + G ≤ T' * G + G"
using hp0 t(2) len_hp0 by simp
also have "... ≤ (N - 1) * G + G"
using T' by auto
also have "... = N * G"
using T' by (metis Suc_diff_1 add.commute less_nat_zero_code mult_Suc not_gr_zero)
also have "... ≤ Z * N"
using Z by simp
finally show ?thesis .
qed
have 13: "Suc G * (43 + 9 * nlength (hp0 ! t * G + G)) ≤ 43 * Z + 9 * Z^2 * N"
proof -
have "Suc G * (43 + 9 * nlength (hp0 ! t * G + G)) ≤ Suc G * (43 + 9 * (hp0 ! t * G + G))"
using nlength_le_n add_le_mono le_refl mult_le_mono by presburger
also have "... ≤ Suc G * (43 + 9 * (Z * N))"
using 12 add_le_mono less_or_eq_imp_le mult_le_mono by presburger
also have "... ≤ Z * (43 + 9 * (Z * N))"
using G Z by simp
also have "... = 43 * Z + 9 * N * Z * Z"
by algebra
also have "... = 43 * Z + 9 * Z^2 * N"
by algebra
finally show ?thesis .
qed
have 14: "nllength [hp0 ! t * G..<hp0 ! t * G + G] ≤ Z^2 * N"
proof -
have "nllength [hp0 ! t * G..<hp0 ! t * G + G] ≤ (hp0 ! t * G + G) * Suc G"
using nllength_upt_le[of "hp0 ! t * G" "hp0 ! t * G + G"] by simp
also have "... ≤ (hp0 ! t * G + G) * Z"
using Z G by simp
also have "... ≤ N * Z * Z"
using 12 by (simp add: mult.commute)
also have "... = Z^2 * N"
by algebra
finally show ?thesis .
qed
have 15: "nlength (hp0 ! t) ≤ N"
using T' hp0 t(2) len_hp0 nlength_le_n by (metis le_imp_less_Suc le_trans less_or_eq_imp_le)
have 16: "nlength (hp0 ! t * G) ≤ Z * N"
proof -
have "nlength (hp0 ! t * G) ≤ hp0 ! t * G"
using nlength_le_n by simp
also have "... ≤ T' * G"
using Z T' hp0 t(2) len_hp0 by simp
also have "... ≤ Z * N"
using Z T' by simp
finally show ?thesis .
qed
have 17: "(12 * T' * Z⇧2 + 4 * Z * N) ^ 2 ≤ 256 * Z^4 * N^2"
proof -
have "(12 * T' * Z⇧2 + 4 * Z * N) ^ 2 ≤ (12 * N * Z^2 + 4 * Z * N)^2"
using T' by simp
also have "... ≤ (12 * N * Z^2 + 4 * Z^2 * N)^2"
using linear_le_pow[of 2 Z] add_le_mono le_refl mult_le_mono power2_nat_le_eq_le power2_nat_le_imp_le
by presburger
also have "... = 256 * Z^4 * N^2"
by algebra
finally show ?thesis .
qed
have 18: "108 * (24 * Z⇧2 * 2 ^ (4 * Z))⇧2 * (3 + (12 * T' * Z⇧2 + 4 * Z * N)⇧2) ≤ 16111872 * 2^(16*Z) * N^2"
proof -
have "108 * (24 * Z⇧2 * 2 ^ (4 * Z))⇧2 = 62208 * (Z^2 * 2 ^ (4*Z))^2"
by algebra
also have "... = 62208 * Z^(2*2) * 2 ^ (2*(4*Z))"
by (metis (no_types, lifting) mult.assoc power_even_eq power_mult_distrib)
also have "... = 62208 * Z^4 * 2 ^ (8*Z)"
by simp
finally have *: "108 * (24 * Z⇧2 * 2 ^ (4 * Z))⇧2 = 62208 * Z^4 * 2 ^ (8*Z)" .
have "3 + (12 * T' * Z⇧2 + 4 * Z * N)⇧2 ≤ 3 + 256 * Z^4 * N^2"
using 17 by simp
moreover have "Z^4 * N^2 ≥ 1"
using Z_ge_1 N by simp
ultimately have "3 + (12 * T' * Z⇧2 + 4 * Z * N)⇧2 ≤ 259 * Z^4 * N^2"
by linarith
then have "108 * (24 * Z⇧2 * 2 ^ (4 * Z))⇧2 * (3 + (12 * T' * Z⇧2 + 4 * Z * N)⇧2) ≤
16111872 * Z^4 * 2 ^ (8*Z) * Z^4 * N^2"
using * by simp
also have "... = 16111872 * Z^8 * 2 ^ (8*Z) * N^2"
by simp
also have "... ≤ 16111872 * 2^(8*Z) * 2 ^ (8*Z) * N^2"
using pow8_le_2pow8 by simp
also have "... = 16111872 * 2^(8*Z+8*Z) * N^2"
by (metis (no_types, lifting) mult.assoc power_add)
also have "... = 16111872 * 2^(16*Z) * N^2"
by simp
finally show ?thesis .
qed
have 19: "nllength σ ≤ 16 * Z^2 * N"
proof -
have "nllength σ ≤ 12 * T' * Z^2 + 4 * Z * N"
using nllength_σ by simp
also have "... ≤ 12 * N * Z^2 + 4 * Z * N"
using T' by simp
also have "... ≤ 12 * Z^2 * N + 4 * Z^2 * N"
using linear_le_pow[of 2 Z] by simp
also have "... ≤ 16 * Z^2 * N"
by simp
finally show ?thesis .
qed
have part4: "ttt27 - ttt20 ≤ 50 * Z + 16111936 * 2^(16*Z) * N^2"
proof -
have "ttt27 - ttt20 = 55 + Suc G * (43 + 9 * nlength (hp0 ! t * G + G)) +
4 * nllength [hp0 ! t * G..<hp0 ! t * G + G] +
2 * nlength (hp0 ! t * G) + 2 * nlength (hp0 ! t) + 3 * nllength σ +
108 * (24 * Z⇧2 * 2 ^ (4 * Z))⇧2 * (3 + (12 * T' * Z⇧2 + 4 * Z * N)⇧2)"
using ttt27_def ttt20_def by linarith
also have "... ≤ 55 + Suc G * (43 + 9 * nlength (hp0 ! t * G + G)) +
4 * nllength [hp0 ! t * G..<hp0 ! t * G + G] +
2 * nlength (hp0 ! t * G) + 2 * nlength (hp0 ! t) + 3 * (16 * Z^2 * N) +
108 * (24 * Z⇧2 * 2 ^ (4 * Z))⇧2 * (3 + (12 * T' * Z⇧2 + 4 * Z * N)⇧2)"
using 19 by (simp add: mult.commute)
also have "... ≤ 55 + Suc G * (43 + 9 * nlength (hp0 ! t * G + G)) +
2 * Z * N + 2 * N + 52 * Z^2 * N + 16111872 * 2^(16*Z) * N^2"
using 14 15 16 18 by linarith
also have "... ≤ 55 + 43 * Z + 9 * Z^2 * N + 2 * Z * N + 2 * N + 52 * Z^2 * N + 16111872 * 2^(16*Z) * N^2"
using 13 by linarith
also have "... = 55 + 43 * Z + 2 * Z * N + 2 * N + 61 * Z^2 * N + 16111872 * 2^(16*Z) * N^2"
by simp
also have "... ≤ 50 * Z + 2 * Z * N + 2 * N + 61 * Z^2 * N + 16111872 * 2^(16*Z) * N^2"
using Z_ge_9 by simp
also have "... ≤ 50 * Z + 3 * Z * N + 61 * Z^2 * N + 16111872 * 2^(16*Z) * N^2"
using Z_ge_9 by simp
also have "... ≤ 50 * Z + 64 * Z^2 * N + 16111872 * 2^(16*Z) * N^2"
using linear_le_pow[of 2 Z] by simp
also have "... ≤ 50 * Z + 64 * Z^2 * N^2 + 16111872 * 2^(16*Z) * N^2"
using linear_le_pow[of 2 N] by simp
also have "... ≤ 50 * Z + 64 * 2^(2*Z) * N^2 + 16111872 * 2^(16*Z) * N^2"
using pow2_le_2pow2 by simp
also have "... ≤ 50 * Z + 64 * 2^(16*Z) * N^2 + 16111872 * 2^(16*Z) * N^2"
by simp
also have "... = 50 * Z + 16111936 * 2^(16*Z) * N^2"
by simp
finally show ?thesis .
qed
have part5: "24 + 4 * (Suc (nllength σ) * 24 * Z ^ 2 * 2 ^ (4*Z)) + 2 * nlength t + 2 * nlength T ≤
24 + 1633 * 2^(8*Z) * N"
proof -
have "24 + 4 * (Suc (nllength σ) * 24 * Z ^ 2 * 2 ^ (4*Z)) + 2 * nlength t + 2 * nlength T ≤
24 + 4 * (Suc (nllength σ) * 24 * Z ^ 2 * 2 ^ (4*Z)) + 4 * N"
using 25 2 by simp
also have "... ≤ 24 + 4 * (Suc (16 * Z^2 * N) * 24 * Z ^ 2 * 2 ^ (4*Z)) + 4 * N"
using 19 by (simp add: mult.commute)
also have "... ≤ 24 + 1632 * Z^2 * N * Z ^ 2 * 2 ^ (4*Z) + 4 * N"
using Z N by simp
also have "... = 24 + 1632 * Z^4 * 2 ^ (4*Z) * N + 4 * N"
by simp
also have "... ≤ 24 + 1632 * 2^(4*Z) * 2 ^ (4*Z) * N + 4 * N"
using pow4_le_2pow4 by simp
also have "... = 24 + 1632 * 2^(8*Z) * N + 4 * N"
by (metis (no_types, lifting) ab_semigroup_mult_class.mult_ac(1) add_mult_distrib numeral_Bit0 power_add)
also have "... ≤ 24 + 1632 * 2^(8*Z) * N + 2^(8*Z) * N"
proof -
have "(4::nat) ≤ 2 ^ 8"
by simp
also have "... ≤ 2 ^ (8*Z)"
using Z_ge_1 by (metis nat_mult_1_right nat_mult_le_cancel_disj one_le_numeral power_increasing)
finally have "(4::nat) ≤ 2 ^ (8*Z)" .
then show ?thesis
by simp
qed
also have "... ≤ 24 + 1633 * 2^(8*Z) * N"
by simp
finally show ?thesis .
qed
show "ttt27 + 24 + 4 * (Suc (nllength σ) * 24 * Z ^ 2 * 2 ^ (4*Z)) + 2 * nlength t + 2 * nlength T ≤
16114765 * 2^(16*Z) * N^6"
proof -
have "ttt27 ≤ ttt20 + 50 * Z + 16111936 * 2^(16*Z) * N^2"
using part4 ttt27_def by simp
also have "... ≤ ttt10 + 120 * Z^2 + 206 * Z^2 * N ^ 4 + 50 * Z + 16111936 * 2^(16*Z) * N^2"
using part3 ttt20_def by simp
also have "... ≤ ttt8 + 63 * Z^2 + 226 * Z^2 * N^6 + 120 * Z^2 + 206 * Z^2 * N ^ 4 + 50 * Z +
16111936 * 2^(16*Z) * N^2"
using part2 ttt10_def by simp
also have "... ≤ 241 * Z^2 + 266 * Z^2 * N ^ 6 + 63 * Z^2 + 226 * Z^2 * N^6 + 120 * Z^2 +
206 * Z^2 * N ^ 4 + 50 * Z + 16111936 * 2^(16*Z) * N^2"
using part1 by simp
also have "... = 424 * Z^2 + 492 * Z^2 * N ^ 6 + 206 * Z^2 * N ^ 4 + 50 * Z + 16111936 * 2^(16*Z) * N^2"
by simp
also have "... ≤ 474 * Z^2 + 492 * Z^2 * N ^ 6 + 206 * Z^2 * N ^ 4 + 16111936 * 2^(16*Z) * N^2"
using linear_le_pow[of 2 Z] by simp
also have "... ≤ 474 * Z^2 + 698 * Z^2 * N ^ 6 + 16111936 * 2^(16*Z) * N^2"
using pow_mono'[of 4 6 N] by simp
also have "... ≤ 474 * Z^2 + 698 * Z^2 * N ^ 6 + 16111936 * 2^(16*Z) * N^6"
using pow_mono'[of 2 6 N] by simp
also have "... ≤ 474 * Z^2 + 698 * 2^(16*Z) * N ^ 6 + 16111936 * 2^(16*Z) * N^6"
using Z_sq_le by simp
also have "... = 474 * Z^2 + 16112634 * 2^(16*Z) * N^6"
by simp
also have "... ≤ 474 * 2^(16*Z) + 16112634 * 2^(16*Z) * N^6"
using Z_sq_le by simp
also have "... ≤ 16113108 * 2^(16*Z) * N^6"
using N by simp
finally have "ttt27 ≤ 16113108 * 2^(16*Z) * N^6" .
then have "ttt27 + 24 + 4 * (Suc (nllength σ) * 24 * Z ^ 2 * 2 ^ (4*Z)) + 2 * nlength t + 2 * nlength T ≤
16113108 * 2^(16*Z) * N^6 + 24 + 1633 * 2^(8*Z) * N"
using part5 by simp
also have "... ≤ 16113108 * 2^(16*Z) * N^6 + 24 + 1633 * 2^(16*Z) * N"
by simp
also have "... ≤ 16113108 * 2^(16*Z) * N^6 + 24 + 1633 * 2^(16*Z) * N^6"
using linear_le_pow[of 6 N] by simp
also have "... = 24 + 16114741 * 2^(16*Z) * N^6"
by simp
also have "... ≤ 24 * 2^(16*Z) + 16114741 * 2^(16*Z) * N^6"
using Z_sq_le by simp
also have "... ≤ 16114765 * 2^(16*Z) * N^6"
using N by simp
finally show ?thesis .
qed
qed
lemma tm30':
assumes "ttt = 16114765 * 2^(16*Z) * N^6"
shows "transforms tm30 tps0 ttt tps30"
using tm30 time_bound transforms_monotone assms by simp
end
end
lemma transforms_tm_chi:
fixes j1 j2 j3 :: tapeidx
fixes tps tps' :: "tape list" and k G N Z T' T t :: nat and hp0 hp1 :: "nat list" and ψ ψ' :: formula
fixes nss :: "nat list list"
assumes "length tps = k"
and "1 < j1" "j1 < j2" "j2 < j3" "j3 + 17 < k"
and "G ≥ 3"
and "Z = 3 * G"
and "N ≥ 1"
and "length hp0 = Suc T'"
and "∀i<length hp0. hp0 ! i ≤ T'"
and "length hp1 = Suc T'"
and "∀i<length hp1. hp1 ! i ≤ T'"
and "0 < t" "t ≤ T'"
and "0 < T" "T ≤ T'"
and "T' < N"
and "variables ψ ⊆ {..<3*Z+G}" "fsize ψ ≤ (3*Z+G) * 2 ^ (3*Z+G)" "length ψ ≤ 2 ^ (3*Z+G)"
and "variables ψ' ⊆ {..<2*Z+G}" "fsize ψ' ≤ (2*Z+G) * 2 ^ (2*Z+G)" "length ψ' ≤ 2 ^ (2*Z+G)"
assumes
"tps ! 1 = nlltape nss"
"tps ! j1 = (⌊hp0⌋⇩N⇩L, 1)"
"tps ! j2 = (⌊hp1⌋⇩N⇩L, 1)"
"tps ! j3 = (⌊N⌋⇩N, 1)"
"tps ! (j3 + 1) = (⌊G⌋⇩N, 1)"
"tps ! (j3 + 2) = (⌊Z⌋⇩N, 1)"
"tps ! (j3 + 3) = (⌊T⌋⇩N, 1)"
"tps ! (j3 + 4) = (⌊formula_n ψ⌋⇩N⇩L⇩L, 1)"
"tps ! (j3 + 5) = (⌊formula_n ψ'⌋⇩N⇩L⇩L, 1)"
"tps ! (j3 + 6) = (⌊t⌋⇩N, 1)"
"⋀i. 6 < i ⟹ i < 17 ⟹ tps ! (j3 + i) = (⌊[]⌋, 1)"
assumes "tps' = tps
[1 := nlltape (nss @ formula_n (relabel
([N + (t - 1) * Z..<N + (t - 1) * Z + Z] @
(if previous hp1 t ≠ t then [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] else []) @
[N + t * Z..<N + t * Z + Z] @
[hp0 ! t * G..<hp0 ! t * G + G])
(if previous hp1 t = t then ψ' else ψ))),
j3 + 6 := (⌊Suc t⌋⇩N, 1),
j3 + 3 := (⌊T - 1⌋⇩N, 1)]"
assumes "ttt = 16114765 * 2 ^ (16*Z) * N^6"
shows "transforms (tm_chi j1 j2 j3) tps ttt tps'"
proof -
interpret loc: turing_machine_chi j1 j2 j3 .
show ?thesis
using loc.tm30'[OF assms(1-34)] loc.tps30_def[OF assms(1-34)] assms(35,36) loc.tm30_eq_tm_chi
by simp
qed
subsubsection ‹A Turing machine for $\Phi_9$ proper›
text ‹
The formula $\Phi_9$ is a conjunction of formulas $\chi_t$. The TM @{const
tm_chi} decreases the number on tape $j_3 + 3$. If this tape is initialized with
$T'$, then a while loop with @{const tm_chi} as its body will generate $\Phi_9$.
The next TM is such a machine:
›
definition tm_PHI9 :: "tapeidx ⇒ tapeidx ⇒ tapeidx ⇒ machine" where
"tm_PHI9 j1 j2 j3 ≡ WHILE [] ; λrs. rs ! (j3 + 3) ≠ □ DO tm_chi j1 j2 j3 DONE"
lemma tm_PHI9_tm:
assumes "0 < j1" and "j1 < j2" and "j2 < j3" and "j3 + 17 < k" and "G ≥ 6"
shows "turing_machine k G (tm_PHI9 j1 j2 j3)"
unfolding tm_PHI9_def
using tm_chi_tm turing_machine_loop_turing_machine Nil_tm assms by simp
lemma map_nth:
fixes zs ys f n i
assumes "zs = map f [0..<n]" and "i < length zs"
shows "zs ! i = f i"
using assms by simp
lemma concat_formula_n:
"concat (map (λt. formula_n (φ t)) [0..<n]) = formula_n (concat (map (λt. φ t) [0..<n]))"
using formula_n_def by (induction n) simp_all
lemma upt_append_upt:
assumes "a ≤ b" and "b ≤ c"
shows "[a..<b] @ [b..<c] = [a..<c]"
proof (rule nth_equalityI)
show "length ([a..<b] @ [b..<c]) = length [a..<c]"
using assms by simp
show "([a..<b] @ [b..<c]) ! i = [a..<c] ! i" if "i < length ([a..<b] @ [b..<c])" for i
using assms that nth_append[of "[a..<b]" "[b..<c]" i] by (cases "i < b - a") simp_all
qed
text ‹
The semantics of the TM @{const tm_PHI9} can be proved inside the locale
@{locale reduction_sat_x} because it is a fairly simple TM.
›
context reduction_sat_x
begin
text ‹
The TM @{const tm_chi} is the first TM whose semantics we transfer into the
locale @{locale reduction_sat_x}.
›
lemma tm_chi:
fixes tps0 :: "tape list" and k t' t :: nat and j1 j2 j3 :: tapeidx
fixes nss :: "nat list list"
assumes jk: "length tps0 = k" "1 < j1" "j1 < j2" "j2 < j3" "j3 + 17 < k"
and t: "0 < t" "t ≤ T'"
and T: "0 < t'" "t' ≤ T'"
assumes "hp0 = map (λt. exc (zeros m) t <#> 0) [0..<Suc T']"
assumes "hp1 = map (λt. exc (zeros m) t <#> 1) [0..<Suc T']"
assumes tps0:
"tps0 ! 1 = nlltape nss"
"tps0 ! j1 = (⌊hp0⌋⇩N⇩L, 1)"
"tps0 ! j2 = (⌊hp1⌋⇩N⇩L, 1)"
"tps0 ! j3 = (⌊N⌋⇩N, 1)"
"tps0 ! (j3 + 1) = (⌊H⌋⇩N, 1)"
"tps0 ! (j3 + 2) = (⌊Z⌋⇩N, 1)"
"tps0 ! (j3 + 3) = (⌊t'⌋⇩N, 1)"
"tps0 ! (j3 + 4) = (⌊formula_n ψ⌋⇩N⇩L⇩L, 1)"
"tps0 ! (j3 + 5) = (⌊formula_n ψ'⌋⇩N⇩L⇩L, 1)"
"tps0 ! (j3 + 6) = (⌊t⌋⇩N, 1)"
"⋀i. 6 < i ⟹ i < 17 ⟹ tps0 ! (j3 + i) = (⌊[]⌋, 1)"
assumes "tps' = tps0
[1 := nlltape (nss @ formula_n (χ t)),
j3 + 6 := (⌊Suc t⌋⇩N, 1),
j3 + 3 := (⌊t' - 1⌋⇩N, 1)]"
assumes "ttt = 16114765 * 2^(16*Z) * N ^ 6"
shows "transforms (tm_chi j1 j2 j3) tps0 ttt tps'"
proof -
interpret loc: turing_machine_chi j1 j2 j3 .
have G: "H ≥ 3"
using H_gr_2 by simp
then have N: "N ≥ 1"
using N_eq by simp
have Z: "Z = 3 * H"
using Z_def by simp
have len_hp0: "length hp0 = Suc T'"
using assms by simp
have len_hp1: "length hp1 = Suc T'"
using assms by simp
have hp0: "∀i<length hp0. hp0 ! i ≤ T'"
proof standard+
fix i :: nat
assume "i < length hp0"
then have "hp0 ! i = exc (zeros m) i <#> 0"
using map_nth assms(10) by blast
then show "hp0 ! i ≤ T'"
using inputpos_less inputpos_def by simp
qed
have hp1: "∀i<length hp1. hp1 ! i ≤ T'"
proof standard+
fix i :: nat
assume "i < length hp1"
then have "hp1 ! i = exc (zeros m) i <#> 1"
using map_nth assms(11) by blast
then show "hp1 ! i ≤ T'"
using headpos_1_less by simp
qed
have psi: "variables ψ ⊆ {..<3*Z+H}" "fsize ψ ≤ (3*Z+H) * 2 ^ (3*Z+H)" "length ψ ≤ 2 ^ (3*Z+H)"
using psi by simp_all
have psi': "variables ψ' ⊆ {..<2*Z+H}" "fsize ψ' ≤ (2*Z+H) * 2 ^ (2*Z+H)" "length ψ' ≤ 2 ^ (2*Z+H)"
using psi' by simp_all
let ?sigma = "[N + (t - 1) * Z..<N + (t - 1) * Z + Z] @
(if previous hp1 t ≠ t then [N + previous hp1 t * Z..<N + previous hp1 t * Z + Z] else []) @
[N + t * Z..<N + t * Z + Z] @
[hp0 ! t * H..<hp0 ! t * H + H]"
have hp0_nth: "hp0 ! i = exc (zeros m) i <#> 0" if "i ≤ T' " for i
using that assms map_nth len_hp0 by (metis (no_types, lifting) le_imp_less_Suc)
then have hp0_eq_inputpos: "hp0 ! i = inputpos m i" if "i ≤ T' " for i
using inputpos_def that by simp
have hp1_nth: "hp1 ! i = exc (zeros m) i <#> 1" if "i ≤ T' " for i
using that assms map_nth len_hp1 by (metis (no_types, lifting) le_imp_less_Suc)
have previous_eq_prev: "previous hp1 idx = prev m idx" if "idx ≤ T' " for idx
proof (cases "∃i<idx. hp1 ! i = hp1 ! idx")
case True
then have 1: "∃i<idx. exc (zeros m) i <#> 1 = exc (zeros m) idx <#> 1"
using that hp1_nth by auto
then have "prev m idx = (GREATEST i. i < idx ∧ exc (zeros m) i <#> 1 = exc (zeros m) idx <#> 1)"
using prev_def by simp
have "previous hp1 idx = (GREATEST i. i < idx ∧ hp1 ! i = hp1 ! idx)"
using True previous_def by simp
also have "... = (GREATEST i. i < idx ∧ exc (zeros m) i <#> 1 = exc (zeros m) idx <#> 1)"
(is "Greatest ?P = Greatest ?Q")
proof (rule Greatest_equality)
have "∃i. ?Q i"
using 1 by simp
moreover have 2: "∀y. ?Q y ⟶ y ≤ idx"
by simp
ultimately have 3: "?Q (Greatest ?Q)"
using GreatestI_ex_nat[of ?Q] by blast
then have 4: "Greatest ?Q < idx"
by simp
then have "Greatest ?Q ≤ T' "
using that by simp
then have "hp1 ! (Greatest ?Q) = exc (zeros m) (Greatest ?Q) <#> 1"
using hp1_nth by simp
moreover have "hp1 ! idx = exc (zeros m) idx <#> 1"
using that hp1_nth by simp
ultimately have "hp1 ! (Greatest ?Q) = hp1 ! idx"
using 3 by simp
then show "?P (Greatest ?Q)"
using 4 by simp
show "i ≤ Greatest ?Q" if "?P i" for i
proof -
have "i < idx"
using that by simp
then have "hp1 ! i = exc (zeros m) i <#> 1"
using `idx ≤ T' ` hp1_nth by simp
moreover have "hp1 ! idx = exc (zeros m) idx <#> 1"
using `idx ≤ T' ` hp1_nth by simp
ultimately have "exc (zeros m) i <#> 1 = exc (zeros m) idx <#> 1"
using that by simp
then have "?Q i"
using `i < idx` by simp
then show ?thesis
using Greatest_le_nat[of ?Q i] 2 by blast
qed
qed
also have "... = prev m idx"
using prev_def 1 by simp
finally show ?thesis .
next
case False
have "¬ (∃i<idx. exc (zeros m) i <#> 1 = exc (zeros m) idx <#> 1)"
proof (rule ccontr)
assume "¬ (¬ (∃i<idx. exc (zeros m) i <#> 1 = exc (zeros m) idx <#> 1))"
then obtain i where "i < idx" "exc (zeros m) i <#> 1 = exc (zeros m) idx <#> 1"
by auto
then have "hp1 ! i = hp1 ! idx"
using hp1_nth that by simp
then show False
using False `i < idx` by simp
qed
then have "prev m idx = idx"
using prev_def by auto
moreover have "previous hp1 idx = idx"
using False assms previous_def by auto
ultimately show ?thesis
by simp
qed
have "ζ⇩0 i @ ζ⇩1 i @ ζ⇩2 i = [N + i * Z..<N + (Suc i) * Z]" for i
using zeta0_def zeta1_def zeta2_def upt_append_upt Z by simp
then have zeta012: "ζ⇩0 i @ ζ⇩1 i @ ζ⇩2 i = [N + i * Z..<N + i * Z + Z]" for i
by (simp add: ab_semigroup_add_class.add_ac(1) add.commute[of Z "i*Z"])
have gamma: "γ (inputpos m i) = [inputpos m i * H..<inputpos m i * H + H]" for i
using gamma_def by (simp add: add.commute)
have rho: "ρ t = ?sigma" if "prev m t < t"
proof -
have "previous hp1 t ≠ t"
using t that previous_eq_prev by simp
then have "?sigma = [N + (t - 1) * Z..<N + (t - 1) * Z + Z] @
[N + prev m t * Z..<N + prev m t * Z + Z] @
[N + t * Z..<N + t * Z + Z] @
[inputpos m t * H..<inputpos m t * H + H]"
using previous_eq_prev hp0_eq_inputpos t by simp
also have "... = (ζ⇩0 (t - 1) @ ζ⇩1 (t - 1) @ ζ⇩2 (t - 1)) @
(ζ⇩0 (prev m t) @ ζ⇩1 (prev m t) @ ζ⇩2 (prev m t)) @
(ζ⇩0 t @ ζ⇩1 t @ ζ⇩2 t) @
γ (inputpos m t)"
using zeta012 gamma by simp
also have "... = ρ t"
using rho_def by simp
finally have "?sigma = ρ t" .
then show ?thesis
by simp
qed
have rho': "ρ' t = ?sigma" if "prev m t = t"
proof -
have "previous hp1 t = t"
using t that previous_eq_prev by simp
then have "?sigma = [N + (t - 1) * Z..<N + (t - 1) * Z + Z] @
[N + t * Z..<N + t * Z + Z] @
[inputpos m t * H..<inputpos m t * H + H]"
using previous_eq_prev hp0_eq_inputpos t by simp
also have "... = (ζ⇩0 (t - 1) @ ζ⇩1 (t - 1) @ ζ⇩2 (t - 1)) @
(ζ⇩0 t @ ζ⇩1 t @ ζ⇩2 t) @
γ (inputpos m t)"
using zeta012 gamma by simp
also have "... = ρ' t"
using rho'_def by simp
finally have "?sigma = ρ' t" .
then show ?thesis
by simp
qed
have "χ t = relabel ?sigma (if previous hp1 t = t then ψ' else ψ)"
proof (cases "prev m t < t")
case True
then have "χ t = relabel (ρ t) ψ"
using chi_def by simp
moreover have "previous hp1 t < t"
using t True previous_eq_prev by simp
ultimately show ?thesis
using rho True by simp
next
case False
then have *: "prev m t = t"
by (simp add: nat_less_le prev_le)
then have "χ t = relabel (ρ' t) ψ'"
using chi_def by simp
moreover have "previous hp1 t = t"
using t * previous_eq_prev by simp
ultimately show ?thesis
using rho' * by simp
qed
then show "transforms (tm_chi j1 j2 j3) tps0 ttt tps'"
using transforms_tm_chi[OF jk G Z N len_hp0 hp0 len_hp1 hp1 t T T'_less psi psi' tps0 _ assms(24)] assms(23)
by simp
qed
lemma Z_sq_le: "Z^2 ≤ 2^(16*Z)"
proof -
have "Z^2 ≤ 2^(2*Z)"
using pow2_le_2pow2[of Z] by simp
also have "... ≤ 2^(16*Z)"
by simp
finally show "Z^2 ≤ 2^(16*Z)" .
qed
lemma tm_PHI9 [transforms_intros]:
fixes tps0 tps' :: "tape list" and k :: nat and j1 j2 j3 :: tapeidx
fixes nss :: "nat list list"
assumes jk: "length tps0 = k" "1 < j1" "j1 < j2" "j2 < j3" "j3 + 17 < k"
assumes "hp0 = map (λt. exc (zeros m) t <#> 0) [0..<Suc T']"
assumes "hp1 = map (λt. exc (zeros m) t <#> 1) [0..<Suc T']"
assumes tps0:
"tps0 ! 1 = nlltape nss"
"tps0 ! j1 = (⌊hp0⌋⇩N⇩L, 1)"
"tps0 ! j2 = (⌊hp1⌋⇩N⇩L, 1)"
"tps0 ! j3 = (⌊N⌋⇩N, 1)"
"tps0 ! (j3 + 1) = (⌊H⌋⇩N, 1)"
"tps0 ! (j3 + 2) = (⌊Z⌋⇩N, 1)"
"tps0 ! (j3 + 3) = (⌊T'⌋⇩N, 1)"
"tps0 ! (j3 + 4) = (⌊formula_n psi⌋⇩N⇩L⇩L, 1)"
"tps0 ! (j3 + 5) = (⌊formula_n psi'⌋⇩N⇩L⇩L, 1)"
"tps0 ! (j3 + 6) = (⌊1⌋⇩N, 1)"
"⋀i. 6 < i ⟹ i < 17 ⟹ tps0 ! (j3 + i) = (⌊[]⌋, 1)"
assumes tps': "tps' = tps0
[1 := nlltape (nss @ formula_n Φ⇩9),
j3 + 6 := (⌊Suc T'⌋⇩N, 1),
j3 + 3 := (⌊0⌋⇩N, 1)]"
assumes "ttt = 16114767 * 2 ^ (16 * Z) * N ^ 7"
shows "transforms (tm_PHI9 j1 j2 j3) tps0 ttt tps'"
proof -
define tps where "tps = (λt. tps0
[1 := nlltape (nss @ concat (map (λt. formula_n (χ (Suc t))) [0..<t])),
j3 + 6 := (⌊Suc t⌋⇩N, 1),
j3 + 3 := (⌊T' - t⌋⇩N, 1)])"
have "transforms (tm_PHI9 j1 j2 j3) (tps 0) ttt (tps T')"
unfolding tm_PHI9_def
proof (tform)
let ?ttt = "16114765 * 2^(16*Z) * N ^ 6"
show "transforms (tm_chi j1 j2 j3) (tps i) ?ttt (tps (Suc i))" if "i < T' " for i
proof (rule tm_chi ; (use assms tps_def that in simp ; fail)?)
show "tps (Suc i) = (tps i)
[1 := nlltape
((nss @ concat (map (λt. formula_n (χ (Suc t))) [0..<i])) @
formula_n (χ (Suc i))),
j3 + 6 := (⌊Suc (Suc i)⌋⇩N, 1),
j3 + 3 := (⌊T' - i - 1⌋⇩N, 1)]"
using that tps_def by (simp add: list_update_swap)
qed
show "⋀i. i < T' ⟹ read (tps i) ! (j3 + 3) ≠ □"
using jk tps_def read_ncontents_eq_0 by simp
show "¬ read (tps T') ! (j3 + 3) ≠ □"
using jk tps_def read_ncontents_eq_0 by simp
show "T' * (16114765 * 2 ^ (16 * Z) * N ^ 6 + 2) + 1 ≤ ttt"
proof -
have "T' * (16114765 * 2 ^ (16 * Z) * N ^ 6 + 2) + 1 ≤ T' * (16114767 * 2 ^ (16 * Z) * N ^ 6) + 1"
using Z_sq_le H_gr_2 N_eq by auto
also have "... ≤ T' * (16114767 * 2 ^ (16 * Z) * N ^ 6) + (16114767 * 2 ^ (16 * Z) * N ^ 6)"
using H_gr_2 N_eq by auto
also have "... = Suc T' * (16114767 * 2 ^ (16 * Z) * N ^ 6)"
by simp
also have "... ≤ N * (16114767 * 2 ^ (16 * Z) * N ^ 6)"
using T'_less Suc_leI mult_le_mono1 by presburger
also have "... = 16114767 * 2 ^ (16 * Z) * N ^ 7"
by algebra
also have "... = ttt"
using assms(20) by simp
finally show ?thesis .
qed
qed
moreover have "tps 0 = tps0"
using tps_def tps0 list_update_id[of tps0 "Suc 0"] list_update_id[of tps0 "j3 + 6"]
list_update_id[of tps0 "j3 + 3"]
by simp
moreover have "tps T' = tps'"
proof -
have "concat (map (λt. formula_n (χ (Suc t))) [0..<T']) =
formula_n (concat (map (λt. χ (Suc t)) [0..<T']))"
using concat_formula_n by simp
then show ?thesis
using PHI9_def tps_def tps' list_update_id[of tps0 "Suc 0"] list_update_id[of tps0 "j3 + 6"]
list_update_id[of tps0 "j3 + 3"]
by simp
qed
ultimately show "transforms (tm_PHI9 j1 j2 j3) tps0 ttt tps'"
by simp
qed
end
end