:: by Jingchao Chen and Yatsuka Nakamura

::

:: Received July 27, 2001

:: Copyright (c) 2001-2021 Association of Mizar Users

definition

let A, B be non empty set ;

let f be Function of A,B;

let g be PartFunc of A,B;

:: original: +*

redefine func f +* g -> Function of A,B;

coherence

f +* g is Function of A,B

end;
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;

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

end;
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;

definition

let n be Nat;

SegM n is Subset of NAT

for b_{1} being Subset of NAT holds

( b_{1} = SegM n iff b_{1} = { k where k is Nat : k <= n } )

end;
:: original: SegM

redefine func SegM n -> Subset of NAT equals :: TURING_1:def 1

{ k where k is Nat : k <= n } ;

coherence redefine func SegM n -> Subset of NAT equals :: TURING_1:def 1

{ k where k is Nat : k <= n } ;

SegM n is Subset of NAT

proof end;

compatibility for b

( b

proof end;

:: deftheorem defines SegM TURING_1:def 1 :

for n being Nat holds SegM n = { k where k is Nat : k <= n } ;

for n being Nat holds SegM n = { k where k is Nat : k <= n } ;

theorem Th2: :: TURING_1:2

for f being Function

for x, y, z, u, v being object st u <> x holds

(f +* ([x,y] .--> z)) . [u,v] = f . [u,v]

for x, y, z, u, v being object st u <> x holds

(f +* ([x,y] .--> z)) . [u,v] = f . [u,v]

proof end;

theorem Th3: :: TURING_1:3

for f being Function

for x, y, z, u, v being object st v <> y holds

(f +* ([x,y] .--> z)) . [u,v] = f . [u,v]

for x, y, z, u, v being object st v <> y holds

(f +* ([x,y] .--> z)) . [u,v] = f . [u,v]

proof end;

registration

let f be natural-valued FinSequence;

let n be Nat;

coherence

for b_{1} being FinSequence st b_{1} = Prefix (f,n) holds

b_{1} is INT -valued
;

end;
let n be Nat;

coherence

for b

b

theorem Th4: :: TURING_1:4

for x1, x2 being Element of NAT holds

( Sum (Prefix (<*x1,x2*>,1)) = x1 & Sum (Prefix (<*x1,x2*>,2)) = x1 + x2 )

( Sum (Prefix (<*x1,x2*>,1)) = x1 & Sum (Prefix (<*x1,x2*>,2)) = x1 + x2 )

proof end;

theorem Th5: :: TURING_1:5

for x1, x2, x3 being Element of NAT holds

( Sum (Prefix (<*x1,x2,x3*>,1)) = x1 & Sum (Prefix (<*x1,x2,x3*>,2)) = x1 + x2 & Sum (Prefix (<*x1,x2,x3*>,3)) = (x1 + x2) + x3 )

( 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 c_{1} is strict ;

struct TuringStr -> ;

aggr TuringStr(# Symbols, FStates, Tran, InitS, AcceptS #) -> TuringStr ;

sel Symbols c_{1} -> non empty finite set ;

sel FStates c_{1} -> non empty finite set ;

sel Tran c_{1} -> Function of [: the FStates of c_{1}, the Symbols of c_{1}:],[: the FStates of c_{1}, the Symbols of c_{1},{(- 1),0,1}:];

sel InitS c_{1} -> Element of the FStates of c_{1};

sel AcceptS c_{1} -> Element of the FStates of c_{1};

end;
struct TuringStr -> ;

aggr TuringStr(# Symbols, FStates, Tran, InitS, AcceptS #) -> TuringStr ;

sel Symbols c

sel FStates c

sel Tran c

sel InitS c

sel AcceptS c

definition

let T be TuringStr ;

mode State of T is Element of the FStates of T;

mode Tape of T is Element of Funcs (INT, the Symbols of T);

mode Symbol of T is Element of the Symbols of T;

end;
mode State of T is Element of the FStates of T;

mode Tape of T is Element of Funcs (INT, the Symbols of T);

mode Symbol of T is Element of the Symbols of T;

definition

let T be TuringStr ;

let t be Tape of T;

let h be Integer;

let s be Symbol of T;

coherence

t +* (h .--> s) is Tape of T

end;
let t be Tape of T;

let h be Integer;

let s be Symbol of T;

coherence

t +* (h .--> s) is Tape of T

proof end;

:: deftheorem defines Tape-Chg TURING_1:def 2 :

for T being TuringStr

for t being Tape of T

for h being Integer

for s being Symbol of T holds Tape-Chg (t,h,s) = t +* (h .--> s);

for T being TuringStr

for t being Tape of T

for h being Integer

for s being Symbol of T holds Tape-Chg (t,h,s) = t +* (h .--> s);

definition

let T be TuringStr ;

mode All-State of T is Element of [: the FStates of T,INT,(Funcs (INT, the Symbols of T)):];

mode Tran-Source of T is Element of [: the FStates of T, the Symbols of T:];

mode Tran-Goal of T is Element of [: the FStates of T, the Symbols of T,{(- 1),0,1}:];

end;
mode All-State of T is Element of [: the FStates of T,INT,(Funcs (INT, the Symbols of T)):];

mode Tran-Source of T is Element of [: the FStates of T, the Symbols of T:];

mode Tran-Goal of T is Element of [: the FStates of T, the Symbols of T,{(- 1),0,1}:];

definition
end;

:: deftheorem defines offset TURING_1:def 3 :

for T being TuringStr

for g being Tran-Goal of T holds offset g = g `3_3 ;

for T being TuringStr

for g being Tran-Goal of T holds offset g = g `3_3 ;

:: deftheorem defines Head TURING_1:def 4 :

for T being TuringStr

for s being All-State of T holds Head s = s `2_3 ;

for T being TuringStr

for s being All-State of T holds Head s = s `2_3 ;

definition

let T be TuringStr ;

let s be All-State of T;

coherence

the Tran of T . [(s `1_3),((s `3_3) . (Head s))] is Tran-Goal of T;

end;
let s be All-State of T;

func TRAN s -> Tran-Goal of T equals :: TURING_1:def 5

the Tran of T . [(s `1_3),((s `3_3) . (Head s))];

correctness the Tran of T . [(s `1_3),((s `3_3) . (Head s))];

coherence

the Tran of T . [(s `1_3),((s `3_3) . (Head s))] is Tran-Goal of T;

proof end;

:: deftheorem defines TRAN TURING_1:def 5 :

for T being TuringStr

for s being All-State of T holds TRAN s = the Tran of T . [(s `1_3),((s `3_3) . (Head s))];

for T being TuringStr

for s being All-State of T holds TRAN s = the Tran of T . [(s `1_3),((s `3_3) . (Head s))];

definition

let T be TuringStr ;

let s be All-State of T;

coherence

( ( s `1_3 <> the AcceptS of T implies [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))] is All-State of T ) & ( not s `1_3 <> the AcceptS of T implies s is All-State of T ) );

consistency

for b_{1} being All-State of T holds verum;

end;
let s be All-State of T;

func Following s -> All-State of T equals :Def6: :: TURING_1:def 6

[((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))] if s `1_3 <> the AcceptS of T

otherwise s;

correctness [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))] if s `1_3 <> the AcceptS of T

otherwise s;

