:: TURING_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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;

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

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

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

theorem Th1: :: TURING_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, n being Nat holds
( k in SegM n iff k <= n )
proof end;

theorem Th2: :: TURING_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function
for x, y, z, u, v being set st u <> x holds
(f +* ([x,y] .--> z)) . [u,v] = f . [u,v]
proof end;

theorem Th3: :: TURING_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function
for x, y, z, u, v being set st v <> y holds
(f +* ([x,y] .--> z)) . [u,v] = f . [u,v]
proof end;

theorem Th4: :: TURING_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, i2 being Element of INT holds Sum <*i1,i2*> = i1 + i2
proof end;

theorem Th5: :: TURING_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, i2, i3 being Element of INT holds Sum <*i1,i2,i3*> = (i1 + i2) + i3
proof end;

theorem Th6: :: TURING_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, i2, i3, i4 being Element of INT holds Sum <*i1,i2,i3,i4*> = ((i1 + i2) + i3) + i4
proof end;

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

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

theorem Th7: :: TURING_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being Nat holds
( Sum (Prefix <*x1,x2*>,1) = x1 & Sum (Prefix <*x1,x2*>,2) = x1 + x2 )
proof end;

theorem Th8: :: TURING_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3 being 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, 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 c1,the Symbols of c1:],[:the States of c1,the Symbols of c1,{(- 1),0,1}:];
sel InitS c1 -> Element of the States of c1;
sel AcceptS c1 -> Element of the States of c1;
end;

definition
let T be TuringStr ;
mode State of T is Element of the States 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 3
t +* (h .--> s);
coherence
t +* (h .--> s) is Tape of T
proof end;
end;

