:: Introduction to Turing Machines
:: by Jingchao Chen and Yatsuka Nakamura
::
:: Received July 27, 2001
:: Copyright (c) 2001-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, XBOOLE_0, FUNCT_1, PARTFUN1, FUNCT_4, RELAT_1,
TARSKI, FUNCOP_1, ORDINAL1, XXREAL_0, FINSET_1, CARD_1, FINSEQ_1, NAT_1,
CARD_3, ARYTM_3, QMAX_1, FSM_1, ZFMISC_1, ARYTM_1, FUNCT_2, LANG1, INT_1,
MCART_1, CIRCUIT2, MSUALG_1, ORDINAL4, VALUED_2, FINSEQ_2, UNIALG_1,
PRALG_3, TURING_1, RECDEF_2, VALUED_0;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1,
NUMBERS, XCMPLX_0, INT_1, FINSET_1, MCART_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, FUNCT_4, FUNCOP_1, GR_CY_1, FINSEQ_1, FINSEQ_2, FINSEQ_4,
VALUED_0, RVSUM_1, COMPUT_1, XXREAL_0, REAL_1, NAT_1, MARGREL1, DOMAIN_1;
constructors DOMAIN_1, REAL_1, BINOP_2, FINSEQ_4, FINSOP_1, GR_CY_1, COMPUT_1,
RECDEF_1, RELSET_1, XTUPLE_0, NAT_3, INT_6;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1,
NUMBERS, XREAL_0, INT_1, COMPUT_1, XTUPLE_0, CARD_1, NAT_1, VALUED_0,
FINSEQ_1, INT_6;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities FINSEQ_1, GR_CY_1, COMPUT_1, FUNCOP_1, ORDINAL1;
theorems FUNCOP_1, FUNCT_4, ZFMISC_1, TARSKI, FUNCT_2, INT_1, MCART_1, NAT_1,
RELSET_1, PARTFUN1, DOMAIN_1, ENUMSET1, FINSEQ_2, FINSEQ_1, FINSEQ_3,
RELAT_1, FINSEQ_6, FINSEQ_7, COMPUT_1, FINSEQ_4, ORDINAL1, XBOOLE_0,
XBOOLE_1, XREAL_1, FUNCT_7, FINSOP_1, XXREAL_0, RVSUM_1, XTUPLE_0;
schemes NAT_1, FUNCT_2, BINOP_2;
begin :: Preliminaries
reserve n,i,j,k for Nat;
definition
let A,B be non empty set, f be Function of A,B, g be PartFunc of A,B;
redefine func f +* g -> Function of A,B; :: redefines +* (FUNCT_4, definition)
coherence
proof
A1: now
let x be object;
assume
A2: x in A;
per cases;
suppose
A3: x in dom g;
then (f +* g).x=g.x by FUNCT_4:13;
hence (f +* g).x in B by A3,PARTFUN1:4;
end;
suppose
not x in dom g;
then (f +* g).x = f.x by FUNCT_4:11;
hence (f +* g).x in B by A2,FUNCT_2:5;
end;
end;
A4: dom f = A & dom g c= A by FUNCT_2:def 1,RELAT_1:def 18;
dom (f +* g) =dom f \/ dom g by FUNCT_4:def 1
.=A by A4,XBOOLE_1:12;
hence thesis by A1,FUNCT_2:3;
end;
end;
definition
let X,Y be non empty set, a be Element of X, b be Element of Y;
redefine func a .--> b -> PartFunc of X,Y; :: redefines .--> (FUNCOP_1, definition)
coherence
proof
set p = a .--> b;
dom p = {a} & rng p ={b} by FUNCOP_1:8;
then dom p c= X & rng p c= Y;
hence thesis by RELSET_1:4;
end;
end;
notation
let n be Nat;
synonym SegM n for succ n;
end;
definition
let n be Nat;
redefine func SegM n -> Subset of NAT equals :: redefines SegM (TURING_1, synonym) → succ (ORDINAL1, definition)
{k where k is Nat : k <= n};
coherence
proof
SegM n c= NAT;
hence thesis;
end;
compatibility
proof let S be Subset of NAT;
SegM Segm n = {k where k is Nat : k <= n} by NAT_1:54;
hence thesis;
end;
end;
theorem Th1: :: GR_CY 10
k in SegM n iff k <= n
proof
thus k in SegM n implies k <= n
proof
assume k in SegM n;
then ex i being Nat st k=i & i <= n;
hence thesis;
end;
thus thesis;
end;
theorem Th2:
for f be Function,x,y,z,u,v be object st u <> x holds (f +* ([x,y]
.--> z)).[u,v]=f.[u,v]
proof
let f be Function,x,y,z,u,v be object;
set p=[x,y] .--> z;
assume u <> x;
then
A1: [u,v]<>[x,y] by XTUPLE_0:1;
not [u,v] in dom p by A1,TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
theorem Th3:
for f be Function,x,y,z,u,v be object st v <> y holds (f +* ([x,y]
.--> z)).[u,v]=f.[u,v]
proof
let f be Function,x,y,z,u,v be object;
set p=[x,y] .--> z;
assume v <> y;
then
A1: [u,v]<>[x,y] by XTUPLE_0:1;
not [u,v] in dom p by A1,TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
notation
let i be Nat, f be FinSequence;
synonym Prefix(f,i) for f|i;
end;
registration let f be natural-valued FinSequence, n be Nat;
cluster Prefix(f,n) -> INT-valued for FinSequence;
coherence;
end;
theorem Th4:
for x1,x2 being Element of NAT holds Sum Prefix(<*x1,x2*>,1)=x1 &
Sum Prefix(<*x1,x2*>,2)=x1+x2
proof
let x1,x2 be Element of NAT;
reconsider y1=x1 as Element of INT by INT_1:def 2;
thus Sum Prefix(<*x1,x2*>,1)=Sum<*y1*> by FINSEQ_6:3
.=x1 by FINSOP_1:11;
reconsider y2=x2 as Element of INT by INT_1:def 2;
len <*x1,x2*>= 2 by FINSEQ_1:44;
hence Sum Prefix(<*x1,x2*>,2)=Sum<*y1,y2*> by FINSEQ_3:49
.=x1+x2 by RVSUM_1:77;
end;
theorem Th5:
for x1,x2,x3 being Element of NAT holds Sum Prefix(<*x1,x2,x3*>,1
)=x1 & Sum Prefix(<*x1,x2,x3*>,2)=x1+x2 & Sum Prefix(<*x1,x2,x3*>,3)=x1+x2+x3
proof
let x1,x2,x3 be Element of NAT;
reconsider y1=x1 as Element of INT by INT_1:def 2;
thus Sum Prefix(<*x1,x2,x3*>,1)=Sum<*y1*> by FINSEQ_6:4
.=x1 by FINSOP_1:11;
reconsider y2=x2 as Element of INT by INT_1:def 2;
thus Sum Prefix(<*x1,x2,x3*>,2)=Sum<*y1,y2*> by FINSEQ_6:5
.=x1+x2 by RVSUM_1:77;
reconsider y3=x3 as Element of INT by INT_1:def 2;
len <*x1,x2,x3*>= 3 by FINSEQ_1:45;
hence Sum Prefix(<*x1,x2,x3*>,3)=Sum<*y1,y2,y3*> by FINSEQ_3:49
.=x1+x2+x3 by RVSUM_1:78;
end;
begin :: Definitions and terminology for TURING Machine
definition
struct TuringStr (# Symbols, FStates -> finite non empty set,
Tran -> Function of [: the FStates, the Symbols :],
[: the FStates,the Symbols,{-1,0,1}
:], InitS,AcceptS -> Element of the FStates #);
end;
definition
let T be TuringStr;
mode State of T is Element of the FStates of T;
mode Tape of T is Element of Funcs(INT,the Symbols of T);
mode Symbol of T is Element of the Symbols of T;
end;
definition
let T be TuringStr,t be Tape of T, h be Integer,s be Symbol of T;
func Tape-Chg(t,h,s) -> Tape of T equals
t +* (h .--> s);
coherence
proof
set X=INT, Y=the Symbols of T;
A1: ex f being Function st t = f & dom f = X & rng f c= Y by FUNCT_2:def 2;
rng (h .--> s) ={s} by FUNCOP_1:8;
then rng (t +* (h .--> s)) c= rng t \/ rng (h .--> s) & rng t \/ rng (h
.--> s) c= Y by A1,FUNCT_4:17,XBOOLE_1:8;
then
A2: rng (t +* (h .--> s)) c= Y by XBOOLE_1:1;
A3: h in INT by INT_1:def 2;
dom(t +* (h .--> s)) = dom t \/ dom(h .--> s) by FUNCT_4:def 1
.= dom t \/ {h}
.= X by A1,A3,ZFMISC_1:40;
hence thesis by A2,FUNCT_2:def 2;
end;
end;
definition
let T be TuringStr;
mode All-State of T is
Element of [: the FStates of T, INT,Funcs(INT,the Symbols of T) :];
mode Tran-Source of T is
Element of [: the FStates of T,the Symbols of T:];
mode Tran-Goal of T is
Element of [: the FStates of T,the Symbols of T,{-1,0,1} :];
end;
definition
let T be TuringStr, g be Tran-Goal of T;
func offset(g) -> Integer equals
g`3_3;
coherence by ENUMSET1:def 1;
end;
definition
let T be TuringStr, s be All-State of T;
func Head(s) -> Integer equals
s`2_3;
coherence;
end;
definition
let T be TuringStr, s be All-State of T;
func TRAN(s) -> Tran-Goal of T equals
(the Tran of T).[s`1_3, (s`3_3 qua Tape of T).Head(s)];
correctness
proof
reconsider x=Head(s) as Element of INT;
(the Tran of T).[s`1_3, (s`3_3 qua Tape of T).x] is Tran-Goal of T;
hence thesis;
end;
end;
definition
let T be TuringStr, s be All-State of T;
func Following s -> All-State of T equals
:Def6:
[(TRAN(s))`1_3, Head(s)+offset TRAN (s),
Tape-Chg(s`3_3, Head(s),(TRAN(s))`2_3)] if s`1_3 <> the AcceptS of T
otherwise s;
correctness
proof
Head(s) + offset TRAN(s) in INT by INT_1:def 2;
hence thesis by MCART_1:69;
end;
end;
definition
let T be TuringStr, s be All-State of T;
func Computation s -> sequence of [: the FStates of T, INT,
Funcs(INT,
the Symbols of T) :] means
:Def7:
it.0 = s & for i being Nat holds it.(i+1) = Following(it.i);
existence
proof
deffunc U(set,All-State of T) = Following $2;
consider f being sequence of [: the FStates of T, INT,
Funcs(INT,the
Symbols of T) :] such that
A1: f.0 = s & for n being Nat holds f.(n+1) = U(n,f.n) from NAT_1:sch
12;
take f;
thus thesis by A1;
end;
uniqueness
proof
deffunc U(set,All-State of T) = Following $2;
let F1,F2 be sequence of [: the FStates of T, INT, Funcs(INT,the
Symbols of T) :] such that
A2: F1.0 = s and
A3: for i being Nat holds F1.(i+1) = Following(F1.i) and
A4: F2.0 = s and
A5: for i being Nat holds F2.(i+1) = Following(F2.i);
A6: for i being Nat holds F1.(i+1) = U(i,F1.i) by A3;
A7: for i being Nat holds F2.(i+1) = U(i,F2.i) by A5;
A8: F2.0 = s by A4;
A9: F1.0 = s by A2;
thus F1 = F2 from NAT_1:sch 16(A9,A6,A8,A7);
end;
end;
reserve T for TuringStr,
s for All-State of T;
theorem
for T being TuringStr, s be All-State of T st s`1_3 = the AcceptS of T
holds s = Following s by Def6;
theorem
(Computation s).0 = s by Def7;
theorem
(Computation s).(k+1) = Following (Computation s).k by Def7;
theorem Th9:
(Computation s).1 = Following s
proof
(Computation s).(0+1) = Following (Computation s).0 by Def7
.=Following s by Def7;
hence thesis;
end;
theorem Th10:
(Computation s).(i+k) = (Computation (Computation s).i).k
proof
defpred X[Nat] means
(Computation s).(i+$1) = (Computation (Computation s).i).$1;
A1: for k st X[k] holds X[k+1]
proof
let k;
assume
A2: (Computation s).(i+k) = (Computation (Computation s).i).k;
thus (Computation s).(i+(k+1)) = (Computation s).(i+k+1)
.= Following (Computation s).(i+k) by Def7
.= (Computation (Computation s).i).(k+1) by A2,Def7;
end;
A3: X[0] by Def7;
for k holds X[k] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th11:
i <= j & Following (Computation s).i = (Computation s).i implies
(Computation s).j = (Computation s).i
proof
assume that
A1: i <= j and
A2: Following (Computation s).i = (Computation s).i;
consider k be Nat such that
A3: j = i + k by A1,NAT_1:10;
defpred X[Nat] means
(Computation s).(i+$1) = (Computation s).i;
A4: for k st X[k] holds X[k+1]
proof
let k;
assume
A5: (Computation s).(i+k) = (Computation s).i;
thus (Computation s).(i+(k+1)) = (Computation s).(i+k+1)
.= (Computation s).i by A2,A5,Def7;
end;
A6: X[0];
A7: for k holds X[k] from NAT_1:sch 2(A6,A4);
thus thesis by A3,A7;
end;
theorem Th12:
i <= j & ((Computation s).i)`1_3 = the AcceptS of T implies (
Computation s).j = (Computation s).i
proof
assume that
A1: i <= j and
A2: ((Computation s).i)`1_3 = the AcceptS of T;
Following (Computation s).i = (Computation s).i by A2,Def6;
hence thesis by A1,Th11;
end;
definition
let T be TuringStr, s be All-State of T;
attr s is Accept-Halt means
ex k st ((Computation s).k)`1_3 = the AcceptS of T;
end;
definition
let T be TuringStr, s be All-State of T such that
A1: s is Accept-Halt;
func Result s -> All-State of T means
:Def9:
ex k st it = (Computation s).k & ((Computation s).k)`1_3 = the AcceptS of T;
uniqueness
proof
let s1,s2 be All-State of T;
given k1 being Nat such that
A2: s1 = (Computation s).k1 & ((Computation s).k1)`1_3 = the AcceptS of T;
given k2 being Nat such that
A3: s2 = (Computation s).k2 & ((Computation s).k2)`1_3 = the AcceptS of T;
k1 <= k2 or k2 <= k1;
hence thesis by A2,A3,Th12;
end;
correctness
by A1;
end;
theorem Th13:
for T being TuringStr,s be All-State of T st s is Accept-Halt
ex k being Nat st
((Computation s).k)`1_3 = the AcceptS of T &
Result s = (Computation s).k & for i be Nat st i < k holds ((
Computation s).i)`1_3 <> the AcceptS of T
proof
let T be TuringStr,s be All-State of T;
defpred P[Nat] means ((Computation s).$1)`1_3 = the AcceptS of T;
assume
A1: s is Accept-Halt;
then ex k st ((Computation s).k)`1_3 = the AcceptS of T;
then
A2: ex k be Nat st P[k];
consider k being Nat such that
A3: P[k] & for n be Nat st P[n] holds k <= n from NAT_1:sch 5(A2);
reconsider k as Element of NAT by ORDINAL1:def 12;
take k;
thus P[k] by A3;
thus Result s=(Computation s).k by A1,A3,Def9;
thus thesis by A3;
end;
definition
let A, B be non empty set, y be set such that
A1: y in B;
func id(A, B, y) -> Function of A, [: A, B :] means
for x be Element of A holds it.x=[x,y];
existence
proof
reconsider yy=y as Element of B by A1;
deffunc U(Element of A) = [$1,yy];
consider f being Function of A, [: A,B :] such that
A2: for x being Element of A holds f.x = U(x) from FUNCT_2:sch 4;
take f;
thus thesis by A2;
end;
uniqueness
proof
deffunc U(Element of A) = [$1,y];
thus for f1,f2 being Function of A, [: A, B :] st (for x being Element of
A holds f1.x = U(x)) & (for x being Element of A holds f2.x = U(x)) holds f1 =
f2 from BINOP_2:sch 1;
end;
end;
definition
func Sum_Tran -> Function of [: SegM 5,{0,1} :], [: SegM 5,{0,1},{ -1,0,1 }
:] equals
id([: SegM 5,{0,1} :],{ -1,0,1 }, 0) +* ([0,0] .--> [0,0,1]) +* ([0,1
] .--> [1,0,1]) +* ([1,1] .--> [1,1,1]) +* ([1,0] .--> [2,1,1]) +* ([2,1] .-->
[2,1,1]) +* ([2,0] .--> [3,0,-1]) +* ([3,1] .--> [4,0,-1]) +* ([4,1] .--> [4,1,
-1]) +* ([4,0] .--> [5,0,0]);
coherence
proof
reconsider p0=0, p1=1, p2=2, p3=3, p4=4, p5=5 as Element of SegM 5 by Th1;
set A=[: SegM 5,{0,1} :], B= { -1,0,1 }, C=[: SegM 5,{0,1}, B :];
reconsider b0=0,b1=1 as Element of {0,1} by TARSKI:def 2;
reconsider L=-1 as Element of B by ENUMSET1:def 1;
reconsider h=0,R=1 as Element of {-1,0,1} by ENUMSET1:def 1;
C=[: A, B :] by ZFMISC_1:def 3;
then reconsider OP=id(A,B,h) as Function of A,C;
id(A,B,0) +* ([0,0] .--> [0,0,1]) +* ([0,1] .--> [1,0,1]) +* ([1,1]
.--> [1,1,1]) +* ([1,0] .--> [2,1,1]) +* ([2,1] .--> [2,1,1]) +* ([2,0] .--> [3
,0,-1]) +* ([3,1] .--> [4,0,-1]) +* ([4,1] .--> [4,1,-1]) +* ([4,0] .--> [5,0,0
]) =OP +* ([p0,b0] .--> [p0,b0,R]) +* ([p0,b1] .--> [p1,b0,R]) +* ([p1,b1] .-->
[p1,b1,R]) +* ([p1,b0] .--> [p2,b1,R]) +* ([p2,b1] .--> [p2,b1,R]) +* ([p2,b0]
.--> [p3,b0,L]) +* ([p3,b1] .--> [p4,b0,L]) +* ([p4,b1] .--> [p4,b1,L]) +* ([p4
,b0] .--> [p5,b0,h]);
hence thesis;
end;
end;
theorem Th14:
Sum_Tran.[0,0]=[0,0,1] & Sum_Tran.[0,1]=[1,0,1] & Sum_Tran.[1,1]
=[1,1,1] & Sum_Tran.[1,0]=[2,1,1] & Sum_Tran.[2,1]=[2,1,1] & Sum_Tran.[2,0]=[3,
0,-1] & Sum_Tran.[3,1]=[4,0,-1] & Sum_Tran.[4,1]=[4,1,-1] & Sum_Tran.[4,0]=[5,0
,0]
proof
set x=[0,1];
set x1=[0,0];
set p1=[0,0] .--> [0,0,1], p2=[0,1] .--> [1,0,1], p3=[1,1] .--> [1,1,1], p4=
[1,0] .--> [2,1,1], p5=[2,1] .--> [2,1,1], p6=[2,0] .--> [3,0,-1], p7=[3,1]
.--> [4,0,-1], p8=[4,1] .--> [4,1,-1], f= id([: SegM 5,{0,1} :],{ -1,0,1 },0);
thus Sum_Tran.x1=(f +* p1+* p2+* p3+* p4+* p5+* p6+* p7+* p8).x1 by Th2
.=(f +* p1+* p2+* p3+* p4+* p5+* p6+* p7).x1 by Th2
.=(f +* p1+* p2+* p3+* p4+* p5+* p6).x1 by Th2
.=(f +* p1+* p2+* p3+* p4+* p5).x1 by Th2
.=(f +* p1+* p2+* p3+* p4).x1 by Th2
.=(f +* p1+* p2+* p3).x1 by Th2
.=(f +* p1+* p2).x1 by Th2
.=(f +* p1).x1 by Th3
.=[0,0,1] by FUNCT_7:94;
thus Sum_Tran.x=(f +* p1+* p2+* p3+* p4+* p5+* p6+* p7+* p8).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5+* p6+* p7).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5+* p6).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5).x by Th2
.=(f +* p1+* p2+* p3+* p4).x by Th2
.=(f +* p1+* p2+* p3).x by Th2
.=(f +* p1+* p2).x by Th2
.=[1,0,1] by FUNCT_7:94;
set x=[1,1];
thus Sum_Tran.x=(f +* p1+* p2+* p3+* p4+* p5+* p6+* p7+* p8).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5+* p6+* p7).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5+* p6).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5).x by Th2
.=(f +* p1+* p2+* p3+* p4).x by Th2
.=(f +* p1+* p2+* p3).x by Th3
.=[1,1,1] by FUNCT_7:94;
set x=[1,0];
thus Sum_Tran.x=(f +* p1+* p2+* p3+* p4+* p5+* p6+* p7+* p8).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5+* p6+* p7).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5+* p6).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5).x by Th2
.=(f +* p1+* p2+* p3+* p4).x by Th2
.=[2,1,1] by FUNCT_7:94;
set x=[2,1];
thus Sum_Tran.x=(f +* p1+* p2+* p3+* p4+* p5+* p6+* p7+* p8).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5+* p6+* p7).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5+* p6).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5).x by Th3
.=[2,1,1] by FUNCT_7:94;
set x=[2,0];
thus Sum_Tran.x=(f +* p1+* p2+* p3+* p4+* p5+* p6+* p7+* p8).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5+* p6+* p7).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5+* p6).x by Th2
.=[3,0,-1] by FUNCT_7:94;
set x=[3,1];
thus Sum_Tran.x=(f +* p1+* p2+* p3+* p4+* p5+* p6+* p7+* p8).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5+* p6+* p7).x by Th2
.=[4,0,-1] by FUNCT_7:94;
set x=[4,1];
thus Sum_Tran.x=(f +* p1+* p2+* p3+* p4+* p5+* p6+* p7+* p8).x by Th3
.=[4,1,-1] by FUNCT_7:94;
thus thesis by FUNCT_7:94;
end;
definition
let T be TuringStr, t be Tape of T, i,j be Integer;
pred t is_1_between i,j means
t.i=0 & t.j=0 & for k be Integer st i < k & k < j holds t.k=1;
end;
definition
let f be natural-valued FinSequence, T be TuringStr, t be Tape of T;
pred t storeData f means
for i be Nat st 1 <= i & i < len f
holds t is_1_between Sum Prefix(f,i)+2*(i-1), Sum Prefix(f,i+1)+2*i;
end;
theorem Th15:
for T being TuringStr,t be Tape of T, s,n be Element of NAT st t
storeData <*s,n*> holds t is_1_between s,s+n+2
proof
let T be TuringStr,t be Tape of T,s,n be Element of NAT;
set f=<*s,n*>;
assume
A1: t storeData f;
A2: len f=2 by FINSEQ_1:44;
Sum Prefix(f,1)+2*(1-1)=s & Sum Prefix(f,1+1)+2*1=s+n+2 by Th4;
hence thesis by A1,A2;
end;
theorem Th16:
for T being TuringStr, t be Tape of T, s,n be Element of NAT st
t is_1_between s,s+n+2 holds t storeData <*s,n*>
proof
let T be TuringStr,t be Tape of T,s,n be Element of NAT;
set f=<*s,n*>;
assume
A1: t is_1_between s,s+n+2;
A2: Sum Prefix(f,1+1)+2*1=s+n+2 by Th4;
now
let i be Nat;
assume that
A3: 1 <= i and
A4: i < len f;
len f=2 by FINSEQ_1:44;
then i+1 <= 1+1 by A4,INT_1:7;
then i <= 1 by XREAL_1:6;
then i=1 by A3,XXREAL_0:1;
hence
t is_1_between Sum Prefix(f,i)+2*(i-1),Sum Prefix(f,i+1)+2*i by A1,A2,Th4;
end;
hence thesis;
end;
theorem Th17:
for T being TuringStr, t be Tape of T, s,n be Element of NAT st
t storeData <*s,n *> holds t.s=0 & t.(s+n+2)=0 & for i be Integer st s < i & i
< s+n+2 holds t.i=1
proof
let T be TuringStr, t be Tape of T, s,n be Element of NAT;
assume t storeData <*s,n*>;
then
A1: t is_1_between s,s+n+2 by Th15;
hence t.s=0 & t.(s+n+2)=0;
thus thesis by A1;
end;
theorem Th18:
for T being TuringStr,t be Tape of T,s,n1,n2 be Element of NAT
st t storeData <*s,n1,n2*> holds t is_1_between s,s+n1+2 & t is_1_between s+n1+
2,s+n1+n2+4
proof
let T be TuringStr,t be Tape of T,s,n1,n2 be Element of NAT;
set f=<*s,n1,n2*>;
assume
A1: t storeData f;
A2: len f=3 by FINSEQ_1:45;
Sum Prefix(f,1)+2*(1-1)=s & Sum Prefix(f,1+1)+2*1=s+n1+2 by Th5;
hence t is_1_between s,s+n1+2 by A1,A2;
Sum Prefix(f,2)+2*(2-1)=s+n1+2 & Sum Prefix(f,2+1)+2*2=s+n1+n2+4 by Th5;
hence thesis by A1,A2;
end;
theorem Th19:
for T being TuringStr, t be Tape of T, s,n1,n2 be Element of NAT
st t storeData <*s,n1,n2 *> holds t.s=0 & t.(s+n1+2)=0 & t.(s+n1+n2+4)=0 & (for
i be Integer st s < i & i < s+n1+2 holds t.i=1) & for i be Integer st s+n1+2 <
i & i < s+n1+n2+4 holds t.i=1
proof
let T be TuringStr, t be Tape of T, s,n1,n2 be Element of NAT;
assume t storeData <*s,n1,n2 *>;
then
A1: t is_1_between s,s+n1+2 & t is_1_between s+n1+2,s+n1+n2+4 by Th18;
hence t.s=0 & t.(s+n1+2)=0 & t.(s+n1+n2+4)=0;
thus thesis by A1;
end;
theorem Th20:
for f being FinSequence of NAT,s being Element of NAT st len f
>= 1 holds Sum Prefix(<*s*>^f,1)=s & Sum Prefix(<*s*>^f,2)=s+f/.1
proof
let f be FinSequence of NAT,s be Element of NAT;
set g=<*s*>, h=g^f;
reconsider x1=s as Element of INT by INT_1:def 2;
reconsider x2=f/.1 as Element of INT by INT_1:def 2;
assume
A1: len f >= 1;
then consider n being Nat such that
A2: len f=1+n by NAT_1:10;
A3: len g=1 by FINSEQ_1:39;
then Seg 1=dom g by FINSEQ_1:def 3;
hence Sum Prefix(h,1)=Sum<*x1*> by FINSEQ_1:21
.=s by FINSOP_1:11;
len h=1+len f by A3,FINSEQ_1:22
.=2+n by A2;
then consider p2,q2 being FinSequence of NAT such that
A4: len p2 = 2 and
len q2 = n and
A5: h = p2^q2 by FINSEQ_2:23;
f/.1=f.1 by A1,FINSEQ_4:15
.=h.(1+1) by A1,A3,FINSEQ_7:3;
then
A6: p2.2=f/.1 by A4,A5,FINSEQ_1:64;
Seg 2=dom p2 by A4,FINSEQ_1:def 3;
then
A7: p2 =Prefix(h,2) by A5,FINSEQ_1:21;
h.1=s by FINSEQ_1:41;
then p2.1=s by A4,A5,FINSEQ_1:64;
hence Sum Prefix(h,2)=Sum<*x1,x2*> by A4,A7,A6,FINSEQ_1:44
.=s+f/.1 by RVSUM_1:77;
end;
theorem Th21:
for f being FinSequence of NAT,s being Element of NAT st len f
>= 3 holds Sum Prefix(<*s*>^f,1)=s & Sum Prefix(<*s*>^f,2)=s+f/.1 & Sum Prefix(
<*s*>^f,3)=s+f/.1+f/.2 & Sum Prefix(<*s*>^f,4)=s+f/.1+f/.2+f/.3
proof
let f be FinSequence of NAT,s be Element of NAT;
set g=<*s*>, h=g^f;
reconsider x1=s as Element of INT by INT_1:def 2;
reconsider x2=f/.1 as Element of INT by INT_1:def 2;
reconsider x3=f/.2 as Element of INT by INT_1:def 2;
reconsider x4=f/.3 as Element of INT by INT_1:def 2;
assume
A1: len f >= 3;
then consider n being Nat such that
A2: len f=3+n by NAT_1:10;
reconsider n as Element of NAT by ORDINAL1:def 12;
A3: len g=1 by FINSEQ_1:39;
then
A4: len h=1+len f by FINSEQ_1:22
.=4+n by A2;
then consider p4,q4 being FinSequence of NAT such that
A5: len p4 = 4 and
len q4 = n and
A6: h = p4^q4 by FINSEQ_2:23;
f/.3=f.3 by A1,FINSEQ_4:15
.=h.(1+3) by A1,A3,FINSEQ_7:3;
then
A7: p4.4=f/.3 by A5,A6,FINSEQ_1:64;
Seg 4=dom p4 by A5,FINSEQ_1:def 3;
then
A8: p4 =Prefix(h,4) by A6,FINSEQ_1:21;
A9: 1 <= len f by A1,XXREAL_0:2;
hence Sum Prefix(<*s*>^f,1)=s & Sum Prefix(<*s*>^f,2)=s+f/.1 by Th20;
len h=3+(1+n) by A4;
then consider p3,q3 being FinSequence of NAT such that
A10: len p3 = 3 and
len q3 = 1+n and
A11: h = p3^q3 by FINSEQ_2:23;
A12: f/.1=f.1 by A9,FINSEQ_4:15
.=h.(1+1) by A9,A3,FINSEQ_7:3;
then
A13: p4.2=f/.1 by A5,A6,FINSEQ_1:64;
A14: 2 <= len f by A1,XXREAL_0:2;
then
A15: f/.2=f.2 by FINSEQ_4:15
.=h.(1+2) by A3,A14,FINSEQ_7:3;
then
A16: p4.3=f/.2 by A5,A6,FINSEQ_1:64;
A17: p3.2=f/.1 by A12,A10,A11,FINSEQ_1:64;
Seg 3=dom p3 by A10,FINSEQ_1:def 3;
then
A18: p3 =Prefix(h,3) by A11,FINSEQ_1:21;
A19: p3.3=f/.2 by A15,A10,A11,FINSEQ_1:64;
A20: h.1=s by FINSEQ_1:41;
then p3.1=s by A10,A11,FINSEQ_1:64;
then p3=<*s,f/.1,f/.2*> by A10,A17,A19,FINSEQ_1:45;
hence Sum Prefix(h,3)=s+f/.1+f/.2 by A18,RVSUM_1:78;
p4.1=s by A20,A5,A6,FINSEQ_1:64;
then p4=<*s,f/.1,f/.2,f/.3*> by A5,A13,A16,A7,FINSEQ_4:76;
hence Sum Prefix(h,4)=x1+x2+x3+x4 by A8,RVSUM_1:142
.=s+f/.1+f/.2+f/.3;
end;
theorem Th22:
for T being TuringStr,t be Tape of T, s be Element of NAT, f be
FinSequence of NAT st len f >=1 & t storeData <*s*>^f holds t is_1_between s,s+
f/.1+2
proof
let T be TuringStr,t be Tape of T,s be Element of NAT, f be FinSequence of
NAT;
set g=<*s*>^f;
assume that
A1: len f >=1 and
A2: t storeData g;
len <*s*>=1 by FINSEQ_1:39;
then len g=1+len f by FINSEQ_1:22;
then len g >= 1+1 by A1,XREAL_1:7;
then
A3: 1 < len g by XXREAL_0:2;
Sum Prefix(g,1)+2*(1-1)=s & Sum Prefix(g,1+1)+2*1=s+f/.1+2 by A1,Th20;
hence thesis by A2,A3;
end;
theorem Th23:
for T being TuringStr,t be Tape of T, s be Element of NAT, f be
FinSequence of NAT st len f >=3 & t storeData <*s*>^f holds t is_1_between s,s+
f/.1+2 & t is_1_between s+f/.1+2, s+f/.1+f/.2+4 & t is_1_between s+f/.1+f/.2+4,
s+f/.1+f/.2+f/.3+6
proof
let T be TuringStr,t be Tape of T, s be Element of NAT, f be FinSequence of
NAT;
set g=<*s*>^f;
assume that
A1: len f >=3 and
A2: t storeData g;
thus t is_1_between s,s+f/.1+2 by A1,A2,Th22,XXREAL_0:2;
len <*s*>=1 by FINSEQ_1:39;
then len g=1+len f by FINSEQ_1:22;
then
A3: len g >= 3+1 by A1,XREAL_1:7;
then
A4: 2 < len g by XXREAL_0:2;
Sum Prefix(g,2)+2*(2-1)=s+f/.1+2 & Sum Prefix(g,2+1)+2*2=s+f/.1+f/.2+4
by A1,Th21;
hence t is_1_between s+f/.1+2,s+f/.1+f/.2+4 by A2,A4;
A5: 3 < len g by A3,XXREAL_0:2;
Sum Prefix(g,3)+2*(3-1)=s+f/.1+f/.2+4 & Sum Prefix(g,3+1)+2*3=s+f/.1+f/.
2+f /.3+6 by A1,Th21;
hence thesis by A2,A5;
end;
begin :: Summation of two Nats
definition
func SumTuring -> strict TuringStr means
:Def14:
the Symbols of it = { 0,1 }
& the FStates of it = SegM 5 & the Tran of it = Sum_Tran & the InitS of it
= 0 &
the AcceptS of it = 5;
existence
proof
set St=SegM 5;
reconsider p0=0, qF=5 as Element of St by Th1;
set Sym = { 0,1 };
take TuringStr(# Sym,St, Sum_Tran, p0, qF #);
thus thesis;
end;
uniqueness;
end;
Lm1: for n be Element of NAT st n <= 5 holds n is State of SumTuring
proof
let n be Element of NAT;
assume
A1: n <= 5;
the FStates of SumTuring=SegM 5 by Def14;
hence thesis by A1,Th1;
end;
theorem Th24:
for T be TuringStr,t be Tape of T, h be Integer,s be Symbol of T
st t.h=s holds Tape-Chg(t,h,s) = t
proof
let T be TuringStr,t be Tape of T, h be Integer,s be Symbol of T;
ex f being Function st t = f & dom f = INT & rng f c= the Symbols of T by
FUNCT_2:def 2;
then
A1: h in dom t by INT_1:def 2;
assume t.h=s;
hence thesis by A1,FUNCT_7:96;
end;
Lm2: 0 in the Symbols of SumTuring & 1 in the Symbols of SumTuring
proof
0 in {0,1} & 1 in {0,1} by TARSKI:def 2;
hence thesis by Def14;
end;
theorem Th25:
for T be TuringStr, s be All-State of T, p,h,t be set st s=[p,h,
t] & p <> the AcceptS of T
holds Following s = [(TRAN(s))`1_3, Head(s)+offset
TRAN(s),Tape-Chg(s`3_3,Head(s),(TRAN(s))`2_3)]
by Def6;
Lm3: for s being All-State of SumTuring, p,h,t be set st s=[p,h,t] & p <> 5
holds Following s = [(TRAN(s))`1_3,Head(s)+ offset TRAN(s),
Tape-Chg(s`3_3,Head(s),(TRAN(s))`2_3)]
proof
let s be All-State of SumTuring, p,h,t be set;
assume
A1: s=[p,h,t] & p <> 5;
5=the AcceptS of SumTuring by Def14;
hence thesis by A1,Th25;
end;
theorem Th26:
for T being TuringStr,t be Tape of T, h be Integer, s be Symbol of T,
i be object holds Tape-Chg(t,h,s).h=s &
(i <> h implies Tape-Chg(t,h,s).i=t.i)
proof
let tm be TuringStr,t be Tape of tm,h be Integer, s be Symbol of tm,
i be object;
set t1=Tape-Chg(t,h,s), p=h .--> s;
thus t1.h=s by FUNCT_7:94;
assume i <> h;
then not i in dom p by TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
Lm4: for tm being TuringStr,s be All-State of tm, p be State of tm, h be
Element of INT,t be Tape of tm, m,d be Element of NAT st d=h & 1 is Symbol of
tm & s=[p,h,t] & (the Tran of tm).[p,1]=[p,1,1] & p <> the AcceptS of tm & (for
i be Integer st d <= i & i < d+m holds t.i=1) holds (Computation s).m=[p,d+m,t]
proof
let tm be TuringStr,s be All-State of tm, p be State of tm, h be Element of
INT,t be Tape of tm, m,d be Element of NAT;
assume that
A1: d=h and
A2: 1 is Symbol of tm and
A3: s=[p,h,t] and
A4: (the Tran of tm).[p,1]=[p,1,1] and
A5: p <> the AcceptS of tm and
A6: for i be Integer st d <= i & i < d+m holds t.i=1;
defpred Q[Nat] means
$1 <= m implies (Computation s).$1=[p,d+$1,t];
A7: for k being Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
assume
A8: Q[k];
now
reconsider T=1 as Symbol of tm by A2;
set dk=d+k;
reconsider ik=d+k as Element of INT by INT_1:def 2;
set sk=[p,ik,t];
reconsider tt=sk`3_3 as Tape of tm;
assume
A9: k+1 <= m;
then k < m by NAT_1:13;
then dk < d+m by XREAL_1:8;
then
A10: t.ik=1 by A6,NAT_1:11;
A11: TRAN(sk) =(the Tran of tm).[p,tt.Head(sk)]
.=(the Tran of tm).[p,t.Head(sk)]
.=[p,1,1] by A4,A10;
then
A12: offset TRAN(sk)=1;
A13: Tape-Chg(sk`3_3, Head(sk),(TRAN(sk))`2_3)=Tape-Chg(t,Head(sk), (TRAN(sk
))`2_3)
.=Tape-Chg(t,dk,(TRAN(sk))`2_3)
.=Tape-Chg(t,dk,T) by A11
.=t by A10,Th24;
thus (Computation s).(k+1)=Following sk by A8,A9,Def7,NAT_1:13
.= [(TRAN(sk))`1_3, Head(sk)+ offset TRAN(sk), t] by A5,A13,Th25
.= [p, Head(sk)+ offset TRAN(sk), t] by A11
.= [p, dk+1, t] by A12
.= [p, d+(k+1), t];
end;
hence thesis;
end;
A14: Q[0] by A1,A3,Def7;
for k holds Q[k] from NAT_1:sch 2(A14,A7);
hence thesis;
end;
theorem Th27:
for s being All-State of SumTuring, t be Tape of SumTuring, head
,n1,n2 be Element of NAT st s=[0,head,t] & t storeData <*head,n1,n2 *> holds s
is Accept-Halt & (Result s)`2_3=1+head &
(Result s)`3_3 storeData <*1+head,n1+n2 *>
proof
reconsider F=0 as Symbol of SumTuring by Lm2;
let s be All-State of SumTuring, t be Tape of SumTuring, h,n1,n2 be Element
of NAT;
assume that
A1: s=[0,h,t] and
A2: t storeData <*h,n1,n2 *>;
A3: t.(h+n1+2)=0 by A2,Th19;
set j3=h+n1+n2+4-1;
reconsider h1=h+1 as Element of INT by INT_1:def 2;
A4: h < h1 by XREAL_1:29;
set t1=Tape-Chg(t,h1,F);
A5: h+1+1+n1=h+n1+2;
reconsider p4=4 as State of SumTuring by Lm1;
reconsider m3=j3 as Element of INT by INT_1:def 2;
set j2=j3-1;
reconsider m2=j2 as Element of INT by INT_1:def 2;
set j1=n1+n2+1;
set Rs=(Computation s).(n1+1+(n2+1)+1+1+(1+1)+(j1+1));
reconsider p2=2 as State of SumTuring by Lm1;
reconsider i2=h1+1 as Element of INT by INT_1:def 2;
reconsider nk=h1+1+n1 as Element of INT by INT_1:def 2;
set i3=h+1+1+n1+1;
reconsider n3=i3 as Element of INT by INT_1:def 2;
A6: j2-1=h+j1;
reconsider T=1 as Symbol of SumTuring by Lm2;
set t2=Tape-Chg(t1,nk,T);
A7: h1+1 <= h+1+1+n1 & h1 < h1+1 by NAT_1:11,XREAL_1:29;
set i4=h+n1+n2+4;
reconsider p0=0 as State of SumTuring by Lm1;
set s1= [p0,h1,t];
A8: t.h=0 by A2,Th19;
h <= h+n1 by NAT_1:11;
then
A9: h+2 <= h+n1+2 by XREAL_1:7;
A10: t.(h+n1+n2+4)=0 by A2,Th19;
h <= h+(n1+n2) by NAT_1:11;
then
A11: h+4 <= h+n1+n2+4 by XREAL_1:7;
then
A12: h1 < h+3 & h+4-1 <= j3 by XREAL_1:8,9;
A13: h1 < h+2 by XREAL_1:8;
then
A14: h1 < h+n1+2 by A9,XXREAL_0:2;
A15: t.h=0 by A2,Th19;
A16: t1.h=0 & t1.(h+n1+2)=0 & t1.(h+n1+n2+4)=0 & (for i be Integer st h1 < i
& i < h+1+1+n1 holds t1.i=1) & for i be Integer st h+n1+2 < i & i < h+n1+n2+4
holds t1.i=1
proof
thus t1.h=0 by A15,A4,Th26;
thus t1.(h+n1+2)=0 by A3,A9,A13,Th26;
h1 < h+4 by XREAL_1:8;
hence t1.(h+n1+n2+4)=0 by A10,A11,Th26;
hereby
let i be Integer;
assume that
A17: h1 < i and
A18: i < h+1+1+n1;
A19: h < i by A4,A17,XXREAL_0:2;
thus t1.i=t.i by A17,Th26
.=1 by A2,A5,A18,A19,Th19;
end;
hereby
let i be Integer;
assume that
A20: h+n1+2 < i and
A21: i < h+n1+n2+4;
thus t1.i=t.i by A14,A20,Th26
.=1 by A2,A20,A21,Th19;
end;
end;
A22: for i be Integer st h+1+1 <= i & i < h+1+1+n1 holds t1.i=1
proof
let i be Integer;
assume that
A23: h+1+1 <= i and
A24: i < h+1+1+n1;
h1 < h1+1 by XREAL_1:29;
then h1 < i by A23,XXREAL_0:2;
hence thesis by A16,A24;
end;
set t3=Tape-Chg(t2,j3,F);
A25: t1.h1=0 by Th26;
A26: t2.h1=0 & t2.(h+n1+n2+4)=0 & for i be Integer st h1 < i & i < h+n1+n2+4
holds t2.i=1
proof
thus t2.h1=0 by A25,A7,Th26;
h+n1 <= h+n1+n2 by NAT_1:11;
then
A27: h+1+1+n1 <= h+n1+n2+2 by A5,XREAL_1:7;
h+n1+n2+2 < h+n1+n2+4 by XREAL_1:8;
hence t2.(h+n1+n2+4)=0 by A16,A27,Th26;
hereby
let i be Integer;
assume that
A28: h1 < i and
A29: i < h+n1+n2+4;
per cases by XXREAL_0:1;
suppose
A30: i < h+1+1+n1;
hence t2.i=t1.i by Th26
.=1 by A16,A28,A30;
end;
suppose
i = h+1+1+n1;
hence t2.i=1 by Th26;
end;
suppose
A31: i > h+1+1+n1;
hence t2.i=t1.i by Th26
.=1 by A16,A29,A31;
end;
end;
end;
A32: t3.h1=0 & t3.j3=0 & for i be Integer st h1 < i & i < j3 holds t3.i=1
proof
thus t3.h1=0 by A26,A12,Th26;
thus t3.j3=0 by Th26;
hereby
let i be Integer;
assume that
A33: h1 < i and
A34: i < j3;
A35: i < h+n1+n2+4 by A34,XREAL_1:146,XXREAL_0:2;
thus t3.i=t2.i by A34,Th26
.=1 by A26,A33,A35;
end;
end;
then
A36: t3 is_1_between h1,h1+(n1+n2)+2;
reconsider p3=3 as State of SumTuring by Lm1;
set sm=[p2,n3,t2];
reconsider n4=i4 as Element of INT by INT_1:def 2;
set sp2=[p2,n4,t2];
set sp3=[p3,m3,t2];
reconsider p1=1 as State of SumTuring by Lm1;
set s2=[p1,i2,t1];
set sn=[p1,nk,t1];
reconsider sn3=sn`3_3 as Tape of SumTuring;
A37: TRAN(sn) =Sum_Tran.[sn`1_3, sn3.Head(sn)] by Def14
.=Sum_Tran.[p1,sn3.Head(sn)]
.=Sum_Tran.[p1,t1.Head(sn)]
.=[2,1,1] by A16,Th14;
then
A38: offset TRAN(sn)=1;
reconsider sn3=sp2`3_3 as Tape of SumTuring;
A39: TRAN(sp2) =Sum_Tran.[sp2`1_3, sn3.Head(sp2)] by Def14
.=Sum_Tran.[p2,sn3.Head(sp2)]
.=Sum_Tran.[p2,t2.Head(sp2)]
.=[3,0,-1] by A26,Th14;
then
A40: offset TRAN(sp2)=-1;
Tape-Chg(sp2`3_3, Head(sp2),(TRAN(sp2))`2_3)=Tape-Chg(t2, Head(sp2), (TRAN(
sp2))`2_3)
.=Tape-Chg(t2,i4,(TRAN(sp2))`2_3)
.=Tape-Chg(t2,i4,F) by A39
.=t2 by A26,Th24;
then
A41: Following sp2 = [(TRAN(sp2))`1_3, Head(sp2)+ offset TRAN(sp2), t2] by Lm3
.= [3, Head(sp2)+ offset TRAN(sp2), t2] by A39
.= [3, j3,t2] by A40;
Tape-Chg(sn`3_3, Head(sn),(TRAN(sn))`2_3)=Tape-Chg(t1, Head(sn),(TRAN(sn))
`2_3)
.=Tape-Chg(t1,nk,(TRAN(sn))`2_3)
.=t2 by A37;
then
A42: Following sn = [(TRAN(sn))`1_3, Head(sn)+ offset TRAN(sn), t2] by Lm3
.= [2, Head(sn)+ offset TRAN(sn), t2] by A37
.= sm by A38;
reconsider s3=s`3_3 as Tape of SumTuring;
A43: TRAN(s) =Sum_Tran.[s`1_3, s3.Head(s)] by Def14
.=Sum_Tran.[0,s3.Head(s)] by A1
.=Sum_Tran.[0,t.Head(s)] by A1
.=Sum_Tran.[0,t.h ] by A1
.=[0,0,1] by A2,Th14,Th19;
then
A44: offset TRAN(s)=1;
A45: h1 < h1+1+n1 by A7,XXREAL_0:2;
A46: for i be Integer st i3 <= i & i < i3+(n2+1) holds t2.i=1
proof
let i be Integer;
assume that
A47: i3 <= i and
A48: i < i3+(n2+1);
nk < i3 by XREAL_1:29;
then h1 < i3 by A45,XXREAL_0:2;
then h1 < i by A47,XXREAL_0:2;
hence thesis by A26,A48;
end;
set sp5=[p4, h1, t3];
set sp4=[p4,m2,t3];
defpred R[Nat] means
h+$1 < j2 implies (Computation sp4).$1=[4,j2-$1,t3];
(the Tran of SumTuring).[p2,1] =[p2,1,1] & p2 <> the AcceptS of
SumTuring by Def14,Th14;
then
A49: (Computation sm).(n2+1)=[2,h+n1+n2+4,t2] by A46,Lm4;
h1 < j3 by A12,XXREAL_0:2;
then
A50: t2.j3=1 by A26,XREAL_1:146;
reconsider sn3=sp3`3_3 as Tape of SumTuring;
A51: TRAN(sp3) =Sum_Tran.[sp3`1_3, sn3.Head(sp3)] by Def14
.=Sum_Tran.[p3,sn3.Head(sp3)]
.=Sum_Tran.[p3,t2.Head(sp3)]
.=[4,0,-1] by A50,Th14;
then
A52: offset TRAN(sp3)=-1;
A53: for k being Nat st R[k] holds R[k+1]
proof
let k be Nat;
assume
A54: R[k];
now
reconsider ik=j2-k as Element of INT by INT_1:def 2;
set k3=j2-k;
set sk=[p4,ik,t3];
reconsider tt=sk`3_3 as Tape of SumTuring;
assume
A55: h+(k+1) < j2;
then h1+k < j2+0;
then
A56: h1-0 < j2-k by XREAL_1:21;
reconsider ii=j2-k as Element of NAT by A56,INT_1:3;
j2 <= j2+k by INT_1:6;
then j2 -k <= j2 by XREAL_1:20;
then j2 -k < j3 by XREAL_1:146,XXREAL_0:2;
then
A57: t3.ii=1 by A32,A56;
A58: TRAN(sk) =Sum_Tran.[sk`1_3, tt.Head(sk)] by Def14
.=Sum_Tran.[p4,tt.Head(sk)]
.=Sum_Tran.[p4,t3.Head(sk)]
.=[4,1,-1] by A57,Th14;
then
A59: offset TRAN(sk)=-1;
A60: Tape-Chg(sk`3_3, Head(sk),(TRAN(sk))`2_3)=Tape-Chg(t3,Head(sk), (TRAN(
sk))`2_3)
.=Tape-Chg(t3,k3,(TRAN(sk))`2_3)
.=Tape-Chg(t3,k3,T) by A58
.=t3 by A57,Th24;
h+k < h+k+1 by XREAL_1:29;
hence (Computation sp4).(k+1)=Following sk by A54,A55,Def7,XXREAL_0:2
.= [(TRAN(sk))`1_3, Head(sk)+ offset TRAN(sk), t3] by A60,Lm3
.= [4, Head(sk)+ offset TRAN(sk), t3] by A58
.= [4, j2-k+-1, t3] by A59
.= [4, j2-(k+1), t3];
end;
hence thesis;
end;
A61: R[0] by Def7;
for k being Nat holds R[k] from NAT_1:sch 2(A61,A53);
then
A62: (Computation sp4).j1=[4,j2-j1,t3] by A6,XREAL_1:146
.=sp5;
reconsider s3=s1`3_3 as Tape of SumTuring;
A63: TRAN(s1) =Sum_Tran.[s1`1_3, s3.Head(s1)] by Def14
.=Sum_Tran.[p0,s3.Head(s1)]
.=Sum_Tran.[p0,t.Head(s1)]
.=Sum_Tran.[0,t.h1]
.=[1,0,1] by A2,A4,A14,Th14,Th19;
then
A64: offset TRAN(s1)=1;
Tape-Chg(sp3`3_3, Head(sp3),(TRAN(sp3))`2_3)=Tape-Chg(t2, Head(sp3), (TRAN(
sp3))`2_3)
.=Tape-Chg(t2,j3,(TRAN(sp3))`2_3)
.=t3 by A51;
then
A65: Following sp3 = [(TRAN(sp3))`1_3, Head(sp3)+ offset TRAN(sp3), t3] by Lm3
.= [4, Head(sp3)+ offset TRAN(sp3), t3] by A51
.= sp4 by A52;
A66: now
reconsider tt=sp5`3_3 as Tape of SumTuring;
A67: TRAN(sp5) =Sum_Tran.[sp5`1_3, tt.Head(sp5)] by Def14
.=Sum_Tran.[4,tt.Head(sp5)]
.=Sum_Tran.[4,t3.Head(sp5)]
.=[5,0,0] by A32,Th14;
then
A68: offset TRAN(sp5)=0;
Tape-Chg(sp5`3_3, Head(sp5),(TRAN(sp5))`2_3) =Tape-Chg(t3, Head(sp5),(
TRAN(sp5))`2_3)
.=Tape-Chg(t3,h1,(TRAN(sp5))`2_3)
.=Tape-Chg(t3,h1,F) by A67
.=t3 by A32,Th24;
hence Following sp5 = [(TRAN(sp5))`1_3, Head(sp5)+ offset TRAN(sp5), t3]
by Lm3
.= [5, Head(sp5)+ offset TRAN(sp5), t3] by A67
.= [5, h1+ 0, t3] by A68;
end;
Tape-Chg(s1`3_3, Head(s1),(TRAN(s1))`2_3)=Tape-Chg(t, Head(s1),(TRAN(s1))`2_3
)
.=Tape-Chg(t,h1,(TRAN(s1))`2_3)
.=t1 by A63;
then
A69: Following s1 = [(TRAN(s1))`1_3, Head(s1)+ offset TRAN(s1), t1] by Lm3
.= [1, Head(s1)+ offset TRAN(s1), t1] by A63
.= s2 by A64;
Tape-Chg(s`3_3, Head(s),(TRAN(s))`2_3)=Tape-Chg(t, Head(s),(TRAN(s))`2_3)
by A1
.=Tape-Chg(t,h,(TRAN(s))`2_3) by A1
.=Tape-Chg(t,h,F) by A43
.=t by A8,Th24;
then
A70: Following s = [(TRAN(s))`1_3, Head(s)+offset TRAN(s),t] by A1,Lm3
.= [0, Head(s)+ offset TRAN(s),t] by A43
.= s1 by A1,A44;
(Computation s).(1+1)= Following (Computation s).1 by Def7
.=s2 by A70,A69,Th9;
then (Computation s).(n1+1+(n2+1)+1+1+(1+1)) = (Computation s2).(n1+1+(n2+1
)+1+1) by Th10;
then (Computation s).(n1+1+(n2+1)+1+1+(1+1)) = Following (Computation s2).(
n1+1+(n2+1)+1) by Def7
.= Following Following (Computation s2).(n1+1+(n2+1)) by Def7
.= Following Following (Computation (Computation s2).(n1+1)).(n2+1) by Th10
;
then
A71: Rs=(Computation Following Following (Computation (Computation s2).(n1+
1)).(n2+1)).(j1+1) by Th10
.=(Computation Following Following (Computation Following (Computation
s2).n1).(n2+1)).(j1+1) by Def7;
(the Tran of SumTuring).[p1,1] =[p1,1,1] & p1 <> the AcceptS of
SumTuring by Def14,Th14;
then Rs=(Computation Following sp3).(j1+1) by A22,A42,A49,A41,A71,Lm4;
then
A72: Rs=[5, h1, t3] by A65,A62,A66,Def7;
then
A73: Rs`1_3 = 5
.=the AcceptS of SumTuring by Def14;
hence s is Accept-Halt;
then
A74: Result s =Rs by A73,Def9;
hence (Result s)`2_3= 1+h by A72;
(Result s)`3_3= t3 by A72,A74;
hence thesis by A36,Th16;
end;
definition
let T be TuringStr,F be Function;
pred T computes F means
for s being All-State of T,t being Tape of T
, a being Element of NAT, x being FinSequence of NAT st x in dom F & s=[the
InitS of T,a,t] & t storeData <*a*>^x holds s is Accept-Halt & ex b, y being
Element of NAT st (Result s)`2_3=b & y=F.x &
(Result s)`3_3 storeData <*b*>^<* y *>;
end;
theorem Th28:
dom [+] c= 2-tuples_on NAT
proof
arity (1 proj 1)=1;
then dom [+] c= (1+1)-tuples_on NAT by COMPUT_1:56;
hence thesis;
end;
theorem
SumTuring computes [+]
proof
now
let s be All-State of SumTuring,t be Tape of SumTuring, h1 be Element of
NAT, x be FinSequence of NAT;
assume that
A1: x in dom [+] and
A2: s=[the InitS of SumTuring,h1,t] and
A3: t storeData <*h1*>^x;
x is Tuple of 2,NAT by A1,Th28,FINSEQ_2:131;
then consider i,j being Element of NAT such that
A4: x = <*i,j*> by FINSEQ_2:100;
A5: s = [0,h1,t] by A2,Def14;
A6: <*h1*>^x=<*h1,i,j*> by A4,FINSEQ_1:43;
hence s is Accept-Halt by A3,A5,Th27;
take h2=1+h1;
take y=i+j;
t storeData <*h1,i,j *> by A3,A4,FINSEQ_1:43;
hence (Result s)`2_3=h2 by A5,Th27;
thus y=[+].x by A4,COMPUT_1:85;
(Result s)`3_3 storeData <*1+h1,i+j *> by A3,A5,A6,Th27;
hence (Result s)`3_3 storeData <*h2*>^<* y *>;
end;
hence thesis;
end;
begin :: Computing successor function(i.e. s(x)=x+1)
definition
func Succ_Tran -> Function of [: SegM 4,{0,1} :], [: SegM 4,{0,1},{ -1,0,1 }
:] equals
id([: SegM 4,{0,1} :],{ -1,0,1 }, 0) +* ([0,0] .--> [1,0,1]) +* ([1,1
] .--> [1,1,1]) +* ([1,0] .--> [2,1,1]) +* ([2,0] .--> [3,0,-1]) +* ([2,1] .-->
[3,0,-1]) +* ([3,1] .--> [3,1,-1]) +* ([3,0] .--> [4,0,0]);
coherence
proof
reconsider p0=0, p1=1, p2=2, p3=3, p4=4 as Element of SegM 4 by Th1;
set A=[: SegM 4,{0,1} :], B= { -1,0,1 }, C=[: SegM 4,{0,1}, B :];
reconsider b0=0, b1=1 as Element of {0,1} by TARSKI:def 2;
reconsider L=-1 as Element of B by ENUMSET1:def 1;
reconsider h=0, R=1 as Element of {-1,0,1} by ENUMSET1:def 1;
C=[: A, B :] by ZFMISC_1:def 3;
then reconsider OP=id(A,B,h) as Function of A,C;
id(A,B,0) +* ([0,0] .--> [1,0,1]) +* ([1,1] .--> [1,1,1]) +* ([1,0]
.--> [2,1,1]) +* ([2,0] .--> [3,0,-1]) +* ([2,1] .--> [3,0,-1]) +* ([3,1] .-->
[3,1,-1]) +* ([3,0] .--> [4,0,0]) =OP +* ([p0,b0] .--> [p1,b0,R]) +* ([p1,b1]
.--> [p1,b1,R]) +* ([p1,b0] .--> [p2,b1,R]) +* ([p2,b0] .--> [p3,b0,L]) +* ([p2
,b1] .--> [p3,b0,L]) +* ([p3,b1] .--> [p3,b1,L]) +* ([p3,b0] .--> [p4,b0,h]);
hence thesis;
end;
end;
theorem Th30:
Succ_Tran.[0,0]=[1,0,1] & Succ_Tran.[1,1]=[1,1,1] & Succ_Tran.[1
,0]=[2,1,1] & Succ_Tran.[2,0]=[3,0,-1] & Succ_Tran.[2,1]=[3,0,-1] & Succ_Tran.[
3,1]=[3,1,-1] & Succ_Tran.[3,0]=[4,0,0]
proof
set x=[1,1];
set x1=[0,0];
set p1=[0,0] .--> [1,0,1], p2=[1,1] .--> [1,1,1], p3=[1,0] .--> [2,1,1], p4=
[2,0] .--> [3,0,-1], p5=[2,1] .--> [3,0,-1], p6=[3,1] .--> [3,1,-1], f= id([:
SegM 4,{0,1} :],{ -1,0,1 },0);
thus Succ_Tran.x1=(f +* p1+* p2+* p3+* p4+* p5+* p6).x1 by Th2
.=(f +* p1+* p2+* p3+* p4+* p5).x1 by Th2
.=(f +* p1+* p2+* p3+* p4).x1 by Th2
.=(f +* p1+* p2+* p3).x1 by Th2
.=(f +* p1+* p2).x1 by Th2
.=(f +* p1).x1 by Th3
.=[1,0,1] by FUNCT_7:94;
thus Succ_Tran.x=(f +* p1+* p2+* p3+* p4+* p5+* p6).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5).x by Th2
.=(f +* p1+* p2+* p3+* p4).x by Th2
.=(f +* p1+* p2+* p3).x by Th2
.=(f +* p1+* p2).x by Th3
.=[1,1,1] by FUNCT_7:94;
set x=[1,0];
thus Succ_Tran.x=(f +* p1+* p2+* p3+* p4+* p5+* p6).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5).x by Th2
.=(f +* p1+* p2+* p3+* p4).x by Th2
.=(f +* p1+* p2+* p3).x by Th2
.=[2,1,1] by FUNCT_7:94;
set x=[2,0];
thus Succ_Tran.x=(f +* p1+* p2+* p3+* p4+* p5+* p6).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5).x by Th2
.=(f +* p1+* p2+* p3+* p4).x by Th3
.=[3,0,-1] by FUNCT_7:94;
set x=[2,1];
thus Succ_Tran.x=(f +* p1+* p2+* p3+* p4+* p5+* p6).x by Th2
.=(f +* p1+* p2+* p3+* p4+* p5).x by Th2
.=[3,0,-1] by FUNCT_7:94;
set x=[3,1];
thus Succ_Tran.x=(f +* p1+* p2+* p3+* p4+* p5+* p6).x by Th3
.=[3,1,-1] by FUNCT_7:94;
thus thesis by FUNCT_7:94;
end;
definition
func SuccTuring -> strict TuringStr means
:Def17:
the Symbols of it = { 0,1
} & the FStates of it = SegM 4 & the Tran of it = Succ_Tran & the InitS of
it =
0 & the AcceptS of it = 4;
existence
proof
set St=SegM 4;
reconsider p0=0, qF=4 as Element of St by Th1;
set Sym = { 0,1 };
take TuringStr(# Sym,St, Succ_Tran, p0, qF #);
thus thesis;
end;
uniqueness;
end;
Lm5: for n be Element of NAT st n <= 4 holds n is State of SuccTuring
proof
let n be Element of NAT;
assume
A1: n <= 4;
the FStates of SuccTuring=SegM 4 by Def17;
hence thesis by A1,Th1;
end;
Lm6: 0 in the Symbols of SuccTuring & 1 in the Symbols of SuccTuring
proof
0 in {0,1} & 1 in {0,1} by TARSKI:def 2;
hence thesis by Def17;
end;
Lm7: for s being All-State of SuccTuring, p,h,t be set st s=[p,h,t] & p <> 4
holds Following s =
[(TRAN(s))`1_3, Head(s)+ offset TRAN(s), Tape-Chg(s`3_3, Head(s
),(TRAN(s))`2_3)]
proof
let s be All-State of SuccTuring, p,h,t be set;
assume
A1: s=[p,h,t] & p <> 4;
4=the AcceptS of SuccTuring by Def17;
hence thesis by A1,Th25;
end;
theorem Th31:
for s being All-State of SuccTuring, t be Tape of SuccTuring,
head,n be Element of NAT st s=[0,head,t] & t storeData <*head,n*> holds s is
Accept-Halt & (Result s)`2_3=head & (Result s)`3_3 storeData <*head,n+1*>
proof
reconsider F=0 as Symbol of SuccTuring by Lm6;
let s be All-State of SuccTuring,t be Tape of SuccTuring, h,n be Element of
NAT;
assume that
A1: s=[0,h,t] and
A2: t storeData <*h,n *>;
A3: t.h=0 by A2,Th17;
set i3=h+1+1+n+1;
reconsider h1=h+1 as Element of INT by INT_1:def 2;
reconsider p1=1 as State of SuccTuring by Lm5;
A4: h1+1+n < i3 by XREAL_1:29;
h <= h+n by NAT_1:11;
then
A5: h+2 <= h+n+2 by XREAL_1:7;
A6: h1 < h+2 by XREAL_1:8;
then
A7: h1 < h+n+2 by A5,XXREAL_0:2;
reconsider p2=2 as State of SuccTuring by Lm5;
reconsider i2=h1+1 as Element of INT by INT_1:def 2;
reconsider nk=h1+1+n as Element of INT by INT_1:def 2;
reconsider hh=h as Element of INT by INT_1:def 2;
reconsider n3=i3 as Element of INT by INT_1:def 2;
reconsider T=1 as Symbol of SuccTuring by Lm6;
set t1=Tape-Chg(t,h1,T);
A8: h < h1 by XREAL_1:29;
A9: t.(h+n+2)=0 by A2,Th17;
A10: t1.h=0 & t1.(h+n+2)=0 & for i be Integer st h < i & i < h+n+2 holds t1.
i=1
proof
thus t1.h=0 by A3,A8,Th26;
thus t1.(h+n+2)=0 by A9,A5,A6,Th26;
hereby
let i be Integer;
assume
A11: h < i & i < h+n+2;
per cases;
suppose
h1=i;
hence t1.i=1 by Th26;
end;
suppose
h1<>i;
hence t1.i=t.i by Th26
.=1 by A2,A11,Th17;
end;
end;
end;
A12: for i be Integer st h+1+1 <= i & i < h+1+1+n holds t1.i=1
proof
let i be Integer;
assume that
A13: h+1+1 <= i and
A14: i < h+1+1+n;
h1 < h1+1 by XREAL_1:29;
then h1 < i by A13,XXREAL_0:2;
then h < i by A8,XXREAL_0:2;
hence thesis by A10,A14;
end;
reconsider s3=s`3_3 as Tape of SuccTuring;
A15: TRAN(s) =Succ_Tran.[s`1_3, s3.Head(s)] by Def17
.=Succ_Tran.[0,s3.Head(s)] by A1
.=Succ_Tran.[0,t.Head(s)] by A1
.=[1,0,1] by A1,A3,Th30;
then
A16: offset TRAN(s)=1;
set s1= [p1,h1,t];
reconsider s3=s1`3_3 as Tape of SuccTuring;
Tape-Chg(s`3_3, Head(s),(TRAN(s))`2_3)=Tape-Chg(t, Head(s),(TRAN(s))`2_3)
by A1
.=Tape-Chg(t,h,(TRAN(s))`2_3) by A1
.=Tape-Chg(t,h,F) by A15
.=t by A3,Th24;
then
A17: Following s = [(TRAN(s))`1_3, Head(s)+offset TRAN(s),t] by A1,Lm7
.= [1, Head(s)+ offset TRAN(s),t] by A15
.= s1 by A1,A16;
A18: TRAN(s1) =Succ_Tran.[s1`1_3, s3.Head(s1)] by Def17
.=Succ_Tran.[p1,s3.Head(s1)]
.=Succ_Tran.[p1,t.Head(s1)]
.=Succ_Tran.[1,t.h1]
.=[1,1,1] by A2,A8,A7,Th17,Th30;
then
A19: offset TRAN(s1)=1;
reconsider p1=1 as State of SuccTuring by Lm5;
set s2=[p1,i2,t1];
Tape-Chg(s1`3_3, Head(s1),(TRAN(s1))`2_3)=Tape-Chg(t, Head(s1),(TRAN(s1))`2_3
)
.=Tape-Chg(t,h1,(TRAN(s1))`2_3)
.=t1 by A18;
then
A20: Following s1 = [(TRAN(s1))`1_3,Head(s1)+ offset TRAN(s1),t1] by Lm7
.= [1,Head(s1)+ offset TRAN(s1),t1] by A18
.= s2 by A19;
reconsider p3=3 as State of SuccTuring by Lm5;
set sn=[p1,nk,t1];
set t2=Tape-Chg(t1,nk,T);
set t3=Tape-Chg(t2,n3,F);
(the Tran of SuccTuring).[p1,1] =[p1,1,1] & p1 <> the AcceptS of
SuccTuring by Def17,Th30;
then
A21: (Computation s2).n=[p1,h+1+1+n,t1] by A12,Lm4;
h1+1 <= h+1+1+n & h1 < h1+1 by NAT_1:11,XREAL_1:29;
then
A22: h1 < h1+1+n by XXREAL_0:2;
A23: t2.h=0 & for i be Integer st h < i & i <= h+n+2 holds t2.i=1
proof
thus t2.h=0 by A8,A10,A22,Th26;
hereby
let i be Integer;
assume that
A24: h < i and
A25: i <= h+n+2;
per cases;
suppose
A26: i <> h+n+2;
then
A27: i < h+n+2 by A25,XXREAL_0:1;
thus t2.i=t1.i by A26,Th26
.=1 by A10,A24,A27;
end;
suppose
i = h+n+2;
hence t2.i=1 by Th26;
end;
end;
end;
set sp3=[p3,nk,t3];
set sm=[p2,n3,t2];
reconsider sm3=sm`3_3 as Tape of SuccTuring;
A28: the Symbols of SuccTuring = {0,1} by Def17;
A29: now
per cases by A28,TARSKI:def 2;
suppose
t2.n3=1;
hence Succ_Tran.[2,t2.n3 ]=[p3,0,-1] by Th30;
end;
suppose
t2.n3=0;
hence Succ_Tran.[2,t2.n3 ]=[p3,0,-1] by Th30;
end;
end;
A30: TRAN(sm) =Succ_Tran.[sm`1_3, sm3.Head(sm)] by Def17
.=Succ_Tran.[2,sm3.Head(sm)]
.=Succ_Tran.[2,t2.Head(sm)]
.=[p3,0,-1] by A29;
then
A31: offset TRAN(sm)=-1;
set j1=1+1+n, sp5=[p3,hh, t3];
defpred R[Nat] means
h+$1 <= nk implies (Computation sp3).$1=[3,
nk-$1,t3];
reconsider sn3=sn`3_3 as Tape of SuccTuring;
A32: h+j1 =nk;
set Rs=(Computation s).(1+1+(n+1+1+(j1+1)));
A33: TRAN(sn) =Succ_Tran.[sn`1_3, sn3.Head(sn)] by Def17
.=Succ_Tran.[p1,sn3.Head(sn)]
.=Succ_Tran.[p1,t1.Head(sn)]
.=[2,1,1] by A10,Th30;
then
A34: offset TRAN(sn)=1;
A35: h < h1+1+n by A8,A22,XXREAL_0:2;
A36: t3.h=0 & t3.(h+(n+1)+2)=0 & for k be Integer st h < k & k < h+(n+1)+2
holds t3.k=1
proof
thus t3.h=0 by A35,A23,A4,Th26;
thus t3.(h+(n+1)+2)=0 by Th26;
hereby
let i be Integer;
assume that
A37: h < i and
A38: i < h+(n+1)+2;
i+1 <= h+(n+1)+2 by A38,INT_1:7;
then
A39: i <= h+(n+1)+2-1 by XREAL_1:19;
thus t3.i=t2.i by A38,Th26
.=1 by A23,A37,A39;
end;
end;
then
A40: t3 is_1_between h,h+(n+1)+2;
Tape-Chg(sm`3_3, Head(sm),(TRAN(sm))`2_3) =Tape-Chg(t2, Head(sm),(TRAN(sm))
`2_3)
.=Tape-Chg(t2,n3,(TRAN(sm))`2_3)
.=t3 by A30;
then
A41: Following sm = [(TRAN(sm))`1_3, Head(sm)+ offset TRAN(sm), t3] by Lm7
.= [p3,Head(sm)+ offset TRAN(sm),t3] by A30
.= sp3 by A31;
Tape-Chg(sn`3_3,Head(sn),(TRAN(sn))`2_3)=Tape-Chg(t1, Head(sn),(TRAN(sn))`2_3
)
.=Tape-Chg(t1,nk,(TRAN(sn))`2_3)
.=t2 by A33;
then
A42: Following sn = [(TRAN(sn))`1_3, Head(sn)+ offset TRAN(sn), t2] by Lm7
.= [2, Head(sn)+ offset TRAN(sn), t2] by A33
.= sm by A34;
A43: for k being Nat st R[k] holds R[k+1]
proof
let k be Nat;
assume
A44: R[k];
now
reconsider ik=nk-k as Element of INT by INT_1:def 2;
set k3=nk-k;
A45: h+k < h+k+1 by XREAL_1:29;
set sk=[p3,ik,t3];
reconsider tt=sk`3_3 as Tape of SuccTuring;
nk <= nk+k by INT_1:6;
then
A46: nk -k <= nk by XREAL_1:20;
assume
A47: h+(k+1) <= nk;
then h+k < nk+0 by A45,XXREAL_0:2;
then
A48: h-0 < nk-k by XREAL_1:21;
reconsider ii=nk-k as Element of NAT by A48,INT_1:3;
h+n+2 < h+n+2+1 by XREAL_1:29;
then ii < h+(n+1)+2 by A46,XXREAL_0:2;
then
A49: t3.ii=1 by A36,A48;
A50: TRAN(sk) =Succ_Tran.[sk`1_3, tt.Head(sk)] by Def17
.=Succ_Tran.[p3,tt.Head(sk)]
.=Succ_Tran.[p3,t3.Head(sk)]
.=[3,1,-1] by A49,Th30;
then
A51: offset TRAN(sk)=-1;
A52: Tape-Chg(sk`3_3, Head(sk),(TRAN(sk))`2_3)=Tape-Chg(t3,Head(sk), (TRAN(
sk))`2_3)
.=Tape-Chg(t3,k3,(TRAN(sk))`2_3)
.=Tape-Chg(t3,k3,T) by A50
.=t3 by A49,Th24;
hereby
thus (Computation sp3).(k+1)=Following sk by A44,A47,A45,Def7,
XXREAL_0:2
.= [(TRAN(sk))`1_3, Head(sk)+ offset TRAN(sk), t3] by A52,Lm7
.= [3, Head(sk)+ offset TRAN(sk), t3] by A50
.= [3, nk-k+-1, t3] by A51
.= [3, nk-(k+1), t3];
end;
end;
hence thesis;
end;
A53: R[0] by Def7;
for k being Nat holds R[k] from NAT_1:sch 2(A53,A43);
then
A54: (Computation sp3).j1=[3,nk-j1,t3] by A32
.=sp5;
A55: now
reconsider tt=sp5`3_3 as Tape of SuccTuring;
A56: TRAN(sp5) =Succ_Tran.[sp5`1_3, tt.Head(sp5)] by Def17
.=Succ_Tran.[3,tt.Head(sp5)]
.=Succ_Tran.[3,t3.Head(sp5)]
.=[4,0,0] by A36,Th30;
then
A57: offset TRAN(sp5)=0;
Tape-Chg(sp5`3_3, Head(sp5),(TRAN(sp5))`2_3) =Tape-Chg(t3, Head(sp5),(
TRAN(sp5))`2_3)
.=Tape-Chg(t3,h,(TRAN(sp5))`2_3)
.=Tape-Chg(t3,h,F) by A56
.=t3 by A36,Th24;
hence Following sp5 = [(TRAN(sp5))`1_3, Head(sp5)+ offset TRAN(sp5), t3]
by Lm7
.= [4, Head(sp5)+ offset TRAN(sp5), t3] by A56
.= [4, h+ 0, t3] by A57;
end;
Rs=(Computation (Computation s).(1+1)).(n+1+1+(j1+1)) by Th10
.=(Computation Following (Computation s).1).(n+1+1+(j1+1)) by Def7
.=(Computation Following s1).(n+1+1+(j1+1)) by A17,Th9
.=(Computation (Computation s2).(n+1+1)).(j1+1) by A20,Th10
.=(Computation Following (Computation s2).(n+1)).(j1+1) by Def7;
then Rs=(Computation sp3).(j1+1) by A21,A42,A41,Def7;
then
A58: Rs=[4, h, t3] by A54,A55,Def7;
then
A59: Rs`1_3 = 4
.=the AcceptS of SuccTuring by Def17;
hence s is Accept-Halt;
then
A60: Result s =Rs by A59,Def9;
hence (Result s)`2_3= h by A58;
(Result s)`3_3= t3 by A58,A60;
hence thesis by A40,Th16;
end;
theorem
SuccTuring computes 1 succ 1
proof
now
set sc=1 succ 1;
let s be All-State of SuccTuring,t be Tape of SuccTuring, h be Element of
NAT, x be FinSequence of NAT;
assume that
A1: x in dom sc and
A2: s=[the InitS of SuccTuring,h,t] and
A3: t storeData <*h*>^x;
A4: s = [0,h,t] by A2,Def17;
A5: dom sc = 1-tuples_on NAT by COMPUT_1:def 7;
then x is Tuple of 1,NAT by A1,FINSEQ_2:131;
then consider i being Element of NAT such that
A6: x = <*i*> by FINSEQ_2:97;
A7: <*h*>^x=<*h,i*> by A6;
hence s is Accept-Halt by A3,A4,Th31;
take h2=h;
take y=i+1;
thus (Result s)`2_3=h2 by A3,A4,A7,Th31;
dom <*i*> = {1} by FINSEQ_1:def 8,FINSEQ_1:2;
then 1 in dom <*i*> by TARSKI:def 1;
then
A8: x/.1 = x.1 by A6,PARTFUN1:def 6;
thus y=(x/.1)+1 by A6,FINSEQ_4:16
.=sc.x by A1,A5,A8,COMPUT_1:def 7;
(Result s)`3_3 storeData <*h2,i+1 *> by A3,A4,A7,Th31;
hence (Result s)`3_3 storeData <*h2*>^<* y *>;
end;
hence thesis;
end;
begin :: Computing zero function (i.e. O(x)=0)
definition
func Zero_Tran -> Function of [:SegM 4,{0,1}:], [:SegM 4,{0,1},{ -1,0,1 }:]
equals
id([: SegM 4,{0,1} :],{ -1,0,1 }, 1) +* ([0,0] .--> [1,0,1]) +* ([1,1
] .--> [2,1,1]) +* ([2,0] .--> [3,0,-1]) +* ([2,1] .--> [3,0,-1]) +* ([3,1]
.--> [4,1,-1]);
coherence
proof
reconsider p0=0, p1=1, p2=2, p3=3, p4=4 as Element of SegM 4 by Th1;
set A=[: SegM 4,{0,1} :], B= { -1,0,1 }, C=[: SegM 4,{0,1}, B :];
reconsider b0=0,b1=1 as Element of {0,1} by TARSKI:def 2;
reconsider L=-1 as Element of B by ENUMSET1:def 1;
reconsider R=1 as Element of {-1,0,1} by ENUMSET1:def 1;
C=[: A, B :] by ZFMISC_1:def 3;
then reconsider OP=id(A,B,R) as Function of A,C;
id(A,B,1) +* ([0,0] .--> [1,0,1]) +* ([1,1] .--> [2,1,1]) +* ([2,0]
.--> [3,0,-1]) +* ([2,1] .--> [3,0,-1]) +* ([3,1] .--> [4,1,-1]) =OP +* ([p0,b0
] .--> [p1,b0,R]) +* ([p1,b1] .--> [p2,b1,R]) +* ([p2,b0] .--> [p3,b0,L]) +* ([
p2,b1] .--> [p3,b0,L]) +* ([p3,b1] .--> [p4,b1,L]);
hence thesis;
end;
end;
theorem Th33:
Zero_Tran.[0,0]=[1,0,1] & Zero_Tran.[1,1]=[2,1,1] & Zero_Tran.[2
,0]=[3,0,-1] & Zero_Tran.[2,1]=[3,0,-1] & Zero_Tran.[3,1]=[4,1,-1]
proof
set x=[1,1];
set x1=[0,0];
set p1=[0,0] .--> [1,0,1], p2=[1,1] .--> [2,1,1], p3=[2,0] .--> [3,0,-1], p4
=[2,1] .--> [3,0,-1], f= id([: SegM 4,{0,1} :],{ -1,0,1 },1);
thus Zero_Tran.x1=(f +* p1+* p2+* p3+* p4).x1 by Th2
.=(f +* p1+* p2+* p3).x1 by Th2
.=(f +* p1+* p2).x1 by Th2
.=(f +* p1).x1 by Th3
.=[1,0,1] by FUNCT_7:94;
thus Zero_Tran.x=(f +* p1+* p2+* p3+* p4).x by Th2
.=(f +* p1+* p2+* p3).x by Th2
.=(f +* p1+* p2).x by Th3
.=[2,1,1] by FUNCT_7:94;
set x=[2,0];
thus Zero_Tran.x=(f +* p1+* p2+* p3+* p4).x by Th3
.=(f +* p1+* p2+* p3).x by Th3
.=[3,0,-1] by FUNCT_7:94;
set x=[2,1];
thus Zero_Tran.x=(f +* p1+* p2+* p3+* p4).x by Th2
.=[3,0,-1] by FUNCT_7:94;
thus thesis by FUNCT_7:94;
end;
definition
func ZeroTuring -> strict TuringStr means
:Def19:
the Symbols of it = { 0,1
} & the FStates of it = SegM 4 & the Tran of it = Zero_Tran & the InitS of
it =
0 & the AcceptS of it = 4;
existence
proof
set St=SegM 4;
reconsider qF=4 as Element of St by Th1;
reconsider p0=0 as Element of St by Th1;
set Sym = { 0,1 };
take TuringStr(# Sym,St, Zero_Tran, p0, qF #);
thus thesis;
end;
uniqueness;
end;
Lm8: for n be Element of NAT st n <= 4 holds n is State of ZeroTuring
proof
let n be Element of NAT;
assume
A1: n <= 4;
the FStates of ZeroTuring=SegM 4 by Def19;
hence thesis by A1,Th1;
end;
Lm9: 0 in the Symbols of ZeroTuring & 1 in the Symbols of ZeroTuring
proof
0 in {0,1} & 1 in {0,1} by TARSKI:def 2;
hence thesis by Def19;
end;
Lm10: for s being All-State of ZeroTuring, p,h,t be set st s=[p,h,t] & p <> 4
holds Following s =
[(TRAN(s))`1_3, Head(s)+ offset TRAN(s), Tape-Chg(s`3_3, Head(s
),(TRAN(s))`2_3)]
proof
let s be All-State of ZeroTuring, p,h,t be set;
assume
A1: s=[p,h,t] & p <> 4;
4=the AcceptS of ZeroTuring by Def19;
hence thesis by A1,Th25;
end;
theorem Th34:
for s being All-State of ZeroTuring, t be Tape of ZeroTuring,
head be Element of NAT, f be FinSequence of NAT st len f >= 1 & s=[0,head,t] &
t storeData <*head*>^f holds s is Accept-Halt &
(Result s)`2_3=head & (Result s)
`3_3 storeData <*head,0*>
proof
reconsider F=0 as Symbol of ZeroTuring by Lm9;
let s be All-State of ZeroTuring, t be Tape of ZeroTuring, h be Element of
NAT, f be FinSequence of NAT;
assume that
A1: len f >= 1 and
A2: s=[0,h,t] and
A3: t storeData <*h*>^f;
reconsider s3=s`3_3 as Tape of ZeroTuring;
reconsider h1=h+1 as Element of INT by INT_1:def 2;
set m=f/.1, n=h+f/.1+2;
A4: h < h1 by XREAL_1:29;
reconsider p1=1 as State of ZeroTuring by Lm8;
set s1= [p1,h1,t];
reconsider i2=h1+1 as Element of INT by INT_1:def 2;
A5: h1 < i2 by XREAL_1:29;
reconsider T=1 as Symbol of ZeroTuring by Lm9;
set t1=Tape-Chg(t,h1,T);
set t2=Tape-Chg(t1,i2,F);
set t3=Tape-Chg(t2,h1,T);
A6: t is_1_between h,n by A1,A3,Th22;
then
A7: t.h=0;
then t1.h=0 by A4,Th26;
then t2.h=0 by A4,A5,Th26;
then
A8: t3.h=0 by A4,Th26;
A9: TRAN(s) =Zero_Tran.[s`1_3, s3.Head(s)] by Def19
.=Zero_Tran.[0,s3.Head(s)] by A2
.=Zero_Tran.[0,t.Head(s)] by A2
.=[1,0,1] by A2,A7,Th33;
then
A10: offset TRAN(s)=1;
set Rs=(Computation s).(1+1+1+1);
reconsider p3=3 as State of ZeroTuring by Lm8;
A11: h+1+1=h+0+2;
A12: t3.(h+1)=1 by Th26;
A13: now
let k be Integer;
assume h < k & k < h+0+2;
then h+1 <= k & k <= h+1 by A11,INT_1:7;
hence t3.k=1 by A12,XXREAL_0:1;
end;
t1.(h+1)=1 by Th26;
then
A14: t2.(h+1)=1 by A5,Th26;
set s3=[p3,h1,t2];
reconsider s33=s3`3_3 as Tape of ZeroTuring;
A15: TRAN(s3) =Zero_Tran.[s3`1_3, s33.Head(s3)] by Def19
.=Zero_Tran.[p3,s33.Head(s3)]
.=Zero_Tran.[p3,t2.Head(s3)]
.=[4,1,-1] by A14,Th33;
then
A16: offset TRAN(s3)=-1;
reconsider p2=2 as State of ZeroTuring by Lm8;
reconsider s13=s1`3_3 as Tape of ZeroTuring;
h <= h+m by NAT_1:11;
then
A17: h+2 <= h+m+2 by XREAL_1:7;
h1 < h+2 by XREAL_1:8;
then
A18: h1 < n by A17,XXREAL_0:2;
A19: TRAN(s1) =Zero_Tran.[s1`1_3, s13.Head(s1)] by Def19
.=Zero_Tran.[p1,s13.Head(s1)]
.=Zero_Tran.[p1,t.Head(s1)]
.=Zero_Tran.[1,t.h1]
.=[2,1,1] by A6,A4,A18,Th33;
then
A20: offset TRAN(s1)=1;
A21: now
A22: the Symbols of ZeroTuring = {0,1} by Def19;
per cases by A22,TARSKI:def 2;
suppose
t1.i2=1;
hence Zero_Tran.[2,t1.i2 ]=[3,0,-1] by Th33;
end;
suppose
t1.i2=0;
hence Zero_Tran.[2,t1.i2 ]=[3,0,-1] by Th33;
end;
end;
set s2=[p2,i2,t1];
reconsider s23=s2`3_3 as Tape of ZeroTuring;
A23: TRAN(s2) =Zero_Tran.[s2`1_3, s23.Head(s2)] by Def19
.=Zero_Tran.[p2,s23.Head(s2)]
.=Zero_Tran.[p2,t1.Head(s2)]
.=[3,0,-1] by A21;
then
A24: offset TRAN(s2)=-1;
Tape-Chg(s2`3_3, Head(s2),(TRAN(s2))`2_3) =Tape-Chg(t1, Head(s2),(TRAN(s2))
`2_3)
.=Tape-Chg(t1,i2,(TRAN(s2))`2_3)
.=t2 by A23;
then
A25: Following s2 = [(TRAN(s2))`1_3, Head(s2)+ offset TRAN(s2), t2] by Lm10
.= [3, Head(s2)+ offset TRAN(s2), t2] by A23
.= s3 by A24;
reconsider p3=3 as State of ZeroTuring by Lm8;
A26: Tape-Chg(s3`3_3, Head(s3),(TRAN(s3))`2_3) =
Tape-Chg(t2, Head(s3),(TRAN(s3))
`2_3)
.=Tape-Chg(t2,h1,(TRAN(s3))`2_3)
.=t3 by A15;
set s3=[p3,h1,t2];
A27: Following s3 = [(TRAN(s3))`1_3, Head(s3)+ offset TRAN(s3), t3] by A26,Lm10
.= [4, Head(s3)+ offset TRAN(s3), t3] by A15
.= [4, h,t3] by A16;
Tape-Chg(s`3_3, Head(s),(TRAN(s))`2_3)=
Tape-Chg(t, Head(s),(TRAN(s))`2_3) by A2
.=Tape-Chg(t,h,(TRAN(s))`2_3) by A2
.=Tape-Chg(t,h,F) by A9
.=t by A7,Th24;
then
A28: Following s = [(TRAN(s))`1_3, Head(s)+offset TRAN(s),t] by A2,Lm10
.= [1, Head(s)+ offset TRAN(s),t] by A9
.= s1 by A2,A10;
Tape-Chg(s1`3_3,Head(s1),(TRAN(s1))`2_3) =Tape-Chg(t,Head(s1),(TRAN(s1))`2_3)
.=Tape-Chg(t,h1,(TRAN(s1))`2_3)
.=t1 by A19;
then
A29: Following s1 = [(TRAN(s1))`1_3, Head(s1)+ offset TRAN(s1), t1] by Lm10
.= [2, Head(s1)+ offset TRAN(s1), t1] by A19
.= s2 by A20;
A30: Rs= Following (Computation s).(1+1+1) by Def7
.= Following Following (Computation s).(1+1) by Def7
.= Following Following Following (Computation s).1 by Def7
.=[4, h,t3] by A28,A29,A25,A27,Th9;
then
A31: Rs`1_3 = 4
.=the AcceptS of ZeroTuring by Def19;
hence s is Accept-Halt;
then
A32: Result s =Rs by A31,Def9;
hence (Result s)`2_3= h by A30;
A33: (Result s)`3_3= t3 by A30,A32;
t2.i2=0 by Th26;
then t3.i2=0 by A5,Th26;
then t3 is_1_between h,h+0+2 by A8,A13;
hence thesis by A33,Th16;
end;
theorem
n >=1 implies ZeroTuring computes n const 0
proof
assume
A1: n>=1;
now
set cs=n const 0;
let s be All-State of ZeroTuring,t be Tape of ZeroTuring, h be Element of
NAT, x be FinSequence of NAT;
assume that
A2: x in dom cs and
A3: s=[the InitS of ZeroTuring,h,t] and
A4: t storeData <*h*>^x;
x in n-tuples_on NAT by A2;
then x in { f where f is Element of NAT*: len f = n } by FINSEQ_2:def 4;
then
A6: ex f be Element of NAT* st x = f & len f = n;
A7: s = [0,h,t] by A3,Def19;
hence s is Accept-Halt by A1,A4,A6,Th34;
take h2=h;
take y=0;
thus (Result s)`2_3=h2 by A1,A4,A6,A7,Th34;
thus y=cs.x by A2,FUNCOP_1:7;
(Result s)`3_3 storeData <*h2,0*> by A1,A4,A6,A7,Th34;
hence (Result s)`3_3 storeData <*h2*>^<*y*>;
end;
hence thesis;
end;
begin :: Computing n-ary project function(i.e. U(x1,x2,...,xn)=x3)
definition
func U3(n)Tran -> Function of [: SegM 3,{0,1} :], [: SegM 3,{0,1},{ -1,0,1 }
:] equals
id([: SegM 3,{0,1} :],{ -1,0,1 }, 0) +* ([0,0] .--> [1,0,1]) +* ([1,1
] .--> [1,0,1]) +* ([1,0] .--> [2,0,1]) +* ([2,1] .--> [2,0,1]) +* ([2,0] .-->
[3,0,0]);
coherence
proof
reconsider p0=0, p1=1, p2=2, p3=3 as Element of SegM 3 by Th1;
set A=[: SegM 3,{0,1} :], B= { -1,0,1 }, C=[: SegM 3,{0,1}, B :];
reconsider b0=0, b1=1 as Element of {0,1} by TARSKI:def 2;
reconsider h=0, R=1 as Element of B by ENUMSET1:def 1;
C=[: A, B :] by ZFMISC_1:def 3;
then reconsider OP=id(A,B,h) as Function of A,C;
id(A,B,0) +* ([0,0] .--> [1,0,1]) +* ([1,1] .--> [1,0,1]) +* ([1,0]
.--> [2,0,1]) +* ([2,1] .--> [2,0,1]) +* ([2,0] .--> [3,0,0]) =OP +* ([p0,b0]
.--> [p1,b0,R]) +* ([p1,b1] .--> [p1,b0,R]) +* ([p1,b0] .--> [p2,b0,R]) +* ([p2
,b1] .--> [p2,b0,R]) +* ([p2,b0] .--> [p3,b0,h]);
hence thesis;
end;
end;
theorem Th36:
U3(n)Tran.[0,0]=[1,0,1] & U3(n)Tran.[1,1]=[1,0,1] & U3(n)Tran.[1
,0]=[2,0,1] & U3(n)Tran.[2,1]=[2,0,1] & U3(n)Tran.[2,0]=[3,0,0]
proof
set x=[1,1];
set x1=[0,0];
set p1=[0,0] .--> [1,0,1], p2=[1,1] .--> [1,0,1], p3=[1,0] .--> [2,0,1], p4=
[2,1] .--> [2,0,1], f= id([: SegM 3,{0,1} :],{ -1,0,1 },0);
thus U3(n)Tran.x1=(f +* p1+* p2+* p3+* p4).x1 by Th2
.=(f +* p1+* p2+* p3).x1 by Th2
.=(f +* p1+* p2).x1 by Th2
.=(f +* p1).x1 by Th3
.=[1,0,1] by FUNCT_7:94;
thus U3(n)Tran.x=(f +* p1+* p2+* p3+* p4).x by Th2
.=(f +* p1+* p2+* p3).x by Th2
.=(f +* p1+* p2).x by Th3
.=[1,0,1] by FUNCT_7:94;
set x=[1,0];
thus U3(n)Tran.x=(f +* p1+* p2+* p3+* p4).x by Th2
.=(f +* p1+* p2+* p3).x by Th3
.=[2,0,1] by FUNCT_7:94;
set x=[2,1];
thus U3(n)Tran.x=(f +* p1+* p2+* p3+* p4).x by Th3
.=[2,0,1] by FUNCT_7:94;
thus thesis by FUNCT_7:94;
end;
definition
func U3(n)Turing -> strict TuringStr means
:Def21:
the Symbols of it = { 0,1
} & the FStates of it = SegM 3 & the Tran of it = U3(n)Tran & the InitS of
it =
0 & the AcceptS of it = 3;
existence
proof
set St=SegM 3;
reconsider qF=3 as Element of St by Th1;
reconsider p0=0 as Element of St by Th1;
set Sym = { 0,1 };
take TuringStr(# Sym,St, U3(n)Tran, p0, qF #);
thus thesis;
end;
uniqueness;
end;
Lm11: for n be Element of NAT st n <= 3 holds n is State of U3(n)Turing
proof
let n be Element of NAT;
assume
A1: n <= 3;
the FStates of U3(n)Turing=SegM 3 by Def21;
hence thesis by A1,Th1;
end;
Lm12: 0 in the Symbols of U3(n)Turing & 1 in the Symbols of U3(n)Turing
proof
0 in {0,1} & 1 in {0,1} by TARSKI:def 2;
hence thesis by Def21;
end;
Lm13: for s being All-State of U3(n)Turing, p,h,t be set st s=[p,h,t] & p <> 3
holds Following s =
[(TRAN(s))`1_3, Head(s)+ offset TRAN(s),Tape-Chg(s`3_3,Head(s),
(TRAN(s))`2_3)]
proof
let s be All-State of U3(n)Turing, p,h,t be set;
assume
A1: s=[p,h,t] & p <> 3;
3=the AcceptS of U3(n)Turing by Def21;
hence thesis by A1,Th25;
end;
Lm14: for tm being TuringStr,s be All-State of tm, p be State of tm, h be
Element of INT,t be Tape of tm, m,d be Element of NAT st d=h & 0 is Symbol of
tm & s=[p,h,t] & (the Tran of tm).[p,1]=[p,0,1] & p <> the AcceptS of tm & (for
i be Integer st d <= i & i < d+m holds t.i=1) holds ex t1 being Tape of tm st (
Computation s).m=[p,d+m,t1] & (for i be Integer st d <= i & i < d+m holds t1.i=
0) & for i be Integer st d > i or i >= d+m holds t1.i=t.i
proof
let tm be TuringStr,s be All-State of tm, p be State of tm, h be Element of
INT,t be Tape of tm, m,d be Element of NAT;
assume that
A1: d=h and
A2: 0 is Symbol of tm and
A3: s=[p,h,t] and
A4: (the Tran of tm).[p,1]=[p,0,1] and
A5: p <> the AcceptS of tm and
A6: for i be Integer st d <= i & i < d+m holds t.i=1;
defpred Q[Nat] means
$1 <= m implies ex t1 being Tape of tm st (
Computation s).$1=[p,d+$1,t1] & (for i be Integer st d <= i & i < d+$1 holds t1
.i=0) & (for i be Integer st d > i or i >= d+$1 holds t1.i=t.i);
A7: for k being Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
assume
A8: Q[k];
now
reconsider F=0 as Symbol of tm by A2;
set dk=d+k;
reconsider ik=d+k as Element of INT by INT_1:def 2;
assume
A9: k+1 <= m;
then consider t1 being Tape of tm such that
A10: (Computation s).k=[p,d+k,t1] and
A11: for i be Integer st d <= i & i < d+k holds t1.i=0 and
A12: for i be Integer st d > i or i >= d+k holds t1.i=t.i by A8,NAT_1:13;
k < m by A9,NAT_1:13;
then
A13: dk < d+m by XREAL_1:8;
A14: t1.ik=t.ik by A12
.=1 by A6,A13,NAT_1:11;
take t2=Tape-Chg(t1,dk,F);
set sk=[p,ik,t1];
reconsider tt=sk`3_3 as Tape of tm;
A15: TRAN(sk) =(the Tran of tm).[p,tt.Head(sk)]
.=(the Tran of tm).[p,t1.Head(sk)]
.=[p,0,1] by A4,A14;
then
A16: offset TRAN(sk)=1;
A17: Tape-Chg(sk`3_3, Head(sk),(TRAN(sk))`2_3) =Tape-Chg(t1,Head(sk),(TRAN(
sk))`2_3)
.=Tape-Chg(t1,dk,(TRAN(sk))`2_3)
.=t2 by A15;
thus (Computation s).(k+1)=Following sk by A10,Def7
.= [(TRAN(sk))`1_3, Head(sk)+ offset TRAN(sk),t2] by A5,A17,Th25
.= [p, Head(sk)+ offset TRAN(sk),t2] by A15
.= [p, dk+1, t2] by A16
.= [p, d+(k+1),t2];
hereby
let i be Integer;
assume that
A18: d <= i and
A19: i < d+(k+1);
per cases;
suppose
i=dk;
hence t2.i=0 by Th26;
end;
suppose
A20: i <> dk;
i < d+k+1 by A19;
then i <= d+k by INT_1:7;
then
A21: i < dk by A20,XXREAL_0:1;
thus t2.i=t1.i by A20,Th26
.=0 by A11,A18,A21;
end;
end;
hereby
let i be Integer;
assume
A22: d > i or i >= d+(k+1);
per cases by A22;
suppose
A23: d > i;
d <= d+k by NAT_1:12;
hence t2.i=t1.i by A23,Th26
.=t.i by A12,A23;
end;
suppose
A24: i >= d+(k+1);
k < k+1 by NAT_1:13;
then
A25: d+k < d+(k+1) by XREAL_1:8;
then
A26: i > d+k by A24,XXREAL_0:2;
thus t2.i=t1.i by A24,A25,Th26
.=t.i by A12,A26;
end;
end;
end;
hence thesis;
end;
A27: Q[0]
proof
assume 0 <= m;
take t1=t;
thus (Computation s).0=[p,d+0,t1] by A1,A3,Def7;
thus for i be Integer st d <= i & i < d+0 holds t1.i=0;
thus thesis;
end;
for k holds Q[k] from NAT_1:sch 2(A27,A7);
hence thesis;
end;
theorem Th37:
for s being All-State of U3(n)Turing, t be Tape of U3(n)Turing,
head be Element of NAT, f be FinSequence of NAT st len f >= 3 & s=[0,head,t] &
t storeData <*head*>^f holds s is Accept-Halt &
(Result s)`2_3=head+f/.1+f/.2+4 &
(Result s)`3_3 storeData <*head+f/.1+f/.2+4,f/.3*>
proof
reconsider F=0 as Symbol of U3(n)Turing by Lm12;
let s be All-State of U3(n)Turing, t be Tape of U3(n)Turing, h be Element of
NAT, f be FinSequence of NAT;
assume that
A1: len f >= 3 and
A2: s=[0,h,t] and
A3: t storeData <*h*>^f;
set n1=h+ f/.1+2, n2=h+f/.1+f/.2+4, n3=h+f/.1+f/.2+f/.3+6;
reconsider s03=s`3_3 as Tape of U3(n)Turing;
A4: t is_1_between h,n1 by A1,A3,Th23;
then
A5: t.h=0;
A6: TRAN(s) =U3(n)Tran.[s`1_3, s03.Head(s)] by Def21
.=U3(n)Tran.[0,s03.Head(s)] by A2
.=U3(n)Tran.[0,t.Head(s)] by A2
.=[1,0,1] by A2,A5,Th36;
then
A7: offset TRAN(s)=1;
reconsider p1=1 as State of U3(n)Turing by Lm11;
set m1=f/.1+1;
reconsider h1=h+1 as Element of INT by INT_1:def 2;
set s1= [p1,h1,t];
A8: t is_1_between n1,n2 by A1,A3,Th23;
then
A9: t.n2=0;
Tape-Chg(s`3_3, Head(s),(TRAN(s))`2_3)=
Tape-Chg(t, Head(s),(TRAN(s))`2_3) by A2
.=Tape-Chg(t,h,(TRAN(s))`2_3) by A2
.=Tape-Chg(t,h,F) by A6
.=t by A5,Th24;
then
A10: Following s = [(TRAN(s))`1_3, Head(s)+offset TRAN(s),t] by A2,Lm13
.= [1, Head(s)+ offset TRAN(s),t] by A6
.= s1 by A2,A7;
A11: t is_1_between n2,n3 by A1,A3,Th23;
then
A12: t.n3=0;
reconsider p2=2 as State of U3(n)Turing by Lm11;
set s2=(Computation s1).m1;
reconsider s23=s2`3_3 as Tape of U3(n)Turing;
set j1=h+1+m1+1;
reconsider k1=j1 as Element of INT by INT_1:def 2;
set m2=f/.2+1;
set Rs=(Computation s).(m2+1+1+m1+1);
set m3=n2+f/.3+2;
A13: now
let i be Integer;
assume that
A14: h+1 <= i and
A15: i < h+1+m1;
h < h+1 by XREAL_1:29;
then h < i by A14,XXREAL_0:2;
hence t.i=1 by A4,A15;
end;
(the Tran of U3(n)Turing).[p1,1] =[p1,0,1] & p1 <> the AcceptS of
U3(n)Turing by Def21,Th36;
then consider t1 being Tape of U3(n)Turing such that
A16: s2=[p1,h+1+m1,t1] and
for i be Integer st h+1 <= i & i < h+1+m1 holds t1.i=0 and
A17: for i be Integer st h+1 > i or i >= h+1+m1 holds t1.i=t.i by A13,Lm12,Lm14
;
t.n1=0 by A4;
then
A18: t1.(h+1+m1)=0 by A17;
A19: TRAN(s2) =U3(n)Tran.[s2`1_3, s23.Head(s2)] by Def21
.=U3(n)Tran.[p1,s23.Head(s2)] by A16
.=U3(n)Tran.[1,t1.Head(s2)] by A16
.=[2,0,1] by A16,A18,Th36;
then
A20: offset TRAN(s2)=1;
set s3= [p2,k1,t1];
Tape-Chg(s2`3_3, Head(s2),(TRAN(s2))`2_3) =Tape-Chg(t1, Head(s2),(TRAN(s2))
`2_3) by A16
.=Tape-Chg(t1,h+1+m1,(TRAN(s2))`2_3) by A16
.=Tape-Chg(t1,h+1+m1,F) by A19
.=t1 by A18,Th24;
then
A21: Following s2 = [(TRAN(s2))`1_3, Head(s2)+offset TRAN(s2),t1] by A16,Lm13
.= [2, Head(s2)+ offset TRAN(s2),t1] by A19
.= s3 by A16,A20;
A22: now
let i be Integer;
assume that
A23: j1 <= i and
A24: i < j1+m2;
h+1+m1 < j1 by XREAL_1:29;
then
A25: h+1+m1 < i by A23,XXREAL_0:2;
hence t1.i=t.i by A17
.=1 by A8,A24,A25;
end;
set s4=(Computation s3).m2;
reconsider s43=s4`3_3 as Tape of U3(n)Turing;
(the Tran of U3(n)Turing).[p2,1] =[p2,0,1] & p2 <> the AcceptS of
U3(n)Turing by Def21,Th36;
then consider t2 being Tape of U3(n)Turing such that
A26: s4=[p2,j1+m2,t2] and
for i be Integer st j1 <= i & i < j1 + m2 holds t2.i=0 and
A27: for i be Integer st j1 > i or i >= j1 + m2 holds t2.i=t1.i by A22,Lm12
,Lm14;
2 <= f/.2+4 by NAT_1:12;
then
A28: n1 <= h+f/.1+(f/.2+4) by XREAL_1:7;
A29: now
let k be Integer;
assume that
A30: n2 < k and
A31: k < m3;
A32: n1 <= k by A28,A30,XXREAL_0:2;
thus t2.k=t1.k by A27,A30
.=t.k by A17,A32
.=1 by A11,A30,A31;
end;
A33: t2.(j1+m2)=t1.(j1+m2) by A27
.=0 by A9,A17,A28;
A34: TRAN(s4) =U3(n)Tran.[s4`1_3, s43.Head(s4)] by Def21
.=U3(n)Tran.[p2,s43.Head(s4)] by A26
.=U3(n)Tran.[2,t2.Head(s4)] by A26
.=[3,0,0] by A26,A33,Th36;
then
A35: offset TRAN(s4)=0;
Tape-Chg(s4`3_3, Head(s4),(TRAN(s4))`2_3) =Tape-Chg(t2, Head(s4),(TRAN(s4))
`2_3) by A26
.=Tape-Chg(t2,j1+m2,(TRAN(s4))`2_3) by A26
.=Tape-Chg(t2,j1+m2,F) by A34
.=t2 by A33,Th24;
then
A36: Following s4 = [(TRAN(s4))`1_3, Head(s4)+offset TRAN(s4),t2] by A26,Lm13
.= [3, Head(s4)+ offset TRAN(s4),t2] by A34
.= [3, j1+m2+0,t2] by A26,A35;
Rs=(Computation (Computation s).1).(m2+1+1+m1) by Th10
.=(Computation s1).(m2+1+1+m1) by A10,Th9
.=(Computation s2).(m2+1+1) by Th10;
then
A37: Rs=(Computation (Computation s2).1).(m2+1)by Th10
.=(Computation s3).(m2+1) by A21,Th9
.=[3, j1+m2,t2] by A36,Def7;
then
A38: Rs`1_3 = 3
.=the AcceptS of U3(n)Turing by Def21;
hence s is Accept-Halt;
then
A39: Result s =Rs by A38,Def9;
hence (Result s)`2_3=n2 by A37;
A40: (Result s)`3_3= t2 by A37,A39;
A41: n2 <= n2+(f/.3+2) by NAT_1:11;
then
A42: n1 <= m3 by A28,XXREAL_0:2;
t2.m3=t1.m3 by A27,A41
.=0 by A12,A17,A42;
then t2 is_1_between n2,n2+f/.3+2 by A33,A29;
hence thesis by A40,Th16;
end;
theorem
n >= 3 implies U3(n)Turing computes n proj 3
proof
assume
A1: n >= 3;
now
set pj=n proj 3;
let s be All-State of U3(n)Turing,t be Tape of U3(n)Turing, h be Element
of NAT, x be FinSequence of NAT;
assume that
A2: x in dom pj and
A3: s=[the InitS of U3(n)Turing,h,t] and
A4: t storeData <*h*>^x;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
set pj=nn proj 3;
arity pj = n;
then
A5: dom pj c= n-tuples_on NAT by COMPUT_1:21;
then x in n-tuples_on NAT by A2;
then x in { f where f is Element of NAT*: len f = n } by FINSEQ_2:def 4;
then
A6: ex f be Element of NAT* st x = f & len f = n;
A7: s = [0,h,t] by A3,Def21;
hence s is Accept-Halt by A1,A4,A6,Th37;
take h2=h+x/.1+x/.2+4;
take y=x/.3;
thus (Result s)`2_3=h2 by A1,A4,A6,A7,Th37;
thus y=x.3 by A1,A6,FINSEQ_4:15
.=pj.x by A2,A5,COMPUT_1:38
.=(n proj 3).x;
(Result s)`3_3 storeData <*h2,y*> by A1,A4,A6,A7,Th37;
hence (Result s)`3_3 storeData <*h2*>^<*y*>;
end;
hence thesis;
end;
begin :: Combining two Turing Machines into one Turing Machine
definition
let t1,t2 be TuringStr;
func UnionSt(t1,t2) -> finite non empty set equals
[: the FStates of t1, {the
InitS of t2} :] \/ [: {the AcceptS of t1}, the FStates of t2 :];
correctness;
end;
theorem Th39:
for t1,t2 being TuringStr holds [ the InitS of t1, the InitS of
t2 ] in UnionSt(t1,t2) & [ the AcceptS of t1,the AcceptS of t2 ] in UnionSt(t1,
t2)
proof
let t1,t2 be TuringStr;
set p0=the InitS of t1, q0=the InitS of t2, p1=the AcceptS of t1, q1=the
AcceptS of t2, A= [: the FStates of t1, { q0 } :],
B= [: {p1}, the FStates
of t2
:];
reconsider q=q0 as Element of { q0 } by TARSKI:def 1;
reconsider p=p1 as Element of { p1 } by TARSKI:def 1;
[ p0, q ] in A;
hence [ p0, q0 ] in UnionSt(t1,t2) by XBOOLE_0:def 3;
[ p, q1 ] in B;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th40:
for s,t being TuringStr, x be State of s holds [ x, the InitS of
t ] in UnionSt(s,t)
proof
let s,t be TuringStr,x be State of s;
set q0=the InitS of t, A= [: the FStates of s, { q0 } :];
reconsider q=q0 as Element of { q0 } by TARSKI:def 1;
[ x, q ] in A;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th41:
for s,t being TuringStr, x be State of t holds [ the AcceptS of
s, x] in UnionSt(s,t)
proof
let s,t be TuringStr,x be State of t;
set p1=the AcceptS of s, B= [:{p1},the FStates of t :];
reconsider p=p1 as Element of { p1 } by TARSKI:def 1;
[ p, x] in B;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th42:
for s,t being TuringStr, x be Element of UnionSt(s,t) holds ex
x1 be State of s, x2 be State of t st x=[x1, x2]
proof
let s,t be TuringStr,x be Element of UnionSt(s,t);
set q0=the InitS of t, p1=the AcceptS of s,
A= [: the FStates of s, { q0 } :]
, B= [: { p1 }, the FStates of t :];
per cases by XBOOLE_0:def 3;
suppose
x in A;
then consider x1 being State of s, x2 be Element of { q0 } such that
A1: x= [x1, x2] by DOMAIN_1:1;
take x1,q0;
thus thesis by A1,TARSKI:def 1;
end;
suppose
x in B;
then consider x1 being Element of { p1 }, x2 being State of t such that
A2: x= [x1, x2] by DOMAIN_1:1;
take p1,x2;
thus thesis by A2,TARSKI:def 1;
end;
end;
definition
let s,t be TuringStr, x be Tran-Goal of s;
func FirstTuringTran(s,t,x) -> Element of [: UnionSt(s,t),(the Symbols of s)
\/ the Symbols of t,{-1,0,1} :] equals
[[x`1_3,the InitS of t], x`2_3, x`3_3];
coherence
proof
reconsider y1=[x`1_3,the InitS of t] as Element of UnionSt(s,t) by Th40;
set Sym=(the Symbols of s) \/ the Symbols of t;
reconsider y2=x`2_3 as Element of Sym by XBOOLE_0:def 3;
[y1, y2, x`3_3] in [: UnionSt(s,t),Sym,{-1,0,1} :];
hence thesis;
end;
end;
definition
let s,t be TuringStr, x be Tran-Goal of t;
func SecondTuringTran(s,t,x) -> Element of [: UnionSt(s,t),(the Symbols of s
) \/ the Symbols of t,{-1,0,1} :] equals
[[the AcceptS of s,x`1_3], x`2_3, x`3_3];
coherence
proof
reconsider y1=[the AcceptS of s,x`1_3] as Element of UnionSt(s,t) by Th41;
set Sym=(the Symbols of s) \/ the Symbols of t;
reconsider y2=x`2_3 as Element of Sym by XBOOLE_0:def 3;
[y1, y2, x`3_3] in [: UnionSt(s,t),Sym,{-1,0,1} :];
hence thesis;
end;
end;
definition
let s,t be TuringStr;
let x be Element of UnionSt(s,t);
redefine func x`1 -> State of s; :: redefines `1 (XTUPLE_0, definition)
coherence
proof
consider x1 being State of s, x2 be State of t such that
A1: x=[x1, x2] by Th42;
thus thesis by A1;
end;
redefine func x`2 -> State of t; :: redefines `2 (XTUPLE_0, definition)
coherence
proof
consider x1 being State of s, x2 be State of t such that
A2: x=[x1, x2] by Th42;
thus thesis by A2;
end;
end;
definition
let s,t be TuringStr, x be Element of [: UnionSt(s,t), (the Symbols of s) \/
the Symbols of t :];
func FirstTuringState x -> State of s equals
x`1`1;
correctness;
func SecondTuringState x -> State of t equals
x`1`2;
correctness;
end;
definition
let X,Y,Z be non empty set, x be Element of [: X, Y \/ Z :];
given u being set,y be Element of Y such that
A1: x = [u,y];
func FirstTuringSymbol(x) -> Element of Y equals
:Def27:
x`2;
coherence by A1;
end;
definition
let X,Y,Z be non empty set, x be Element of [: X, Y \/ Z :];
given u being set,z be Element of Z such that
A1: x = [u, z];
func SecondTuringSymbol(x) -> Element of Z equals
:Def28:
x`2;
coherence by A1;
end;
definition
let s,t be TuringStr, x be Element of [: UnionSt(s,t), (the Symbols of s) \/
the Symbols of t :];
func Uniontran(s,t,x) -> Element of [: UnionSt(s,t), (the Symbols of s) \/
the Symbols of t,{-1,0,1} :] equals
:Def29:
FirstTuringTran(s,t,(the Tran of s)
.[FirstTuringState x, FirstTuringSymbol(x)]) if ex p being State of s,y be
Symbol of s st x = [ [p,the InitS of t],y] & p <> the AcceptS of s,
SecondTuringTran(s,t,(the Tran of t). [SecondTuringState x,SecondTuringSymbol(x
)]) if ex q being State of t, y be Symbol of t st x = [ [the AcceptS of s,q],y]
otherwise [x`1,x`2,-1];
consistency
proof
let w be Element of [: UnionSt(s,t), (the Symbols of s) \/ the Symbols of
t,{-1,0,1} :];
thus (ex p be State of s,y be Symbol of s st x = [ [p,the InitS of t],y] &
p <> the AcceptS of s) & (ex q being State of t, y be Symbol of t st x = [ [the
AcceptS of s,q],y] ) implies ( w=FirstTuringTran(s,t,(the Tran of s). [
FirstTuringState x,FirstTuringSymbol(x)]) iff w=SecondTuringTran(s,t,(the Tran
of t). [SecondTuringState x,SecondTuringSymbol(x)]))
proof
given p be State of s,y be Symbol of s such that
A1: x = [ [p,the InitS of t],y] and
A2: p <> the AcceptS of s;
given q be State of t, z be Symbol of t such that
A3: x = [ [the AcceptS of s,q],z];
[p,the InitS of t]=[the AcceptS of s,q] by A1,A3,XTUPLE_0:1;
hence thesis by A2,XTUPLE_0:1;
end;
end;
coherence
proof
reconsider l=-1 as Element of { -1,0,1 } by ENUMSET1:def 1;
[x`1,x`2,l] in [: UnionSt(s,t), (the Symbols of s) \/ the Symbols of t
,{-1,0,1} :];
hence thesis;
end;
end;
definition
let s,t be TuringStr;
func UnionTran(s,t) -> Function of [: UnionSt(s,t), (the Symbols of s) \/
the Symbols of t :], [: UnionSt(s,t), (the Symbols of s) \/ the Symbols of t,{-
1,0,1} :] means
:Def30:
for x being Element of [: UnionSt(s,t), (the Symbols of
s) \/ the Symbols of t :] holds it.x = Uniontran(s,t,x);
existence
proof
set Sm=(the Symbols of s) \/ the Symbols of t, X=[: UnionSt(s,t),Sm :];
deffunc U(Element of X) = Uniontran(s,t,$1);
consider f being Function of X, [: UnionSt(s,t),Sm,{-1,0,1} :] such that
A1: for x being Element of X holds f.x = U(x) from FUNCT_2:sch 4;
take f;
thus thesis by A1;
end;
uniqueness
proof
set Sm=(the Symbols of s) \/ the Symbols of t, X=[: UnionSt(s,t), Sm :];
let f,g be Function of X,[: UnionSt(s,t),Sm,{-1,0,1} :] such that
A2: for x being Element of X holds f.x = Uniontran(s,t,x) and
A3: for x being Element of X holds g.x = Uniontran(s,t,x);
now
let x be Element of X;
thus f.x =Uniontran(s,t,x) by A2
.=g.x by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let T1,T2 be TuringStr;
func T1 ';' T2 -> strict TuringStr means
:Def31:
the Symbols of it = (the Symbols of T1) \/ the Symbols of T2 &
the FStates of it = UnionSt(T1,T2) & the
Tran of it = UnionTran(T1,T2) & the InitS of it = [the InitS of T1,the InitS of
T2] & the AcceptS of it = [the AcceptS of T1,the AcceptS of T2];
existence
proof
set St =UnionSt(T1,T2);
reconsider q1=[the AcceptS of T1,the AcceptS of T2] as Element of St by
Th39;
reconsider p0=[the InitS of T1,the InitS of T2] as Element of St by Th39;
set Sym=(the Symbols of T1) \/ the Symbols of T2;
take TuringStr(# Sym,St, UnionTran(T1,T2), p0, q1 #);
thus thesis;
end;
uniqueness;
end;
theorem Th43:
for T1,T2 being TuringStr, g be Tran-Goal of T1,p be State of T1
, y be Symbol of T1 st p <> the AcceptS of T1 & g = (the Tran of T1).[p, y]
holds (the Tran of T1 ';' T2).[ [p,the InitS of T2],y]
= [[g`1_3,the InitS of T2]
, g`2_3, g`3_3]
proof
let t1,t2 be TuringStr, g be Tran-Goal of t1,p be State of t1, y be Symbol
of t1;
assume that
A1: p <> the AcceptS of t1 and
A2: g = (the Tran of t1).[p, y];
set q0=the InitS of t2;
set x=[[p,q0],y];
q0 in { q0 } by TARSKI:def 1;
then [p,q0] in [: the FStates of t1, {q0} :] by ZFMISC_1:def 2;
then
A3: [p,q0] in [: the FStates of t1, {q0} :] \/ [: {the AcceptS of t1}, the
FStates of t2 :] by XBOOLE_0:def 3;
y in (the Symbols of t1) \/ the Symbols of t2 by XBOOLE_0:def 3;
then reconsider
xx=x as Element of [: UnionSt(t1,t2), (the Symbols of t1) \/ the
Symbols of t2 :] by A3,ZFMISC_1:def 2;
A4: FirstTuringState xx = [[p,q0],y]`1`1
.=[p,q0]`1
.=p;
A5: FirstTuringSymbol(xx)=[[p,q0],y]`2 by Def27
.=y;
thus (the Tran of t1 ';' t2).x = UnionTran(t1,t2).xx by Def31
.=Uniontran(t1,t2,xx) by Def30
.=FirstTuringTran(t1,t2,(the Tran of t1).[p,y]) by A1,A4,A5,Def29
.=[[g`1_3,q0], g`2_3, g`3_3] by A2;
end;
theorem Th44:
for T1,T2 being TuringStr, g be Tran-Goal of T2, q be State of
T2, y be Symbol of T2 st g = (the Tran of T2).[q, y] holds (the Tran of T1 ';'
T2).[ [the AcceptS of T1,q],y] = [[the AcceptS of T1,g`1_3], g`2_3, g`3_3]
proof
let t1,t2 be TuringStr, g be Tran-Goal of t2,q be State of t2, y be Symbol
of t2;
assume
A1: g = (the Tran of t2).[q, y];
set pF=the AcceptS of t1;
set x=[[pF,q],y];
pF in { pF } by TARSKI:def 1;
then [pF,q] in [: {pF}, the FStates of t2 :] by ZFMISC_1:def 2;
then
A2: [pF,q] in [: the FStates of t1, {the InitS of t2} :] \/ [: {pF}, the
FStates of t2 :] by XBOOLE_0:def 3;
y in (the Symbols of t1) \/ the Symbols of t2 by XBOOLE_0:def 3;
then reconsider
xx=x as Element of [: UnionSt(t1,t2), (the Symbols of t1) \/ the
Symbols of t2 :] by A2,ZFMISC_1:def 2;
A3: SecondTuringState xx =[[pF,q],y]`1`2
.=q;
A4: SecondTuringSymbol(xx)=[[pF,q],y]`2 by Def28
.=y;
thus (the Tran of t1 ';' t2).x = UnionTran(t1,t2).xx by Def31
.=Uniontran(t1,t2,xx) by Def30
.=SecondTuringTran(t1,t2,(the Tran of t2).[q,y]) by A3,A4,Def29
.=[[pF,g`1_3], g`2_3, g`3_3] by A1;
end;
theorem Th45:
for T1,T2 being TuringStr,s1 be All-State of T1,h be Element of
NAT, t be Tape of T1, s2 be All-State of T2,s3 be All-State of (T1 ';' T2) st
s1 is Accept-Halt & s1=[the InitS of T1,h,t] & s2 is Accept-Halt & s2=[the
InitS of T2,(Result s1)`2_3,(Result s1)`3_3] &
s3=[the InitS of (T1 ';' T2),h,t]
holds s3 is Accept-Halt & (Result s3)`2_3=(Result s2)`2_3 &
(Result s3)`3_3=(Result
s2)`3_3
proof
let tm1,tm2 be TuringStr,s1 be All-State of tm1,h be Element of NAT, t be
Tape of tm1, s2 be All-State of tm2, s3 be All-State of (tm1 ';' tm2);
set p0=the InitS of tm1, q0=the InitS of tm2;
assume that
A1: s1 is Accept-Halt and
A2: s1=[p0,h,t] and
A3: s2 is Accept-Halt and
A4: s2=[q0,(Result s1)`2_3,(Result s1)`3_3] and
A5: s3=[the InitS of (tm1 ';' tm2),h,t];
set pF=the AcceptS of tm1, qF=the AcceptS of tm2;
consider k such that
A6: ((Computation s1).k)`1_3 = pF and
A7: Result s1 = (Computation s1).k and
A8: for i be Nat st i < k holds ((Computation s1).i)`1_3 <> pF
by A1,Th13;
defpred P[Nat] means
$1 <= k implies [((Computation s1).$1)`1_3,q0]
=((Computation s3).$1)`1_3 &
((Computation s1).$1)`2_3=((Computation s3).$1)`2_3 & ((
Computation s1).$1)`3_3=((Computation s3).$1)`3_3;
A9: for i st P[i] holds P[i + 1]
proof
let i;
assume
A10: P[i];
now
set s1i1=(Computation s1).(i+1), s1i=(Computation s1).i, s3i1=(
Computation s3).(i+1), s3i=(Computation s3).i;
A11: i < i+1 by XREAL_1:29;
set f=TRAN(s3i);
reconsider h=Head(s1i) as Element of INT;
reconsider ss1=s1i`3_3 as Tape of tm1;
reconsider y=ss1.h as Symbol of tm1;
reconsider ss3=s3i`3_3 as Tape of tm1 ';' tm2;
set p=s1i`1_3, g=TRAN(s1i);
assume
A12: i+1 <= k;
then
A13: i < k by A11,XXREAL_0:2;
then
A14: p <> pF by A8;
A15: s3i`1_3 <> the AcceptS of tm1 ';' tm2
proof
assume s3i`1_3 = the AcceptS of tm1 ';' tm2;
then [p,q0] = [pF,qF] by A10,A12,A11,Def31,XXREAL_0:2;
hence contradiction by A14,XTUPLE_0:1;
end;
A16: f= (the Tran of tm1 ';' tm2).[[p,q0],y] by A10,A12,A11,XXREAL_0:2
.= [[g`1_3,q0], g`2_3, g`3_3] by A8,A13,Th43;
then
A17: g`2_3=f`2_3;
A18: s3i1=Following s3i by Def7
.= [f`1_3, Head(s3i)+ offset (f),Tape-Chg(ss3,Head(s3i),f`2_3)]
by A15,Def6;
A19: s1i1=Following s1i by Def7
.= [g`1_3, h+ offset(g),Tape-Chg(ss1,h,g`2_3)] by A14,Def6;
hence [s1i1`1_3,q0]=[g`1_3,q0]
.=f`1_3 by A16
.=s3i1`1_3 by A18;
offset g=offset f by A16;
hence s1i1`2_3= Head(s3i) + offset f by A10,A12,A11,A19,XXREAL_0:2
.= s3i1`2_3 by A18;
thus s1i1`3_3= ss3 +* (h .--> (g`2_3)) by A10,A12,A11,A19,XXREAL_0:2
.= s3i1`3_3 by A10,A12,A11,A17,A18,XXREAL_0:2;
end;
hence thesis;
end;
set s1k=(Computation s1).k, s3k=(Computation s3).k;
A20: s3=[[p0,q0],h,t] by A5,Def31;
A21: P[0]
proof
assume 0 <= k;
A22: ((Computation s3).0)`1_3=s3`1_3 by Def7
.=[p0,q0] by A20;
((Computation s1).0)`1_3=s1`1_3 by Def7
.=p0 by A2;
hence [((Computation s1).0)`1_3,q0]=((Computation s3).0)`1_3 by A22;
thus ((Computation s1).0)`2_3=s1`2_3 by Def7
.=h by A2
.=s3`2_3 by A5
.=((Computation s3).0)`2_3 by Def7;
thus ((Computation s1).0)`3_3=s1`3_3 by Def7
.=t by A2
.=s3`3_3 by A5
.=((Computation s3).0)`3_3 by Def7;
end;
A23: for i holds P[i] from NAT_1:sch 2(A21,A9);
then
A24: s1k`2_3=s3k`2_3;
consider m be Nat such that
A25: ((Computation s2).m)`1_3 = qF and
A26: Result s2 = (Computation s2).m and
A27: for i be Nat st i < m holds ((Computation s2).i)`1_3 <> qF
by A3,Th13;
defpred Q[Nat] means
$1 <= m implies [pF,((Computation s2).$1)`1_3]
=((Computation s3k).$1)`1_3 &
((Computation s2).$1)`2_3=((Computation s3k).$1)`2_3 &
((Computation s2).$1)`3_3=((Computation s3k).$1)`3_3;
A28: for i st Q[i] holds Q[i + 1]
proof
let i;
assume
A29: Q[i];
now
set s2i1=(Computation s2).(i+1), s2i=(Computation s2).i, ski1=(
Computation s3k).(i+1), ski=(Computation s3k).i;
A30: i < i+1 by XREAL_1:29;
reconsider ssk=ski`3_3 as Tape of tm1 ';' tm2;
set f=TRAN(ski);
set q=s2i`1_3, g=TRAN(s2i);
reconsider h=Head(s2i) as Element of INT;
reconsider ss2=s2i`3_3 as Tape of tm2;
reconsider y=ss2.h as Symbol of tm2;
assume
A31: i+1 <= m;
then
A32: f= (the Tran of tm1 ';' tm2).[[pF,q],y] by A29,A30,XXREAL_0:2
.= [[pF,g`1_3], g`2_3, g`3_3] by Th44;
then
A33: g`2_3=f`2_3;
i < m by A31,A30,XXREAL_0:2;
then
A34: q <> qF by A27;
A35: ski`1_3 <> the AcceptS of tm1 ';' tm2
proof
assume ski`1_3 = the AcceptS of tm1 ';' tm2;
then [pF,q] = [pF,qF] by A29,A31,A30,Def31,XXREAL_0:2;
hence contradiction by A34,XTUPLE_0:1;
end;
A36: ski1=Following ski by Def7
.= [f`1_3, Head(ski)+ offset (f),Tape-Chg(ssk,Head(ski),f`2_3)]
by A35,Def6;
A37: s2i1=Following s2i by Def7
.= [g`1_3, h+ offset(g),Tape-Chg(ss2,h,g`2_3)] by A34,Def6;
hence [pF,s2i1`1_3]=[pF,g`1_3]
.=f`1_3 by A32
.=ski1`1_3 by A36;
offset g=offset f by A32;
hence s2i1`2_3= Head(ski) + offset f by A29,A31,A30,A37,XXREAL_0:2
.= ski1`2_3 by A36;
thus s2i1`3_3= ssk +* (h .--> (g`2_3)) by A29,A31,A30,A37,XXREAL_0:2
.= ski1`3_3 by A29,A31,A30,A33,A36,XXREAL_0:2;
end;
hence thesis;
end;
A38: s1k`3_3=s3k`3_3 by A23;
set s2m=(Computation s2).m, skm=(Computation s3k).m;
A39: (Computation s3).(k+m)=skm by Th10;
A40: [s1k`1_3,q0]=s3k`1_3 by A23;
A41: Q[0]
proof
assume 0 <= m;
thus [pF,((Computation s2).0)`1_3]=[pF,s2`1_3] by Def7
.=[pF,q0] by A4
.=((Computation s3k).0)`1_3 by A6,A40,Def7;
thus ((Computation s2).0)`2_3=s2`2_3 by Def7
.=s3k`2_3 by A4,A7,A24
.=((Computation s3k).0)`2_3 by Def7;
thus ((Computation s2).0)`3_3=s2`3_3 by Def7
.=s3k`3_3 by A4,A7,A38
.=((Computation s3k).0)`3_3 by Def7;
end;
A42: for i holds Q[i] from NAT_1:sch 2(A41,A28);
then [pF,s2m`1_3]=skm`1_3;
then
A43: ((Computation s3).(k+m))`1_3=the AcceptS of tm1 ';' tm2 by A25,A39,Def31;
hence
A44: s3 is Accept-Halt;
s2m`2_3=skm`2_3 & s2m`3_3=skm`3_3 by A42;
hence thesis by A26,A39,A43,A44,Def9;
end;
theorem
for tm1,tm2 being TuringStr,t be Tape of tm1 st the Symbols of tm1 =
the Symbols of tm2 holds t is Tape of tm1 ';' tm2
proof
let tm1,tm2 be TuringStr,t be Tape of tm1;
set S1=the Symbols of tm1, S2=the Symbols of tm2;
assume
A1: S1=S2;
the Symbols of tm1 ';' tm2=S1 \/ S2 by Def31
.=S1 by A1;
hence thesis;
end;
theorem
for tm1,tm2 being TuringStr,t be Tape of tm1 ';' tm2 st the Symbols of
tm1 = the Symbols of tm2 holds t is Tape of tm1 & t is Tape of tm2
proof
let tm1,tm2 be TuringStr,t be Tape of tm1 ';' tm2;
set S1=the Symbols of tm1, S2=the Symbols of tm2;
assume
A1: S1=S2;
the Symbols of tm1 ';' tm2=S1 \/ S2 by Def31
.=S1 by A1;
hence thesis by A1;
end;
theorem Th48:
for f being FinSequence of NAT,tm1,tm2 be TuringStr,t1 be Tape
of tm1, t2 be Tape of tm2 st t1=t2 & t1 storeData f holds t2 storeData f
proof
let f be FinSequence of NAT,tm1,tm2 be TuringStr,t1 be Tape of tm1, t2 be
Tape of tm2;
assume that
A1: t1=t2 and
A2: t1 storeData f;
now
let i be Nat;
set m=Sum Prefix(f,i)+2*(i-1), n=Sum Prefix(f,i+1)+2*i;
assume 1 <= i & i < len f;
then
A3: t1 is_1_between m,n by A2;
then
A4: for k be Integer st m < k & k < n holds t1.k=1;
t1.m=0 & t1.n=0 by A3;
hence t2 is_1_between m,n by A1,A4;
end;
hence thesis;
end;
Lm15: for s being All-State of ZeroTuring, t be Tape of ZeroTuring, head, n be
Element of NAT st s=[0,head,t] & t storeData <*head,n*> holds s is Accept-Halt
& (Result s)`2_3=head & (Result s)`3_3 storeData <*head,0*>
proof
let s be All-State of ZeroTuring, t be Tape of ZeroTuring, h,n be Element of
NAT;
len <*n*> =1 by FINSEQ_1:39;
hence thesis by Th34;
end;
theorem
for s being All-State of ZeroTuring ';' SuccTuring, t be Tape of
ZeroTuring , head,n be Element of NAT st s=[[0,0],head,t] & t storeData <*head,
n*> holds s is Accept-Halt & (Result s)`2_3=head &
(Result s)`3_3 storeData <*head,
1*>
proof
let s be All-State of ZeroTuring ';' SuccTuring, t be Tape of ZeroTuring, h,
n be Element of NAT;
assume that
A1: s=[[0,0],h,t] and
A2: t storeData <*h,n*>;
reconsider h1=h as Element of INT by INT_1:def 2;
set s1=[the InitS of ZeroTuring,h1,t];
A3: 0=the InitS of ZeroTuring by Def19;
then
A4: s1 is Accept-Halt & (Result s1)`2_3=h by A2,Lm15;
the Symbols of ZeroTuring={0,1} by Def19
.=the Symbols of SuccTuring by Def17;
then reconsider t2=(Result s1)`3_3 as Tape of SuccTuring;
set s2=[the InitS of SuccTuring,h1,t2];
A5: 0=the InitS of SuccTuring by Def17;
then
A6: s=[the InitS of ZeroTuring ';' SuccTuring,h,t] by A1,A3,Def31;
(Result s1)`3_3 storeData <*h,0 *> by A2,A3,Lm15;
then
A7: t2 storeData <*h,0*> by Th48;
then
A8: (Result s2)`3_3 storeData <*h,0+ 1 *> by A5,Th31;
A9: s2 is Accept-Halt by A7,A5,Th31;
hence s is Accept-Halt by A4,A6,Th45;
(Result s2)`2_3=h by A7,A5,Th31;
hence (Result s)`2_3=h by A4,A9,A6,Th45;
(Result s)`3_3=(Result s2)`3_3 by A4,A9,A6,Th45;
hence thesis by A8,Th48;
end;