coherence

( ( s `1_3 <> the AcceptS of T implies [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))] is All-State of T ) & ( not s `1_3 <> the AcceptS of T implies s is All-State of T ) );

consistency

for b

proof end;

:: deftheorem Def6 defines Following TURING_1:def 6 :

for T being TuringStr

for s being All-State of T holds

( ( s `1_3 <> the AcceptS of T implies Following s = [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))] ) & ( not s `1_3 <> the AcceptS of T implies Following s = s ) );

for T being TuringStr

for s being All-State of T holds

( ( s `1_3 <> the AcceptS of T implies Following s = [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))] ) & ( not s `1_3 <> the AcceptS of T implies Following s = s ) );

definition

let T be TuringStr ;

let s be All-State of T;

ex b_{1} being sequence of [: the FStates of T,INT,(Funcs (INT, the Symbols of T)):] st

( b_{1} . 0 = s & ( for i being Nat holds b_{1} . (i + 1) = Following (b_{1} . i) ) )

for b_{1}, b_{2} being sequence of [: the FStates of T,INT,(Funcs (INT, the Symbols of T)):] st b_{1} . 0 = s & ( for i being Nat holds b_{1} . (i + 1) = Following (b_{1} . i) ) & b_{2} . 0 = s & ( for i being Nat holds b_{2} . (i + 1) = Following (b_{2} . i) ) holds

b_{1} = b_{2}

end;
let s be All-State of T;

func Computation s -> sequence of [: the FStates of T,INT,(Funcs (INT, the Symbols of T)):] means :Def7: :: TURING_1:def 7

( it . 0 = s & ( for i being Nat holds it . (i + 1) = Following (it . i) ) );

