:: Introduction to Turing Machines :: by Jingchao Chen and Yatsuka Nakamura :: :: Received July 27, 2001 :: Copyright (c) 2001-2012 Association of Mizar Users begin definition let A, B be non empty set ; let f be Function of A,B; let g be PartFunc of A,B; :: original:+* redefine funcf +* g -> Function of A,B; coherence f +* g is Function of A,B proofend; end; definition let X, Y be non empty set ; let a be Element of X; let b be Element of Y; :: original:.--> redefine funca .--> b -> PartFunc of X,Y; coherence a .--> b is PartFunc of X,Y proofend; end; notation let n be Nat; synonym SegM n for succ n; end; definition let n be Nat; :: original:SegM redefine func SegM n -> Subset of NAT equals :: TURING_1:def 1 { k where k is Element of NAT : k <= n } ; coherence SegM n is Subset of NAT proofend; compatibility for b1 being Subset of NAT holds ( b1 = SegM n iff b1 = { k where k is Element of NAT : k <= n } ) by NAT_1:54; end; :: deftheorem defines SegM TURING_1:def_1_:_ for n being Nat holds SegM n = { k where k is Element of NAT : k <= n } ; registration let n be Nat; cluster SegM n -> non empty finite ; coherence ( SegM n is finite & not SegM n is empty ) proofend; end; theorem Th1: :: TURING_1:1 for k, n being Element of NAT holds ( k in SegM n iff k <= n ) proofend; 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] proofend; 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] proofend; notation let i be Nat; let f be FinSequence; synonym Prefix (f,i) for f | i; end; definition let i be Element of NAT ; let f be FinSequence of NAT ; :: original:Prefix redefine func Prefix (f,i) -> FinSequence of INT ; coherence Prefix (f,i) is FinSequence of INT proofend; end; 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 ) proofend; 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 ) proofend; begin definition attrc1 is strict ; struct TuringStr -> ; aggrTuringStr(# 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; 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; 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 2 t +* (h .--> s); coherence t +* (h .--> s) is Tape of T proofend; 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); 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; definition let T be TuringStr ; let g be Tran-Goal of T; func offset g -> Integer equals :: TURING_1:def 3 g `3_3 ; coherence g `3_3 is Integer by ENUMSET1:def_1; 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 ; definition let T be TuringStr ; let s be All-State of T; func Head s -> Integer equals :: TURING_1:def 4 s `2_3 ; coherence s `2_3 is Integer ; end; :: deftheorem defines Head TURING_1:def_4_:_ 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; 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 coherence the Tran of T . [(s `1_3),((s `3_3) . (Head s))] is Tran-Goal of T; proofend; 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))]; definition let T be TuringStr ; 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 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 b1 being All-State of T holds verum; proofend; 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 ) ); 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 :Def7: :: TURING_1:def 7 ( 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) ) ) proofend; 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 proofend; end; :: deftheorem Def7 defines Computation TURING_1:def_7_:_ 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 :: TURING_1:6 for T being TuringStr for s being All-State of T st s `1_3 = the AcceptS of T holds s = Following s by Def6; theorem :: TURING_1:7 for T being TuringStr for s being All-State of T holds (Computation s) . 0 = s by Def7; theorem :: TURING_1:8 for k being Element of NAT for T being TuringStr for s being All-State of T holds (Computation s) . (k + 1) = Following ((Computation s) . k) by Def7; theorem Th9: :: TURING_1:9 for T being TuringStr for s being All-State of T holds (Computation s) . 1 = Following s proofend; theorem Th10: :: TURING_1:10 for i, k being Element of NAT for T being TuringStr for s being All-State of T holds (Computation s) . (i + k) = (Computation ((Computation s) . i)) . k proofend; theorem Th11: :: TURING_1:11 for i, j being Element of 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 proofend; theorem Th12: :: TURING_1:12 for i, j being Element of 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 proofend; definition let T be TuringStr ; let s be All-State of T; attrs is Accept-Halt means :Def8: :: TURING_1:def 8 ex k being Element of NAT st ((Computation s) . k) `1_3 = the AcceptS of T; end; :: deftheorem Def8 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 Element of 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 ; func Result s -> All-State of T means :Def9: :: TURING_1:def 9 ex k being Element of NAT st ( it = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T ); uniqueness for b1, b2 being All-State of T st ex k being Element of NAT st ( b1 = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T ) & ex k being Element of NAT st ( b2 = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T ) holds b1 = b2 proofend; correctness existence ex b1 being All-State of T ex k being Element of NAT st ( b1 = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T ); proofend; end; :: 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 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_3 = the AcceptS of T ) ); 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 Element of NAT st ( ((Computation s) . k) `1_3 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Element of NAT st i < k holds ((Computation s) . i) `1_3 <> the AcceptS of T ) ) proofend; 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 10 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] proofend; 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 proofend; 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 b4 being Function of A,[:A,B:] holds ( b4 = id (A,B,y) iff for x being Element of A holds b4 . x = [x,y] ); definition func Sum_Tran -> Function of [:(SegM 5),{0,1}:],[:(SegM 5),{0,1},{(- 1),0,1}:] equals :: TURING_1:def 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]) is Function of [:(SegM 5),{0,1}:],[:(SegM 5),{0,1},{(- 1),0,1}:] proofend; 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]); 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] ) proofend; definition let T be TuringStr ; let t be Tape of T; let i, j be Integer; predt is_1_between i,j means :Def12: :: TURING_1:def 12 ( t . i = 0 & t . j = 0 & ( for k being Integer st i < k & k < j holds t . k = 1 ) ); end; :: deftheorem Def12 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 ) ) ); definition let f be FinSequence of NAT ; let T be TuringStr ; let t be Tape of T; predt storeData f means :Def13: :: TURING_1:def 13 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); end; :: deftheorem Def13 defines storeData TURING_1:def_13_:_ 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 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 proofend; 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*> proofend; 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 ) ) proofend; 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 ) proofend; 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 ) ) proofend; 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) ) proofend; 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) ) proofend; 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 proofend; 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 ) proofend; begin definition 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 ex b1 being strict TuringStr st ( 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 ) proofend; uniqueness for b1, b2 being strict TuringStr st 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 & the Symbols of b2 = {0,1} & the FStates of b2 = SegM 5 & the Tran of b2 = Sum_Tran & the InitS of b2 = 0 & the AcceptS of b2 = 5 holds b1 = b2 ; end; :: deftheorem Def14 defines SumTuring TURING_1:def_14_:_ 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 proofend; 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 proofend; Lm2: ( 0 in the Symbols of SumTuring & 1 in the Symbols of SumTuring ) proofend; theorem Th25: :: TURING_1:25 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_3),((Head s) + (offset (TRAN s))),(Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)))] proofend; 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)))] proofend; 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 set holds ( (Tape-Chg (t,h,s)) . h = s & ( i <> h implies (Tape-Chg (t,h,s)) . i = t . i ) ) proofend; 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] proofend; 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)*> ) proofend; definition let T be TuringStr ; let F be Function; predT computes F means :Def15: :: 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*> ) ); end; :: deftheorem Def15 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*> ) ) ); theorem Th28: :: TURING_1:28 dom [+] c= 2 -tuples_on NAT proofend; theorem :: TURING_1:29 SumTuring computes [+] proofend; begin definition 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]) is Function of [:(SegM 4),{0,1}:],[:(SegM 4),{0,1},{(- 1),0,1}:] proofend; 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]); 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] ) proofend; definition 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 ex b1 being strict TuringStr st ( 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 ) proofend; uniqueness for b1, b2 being strict TuringStr st 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 & the Symbols of b2 = {0,1} & the FStates of b2 = SegM 4 & the Tran of b2 = Succ_Tran & the InitS of b2 = 0 & the AcceptS of b2 = 4 holds b1 = b2 ; end; :: deftheorem Def17 defines SuccTuring TURING_1:def_17_:_ 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 proofend; Lm6: ( 0 in the Symbols of SuccTuring & 1 in the Symbols of SuccTuring ) proofend; 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)))] proofend; 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)*> ) proofend; theorem :: TURING_1:32 SuccTuring computes 1 succ 1 proofend; begin definition 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)]) is Function of [:(SegM 4),{0,1}:],[:(SegM 4),{0,1},{(- 1),0,1}:] proofend; 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)]); 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)] ) proofend; definition 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 ex b1 being strict TuringStr st ( 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 ) proofend; uniqueness for b1, b2 being strict TuringStr st 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 & the Symbols of b2 = {0,1} & the FStates of b2 = SegM 4 & the Tran of b2 = Zero_Tran & the InitS of b2 = 0 & the AcceptS of b2 = 4 holds b1 = b2 ; end; :: deftheorem Def19 defines ZeroTuring TURING_1:def_19_:_ 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 proofend; Lm9: ( 0 in the Symbols of ZeroTuring & 1 in the Symbols of ZeroTuring ) proofend; 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)))] proofend; 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*> ) proofend; theorem :: TURING_1:35 for n being Element of NAT st n >= 1 holds ZeroTuring computes n const 0 proofend; begin definition 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]) is Function of [:(SegM 3),{0,1}:],[:(SegM 3),{0,1},{(- 1),0,1}:] proofend; 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]); 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] ) proofend; definition 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 ex b1 being strict TuringStr st ( 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 ) proofend; uniqueness for b1, b2 being strict TuringStr st 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 & the Symbols of b2 = {0,1} & the FStates of b2 = SegM 3 & the Tran of b2 = U3(n)Tran & the InitS of b2 = 0 & the AcceptS of b2 = 3 holds b1 = b2 ; end; :: deftheorem Def21 defines U3(n)Turing TURING_1:def_21_:_ 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 proofend; Lm12: ( 0 in the Symbols of U3(n)Turing & 1 in the Symbols of U3(n)Turing ) proofend; 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)))] proofend; 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 ) ) proofend; 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)*> ) proofend; theorem :: TURING_1:38 for n being Element of NAT st n >= 3 holds U3(n)Turing computes n proj 3 proofend; begin definition let t1, t2 be TuringStr ; 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 coherence [: the FStates of t1,{ the InitS of t2}:] \/ [:{ the AcceptS of t1}, the FStates of t2:] is non empty finite set ; ; end; :: 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:]; 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) ) proofend; theorem Th40: :: TURING_1:40 for s, t being TuringStr for x being State of s holds [x, the InitS of t] in UnionSt (s,t) proofend; theorem Th41: :: TURING_1:41 for s, t being TuringStr for x being State of t holds [ the AcceptS of s,x] in UnionSt (s,t) proofend; 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] proofend; 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 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)] is Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:] proofend; 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)]; 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 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)] is Element of [:(UnionSt (s,t)),( the Symbols of s \/ the Symbols of t),{(- 1),0,1}:] proofend; 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)]; definition let s, t be TuringStr ; let x be Element of UnionSt (s,t); :: original:`1 redefine funcx `1 -> State of s; coherence x `1 is State of s proofend; :: original:`2 redefine funcx `2 -> State of t; coherence x `2 is State of t proofend; 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 25 (x `1) `1 ; correctness coherence (x `1) `1 is State of s; ; func SecondTuringState x -> State of t equals :: TURING_1:def 26 (x `1) `2 ; correctness coherence (x `1) `2 is State of t; ; end; :: 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 ; :: 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 ; 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] ; A2: [u,y] `2 = y ; func FirstTuringSymbol x -> Element of Y equals :Def27: :: TURING_1:def 27 x `2 ; coherence x `2 is Element of Y by A1, A2; end; :: 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 ; 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] ; A2: [u,z] `2 = z ; func SecondTuringSymbol x -> Element of Z equals :Def28: :: TURING_1:def 28 x `2 ; coherence x `2 is Element of Z by A1, A2; end; :: 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 ; 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 :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 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)])) ) proofend; 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}:] ) ) proofend; 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)] ) ); 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 :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 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) proofend; 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 proofend; end; :: deftheorem Def30 defines UnionTran TURING_1:def_30_:_ 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 ; funcT1 ';' 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 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] ) proofend; 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 Def31 defines ';' TURING_1:def_31_:_ 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 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)] proofend; 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)] proofend; 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 ) proofend; 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) proofend; 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 ) proofend; 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 proofend; 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*> ) proofend; 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*> ) proofend;