:: Introduction to Turing Machines
:: by Jingchao Chen and Yatsuka Nakamura
::
:: Received July 27, 2001
:: Copyright (c) 2001-2021 Association of Mizar Users


definition
let A, B be non empty set ;
let f be Function of A,B;
let g be PartFunc of A,B;
:: original: +*
redefine func f +* g -> Function of A,B;
coherence
f +* g is Function of A,B
proof end;
end;

definition
let X, Y be non empty set ;
let a be Element of X;
let b be Element of Y;
:: original: .-->
redefine func a .--> b -> PartFunc of X,Y;
coherence
a .--> b is PartFunc of X,Y
proof end;
end;

notation
let n be Nat;
synonym SegM n for succ n;
end;

definition
let n be Nat;
:: original: SegM
redefine func SegM n -> Subset of NAT equals :: TURING_1:def 1
 { k where k is Nat : k <= n } ;
coherence
SegM n is Subset of NAT
proof end;
compatibility
for b1 being Subset of NAT holds
( b1 = SegM n iff b1 = { k where k is Nat : k <= n } )
proof end;
end;

:: deftheorem defines SegM TURING_1:def 1 :
for n being Nat holds SegM n = { k where k is Nat : k <= n } ;

theorem Th1: :: TURING_1:1
for n, k being Nat holds
( k in SegM n iff k <= n )
proof end;

theorem Th2: :: TURING_1:2
for f being Function
for x, y, z, u, v being object st u <> x holds
(f +* ([x,y] .--> z)) . [u,v] = f . [u,v]
proof end;

theorem Th3: :: TURING_1:3
for f being Function
for x, y, z, u, v being object st v <> y holds
(f +* ([x,y] .--> z)) . [u,v] = f . [u,v]
proof end;

notation
let i be Nat;
let f be FinSequence;
synonym Prefix (f,i) for f | i;
end;

registration
let f be natural-valued FinSequence;
let n be Nat;
cluster Prefix (f,n) -> INT -valued for FinSequence;
coherence
for b1 being FinSequence st b1 = Prefix (f,n) holds
b1 is INT -valued ;
end;

theorem Th4: :: TURING_1:4
for x1, x2 being Element of NAT holds
( Sum (Prefix (<*x1,x2*>,1)) = x1 & Sum (Prefix (<*x1,x2*>,2)) = x1 + x2 )
proof end;

theorem Th5: :: TURING_1:5
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 end;

definition
attr c1 is strict ;
struct TuringStr -> ;
aggr TuringStr(# Symbols, FStates, Tran, InitS, AcceptS #) -> TuringStr ;
sel Symbols c1 -> non empty finite set ;
sel FStates c1 -> non empty finite set ;
sel Tran c1 -> Function of [: the FStates of c1, the Symbols of c1:],[: the FStates of c1, the Symbols of c1,{(- 1),0,1}:];
sel InitS c1 -> Element of the FStates of c1;
sel AcceptS c1 -> Element of the FStates of c1;
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 ;
let t be Tape of T;
let h be Integer;
let s be Symbol of T;
func Tape-Chg (t,h,s) -> Tape of T equals :: TURING_1:def 2
t +* (h .--> s);
coherence
t +* (h .--> s) is Tape of T
proof end;
end;

:: deftheorem defines Tape-Chg TURING_1:def 2 :
for T being TuringStr
for t being Tape of T
for h being Integer
for s being Symbol of T holds Tape-Chg (t,h,s) = t +* (h .--> s);

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 ;
let g be Tran-Goal of T;
func offset g -> Integer equals :: TURING_1:def 3
g `3_3 ;
coherence
g `3_3 is Integer by ENUMSET1:def 1;
end;

:: deftheorem defines offset TURING_1:def 3 :
for T being TuringStr
for g being Tran-Goal of T holds offset g = g `3_3 ;

definition
let T be TuringStr ;
let s be All-State of T;
func Head s -> Integer equals :: TURING_1:def 4
s `2_3 ;
coherence
s `2_3 is Integer ;
end;

:: deftheorem defines Head TURING_1:def 4 :
for T being TuringStr
for s being All-State of T holds Head s = s `2_3 ;

definition
let T be TuringStr ;
let s be All-State of T;
func TRAN s -> Tran-Goal of T equals :: TURING_1:def 5
 the Tran of T . [(s `1_3),((s `3_3) . (Head s))];