existence ( it . 0 = s & ( for i being Nat holds it . (i + 1) = Following (it . i) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines Computation TURING_1:def 7 :

for T being TuringStr

for s being All-State of T

for b_{3} being sequence of [: the FStates of T,INT,(Funcs (INT, the Symbols of T)):] holds

( b_{3} = Computation s iff ( b_{3} . 0 = s & ( for i being Nat holds b_{3} . (i + 1) = Following (b_{3} . i) ) ) );

for T being TuringStr

for s being All-State of T

for b

( b

theorem :: TURING_1:6

theorem :: TURING_1:7

theorem :: TURING_1:8

theorem Th10: :: TURING_1:10

for i, k being Nat

for T being TuringStr

for s being All-State of T holds (Computation s) . (i + k) = (Computation ((Computation s) . i)) . k

for T being TuringStr

for s being All-State of T holds (Computation s) . (i + k) = (Computation ((Computation s) . i)) . k

proof end;

theorem Th11: :: TURING_1:11

for i, j being Nat

for T being TuringStr

for s being All-State of T st i <= j & Following ((Computation s) . i) = (Computation s) . i holds

(Computation s) . j = (Computation s) . i

for T being TuringStr

for s being All-State of T st i <= j & Following ((Computation s) . i) = (Computation s) . i holds

(Computation s) . j = (Computation s) . i

proof end;

theorem Th12: :: TURING_1:12

for i, j being Nat

for T being TuringStr

for s being All-State of T st i <= j & ((Computation s) . i) `1_3 = the AcceptS of T holds

(Computation s) . j = (Computation s) . i

for T being TuringStr

for s being All-State of T st i <= j & ((Computation s) . i) `1_3 = the AcceptS of T holds

(Computation s) . j = (Computation s) . i

proof end;

definition

let T be TuringStr ;

let s be All-State of T;

end;
let s be All-State of T;

attr s is Accept-Halt means :: TURING_1:def 8

ex k being Nat st ((Computation s) . k) `1_3 = the AcceptS of T;

ex k being Nat st ((Computation s) . k) `1_3 = the AcceptS of T;

:: deftheorem defines Accept-Halt TURING_1:def 8 :

for T being TuringStr

for s being All-State of T holds

( s is Accept-Halt iff ex k being Nat st ((Computation s) . k) `1_3 = the AcceptS of T );

for T being TuringStr

for s being All-State of T holds

( s is Accept-Halt iff ex k being Nat st ((Computation s) . k) `1_3 = the AcceptS of T );

definition

let T be TuringStr ;

let s be All-State of T;

assume A1: s is Accept-Halt ;

for b_{1}, b_{2} being All-State of T st ex k being Nat st

( b_{1} = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T ) & ex k being Nat st

( b_{2} = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T ) holds

b_{1} = b_{2}

existence

ex b_{1} being All-State of T ex k being Nat st

( b_{1} = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T );

by A1;

end;
let s be All-State of T;

assume A1: s is Accept-Halt ;

func Result s -> All-State of T means :Def9: :: TURING_1:def 9

ex k being Nat st

( it = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T );

uniqueness ex k being Nat st

( it = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T );

for b

( b

( b

b

proof end;

correctness existence

ex b

( b

by A1;

:: deftheorem Def9 defines Result TURING_1:def 9 :

for T being TuringStr

for s being All-State of T st s is Accept-Halt holds

for b_{3} being All-State of T holds

( b_{3} = Result s iff ex k being Nat st

( b_{3} = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T ) );

for T being TuringStr

for s being All-State of T st s is Accept-Halt holds

for b

( b

( b

theorem Th13: :: TURING_1:13

for T being TuringStr

for s being All-State of T st s is Accept-Halt holds

ex k being Nat st

( ((Computation s) . k) `1_3 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Nat st i < k holds

((Computation s) . i) `1_3 <> the AcceptS of T ) )

for s being All-State of T st s is Accept-Halt holds

ex k being Nat st

( ((Computation s) . k) `1_3 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Nat st i < k holds

((Computation s) . i) `1_3 <> the AcceptS of T ) )

proof end;

definition

let A, B be non empty set ;

let y be set ;

assume A1: y in B ;

ex b_{1} being Function of A,[:A,B:] st

for x being Element of A holds b_{1} . x = [x,y]

for b_{1}, b_{2} being Function of A,[:A,B:] st ( for x being Element of A holds b_{1} . x = [x,y] ) & ( for x being Element of A holds b_{2} . x = [x,y] ) holds

b_{1} = b_{2}

end;
let y be set ;

assume A1: y in B ;

func id (A,B,y) -> Function of A,[:A,B:] means :: TURING_1:def 10

for x being Element of A holds it . x = [x,y];

existence for x being Element of A holds it . x = [x,y];

ex b

for x being Element of A holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines id TURING_1:def 10 :

for A, B being non empty set

for y being set st y in B holds

for b_{4} being Function of A,[:A,B:] holds

( b_{4} = id (A,B,y) iff for x being Element of A holds b_{4} . x = [x,y] );

for A, B being non empty set

for y being set st y in B holds

for b

( b

definition

(((((((((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;

func Sum_Tran -> Function of [:(SegM 5),{0,1}:],[:(SegM 5),{0,1},{(- 1),0,1}:] equals :: TURING_1:def 11

(((((((((id ([:(SegM 5),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [0,0,1])) +* ([0,1] .--> [1,0,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0] .--> [2,1,1])) +* ([2,1] .--> [2,1,1])) +* ([2,0] .--> [3,0,(- 1)])) +* ([3,1] .--> [4,0,(- 1)])) +* ([4,1] .--> [4,1,(- 1)])) +* ([4,0] .--> [5,0,0]);

coherence (((((((((id ([:(SegM 5),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [0,0,1])) +* ([0,1] .--> [1,0,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0] .--> [2,1,1])) +* ([2,1] .--> [2,1,1])) +* ([2,0] .--> [3,0,(- 1)])) +* ([3,1] .--> [4,0,(- 1)])) +* ([4,1] .--> [4,1,(- 1)])) +* ([4,0] .--> [5,0,0]);

(((((((((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;

:: deftheorem defines Sum_Tran TURING_1:def 11 :

Sum_Tran = (((((((((id ([:(SegM 5),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [0,0,1])) +* ([0,1] .--> [1,0,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0] .--> [2,1,1])) +* ([2,1] .--> [2,1,1])) +* ([2,0] .--> [3,0,(- 1)])) +* ([3,1] .--> [4,0,(- 1)])) +* ([4,1] .--> [4,1,(- 1)])) +* ([4,0] .--> [5,0,0]);

Sum_Tran = (((((((((id ([:(SegM 5),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [0,0,1])) +* ([0,1] .--> [1,0,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0] .--> [2,1,1])) +* ([2,1] .--> [2,1,1])) +* ([2,0] .--> [3,0,(- 1)])) +* ([3,1] .--> [4,0,(- 1)])) +* ([4,1] .--> [4,1,(- 1)])) +* ([4,0] .--> [5,0,0]);

theorem Th14: :: TURING_1:14

( Sum_Tran . [0,0] = [0,0,1] & Sum_Tran . [0,1] = [1,0,1] & Sum_Tran . [1,1] = [1,1,1] & Sum_Tran . [1,0] = [2,1,1] & Sum_Tran . [2,1] = [2,1,1] & Sum_Tran . [2,0] = [3,0,(- 1)] & Sum_Tran . [3,1] = [4,0,(- 1)] & Sum_Tran . [4,1] = [4,1,(- 1)] & Sum_Tran . [4,0] = [5,0,0] )

proof end;

:: deftheorem defines is_1_between TURING_1:def 12 :

for T being TuringStr

for t being Tape of T

for i, j being Integer holds

( t is_1_between i,j iff ( t . i = 0 & t . j = 0 & ( for k being Integer st i < k & k < j holds

t . k = 1 ) ) );

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 defines storeData TURING_1:def 13 :

for f being natural-valued FinSequence

for T being TuringStr

for t being Tape of T holds

( t storeData f iff for i being Nat st 1 <= i & i < len f holds

t is_1_between (Sum (Prefix (f,i))) + (2 * (i - 1)),(Sum (Prefix (f,(i + 1)))) + (2 * i) );

for f being natural-valued FinSequence

for T being TuringStr

for t being Tape of T holds

( t storeData f iff for i being Nat st 1 <= i & i < len f holds

t is_1_between (Sum (Prefix (f,i))) + (2 * (i - 1)),(Sum (Prefix (f,(i + 1)))) + (2 * i) );

theorem Th15: :: TURING_1:15

for T being TuringStr

for t being Tape of T

for s, n being Element of NAT st t storeData <*s,n*> holds

t is_1_between s,(s + n) + 2

for t being Tape of T

for s, n being Element of NAT st t storeData <*s,n*> holds

t is_1_between s,(s + n) + 2

proof end;

theorem Th16: :: TURING_1:16

for T being TuringStr

for t being Tape of T

for s, n being Element of NAT st t is_1_between s,(s + n) + 2 holds

t storeData <*s,n*>

for t being Tape of T

for s, n being Element of NAT st t is_1_between s,(s + n) + 2 holds

t storeData <*s,n*>

proof end;

theorem Th17: :: TURING_1:17

for T being TuringStr

for t being Tape of T

for s, n being Element of NAT st t storeData <*s,n*> holds

( t . s = 0 & t . ((s + n) + 2) = 0 & ( for i being Integer st s < i & i < (s + n) + 2 holds

t . i = 1 ) )

for t being Tape of T

for s, n being Element of NAT st t storeData <*s,n*> holds

( t . s = 0 & t . ((s + n) + 2) = 0 & ( for i being Integer st s < i & i < (s + n) + 2 holds

t . i = 1 ) )

proof end;

theorem Th18: :: TURING_1:18

for T being TuringStr

for t being Tape of T

for s, n1, n2 being Element of NAT st t storeData <*s,n1,n2*> holds

( t is_1_between s,(s + n1) + 2 & t is_1_between (s + n1) + 2,((s + n1) + n2) + 4 )

for t being Tape of T

for s, n1, n2 being Element of NAT st t storeData <*s,n1,n2*> holds

( t is_1_between s,(s + n1) + 2 & t is_1_between (s + n1) + 2,((s + n1) + n2) + 4 )

proof end;

theorem Th19: :: TURING_1:19

for T being TuringStr

for t being Tape of T

for s, n1, n2 being Element of NAT st t storeData <*s,n1,n2*> holds

( t . s = 0 & t . ((s + n1) + 2) = 0 & t . (((s + n1) + n2) + 4) = 0 & ( for i being Integer st s < i & i < (s + n1) + 2 holds

t . i = 1 ) & ( for i being Integer st (s + n1) + 2 < i & i < ((s + n1) + n2) + 4 holds

t . i = 1 ) )

for t being Tape of T

for s, n1, n2 being Element of NAT st t storeData <*s,n1,n2*> holds

( t . s = 0 & t . ((s + n1) + 2) = 0 & t . (((s + n1) + n2) + 4) = 0 & ( for i being Integer st s < i & i < (s + n1) + 2 holds

t . i = 1 ) & ( for i being Integer st (s + n1) + 2 < i & i < ((s + n1) + n2) + 4 holds

t . i = 1 ) )

proof end;

theorem Th20: :: TURING_1:20

for f being FinSequence of NAT

for s being Element of NAT st len f >= 1 holds

( Sum (Prefix ((<*s*> ^ f),1)) = s & Sum (Prefix ((<*s*> ^ f),2)) = s + (f /. 1) )

for s being Element of NAT st len f >= 1 holds

( Sum (Prefix ((<*s*> ^ f),1)) = s & Sum (Prefix ((<*s*> ^ f),2)) = s + (f /. 1) )

proof end;

theorem Th21: :: TURING_1:21

for f being FinSequence of NAT

for s being Element of NAT st len f >= 3 holds

( Sum (Prefix ((<*s*> ^ f),1)) = s & Sum (Prefix ((<*s*> ^ f),2)) = s + (f /. 1) & Sum (Prefix ((<*s*> ^ f),3)) = (s + (f /. 1)) + (f /. 2) & Sum (Prefix ((<*s*> ^ f),4)) = ((s + (f /. 1)) + (f /. 2)) + (f /. 3) )

for s being Element of NAT st len f >= 3 holds

( Sum (Prefix ((<*s*> ^ f),1)) = s & Sum (Prefix ((<*s*> ^ f),2)) = s + (f /. 1) & Sum (Prefix ((<*s*> ^ f),3)) = (s + (f /. 1)) + (f /. 2) & Sum (Prefix ((<*s*> ^ f),4)) = ((s + (f /. 1)) + (f /. 2)) + (f /. 3) )

proof end;

theorem Th22: :: TURING_1:22

for T being TuringStr

for t being Tape of T

for s being Element of NAT

for f being FinSequence of NAT st len f >= 1 & t storeData <*s*> ^ f holds

t is_1_between s,(s + (f /. 1)) + 2

for t being Tape of T

for s being Element of NAT

for f being FinSequence of NAT st len f >= 1 & t storeData <*s*> ^ f holds

t is_1_between s,(s + (f /. 1)) + 2

proof end;

theorem Th23: :: TURING_1:23

for T being TuringStr

for t being Tape of T

for s being Element of NAT

for f being FinSequence of NAT st len f >= 3 & t storeData <*s*> ^ f holds

( t is_1_between s,(s + (f /. 1)) + 2 & t is_1_between (s + (f /. 1)) + 2,((s + (f /. 1)) + (f /. 2)) + 4 & t is_1_between ((s + (f /. 1)) + (f /. 2)) + 4,(((s + (f /. 1)) + (f /. 2)) + (f /. 3)) + 6 )

for t being Tape of T

for s being Element of NAT

for f being FinSequence of NAT st len f >= 3 & t storeData <*s*> ^ f holds

( t is_1_between s,(s + (f /. 1)) + 2 & t is_1_between (s + (f /. 1)) + 2,((s + (f /. 1)) + (f /. 2)) + 4 & t is_1_between ((s + (f /. 1)) + (f /. 2)) + 4,(((s + (f /. 1)) + (f /. 2)) + (f /. 3)) + 6 )

proof end;

definition

ex b_{1} being strict TuringStr st

( the Symbols of b_{1} = {0,1} & the FStates of b_{1} = SegM 5 & the Tran of b_{1} = Sum_Tran & the InitS of b_{1} = 0 & the AcceptS of b_{1} = 5 )

for b_{1}, b_{2} being strict TuringStr st the Symbols of b_{1} = {0,1} & the FStates of b_{1} = SegM 5 & the Tran of b_{1} = Sum_Tran & the InitS of b_{1} = 0 & the AcceptS of b_{1} = 5 & the Symbols of b_{2} = {0,1} & the FStates of b_{2} = SegM 5 & the Tran of b_{2} = Sum_Tran & the InitS of b_{2} = 0 & the AcceptS of b_{2} = 5 holds

b_{1} = b_{2}
;

end;

func SumTuring -> strict TuringStr means :Def14: :: TURING_1:def 14

( the Symbols of it = {0,1} & the FStates of it = SegM 5 & the Tran of it = Sum_Tran & the InitS of it = 0 & the AcceptS of it = 5 );

existence ( the Symbols of it = {0,1} & the FStates of it = SegM 5 & the Tran of it = Sum_Tran & the InitS of it = 0 & the AcceptS of it = 5 );

ex b

( the Symbols of b

proof end;

uniqueness for b

b

:: deftheorem Def14 defines SumTuring TURING_1:def 14 :

for b_{1} being strict TuringStr holds

( b_{1} = SumTuring iff ( the Symbols of b_{1} = {0,1} & the FStates of b_{1} = SegM 5 & the Tran of b_{1} = Sum_Tran & the InitS of b_{1} = 0 & the AcceptS of b_{1} = 5 ) );

for b

( b

Lm1: for n being Element of NAT st n <= 5 holds

n is State of SumTuring

proof end;

theorem Th24: :: TURING_1:24

for T being TuringStr

for t being Tape of T

for h being Integer

for s being Symbol of T st t . h = s holds

Tape-Chg (t,h,s) = t

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;

Lm3: for s being All-State of SumTuring

for p, h, t being set st s = [p,h,t] & p <> 5 holds

Following s = [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))]

proof end;

theorem Th26: :: TURING_1:26

for T being TuringStr

for t being Tape of T

for h being Integer

for s being Symbol of T

for i being object holds

( (Tape-Chg (t,h,s)) . h = s & ( i <> h implies (Tape-Chg (t,h,s)) . i = t . i ) )

for t being Tape of T

for h being Integer

for s being Symbol of T

for i being object holds

( (Tape-Chg (t,h,s)) . h = s & ( i <> h implies (Tape-Chg (t,h,s)) . i = t . i ) )

proof end;

Lm4: for tm being TuringStr

for s being All-State of tm

for p being State of tm

for h being Element of INT

for t being Tape of tm

for m, d being Element of NAT st d = h & 1 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,1,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds

t . i = 1 ) holds

(Computation s) . m = [p,(d + m),t]

proof end;

theorem Th27: :: TURING_1:27

for s being All-State of SumTuring

for t being Tape of SumTuring

for head, n1, n2 being Element of NAT st s = [0,head,t] & t storeData <*head,n1,n2*> holds

( s is Accept-Halt & (Result s) `2_3 = 1 + head & (Result s) `3_3 storeData <*(1 + head),(n1 + n2)*> )

for t being Tape of SumTuring

for head, n1, n2 being Element of NAT st s = [0,head,t] & t storeData <*head,n1,n2*> holds

( s is Accept-Halt & (Result s) `2_3 = 1 + head & (Result s) `3_3 storeData <*(1 + head),(n1 + n2)*> )

proof end;

definition

let T be TuringStr ;

let F be Function;

end;
let F be Function;

pred T computes F means :: TURING_1:def 15

for s being All-State of T

for t being Tape of T

for a being Element of NAT

for x being FinSequence of NAT st x in dom F & s = [ the InitS of T,a,t] & t storeData <*a*> ^ x holds

( s is Accept-Halt & ex b, y being Element of NAT st

( (Result s) `2_3 = b & y = F . x & (Result s) `3_3 storeData <*b*> ^ <*y*> ) );

for s being All-State of T

for t being Tape of T

for a being Element of NAT

for x being FinSequence of NAT st x in dom F & s = [ the InitS of T,a,t] & t storeData <*a*> ^ x holds

( s is Accept-Halt & ex b, y being Element of NAT st

( (Result s) `2_3 = b & y = F . x & (Result s) `3_3 storeData <*b*> ^ <*y*> ) );

:: deftheorem defines computes TURING_1:def 15 :

for T being TuringStr

for F being Function holds

( T computes F iff for s being All-State of T

for t being Tape of T

for a being Element of NAT

for x being FinSequence of NAT st x in dom F & s = [ the InitS of T,a,t] & t storeData <*a*> ^ x holds

( s is Accept-Halt & ex b, y being Element of NAT st

( (Result s) `2_3 = b & y = F . x & (Result s) `3_3 storeData <*b*> ^ <*y*> ) ) );

for T being TuringStr

for F being Function holds

( T computes F iff for s being All-State of T

for t being Tape of T

for a being Element of NAT

for x being FinSequence of NAT st x in dom F & s = [ the InitS of T,a,t] & t storeData <*a*> ^ x holds

( s is Accept-Halt & ex b, y being Element of NAT st

( (Result s) `2_3 = b & y = F . x & (Result s) `3_3 storeData <*b*> ^ <*y*> ) ) );

definition

(((((((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;

func Succ_Tran -> Function of [:(SegM 4),{0,1}:],[:(SegM 4),{0,1},{(- 1),0,1}:] equals :: TURING_1:def 16

(((((((id ([:(SegM 4),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [1,0,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0] .--> [2,1,1])) +* ([2,0] .--> [3,0,(- 1)])) +* ([2,1] .--> [3,0,(- 1)])) +* ([3,1] .--> [3,1,(- 1)])) +* ([3,0] .--> [4,0,0]);

coherence (((((((id ([:(SegM 4),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [1,0,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0] .--> [2,1,1])) +* ([2,0] .--> [3,0,(- 1)])) +* ([2,1] .--> [3,0,(- 1)])) +* ([3,1] .--> [3,1,(- 1)])) +* ([3,0] .--> [4,0,0]);

(((((((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;

:: deftheorem defines Succ_Tran TURING_1:def 16 :

Succ_Tran = (((((((id ([:(SegM 4),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [1,0,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0] .--> [2,1,1])) +* ([2,0] .--> [3,0,(- 1)])) +* ([2,1] .--> [3,0,(- 1)])) +* ([3,1] .--> [3,1,(- 1)])) +* ([3,0] .--> [4,0,0]);

Succ_Tran = (((((((id ([:(SegM 4),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [1,0,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0] .--> [2,1,1])) +* ([2,0] .--> [3,0,(- 1)])) +* ([2,1] .--> [3,0,(- 1)])) +* ([3,1] .--> [3,1,(- 1)])) +* ([3,0] .--> [4,0,0]);

theorem Th30: :: TURING_1:30

( Succ_Tran . [0,0] = [1,0,1] & Succ_Tran . [1,1] = [1,1,1] & Succ_Tran . [1,0] = [2,1,1] & Succ_Tran . [2,0] = [3,0,(- 1)] & Succ_Tran . [2,1] = [3,0,(- 1)] & Succ_Tran . [3,1] = [3,1,(- 1)] & Succ_Tran . [3,0] = [4,0,0] )

proof end;

definition

ex b_{1} being strict TuringStr st

( the Symbols of b_{1} = {0,1} & the FStates of b_{1} = SegM 4 & the Tran of b_{1} = Succ_Tran & the InitS of b_{1} = 0 & the AcceptS of b_{1} = 4 )

for b_{1}, b_{2} being strict TuringStr st the Symbols of b_{1} = {0,1} & the FStates of b_{1} = SegM 4 & the Tran of b_{1} = Succ_Tran & the InitS of b_{1} = 0 & the AcceptS of b_{1} = 4 & the Symbols of b_{2} = {0,1} & the FStates of b_{2} = SegM 4 & the Tran of b_{2} = Succ_Tran & the InitS of b_{2} = 0 & the AcceptS of b_{2} = 4 holds

b_{1} = b_{2}
;

end;

func SuccTuring -> strict TuringStr means :Def17: :: TURING_1:def 17

( the Symbols of it = {0,1} & the FStates of it = SegM 4 & the Tran of it = Succ_Tran & the InitS of it = 0 & the AcceptS of it = 4 );

existence ( the Symbols of it = {0,1} & the FStates of it = SegM 4 & the Tran of it = Succ_Tran & the InitS of it = 0 & the AcceptS of it = 4 );

ex b

( the Symbols of b

proof end;

uniqueness for b

b

:: deftheorem Def17 defines SuccTuring TURING_1:def 17 :

for b_{1} being strict TuringStr holds

( b_{1} = SuccTuring iff ( the Symbols of b_{1} = {0,1} & the FStates of b_{1} = SegM 4 & the Tran of b_{1} = Succ_Tran & the InitS of b_{1} = 0 & the AcceptS of b_{1} = 4 ) );

for b

( b

Lm5: for n being Element of NAT st n <= 4 holds

n is State of SuccTuring

proof end;

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

proof end;

Lm7: for s being All-State of SuccTuring

for p, h, t being set st s = [p,h,t] & p <> 4 holds

Following s = [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))]

proof end;

theorem Th31: :: TURING_1:31

for s being All-State of SuccTuring

for t being Tape of SuccTuring

for head, n being Element of NAT st s = [0,head,t] & t storeData <*head,n*> holds

( s is Accept-Halt & (Result s) `2_3 = head & (Result s) `3_3 storeData <*head,(n + 1)*> )

for t being Tape of SuccTuring

for head, n being Element of NAT st s = [0,head,t] & t storeData <*head,n*> holds

( s is Accept-Halt & (Result s) `2_3 = head & (Result s) `3_3 storeData <*head,(n + 1)*> )

proof end;

definition

(((((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;

func Zero_Tran -> Function of [:(SegM 4),{0,1}:],[:(SegM 4),{0,1},{(- 1),0,1}:] equals :: TURING_1:def 18

(((((id ([:(SegM 4),{0,1}:],{(- 1),0,1},1)) +* ([0,0] .--> [1,0,1])) +* ([1,1] .--> [2,1,1])) +* ([2,0] .--> [3,0,(- 1)])) +* ([2,1] .--> [3,0,(- 1)])) +* ([3,1] .--> [4,1,(- 1)]);

coherence (((((id ([:(SegM 4),{0,1}:],{(- 1),0,1},1)) +* ([0,0] .--> [1,0,1])) +* ([1,1] .--> [2,1,1])) +* ([2,0] .--> [3,0,(- 1)])) +* ([2,1] .--> [3,0,(- 1)])) +* ([3,1] .--> [4,1,(- 1)]);

(((((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;

:: deftheorem defines Zero_Tran TURING_1:def 18 :

Zero_Tran = (((((id ([:(SegM 4),{0,1}:],{(- 1),0,1},1)) +* ([0,0] .--> [1,0,1])) +* ([1,1] .--> [2,1,1])) +* ([2,0] .--> [3,0,(- 1)])) +* ([2,1] .--> [3,0,(- 1)])) +* ([3,1] .--> [4,1,(- 1)]);

Zero_Tran = (((((id ([:(SegM 4),{0,1}:],{(- 1),0,1},1)) +* ([0,0] .--> [1,0,1])) +* ([1,1] .--> [2,1,1])) +* ([2,0] .--> [3,0,(- 1)])) +* ([2,1] .--> [3,0,(- 1)])) +* ([3,1] .--> [4,1,(- 1)]);

theorem Th33: :: TURING_1:33

( Zero_Tran . [0,0] = [1,0,1] & Zero_Tran . [1,1] = [2,1,1] & Zero_Tran . [2,0] = [3,0,(- 1)] & Zero_Tran . [2,1] = [3,0,(- 1)] & Zero_Tran . [3,1] = [4,1,(- 1)] )

proof end;

definition

ex b_{1} being strict TuringStr st

( the Symbols of b_{1} = {0,1} & the FStates of b_{1} = SegM 4 & the Tran of b_{1} = Zero_Tran & the InitS of b_{1} = 0 & the AcceptS of b_{1} = 4 )

for b_{1}, b_{2} being strict TuringStr st the Symbols of b_{1} = {0,1} & the FStates of b_{1} = SegM 4 & the Tran of b_{1} = Zero_Tran & the InitS of b_{1} = 0 & the AcceptS of b_{1} = 4 & the Symbols of b_{2} = {0,1} & the FStates of b_{2} = SegM 4 & the Tran of b_{2} = Zero_Tran & the InitS of b_{2} = 0 & the AcceptS of b_{2} = 4 holds

b_{1} = b_{2}
;

end;

func ZeroTuring -> strict TuringStr means :Def19: :: TURING_1:def 19

( the Symbols of it = {0,1} & the FStates of it = SegM 4 & the Tran of it = Zero_Tran & the InitS of it = 0 & the AcceptS of it = 4 );

existence ( the Symbols of it = {0,1} & the FStates of it = SegM 4 & the Tran of it = Zero_Tran & the InitS of it = 0 & the AcceptS of it = 4 );

ex b

( the Symbols of b

proof end;

uniqueness for b

b

:: deftheorem Def19 defines ZeroTuring TURING_1:def 19 :

for b_{1} being strict TuringStr holds

( b_{1} = ZeroTuring iff ( the Symbols of b_{1} = {0,1} & the FStates of b_{1} = SegM 4 & the Tran of b_{1} = Zero_Tran & the InitS of b_{1} = 0 & the AcceptS of b_{1} = 4 ) );

for b

( b

Lm8: for n being Element of NAT st n <= 4 holds

n is State of ZeroTuring

proof end;

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

proof end;

Lm10: for s being All-State of ZeroTuring

for p, h, t being set st s = [p,h,t] & p <> 4 holds

Following s = [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))]

proof end;

theorem Th34: :: TURING_1:34

for s being All-State of ZeroTuring

for t being Tape of ZeroTuring

for head being Element of NAT

for f being FinSequence of NAT st len f >= 1 & s = [0,head,t] & t storeData <*head*> ^ f holds

( s is Accept-Halt & (Result s) `2_3 = head & (Result s) `3_3 storeData <*head,0*> )

for t being Tape of ZeroTuring

for head being Element of NAT

for f being FinSequence of NAT st len f >= 1 & s = [0,head,t] & t storeData <*head*> ^ f holds

( s is Accept-Halt & (Result s) `2_3 = head & (Result s) `3_3 storeData <*head,0*> )

proof end;

definition

(((((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;

func U3(n)Tran -> Function of [:(SegM 3),{0,1}:],[:(SegM 3),{0,1},{(- 1),0,1}:] equals :: TURING_1:def 20

(((((id ([:(SegM 3),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [1,0,1])) +* ([1,1] .--> [1,0,1])) +* ([1,0] .--> [2,0,1])) +* ([2,1] .--> [2,0,1])) +* ([2,0] .--> [3,0,0]);

coherence (((((id ([:(SegM 3),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [1,0,1])) +* ([1,1] .--> [1,0,1])) +* ([1,0] .--> [2,0,1])) +* ([2,1] .--> [2,0,1])) +* ([2,0] .--> [3,0,0]);

(((((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;

:: deftheorem defines U3(n)Tran TURING_1:def 20 :

U3(n)Tran = (((((id ([:(SegM 3),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [1,0,1])) +* ([1,1] .--> [1,0,1])) +* ([1,0] .--> [2,0,1])) +* ([2,1] .--> [2,0,1])) +* ([2,0] .--> [3,0,0]);

U3(n)Tran = (((((id ([:(SegM 3),{0,1}:],{(- 1),0,1},0)) +* ([0,0] .--> [1,0,1])) +* ([1,1] .--> [1,0,1])) +* ([1,0] .--> [2,0,1])) +* ([2,1] .--> [2,0,1])) +* ([2,0] .--> [3,0,0]);

theorem Th36: :: TURING_1:36

( U3(n)Tran . [0,0] = [1,0,1] & U3(n)Tran . [1,1] = [1,0,1] & U3(n)Tran . [1,0] = [2,0,1] & U3(n)Tran . [2,1] = [2,0,1] & U3(n)Tran . [2,0] = [3,0,0] )

proof end;

definition

ex b_{1} being strict TuringStr st

( the Symbols of b_{1} = {0,1} & the FStates of b_{1} = SegM 3 & the Tran of b_{1} = U3(n)Tran & the InitS of b_{1} = 0 & the AcceptS of b_{1} = 3 )

for b_{1}, b_{2} being strict TuringStr st the Symbols of b_{1} = {0,1} & the FStates of b_{1} = SegM 3 & the Tran of b_{1} = U3(n)Tran & the InitS of b_{1} = 0 & the AcceptS of b_{1} = 3 & the Symbols of b_{2} = {0,1} & the FStates of b_{2} = SegM 3 & the Tran of b_{2} = U3(n)Tran & the InitS of b_{2} = 0 & the AcceptS of b_{2} = 3 holds

b_{1} = b_{2}
;

end;

func U3(n)Turing -> strict TuringStr means :Def21: :: TURING_1:def 21

( the Symbols of it = {0,1} & the FStates of it = SegM 3 & the Tran of it = U3(n)Tran & the InitS of it = 0 & the AcceptS of it = 3 );

existence ( the Symbols of it = {0,1} & the FStates of it = SegM 3 & the Tran of it = U3(n)Tran & the InitS of it = 0 & the AcceptS of it = 3 );

ex b

( the Symbols of b

proof end;

uniqueness for b

b

:: deftheorem Def21 defines U3(n)Turing TURING_1:def 21 :

for b_{1} being strict TuringStr holds

( b_{1} = U3(n)Turing iff ( the Symbols of b_{1} = {0,1} & the FStates of b_{1} = SegM 3 & the Tran of b_{1} = U3(n)Tran & the InitS of b_{1} = 0 & the AcceptS of b_{1} = 3 ) );

for b

( b

Lm11: for n being Element of NAT st n <= 3 holds

n is State of U3(n)Turing

proof end;

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

proof end;

Lm13: for s being All-State of U3(n)Turing

for p, h, t being set st s = [p,h,t] & p <> 3 holds

Following s = [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))]

proof end;

Lm14: for tm being TuringStr

for s being All-State of tm

for p being State of tm

for h being Element of INT

for t being Tape of tm

for m, d being Element of NAT st d = h & 0 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,0,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds

t . i = 1 ) holds

ex t1 being Tape of tm st

( (Computation s) . m = [p,(d + m),t1] & ( for i being Integer st d <= i & i < d + m holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds

t1 . i = t . i ) )

proof end;

theorem Th37: :: TURING_1:37

for s being All-State of U3(n)Turing

for t being Tape of U3(n)Turing

for head being Element of NAT

for f being FinSequence of NAT st len f >= 3 & s = [0,head,t] & t storeData <*head*> ^ f holds

( s is Accept-Halt & (Result s) `2_3 = ((head + (f /. 1)) + (f /. 2)) + 4 & (Result s) `3_3 storeData <*(((head + (f /. 1)) + (f /. 2)) + 4),(f /. 3)*> )

for t being Tape of U3(n)Turing

for head being Element of NAT

for f being FinSequence of NAT st len f >= 3 & s = [0,head,t] & t storeData <*head*> ^ f holds

( s is Accept-Halt & (Result s) `2_3 = ((head + (f /. 1)) + (f /. 2)) + 4 & (Result s) `3_3 storeData <*(((head + (f /. 1)) + (f /. 2)) + 4),(f /. 3)*> )

proof end;

definition

let t1, t2 be TuringStr ;

coherence

[: the FStates of t1,{ the InitS of t2}:] \/ [:{ the AcceptS of t1}, the FStates of t2:] is non empty finite set ;

;

end;
func UnionSt (t1,t2) -> non empty finite set equals :: TURING_1:def 22

[: the FStates of t1,{ the InitS of t2}:] \/ [:{ the AcceptS of t1}, the FStates of t2:];

correctness [: the FStates of t1,{ the InitS of t2}:] \/ [:{ the AcceptS of t1}, the FStates of t2:];

coherence

[: the FStates of t1,{ the InitS of t2}:] \/ [:{ the AcceptS of t1}, the FStates of t2:] is non empty finite set ;

;

:: deftheorem defines UnionSt TURING_1:def 22 :

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

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

theorem Th39: :: TURING_1:39

for t1, t2 being TuringStr holds

( [ the InitS of t1, the InitS of t2] in UnionSt (t1,t2) & [ the AcceptS of t1, the AcceptS of t2] in UnionSt (t1,t2) )

( [ 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 Th42: :: TURING_1:42

for s, t being TuringStr

for x being Element of UnionSt (s,t) ex x1 being State of s ex x2 being State of t st x = [x1,x2]

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;

[[(x `1_3), the InitS of t],(x `2_3),(x `3_3)] is Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:]

end;
let x be Tran-Goal of s;

func FirstTuringTran (s,t,x) -> Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:] equals :: TURING_1:def 23

[[(x `1_3), the InitS of t],(x `2_3),(x `3_3)];

coherence [[(x `1_3), the InitS of t],(x `2_3),(x `3_3)];

[[(x `1_3), the InitS of t],(x `2_3),(x `3_3)] is Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:]

proof end;

:: deftheorem defines FirstTuringTran TURING_1:def 23 :

for s, t being TuringStr

for x being Tran-Goal of s holds FirstTuringTran (s,t,x) = [[(x `1_3), the InitS of t],(x `2_3),(x `3_3)];

for s, t being TuringStr

for x being Tran-Goal of s holds FirstTuringTran (s,t,x) = [[(x `1_3), the InitS of t],(x `2_3),(x `3_3)];

definition

let s, t be TuringStr ;

let x be Tran-Goal of t;

[[ the AcceptS of s,(x `1_3)],(x `2_3),(x `3_3)] is Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:]

end;
let x be Tran-Goal of t;

func SecondTuringTran (s,t,x) -> Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:] equals :: TURING_1:def 24

[[ the AcceptS of s,(x `1_3)],(x `2_3),(x `3_3)];

coherence [[ the AcceptS of s,(x `1_3)],(x `2_3),(x `3_3)];

[[ the AcceptS of s,(x `1_3)],(x `2_3),(x `3_3)] is Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:]

proof end;

:: deftheorem defines SecondTuringTran TURING_1:def 24 :

for s, t being TuringStr

for x being Tran-Goal of t holds SecondTuringTran (s,t,x) = [[ the AcceptS of s,(x `1_3)],(x `2_3),(x `3_3)];

for s, t being TuringStr

for x being Tran-Goal of t holds SecondTuringTran (s,t,x) = [[ the AcceptS of s,(x `1_3)],(x `2_3),(x `3_3)];

definition

let s, t be TuringStr ;

let x be Element of UnionSt (s,t);

:: original: `1

redefine func x `1 -> State of s;

coherence

x `1 is State of s

redefine func x `2 -> State of t;

coherence

x `2 is State of t

end;
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: `2redefine func x `2 -> State of t;

coherence

x `2 is State of t

proof end;

definition

let s, t be TuringStr ;

let x be Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):];

correctness

coherence

(x `1) `1 is State of s;

;

correctness

coherence

(x `1) `2 is State of t;

;

end;
let x be Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):];

correctness

coherence

(x `1) `1 is State of s;

;

correctness

coherence

(x `1) `2 is State of t;

;

:: deftheorem defines FirstTuringState TURING_1:def 25 :

for s, t being TuringStr

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

for s, t being TuringStr

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

:: deftheorem defines SecondTuringState TURING_1:def 26 :

for s, t being TuringStr

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

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] ;

coherence

x `2 is Element of Y by A1;

end;
let x be Element of [:X,(Y \/ Z):];

given u being set , y being Element of Y such that A1: x = [u,y] ;

coherence

x `2 is Element of Y by A1;

:: deftheorem Def27 defines FirstTuringSymbol TURING_1:def 27 :

for X, Y, Z being non empty set

for x being Element of [:X,(Y \/ Z):] st ex u being set ex y being Element of Y st x = [u,y] holds

FirstTuringSymbol x = x `2 ;

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] ;

coherence

x `2 is Element of Z by A1;

end;
let x be Element of [:X,(Y \/ Z):];

given u being set , z being Element of Z such that A1: x = [u,z] ;

coherence

x `2 is Element of Z by A1;

:: deftheorem Def28 defines SecondTuringSymbol TURING_1:def 28 :

for X, Y, Z being non empty set

for x being Element of [:X,(Y \/ Z):] st ex u being set ex z being Element of Z st x = [u,z] holds

SecondTuringSymbol x = x `2 ;

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):];

for b_{1} 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

( b_{1} = FirstTuringTran (s,t,( the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)])) iff b_{1} = SecondTuringTran (s,t,( the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)])) )

( ( 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;
let x be Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):];

func Uniontran (s,t,x) -> Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:] equals :Def29: :: TURING_1:def 29

FirstTuringTran (s,t,( the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)])) if ex p being State of s ex y being Symbol of s st

( x = [[p, the InitS of t],y] & p <> the AcceptS of s )

SecondTuringTran (s,t,( the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)])) if ex q being State of t ex y being Symbol of t st x = [[ the AcceptS of s,q],y]

otherwise [(x `1),(x `2),(- 1)];

consistency 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)];

for b

( 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

( b

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;

:: deftheorem Def29 defines Uniontran TURING_1:def 29 :

for s, t being TuringStr

for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds

( ( ex p being State of s ex y being Symbol of s st

( x = [[p, the InitS of t],y] & p <> the AcceptS of s ) implies Uniontran (s,t,x) = FirstTuringTran (s,t,( the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)])) ) & ( ex q being State of t ex y being Symbol of t st x = [[ the AcceptS of s,q],y] implies Uniontran (s,t,x) = SecondTuringTran (s,t,( the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)])) ) & ( ( for p being State of s

for y being Symbol of s holds

( not x = [[p, the InitS of t],y] or not p <> the AcceptS of s ) ) & ( for q being State of t

for y being Symbol of t holds not x = [[ the AcceptS of s,q],y] ) implies Uniontran (s,t,x) = [(x `1),(x `2),(- 1)] ) );

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 ;

ex b_{1} 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 b_{1} . x = Uniontran (s,t,x)

for b_{1}, b_{2} 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 b_{1} . x = Uniontran (s,t,x) ) & ( for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds b_{2} . x = Uniontran (s,t,x) ) holds

b_{1} = b_{2}

end;
func UnionTran (s,t) -> Function of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):],[:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:] means :Def30: :: TURING_1:def 30

for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds it . x = Uniontran (s,t,x);

existence for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds it . x = Uniontran (s,t,x);

ex b

for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def30 defines UnionTran TURING_1:def 30 :

for s, t being TuringStr

for b_{3} 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

( b_{3} = UnionTran (s,t) iff for x being Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t):] holds b_{3} . x = Uniontran (s,t,x) );

for s, t being TuringStr

for b

( b

definition

let T1, T2 be TuringStr ;

ex b_{1} being strict TuringStr st

( the Symbols of b_{1} = the Symbols of T1 \/ the Symbols of T2 & the FStates of b_{1} = UnionSt (T1,T2) & the Tran of b_{1} = UnionTran (T1,T2) & the InitS of b_{1} = [ the InitS of T1, the InitS of T2] & the AcceptS of b_{1} = [ the AcceptS of T1, the AcceptS of T2] )

for b_{1}, b_{2} being strict TuringStr st the Symbols of b_{1} = the Symbols of T1 \/ the Symbols of T2 & the FStates of b_{1} = UnionSt (T1,T2) & the Tran of b_{1} = UnionTran (T1,T2) & the InitS of b_{1} = [ the InitS of T1, the InitS of T2] & the AcceptS of b_{1} = [ the AcceptS of T1, the AcceptS of T2] & the Symbols of b_{2} = the Symbols of T1 \/ the Symbols of T2 & the FStates of b_{2} = UnionSt (T1,T2) & the Tran of b_{2} = UnionTran (T1,T2) & the InitS of b_{2} = [ the InitS of T1, the InitS of T2] & the AcceptS of b_{2} = [ the AcceptS of T1, the AcceptS of T2] holds

b_{1} = b_{2}
;

end;
func T1 ';' T2 -> strict TuringStr means :Def31: :: TURING_1:def 31

( the Symbols of it = the Symbols of T1 \/ the Symbols of T2 & the FStates of it = UnionSt (T1,T2) & the Tran of it = UnionTran (T1,T2) & the InitS of it = [ the InitS of T1, the InitS of T2] & the AcceptS of it = [ the AcceptS of T1, the AcceptS of T2] );

existence ( 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] );

ex b

( the Symbols of b

proof end;

uniqueness for b

b

:: deftheorem Def31 defines ';' TURING_1:def 31 :

for T1, T2 being TuringStr

for b_{3} being strict TuringStr holds

( b_{3} = T1 ';' T2 iff ( the Symbols of b_{3} = the Symbols of T1 \/ the Symbols of T2 & the FStates of b_{3} = UnionSt (T1,T2) & the Tran of b_{3} = UnionTran (T1,T2) & the InitS of b_{3} = [ the InitS of T1, the InitS of T2] & the AcceptS of b_{3} = [ the AcceptS of T1, the AcceptS of T2] ) );

for T1, T2 being TuringStr

for b

( b

theorem Th43: :: TURING_1:43

for T1, T2 being TuringStr

for g being Tran-Goal of T1

for p being State of T1

for y being Symbol of T1 st p <> the AcceptS of T1 & g = the Tran of T1 . [p,y] holds

the Tran of (T1 ';' T2) . [[p, the InitS of T2],y] = [[(g `1_3), the InitS of T2],(g `2_3),(g `3_3)]

for g being Tran-Goal of T1

for p being State of T1

for y being Symbol of T1 st p <> the AcceptS of T1 & g = the Tran of T1 . [p,y] holds

the Tran of (T1 ';' T2) . [[p, the InitS of T2],y] = [[(g `1_3), the InitS of T2],(g `2_3),(g `3_3)]

proof end;

theorem Th44: :: TURING_1:44

for T1, T2 being TuringStr

for g being Tran-Goal of T2

for q being State of T2

for y being Symbol of T2 st g = the Tran of T2 . [q,y] holds

the Tran of (T1 ';' T2) . [[ the AcceptS of T1,q],y] = [[ the AcceptS of T1,(g `1_3)],(g `2_3),(g `3_3)]

for g being Tran-Goal of T2

for q being State of T2

for y being Symbol of T2 st g = the Tran of T2 . [q,y] holds

the Tran of (T1 ';' T2) . [[ the AcceptS of T1,q],y] = [[ the AcceptS of T1,(g `1_3)],(g `2_3),(g `3_3)]

proof end;

theorem Th45: :: TURING_1:45

for T1, T2 being TuringStr

for s1 being All-State of T1

for h being Element of NAT

for t being Tape of T1

for s2 being All-State of T2

for s3 being All-State of (T1 ';' T2) st s1 is Accept-Halt & s1 = [ the InitS of T1,h,t] & s2 is Accept-Halt & s2 = [ the InitS of T2,((Result s1) `2_3),((Result s1) `3_3)] & s3 = [ the InitS of (T1 ';' T2),h,t] holds

( s3 is Accept-Halt & (Result s3) `2_3 = (Result s2) `2_3 & (Result s3) `3_3 = (Result s2) `3_3 )

for s1 being All-State of T1

for h being Element of NAT

for t being Tape of T1

for s2 being All-State of T2

for s3 being All-State of (T1 ';' T2) st s1 is Accept-Halt & s1 = [ the InitS of T1,h,t] & s2 is Accept-Halt & s2 = [ the InitS of T2,((Result s1) `2_3),((Result s1) `3_3)] & s3 = [ the InitS of (T1 ';' T2),h,t] holds

( s3 is Accept-Halt & (Result s3) `2_3 = (Result s2) `2_3 & (Result s3) `3_3 = (Result s2) `3_3 )

proof end;

theorem :: TURING_1:46

for tm1, tm2 being TuringStr

for t being Tape of tm1 st the Symbols of tm1 = the Symbols of tm2 holds

t is Tape of (tm1 ';' tm2)

for t being Tape of tm1 st the Symbols of tm1 = the Symbols of tm2 holds

t is Tape of (tm1 ';' tm2)

proof end;

theorem :: TURING_1:47

for tm1, tm2 being TuringStr

for t being Tape of (tm1 ';' tm2) st the Symbols of tm1 = the Symbols of tm2 holds

( t is Tape of tm1 & t is Tape of tm2 )

for t being Tape of (tm1 ';' tm2) st the Symbols of tm1 = the Symbols of tm2 holds

( t is Tape of tm1 & t is Tape of tm2 )

proof end;

theorem Th48: :: TURING_1:48

for f being FinSequence of NAT

for tm1, tm2 being TuringStr

for t1 being Tape of tm1

for t2 being Tape of tm2 st t1 = t2 & t1 storeData f holds

t2 storeData f

for tm1, tm2 being TuringStr

for t1 being Tape of tm1

for t2 being Tape of tm2 st t1 = t2 & t1 storeData f holds

t2 storeData f

proof end;

Lm15: for s being All-State of ZeroTuring

for t being Tape of ZeroTuring

for head, n being Element of NAT st s = [0,head,t] & t storeData <*head,n*> holds

( s is Accept-Halt & (Result s) `2_3 = head & (Result s) `3_3 storeData <*head,0*> )

proof end;

theorem :: TURING_1:49

for s being All-State of (ZeroTuring ';' SuccTuring)

for t being Tape of ZeroTuring

for head, n being Element of NAT st s = [[0,0],head,t] & t storeData <*head,n*> holds

( s is Accept-Halt & (Result s) `2_3 = head & (Result s) `3_3 storeData <*head,1*> )

for t being Tape of ZeroTuring

for head, n being Element of NAT st s = [[0,0],head,t] & t storeData <*head,n*> holds

( s is Accept-Halt & (Result s) `2_3 = head & (Result s) `3_3 storeData <*head,1*> )

proof end;