:: TURING_1 semantic presentation

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

proof end;

end;

definition

let X, Y be non empty set ;
let a be Element of X;
let b be Element of Y;
:: original: .-->
redefine func a .--> b -> PartFunc of X,Y;
coherence

proof end;

end;

definition

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

proof end;

end;

:: deftheorem defines SegM TURING_1:def 1 :

registration

let n be natural number ;
cluster SegM n -> non empty finite ;
coherence

proof end;

end;

theorem Th1: :: TURING_1:1

for k, n being Nat holds
( k in SegM n iff k <= n )

proof end;

theorem Th2: :: TURING_1:2

for f being Function
for x, y, z, u, v being set st u <> x holds
(f +* ([x,y] .--> z)) . [u,v] = f . [u,v]

proof end;

theorem Th3: :: TURING_1:3

for f being Function
for x, y, z, u, v being set st v <> y holds
(f +* ([x,y] .--> z)) . [u,v] = f . [u,v]

proof end;

theorem Th4: :: TURING_1:4

for i1, i2 being Element of INT holds Sum <*i1,i2*> = i1 + i2

proof end;

theorem Th5: :: TURING_1:5

for i1, i2, i3 being Element of INT holds Sum <*i1,i2,i3*> = (i1 + i2) + i3

proof end;

theorem Th6: :: TURING_1:6

for i1, i2, i3, i4 being Element of INT holds Sum <*i1,i2,i3,i4*> = ((i1 + i2) + i3) + i4

proof end;

definition

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

proof end;

end;

:: deftheorem defines Prefix TURING_1:def 2 :

theorem Th7: :: TURING_1:7

for x1, x2 being Nat holds
( Sum (Prefix <*x1,x2*>,1) = x1 & Sum (Prefix <*x1,x2*>,2) = x1 + x2 )

proof end;

theorem Th8: :: TURING_1:8

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

proof end;

definition

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

end;

definition

let T be TuringStr ;
mode State of T is Element of the States of T;
mode Tape of T is Element of Funcs INT ,the Symbols of T;
mode Symbol of T is Element of the Symbols of T;

end;

definition

let T be TuringStr ;
let t be Tape of T;
let h be Integer;
let s be Symbol of T;
func Tape-Chg t,h,s -> Tape of T equals :: TURING_1:def 3
t +* (h .--> s);
coherence

proof end;

end;

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

definition

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

end;

definition

let T be TuringStr ;
let g be Tran-Goal of T;
func offset g -> Integer equals :: TURING_1:def 4
g `3 ;
coherence by ENUMSET1:def 1;

end;

:: deftheorem defines offset TURING_1:def 4 :

definition

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

end;

:: deftheorem defines Head TURING_1:def 5 :

definition

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

proof end;

end;

:: deftheorem defines TRAN TURING_1:def 6 :

definition

let T be TuringStr ;
let s be All-State of T;
func Following s -> All-State of T equals :Def7: :: TURING_1:def 7
[((TRAN s) `1 ),((Head s) + (offset (TRAN s))),(Tape-Chg (s `3 ),(Head s),((TRAN s) `2 ))] if s `1 <> the AcceptS of T
otherwise s;
correctness

proof end;

end;

:: 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: :: TURING_1:def 8
( it . 0 = s & ( for i being Nat holds it . (i + 1) = Following (it . i) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines Computation TURING_1:def 8 :

theorem :: TURING_1:9

for T being TuringStr
for s being All-State of T st s `1 = the AcceptS of T holds
s = Following s by Def7;

theorem :: TURING_1:10

for T being TuringStr
for s being All-State of T holds (Computation s) . 0 = s by Def8;

theorem :: TURING_1:11

for k being Nat
for T being TuringStr
for s being All-State of T holds (Computation s) . (k + 1) = Following ((Computation s) . k) by Def8;

theorem Th12: :: TURING_1:12

for T being TuringStr
for s being All-State of T holds (Computation s) . 1 = Following s

proof end;

theorem Th13: :: TURING_1:13

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

proof end;

theorem Th14: :: TURING_1:14

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

proof end;

theorem Th15: :: TURING_1:15

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

proof end;

definition

