:: TURING_1 semantic presentation

definition
let c1, c2 be non empty set ;
let c3 be Function of c1,c2;
let c4 be PartFunc of c1,c2;
redefine func +* as c3 +* c4 -> Function of a1,a2;
coherence
c3 +* c4 is Function of c1,c2
proof end;
end;

definition
let c1, c2 be non empty set ;
let c3 be Element of c1;
let c4 be Element of c2;
redefine func .--> as c3 .--> c4 -> PartFunc of a1,a2;
coherence
c3 .--> c4 is PartFunc of c1,c2
proof end;
end;

definition
let c1 be natural number ;
func SegM c1 -> Subset of NAT equals :: TURING_1:def 1
{ b1 where B is Nat : b1 <= a1 } ;
coherence
{ b1 where B is Nat : b1 <= c1 } is Subset of NAT
proof end;
end;

:: deftheorem Def1 defines SegM TURING_1:def 1 :
for b1 being natural number holds SegM b1 = { b2 where B is Nat : b2 <= b1 } ;

registration
let c1 be natural number ;
cluster SegM a1 -> non empty finite ;
coherence
( SegM c1 is finite & not SegM c1 is empty )
proof end;
end;

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

theorem Th2: :: TURING_1:2
for b1 being Function
for b2, b3, b4, b5, b6 being set st b5 <> b2 holds
(b1 +* ([b2,b3] .--> b4)) . [b5,b6] = b1 . [b5,b6]
proof end;

theorem Th3: :: TURING_1:3
for b1 being Function
for b2, b3, b4, b5, b6 being set st b6 <> b3 holds
(b1 +* ([b2,b3] .--> b4)) . [b5,b6] = b1 . [b5,b6]
proof end;

theorem Th4: :: TURING_1:4
for b1, b2 being Element of INT holds Sum <*b1,b2*> = b1 + b2
proof end;

theorem Th5: :: TURING_1:5
for b1, b2, b3 being Element of INT holds Sum <*b1,b2,b3*> = (b1 + b2) + b3
proof end;

theorem Th6: :: TURING_1:6
for b1, b2, b3, b4 being Element of INT holds Sum <*b1,b2,b3,b4*> = ((b1 + b2) + b3) + b4
proof end;

definition
let c1 be FinSequence of NAT ;
let c2 be Nat;
func Prefix c1,c2 -> FinSequence of INT equals :: TURING_1:def 2
a1 | (Seg a2);
coherence
c1 | (Seg c2) is FinSequence of INT
proof end;
end;

:: deftheorem Def2 defines Prefix TURING_1:def 2 :
for b1 being FinSequence of NAT
for b2 being Nat holds Prefix b1,b2 = b1 | (Seg b2);

theorem Th7: :: TURING_1:7
for b1, b2 being Nat holds
( Sum (Prefix <*b1,b2*>,1) = b1 & Sum (Prefix <*b1,b2*>,2) = b1 + b2 )
proof end;

theorem Th8: :: TURING_1:8
for b1, b2, b3 being Nat holds
( Sum (Prefix <*b1,b2,b3*>,1) = b1 & Sum (Prefix <*b1,b2,b3*>,2) = b1 + b2 & Sum (Prefix <*b1,b2,b3*>,3) = (b1 + b2) + b3 )
proof end;

definition
attr a1 is strict;
struct TuringStr -> ;
aggr TuringStr(# Symbols, States, Tran, InitS, AcceptS #) -> TuringStr ;
sel Symbols c1 -> non empty finite set ;
sel States c1 -> non empty finite set ;
sel Tran c1 -> Function of [:the States of a1,the Symbols of a1:],[:the States of a1,the Symbols of a1,{(- 1),0,1}:];
sel InitS c1 -> Element of the States of a1;
sel AcceptS c1 -> Element of the States of a1;
end;

definition
let c1 be TuringStr ;
mode State of a1 is Element of the States of a1;
mode Tape of a1 is Element of Funcs INT ,the Symbols of a1;
mode Symbol of a1 is Element of the Symbols of a1;
end;

definition
let c1 be TuringStr ;
let c2 be Tape of c1;
let c3 be Integer;
let c4 be Symbol of c1;
func Tape-Chg c2,c3,c4 -> Tape of a1 equals :: TURING_1:def 3
a2 +* (a3 .--> a4);
coherence
c2 +* (c3 .--> c4) is Tape of c1
proof end;
end;

:: deftheorem Def3 defines Tape-Chg TURING_1:def 3 :
for b1 being TuringStr
for b2 being Tape of b1
for b3 being Integer
for b4 being Symbol of b1 holds Tape-Chg b2,b3,b4 = b2 +* (b3 .--> b4);

definition
let c1 be TuringStr ;
mode All-State of a1 is Element of [:the States of a1,INT ,(Funcs INT ,the Symbols of a1):];
mode Tran-Source of a1 is Element of [:the States of a1,the Symbols of a1:];
mode Tran-Goal of a1 is Element of [:the States of a1,the Symbols of a1,{(- 1),0,1}:];
end;

definition
let c1 be TuringStr ;
let c2 be Tran-Goal of c1;
func offset c2 -> Integer equals :: TURING_1:def 4
a2 `3 ;
coherence
c2 `3 is Integer by ENUMSET1:def 1;
end;

:: deftheorem Def4 defines offset TURING_1:def 4 :
for b1 being TuringStr
for b2 being Tran-Goal of b1 holds offset b2 = b2 `3 ;

definition
let c1 be TuringStr ;
let c2 be All-State of c1;
func Head c2 -> Integer equals :: TURING_1:def 5
a2 `2 ;
coherence
c2 `2 is Integer ;
end;

:: deftheorem Def5 defines Head TURING_1:def 5 :
for b1 being TuringStr
for b2 being All-State of b1 holds Head b2 = b2 `2 ;

definition
let c1 be TuringStr ;
let c2 be All-State of c1;
func TRAN c2 -> Tran-Goal of a1 equals :: TURING_1:def 6
the Tran of a1 . [(a2 `1 ),((a2 `3 ) . (Head a2))];
correctness
coherence
the Tran of c1 . [(c2 `1 ),((c2 `3 ) . (Head c2))] is Tran-Goal of c1;
proof end;
end;