:: deftheorem defines Tape-Chg TURING_1:def 3 :
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 States of T,INT ,(Funcs INT ,the Symbols of T):];
mode Tran-Source of T is Element of [:the States of T,the Symbols of T:];
mode Tran-Goal of T is Element of [:the States 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 4
g `3 ;
coherence
g `3 is Integer
by ENUMSET1:def 1;
end;

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

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

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

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

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

definition
let T be TuringStr ;
let s be All-State of T;
func Following s -> All-State of T equals :Def7: :: TURING_1:def 7
[((TRAN s) `1 ),((Head s) + (offset (TRAN s))),(Tape-Chg (s `3 ),(Head s),((TRAN s) `2 ))] if s `1 <> the AcceptS of T
otherwise s;
correctness
coherence
( ( s `1 <> the AcceptS of T implies [((TRAN s) `1 ),((Head s) + (offset (TRAN s))),(Tape-Chg (s `3 ),(Head s),((TRAN s) `2 ))] is All-State of T ) & ( not s `1 <> 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 Def7 defines Following TURING_1:def 7 :
for T being TuringStr
for s being All-State of T holds
( ( s `1 <> the AcceptS of T implies Following s = [((TRAN s) `1 ),((Head s) + (offset (TRAN s))),(Tape-Chg (s `3 ),(Head s),((TRAN s) `2 ))] ) & ( not s `1 <> the AcceptS of T implies Following s = s ) );

definition
let T be TuringStr ;
let s be All-State of T;
func Computation s -> Function of NAT ,[:the States of T,INT ,(Funcs INT ,the Symbols of T):] means :Def8: :: TURING_1:def 8
( it . 0 = s & ( for i being Nat holds it . (i + 1) = Following (it . i) ) );
existence
ex b1 being Function of NAT ,[:the States 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 Function of NAT ,[:the States 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 Def8 defines Computation TURING_1:def 8 :
for T being TuringStr
for s being All-State of T
for b3 being Function of NAT ,[:the States 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:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TuringStr
for s being All-State of T st s `1 = the AcceptS of T holds
s = Following s by Def7;

theorem :: TURING_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TuringStr
for s being All-State of T holds (Computation s) . 0 = s by Def8;

theorem :: TURING_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Def8;

theorem Th12: :: TURING_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TuringStr
for s being All-State of T holds (Computation s) . 1 = Following s
proof end;

theorem Th13: :: TURING_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th14: :: TURING_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th15: :: TURING_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat
for T being TuringStr
for s being All-State of T st i <= j & ((Computation s) . i) `1 = 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 :Def9: :: TURING_1:def 9
ex k being Nat st ((Computation s) . k) `1 = the AcceptS of T;
end;

:: deftheorem Def9 defines Accept-Halt TURING_1:def 9 :
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 = 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 :Def10: :: TURING_1:def 10
ex k being Nat st
( it = (Computation s) . k & ((Computation s) . k) `1 = 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 = the AcceptS of T ) & ex k being Nat st
( b2 = (Computation s) . k & ((Computation s) . k) `1 = 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 = the AcceptS of T )
;
proof end;
end;

:: deftheorem Def10 defines Result TURING_1:def 10 :
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 = the AcceptS of T ) );

theorem Th16: :: TURING_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Nat st i < k holds
((Computation s) . i) `1 <> 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 11
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 11 :
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 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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 :Def13: :: TURING_1:def 13
( t . i = 0 & t . j = 0 & ( for k being Integer st i < k & k < j holds
t . k = 1 ) );
end;

:: deftheorem Def13 defines is_1_between TURING_1:def 13 :
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 FinSequence of NAT ;
let T be TuringStr ;
let t be Tape of T;
pred t storeData f means :Def14: :: TURING_1:def 14
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 Def14 defines storeData TURING_1:def 14 :
for f being FinSequence of NAT
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 Th18: :: TURING_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TuringStr
for t being Tape of T
for s, n being Nat st t storeData <*s,n*> holds
t is_1_between s,(s + n) + 2
proof end;

theorem Th19: :: TURING_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TuringStr
for t being Tape of T
for s, n being Nat st t is_1_between s,(s + n) + 2 holds
t storeData <*s,n*>
proof end;

theorem Th20: :: TURING_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TuringStr
for t being Tape of T
for s, n being 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 Th21: :: TURING_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TuringStr
for t being Tape of T
for s, n1, n2 being 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 Th22: :: TURING_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TuringStr
for t being Tape of T
for s, n1, n2 being 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 Th23: :: TURING_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of NAT
for s being Nat st len f >= 1 holds
( Sum (Prefix (<*s*> ^ f),1) = s & Sum (Prefix (<*s*> ^ f),2) = s + (f /. 1) )
proof end;

theorem Th24: :: TURING_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of NAT
for s being 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 Th25: :: TURING_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TuringStr
for t being Tape of T
for s being 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 Th26: :: TURING_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TuringStr
for t being Tape of T
for s being 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 :Def15: :: TURING_1:def 15
( the Symbols of it = {0,1} & the States 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 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 ) );

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

theorem Th27: :: TURING_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TuringStr
for s being All-State of T
for p, h, t being set st s = [p,h,t] holds
Head s = h by MCART_1:68;

theorem Th28: :: TURING_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th29: :: TURING_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ),((Head s) + (offset (TRAN s))),(Tape-Chg (s `3 ),(Head s),((TRAN s) `2 ))]
proof end;

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 ),((Head s) + (offset (TRAN s))),(Tape-Chg (s `3 ),(Head s),((TRAN s) `2 ))]
proof end;

theorem Th30: :: TURING_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TuringStr
for t being Tape of T
for h being Integer
for s being Symbol of T
for i being set 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 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 Th31: :: TURING_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being All-State of SumTuring
for t being Tape of SumTuring
for head, n1, n2 being Nat st s = [0,head,t] & t storeData <*head,n1,n2*> holds
( s is Accept-Halt & (Result s) `2 = 1 + head & (Result s) `3 storeData <*(1 + head),(n1 + n2)*> )
proof end;

definition
let T be TuringStr ;
let F be Function;
pred T computes F means :Def16: :: TURING_1:def 16
for s being All-State of T
for t being Tape of T
for a being 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 Nat st
( (Result s) `2 = b & y = F . x & (Result s) `3 storeData <*b*> ^ <*y*> ) );
end;

:: deftheorem Def16 defines computes TURING_1:def 16 :
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 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 Nat st
( (Result s) `2 = b & y = F . x & (Result s) `3 storeData <*b*> ^ <*y*> ) ) );

theorem Th32: :: TURING_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
dom [+] c= 2 -tuples_on NAT
proof end;

theorem :: TURING_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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 it = {0,1} & the States 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 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 ) );

Lm5: for n being 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 ),((Head s) + (offset (TRAN s))),(Tape-Chg (s `3 ),(Head s),((TRAN s) `2 ))]
proof end;

theorem :: TURING_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th36: :: TURING_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being All-State of SuccTuring
for t being Tape of SuccTuring
for head, n being Nat st s = [0,head,t] & t storeData <*head,n*> holds
( s is Accept-Halt & (Result s) `2 = head & (Result s) `3 storeData <*head,(n + 1)*> )
proof end;

theorem :: TURING_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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 it = {0,1} & the States 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 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 ) );

Lm8: for n being 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 ),((Head s) + (offset (TRAN s))),(Tape-Chg (s `3 ),(Head s),((TRAN s) `2 ))]
proof end;