correctness
coherence
the Tran of T . [(s `1_3),((s `3_3) . (Head s))] is Tran-Goal of T;
proof end;
end;

:: deftheorem defines TRAN TURING_1:def 5 :
for T being TuringStr
for s being All-State of T holds TRAN s = the Tran of T . [(s `1_3),((s `3_3) . (Head s))];

definition
let T be TuringStr ;
let s be All-State of T;
func Following s -> All-State of T equals :Def6: :: TURING_1:def 6
[((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
coherence
( ( s `1_3 <> the AcceptS of T implies [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))] is All-State of T ) & ( not s `1_3 <> the AcceptS of T implies s is All-State of T ) );
consistency
for b1 being All-State of T holds verum;
proof end;
end;

:: deftheorem Def6 defines Following TURING_1:def 6 :
for T being TuringStr
for s being All-State of T holds
( ( s `1_3 <> the AcceptS of T implies Following s = [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))] ) & ( not s `1_3 <> the AcceptS of T implies Following s = s ) );

definition
let T be TuringStr ;
let s be All-State of T;
func Computation s -> sequence of [: the FStates of T,INT,(Funcs (INT, the Symbols of T)):] means :Def7: :: TURING_1:def 7
( it . 0 = s & ( for i being Nat holds it . (i + 1) = Following (it . i) ) );
existence
ex b1 being sequence of [: the FStates of T,INT,(Funcs (INT, the Symbols of T)):] st
( b1 . 0 = s & ( for i being Nat holds b1 . (i + 1) = Following (b1 . i) ) )
proof end;
uniqueness
for b1, b2 being sequence of [: the FStates of T,INT,(Funcs (INT, the Symbols of T)):] st b1 . 0 = s & ( for i being Nat holds b1 . (i + 1) = Following (b1 . i) ) & b2 . 0 = s & ( for i being Nat holds b2 . (i + 1) = Following (b2 . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Computation TURING_1:def 7 :
for T being TuringStr
for s being All-State of T
for b3 being sequence of [: the FStates of T,INT,(Funcs (INT, the Symbols of T)):] holds
( b3 = Computation s iff ( b3 . 0 = s & ( for i being Nat holds b3 . (i + 1) = Following (b3 . i) ) ) );

theorem :: TURING_1:6
for T being TuringStr
for s being All-State of T st s `1_3 = the AcceptS of T holds
s = Following s by Def6;

theorem :: TURING_1:7
for T being TuringStr
for s being All-State of T holds (Computation s) . 0 = s by Def7;

theorem :: TURING_1:8
for k being Nat
for T being TuringStr
for s being All-State of T holds (Computation s) . (k + 1) = Following ((Computation s) . k) by Def7;

theorem Th9: :: TURING_1:9
for T being TuringStr
for s being All-State of T holds (Computation s) . 1 = Following s
proof end;

theorem Th10: :: TURING_1:10
for i, k being Nat
for T being TuringStr
for s being All-State of T holds (Computation s) . (i + k) = (Computation ((Computation s) . i)) . k
proof end;

theorem Th11: :: TURING_1:11
for i, j being Nat
for T being TuringStr
for s being All-State of T st i <= j & Following ((Computation s) . i) = (Computation s) . i holds
(Computation s) . j = (Computation s) . i
proof end;

theorem Th12: :: TURING_1:12
for i, j being Nat
for T being TuringStr
for s being All-State of T st i <= j & ((Computation s) . i) `1_3 = the AcceptS of T holds
(Computation s) . j = (Computation s) . i
proof end;

definition
let T be TuringStr ;
let s be All-State of T;
attr s is Accept-Halt means :: TURING_1:def 8
 ex k being Nat st ((Computation s) . k) `1_3 = the AcceptS of T;
end;

:: deftheorem defines Accept-Halt TURING_1:def 8 :
for T being TuringStr
for s being All-State of T holds
( s is Accept-Halt iff ex k being Nat st ((Computation s) . k) `1_3 = the AcceptS of T );

definition
let T be TuringStr ;
let s be All-State of T;
assume A1: s is Accept-Halt ;
func Result s -> All-State of T means :Def9: :: TURING_1:def 9
 ex k being Nat st
( it = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T );
uniqueness
for b1, b2 being All-State of T st ex k being Nat st
( b1 = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T ) & ex k being Nat st
( b2 = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T ) holds
b1 = b2
proof end;
correctness
existence
ex b1 being All-State of T ex k being Nat st
( b1 = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T );
by A1;
end;

:: deftheorem Def9 defines Result TURING_1:def 9 :
for T being TuringStr
for s being All-State of T st s is Accept-Halt holds
for b3 being All-State of T holds
( b3 = Result s iff ex k being Nat st
( b3 = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T ) );

theorem Th13: :: TURING_1:13
for T being TuringStr
for s being All-State of T st s is Accept-Halt holds
ex k being Nat st
( ((Computation s) . k) `1_3 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Nat st i < k holds
((Computation s) . i) `1_3 <> the AcceptS of T ) )
proof end;

definition
let A, B be non empty set ;
let y be set ;
assume A1: y in B ;
func id (A,B,y) -> Function of A,[:A,B:] means :: TURING_1:def 10
 for x being Element of A holds it . x = [x,y];
existence
ex b1 being Function of A,[:A,B:] st
for x being Element of A holds b1 . x = [x,y]
proof end;
uniqueness
for b1, b2 being Function of A,[:A,B:] st ( for x being Element of A holds b1 . x = [x,y] ) & ( for x being Element of A holds b2 . x = [x,y] ) holds
b1 = b2
proof end;
end;

:: deftheorem defines id TURING_1:def 10 :
for A, B being non empty set
for y being set st y in B holds
for b4 being Function of A,[:A,B:] holds
( b4 = id (A,B,y) iff for x being Element of A holds b4 . x = [x,y] );

definition
func Sum_Tran -> Function of [:(SegM 5),{0,1}:],[:(SegM 5),{0,1},{(- 1),0,1}:] equals :: TURING_1:def 11
(((((((((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
(((((((((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]) is Function of [:(SegM 5),{0,1}:],[:(SegM 5),{0,1},{(- 1),0,1}:]
proof end;
end;

:: deftheorem defines Sum_Tran TURING_1:def 11 :
Sum_Tran = (((((((((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]);

theorem Th14: :: TURING_1:14
( 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 end;

definition
let T be TuringStr ;
let t be Tape of T;
let i, j be Integer;
pred t is_1_between i,j means :: TURING_1:def 12
( t . i = 0 & t . j = 0 & ( for k being Integer st i < k & k < j holds
t . k = 1 ) );
end;

:: deftheorem defines is_1_between TURING_1:def 12 :
for T being TuringStr
for t being Tape of T
for i, j being Integer holds
( t is_1_between i,j iff ( t . i = 0 & t . j = 0 & ( for k being Integer st i < k & k < j holds
t . k = 1 ) ) );

definition
let f be natural-valued FinSequence;
let T be TuringStr ;
let t be Tape of T;
pred t storeData f means :: TURING_1:def 13
 for i being 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;

:: deftheorem defines storeData TURING_1:def 13 :
for f being natural-valued FinSequence
for T being TuringStr
for t being Tape of T holds
( t storeData f iff for i being 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) );

theorem Th15: :: TURING_1:15
for T being TuringStr
for t being Tape of T
for s, n being Element of NAT st t storeData <*s,n*> holds
t is_1_between s,(s + n) + 2
proof end;

theorem Th16: :: TURING_1:16
for T being TuringStr
for t being Tape of T
for s, n being Element of NAT st t is_1_between s,(s + n) + 2 holds
t storeData <*s,n*>
proof end;

theorem Th17: :: TURING_1:17
for T being TuringStr
for t being Tape of T
for s, n being Element of NAT st t storeData <*s,n*> holds
( t . s = 0 & t . ((s + n) + 2) = 0 & ( for i being Integer st s < i & i < (s + n) + 2 holds
t . i = 1 ) )
proof end;

theorem Th18: :: TURING_1:18
for T being TuringStr
for t being Tape of T
for s, n1, n2 being 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 end;

theorem Th19: :: TURING_1:19
for T being TuringStr
for t being Tape of T
for s, n1, n2 being 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 being Integer st s < i & i < (s + n1) + 2 holds
t . i = 1 ) & ( for i being Integer st (s + n1) + 2 < i & i < ((s + n1) + n2) + 4 holds
t . i = 1 ) )
proof end;

theorem Th20: :: TURING_1:20
for f being FinSequence of NAT
for 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 end;

theorem Th21: :: TURING_1:21
for f being FinSequence of NAT
for 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 end;

theorem Th22: :: TURING_1:22
for T being TuringStr
for t being Tape of T
for s being Element of NAT
for f being FinSequence of NAT st len f >= 1 & t storeData <*s*> ^ f holds
t is_1_between s,(s + (f /. 1)) + 2
proof end;

theorem Th23: :: TURING_1:23
for T being TuringStr
for t being Tape of T
for s being Element of NAT
for f being 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 end;

definition
func SumTuring -> strict TuringStr means :Def14: :: TURING_1:def 14
( 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
ex b1 being strict TuringStr st
( the Symbols of b1 = {0,1} & the FStates of b1 = SegM 5 & the Tran of b1 = Sum_Tran & the InitS of b1 = 0 & the AcceptS of b1 = 5 )
proof end;
uniqueness
for b1, b2 being strict TuringStr st the Symbols of b1 = {0,1} & the FStates of b1 = SegM 5 & the Tran of b1 = Sum_Tran & the InitS of b1 = 0 & the AcceptS of b1 = 5 & the Symbols of b2 = {0,1} & the FStates of b2 = SegM 5 & the Tran of b2 = Sum_Tran & the InitS of b2 = 0 & the AcceptS of b2 = 5 holds
b1 = b2 ;
end;

:: deftheorem Def14 defines SumTuring TURING_1:def 14 :
for b1 being strict TuringStr holds
( b1 = SumTuring iff ( the Symbols of b1 = {0,1} & the FStates of b1 = SegM 5 & the Tran of b1 = Sum_Tran & the InitS of b1 = 0 & the AcceptS of b1 = 5 ) );

Lm1: for n being Element of NAT st n <= 5 holds
n is State of SumTuring
proof end;

theorem Th24: :: TURING_1:24
for T being TuringStr
for t being Tape of T
for h being Integer
for s being Symbol of T st t . h = s holds
Tape-Chg (t,h,s) = t
proof end;

Lm2: ( 0 in the Symbols of SumTuring & 1 in the Symbols of SumTuring )
proof end;

theorem Th25: :: TURING_1:25
for T being TuringStr
for s being All-State of T
for p, h, t being 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
for p, h, t being 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 end;

theorem Th26: :: TURING_1:26
for T being TuringStr
for t being Tape of T
for h being Integer
for s being Symbol of T
for i being object holds
( (Tape-Chg (t,h,s)) . h = s & ( i <> h implies (Tape-Chg (t,h,s)) . i = t . i ) )
proof end;

Lm4: for tm being TuringStr
for s being All-State of tm
for p being State of tm
for h being Element of INT
for t being Tape of tm
for m, d being 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 being Integer st d <= i & i < d + m holds
t . i = 1 ) holds
(Computation s) . m = [p,(d + m),t]
proof end;

theorem Th27: :: TURING_1:27
for s being All-State of SumTuring
for t being Tape of SumTuring
for head, n1, n2 being 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 end;

definition
let T be TuringStr ;
let F be Function;
pred T computes F means :: TURING_1:def 15
 for s being All-State of T
for t being Tape of T
for a being Element of NAT
for 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;

:: deftheorem defines computes TURING_1:def 15 :
for T being TuringStr
for F being Function holds
( T computes F iff for s being All-State of T
for t being Tape of T
for a being Element of NAT
for 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*> ) ) );

theorem Th28: :: TURING_1:28
dom [+] c= 2 -tuples_on NAT
proof end;

theorem :: TURING_1:29
SumTuring computes [+]
proof end;

definition
func Succ_Tran -> Function of [:(SegM 4),{0,1}:],[:(SegM 4),{0,1},{(- 1),0,1}:] equals :: TURING_1:def 16
(((((((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
(((((((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]) is Function of [:(SegM 4),{0,1}:],[:(SegM 4),{0,1},{(- 1),0,1}:]
proof end;
end;

:: deftheorem defines Succ_Tran TURING_1:def 16 :
Succ_Tran = (((((((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]);

theorem Th30: :: TURING_1:30
( 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 end;

definition
func SuccTuring -> strict TuringStr means :Def17: :: TURING_1:def 17
( 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
ex b1 being strict TuringStr st
( the Symbols of b1 = {0,1} & the FStates of b1 = SegM 4 & the Tran of b1 = Succ_Tran & the InitS of b1 = 0 & the AcceptS of b1 = 4 )
proof end;
uniqueness
for b1, b2 being strict TuringStr st the Symbols of b1 = {0,1} & the FStates of b1 = SegM 4 & the Tran of b1 = Succ_Tran & the InitS of b1 = 0 & the AcceptS of b1 = 4 & the Symbols of b2 = {0,1} & the FStates of b2 = SegM 4 & the Tran of b2 = Succ_Tran & the InitS of b2 = 0 & the AcceptS of b2 = 4 holds
b1 = b2 ;
end;

:: deftheorem Def17 defines SuccTuring TURING_1:def 17 :
for b1 being strict TuringStr holds
( b1 = SuccTuring iff ( the Symbols of b1 = {0,1} & the FStates of b1 = SegM 4 & the Tran of b1 = Succ_Tran & the InitS of b1 = 0 & the AcceptS of b1 = 4 ) );

Lm5: for n being Element of NAT st n <= 4 holds
n is State of SuccTuring
proof end;

Lm6: ( 0 in the Symbols of SuccTuring & 1 in the Symbols of SuccTuring )
proof end;

Lm7: for s being All-State of SuccTuring
for p, h, t being 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 end;

theorem Th31: :: TURING_1:31
for s being All-State of SuccTuring
for t being Tape of SuccTuring
for head, n being 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 end;

theorem :: TURING_1:32
SuccTuring computes 1 succ 1
proof end;

definition
func Zero_Tran -> Function of [:(SegM 4),{0,1}:],[:(SegM 4),{0,1},{(- 1),0,1}:] equals :: TURING_1:def 18
(((((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
(((((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)]) is Function of [:(SegM 4),{0,1}:],[:(SegM 4),{0,1},{(- 1),0,1}:]
proof end;
end;

:: deftheorem defines Zero_Tran TURING_1:def 18 :
Zero_Tran = (((((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)]);

theorem Th33: :: TURING_1:33
( 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 end;

definition
func ZeroTuring -> strict TuringStr means :Def19: :: TURING_1:def 19
( 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
ex b1 being strict TuringStr st
( the Symbols of b1 = {0,1} & the FStates of b1 = SegM 4 & the Tran of b1 = Zero_Tran & the InitS of b1 = 0 & the AcceptS of b1 = 4 )
proof end;
uniqueness
for b1, b2 being strict TuringStr st the Symbols of b1 = {0,1} & the FStates of b1 = SegM 4 & the Tran of b1 = Zero_Tran & the InitS of b1 = 0 & the AcceptS of b1 = 4 & the Symbols of b2 = {0,1} & the FStates of b2 = SegM 4 & the Tran of b2 = Zero_Tran & the InitS of b2 = 0 & the AcceptS of b2 = 4 holds
b1 = b2 ;
end;

:: deftheorem Def19 defines ZeroTuring TURING_1:def 19 :
for b1 being strict TuringStr holds
( b1 = ZeroTuring iff ( the Symbols of b1 = {0,1} & the FStates of b1 = SegM 4 & the Tran of b1 = Zero_Tran & the InitS of b1 = 0 & the AcceptS of b1 = 4 ) );

Lm8: for n being Element of NAT st n <= 4 holds
n is State of ZeroTuring
proof end;

Lm9: ( 0 in the Symbols of ZeroTuring & 1 in the Symbols of ZeroTuring )
proof end;

Lm10: for s being All-State of ZeroTuring
for p, h, t being 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 end;

theorem Th34: :: TURING_1:34
for s being All-State of ZeroTuring
for t being Tape of ZeroTuring
for head being Element of NAT
for f being 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 end;

theorem :: TURING_1:35
for n being Nat st n >= 1 holds
ZeroTuring computes n const 0
proof end;

definition
func U3(n)Tran -> Function of [:(SegM 3),{0,1}:],[:(SegM 3),{0,1},{(- 1),0,1}:] equals :: TURING_1:def 20
(((((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
(((((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]) is Function of [:(SegM 3),{0,1}:],[:(SegM 3),{0,1},{(- 1),0,1}:]
proof end;
end;

:: deftheorem defines U3(n)Tran TURING_1:def 20 :
U3(n)Tran = (((((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]);

theorem Th36: :: TURING_1:36
( 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 end;

definition
func U3(n)Turing -> strict TuringStr means :Def21: :: TURING_1:def 21
( 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
ex b1 being strict TuringStr st
( the Symbols of b1 = {0,1} & the FStates of b1 = SegM 3 & the Tran of b1 = U3(n)Tran & the InitS of b1 = 0 & the AcceptS of b1 = 3 )
proof end;
uniqueness
for b1, b2 being strict TuringStr st the Symbols of b1 = {0,1} & the FStates of b1 = SegM 3 & the Tran of b1 = U3(n)Tran & the InitS of b1 = 0 & the AcceptS of b1 = 3 & the Symbols of b2 = {0,1} & the FStates of b2 = SegM 3 & the Tran of b2 = U3(n)Tran & the InitS of b2 = 0 & the AcceptS of b2 = 3 holds
b1 = b2 ;
end;

:: deftheorem Def21 defines U3(n)Turing TURING_1:def 21 :
for b1 being strict TuringStr holds
( b1 = U3(n)Turing iff ( the Symbols of b1 = {0,1} & the FStates of b1 = SegM 3 & the Tran of b1 = U3(n)Tran & the InitS of b1 = 0 & the AcceptS of b1 = 3 ) );

Lm11: for n being Element of NAT st n <= 3 holds
n is State of U3(n)Turing
proof end;

Lm12: ( 0 in the Symbols of U3(n)Turing & 1 in the Symbols of U3(n)Turing )
proof end;

Lm13: for s being All-State of U3(n)Turing
for p, h, t being 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 end;

Lm14: for tm being TuringStr
for s being All-State of tm
for p being State of tm
for h being Element of INT
for t being Tape of tm
for m, d being 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 being 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 being Integer st d <= i & i < d + m holds
t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds
t1 . i = t . i ) )
proof end;

theorem Th37: :: TURING_1:37
for s being All-State of U3(n)Turing
for t being Tape of U3(n)Turing
for head being Element of NAT
for f being 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 end;

theorem :: TURING_1:38
for n being Nat st n >= 3 holds
U3(n)Turing computes n proj 3
proof end;

definition
let t1, t2 be TuringStr ;
func UnionSt (t1,t2) -> non empty finite set equals :: TURING_1:def 22
[: the FStates of t1,{ the InitS of t2}:] \/ [:{ the AcceptS of t1}, the FStates of t2:];
correctness
coherence
[: the FStates of t1,{ the InitS of t2}:] \/ [:{ the AcceptS of t1}, the FStates of t2:] is non empty finite set ;
;
end;

:: deftheorem defines UnionSt TURING_1:def 22 :
for t1, t2 being TuringStr holds UnionSt (t1,t2) = [: the FStates of t1,{ the InitS of t2}:] \/ [:{ the AcceptS of t1}, the FStates of t2:];

theorem Th39: :: TURING_1:39
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 end;

theorem Th40: :: TURING_1:40
for s, t being TuringStr
for x being State of s holds [x, the InitS of t] in UnionSt (s,t)
proof end;

theorem Th41: :: TURING_1:41
for s, t being TuringStr
for x being State of t holds [ the AcceptS of s,x] in UnionSt (s,t)
proof end;

theorem Th42: :: TURING_1:42
for s, t being TuringStr
for x being Element of UnionSt (s,t) ex x1 being State of s ex x2 being State of t st x = [x1,x2]
proof end;

definition
let s, t be TuringStr ;
let 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 :: TURING_1:def 23
[[(x `1_3), the InitS of t],(x `2_3),(x `3_3)];
coherence
[[(x `1_3), the InitS of t],(x `2_3),(x `3_3)] is Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:]
proof end;
end;

:: deftheorem defines FirstTuringTran TURING_1:def 23 :
for s, t being TuringStr
for x being Tran-Goal of s holds FirstTuringTran (s,t,x) = [[(x `1_3), the InitS of t],(x `2_3),(x `3_3)];

definition
let s, t be TuringStr ;
let 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 :: TURING_1:def 24
[[ the AcceptS of s,(x `1_3)],(x `2_3),(x `3_3)];
coherence
[[ the AcceptS of s,(x `1_3)],(x `2_3),(x `3_3)] is Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:]
proof end;
end;

:: deftheorem defines SecondTuringTran TURING_1:def 24 :
for s, t being TuringStr
for x being Tran-Goal of t holds SecondTuringTran (s,t,x) = [[ the AcceptS of s,(x `1_3)],(x `2_3),(x `3_3)];

definition
let s, t be TuringStr ;
let x be Element of UnionSt (s,t);
:: original: `1
redefine func x `1 -> State of s;
coherence
x `1 is State of s
proof end;
:: original: `2
redefine func x `2 -> State of t;
coherence
x `2 is State of t
proof end;
end;

definition
let s, t be TuringStr ;
let x be Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):];
func FirstTuringState x -> State of s equals :: TURING_1:def 25
(x `1) `1 ;
correctness
coherence
(x `1) `1 is State of s;
;
func SecondTuringState x -> State of t equals :: TURING_1:def 26
(x `1) `2 ;
correctness
coherence
(x `1) `2 is State of t;
;
end;

:: deftheorem defines FirstTuringState TURING_1:def 25 :
for s, t being TuringStr
for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds FirstTuringState x = (x `1) `1 ;

:: deftheorem defines SecondTuringState TURING_1:def 26 :
for s, t being TuringStr
for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds SecondTuringState x = (x `1) `2 ;

definition
let X, Y, Z be non empty set ;
let x be Element of [:X,(Y \/ Z):];
given u being set , y being Element of Y such that A1: x = [u,y] ;
func FirstTuringSymbol x -> Element of Y equals :Def27: :: TURING_1:def 27
x `2 ;
coherence
x `2 is Element of Y by A1;
end;

:: deftheorem Def27 defines FirstTuringSymbol TURING_1:def 27 :
for X, Y, Z being non empty set
for x being Element of [:X,(Y \/ Z):] st ex u being set ex y being Element of Y st x = [u,y] holds
FirstTuringSymbol x = x `2 ;

definition
let X, Y, Z be non empty set ;
let x be Element of [:X,(Y \/ Z):];
given u being set , z being Element of Z such that A1: x = [u,z] ;
func SecondTuringSymbol x -> Element of Z equals :Def28: :: TURING_1:def 28
x `2 ;
coherence
x `2 is Element of Z by A1;
end;

:: deftheorem Def28 defines SecondTuringSymbol TURING_1:def 28 :
for X, Y, Z being non empty set
for x being Element of [:X,(Y \/ Z):] st ex u being set ex z being Element of Z st x = [u,z] holds
SecondTuringSymbol x = x `2 ;

definition
let s, t be TuringStr ;
let 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: :: TURING_1:def 29
 FirstTuringTran (s,t,( the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)])) if ex p being State of s ex y being 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 ex y being Symbol of t st x = [[ the AcceptS of s,q],y]
otherwise [(x `1),(x `2),(- 1)];
consistency
for b1 being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:] st ex p being State of s ex y being Symbol of s st
( x = [[p, the InitS of t],y] & p <> the AcceptS of s ) & ex q being State of t ex y being Symbol of t st x = [[ the AcceptS of s,q],y] holds
( b1 = FirstTuringTran (s,t,( the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)])) iff b1 = SecondTuringTran (s,t,( the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)])) )
proof end;
coherence
( ( ex p being State of s ex y being Symbol of s st
( x = [[p, the InitS of t],y] & p <> the AcceptS of s ) implies FirstTuringTran (s,t,( the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)])) is Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:] ) & ( ex q being State of t ex y being Symbol of t st x = [[ the AcceptS of s,q],y] implies SecondTuringTran (s,t,( the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)])) is Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:] ) & ( ( for p being State of s
for y being Symbol of s holds
( not x = [[p, the InitS of t],y] or not p <> the AcceptS of s ) ) & ( for q being State of t
for y being Symbol of t holds not x = [[ the AcceptS of s,q],y] ) implies [(x `1),(x `2),(- 1)] is Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:] ) )
proof end;
end;

:: deftheorem Def29 defines Uniontran TURING_1:def 29 :
for s, t being TuringStr
for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds
( ( ex p being State of s ex y being Symbol of s st
( x = [[p, the InitS of t],y] & p <> the AcceptS of s ) implies Uniontran (s,t,x) = FirstTuringTran (s,t,( the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)])) ) & ( ex q being State of t ex y being Symbol of t st x = [[ the AcceptS of s,q],y] implies Uniontran (s,t,x) = SecondTuringTran (s,t,( the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)])) ) & ( ( for p being State of s
for y being Symbol of s holds
( not x = [[p, the InitS of t],y] or not p <> the AcceptS of s ) ) & ( for q being State of t
for y being Symbol of t holds not x = [[ the AcceptS of s,q],y] ) implies Uniontran (s,t,x) = [(x `1),(x `2),(- 1)] ) );

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: :: TURING_1:def 30
 for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds it . x = Uniontran (s,t,x);
existence
ex b1 being 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}:] st
for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds b1 . x = Uniontran (s,t,x)
proof end;
uniqueness
for b1, b2 being 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}:] st ( for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds b1 . x = Uniontran (s,t,x) ) & ( for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds b2 . x = Uniontran (s,t,x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def30 defines UnionTran TURING_1:def 30 :
for s, t being TuringStr
for b3 being 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}:] holds
( b3 = UnionTran (s,t) iff for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds b3 . x = Uniontran (s,t,x) );

definition
let T1, T2 be TuringStr ;
func T1 ';' T2 -> strict TuringStr means :Def31: :: TURING_1:def 31
( 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
ex b1 being strict TuringStr st
( the Symbols of b1 = the Symbols of T1 \/ the Symbols of T2 & the FStates of b1 = UnionSt (T1,T2) & the Tran of b1 = UnionTran (T1,T2) & the InitS of b1 = [ the InitS of T1, the InitS of T2] & the AcceptS of b1 = [ the AcceptS of T1, the AcceptS of T2] )
proof end;
uniqueness
for b1, b2 being strict TuringStr st the Symbols of b1 = the Symbols of T1 \/ the Symbols of T2 & the FStates of b1 = UnionSt (T1,T2) & the Tran of b1 = UnionTran (T1,T2) & the InitS of b1 = [ the InitS of T1, the InitS of T2] & the AcceptS of b1 = [ the AcceptS of T1, the AcceptS of T2] & the Symbols of b2 = the Symbols of T1 \/ the Symbols of T2 & the FStates of b2 = UnionSt (T1,T2) & the Tran of b2 = UnionTran (T1,T2) & the InitS of b2 = [ the InitS of T1, the InitS of T2] & the AcceptS of b2 = [ the AcceptS of T1, the AcceptS of T2] holds
b1 = b2 ;
end;

:: deftheorem Def31 defines ';' TURING_1:def 31 :
for T1, T2 being TuringStr
for b3 being strict TuringStr holds
( b3 = T1 ';' T2 iff ( the Symbols of b3 = the Symbols of T1 \/ the Symbols of T2 & the FStates of b3 = UnionSt (T1,T2) & the Tran of b3 = UnionTran (T1,T2) & the InitS of b3 = [ the InitS of T1, the InitS of T2] & the AcceptS of b3 = [ the AcceptS of T1, the AcceptS of T2] ) );

theorem Th43: :: TURING_1:43
for T1, T2 being TuringStr
for g being Tran-Goal of T1
for p being State of T1
for y being 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 end;

theorem Th44: :: TURING_1:44
for T1, T2 being TuringStr
for g being Tran-Goal of T2
for q being State of T2
for y being 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 end;

theorem Th45: :: TURING_1:45
for T1, T2 being TuringStr
for s1 being All-State of T1
for h being Element of NAT
for t being Tape of T1
for s2 being All-State of T2
for s3 being 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 end;

theorem :: TURING_1:46
for tm1, tm2 being TuringStr
for t being Tape of tm1 st the Symbols of tm1 = the Symbols of tm2 holds
t is Tape of (tm1 ';' tm2)
proof end;

theorem :: TURING_1:47
for tm1, tm2 being TuringStr
for t being 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 end;

theorem Th48: :: TURING_1:48
for f being FinSequence of NAT
for tm1, tm2 being TuringStr
for t1 being Tape of tm1
for t2 being Tape of tm2 st t1 = t2 & t1 storeData f holds
t2 storeData f
proof end;

Lm15: for s being All-State of ZeroTuring
for t being Tape of ZeroTuring
for head, n being 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 end;

theorem :: TURING_1:49
for s being All-State of (ZeroTuring ';' SuccTuring)
for t being Tape of ZeroTuring
for head, n being 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 end;