let T be TuringStr ;
let s be All-State of T;
attr s is Accept-Halt means :Def9: :: TURING_1:def 9
ex k being Nat st ((Computation s) . k) `1 = the AcceptS of T;

end;

:: deftheorem Def9 defines Accept-Halt TURING_1:def 9 :

definition

let T be TuringStr ;
let s be All-State of T;
assume A1: s is Accept-Halt ;
func Result s -> All-State of T means :Def10: :: TURING_1:def 10
ex k being Nat st
( it = (Computation s) . k & ((Computation s) . k) `1 = the AcceptS of T );
uniqueness

proof end;

correctness

proof end;

end;

:: deftheorem Def10 defines Result TURING_1:def 10 :

theorem Th16: :: TURING_1:16

for T being TuringStr
for s being All-State of T st s is Accept-Halt holds
ex k being Nat st
( ((Computation s) . k) `1 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Nat st i < k holds
((Computation s) . i) `1 <> the AcceptS of T ) )

proof end;

definition

let A, B be non empty set ;
let y be set ;
assume A1: y in B ;
func id A,B,y -> Function of A,[:A,B:] means :: TURING_1:def 11
for x being Element of A holds it . x = [x,y];
existence

proof end;

uniqueness

proof end;

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 :: TURING_1:def 12
(((((((((id [:(SegM 5),{0,1}:],{(- 1),0,1},0) +* ([0,0] .--> [0,0,1])) +* ([0,1] .--> [1,0,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0] .--> [2,1,1])) +* ([2,1] .--> [2,1,1])) +* ([2,0] .--> [3,0,(- 1)])) +* ([3,1] .--> [4,0,(- 1)])) +* ([4,1] .--> [4,1,(- 1)])) +* ([4,0] .--> [5,0,0]);
coherence

proof end;

end;

:: deftheorem defines Sum_Tran TURING_1:def 12 :

theorem Th17: :: TURING_1:17

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

proof end;

definition

let T be TuringStr ;
let t be Tape of T;
let i, j be Integer;
pred t is_1_between i,j means :Def13: :: TURING_1:def 13
( t . i = 0 & t . j = 0 & ( for k being Integer st i < k & k < j holds
t . k = 1 ) );

end;

:: deftheorem Def13 defines is_1_between TURING_1:def 13 :

definition

let f be FinSequence of NAT ;
let T be TuringStr ;
let t be Tape of T;
pred t storeData f means :Def14: :: TURING_1:def 14
for i being Nat st 1 <= i & i < len f holds
t is_1_between (Sum (Prefix f,i)) + (2 * (i - 1)),(Sum (Prefix f,(i + 1))) + (2 * i);

end;

:: deftheorem Def14 defines storeData TURING_1:def 14 :

theorem Th18: :: TURING_1:18

for T being TuringStr
for t being Tape of T
for s, n being Nat st t storeData <*s,n*> holds
t is_1_between s,(s + n) + 2

proof end;

theorem Th19: :: TURING_1:19

for T being TuringStr
for t being Tape of T
for s, n being Nat st t is_1_between s,(s + n) + 2 holds
t storeData <*s,n*>

proof end;

theorem Th20: :: TURING_1:20

for T being TuringStr
for t being Tape of T
for s, n being Nat st t storeData <*s,n*> holds
( t . s = 0 & t . ((s + n) + 2) = 0 & ( for i being Integer st s < i & i < (s + n) + 2 holds
t . i = 1 ) )

proof end;

theorem Th21: :: TURING_1:21

for T being TuringStr
for t being Tape of T
for s, n1, n2 being Nat st t storeData <*s,n1,n2*> holds
( t is_1_between s,(s + n1) + 2 & t is_1_between (s + n1) + 2,((s + n1) + n2) + 4 )

proof end;

theorem Th22: :: TURING_1:22

for T being TuringStr
for t being Tape of T
for s, n1, n2 being Nat st t storeData <*s,n1,n2*> holds
( t . s = 0 & t . ((s + n1) + 2) = 0 & t . (((s + n1) + n2) + 4) = 0 & ( for i being Integer st s < i & i < (s + n1) + 2 holds
t . i = 1 ) & ( for i being Integer st (s + n1) + 2 < i & i < ((s + n1) + n2) + 4 holds
t . i = 1 ) )

proof end;

theorem Th23: :: TURING_1:23

for f being FinSequence of NAT
for s being Nat st len f >= 1 holds
( Sum (Prefix (<*s*> ^ f),1) = s & Sum (Prefix (<*s*> ^ f),2) = s + (f /. 1) )

proof end;

theorem Th24: :: TURING_1:24

for f being FinSequence of NAT
for s being Nat st len f >= 3 holds
( Sum (Prefix (<*s*> ^ f),1) = s & Sum (Prefix (<*s*> ^ f),2) = s + (f /. 1) & Sum (Prefix (<*s*> ^ f),3) = (s + (f /. 1)) + (f /. 2) & Sum (Prefix (<*s*> ^ f),4) = ((s + (f /. 1)) + (f /. 2)) + (f /. 3) )

proof end;

theorem Th25: :: TURING_1:25

for T being TuringStr
for t being Tape of T
for s being Nat
for f being FinSequence of NAT st len f >= 1 & t storeData <*s*> ^ f holds
t is_1_between s,(s + (f /. 1)) + 2

proof end;

theorem Th26: :: TURING_1:26

for T being TuringStr
for t being Tape of T
for s being Nat
for f being FinSequence of NAT st len f >= 3 & t storeData <*s*> ^ f holds
( t is_1_between s,(s + (f /. 1)) + 2 & t is_1_between (s + (f /. 1)) + 2,((s + (f /. 1)) + (f /. 2)) + 4 & t is_1_between ((s + (f /. 1)) + (f /. 2)) + 4,(((s + (f /. 1)) + (f /. 2)) + (f /. 3)) + 6 )

proof end;

definition

func SumTuring -> strict TuringStr means :Def15: :: TURING_1:def 15
( the Symbols of it = {0,1} & the States of it = SegM 5 & the Tran of it = Sum_Tran & the InitS of it = 0 & the AcceptS of it = 5 );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def15 defines SumTuring TURING_1:def 15 :

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

proof end;

theorem Th27: :: TURING_1:27

for T being TuringStr
for s being All-State of T
for p, h, t being set st s = [p,h,t] holds
Head s = h by MCART_1:68;

theorem Th28: :: TURING_1:28

for T being TuringStr
for t being Tape of T
for h being Integer
for s being Symbol of T st t . h = s holds
Tape-Chg t,h,s = t

proof end;

Lm2: ( 0 in the Symbols of SumTuring & 1 in the Symbols of SumTuring )

proof end;

theorem Th29: :: TURING_1:29

for T being TuringStr
for s being All-State of T
for p, h, t being set st s = [p,h,t] & p <> the AcceptS of T holds
Following s = [((TRAN s) `1 ),((Head s) + (offset (TRAN s))),(Tape-Chg (s `3 ),(Head s),((TRAN s) `2 ))]

proof end;

Lm3: for s being All-State of SumTuring
for p, h, t being set st s = [p,h,t] & p <> 5 holds
Following s = [((TRAN s) `1 ),((Head s) + (offset (TRAN s))),(Tape-Chg (s `3 ),(Head s),((TRAN s) `2 ))]

proof end;

theorem Th30: :: TURING_1:30

for T being TuringStr
for t being Tape of T
for h being Integer
for s being Symbol of T
for i being set holds
( (Tape-Chg t,h,s) . h = s & ( i <> h implies (Tape-Chg t,h,s) . i = t . i ) )

proof end;

Lm4: for tm being TuringStr
for s being All-State of tm
for p being State of tm
for h being Element of INT
for t being Tape of tm
for m, d being Nat st d = h & 1 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,1,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds
t . i = 1 ) holds
(Computation s) . m = [p,(d + m),t]

proof end;

theorem Th31: :: TURING_1:31

for s being All-State of SumTuring
for t being Tape of SumTuring
for head, n1, n2 being Nat st s = [0,head,t] & t storeData <*head,n1,n2*> holds
( s is Accept-Halt & (Result s) `2 = 1 + head & (Result s) `3 storeData <*(1 + head),(n1 + n2)*> )

proof end;

definition

let T be TuringStr ;
let F be Function;
pred T computes F means :Def16: :: TURING_1:def 16
for s being All-State of T
for t being Tape of T
for a being Nat
for x being FinSequence of NAT st x in dom F & s = [the InitS of T,a,t] & t storeData <*a*> ^ x holds
( s is Accept-Halt & ex b, y being Nat st
( (Result s) `2 = b & y = F . x & (Result s) `3 storeData <*b*> ^ <*y*> ) );

end;

:: deftheorem Def16 defines computes TURING_1:def 16 :

theorem Th32: :: TURING_1:32

dom [+] c= 2 -tuples_on NAT

proof end;

theorem :: TURING_1:33

SumTuring computes [+]

proof end;

definition

func Succ_Tran -> Function of [:(SegM 4),{0,1}:],[:(SegM 4),{0,1},{(- 1),0,1}:] equals :: TURING_1:def 17
(((((((id [:(SegM 4),{0,1}:],{(- 1),0,1},0) +* ([0,0] .--> [1,0,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0] .--> [2,1,1])) +* ([2,0] .--> [3,0,(- 1)])) +* ([2,1] .--> [3,0,(- 1)])) +* ([3,1] .--> [3,1,(- 1)])) +* ([3,0] .--> [4,0,0]);
coherence

proof end;

end;

:: deftheorem defines Succ_Tran TURING_1:def 17 :

theorem Th34: :: TURING_1:34

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

proof end;

definition

func SuccTuring -> strict TuringStr means :Def18: :: TURING_1:def 18
( the Symbols of it = {0,1} & the States of it = SegM 4 & the Tran of it = Succ_Tran & the InitS of it = 0 & the AcceptS of it = 4 );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def18 defines SuccTuring TURING_1:def 18 :

Lm5: for n being Nat st n <= 4 holds
n is State of SuccTuring

proof end;

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

proof end;

Lm7: for s being All-State of SuccTuring
for p, h, t being set st s = [p,h,t] & p <> 4 holds
Following s = [((TRAN s) `1 ),((Head s) + (offset (TRAN s))),(Tape-Chg (s `3 ),(Head s),((TRAN s) `2 ))]

proof end;

theorem :: TURING_1:35

canceled;

theorem Th36: :: TURING_1:36

for s being All-State of SuccTuring
for t being Tape of SuccTuring
for head, n being Nat st s = [0,head,t] & t storeData <*head,n*> holds
( s is Accept-Halt & (Result s) `2 = head & (Result s) `3 storeData <*head,(n + 1)*> )

proof end;

theorem :: TURING_1:37

SuccTuring computes 1 succ 1

proof end;

definition

func Zero_Tran -> Function of [:(SegM 4),{0,1}:],[:(SegM 4),{0,1},{(- 1),0,1}:] equals :: TURING_1:def 19
(((((id [:(SegM 4),{0,1}:],{(- 1),0,1},1) +* ([0,0] .--> [1,0,1])) +* ([1,1] .--> [2,1,1])) +* ([2,0] .--> [3,0,(- 1)])) +* ([2,1] .--> [3,0,(- 1)])) +* ([3,1] .--> [4,1,(- 1)]);
coherence

proof end;

end;

:: deftheorem defines Zero_Tran TURING_1:def 19 :

theorem Th38: :: TURING_1:38

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

proof end;

definition

func ZeroTuring -> strict TuringStr means :Def20: :: TURING_1:def 20
( the Symbols of it = {0,1} & the States of it = SegM 4 & the Tran of it = Zero_Tran & the InitS of it = 0 & the AcceptS of it = 4 );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def20 defines ZeroTuring TURING_1:def 20 :

Lm8: for n being Nat st n <= 4 holds
n is State of ZeroTuring

proof end;

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

proof end;

Lm10: for s being All-State of ZeroTuring
for p, h, t being set st s = [p,h,t] & p <> 4 holds
Following s = [((TRAN s) `1 ),((Head s) + (offset (TRAN s))),(Tape-Chg (s `3 ),(Head s),((TRAN s) `2 ))]

proof end;

theorem Th39: :: TURING_1:39

for s being All-State of ZeroTuring
for t being Tape of ZeroTuring
for head being Nat
for f being FinSequence of NAT st len f >= 1 & s = [0,head,t] & t storeData <*head*> ^ f holds
( s is Accept-Halt & (Result s) `2 = head & (Result s) `3 storeData <*head,0*> )

proof end;

theorem :: TURING_1:40

for n being Nat st n >= 1 holds
ZeroTuring computes n const 0

proof end;

definition

func U3(n)Tran -> Function of [:(SegM 3),{0,1}:],[:(SegM 3),{0,1},{(- 1),0,1}:] equals :: TURING_1:def 21
(((((id [:(SegM 3),{0,1}:],{(- 1),0,1},0) +* ([0,0] .--> [1,0,1])) +* ([1,1] .--> [1,0,1])) +* ([1,0] .--> [2,0,1])) +* ([2,1] .--> [2,0,1])) +* ([2,0] .--> [3,0,0]);
coherence

proof end;

end;

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

theorem Th41: :: TURING_1:41

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

proof end;

definition

func U3(n)Turing -> strict TuringStr means :Def22: :: TURING_1:def 22
( the Symbols of it = {0,1} & the States of it = SegM 3 & the Tran of it = U3(n)Tran & the InitS of it = 0 & the AcceptS of it = 3 );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def22 defines U3(n)Turing TURING_1:def 22 :

Lm11: for n being Nat st n <= 3 holds
n is State of U3(n)Turing

proof end;

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

proof end;

Lm13: for s being All-State of U3(n)Turing
for p, h, t being set st s = [p,h,t] & p <> 3 holds
Following s = [((TRAN s) `1 ),((Head s) + (offset (TRAN s))),(Tape-Chg (s `3 ),(Head s),((TRAN s) `2 ))]

proof end;

Lm14: for tm being TuringStr
for s being All-State of tm
for p being State of tm
for h being Element of INT
for t being Tape of tm
for m, d being Nat st d = h & 0 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,0,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds
t . i = 1 ) holds
ex t1 being Tape of tm st
( (Computation s) . m = [p,(d + m),t1] & ( for i being Integer st d <= i & i < d + m holds
t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds
t1 . i = t . i ) )

proof end;

theorem Th42: :: TURING_1:42

for s being All-State of U3(n)Turing
for t being Tape of U3(n)Turing
for head being Nat
for f being FinSequence of NAT st len f >= 3 & s = [0,head,t] & t storeData <*head*> ^ f holds
( s is Accept-Halt & (Result s) `2 = ((head + (f /. 1)) + (f /. 2)) + 4 & (Result s) `3 storeData <*(((head + (f /. 1)) + (f /. 2)) + 4),(f /. 3)*> )

proof end;

theorem :: TURING_1:43

for n being Nat st n >= 3 holds
U3(n)Turing computes n proj 3

proof end;

definition

let t1, t2 be TuringStr ;
func UnionSt t1,t2 -> non empty finite set equals :: TURING_1:def 23
[:the States of t1,{the InitS of t2}:] \/ [:{the AcceptS of t1},the States of t2:];
correctness ;

end;

:: deftheorem defines UnionSt TURING_1:def 23 :

theorem Th44: :: TURING_1:44

for t1, t2 being TuringStr holds
( [the InitS of t1,the InitS of t2] in UnionSt t1,t2 & [the AcceptS of t1,the AcceptS of t2] in UnionSt t1,t2 )

proof end;

theorem Th45: :: TURING_1:45

for s, t being TuringStr
for x being State of s holds [x,the InitS of t] in UnionSt s,t

proof end;

theorem Th46: :: TURING_1:46

for s, t being TuringStr
for x being State of t holds [the AcceptS of s,x] in UnionSt s,t

proof end;

theorem Th47: :: TURING_1:47

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

proof end;

definition

let s, t be TuringStr ;
let x be Tran-Goal of s;
func FirstTuringTran s,t,x -> Element of [:(UnionSt s,t),(the Symbols of s \/ the Symbols of t),{(- 1),0,1}:] equals :: TURING_1:def 24
[[(x `1 ),the InitS of t],(x `2 ),(x `3 )];
coherence

proof end;

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 :: TURING_1:def 25
[[the AcceptS of s,(x `1 )],(x `2 ),(x `3 )];
coherence

proof end;

end;

:: deftheorem defines SecondTuringTran TURING_1:def 25 :

definition

let s, t be TuringStr ;
let x be Element of UnionSt s,t;
:: original: `1
redefine func x `1 -> State of s;
coherence

proof end;

:: original: `2
redefine func x `2 -> State of t;
coherence

proof end;

end;

definition

let s, t be TuringStr ;
let x be Element of [:(UnionSt s,t),(the Symbols of s \/ the Symbols of t):];
func FirstTuringState x -> State of s equals :: TURING_1:def 26
(x `1 ) `1 ;
correctness ;
func SecondTuringState x -> State of t equals :: TURING_1:def 27
(x `1 ) `2 ;
correctness ;

end;

:: deftheorem defines FirstTuringState TURING_1:def 26 :

:: deftheorem defines SecondTuringState TURING_1:def 27 :

definition

let X, Y, Z be non empty set ;
let x be Element of [:X,(Y \/ Z):];
given u being set , y being Element of Y such that A1: x = [u,y] ;
func FirstTuringSymbol x -> Element of Y equals :Def28: :: TURING_1:def 28
x `2 ;
coherence by A1, MCART_1:def 2;

end;

:: deftheorem Def28 defines FirstTuringSymbol TURING_1:def 28 :

definition

let X, Y, Z be non empty set ;
let x be Element of [:X,(Y \/ Z):];
given u being set , z being Element of Z such that A1: x = [u,z] ;
func SecondTuringSymbol x -> Element of Z equals :Def29: :: TURING_1:def 29
x `2 ;
coherence by A1, MCART_1:def 2;

end;

:: 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: :: TURING_1:def 30
FirstTuringTran s,t,(the Tran of s . [(FirstTuringState x),(FirstTuringSymbol x)]) if ex p being State of s ex y being Symbol of s st
( x = [[p,the InitS of t],y] & p <> the AcceptS of s )
SecondTuringTran s,t,(the Tran of t . [(SecondTuringState x),(SecondTuringSymbol x)]) if ex q being State of t ex y being Symbol of t st x = [[the AcceptS of s,q],y]
otherwise [(x `1 ),(x `2 ),(- 1)];
consistency

proof end;

coherence

proof end;

end;

:: deftheorem Def30 defines Uniontran TURING_1:def 30 :

definition

let s, t be TuringStr ;
func UnionTran s,t -> Function of [:(UnionSt s,t),(the Symbols of s \/ the Symbols of t):],[:(UnionSt s,t),(the Symbols of s \/ the Symbols of t),{(- 1),0,1}:] means :Def31: :: TURING_1:def 31
for x being Element of [:(UnionSt s,t),(the Symbols of s \/ the Symbols of t):] holds it . x = Uniontran s,t,x;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def31 defines UnionTran TURING_1:def 31 :

definition

let T1, T2 be TuringStr ;
func T1 ';' T2 -> strict TuringStr means :Def32: :: TURING_1:def 32
( the Symbols of it = the Symbols of T1 \/ the Symbols of T2 & the States of it = UnionSt T1,T2 & the Tran of it = UnionTran T1,T2 & the InitS of it = [the InitS of T1,the InitS of T2] & the AcceptS of it = [the AcceptS of T1,the AcceptS of T2] );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def32 defines ';' TURING_1:def 32 :

theorem Th48: :: TURING_1:48

for T1, T2 being TuringStr
for g being Tran-Goal of T1
for p being State of T1
for y being Symbol of T1 st p <> the AcceptS of T1 & g = the Tran of T1 . [p,y] holds
the Tran of (T1 ';' T2) . [[p,the InitS of T2],y] = [[(g `1 ),the InitS of T2],(g `2 ),(g `3 )]