theorem Th39: :: TURING_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being All-State of ZeroTuring
for t being Tape of ZeroTuring
for head being 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 = head & (Result s) `3 storeData <*head,0*> )
proof end;

theorem :: TURING_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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 it = {0,1} & the States 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 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 ) );

Lm11: for n being 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 ),((Head s) + (offset (TRAN s))),(Tape-Chg (s `3 ),(Head s),((TRAN s) `2 ))]
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 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 Th42: :: TURING_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being All-State of U3(n)Turing
for t being Tape of U3(n)Turing
for head being 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 = ((head + (f /. 1)) + (f /. 2)) + 4 & (Result s) `3 storeData <*(((head + (f /. 1)) + (f /. 2)) + 4),(f /. 3)*> )
proof end;

theorem :: TURING_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 23
[:the States of t1,{the InitS of t2}:] \/ [:{the AcceptS of t1},the States of t2:];
correctness
coherence
[:the States of t1,{the InitS of t2}:] \/ [:{the AcceptS of t1},the States of t2:] is non empty finite set
;
;
end;

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

theorem Th44: :: TURING_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th45: :: TURING_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s, t being TuringStr
for x being State of s holds [x,the InitS of t] in UnionSt s,t
proof end;

theorem Th46: :: TURING_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s, t being TuringStr
for x being State of t holds [the AcceptS of s,x] in UnionSt s,t
proof end;

theorem Th47: :: TURING_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 24
[[(x `1 ),the InitS of t],(x `2 ),(x `3 )];
coherence
[[(x `1 ),the InitS of t],(x `2 ),(x `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 24 :
for s, t being TuringStr
for x being Tran-Goal of s holds FirstTuringTran s,t,x = [[(x `1 ),the InitS of t],(x `2 ),(x `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 25
[[the AcceptS of s,(x `1 )],(x `2 ),(x `3 )];
coherence
[[the AcceptS of s,(x `1 )],(x `2 ),(x `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 25 :
for s, t being TuringStr
for x being Tran-Goal of t holds SecondTuringTran s,t,x = [[the AcceptS of s,(x `1 )],(x `2 ),(x `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 26
(x `1 ) `1 ;
correctness
coherence
(x `1 ) `1 is State of s
;
;
func SecondTuringState x -> State of t equals :: TURING_1:def 27
(x `1 ) `2 ;
correctness
coherence
(x `1 ) `2 is State of t
;
;
end;

:: deftheorem defines FirstTuringState 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 FirstTuringState x = (x `1 ) `1 ;

:: deftheorem defines SecondTuringState TURING_1:def 27 :
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 :Def28: :: TURING_1:def 28
x `2 ;
coherence
x `2 is Element of Y
by A1, MCART_1:def 2;
end;

:: deftheorem Def28 defines FirstTuringSymbol 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 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 :Def29: :: TURING_1:def 29
x `2 ;
coherence
x `2 is Element of Z
by A1, MCART_1:def 2;
end;

:: deftheorem Def29 defines SecondTuringSymbol TURING_1:def 29 :
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 :Def30: :: TURING_1:def 30
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 Def30 defines Uniontran TURING_1:def 30 :
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 :Def31: :: TURING_1:def 31
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 Def31 defines UnionTran TURING_1:def 31 :
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 :Def32: :: TURING_1:def 32
( the Symbols of it = the Symbols of T1 \/ the Symbols of T2 & the States 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 States 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 States 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 States 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 Def32 defines ';' TURING_1:def 32 :
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 States 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 Th48: :: TURING_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ),the InitS of T2],(g `2 ),(g `3 )]
proof end;

theorem Th49: :: TURING_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )],(g `2 ),(g `3 )]
proof end;

theorem Th50: :: TURING_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T1, T2 being TuringStr
for s1 being All-State of T1
for h being 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 ),((Result s1) `3 )] & s3 = [the InitS of (T1 ';' T2),h,t] holds
( s3 is Accept-Halt & (Result s3) `2 = (Result s2) `2 & (Result s3) `3 = (Result s2) `3 )
proof end;

theorem :: TURING_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th53: :: TURING_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Nat st s = [0,head,t] & t storeData <*head,n*> holds
( s is Accept-Halt & (Result s) `2 = head & (Result s) `3 storeData <*head,0*> )
proof end;

theorem :: TURING_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being All-State of (ZeroTuring ';' SuccTuring )
for t being Tape of ZeroTuring
for head, n being Nat st s = [[0,0],head,t] & t storeData <*head,n*> holds
( s is Accept-Halt & (Result s) `2 = head & (Result s) `3 storeData <*head,1*> )
proof end;