begin
:: deftheorem defines SegM TURING_1:def 1 :
for n being natural number holds SegM n = { k where k is Element of NAT : k <= n } ;
theorem Th1:
theorem Th2:
theorem Th3:
theorem
canceled;
theorem
canceled;
theorem
canceled;
:: deftheorem TURING_1:def 2 :
canceled;
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,
FStates,
Tran,
InitS,
AcceptS #)
-> TuringStr ;
sel Symbols c1 -> non
empty finite set ;
sel FStates c1 -> non
empty finite set ;
sel Tran c1 -> Function of
[: the FStates of c1, the Symbols of c1:],
[: the FStates of c1, the Symbols of c1,{(- 1),0,1}:];
sel InitS c1 -> Element of the
FStates of
c1;
sel AcceptS c1 -> Element of the
FStates of
c1;
end;
:: 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);
:: deftheorem defines offset TURING_1:def 4 :
for T being TuringStr
for g being Tran-Goal of T holds offset g = g `3 ;
:: deftheorem defines Head TURING_1:def 5 :
for T being TuringStr
for s being All-State of T holds Head s = s `2 ;
:: 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))];
:: 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 FStates 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 FStates of T,INT,(Funcs (INT, the Symbols of T)):] st
( b1 . 0 = s & ( for i being Nat holds b1 . (i + 1) = Following (b1 . i) ) )
uniqueness
for b1, b2 being Function of NAT,[: the FStates of T,INT,(Funcs (INT, the Symbols of T)):] st b1 . 0 = s & ( for i being Nat holds b1 . (i + 1) = Following (b1 . i) ) & b2 . 0 = s & ( for i being Nat holds b2 . (i + 1) = Following (b2 . i) ) holds
b1 = b2
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 FStates of T,INT,(Funcs (INT, the Symbols of T)):] holds
( b3 = Computation s iff ( b3 . 0 = s & ( for i being Nat holds b3 . (i + 1) = Following (b3 . i) ) ) );
theorem
theorem
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
:: 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 Element of NAT st ((Computation s) . k) `1 = the AcceptS of T );
:: 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 Element of NAT st
( b3 = (Computation s) . k & ((Computation s) . k) `1 = the AcceptS of T ) );
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 :
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
(((((((((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 :
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 ) ) );
:: 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 Element of 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:
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 :
for b1 being strict TuringStr holds
( b1 = SumTuring iff ( the Symbols of b1 = {0,1} & the FStates of b1 = SegM 5 & the Tran of b1 = Sum_Tran & the InitS of b1 = 0 & the AcceptS of b1 = 5 ) );
Lm1:
for n being Element of NAT st n <= 5 holds
n is State of SumTuring
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 :
for T being TuringStr
for F being Function holds
( T computes F iff for s being All-State of T
for t being Tape of T
for a being Element of NAT
for x being FinSequence of NAT st x in dom F & s = [ the InitS of T,a,t] & t storeData <*a*> ^ x holds
( s is Accept-Halt & ex b, y being Element of NAT st
( (Result s) `2 = b & y = F . x & (Result s) `3 storeData <*b*> ^ <*y*> ) ) );
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 :
for b1 being strict TuringStr holds
( b1 = SuccTuring iff ( the Symbols of b1 = {0,1} & the FStates of b1 = SegM 4 & the Tran of b1 = Succ_Tran & the InitS of b1 = 0 & the AcceptS of b1 = 4 ) );
Lm5:
for n being Element of NAT st n <= 4 holds
n is State of SuccTuring
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 :
for b1 being strict TuringStr holds
( b1 = ZeroTuring iff ( the Symbols of b1 = {0,1} & the FStates of b1 = SegM 4 & the Tran of b1 = Zero_Tran & the InitS of b1 = 0 & the AcceptS of b1 = 4 ) );
Lm8:
for n being Element of NAT st n <= 4 holds
n is State of ZeroTuring
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 :
for b1 being strict TuringStr holds
( b1 = U3(n)Turing iff ( the Symbols of b1 = {0,1} & the FStates of b1 = SegM 3 & the Tran of b1 = U3(n)Tran & the InitS of b1 = 0 & the AcceptS of b1 = 3 ) );
Lm11:
for n being Element of NAT st n <= 3 holds
n is State of U3(n)Turing
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 :
for t1, t2 being TuringStr holds UnionSt (t1,t2) = [: the FStates of t1,{ the InitS of t2}:] \/ [:{ the AcceptS of t1}, the FStates of t2:];
theorem 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 :
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
[[ 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 :
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)];
:: 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 ;
:: 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 ;
:: 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:
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
FStates of
it = UnionSt (
T1,
T2) & the
Tran of
it = UnionTran (
T1,
T2) & the
InitS of
it = [ the InitS of T1, the InitS of T2] & the
AcceptS of
it = [ the AcceptS of T1, the AcceptS of T2] );
existence
ex b1 being strict TuringStr st
( the Symbols of b1 = the Symbols of T1 \/ the Symbols of T2 & the FStates of b1 = UnionSt (T1,T2) & the Tran of b1 = UnionTran (T1,T2) & the InitS of b1 = [ the InitS of T1, the InitS of T2] & the AcceptS of b1 = [ the AcceptS of T1, the AcceptS of T2] )
uniqueness
for b1, b2 being strict TuringStr st the Symbols of b1 = the Symbols of T1 \/ the Symbols of T2 & the FStates of b1 = UnionSt (T1,T2) & the Tran of b1 = UnionTran (T1,T2) & the InitS of b1 = [ the InitS of T1, the InitS of T2] & the AcceptS of b1 = [ the AcceptS of T1, the AcceptS of T2] & the Symbols of b2 = the Symbols of T1 \/ the Symbols of T2 & the FStates of b2 = UnionSt (T1,T2) & the Tran of b2 = UnionTran (T1,T2) & the InitS of b2 = [ the InitS of T1, the InitS of T2] & the AcceptS of b2 = [ the AcceptS of T1, the AcceptS of T2] holds
b1 = b2
;
end;
:: deftheorem 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 FStates of b3 = UnionSt (T1,T2) & the Tran of b3 = UnionTran (T1,T2) & the InitS of b3 = [ the InitS of T1, the InitS of T2] & the AcceptS of b3 = [ the AcceptS of T1, the AcceptS of T2] ) );
theorem 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