proof end;

theorem Th49: :: TURING_1:49

for T1, T2 being TuringStr
for g being Tran-Goal of T2
for q being State of T2
for y being Symbol of T2 st g = the Tran of T2 . [q,y] holds
the Tran of (T1 ';' T2) . [[the AcceptS of T1,q],y] = [[the AcceptS of T1,(g `1 )],(g `2 ),(g `3 )]

proof end;

theorem Th50: :: TURING_1:50

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

proof end;

theorem :: TURING_1:51

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

proof end;

theorem :: TURING_1:52

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

proof end;

theorem Th53: :: TURING_1:53

for f being FinSequence of NAT
for tm1, tm2 being TuringStr
for t1 being Tape of tm1
for t2 being Tape of tm2 st t1 = t2 & t1 storeData f holds
t2 storeData f

proof end;

Lm15: for s being All-State of ZeroTuring
for t being Tape of ZeroTuring
for head, n being Nat st s = [0,head,t] & t storeData <*head,n*> holds
( s is Accept-Halt & (Result s) `2 = head & (Result s) `3 storeData <*head,0*> )

proof end;

theorem :: TURING_1:54

for s being All-State of (ZeroTuring ';' SuccTuring )
for t being Tape of ZeroTuring
for head, n being Nat st s = [[0,0],head,t] & t storeData <*head,n*> holds
( s is Accept-Halt & (Result s) `2 = head & (Result s) `3 storeData <*head,1*> )

proof end;