:: deftheorem Def6 defines TRAN TURING_1:def 6 :
for b1 being TuringStr
for b2 being All-State of b1 holds TRAN b2 = the Tran of b1 . [(b2 `1 ),((b2 `3 ) . (Head b2))];

definition
let c1 be TuringStr ;
let c2 be All-State of c1;
func Following c2 -> All-State of a1 equals :Def7: :: TURING_1:def 7
[((TRAN a2) `1 ),((Head a2) + (offset (TRAN a2))),(Tape-Chg (a2 `3 ),(Head a2),((TRAN a2) `2 ))] if a2 `1 <> the AcceptS of a1
otherwise a2;
correctness
coherence
( ( c2 `1 <> the AcceptS of c1 implies [((TRAN c2) `1 ),((Head c2) + (offset (TRAN c2))),(Tape-Chg (c2 `3 ),(Head c2),((TRAN c2) `2 ))] is All-State of c1 ) & ( not c2 `1 <> the AcceptS of c1 implies c2 is All-State of c1 ) );
consistency
for b1 being All-State of c1 holds verum;
proof end;
end;

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

definition
let c1 be TuringStr ;
let c2 be All-State of c1;
func Computation c2 -> Function of NAT ,[:the States of a1,INT ,(Funcs INT ,the Symbols of a1):] means :Def8: :: TURING_1:def 8
( a3 . 0 = a2 & ( for b1 being Nat holds a3 . (b1 + 1) = Following (a3 . b1) ) );
existence
ex b1 being Function of NAT ,[:the States of c1,INT ,(Funcs INT ,the Symbols of c1):] st
( b1 . 0 = c2 & ( for b2 being Nat holds b1 . (b2 + 1) = Following (b1 . b2) ) )
proof end;
uniqueness
for b1, b2 being Function of NAT ,[:the States of c1,INT ,(Funcs INT ,the Symbols of c1):] st b1 . 0 = c2 & ( for b3 being Nat holds b1 . (b3 + 1) = Following (b1 . b3) ) & b2 . 0 = c2 & ( for b3 being Nat holds b2 . (b3 + 1) = Following (b2 . b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Computation TURING_1:def 8 :
for b1 being TuringStr
for b2 being All-State of b1
for b3 being Function of NAT ,[:the States of b1,INT ,(Funcs INT ,the Symbols of b1):] holds
( b3 = Computation b2 iff ( b3 . 0 = b2 & ( for b4 being Nat holds b3 . (b4 + 1) = Following (b3 . b4) ) ) );

theorem Th9: :: TURING_1:9
for b1 being TuringStr
for b2 being All-State of b1 st b2 `1 = the AcceptS of b1 holds
b2 = Following b2 by Def7;

theorem Th10: :: TURING_1:10
for b1 being TuringStr
for b2 being All-State of b1 holds (Computation b2) . 0 = b2 by Def8;

theorem Th11: :: TURING_1:11
for b1 being Nat
for b2 being TuringStr
for b3 being All-State of b2 holds (Computation b3) . (b1 + 1) = Following ((Computation b3) . b1) by Def8;

theorem Th12: :: TURING_1:12
for b1 being TuringStr
for b2 being All-State of b1 holds (Computation b2) . 1 = Following b2
proof end;

theorem Th13: :: TURING_1:13
for b1, b2 being Nat
for b3 being TuringStr
for b4 being All-State of b3 holds (Computation b4) . (b1 + b2) = (Computation ((Computation b4) . b1)) . b2
proof end;

theorem Th14: :: TURING_1:14
for b1, b2 being Nat
for b3 being TuringStr
for b4 being All-State of b3 st b1 <= b2 & Following ((Computation b4) . b1) = (Computation b4) . b1 holds
(Computation b4) . b2 = (Computation b4) . b1
proof end;

theorem Th15: :: TURING_1:15
for b1, b2 being Nat
for b3 being TuringStr
for b4 being All-State of b3 st b1 <= b2 & ((Computation b4) . b1) `1 = the AcceptS of b3 holds
(Computation b4) . b2 = (Computation b4) . b1
proof end;

definition
let c1 be TuringStr ;
let c2 be All-State of c1;
attr a2 is Accept-Halt means :Def9: :: TURING_1:def 9
ex b1 being Nat st ((Computation a2) . b1) `1 = the AcceptS of a1;
end;

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

definition
let c1 be TuringStr ;
let c2 be All-State of c1;
assume E16: c2 is Accept-Halt ;
func Result c2 -> All-State of a1 means :Def10: :: TURING_1:def 10
ex b1 being Nat st
( a3 = (Computation a2) . b1 & ((Computation a2) . b1) `1 = the AcceptS of a1 );
uniqueness
for b1, b2 being All-State of c1 st ex b3 being Nat st
( b1 = (Computation c2) . b3 & ((Computation c2) . b3) `1 = the AcceptS of c1 ) & ex b3 being Nat st
( b2 = (Computation c2) . b3 & ((Computation c2) . b3) `1 = the AcceptS of c1 ) holds
b1 = b2
proof end;
correctness
existence
ex b1 being All-State of c1ex b2 being Nat st
( b1 = (Computation c2) . b2 & ((Computation c2) . b2) `1 = the AcceptS of c1 );
proof end;
end;

:: deftheorem Def10 defines Result TURING_1:def 10 :
for b1 being TuringStr
for b2 being All-State of b1 st b2 is Accept-Halt holds
for b3 being All-State of b1 holds
( b3 = Result b2 iff ex b4 being Nat st
( b3 = (Computation b2) . b4 & ((Computation b2) . b4) `1 = the AcceptS of b1 ) );

theorem Th16: :: TURING_1:16
for b1 being TuringStr
for b2 being All-State of b1 st b2 is Accept-Halt holds
ex b3 being Nat st
( ((Computation b2) . b3) `1 = the AcceptS of b1 & Result b2 = (Computation b2) . b3 & ( for b4 being Nat st b4 < b3 holds
((Computation b2) . b4) `1 <> the AcceptS of b1 ) )
proof end;

definition
let c1, c2 be non empty set ;
let c3 be set ;
assume E18: c3 in c2 ;
func id c1,c2,c3 -> Function of a1,[:a1,a2:] means :: TURING_1:def 11
for b1 being Element of a1 holds a4 . b1 = [b1,a3];
existence
ex b1 being Function of c1,[:c1,c2:] st
for b2 being Element of c1 holds b1 . b2 = [b2,c3]
proof end;
uniqueness
for b1, b2 being Function of c1,[:c1,c2:] st ( for b3 being Element of c1 holds b1 . b3 = [b3,c3] ) & ( for b3 being Element of c1 holds b2 . b3 = [b3,c3] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines id TURING_1:def 11 :
for b1, b2 being non empty set
for b3 being set st b3 in b2 holds
for b4 being Function of b1,[:b1,b2:] holds
( b4 = id b1,b2,b3 iff for b5 being Element of b1 holds b4 . b5 = [b5,b3] );

definition
func Sum_Tran -> Function of [:(SegM 5),{0,1}:],[:(SegM 5),{0,1},{(- 1),0,1}:] equals :: TURING_1:def 12
(((((((((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 Def12 defines Sum_Tran TURING_1:def 12 :
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 Th17: :: TURING_1:17
( 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 c1 be TuringStr ;
let c2 be Tape of c1;
let c3, c4 be Integer;
pred c2 is_1_between c3,c4 means :Def13: :: TURING_1:def 13
( a2 . a3 = 0 & a2 . a4 = 0 & ( for b1 being Integer st a3 < b1 & b1 < a4 holds
a2 . b1 = 1 ) );
end;

:: deftheorem Def13 defines is_1_between TURING_1:def 13 :
for b1 being TuringStr
for b2 being Tape of b1
for b3, b4 being Integer holds
( b2 is_1_between b3,b4 iff ( b2 . b3 = 0 & b2 . b4 = 0 & ( for b5 being Integer st b3 < b5 & b5 < b4 holds
b2 . b5 = 1 ) ) );

definition
let c1 be FinSequence of NAT ;
let c2 be TuringStr ;
let c3 be Tape of c2;
pred c3 storeData c1 means :Def14: :: TURING_1:def 14
for b1 being Nat st 1 <= b1 & b1 < len a1 holds
a3 is_1_between (Sum (Prefix a1,b1)) + (2 * (b1 - 1)),(Sum (Prefix a1,(b1 + 1))) + (2 * b1);
end;

:: deftheorem Def14 defines storeData TURING_1:def 14 :
for b1 being FinSequence of NAT
for b2 being TuringStr
for b3 being Tape of b2 holds
( b3 storeData b1 iff for b4 being Nat st 1 <= b4 & b4 < len b1 holds
b3 is_1_between (Sum (Prefix b1,b4)) + (2 * (b4 - 1)),(Sum (Prefix b1,(b4 + 1))) + (2 * b4) );

theorem Th18: :: TURING_1:18
for b1 being TuringStr
for b2 being Tape of b1
for b3, b4 being Nat st b2 storeData <*b3,b4*> holds
b2 is_1_between b3,(b3 + b4) + 2
proof end;

theorem Th19: :: TURING_1:19
for b1 being TuringStr
for b2 being Tape of b1
for b3, b4 being Nat st b2 is_1_between b3,(b3 + b4) + 2 holds
b2 storeData <*b3,b4*>
proof end;

theorem Th20: :: TURING_1:20
for b1 being TuringStr
for b2 being Tape of b1
for b3, b4 being Nat st b2 storeData <*b3,b4*> holds
( b2 . b3 = 0 & b2 . ((b3 + b4) + 2) = 0 & ( for b5 being Integer st b3 < b5 & b5 < (b3 + b4) + 2 holds
b2 . b5 = 1 ) )
proof end;

theorem Th21: :: TURING_1:21
for b1 being TuringStr
for b2 being Tape of b1
for b3, b4, b5 being Nat st b2 storeData <*b3,b4,b5*> holds
( b2 is_1_between b3,(b3 + b4) + 2 & b2 is_1_between (b3 + b4) + 2,((b3 + b4) + b5) + 4 )
proof end;

theorem Th22: :: TURING_1:22
for b1 being TuringStr
for b2 being Tape of b1
for b3, b4, b5 being Nat st b2 storeData <*b3,b4,b5*> holds
( b2 . b3 = 0 & b2 . ((b3 + b4) + 2) = 0 & b2 . (((b3 + b4) + b5) + 4) = 0 & ( for b6 being Integer st b3 < b6 & b6 < (b3 + b4) + 2 holds
b2 . b6 = 1 ) & ( for b6 being Integer st (b3 + b4) + 2 < b6 & b6 < ((b3 + b4) + b5) + 4 holds
b2 . b6 = 1 ) )
proof end;

theorem Th23: :: TURING_1:23
for b1 being FinSequence of NAT
for b2 being Nat st len b1 >= 1 holds
( Sum (Prefix (<*b2*> ^ b1),1) = b2 & Sum (Prefix (<*b2*> ^ b1),2) = b2 + (b1 /. 1) )
proof end;

theorem Th24: :: TURING_1:24
for b1 being FinSequence of NAT
for b2 being Nat st len b1 >= 3 holds
( Sum (Prefix (<*b2*> ^ b1),1) = b2 & Sum (Prefix (<*b2*> ^ b1),2) = b2 + (b1 /. 1) & Sum (Prefix (<*b2*> ^ b1),3) = (b2 + (b1 /. 1)) + (b1 /. 2) & Sum (Prefix (<*b2*> ^ b1),4) = ((b2 + (b1 /. 1)) + (b1 /. 2)) + (b1 /. 3) )
proof end;

theorem Th25: :: TURING_1:25
for b1 being TuringStr
for b2 being Tape of b1
for b3 being Nat
for b4 being FinSequence of NAT st len b4 >= 1 & b2 storeData <*b3*> ^ b4 holds
b2 is_1_between b3,(b3 + (b4 /. 1)) + 2
proof end;

theorem Th26: :: TURING_1:26
for b1 being TuringStr
for b2 being Tape of b1
for b3 being Nat
for b4 being FinSequence of NAT st len b4 >= 3 & b2 storeData <*b3*> ^ b4 holds
( b2 is_1_between b3,(b3 + (b4 /. 1)) + 2 & b2 is_1_between (b3 + (b4 /. 1)) + 2,((b3 + (b4 /. 1)) + (b4 /. 2)) + 4 & b2 is_1_between ((b3 + (b4 /. 1)) + (b4 /. 2)) + 4,(((b3 + (b4 /. 1)) + (b4 /. 2)) + (b4 /. 3)) + 6 )
proof end;

definition
func SumTuring -> strict TuringStr means :Def15: :: TURING_1:def 15
( the Symbols of a1 = {0,1} & the States of a1 = SegM 5 & the Tran of a1 = Sum_Tran & the InitS of a1 = 0 & the AcceptS of a1 = 5 );
existence
ex b1 being strict TuringStr st
( the Symbols of b1 = {0,1} & the States 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 States 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 States 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 Def15 defines SumTuring TURING_1:def 15 :
for b1 being strict TuringStr holds
( b1 = SumTuring iff ( the Symbols of b1 = {0,1} & the States of b1 = SegM 5 & the Tran of b1 = Sum_Tran & the InitS of b1 = 0 & the AcceptS of b1 = 5 ) );

Lemma31: for b1 being Nat st b1 <= 5 holds
b1 is State of SumTuring
proof end;

theorem Th27: :: TURING_1:27
for b1 being TuringStr
for b2 being All-State of b1
for b3, b4, b5 being set st b2 = [b3,b4,b5] holds
Head b2 = b4 by MCART_1:68;

theorem Th28: :: TURING_1:28
for b1 being TuringStr
for b2 being Tape of b1
for b3 being Integer
for b4 being Symbol of b1 st b2 . b3 = b4 holds
Tape-Chg b2,b3,b4 = b2
proof end;

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

theorem Th29: :: TURING_1:29
for b1 being TuringStr
for b2 being All-State of b1
for b3, b4, b5 being set st b2 = [b3,b4,b5] & b3 <> the AcceptS of b1 holds
Following b2 = [((TRAN b2) `1 ),((Head b2) + (offset (TRAN b2))),(Tape-Chg (b2 `3 ),(Head b2),((TRAN b2) `2 ))]
proof end;

Lemma36: for b1 being All-State of SumTuring
for b2, b3, b4 being set st b1 = [b2,b3,b4] & b2 <> 5 holds
Following b1 = [((TRAN b1) `1 ),((Head b1) + (offset (TRAN b1))),(Tape-Chg (b1 `3 ),(Head b1),((TRAN b1) `2 ))]
proof end;

theorem Th30: :: TURING_1:30
for b1 being TuringStr
for b2 being Tape of b1
for b3 being Integer
for b4 being Symbol of b1
for b5 being set holds
( (Tape-Chg b2,b3,b4) . b3 = b4 & ( b5 <> b3 implies (Tape-Chg b2,b3,b4) . b5 = b2 . b5 ) )
proof end;

Lemma38: for b1 being TuringStr
for b2 being All-State of b1
for b3 being State of b1
for b4 being Element of INT
for b5 being Tape of b1
for b6, b7 being Nat st b7 = b4 & 1 is Symbol of b1 & b2 = [b3,b4,b5] & the Tran of b1 . [b3,1] = [b3,1,1] & b3 <> the AcceptS of b1 & ( for b8 being Integer st b7 <= b8 & b8 < b7 + b6 holds
b5 . b8 = 1 ) holds
(Computation b2) . b6 = [b3,(b7 + b6),b5]
proof end;

theorem Th31: :: TURING_1:31
for b1 being All-State of SumTuring
for b2 being Tape of SumTuring
for b3, b4, b5 being Nat st b1 = [0,b3,b2] & b2 storeData <*b3,b4,b5*> holds
( b1 is Accept-Halt & (Result b1) `2 = 1 + b3 & (Result b1) `3 storeData <*(1 + b3),(b4 + b5)*> )
proof end;

definition
let c1 be TuringStr ;
let c2 be Function;
pred c1 computes c2 means :Def16: :: TURING_1:def 16
for b1 being All-State of a1
for b2 being Tape of a1
for b3 being Nat
for b4 being FinSequence of NAT st b4 in dom a2 & b1 = [the InitS of a1,b3,b2] & b2 storeData <*b3*> ^ b4 holds
( b1 is Accept-Halt & ex b5, b6 being Nat st
( (Result b1) `2 = b5 & b6 = a2 . b4 & (Result b1) `3 storeData <*b5*> ^ <*b6*> ) );
end;

:: deftheorem Def16 defines computes TURING_1:def 16 :
for b1 being TuringStr
for b2 being Function holds
( b1 computes b2 iff for b3 being All-State of b1
for b4 being Tape of b1
for b5 being Nat
for b6 being FinSequence of NAT st b6 in dom b2 & b3 = [the InitS of b1,b5,b4] & b4 storeData <*b5*> ^ b6 holds
( b3 is Accept-Halt & ex b7, b8 being Nat st
( (Result b3) `2 = b7 & b8 = b2 . b6 & (Result b3) `3 storeData <*b7*> ^ <*b8*> ) ) );

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

theorem Th33: :: TURING_1:33
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 17
(((((((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 Def17 defines Succ_Tran TURING_1:def 17 :
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 Th34: :: TURING_1:34
( 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 :Def18: :: TURING_1:def 18
( the Symbols of a1 = {0,1} & the States of a1 = SegM 4 & the Tran of a1 = Succ_Tran & the InitS of a1 = 0 & the AcceptS of a1 = 4 );
existence
ex b1 being strict TuringStr st
( the Symbols of b1 = {0,1} & the States 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 States 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 States 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 Def18 defines SuccTuring TURING_1:def 18 :
for b1 being strict TuringStr holds
( b1 = SuccTuring iff ( the Symbols of b1 = {0,1} & the States of b1 = SegM 4 & the Tran of b1 = Succ_Tran & the InitS of b1 = 0 & the AcceptS of b1 = 4 ) );

Lemma44: for b1 being Nat st b1 <= 4 holds
b1 is State of SuccTuring
proof end;

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

Lemma46: for b1 being All-State of SuccTuring
for b2, b3, b4 being set st b1 = [b2,b3,b4] & b2 <> 4 holds
Following b1 = [((TRAN b1) `1 ),((Head b1) + (offset (TRAN b1))),(Tape-Chg (b1 `3 ),(Head b1),((TRAN b1) `2 ))]
proof end;

theorem Th35: :: TURING_1:35
canceled;

theorem Th36: :: TURING_1:36
for b1 being All-State of SuccTuring
for b2 being Tape of SuccTuring
for b3, b4 being Nat st b1 = [0,b3,b2] & b2 storeData <*b3,b4*> holds
( b1 is Accept-Halt & (Result b1) `2 = b3 & (Result b1) `3 storeData <*b3,(b4 + 1)*> )
proof end;

theorem Th37: :: TURING_1:37
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 19
(((((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 Def19 defines Zero_Tran TURING_1:def 19 :
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 Th38: :: TURING_1:38
( 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 :Def20: :: TURING_1:def 20
( the Symbols of a1 = {0,1} & the States of a1 = SegM 4 & the Tran of a1 = Zero_Tran & the InitS of a1 = 0 & the AcceptS of a1 = 4 );
existence
ex b1 being strict TuringStr st
( the Symbols of b1 = {0,1} & the States 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 States 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 States 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 Def20 defines ZeroTuring TURING_1:def 20 :
for b1 being strict TuringStr holds
( b1 = ZeroTuring iff ( the Symbols of b1 = {0,1} & the States of b1 = SegM 4 & the Tran of b1 = Zero_Tran & the InitS of b1 = 0 & the AcceptS of b1 = 4 ) );

Lemma50: for b1 being Nat st b1 <= 4 holds
b1 is State of ZeroTuring
proof end;

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

Lemma52: for b1 being All-State of ZeroTuring
for b2, b3, b4 being set st b1 = [b2,b3,b4] & b2 <> 4 holds
Following b1 = [((TRAN b1) `1 ),((Head b1) + (offset (TRAN b1))),(Tape-Chg (b1 `3 ),(Head b1),((TRAN b1) `2 ))]
proof end;

theorem Th39: :: TURING_1:39
for b1 being All-State of ZeroTuring
for b2 being Tape of ZeroTuring
for b3 being Nat
for b4 being FinSequence of NAT st len b4 >= 1 & b1 = [0,b3,b2] & b2 storeData <*b3*> ^ b4 holds
( b1 is Accept-Halt & (Result b1) `2 = b3 & (Result b1) `3 storeData <*b3,0*> )
proof end;

theorem Th40: :: TURING_1:40
for b1 being Nat st b1 >= 1 holds
ZeroTuring computes b1 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 21
(((((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 Def21 defines U3(n)Tran TURING_1:def 21 :
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 Th41: :: TURING_1:41
( 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 :Def22: :: TURING_1:def 22
( the Symbols of a1 = {0,1} & the States of a1 = SegM 3 & the Tran of a1 = U3(n)Tran & the InitS of a1 = 0 & the AcceptS of a1 = 3 );
existence
ex b1 being strict TuringStr st
( the Symbols of b1 = {0,1} & the States 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 States 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 States 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 Def22 defines U3(n)Turing TURING_1:def 22 :
for b1 being strict TuringStr holds
( b1 = U3(n)Turing iff ( the Symbols of b1 = {0,1} & the States of b1 = SegM 3 & the Tran of b1 = U3(n)Tran & the InitS of b1 = 0 & the AcceptS of b1 = 3 ) );

Lemma56: for b1 being Nat st b1 <= 3 holds
b1 is State of U3(n)Turing
proof end;

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

Lemma58: for b1 being All-State of U3(n)Turing
for b2, b3, b4 being set st b1 = [b2,b3,b4] & b2 <> 3 holds
Following b1 = [((TRAN b1) `1 ),((Head b1) + (offset (TRAN b1))),(Tape-Chg (b1 `3 ),(Head b1),((TRAN b1) `2 ))]
proof end;

Lemma59: for b1 being TuringStr
for b2 being All-State of b1
for b3 being State of b1
for b4 being Element of INT
for b5 being Tape of b1
for b6, b7 being Nat st b7 = b4 & 0 is Symbol of b1 & b2 = [b3,b4,b5] & the Tran of b1 . [b3,1] = [b3,0,1] & b3 <> the AcceptS of b1 & ( for b8 being Integer st b7 <= b8 & b8 < b7 + b6 holds
b5 . b8 = 1 ) holds
ex b8 being Tape of b1 st
( (Computation b2) . b6 = [b3,(b7 + b6),b8] & ( for b9 being Integer st b7 <= b9 & b9 < b7 + b6 holds
b8 . b9 = 0 ) & ( for b9 being Integer st ( b7 > b9 or b9 >= b7 + b6 ) holds
b8 . b9 = b5 . b9 ) )
proof end;

theorem Th42: :: TURING_1:42
for b1 being All-State of U3(n)Turing
for b2 being Tape of U3(n)Turing
for b3 being Nat
for b4 being FinSequence of NAT st len b4 >= 3 & b1 = [0,b3,b2] & b2 storeData <*b3*> ^ b4 holds
( b1 is Accept-Halt & (Result b1) `2 = ((b3 + (b4 /. 1)) + (b4 /. 2)) + 4 & (Result b1) `3 storeData <*(((b3 + (b4 /. 1)) + (b4 /. 2)) + 4),(b4 /. 3)*> )
proof end;

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

definition
let c1, c2 be TuringStr ;
func UnionSt c1,c2 -> non empty finite set equals :: TURING_1:def 23
[:the States of a1,{the InitS of a2}:] \/ [:{the AcceptS of a1},the States of a2:];
correctness
coherence
[:the States of c1,{the InitS of c2}:] \/ [:{the AcceptS of c1},the States of c2:] is non empty finite set ;
;
end;

:: deftheorem Def23 defines UnionSt TURING_1:def 23 :
for b1, b2 being TuringStr holds UnionSt b1,b2 = [:the States of b1,{the InitS of b2}:] \/ [:{the AcceptS of b1},the States of b2:];

theorem Th44: :: TURING_1:44
for b1, b2 being TuringStr holds
( [the InitS of b1,the InitS of b2] in UnionSt b1,b2 & [the AcceptS of b1,the AcceptS of b2] in UnionSt b1,b2 )
proof end;

theorem Th45: :: TURING_1:45
for b1, b2 being TuringStr
for b3 being State of b1 holds [b3,the InitS of b2] in UnionSt b1,b2
proof end;

theorem Th46: :: TURING_1:46
for b1, b2 being TuringStr
for b3 being State of b2 holds [the AcceptS of b1,b3] in UnionSt b1,b2
proof end;

theorem Th47: :: TURING_1:47
for b1, b2 being TuringStr
for b3 being Element of UnionSt b1,b2 ex b4 being State of b1ex b5 being State of b2 st b3 = [b4,b5]
proof end;

definition
let c1, c2 be TuringStr ;
let c3 be Tran-Goal of c1;
func FirstTuringTran c1,c2,c3 -> Element of [:(UnionSt a1,a2),(the Symbols of a1 \/ the Symbols of a2),{(- 1),0,1}:] equals :: TURING_1:def 24
[[(a3 `1 ),the InitS of a2],(a3 `2 ),(a3 `3 )];
coherence
[[(c3 `1 ),the InitS of c2],(c3 `2 ),(c3 `3 )] is Element of [:(UnionSt c1,c2),(the Symbols of c1 \/ the Symbols of c2),{(- 1),0,1}:]
proof end;
end;

:: deftheorem Def24 defines FirstTuringTran TURING_1:def 24 :
for b1, b2 being TuringStr
for b3 being Tran-Goal of b1 holds FirstTuringTran b1,b2,b3 = [[(b3 `1 ),the InitS of b2],(b3 `2 ),(b3 `3 )];

definition
let c1, c2 be TuringStr ;
let c3 be Tran-Goal of c2;
func SecondTuringTran c1,c2,c3 -> Element of [:(UnionSt a1,a2),(the Symbols of a1 \/ the Symbols of a2),{(- 1),0,1}:] equals :: TURING_1:def 25
[[the AcceptS of a1,(a3 `1 )],(a3 `2 ),(a3 `3 )];
coherence
[[the AcceptS of c1,(c3 `1 )],(c3 `2 ),(c3 `3 )] is Element of [:(UnionSt c1,c2),(the Symbols of c1 \/ the Symbols of c2),{(- 1),0,1}:]
proof end;
end;

:: deftheorem Def25 defines SecondTuringTran TURING_1:def 25 :
for b1, b2 being TuringStr
for b3 being Tran-Goal of b2 holds SecondTuringTran b1,b2,b3 = [[the AcceptS of b1,(b3 `1 )],(b3 `2 ),(b3 `3 )];

definition
let c1, c2 be TuringStr ;
let c3 be Element of UnionSt c1,c2;
redefine func `1 as c3 `1 -> State of a1;
coherence
c3 `1 is State of c1
proof end;
redefine func `2 as c3 `2 -> State of a2;
coherence
c3 `2 is State of c2
proof end;
end;

definition
let c1, c2 be TuringStr ;
let c3 be Element of [:(UnionSt c1,c2),(the Symbols of c1 \/ the Symbols of c2):];
func FirstTuringState c3 -> State of a1 equals :: TURING_1:def 26
(a3 `1 ) `1 ;
correctness
coherence
(c3 `1 ) `1 is State of c1;
;
func SecondTuringState c3 -> State of a2 equals :: TURING_1:def 27
(a3 `1 ) `2 ;
correctness
coherence
(c3 `1 ) `2 is State of c2;
;
end;

:: deftheorem Def26 defines FirstTuringState TURING_1:def 26 :
for b1, b2 being TuringStr
for b3 being Element of [:(UnionSt b1,b2),(the Symbols of b1 \/ the Symbols of b2):] holds FirstTuringState b3 = (b3 `1 ) `1 ;

:: deftheorem Def27 defines SecondTuringState TURING_1:def 27 :
for b1, b2 being TuringStr
for b3 being Element of [:(UnionSt b1,b2),(the Symbols of b1 \/ the Symbols of b2):] holds SecondTuringState b3 = (b3 `1 ) `2 ;

definition
let c1, c2, c3 be non empty set ;
let c4 be Element of [:c1,(c2 \/ c3):];
given c5 being set , c6 being Element of c2 such that E65: c4 = [c5,c6] ;
func FirstTuringSymbol c4 -> Element of a2 equals :Def28: :: TURING_1:def 28
a4 `2 ;
coherence
c4 `2 is Element of c2 by E65, MCART_1:def 2;
end;

:: deftheorem Def28 defines FirstTuringSymbol TURING_1:def 28 :
for b1, b2, b3 being non empty set
for b4 being Element of [:b1,(b2 \/ b3):] st ex b5 being set ex b6 being Element of b2 st b4 = [b5,b6] holds
FirstTuringSymbol b4 = b4 `2 ;

definition
let c1, c2, c3 be non empty set ;
let c4 be Element of [:c1,(c2 \/ c3):];
given c5 being set , c6 being Element of c3 such that E66: c4 = [c5,c6] ;
func SecondTuringSymbol c4 -> Element of a3 equals :Def29: :: TURING_1:def 29
a4 `2 ;
coherence
c4 `2 is Element of c3 by E66, MCART_1:def 2;
end;

:: deftheorem Def29 defines SecondTuringSymbol TURING_1:def 29 :
for b1, b2, b3 being non empty set
for b4 being Element of [:b1,(b2 \/ b3):] st ex b5 being set ex b6 being Element of b3 st b4 = [b5,b6] holds
SecondTuringSymbol b4 = b4 `2 ;

definition
let c1, c2 be TuringStr ;
let c3 be Element of [:(UnionSt c1,c2),(the Symbols of c1 \/ the Symbols of c2):];
func Uniontran c1,c2,c3 -> Element of [:(UnionSt a1,a2),(the Symbols of a1 \/ the Symbols of a2),{(- 1),0,1}:] equals :Def30: :: TURING_1:def 30
 FirstTuringTran a1,a2,(the Tran of a1 . [(FirstTuringState a3),(FirstTuringSymbol a3)]) if ex b1 being State of a1ex b2 being Symbol of a1 st
( a3 = [[b1,the InitS of a2],b2] & b1 <> the AcceptS of a1 )
SecondTuringTran a1,a2,(the Tran of a2 . [(SecondTuringState a3),(SecondTuringSymbol a3)]) if ex b1 being State of a2ex b2 being Symbol of a2 st a3 = [[the AcceptS of a1,b1],b2]
otherwise [(a3 `1 ),(a3 `2 ),(- 1)];
consistency
for b1 being Element of [:(UnionSt c1,c2),(the Symbols of c1 \/ the Symbols of c2),{(- 1),0,1}:] st ex b2 being State of c1ex b3 being Symbol of c1 st
( c3 = [[b2,the InitS of c2],b3] & b2 <> the AcceptS of c1 ) & ex b2 being State of c2ex b3 being Symbol of c2 st c3 = [[the AcceptS of c1,b2],b3] holds
( b1 = FirstTuringTran c1,c2,(the Tran of c1 . [(FirstTuringState c3),(FirstTuringSymbol c3)]) iff b1 = SecondTuringTran c1,c2,(the Tran of c2 . [(SecondTuringState c3),(SecondTuringSymbol c3)]) )
proof end;
coherence
( ( ex b1 being State of c1ex b2 being Symbol of c1 st
( c3 = [[b1,the InitS of c2],b2] & b1 <> the AcceptS of c1 ) implies FirstTuringTran c1,c2,(the Tran of c1 . [(FirstTuringState c3),(FirstTuringSymbol c3)]) is Element of [:(UnionSt c1,c2),(the Symbols of c1 \/ the Symbols of c2),{(- 1),0,1}:] ) & ( ex b1 being State of c2ex b2 being Symbol of c2 st c3 = [[the AcceptS of c1,b1],b2] implies SecondTuringTran c1,c2,(the Tran of c2 . [(SecondTuringState c3),(SecondTuringSymbol c3)]) is Element of [:(UnionSt c1,c2),(the Symbols of c1 \/ the Symbols of c2),{(- 1),0,1}:] ) & ( ( for b1 being State of c1
for b2 being Symbol of c1 holds
( not c3 = [[b1,the InitS of c2],b2] or not b1 <> the AcceptS of c1 ) ) & ( for b1 being State of c2
for b2 being Symbol of c2 holds not c3 = [[the AcceptS of c1,b1],b2] ) implies [(c3 `1 ),(c3 `2 ),(- 1)] is Element of [:(UnionSt c1,c2),(the Symbols of c1 \/ the Symbols of c2),{(- 1),0,1}:] ) )
proof end;
end;

:: deftheorem Def30 defines Uniontran TURING_1:def 30 :
for b1, b2 being TuringStr
for b3 being Element of [:(UnionSt b1,b2),(the Symbols of b1 \/ the Symbols of b2):] holds
( ( ex b4 being State of b1ex b5 being Symbol of b1 st
( b3 = [[b4,the InitS of b2],b5] & b4 <> the AcceptS of b1 ) implies Uniontran b1,b2,b3 = FirstTuringTran b1,b2,(the Tran of b1 . [(FirstTuringState b3),(FirstTuringSymbol b3)]) ) & ( ex b4 being State of b2ex b5 being Symbol of b2 st b3 = [[the AcceptS of b1,b4],b5] implies Uniontran b1,b2,b3 = SecondTuringTran b1,b2,(the Tran of b2 . [(SecondTuringState b3),(SecondTuringSymbol b3)]) ) & ( ( for b4 being State of b1
for b5 being Symbol of b1 holds
( not b3 = [[b4,the InitS of b2],b5] or not b4 <> the AcceptS of b1 ) ) & ( for b4 being State of b2
for b5 being Symbol of b2 holds not b3 = [[the AcceptS of b1,b4],b5] ) implies Uniontran b1,b2,b3 = [(b3 `1 ),(b3 `2 ),(- 1)] ) );

definition
let c1, c2 be TuringStr ;
func UnionTran c1,c2 -> Function of [:(UnionSt a1,a2),(the Symbols of a1 \/ the Symbols of a2):],[:(UnionSt a1,a2),(the Symbols of a1 \/ the Symbols of a2),{(- 1),0,1}:] means :Def31: :: TURING_1:def 31
for b1 being Element of [:(UnionSt a1,a2),(the Symbols of a1 \/ the Symbols of a2):] holds a3 . b1 = Uniontran a1,a2,b1;
existence
ex b1 being Function of [:(UnionSt c1,c2),(the Symbols of c1 \/ the Symbols of c2):],[:(UnionSt c1,c2),(the Symbols of c1 \/ the Symbols of c2),{(- 1),0,1}:] st
for b2 being Element of [:(UnionSt c1,c2),(the Symbols of c1 \/ the Symbols of c2):] holds b1 . b2 = Uniontran c1,c2,b2
proof end;
uniqueness
for b1, b2 being Function of [:(UnionSt c1,c2),(the Symbols of c1 \/ the Symbols of c2):],[:(UnionSt c1,c2),(the Symbols of c1 \/ the Symbols of c2),{(- 1),0,1}:] st ( for b3 being Element of [:(UnionSt c1,c2),(the Symbols of c1 \/ the Symbols of c2):] holds b1 . b3 = Uniontran c1,c2,b3 ) & ( for b3 being Element of [:(UnionSt c1,c2),(the Symbols of c1 \/ the Symbols of c2):] holds b2 . b3 = Uniontran c1,c2,b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def31 defines UnionTran TURING_1:def 31 :
for b1, b2 being TuringStr
for b3 being Function of [:(UnionSt b1,b2),(the Symbols of b1 \/ the Symbols of b2):],[:(UnionSt b1,b2),(the Symbols of b1 \/ the Symbols of b2),{(- 1),0,1}:] holds
( b3 = UnionTran b1,b2 iff for b4 being Element of [:(UnionSt b1,b2),(the Symbols of b1 \/ the Symbols of b2):] holds b3 . b4 = Uniontran b1,b2,b4 );

definition
let c1, c2 be TuringStr ;
func c1 ';' c2 -> strict TuringStr means :Def32: :: TURING_1:def 32
( the Symbols of a3 = the Symbols of a1 \/ the Symbols of a2 & the States of a3 = UnionSt a1,a2 & the Tran of a3 = UnionTran a1,a2 & the InitS of a3 = [the InitS of a1,the InitS of a2] & the AcceptS of a3 = [the AcceptS of a1,the AcceptS of a2] );
existence
ex b1 being strict TuringStr st
( the Symbols of b1 = the Symbols of c1 \/ the Symbols of c2 & the States of b1 = UnionSt c1,c2 & the Tran of b1 = UnionTran c1,c2 & the InitS of b1 = [the InitS of c1,the InitS of c2] & the AcceptS of b1 = [the AcceptS of c1,the AcceptS of c2] )
proof end;
uniqueness
for b1, b2 being strict TuringStr st the Symbols of b1 = the Symbols of c1 \/ the Symbols of c2 & the States of b1 = UnionSt c1,c2 & the Tran of b1 = UnionTran c1,c2 & the InitS of b1 = [the InitS of c1,the InitS of c2] & the AcceptS of b1 = [the AcceptS of c1,the AcceptS of c2] & the Symbols of b2 = the Symbols of c1 \/ the Symbols of c2 & the States of b2 = UnionSt c1,c2 & the Tran of b2 = UnionTran c1,c2 & the InitS of b2 = [the InitS of c1,the InitS of c2] & the AcceptS of b2 = [the AcceptS of c1,the AcceptS of c2] holds
b1 = b2 ;
end;

:: deftheorem Def32 defines ';' TURING_1:def 32 :
for b1, b2 being TuringStr
for b3 being strict TuringStr holds
( b3 = b1 ';' b2 iff ( the Symbols of b3 = the Symbols of b1 \/ the Symbols of b2 & the States of b3 = UnionSt b1,b2 & the Tran of b3 = UnionTran b1,b2 & the InitS of b3 = [the InitS of b1,the InitS of b2] & the AcceptS of b3 = [the AcceptS of b1,the AcceptS of b2] ) );

theorem Th48: :: TURING_1:48
for b1, b2 being TuringStr
for b3 being Tran-Goal of b1
for b4 being State of b1
for b5 being Symbol of b1 st b4 <> the AcceptS of b1 & b3 = the Tran of b1 . [b4,b5] holds
the Tran of (b1 ';' b2) . [[b4,the InitS of b2],b5] = [[(b3 `1 ),the InitS of b2],(b3 `2 ),(b3 `3 )]
proof end;

theorem Th49: :: TURING_1:49
for b1, b2 being TuringStr
for b3 being Tran-Goal of b2
for b4 being State of b2
for b5 being Symbol of b2 st b3 = the Tran of b2 . [b4,b5] holds
the Tran of (b1 ';' b2) . [[the AcceptS of b1,b4],b5] = [[the AcceptS of b1,(b3 `1 )],(b3 `2 ),(b3 `3 )]
proof end;

theorem Th50: :: TURING_1:50
for b1, b2 being TuringStr
for b3 being All-State of b1
for b4 being Nat
for b5 being Tape of b1
for b6 being All-State of b2
for b7 being All-State of (b1 ';' b2) st b3 is Accept-Halt & b3 = [the InitS of b1,b4,b5] & b6 is Accept-Halt & b6 = [the InitS of b2,((Result b3) `2 ),((Result b3) `3 )] & b7 = [the InitS of (b1 ';' b2),b4,b5] holds
( b7 is Accept-Halt & (Result b7) `2 = (Result b6) `2 & (Result b7) `3 = (Result b6) `3 )
proof end;

theorem Th51: :: TURING_1:51
for b1, b2 being TuringStr
for b3 being Tape of b1 st the Symbols of b1 = the Symbols of b2 holds
b3 is Tape of (b1 ';' b2)
proof end;

theorem Th52: :: TURING_1:52
for b1, b2 being TuringStr
for b3 being Tape of (b1 ';' b2) st the Symbols of b1 = the Symbols of b2 holds
( b3 is Tape of b1 & b3 is Tape of b2 )
proof end;

theorem Th53: :: TURING_1:53
for b1 being FinSequence of NAT
for b2, b3 being TuringStr
for b4 being Tape of b2
for b5 being Tape of b3 st b4 = b5 & b4 storeData b1 holds
b5 storeData b1
proof end;

Lemma74: for b1 being All-State of ZeroTuring
for b2 being Tape of ZeroTuring
for b3, b4 being Nat st b1 = [0,b3,b2] & b2 storeData <*b3,b4*> holds
( b1 is Accept-Halt & (Result b1) `2 = b3 & (Result b1) `3 storeData <*b3,0*> )
proof end;

theorem Th54: :: TURING_1:54
for b1 being All-State of (ZeroTuring ';' SuccTuring )
for b2 being Tape of ZeroTuring
for b3, b4 being Nat st b1 = [[0,0],b3,b2] & b2 storeData <*b3,b4*> holds
( b1 is Accept-Halt & (Result b1) `2 = b3 & (Result b1) `3 storeData <*b3,1*> )
proof end;