begin
:: deftheorem defines SegM TURING_1:def 1 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem
canceled;
theorem
canceled;
theorem
canceled;
:: deftheorem defines Prefix TURING_1:def 2 :
theorem Th7:
theorem Th8:
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 )
begin
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;
:: deftheorem defines Tape-Chg TURING_1:def 3 :
:: deftheorem defines offset TURING_1:def 4 :
:: deftheorem defines Head TURING_1:def 5 :
:: deftheorem defines TRAN TURING_1:def 6 :
:: deftheorem Def7 defines Following TURING_1:def 7 :
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:
(
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) ) )
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
end;
:: deftheorem Def8 defines Computation TURING_1:def 8 :
theorem
theorem
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
:: deftheorem Def9 defines Accept-Halt TURING_1:def 9 :
:: deftheorem Def10 defines Result TURING_1:def 10 :
theorem Th16:
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
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]
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
end;
:: deftheorem defines id TURING_1:def 11 :
definition
func Sum_Tran -> Function of
[:(SegM 5),{0 ,1}:],
[:(SegM 5),{0 ,1},{(- 1),0 ,1}:] equals
(((((((((id [:(SegM 5),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [0 ,0 ,1])) +* ([0 ,1] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) +* ([2,1] .--> [2,1,1])) +* ([2,0 ] .--> [3,0 ,(- 1)])) +* ([3,1] .--> [4,0 ,(- 1)])) +* ([4,1] .--> [4,1,(- 1)])) +* ([4,0 ] .--> [5,0 ,0 ]);
coherence
(((((((((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}:]
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:
(
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 ] )
:: deftheorem Def13 defines is_1_between TURING_1:def 13 :
:: deftheorem Def14 defines storeData TURING_1:def 14 :
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
begin
:: deftheorem Def15 defines SumTuring TURING_1:def 15 :
Lm1:
for n being Element of NAT st n <= 5 holds
n is State of SumTuring
theorem
canceled;
theorem Th28:
Lm2:
( 0 in the Symbols of SumTuring & 1 in the Symbols of SumTuring )
theorem Th29:
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 ))]
theorem Th30:
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]
theorem Th31:
:: deftheorem Def16 defines computes TURING_1:def 16 :
theorem Th32:
theorem
begin
definition
func Succ_Tran -> Function of
[:(SegM 4),{0 ,1}:],
[:(SegM 4),{0 ,1},{(- 1),0 ,1}:] equals
(((((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) +* ([2,0 ] .--> [3,0 ,(- 1)])) +* ([2,1] .--> [3,0 ,(- 1)])) +* ([3,1] .--> [3,1,(- 1)])) +* ([3,0 ] .--> [4,0 ,0 ]);
coherence
(((((((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}:]
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:
(
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 ] )
:: deftheorem Def18 defines SuccTuring TURING_1:def 18 :
Lm5:
for n being Element of NAT st n <= 4 holds
n is State of SuccTuring
Lm6:
( 0 in the Symbols of SuccTuring & 1 in the Symbols of SuccTuring )
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 ))]
theorem
canceled;
theorem Th36:
theorem
begin
definition
func Zero_Tran -> Function of
[:(SegM 4),{0 ,1}:],
[:(SegM 4),{0 ,1},{(- 1),0 ,1}:] equals
(((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},1) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [2,1,1])) +* ([2,0 ] .--> [3,0 ,(- 1)])) +* ([2,1] .--> [3,0 ,(- 1)])) +* ([3,1] .--> [4,1,(- 1)]);
coherence
(((((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}:]
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:
(
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)] )
:: deftheorem Def20 defines ZeroTuring TURING_1:def 20 :
Lm8:
for n being Element of NAT st n <= 4 holds
n is State of ZeroTuring
Lm9:
( 0 in the Symbols of ZeroTuring & 1 in the Symbols of ZeroTuring )
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 ))]
theorem Th39:
theorem
begin
definition
func U3(n)Tran -> Function of
[:(SegM 3),{0 ,1}:],
[:(SegM 3),{0 ,1},{(- 1),0 ,1}:] equals
(((((id [:(SegM 3),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,0 ,1])) +* ([1,0 ] .--> [2,0 ,1])) +* ([2,1] .--> [2,0 ,1])) +* ([2,0 ] .--> [3,0 ,0 ]);
coherence
(((((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}:]
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:
(
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 ] )
:: deftheorem Def22 defines U3(n)Turing TURING_1:def 22 :
Lm11:
for n being Element of NAT st n <= 3 holds
n is State of U3(n)Turing
Lm12:
( 0 in the Symbols of U3(n)Turing & 1 in the Symbols of U3(n)Turing )
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 ))]
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 ) )
theorem Th42:
theorem
begin
:: deftheorem defines UnionSt TURING_1:def 23 :
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
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
[[(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}:]
end;
:: deftheorem defines FirstTuringTran TURING_1:def 24 :
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
[[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}:]
end;
:: deftheorem defines SecondTuringTran TURING_1:def 25 :
:: deftheorem defines FirstTuringState TURING_1:def 26 :
:: deftheorem defines SecondTuringState TURING_1:def 27 :
:: deftheorem Def28 defines FirstTuringSymbol TURING_1:def 28 :
:: deftheorem Def29 defines SecondTuringSymbol TURING_1:def 29 :
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:
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)]) )
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}:] ) )
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:
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
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
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:
( 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] )
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 :
theorem Th48:
theorem Th49:
theorem Th50:
theorem
theorem
theorem Th53:
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 = head & (Result s) `3 storeData <*head,0 *> )
theorem