turing_1.miz



    begin

    reserve n,i,j,k for Nat;

    definition

      let A,B be non empty set, f be Function of A, B, g be PartFunc of A, B;

      :: original: +*

      redefine

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

      coherence

      proof

         A1:

        now

          let x be object;

          assume

           A2: x in A;

          per cases ;

            suppose

             A3: x in ( dom g);

            then ((f +* g) . x) = (g . x) by FUNCT_4: 13;

            hence ((f +* g) . x) in B by A3, PARTFUN1: 4;

          end;

            suppose not x in ( dom g);

            then ((f +* g) . x) = (f . x) by FUNCT_4: 11;

            hence ((f +* g) . x) in B by A2, FUNCT_2: 5;

          end;

        end;

        

         A4: ( dom f) = A & ( dom g) c= A by FUNCT_2:def 1, RELAT_1:def 18;

        ( dom (f +* g)) = (( dom f) \/ ( dom g)) by FUNCT_4:def 1

        .= A by A4, XBOOLE_1: 12;

        hence thesis by A1, FUNCT_2: 3;

      end;

    end

    definition

      let X,Y be non empty set, a be Element of X, b be Element of Y;

      :: original: .-->

      redefine

      func a .--> b -> PartFunc of X, Y ;

      coherence

      proof

        set p = (a .--> b);

        ( dom p) = {a} & ( rng p) = {b} by FUNCOP_1: 8;

        then ( dom p) c= X & ( rng p) c= Y;

        hence thesis by RELSET_1: 4;

      end;

    end

    notation

      let n be Nat;

      synonym SegM n for succ n;

    end

    definition

      let n be Nat;

      :: original: SegM

      redefine

      :: TURING_1:def1

      func SegM n -> Subset of NAT equals { k where k be Nat : k <= n };

      coherence

      proof

        ( SegM n) c= NAT ;

        hence thesis;

      end;

      compatibility

      proof

        let S be Subset of NAT ;

        ( SegM ( Segm n)) = { k where k be Nat : k <= n } by NAT_1: 54;

        hence thesis;

      end;

    end

    theorem :: TURING_1:1

    

     Th1: k in ( SegM n) iff k <= n

    proof

      thus k in ( SegM n) implies k <= n

      proof

        assume k in ( SegM n);

        then ex i be Nat st k = i & i <= n;

        hence thesis;

      end;

      thus thesis;

    end;

    theorem :: TURING_1:2

    

     Th2: for f be Function, x,y,z,u,v be object st u <> x holds ((f +* ( [x, y] .--> z)) . [u, v]) = (f . [u, v])

    proof

      let f be Function, x,y,z,u,v be object;

      set p = ( [x, y] .--> z);

      assume u <> x;

      then

       A1: [u, v] <> [x, y] by XTUPLE_0: 1;

       not [u, v] in ( dom p) by A1, TARSKI:def 1;

      hence thesis by FUNCT_4: 11;

    end;

    theorem :: TURING_1:3

    

     Th3: for f be Function, x,y,z,u,v be object st v <> y holds ((f +* ( [x, y] .--> z)) . [u, v]) = (f . [u, v])

    proof

      let f be Function, x,y,z,u,v be object;

      set p = ( [x, y] .--> z);

      assume v <> y;

      then

       A1: [u, v] <> [x, y] by XTUPLE_0: 1;

       not [u, v] in ( dom p) by A1, TARSKI:def 1;

      hence thesis by FUNCT_4: 11;

    end;

    notation

      let i be Nat, f be FinSequence;

      synonym Prefix (f,i) for f | i;

    end

    registration

      let f be natural-valued FinSequence, n be Nat;

      cluster ( Prefix (f,n)) -> INT -valued;

      coherence ;

    end

    theorem :: TURING_1:4

    

     Th4: for x1,x2 be Element of NAT holds ( Sum ( Prefix ( <*x1, x2*>,1))) = x1 & ( Sum ( Prefix ( <*x1, x2*>,2))) = (x1 + x2)

    proof

      let x1,x2 be Element of NAT ;

      reconsider y1 = x1 as Element of INT by INT_1:def 2;

      

      thus ( Sum ( Prefix ( <*x1, x2*>,1))) = ( Sum <*y1*>) by FINSEQ_6: 3

      .= x1 by FINSOP_1: 11;

      reconsider y2 = x2 as Element of INT by INT_1:def 2;

      ( len <*x1, x2*>) = 2 by FINSEQ_1: 44;

      

      hence ( Sum ( Prefix ( <*x1, x2*>,2))) = ( Sum <*y1, y2*>) by FINSEQ_3: 49

      .= (x1 + x2) by RVSUM_1: 77;

    end;

    theorem :: TURING_1:5

    

     Th5: for x1,x2,x3 be 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)

    proof

      let x1,x2,x3 be Element of NAT ;

      reconsider y1 = x1 as Element of INT by INT_1:def 2;

      

      thus ( Sum ( Prefix ( <*x1, x2, x3*>,1))) = ( Sum <*y1*>) by FINSEQ_6: 4

      .= x1 by FINSOP_1: 11;

      reconsider y2 = x2 as Element of INT by INT_1:def 2;

      

      thus ( Sum ( Prefix ( <*x1, x2, x3*>,2))) = ( Sum <*y1, y2*>) by FINSEQ_6: 5

      .= (x1 + x2) by RVSUM_1: 77;

      reconsider y3 = x3 as Element of INT by INT_1:def 2;

      ( len <*x1, x2, x3*>) = 3 by FINSEQ_1: 45;

      

      hence ( Sum ( Prefix ( <*x1, x2, x3*>,3))) = ( Sum <*y1, y2, y3*>) by FINSEQ_3: 49

      .= ((x1 + x2) + x3) by RVSUM_1: 78;

    end;

    begin

    definition

      struct TuringStr (# the Symbols, FStates -> finite non empty set,

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

the InitS, AcceptS -> Element of the FStates #)

       attr strict strict;

    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, t be Tape of T, h be Integer, s be Symbol of T;

      :: TURING_1:def2

      func Tape-Chg (t,h,s) -> Tape of T equals (t +* (h .--> s));

      coherence

      proof

        set X = INT , Y = the Symbols of T;

        

         A1: ex f be Function st t = f & ( dom f) = X & ( rng f) c= Y by FUNCT_2:def 2;

        ( rng (h .--> s)) = {s} by FUNCOP_1: 8;

        then ( rng (t +* (h .--> s))) c= (( rng t) \/ ( rng (h .--> s))) & (( rng t) \/ ( rng (h .--> s))) c= Y by A1, FUNCT_4: 17, XBOOLE_1: 8;

        then

         A2: ( rng (t +* (h .--> s))) c= Y by XBOOLE_1: 1;

        

         A3: h in INT by INT_1:def 2;

        ( dom (t +* (h .--> s))) = (( dom t) \/ ( dom (h .--> s))) by FUNCT_4:def 1

        .= (( dom t) \/ {h})

        .= X by A1, A3, ZFMISC_1: 40;

        hence thesis by A2, FUNCT_2:def 2;

      end;

    end

    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, g be Tran-Goal of T;

      :: TURING_1:def3

      func offset (g) -> Integer equals (g `3_3 );

      coherence by ENUMSET1:def 1;

    end

    definition

      let T be TuringStr, s be All-State of T;

      :: TURING_1:def4

      func Head (s) -> Integer equals (s `2_3 );

      coherence ;

    end

    definition

      let T be TuringStr, s be All-State of T;

      :: TURING_1:def5

      func TRAN (s) -> Tran-Goal of T equals (the Tran of T . [(s `1_3 ), ((s `3_3 ) qua Tape of T . ( Head s))]);

      correctness

      proof

        reconsider x = ( Head s) as Element of INT ;

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

        hence thesis;

      end;

    end

    definition

      let T be TuringStr, s be All-State of T;

      :: TURING_1:def6

      func Following s -> All-State of T equals

      : Def6: [(( 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

      proof

        (( Head s) + ( offset ( TRAN s))) in INT by INT_1:def 2;

        hence thesis by MCART_1: 69;

      end;

    end

    definition

      let T be TuringStr, s be All-State of T;

      :: TURING_1:def7

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

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

      existence

      proof

        deffunc U( set, All-State of T) = ( Following $2);

        consider f be sequence of [:the FStates of T, INT , ( Funcs ( INT ,the Symbols of T)):] such that

         A1: (f . 0 ) = s & for n be Nat holds (f . (n + 1)) = U(n,.) from NAT_1:sch 12;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        deffunc U( set, All-State of T) = ( Following $2);

        let F1,F2 be sequence of [:the FStates of T, INT , ( Funcs ( INT ,the Symbols of T)):] such that

         A2: (F1 . 0 ) = s and

         A3: for i be Nat holds (F1 . (i + 1)) = ( Following (F1 . i)) and

         A4: (F2 . 0 ) = s and

         A5: for i be Nat holds (F2 . (i + 1)) = ( Following (F2 . i));

        

         A6: for i be Nat holds (F1 . (i + 1)) = U(i,.) by A3;

        

         A7: for i be Nat holds (F2 . (i + 1)) = U(i,.) by A5;

        

         A8: (F2 . 0 ) = s by A4;

        

         A9: (F1 . 0 ) = s by A2;

        thus F1 = F2 from NAT_1:sch 16( A9, A6, A8, A7);

      end;

    end

    reserve T for TuringStr,

s for All-State of T;

    theorem :: TURING_1:6

    for T be TuringStr, s be All-State of T st (s `1_3 ) = the AcceptS of T holds s = ( Following s) by Def6;

    theorem :: TURING_1:7

    (( Computation s) . 0 ) = s by Def7;

    theorem :: TURING_1:8

    (( Computation s) . (k + 1)) = ( Following (( Computation s) . k)) by Def7;

    theorem :: TURING_1:9

    

     Th9: (( Computation s) . 1) = ( Following s)

    proof

      (( Computation s) . ( 0 + 1)) = ( Following (( Computation s) . 0 )) by Def7

      .= ( Following s) by Def7;

      hence thesis;

    end;

    theorem :: TURING_1:10

    

     Th10: (( Computation s) . (i + k)) = (( Computation (( Computation s) . i)) . k)

    proof

      defpred X[ Nat] means (( Computation s) . (i + $1)) = (( Computation (( Computation s) . i)) . $1);

      

       A1: for k st X[k] holds X[(k + 1)]

      proof

        let k;

        assume

         A2: (( Computation s) . (i + k)) = (( Computation (( Computation s) . i)) . k);

        

        thus (( Computation s) . (i + (k + 1))) = (( Computation s) . ((i + k) + 1))

        .= ( Following (( Computation s) . (i + k))) by Def7

        .= (( Computation (( Computation s) . i)) . (k + 1)) by A2, Def7;

      end;

      

       A3: X[ 0 ] by Def7;

      for k holds X[k] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: TURING_1:11

    

     Th11: i <= j & ( Following (( Computation s) . i)) = (( Computation s) . i) implies (( Computation s) . j) = (( Computation s) . i)

    proof

      assume that

       A1: i <= j and

       A2: ( Following (( Computation s) . i)) = (( Computation s) . i);

      consider k be Nat such that

       A3: j = (i + k) by A1, NAT_1: 10;

      defpred X[ Nat] means (( Computation s) . (i + $1)) = (( Computation s) . i);

      

       A4: for k st X[k] holds X[(k + 1)]

      proof

        let k;

        assume

         A5: (( Computation s) . (i + k)) = (( Computation s) . i);

        

        thus (( Computation s) . (i + (k + 1))) = (( Computation s) . ((i + k) + 1))

        .= (( Computation s) . i) by A2, A5, Def7;

      end;

      

       A6: X[ 0 ];

      

       A7: for k holds X[k] from NAT_1:sch 2( A6, A4);

      thus thesis by A3, A7;

    end;

    theorem :: TURING_1:12

    

     Th12: i <= j & ((( Computation s) . i) `1_3 ) = the AcceptS of T implies (( Computation s) . j) = (( Computation s) . i)

    proof

      assume that

       A1: i <= j and

       A2: ((( Computation s) . i) `1_3 ) = the AcceptS of T;

      ( Following (( Computation s) . i)) = (( Computation s) . i) by A2, Def6;

      hence thesis by A1, Th11;

    end;

    definition

      let T be TuringStr, s be All-State of T;

      :: TURING_1:def8

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

    end

    definition

      let T be TuringStr, s be All-State of T;

      :: TURING_1:def9

      func Result s -> All-State of T means

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

      uniqueness

      proof

        let s1,s2 be All-State of T;

        given k1 be Nat such that

         A2: s1 = (( Computation s) . k1) & ((( Computation s) . k1) `1_3 ) = the AcceptS of T;

        given k2 be Nat such that

         A3: s2 = (( Computation s) . k2) & ((( Computation s) . k2) `1_3 ) = the AcceptS of T;

        k1 <= k2 or k2 <= k1;

        hence thesis by A2, A3, Th12;

      end;

      correctness by A1;

    end

    theorem :: TURING_1:13

    

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

    proof

      let T be TuringStr, s be All-State of T;

      defpred P[ Nat] means ((( Computation s) . $1) `1_3 ) = the AcceptS of T;

      assume

       A1: s is Accept-Halt;

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

      then

       A2: ex k be Nat st P[k];

      consider k be Nat such that

       A3: P[k] & for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A2);

      reconsider k as Element of NAT by ORDINAL1:def 12;

      take k;

      thus P[k] by A3;

      thus ( Result s) = (( Computation s) . k) by A1, A3, Def9;

      thus thesis by A3;

    end;

    definition

      let A,B be non empty set, y be set;

      :: TURING_1:def10

      func id (A,B,y) -> Function of A, [:A, B:] means for x be Element of A holds (it . x) = [x, y];

      existence

      proof

        reconsider yy = y as Element of B by A1;

        deffunc U( Element of A) = [$1, yy];

        consider f be Function of A, [:A, B:] such that

         A2: for x be Element of A holds (f . x) = U(x) from FUNCT_2:sch 4;

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        deffunc U( Element of A) = [$1, y];

        thus for f1,f2 be Function of A, [:A, B:] st (for x be Element of A holds (f1 . x) = U(x)) & (for x be Element of A holds (f2 . x) = U(x)) holds f1 = f2 from BINOP_2:sch 1;

      end;

    end

    definition

      :: TURING_1:def11

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

      coherence

      proof

        reconsider p0 = 0 , p1 = 1, p2 = 2, p3 = 3, p4 = 4, p5 = 5 as Element of ( SegM 5) by Th1;

        set A = [:( SegM 5), { 0 , 1}:], B = {( - 1), 0 , 1}, C = [:( SegM 5), { 0 , 1}, B:];

        reconsider b0 = 0 , b1 = 1 as Element of { 0 , 1} by TARSKI:def 2;

        reconsider L = ( - 1) as Element of B by ENUMSET1:def 1;

        reconsider h = 0 , R = 1 as Element of {( - 1), 0 , 1} by ENUMSET1:def 1;

        C = [:A, B:] by ZFMISC_1:def 3;

        then

        reconsider OP = ( id (A,B,h)) as Function of A, C;

        (((((((((( id (A,B, 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 ])) = (((((((((OP +* ( [p0, b0] .--> [p0, b0, R])) +* ( [p0, b1] .--> [p1, b0, R])) +* ( [p1, b1] .--> [p1, b1, R])) +* ( [p1, b0] .--> [p2, b1, R])) +* ( [p2, b1] .--> [p2, b1, R])) +* ( [p2, b0] .--> [p3, b0, L])) +* ( [p3, b1] .--> [p4, b0, L])) +* ( [p4, b1] .--> [p4, b1, L])) +* ( [p4, b0] .--> [p5, b0, h]));

        hence thesis;

      end;

    end

    theorem :: TURING_1:14

    

     Th14: ( 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

      set x = [ 0 , 1];

      set x1 = [ 0 , 0 ];

      set p1 = ( [ 0 , 0 ] .--> [ 0 , 0 , 1]), p2 = ( [ 0 , 1] .--> [1, 0 , 1]), p3 = ( [1, 1] .--> [1, 1, 1]), p4 = ( [1, 0 ] .--> [2, 1, 1]), p5 = ( [2, 1] .--> [2, 1, 1]), p6 = ( [2, 0 ] .--> [3, 0 , ( - 1)]), p7 = ( [3, 1] .--> [4, 0 , ( - 1)]), p8 = ( [4, 1] .--> [4, 1, ( - 1)]), f = ( id ( [:( SegM 5), { 0 , 1}:], {( - 1), 0 , 1}, 0 ));

      

      thus ( Sum_Tran . x1) = (((((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) +* p7) +* p8) . x1) by Th2

      .= ((((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) +* p7) . x1) by Th2

      .= (((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) . x1) by Th2

      .= ((((((f +* p1) +* p2) +* p3) +* p4) +* p5) . x1) by Th2

      .= (((((f +* p1) +* p2) +* p3) +* p4) . x1) by Th2

      .= ((((f +* p1) +* p2) +* p3) . x1) by Th2

      .= (((f +* p1) +* p2) . x1) by Th2

      .= ((f +* p1) . x1) by Th3

      .= [ 0 , 0 , 1] by FUNCT_7: 94;

      

      thus ( Sum_Tran . x) = (((((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) +* p7) +* p8) . x) by Th2

      .= ((((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) +* p7) . x) by Th2

      .= (((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) . x) by Th2

      .= ((((((f +* p1) +* p2) +* p3) +* p4) +* p5) . x) by Th2

      .= (((((f +* p1) +* p2) +* p3) +* p4) . x) by Th2

      .= ((((f +* p1) +* p2) +* p3) . x) by Th2

      .= (((f +* p1) +* p2) . x) by Th2

      .= [1, 0 , 1] by FUNCT_7: 94;

      set x = [1, 1];

      

      thus ( Sum_Tran . x) = (((((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) +* p7) +* p8) . x) by Th2

      .= ((((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) +* p7) . x) by Th2

      .= (((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) . x) by Th2

      .= ((((((f +* p1) +* p2) +* p3) +* p4) +* p5) . x) by Th2

      .= (((((f +* p1) +* p2) +* p3) +* p4) . x) by Th2

      .= ((((f +* p1) +* p2) +* p3) . x) by Th3

      .= [1, 1, 1] by FUNCT_7: 94;

      set x = [1, 0 ];

      

      thus ( Sum_Tran . x) = (((((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) +* p7) +* p8) . x) by Th2

      .= ((((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) +* p7) . x) by Th2

      .= (((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) . x) by Th2

      .= ((((((f +* p1) +* p2) +* p3) +* p4) +* p5) . x) by Th2

      .= (((((f +* p1) +* p2) +* p3) +* p4) . x) by Th2

      .= [2, 1, 1] by FUNCT_7: 94;

      set x = [2, 1];

      

      thus ( Sum_Tran . x) = (((((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) +* p7) +* p8) . x) by Th2

      .= ((((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) +* p7) . x) by Th2

      .= (((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) . x) by Th2

      .= ((((((f +* p1) +* p2) +* p3) +* p4) +* p5) . x) by Th3

      .= [2, 1, 1] by FUNCT_7: 94;

      set x = [2, 0 ];

      

      thus ( Sum_Tran . x) = (((((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) +* p7) +* p8) . x) by Th2

      .= ((((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) +* p7) . x) by Th2

      .= (((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) . x) by Th2

      .= [3, 0 , ( - 1)] by FUNCT_7: 94;

      set x = [3, 1];

      

      thus ( Sum_Tran . x) = (((((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) +* p7) +* p8) . x) by Th2

      .= ((((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) +* p7) . x) by Th2

      .= [4, 0 , ( - 1)] by FUNCT_7: 94;

      set x = [4, 1];

      

      thus ( Sum_Tran . x) = (((((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) +* p7) +* p8) . x) by Th3

      .= [4, 1, ( - 1)] by FUNCT_7: 94;

      thus thesis by FUNCT_7: 94;

    end;

    definition

      let T be TuringStr, t be Tape of T, i,j be Integer;

      :: TURING_1:def12

      pred t is_1_between i,j means (t . i) = 0 & (t . j) = 0 & for k be Integer st i < k & k < j holds (t . k) = 1;

    end

    definition

      let f be natural-valued FinSequence, T be TuringStr, t be Tape of T;

      :: TURING_1:def13

      pred t storeData f means for i be 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

    theorem :: TURING_1:15

    

     Th15: for T be TuringStr, t be Tape of T, s,n be Element of NAT st t storeData <*s, n*> holds t is_1_between (s,((s + n) + 2))

    proof

      let T be TuringStr, t be Tape of T, s,n be Element of NAT ;

      set f = <*s, n*>;

      assume

       A1: t storeData f;

      

       A2: ( len f) = 2 by FINSEQ_1: 44;

      (( Sum ( Prefix (f,1))) + (2 * (1 - 1))) = s & (( Sum ( Prefix (f,(1 + 1)))) + (2 * 1)) = ((s + n) + 2) by Th4;

      hence thesis by A1, A2;

    end;

    theorem :: TURING_1:16

    

     Th16: for T be TuringStr, t be Tape of T, s,n be Element of NAT st t is_1_between (s,((s + n) + 2)) holds t storeData <*s, n*>

    proof

      let T be TuringStr, t be Tape of T, s,n be Element of NAT ;

      set f = <*s, n*>;

      assume

       A1: t is_1_between (s,((s + n) + 2));

      

       A2: (( Sum ( Prefix (f,(1 + 1)))) + (2 * 1)) = ((s + n) + 2) by Th4;

      now

        let i be Nat;

        assume that

         A3: 1 <= i and

         A4: i < ( len f);

        ( len f) = 2 by FINSEQ_1: 44;

        then (i + 1) <= (1 + 1) by A4, INT_1: 7;

        then i <= 1 by XREAL_1: 6;

        then i = 1 by A3, XXREAL_0: 1;

        hence t is_1_between ((( Sum ( Prefix (f,i))) + (2 * (i - 1))),(( Sum ( Prefix (f,(i + 1)))) + (2 * i))) by A1, A2, Th4;

      end;

      hence thesis;

    end;

    theorem :: TURING_1:17

    

     Th17: for T be TuringStr, t be Tape of T, s,n be Element of NAT st t storeData <*s, n*> holds (t . s) = 0 & (t . ((s + n) + 2)) = 0 & for i be Integer st s < i & i < ((s + n) + 2) holds (t . i) = 1

    proof

      let T be TuringStr, t be Tape of T, s,n be Element of NAT ;

      assume t storeData <*s, n*>;

      then

       A1: t is_1_between (s,((s + n) + 2)) by Th15;

      hence (t . s) = 0 & (t . ((s + n) + 2)) = 0 ;

      thus thesis by A1;

    end;

    theorem :: TURING_1:18

    

     Th18: for T be TuringStr, t be Tape of T, s,n1,n2 be 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

      let T be TuringStr, t be Tape of T, s,n1,n2 be Element of NAT ;

      set f = <*s, n1, n2*>;

      assume

       A1: t storeData f;

      

       A2: ( len f) = 3 by FINSEQ_1: 45;

      (( Sum ( Prefix (f,1))) + (2 * (1 - 1))) = s & (( Sum ( Prefix (f,(1 + 1)))) + (2 * 1)) = ((s + n1) + 2) by Th5;

      hence t is_1_between (s,((s + n1) + 2)) by A1, A2;

      (( Sum ( Prefix (f,2))) + (2 * (2 - 1))) = ((s + n1) + 2) & (( Sum ( Prefix (f,(2 + 1)))) + (2 * 2)) = (((s + n1) + n2) + 4) by Th5;

      hence thesis by A1, A2;

    end;

    theorem :: TURING_1:19

    

     Th19: for T be TuringStr, t be Tape of T, s,n1,n2 be 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 be Integer st s < i & i < ((s + n1) + 2) holds (t . i) = 1) & for i be Integer st ((s + n1) + 2) < i & i < (((s + n1) + n2) + 4) holds (t . i) = 1

    proof

      let T be TuringStr, t be Tape of T, s,n1,n2 be Element of NAT ;

      assume t storeData <*s, n1, n2*>;

      then

       A1: t is_1_between (s,((s + n1) + 2)) & t is_1_between (((s + n1) + 2),(((s + n1) + n2) + 4)) by Th18;

      hence (t . s) = 0 & (t . ((s + n1) + 2)) = 0 & (t . (((s + n1) + n2) + 4)) = 0 ;

      thus thesis by A1;

    end;

    theorem :: TURING_1:20

    

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

    proof

      let f be FinSequence of NAT , s be Element of NAT ;

      set g = <*s*>, h = (g ^ f);

      reconsider x1 = s as Element of INT by INT_1:def 2;

      reconsider x2 = (f /. 1) as Element of INT by INT_1:def 2;

      assume

       A1: ( len f) >= 1;

      then

      consider n be Nat such that

       A2: ( len f) = (1 + n) by NAT_1: 10;

      

       A3: ( len g) = 1 by FINSEQ_1: 39;

      then ( Seg 1) = ( dom g) by FINSEQ_1:def 3;

      

      hence ( Sum ( Prefix (h,1))) = ( Sum <*x1*>) by FINSEQ_1: 21

      .= s by FINSOP_1: 11;

      ( len h) = (1 + ( len f)) by A3, FINSEQ_1: 22

      .= (2 + n) by A2;

      then

      consider p2,q2 be FinSequence of NAT such that

       A4: ( len p2) = 2 and ( len q2) = n and

       A5: h = (p2 ^ q2) by FINSEQ_2: 23;

      (f /. 1) = (f . 1) by A1, FINSEQ_4: 15

      .= (h . (1 + 1)) by A1, A3, FINSEQ_7: 3;

      then

       A6: (p2 . 2) = (f /. 1) by A4, A5, FINSEQ_1: 64;

      ( Seg 2) = ( dom p2) by A4, FINSEQ_1:def 3;

      then

       A7: p2 = ( Prefix (h,2)) by A5, FINSEQ_1: 21;

      (h . 1) = s by FINSEQ_1: 41;

      then (p2 . 1) = s by A4, A5, FINSEQ_1: 64;

      

      hence ( Sum ( Prefix (h,2))) = ( Sum <*x1, x2*>) by A4, A7, A6, FINSEQ_1: 44

      .= (s + (f /. 1)) by RVSUM_1: 77;

    end;

    theorem :: TURING_1:21

    

     Th21: for f be FinSequence of NAT , s be 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

      let f be FinSequence of NAT , s be Element of NAT ;

      set g = <*s*>, h = (g ^ f);

      reconsider x1 = s as Element of INT by INT_1:def 2;

      reconsider x2 = (f /. 1) as Element of INT by INT_1:def 2;

      reconsider x3 = (f /. 2) as Element of INT by INT_1:def 2;

      reconsider x4 = (f /. 3) as Element of INT by INT_1:def 2;

      assume

       A1: ( len f) >= 3;

      then

      consider n be Nat such that

       A2: ( len f) = (3 + n) by NAT_1: 10;

      reconsider n as Element of NAT by ORDINAL1:def 12;

      

       A3: ( len g) = 1 by FINSEQ_1: 39;

      

      then

       A4: ( len h) = (1 + ( len f)) by FINSEQ_1: 22

      .= (4 + n) by A2;

      then

      consider p4,q4 be FinSequence of NAT such that

       A5: ( len p4) = 4 and ( len q4) = n and

       A6: h = (p4 ^ q4) by FINSEQ_2: 23;

      (f /. 3) = (f . 3) by A1, FINSEQ_4: 15

      .= (h . (1 + 3)) by A1, A3, FINSEQ_7: 3;

      then

       A7: (p4 . 4) = (f /. 3) by A5, A6, FINSEQ_1: 64;

      ( Seg 4) = ( dom p4) by A5, FINSEQ_1:def 3;

      then

       A8: p4 = ( Prefix (h,4)) by A6, FINSEQ_1: 21;

      

       A9: 1 <= ( len f) by A1, XXREAL_0: 2;

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

      ( len h) = (3 + (1 + n)) by A4;

      then

      consider p3,q3 be FinSequence of NAT such that

       A10: ( len p3) = 3 and ( len q3) = (1 + n) and

       A11: h = (p3 ^ q3) by FINSEQ_2: 23;

      

       A12: (f /. 1) = (f . 1) by A9, FINSEQ_4: 15

      .= (h . (1 + 1)) by A9, A3, FINSEQ_7: 3;

      then

       A13: (p4 . 2) = (f /. 1) by A5, A6, FINSEQ_1: 64;

      

       A14: 2 <= ( len f) by A1, XXREAL_0: 2;

      

      then

       A15: (f /. 2) = (f . 2) by FINSEQ_4: 15

      .= (h . (1 + 2)) by A3, A14, FINSEQ_7: 3;

      then

       A16: (p4 . 3) = (f /. 2) by A5, A6, FINSEQ_1: 64;

      

       A17: (p3 . 2) = (f /. 1) by A12, A10, A11, FINSEQ_1: 64;

      ( Seg 3) = ( dom p3) by A10, FINSEQ_1:def 3;

      then

       A18: p3 = ( Prefix (h,3)) by A11, FINSEQ_1: 21;

      

       A19: (p3 . 3) = (f /. 2) by A15, A10, A11, FINSEQ_1: 64;

      

       A20: (h . 1) = s by FINSEQ_1: 41;

      then (p3 . 1) = s by A10, A11, FINSEQ_1: 64;

      then p3 = <*s, (f /. 1), (f /. 2)*> by A10, A17, A19, FINSEQ_1: 45;

      hence ( Sum ( Prefix (h,3))) = ((s + (f /. 1)) + (f /. 2)) by A18, RVSUM_1: 78;

      (p4 . 1) = s by A20, A5, A6, FINSEQ_1: 64;

      then p4 = <*s, (f /. 1), (f /. 2), (f /. 3)*> by A5, A13, A16, A7, FINSEQ_4: 76;

      

      hence ( Sum ( Prefix (h,4))) = (((x1 + x2) + x3) + x4) by A8, RVSUM_1: 142

      .= (((s + (f /. 1)) + (f /. 2)) + (f /. 3));

    end;

    theorem :: TURING_1:22

    

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

    proof

      let T be TuringStr, t be Tape of T, s be Element of NAT , f be FinSequence of NAT ;

      set g = ( <*s*> ^ f);

      assume that

       A1: ( len f) >= 1 and

       A2: t storeData g;

      ( len <*s*>) = 1 by FINSEQ_1: 39;

      then ( len g) = (1 + ( len f)) by FINSEQ_1: 22;

      then ( len g) >= (1 + 1) by A1, XREAL_1: 7;

      then

       A3: 1 < ( len g) by XXREAL_0: 2;

      (( Sum ( Prefix (g,1))) + (2 * (1 - 1))) = s & (( Sum ( Prefix (g,(1 + 1)))) + (2 * 1)) = ((s + (f /. 1)) + 2) by A1, Th20;

      hence thesis by A2, A3;

    end;

    theorem :: TURING_1:23

    

     Th23: for T be TuringStr, t be Tape of T, s be Element of NAT , f be 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

      let T be TuringStr, t be Tape of T, s be Element of NAT , f be FinSequence of NAT ;

      set g = ( <*s*> ^ f);

      assume that

       A1: ( len f) >= 3 and

       A2: t storeData g;

      thus t is_1_between (s,((s + (f /. 1)) + 2)) by A1, A2, Th22, XXREAL_0: 2;

      ( len <*s*>) = 1 by FINSEQ_1: 39;

      then ( len g) = (1 + ( len f)) by FINSEQ_1: 22;

      then

       A3: ( len g) >= (3 + 1) by A1, XREAL_1: 7;

      then

       A4: 2 < ( len g) by XXREAL_0: 2;

      (( Sum ( Prefix (g,2))) + (2 * (2 - 1))) = ((s + (f /. 1)) + 2) & (( Sum ( Prefix (g,(2 + 1)))) + (2 * 2)) = (((s + (f /. 1)) + (f /. 2)) + 4) by A1, Th21;

      hence t is_1_between (((s + (f /. 1)) + 2),(((s + (f /. 1)) + (f /. 2)) + 4)) by A2, A4;

      

       A5: 3 < ( len g) by A3, XXREAL_0: 2;

      (( Sum ( Prefix (g,3))) + (2 * (3 - 1))) = (((s + (f /. 1)) + (f /. 2)) + 4) & (( Sum ( Prefix (g,(3 + 1)))) + (2 * 3)) = ((((s + (f /. 1)) + (f /. 2)) + (f /. 3)) + 6) by A1, Th21;

      hence thesis by A2, A5;

    end;

    begin

    definition

      :: TURING_1:def14

      func SumTuring -> strict TuringStr means

      : Def14: 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

      proof

        set St = ( SegM 5);

        reconsider p0 = 0 , qF = 5 as Element of St by Th1;

        set Sym = { 0 , 1};

        take TuringStr (# Sym, St, Sum_Tran , p0, qF #);

        thus thesis;

      end;

      uniqueness ;

    end

    

     Lm1: for n be Element of NAT st n <= 5 holds n is State of SumTuring

    proof

      let n be Element of NAT ;

      assume

       A1: n <= 5;

      the FStates of SumTuring = ( SegM 5) by Def14;

      hence thesis by A1, Th1;

    end;

    theorem :: TURING_1:24

    

     Th24: for T be TuringStr, t be Tape of T, h be Integer, s be Symbol of T st (t . h) = s holds ( Tape-Chg (t,h,s)) = t

    proof

      let T be TuringStr, t be Tape of T, h be Integer, s be Symbol of T;

      ex f be Function st t = f & ( dom f) = INT & ( rng f) c= the Symbols of T by FUNCT_2:def 2;

      then

       A1: h in ( dom t) by INT_1:def 2;

      assume (t . h) = s;

      hence thesis by A1, FUNCT_7: 96;

    end;

    

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

    proof

       0 in { 0 , 1} & 1 in { 0 , 1} by TARSKI:def 2;

      hence thesis by Def14;

    end;

    theorem :: TURING_1:25

    

     Th25: for T be TuringStr, s be All-State of T, p,h,t be 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 )))] by Def6;

    

     Lm3: for s be All-State of SumTuring , p,h,t be 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

      let s be All-State of SumTuring , p,h,t be set;

      assume

       A1: s = [p, h, t] & p <> 5;

      5 = the AcceptS of SumTuring by Def14;

      hence thesis by A1, Th25;

    end;

    theorem :: TURING_1:26

    

     Th26: for T be TuringStr, t be Tape of T, h be Integer, s be Symbol of T, i be object holds (( Tape-Chg (t,h,s)) . h) = s & (i <> h implies (( Tape-Chg (t,h,s)) . i) = (t . i))

    proof

      let tm be TuringStr, t be Tape of tm, h be Integer, s be Symbol of tm, i be object;

      set t1 = ( Tape-Chg (t,h,s)), p = (h .--> s);

      thus (t1 . h) = s by FUNCT_7: 94;

      assume i <> h;

      then not i in ( dom p) by TARSKI:def 1;

      hence thesis by FUNCT_4: 11;

    end;

    

     Lm4: for tm be TuringStr, s be All-State of tm, p be State of tm, h be Element of INT , t be Tape of tm, m,d be 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 be Integer st d <= i & i < (d + m) holds (t . i) = 1) holds (( Computation s) . m) = [p, (d + m), t]

    proof

      let tm be TuringStr, s be All-State of tm, p be State of tm, h be Element of INT , t be Tape of tm, m,d be Element of NAT ;

      assume that

       A1: d = h and

       A2: 1 is Symbol of tm and

       A3: s = [p, h, t] and

       A4: (the Tran of tm . [p, 1]) = [p, 1, 1] and

       A5: p <> the AcceptS of tm and

       A6: for i be Integer st d <= i & i < (d + m) holds (t . i) = 1;

      defpred Q[ Nat] means $1 <= m implies (( Computation s) . $1) = [p, (d + $1), t];

      

       A7: for k be Nat st Q[k] holds Q[(k + 1)]

      proof

        let k be Nat;

        assume

         A8: Q[k];

        now

          reconsider T = 1 as Symbol of tm by A2;

          set dk = (d + k);

          reconsider ik = (d + k) as Element of INT by INT_1:def 2;

          set sk = [p, ik, t];

          reconsider tt = (sk `3_3 ) as Tape of tm;

          assume

           A9: (k + 1) <= m;

          then k < m by NAT_1: 13;

          then dk < (d + m) by XREAL_1: 8;

          then

           A10: (t . ik) = 1 by A6, NAT_1: 11;

          

           A11: ( TRAN sk) = (the Tran of tm . [p, (tt . ( Head sk))])

          .= (the Tran of tm . [p, (t . ( Head sk))])

          .= [p, 1, 1] by A4, A10;

          then

           A12: ( offset ( TRAN sk)) = 1;

          

           A13: ( Tape-Chg ((sk `3_3 ),( Head sk),(( TRAN sk) `2_3 ))) = ( Tape-Chg (t,( Head sk),(( TRAN sk) `2_3 )))

          .= ( Tape-Chg (t,dk,(( TRAN sk) `2_3 )))

          .= ( Tape-Chg (t,dk,T)) by A11

          .= t by A10, Th24;

          

          thus (( Computation s) . (k + 1)) = ( Following sk) by A8, A9, Def7, NAT_1: 13

          .= [(( TRAN sk) `1_3 ), (( Head sk) + ( offset ( TRAN sk))), t] by A5, A13, Th25

          .= [p, (( Head sk) + ( offset ( TRAN sk))), t] by A11

          .= [p, (dk + 1), t] by A12

          .= [p, (d + (k + 1)), t];

        end;

        hence thesis;

      end;

      

       A14: Q[ 0 ] by A1, A3, Def7;

      for k holds Q[k] from NAT_1:sch 2( A14, A7);

      hence thesis;

    end;

    theorem :: TURING_1:27

    

     Th27: for s be All-State of SumTuring , t be Tape of SumTuring , head,n1,n2 be 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

      reconsider F = 0 as Symbol of SumTuring by Lm2;

      let s be All-State of SumTuring , t be Tape of SumTuring , h,n1,n2 be Element of NAT ;

      assume that

       A1: s = [ 0 , h, t] and

       A2: t storeData <*h, n1, n2*>;

      

       A3: (t . ((h + n1) + 2)) = 0 by A2, Th19;

      set j3 = ((((h + n1) + n2) + 4) - 1);

      reconsider h1 = (h + 1) as Element of INT by INT_1:def 2;

      

       A4: h < h1 by XREAL_1: 29;

      set t1 = ( Tape-Chg (t,h1,F));

      

       A5: (((h + 1) + 1) + n1) = ((h + n1) + 2);

      reconsider p4 = 4 as State of SumTuring by Lm1;

      reconsider m3 = j3 as Element of INT by INT_1:def 2;

      set j2 = (j3 - 1);

      reconsider m2 = j2 as Element of INT by INT_1:def 2;

      set j1 = ((n1 + n2) + 1);

      set Rs = (( Computation s) . ((((((n1 + 1) + (n2 + 1)) + 1) + 1) + (1 + 1)) + (j1 + 1)));

      reconsider p2 = 2 as State of SumTuring by Lm1;

      reconsider i2 = (h1 + 1) as Element of INT by INT_1:def 2;

      reconsider nk = ((h1 + 1) + n1) as Element of INT by INT_1:def 2;

      set i3 = ((((h + 1) + 1) + n1) + 1);

      reconsider n3 = i3 as Element of INT by INT_1:def 2;

      

       A6: (j2 - 1) = (h + j1);

      reconsider T = 1 as Symbol of SumTuring by Lm2;

      set t2 = ( Tape-Chg (t1,nk,T));

      

       A7: (h1 + 1) <= (((h + 1) + 1) + n1) & h1 < (h1 + 1) by NAT_1: 11, XREAL_1: 29;

      set i4 = (((h + n1) + n2) + 4);

      reconsider p0 = 0 as State of SumTuring by Lm1;

      set s1 = [p0, h1, t];

      

       A8: (t . h) = 0 by A2, Th19;

      h <= (h + n1) by NAT_1: 11;

      then

       A9: (h + 2) <= ((h + n1) + 2) by XREAL_1: 7;

      

       A10: (t . (((h + n1) + n2) + 4)) = 0 by A2, Th19;

      h <= (h + (n1 + n2)) by NAT_1: 11;

      then

       A11: (h + 4) <= (((h + n1) + n2) + 4) by XREAL_1: 7;

      then

       A12: h1 < (h + 3) & ((h + 4) - 1) <= j3 by XREAL_1: 8, XREAL_1: 9;

      

       A13: h1 < (h + 2) by XREAL_1: 8;

      then

       A14: h1 < ((h + n1) + 2) by A9, XXREAL_0: 2;

      

       A15: (t . h) = 0 by A2, Th19;

      

       A16: (t1 . h) = 0 & (t1 . ((h + n1) + 2)) = 0 & (t1 . (((h + n1) + n2) + 4)) = 0 & (for i be Integer st h1 < i & i < (((h + 1) + 1) + n1) holds (t1 . i) = 1) & for i be Integer st ((h + n1) + 2) < i & i < (((h + n1) + n2) + 4) holds (t1 . i) = 1

      proof

        thus (t1 . h) = 0 by A15, A4, Th26;

        thus (t1 . ((h + n1) + 2)) = 0 by A3, A9, A13, Th26;

        h1 < (h + 4) by XREAL_1: 8;

        hence (t1 . (((h + n1) + n2) + 4)) = 0 by A10, A11, Th26;

        hereby

          let i be Integer;

          assume that

           A17: h1 < i and

           A18: i < (((h + 1) + 1) + n1);

          

           A19: h < i by A4, A17, XXREAL_0: 2;

          

          thus (t1 . i) = (t . i) by A17, Th26

          .= 1 by A2, A5, A18, A19, Th19;

        end;

        hereby

          let i be Integer;

          assume that

           A20: ((h + n1) + 2) < i and

           A21: i < (((h + n1) + n2) + 4);

          

          thus (t1 . i) = (t . i) by A14, A20, Th26

          .= 1 by A2, A20, A21, Th19;

        end;

      end;

      

       A22: for i be Integer st ((h + 1) + 1) <= i & i < (((h + 1) + 1) + n1) holds (t1 . i) = 1

      proof

        let i be Integer;

        assume that

         A23: ((h + 1) + 1) <= i and

         A24: i < (((h + 1) + 1) + n1);

        h1 < (h1 + 1) by XREAL_1: 29;

        then h1 < i by A23, XXREAL_0: 2;

        hence thesis by A16, A24;

      end;

      set t3 = ( Tape-Chg (t2,j3,F));

      

       A25: (t1 . h1) = 0 by Th26;

      

       A26: (t2 . h1) = 0 & (t2 . (((h + n1) + n2) + 4)) = 0 & for i be Integer st h1 < i & i < (((h + n1) + n2) + 4) holds (t2 . i) = 1

      proof

        thus (t2 . h1) = 0 by A25, A7, Th26;

        (h + n1) <= ((h + n1) + n2) by NAT_1: 11;

        then

         A27: (((h + 1) + 1) + n1) <= (((h + n1) + n2) + 2) by A5, XREAL_1: 7;

        (((h + n1) + n2) + 2) < (((h + n1) + n2) + 4) by XREAL_1: 8;

        hence (t2 . (((h + n1) + n2) + 4)) = 0 by A16, A27, Th26;

        hereby

          let i be Integer;

          assume that

           A28: h1 < i and

           A29: i < (((h + n1) + n2) + 4);

          per cases by XXREAL_0: 1;

            suppose

             A30: i < (((h + 1) + 1) + n1);

            

            hence (t2 . i) = (t1 . i) by Th26

            .= 1 by A16, A28, A30;

          end;

            suppose i = (((h + 1) + 1) + n1);

            hence (t2 . i) = 1 by Th26;

          end;

            suppose

             A31: i > (((h + 1) + 1) + n1);

            

            hence (t2 . i) = (t1 . i) by Th26

            .= 1 by A16, A29, A31;

          end;

        end;

      end;

      

       A32: (t3 . h1) = 0 & (t3 . j3) = 0 & for i be Integer st h1 < i & i < j3 holds (t3 . i) = 1

      proof

        thus (t3 . h1) = 0 by A26, A12, Th26;

        thus (t3 . j3) = 0 by Th26;

        hereby

          let i be Integer;

          assume that

           A33: h1 < i and

           A34: i < j3;

          

           A35: i < (((h + n1) + n2) + 4) by A34, XREAL_1: 146, XXREAL_0: 2;

          

          thus (t3 . i) = (t2 . i) by A34, Th26

          .= 1 by A26, A33, A35;

        end;

      end;

      then

       A36: t3 is_1_between (h1,((h1 + (n1 + n2)) + 2));

      reconsider p3 = 3 as State of SumTuring by Lm1;

      set sm = [p2, n3, t2];

      reconsider n4 = i4 as Element of INT by INT_1:def 2;

      set sp2 = [p2, n4, t2];

      set sp3 = [p3, m3, t2];

      reconsider p1 = 1 as State of SumTuring by Lm1;

      set s2 = [p1, i2, t1];

      set sn = [p1, nk, t1];

      reconsider sn3 = (sn `3_3 ) as Tape of SumTuring ;

      

       A37: ( TRAN sn) = ( Sum_Tran . [(sn `1_3 ), (sn3 . ( Head sn))]) by Def14

      .= ( Sum_Tran . [p1, (sn3 . ( Head sn))])

      .= ( Sum_Tran . [p1, (t1 . ( Head sn))])

      .= [2, 1, 1] by A16, Th14;

      then

       A38: ( offset ( TRAN sn)) = 1;

      reconsider sn3 = (sp2 `3_3 ) as Tape of SumTuring ;

      

       A39: ( TRAN sp2) = ( Sum_Tran . [(sp2 `1_3 ), (sn3 . ( Head sp2))]) by Def14

      .= ( Sum_Tran . [p2, (sn3 . ( Head sp2))])

      .= ( Sum_Tran . [p2, (t2 . ( Head sp2))])

      .= [3, 0 , ( - 1)] by A26, Th14;

      then

       A40: ( offset ( TRAN sp2)) = ( - 1);

      ( Tape-Chg ((sp2 `3_3 ),( Head sp2),(( TRAN sp2) `2_3 ))) = ( Tape-Chg (t2,( Head sp2),(( TRAN sp2) `2_3 )))

      .= ( Tape-Chg (t2,i4,(( TRAN sp2) `2_3 )))

      .= ( Tape-Chg (t2,i4,F)) by A39

      .= t2 by A26, Th24;

      

      then

       A41: ( Following sp2) = [(( TRAN sp2) `1_3 ), (( Head sp2) + ( offset ( TRAN sp2))), t2] by Lm3

      .= [3, (( Head sp2) + ( offset ( TRAN sp2))), t2] by A39

      .= [3, j3, t2] by A40;

      ( Tape-Chg ((sn `3_3 ),( Head sn),(( TRAN sn) `2_3 ))) = ( Tape-Chg (t1,( Head sn),(( TRAN sn) `2_3 )))

      .= ( Tape-Chg (t1,nk,(( TRAN sn) `2_3 )))

      .= t2 by A37;

      

      then

       A42: ( Following sn) = [(( TRAN sn) `1_3 ), (( Head sn) + ( offset ( TRAN sn))), t2] by Lm3

      .= [2, (( Head sn) + ( offset ( TRAN sn))), t2] by A37

      .= sm by A38;

      reconsider s3 = (s `3_3 ) as Tape of SumTuring ;

      

       A43: ( TRAN s) = ( Sum_Tran . [(s `1_3 ), (s3 . ( Head s))]) by Def14

      .= ( Sum_Tran . [ 0 , (s3 . ( Head s))]) by A1

      .= ( Sum_Tran . [ 0 , (t . ( Head s))]) by A1

      .= ( Sum_Tran . [ 0 , (t . h)]) by A1

      .= [ 0 , 0 , 1] by A2, Th14, Th19;

      then

       A44: ( offset ( TRAN s)) = 1;

      

       A45: h1 < ((h1 + 1) + n1) by A7, XXREAL_0: 2;

      

       A46: for i be Integer st i3 <= i & i < (i3 + (n2 + 1)) holds (t2 . i) = 1

      proof

        let i be Integer;

        assume that

         A47: i3 <= i and

         A48: i < (i3 + (n2 + 1));

        nk < i3 by XREAL_1: 29;

        then h1 < i3 by A45, XXREAL_0: 2;

        then h1 < i by A47, XXREAL_0: 2;

        hence thesis by A26, A48;

      end;

      set sp5 = [p4, h1, t3];

      set sp4 = [p4, m2, t3];

      defpred R[ Nat] means (h + $1) < j2 implies (( Computation sp4) . $1) = [4, (j2 - $1), t3];

      (the Tran of SumTuring . [p2, 1]) = [p2, 1, 1] & p2 <> the AcceptS of SumTuring by Def14, Th14;

      then

       A49: (( Computation sm) . (n2 + 1)) = [2, (((h + n1) + n2) + 4), t2] by A46, Lm4;

      h1 < j3 by A12, XXREAL_0: 2;

      then

       A50: (t2 . j3) = 1 by A26, XREAL_1: 146;

      reconsider sn3 = (sp3 `3_3 ) as Tape of SumTuring ;

      

       A51: ( TRAN sp3) = ( Sum_Tran . [(sp3 `1_3 ), (sn3 . ( Head sp3))]) by Def14

      .= ( Sum_Tran . [p3, (sn3 . ( Head sp3))])

      .= ( Sum_Tran . [p3, (t2 . ( Head sp3))])

      .= [4, 0 , ( - 1)] by A50, Th14;

      then

       A52: ( offset ( TRAN sp3)) = ( - 1);

      

       A53: for k be Nat st R[k] holds R[(k + 1)]

      proof

        let k be Nat;

        assume

         A54: R[k];

        now

          reconsider ik = (j2 - k) as Element of INT by INT_1:def 2;

          set k3 = (j2 - k);

          set sk = [p4, ik, t3];

          reconsider tt = (sk `3_3 ) as Tape of SumTuring ;

          assume

           A55: (h + (k + 1)) < j2;

          then (h1 + k) < (j2 + 0 );

          then

           A56: (h1 - 0 ) < (j2 - k) by XREAL_1: 21;

          reconsider ii = (j2 - k) as Element of NAT by A56, INT_1: 3;

          j2 <= (j2 + k) by INT_1: 6;

          then (j2 - k) <= j2 by XREAL_1: 20;

          then (j2 - k) < j3 by XREAL_1: 146, XXREAL_0: 2;

          then

           A57: (t3 . ii) = 1 by A32, A56;

          

           A58: ( TRAN sk) = ( Sum_Tran . [(sk `1_3 ), (tt . ( Head sk))]) by Def14

          .= ( Sum_Tran . [p4, (tt . ( Head sk))])

          .= ( Sum_Tran . [p4, (t3 . ( Head sk))])

          .= [4, 1, ( - 1)] by A57, Th14;

          then

           A59: ( offset ( TRAN sk)) = ( - 1);

          

           A60: ( Tape-Chg ((sk `3_3 ),( Head sk),(( TRAN sk) `2_3 ))) = ( Tape-Chg (t3,( Head sk),(( TRAN sk) `2_3 )))

          .= ( Tape-Chg (t3,k3,(( TRAN sk) `2_3 )))

          .= ( Tape-Chg (t3,k3,T)) by A58

          .= t3 by A57, Th24;

          (h + k) < ((h + k) + 1) by XREAL_1: 29;

          

          hence (( Computation sp4) . (k + 1)) = ( Following sk) by A54, A55, Def7, XXREAL_0: 2

          .= [(( TRAN sk) `1_3 ), (( Head sk) + ( offset ( TRAN sk))), t3] by A60, Lm3

          .= [4, (( Head sk) + ( offset ( TRAN sk))), t3] by A58

          .= [4, ((j2 - k) + ( - 1)), t3] by A59

          .= [4, (j2 - (k + 1)), t3];

        end;

        hence thesis;

      end;

      

       A61: R[ 0 ] by Def7;

      for k be Nat holds R[k] from NAT_1:sch 2( A61, A53);

      

      then

       A62: (( Computation sp4) . j1) = [4, (j2 - j1), t3] by A6, XREAL_1: 146

      .= sp5;

      reconsider s3 = (s1 `3_3 ) as Tape of SumTuring ;

      

       A63: ( TRAN s1) = ( Sum_Tran . [(s1 `1_3 ), (s3 . ( Head s1))]) by Def14

      .= ( Sum_Tran . [p0, (s3 . ( Head s1))])

      .= ( Sum_Tran . [p0, (t . ( Head s1))])

      .= ( Sum_Tran . [ 0 , (t . h1)])

      .= [1, 0 , 1] by A2, A4, A14, Th14, Th19;

      then

       A64: ( offset ( TRAN s1)) = 1;

      ( Tape-Chg ((sp3 `3_3 ),( Head sp3),(( TRAN sp3) `2_3 ))) = ( Tape-Chg (t2,( Head sp3),(( TRAN sp3) `2_3 )))

      .= ( Tape-Chg (t2,j3,(( TRAN sp3) `2_3 )))

      .= t3 by A51;

      

      then

       A65: ( Following sp3) = [(( TRAN sp3) `1_3 ), (( Head sp3) + ( offset ( TRAN sp3))), t3] by Lm3

      .= [4, (( Head sp3) + ( offset ( TRAN sp3))), t3] by A51

      .= sp4 by A52;

       A66:

      now

        reconsider tt = (sp5 `3_3 ) as Tape of SumTuring ;

        

         A67: ( TRAN sp5) = ( Sum_Tran . [(sp5 `1_3 ), (tt . ( Head sp5))]) by Def14

        .= ( Sum_Tran . [4, (tt . ( Head sp5))])

        .= ( Sum_Tran . [4, (t3 . ( Head sp5))])

        .= [5, 0 , 0 ] by A32, Th14;

        then

         A68: ( offset ( TRAN sp5)) = 0 ;

        ( Tape-Chg ((sp5 `3_3 ),( Head sp5),(( TRAN sp5) `2_3 ))) = ( Tape-Chg (t3,( Head sp5),(( TRAN sp5) `2_3 )))

        .= ( Tape-Chg (t3,h1,(( TRAN sp5) `2_3 )))

        .= ( Tape-Chg (t3,h1,F)) by A67

        .= t3 by A32, Th24;

        

        hence ( Following sp5) = [(( TRAN sp5) `1_3 ), (( Head sp5) + ( offset ( TRAN sp5))), t3] by Lm3

        .= [5, (( Head sp5) + ( offset ( TRAN sp5))), t3] by A67

        .= [5, (h1 + 0 ), t3] by A68;

      end;

      ( Tape-Chg ((s1 `3_3 ),( Head s1),(( TRAN s1) `2_3 ))) = ( Tape-Chg (t,( Head s1),(( TRAN s1) `2_3 )))

      .= ( Tape-Chg (t,h1,(( TRAN s1) `2_3 )))

      .= t1 by A63;

      

      then

       A69: ( Following s1) = [(( TRAN s1) `1_3 ), (( Head s1) + ( offset ( TRAN s1))), t1] by Lm3

      .= [1, (( Head s1) + ( offset ( TRAN s1))), t1] by A63

      .= s2 by A64;

      ( Tape-Chg ((s `3_3 ),( Head s),(( TRAN s) `2_3 ))) = ( Tape-Chg (t,( Head s),(( TRAN s) `2_3 ))) by A1

      .= ( Tape-Chg (t,h,(( TRAN s) `2_3 ))) by A1

      .= ( Tape-Chg (t,h,F)) by A43

      .= t by A8, Th24;

      

      then

       A70: ( Following s) = [(( TRAN s) `1_3 ), (( Head s) + ( offset ( TRAN s))), t] by A1, Lm3

      .= [ 0 , (( Head s) + ( offset ( TRAN s))), t] by A43

      .= s1 by A1, A44;

      (( Computation s) . (1 + 1)) = ( Following (( Computation s) . 1)) by Def7

      .= s2 by A70, A69, Th9;

      then (( Computation s) . (((((n1 + 1) + (n2 + 1)) + 1) + 1) + (1 + 1))) = (( Computation s2) . ((((n1 + 1) + (n2 + 1)) + 1) + 1)) by Th10;

      

      then (( Computation s) . (((((n1 + 1) + (n2 + 1)) + 1) + 1) + (1 + 1))) = ( Following (( Computation s2) . (((n1 + 1) + (n2 + 1)) + 1))) by Def7

      .= ( Following ( Following (( Computation s2) . ((n1 + 1) + (n2 + 1))))) by Def7

      .= ( Following ( Following (( Computation (( Computation s2) . (n1 + 1))) . (n2 + 1)))) by Th10;

      

      then

       A71: Rs = (( Computation ( Following ( Following (( Computation (( Computation s2) . (n1 + 1))) . (n2 + 1))))) . (j1 + 1)) by Th10

      .= (( Computation ( Following ( Following (( Computation ( Following (( Computation s2) . n1))) . (n2 + 1))))) . (j1 + 1)) by Def7;

      (the Tran of SumTuring . [p1, 1]) = [p1, 1, 1] & p1 <> the AcceptS of SumTuring by Def14, Th14;

      then Rs = (( Computation ( Following sp3)) . (j1 + 1)) by A22, A42, A49, A41, A71, Lm4;

      then

       A72: Rs = [5, h1, t3] by A65, A62, A66, Def7;

      

      then

       A73: (Rs `1_3 ) = 5

      .= the AcceptS of SumTuring by Def14;

      hence s is Accept-Halt;

      then

       A74: ( Result s) = Rs by A73, Def9;

      hence (( Result s) `2_3 ) = (1 + h) by A72;

      (( Result s) `3_3 ) = t3 by A72, A74;

      hence thesis by A36, Th16;

    end;

    definition

      let T be TuringStr, F be Function;

      :: TURING_1:def15

      pred T computes F means for s be All-State of T, t be Tape of T, a be Element of NAT , x be 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 be Element of NAT st (( Result s) `2_3 ) = b & y = (F . x) & (( Result s) `3_3 ) storeData ( <*b*> ^ <*y*>);

    end

    theorem :: TURING_1:28

    

     Th28: ( dom [+] ) c= (2 -tuples_on NAT )

    proof

      ( arity (1 proj 1)) = 1 by COMPUT_1: 37;

      then ( dom [+] ) c= ((1 + 1) -tuples_on NAT ) by COMPUT_1: 56;

      hence thesis;

    end;

    theorem :: TURING_1:29

     SumTuring computes [+]

    proof

      now

        let s be All-State of SumTuring , t be Tape of SumTuring , h1 be Element of NAT , x be FinSequence of NAT ;

        assume that

         A1: x in ( dom [+] ) and

         A2: s = [the InitS of SumTuring , h1, t] and

         A3: t storeData ( <*h1*> ^ x);

        x is Tuple of 2, NAT by A1, Th28, FINSEQ_2: 131;

        then

        consider i,j be Element of NAT such that

         A4: x = <*i, j*> by FINSEQ_2: 100;

        

         A5: s = [ 0 , h1, t] by A2, Def14;

        

         A6: ( <*h1*> ^ x) = <*h1, i, j*> by A4, FINSEQ_1: 43;

        hence s is Accept-Halt by A3, A5, Th27;

        take h2 = (1 + h1);

        take y = (i + j);

        t storeData <*h1, i, j*> by A3, A4, FINSEQ_1: 43;

        hence (( Result s) `2_3 ) = h2 by A5, Th27;

        thus y = ( [+] . x) by A4, COMPUT_1: 85;

        (( Result s) `3_3 ) storeData <*(1 + h1), (i + j)*> by A3, A5, A6, Th27;

        hence (( Result s) `3_3 ) storeData ( <*h2*> ^ <*y*>);

      end;

      hence thesis;

    end;

    begin

    definition

      :: TURING_1:def16

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

      coherence

      proof

        reconsider p0 = 0 , p1 = 1, p2 = 2, p3 = 3, p4 = 4 as Element of ( SegM 4) by Th1;

        set A = [:( SegM 4), { 0 , 1}:], B = {( - 1), 0 , 1}, C = [:( SegM 4), { 0 , 1}, B:];

        reconsider b0 = 0 , b1 = 1 as Element of { 0 , 1} by TARSKI:def 2;

        reconsider L = ( - 1) as Element of B by ENUMSET1:def 1;

        reconsider h = 0 , R = 1 as Element of {( - 1), 0 , 1} by ENUMSET1:def 1;

        C = [:A, B:] by ZFMISC_1:def 3;

        then

        reconsider OP = ( id (A,B,h)) as Function of A, C;

        (((((((( id (A,B, 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 ])) = (((((((OP +* ( [p0, b0] .--> [p1, b0, R])) +* ( [p1, b1] .--> [p1, b1, R])) +* ( [p1, b0] .--> [p2, b1, R])) +* ( [p2, b0] .--> [p3, b0, L])) +* ( [p2, b1] .--> [p3, b0, L])) +* ( [p3, b1] .--> [p3, b1, L])) +* ( [p3, b0] .--> [p4, b0, h]));

        hence thesis;

      end;

    end

    theorem :: TURING_1:30

    

     Th30: ( 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

      set x = [1, 1];

      set x1 = [ 0 , 0 ];

      set p1 = ( [ 0 , 0 ] .--> [1, 0 , 1]), p2 = ( [1, 1] .--> [1, 1, 1]), p3 = ( [1, 0 ] .--> [2, 1, 1]), p4 = ( [2, 0 ] .--> [3, 0 , ( - 1)]), p5 = ( [2, 1] .--> [3, 0 , ( - 1)]), p6 = ( [3, 1] .--> [3, 1, ( - 1)]), f = ( id ( [:( SegM 4), { 0 , 1}:], {( - 1), 0 , 1}, 0 ));

      

      thus ( Succ_Tran . x1) = (((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) . x1) by Th2

      .= ((((((f +* p1) +* p2) +* p3) +* p4) +* p5) . x1) by Th2

      .= (((((f +* p1) +* p2) +* p3) +* p4) . x1) by Th2

      .= ((((f +* p1) +* p2) +* p3) . x1) by Th2

      .= (((f +* p1) +* p2) . x1) by Th2

      .= ((f +* p1) . x1) by Th3

      .= [1, 0 , 1] by FUNCT_7: 94;

      

      thus ( Succ_Tran . x) = (((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) . x) by Th2

      .= ((((((f +* p1) +* p2) +* p3) +* p4) +* p5) . x) by Th2

      .= (((((f +* p1) +* p2) +* p3) +* p4) . x) by Th2

      .= ((((f +* p1) +* p2) +* p3) . x) by Th2

      .= (((f +* p1) +* p2) . x) by Th3

      .= [1, 1, 1] by FUNCT_7: 94;

      set x = [1, 0 ];

      

      thus ( Succ_Tran . x) = (((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) . x) by Th2

      .= ((((((f +* p1) +* p2) +* p3) +* p4) +* p5) . x) by Th2

      .= (((((f +* p1) +* p2) +* p3) +* p4) . x) by Th2

      .= ((((f +* p1) +* p2) +* p3) . x) by Th2

      .= [2, 1, 1] by FUNCT_7: 94;

      set x = [2, 0 ];

      

      thus ( Succ_Tran . x) = (((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) . x) by Th2

      .= ((((((f +* p1) +* p2) +* p3) +* p4) +* p5) . x) by Th2

      .= (((((f +* p1) +* p2) +* p3) +* p4) . x) by Th3

      .= [3, 0 , ( - 1)] by FUNCT_7: 94;

      set x = [2, 1];

      

      thus ( Succ_Tran . x) = (((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) . x) by Th2

      .= ((((((f +* p1) +* p2) +* p3) +* p4) +* p5) . x) by Th2

      .= [3, 0 , ( - 1)] by FUNCT_7: 94;

      set x = [3, 1];

      

      thus ( Succ_Tran . x) = (((((((f +* p1) +* p2) +* p3) +* p4) +* p5) +* p6) . x) by Th3

      .= [3, 1, ( - 1)] by FUNCT_7: 94;

      thus thesis by FUNCT_7: 94;

    end;

    definition

      :: TURING_1:def17

      func SuccTuring -> strict TuringStr means

      : Def17: 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

      proof

        set St = ( SegM 4);

        reconsider p0 = 0 , qF = 4 as Element of St by Th1;

        set Sym = { 0 , 1};

        take TuringStr (# Sym, St, Succ_Tran , p0, qF #);

        thus thesis;

      end;

      uniqueness ;

    end

    

     Lm5: for n be Element of NAT st n <= 4 holds n is State of SuccTuring

    proof

      let n be Element of NAT ;

      assume

       A1: n <= 4;

      the FStates of SuccTuring = ( SegM 4) by Def17;

      hence thesis by A1, Th1;

    end;

    

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

    proof

       0 in { 0 , 1} & 1 in { 0 , 1} by TARSKI:def 2;

      hence thesis by Def17;

    end;

    

     Lm7: for s be All-State of SuccTuring , p,h,t be 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

      let s be All-State of SuccTuring , p,h,t be set;

      assume

       A1: s = [p, h, t] & p <> 4;

      4 = the AcceptS of SuccTuring by Def17;

      hence thesis by A1, Th25;

    end;

    theorem :: TURING_1:31

    

     Th31: for s be All-State of SuccTuring , t be Tape of SuccTuring , head,n be 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

      reconsider F = 0 as Symbol of SuccTuring by Lm6;

      let s be All-State of SuccTuring , t be Tape of SuccTuring , h,n be Element of NAT ;

      assume that

       A1: s = [ 0 , h, t] and

       A2: t storeData <*h, n*>;

      

       A3: (t . h) = 0 by A2, Th17;

      set i3 = ((((h + 1) + 1) + n) + 1);

      reconsider h1 = (h + 1) as Element of INT by INT_1:def 2;

      reconsider p1 = 1 as State of SuccTuring by Lm5;

      

       A4: ((h1 + 1) + n) < i3 by XREAL_1: 29;

      h <= (h + n) by NAT_1: 11;

      then

       A5: (h + 2) <= ((h + n) + 2) by XREAL_1: 7;

      

       A6: h1 < (h + 2) by XREAL_1: 8;

      then

       A7: h1 < ((h + n) + 2) by A5, XXREAL_0: 2;

      reconsider p2 = 2 as State of SuccTuring by Lm5;

      reconsider i2 = (h1 + 1) as Element of INT by INT_1:def 2;

      reconsider nk = ((h1 + 1) + n) as Element of INT by INT_1:def 2;

      reconsider hh = h as Element of INT by INT_1:def 2;

      reconsider n3 = i3 as Element of INT by INT_1:def 2;

      reconsider T = 1 as Symbol of SuccTuring by Lm6;

      set t1 = ( Tape-Chg (t,h1,T));

      

       A8: h < h1 by XREAL_1: 29;

      

       A9: (t . ((h + n) + 2)) = 0 by A2, Th17;

      

       A10: (t1 . h) = 0 & (t1 . ((h + n) + 2)) = 0 & for i be Integer st h < i & i < ((h + n) + 2) holds (t1 . i) = 1

      proof

        thus (t1 . h) = 0 by A3, A8, Th26;

        thus (t1 . ((h + n) + 2)) = 0 by A9, A5, A6, Th26;

        hereby

          let i be Integer;

          assume

           A11: h < i & i < ((h + n) + 2);

          per cases ;

            suppose h1 = i;

            hence (t1 . i) = 1 by Th26;

          end;

            suppose h1 <> i;

            

            hence (t1 . i) = (t . i) by Th26

            .= 1 by A2, A11, Th17;

          end;

        end;

      end;

      

       A12: for i be Integer st ((h + 1) + 1) <= i & i < (((h + 1) + 1) + n) holds (t1 . i) = 1

      proof

        let i be Integer;

        assume that

         A13: ((h + 1) + 1) <= i and

         A14: i < (((h + 1) + 1) + n);

        h1 < (h1 + 1) by XREAL_1: 29;

        then h1 < i by A13, XXREAL_0: 2;

        then h < i by A8, XXREAL_0: 2;

        hence thesis by A10, A14;

      end;

      reconsider s3 = (s `3_3 ) as Tape of SuccTuring ;

      

       A15: ( TRAN s) = ( Succ_Tran . [(s `1_3 ), (s3 . ( Head s))]) by Def17

      .= ( Succ_Tran . [ 0 , (s3 . ( Head s))]) by A1

      .= ( Succ_Tran . [ 0 , (t . ( Head s))]) by A1

      .= [1, 0 , 1] by A1, A3, Th30;

      then

       A16: ( offset ( TRAN s)) = 1;

      set s1 = [p1, h1, t];

      reconsider s3 = (s1 `3_3 ) as Tape of SuccTuring ;

      ( Tape-Chg ((s `3_3 ),( Head s),(( TRAN s) `2_3 ))) = ( Tape-Chg (t,( Head s),(( TRAN s) `2_3 ))) by A1

      .= ( Tape-Chg (t,h,(( TRAN s) `2_3 ))) by A1

      .= ( Tape-Chg (t,h,F)) by A15

      .= t by A3, Th24;

      

      then

       A17: ( Following s) = [(( TRAN s) `1_3 ), (( Head s) + ( offset ( TRAN s))), t] by A1, Lm7

      .= [1, (( Head s) + ( offset ( TRAN s))), t] by A15

      .= s1 by A1, A16;

      

       A18: ( TRAN s1) = ( Succ_Tran . [(s1 `1_3 ), (s3 . ( Head s1))]) by Def17

      .= ( Succ_Tran . [p1, (s3 . ( Head s1))])

      .= ( Succ_Tran . [p1, (t . ( Head s1))])

      .= ( Succ_Tran . [1, (t . h1)])

      .= [1, 1, 1] by A2, A8, A7, Th17, Th30;

      then

       A19: ( offset ( TRAN s1)) = 1;

      reconsider p1 = 1 as State of SuccTuring by Lm5;

      set s2 = [p1, i2, t1];

      ( Tape-Chg ((s1 `3_3 ),( Head s1),(( TRAN s1) `2_3 ))) = ( Tape-Chg (t,( Head s1),(( TRAN s1) `2_3 )))

      .= ( Tape-Chg (t,h1,(( TRAN s1) `2_3 )))

      .= t1 by A18;

      

      then

       A20: ( Following s1) = [(( TRAN s1) `1_3 ), (( Head s1) + ( offset ( TRAN s1))), t1] by Lm7

      .= [1, (( Head s1) + ( offset ( TRAN s1))), t1] by A18

      .= s2 by A19;

      reconsider p3 = 3 as State of SuccTuring by Lm5;

      set sn = [p1, nk, t1];

      set t2 = ( Tape-Chg (t1,nk,T));

      set t3 = ( Tape-Chg (t2,n3,F));

      (the Tran of SuccTuring . [p1, 1]) = [p1, 1, 1] & p1 <> the AcceptS of SuccTuring by Def17, Th30;

      then

       A21: (( Computation s2) . n) = [p1, (((h + 1) + 1) + n), t1] by A12, Lm4;

      (h1 + 1) <= (((h + 1) + 1) + n) & h1 < (h1 + 1) by NAT_1: 11, XREAL_1: 29;

      then

       A22: h1 < ((h1 + 1) + n) by XXREAL_0: 2;

      

       A23: (t2 . h) = 0 & for i be Integer st h < i & i <= ((h + n) + 2) holds (t2 . i) = 1

      proof

        thus (t2 . h) = 0 by A8, A10, A22, Th26;

        hereby

          let i be Integer;

          assume that

           A24: h < i and

           A25: i <= ((h + n) + 2);

          per cases ;

            suppose

             A26: i <> ((h + n) + 2);

            then

             A27: i < ((h + n) + 2) by A25, XXREAL_0: 1;

            

            thus (t2 . i) = (t1 . i) by A26, Th26

            .= 1 by A10, A24, A27;

          end;

            suppose i = ((h + n) + 2);

            hence (t2 . i) = 1 by Th26;

          end;

        end;

      end;

      set sp3 = [p3, nk, t3];

      set sm = [p2, n3, t2];

      reconsider sm3 = (sm `3_3 ) as Tape of SuccTuring ;

      

       A28: the Symbols of SuccTuring = { 0 , 1} by Def17;

       A29:

      now

        per cases by A28, TARSKI:def 2;

          suppose (t2 . n3) = 1;

          hence ( Succ_Tran . [2, (t2 . n3)]) = [p3, 0 , ( - 1)] by Th30;

        end;

          suppose (t2 . n3) = 0 ;

          hence ( Succ_Tran . [2, (t2 . n3)]) = [p3, 0 , ( - 1)] by Th30;

        end;

      end;

      

       A30: ( TRAN sm) = ( Succ_Tran . [(sm `1_3 ), (sm3 . ( Head sm))]) by Def17

      .= ( Succ_Tran . [2, (sm3 . ( Head sm))])

      .= ( Succ_Tran . [2, (t2 . ( Head sm))])

      .= [p3, 0 , ( - 1)] by A29;

      then

       A31: ( offset ( TRAN sm)) = ( - 1);

      set j1 = ((1 + 1) + n), sp5 = [p3, hh, t3];

      defpred R[ Nat] means (h + $1) <= nk implies (( Computation sp3) . $1) = [3, (nk - $1), t3];

      reconsider sn3 = (sn `3_3 ) as Tape of SuccTuring ;

      

       A32: (h + j1) = nk;

      set Rs = (( Computation s) . ((1 + 1) + (((n + 1) + 1) + (j1 + 1))));

      

       A33: ( TRAN sn) = ( Succ_Tran . [(sn `1_3 ), (sn3 . ( Head sn))]) by Def17

      .= ( Succ_Tran . [p1, (sn3 . ( Head sn))])

      .= ( Succ_Tran . [p1, (t1 . ( Head sn))])

      .= [2, 1, 1] by A10, Th30;

      then

       A34: ( offset ( TRAN sn)) = 1;

      

       A35: h < ((h1 + 1) + n) by A8, A22, XXREAL_0: 2;

      

       A36: (t3 . h) = 0 & (t3 . ((h + (n + 1)) + 2)) = 0 & for k be Integer st h < k & k < ((h + (n + 1)) + 2) holds (t3 . k) = 1

      proof

        thus (t3 . h) = 0 by A35, A23, A4, Th26;

        thus (t3 . ((h + (n + 1)) + 2)) = 0 by Th26;

        hereby

          let i be Integer;

          assume that

           A37: h < i and

           A38: i < ((h + (n + 1)) + 2);

          (i + 1) <= ((h + (n + 1)) + 2) by A38, INT_1: 7;

          then

           A39: i <= (((h + (n + 1)) + 2) - 1) by XREAL_1: 19;

          

          thus (t3 . i) = (t2 . i) by A38, Th26

          .= 1 by A23, A37, A39;

        end;

      end;

      then

       A40: t3 is_1_between (h,((h + (n + 1)) + 2));

      ( Tape-Chg ((sm `3_3 ),( Head sm),(( TRAN sm) `2_3 ))) = ( Tape-Chg (t2,( Head sm),(( TRAN sm) `2_3 )))

      .= ( Tape-Chg (t2,n3,(( TRAN sm) `2_3 )))

      .= t3 by A30;

      

      then

       A41: ( Following sm) = [(( TRAN sm) `1_3 ), (( Head sm) + ( offset ( TRAN sm))), t3] by Lm7

      .= [p3, (( Head sm) + ( offset ( TRAN sm))), t3] by A30

      .= sp3 by A31;

      ( Tape-Chg ((sn `3_3 ),( Head sn),(( TRAN sn) `2_3 ))) = ( Tape-Chg (t1,( Head sn),(( TRAN sn) `2_3 )))

      .= ( Tape-Chg (t1,nk,(( TRAN sn) `2_3 )))

      .= t2 by A33;

      

      then

       A42: ( Following sn) = [(( TRAN sn) `1_3 ), (( Head sn) + ( offset ( TRAN sn))), t2] by Lm7

      .= [2, (( Head sn) + ( offset ( TRAN sn))), t2] by A33

      .= sm by A34;

      

       A43: for k be Nat st R[k] holds R[(k + 1)]

      proof

        let k be Nat;

        assume

         A44: R[k];

        now

          reconsider ik = (nk - k) as Element of INT by INT_1:def 2;

          set k3 = (nk - k);

          

           A45: (h + k) < ((h + k) + 1) by XREAL_1: 29;

          set sk = [p3, ik, t3];

          reconsider tt = (sk `3_3 ) as Tape of SuccTuring ;

          nk <= (nk + k) by INT_1: 6;

          then

           A46: (nk - k) <= nk by XREAL_1: 20;

          assume

           A47: (h + (k + 1)) <= nk;

          then (h + k) < (nk + 0 ) by A45, XXREAL_0: 2;

          then

           A48: (h - 0 ) < (nk - k) by XREAL_1: 21;

          reconsider ii = (nk - k) as Element of NAT by A48, INT_1: 3;

          ((h + n) + 2) < (((h + n) + 2) + 1) by XREAL_1: 29;

          then ii < ((h + (n + 1)) + 2) by A46, XXREAL_0: 2;

          then

           A49: (t3 . ii) = 1 by A36, A48;

          

           A50: ( TRAN sk) = ( Succ_Tran . [(sk `1_3 ), (tt . ( Head sk))]) by Def17

          .= ( Succ_Tran . [p3, (tt . ( Head sk))])

          .= ( Succ_Tran . [p3, (t3 . ( Head sk))])

          .= [3, 1, ( - 1)] by A49, Th30;

          then

           A51: ( offset ( TRAN sk)) = ( - 1);

          

           A52: ( Tape-Chg ((sk `3_3 ),( Head sk),(( TRAN sk) `2_3 ))) = ( Tape-Chg (t3,( Head sk),(( TRAN sk) `2_3 )))

          .= ( Tape-Chg (t3,k3,(( TRAN sk) `2_3 )))

          .= ( Tape-Chg (t3,k3,T)) by A50

          .= t3 by A49, Th24;

          hereby

            

            thus (( Computation sp3) . (k + 1)) = ( Following sk) by A44, A47, A45, Def7, XXREAL_0: 2

            .= [(( TRAN sk) `1_3 ), (( Head sk) + ( offset ( TRAN sk))), t3] by A52, Lm7

            .= [3, (( Head sk) + ( offset ( TRAN sk))), t3] by A50

            .= [3, ((nk - k) + ( - 1)), t3] by A51

            .= [3, (nk - (k + 1)), t3];

          end;

        end;

        hence thesis;

      end;

      

       A53: R[ 0 ] by Def7;

      for k be Nat holds R[k] from NAT_1:sch 2( A53, A43);

      

      then

       A54: (( Computation sp3) . j1) = [3, (nk - j1), t3] by A32

      .= sp5;

       A55:

      now

        reconsider tt = (sp5 `3_3 ) as Tape of SuccTuring ;

        

         A56: ( TRAN sp5) = ( Succ_Tran . [(sp5 `1_3 ), (tt . ( Head sp5))]) by Def17

        .= ( Succ_Tran . [3, (tt . ( Head sp5))])

        .= ( Succ_Tran . [3, (t3 . ( Head sp5))])

        .= [4, 0 , 0 ] by A36, Th30;

        then

         A57: ( offset ( TRAN sp5)) = 0 ;

        ( Tape-Chg ((sp5 `3_3 ),( Head sp5),(( TRAN sp5) `2_3 ))) = ( Tape-Chg (t3,( Head sp5),(( TRAN sp5) `2_3 )))

        .= ( Tape-Chg (t3,h,(( TRAN sp5) `2_3 )))

        .= ( Tape-Chg (t3,h,F)) by A56

        .= t3 by A36, Th24;

        

        hence ( Following sp5) = [(( TRAN sp5) `1_3 ), (( Head sp5) + ( offset ( TRAN sp5))), t3] by Lm7

        .= [4, (( Head sp5) + ( offset ( TRAN sp5))), t3] by A56

        .= [4, (h + 0 ), t3] by A57;

      end;

      Rs = (( Computation (( Computation s) . (1 + 1))) . (((n + 1) + 1) + (j1 + 1))) by Th10

      .= (( Computation ( Following (( Computation s) . 1))) . (((n + 1) + 1) + (j1 + 1))) by Def7

      .= (( Computation ( Following s1)) . (((n + 1) + 1) + (j1 + 1))) by A17, Th9

      .= (( Computation (( Computation s2) . ((n + 1) + 1))) . (j1 + 1)) by A20, Th10

      .= (( Computation ( Following (( Computation s2) . (n + 1)))) . (j1 + 1)) by Def7;

      then Rs = (( Computation sp3) . (j1 + 1)) by A21, A42, A41, Def7;

      then

       A58: Rs = [4, h, t3] by A54, A55, Def7;

      

      then

       A59: (Rs `1_3 ) = 4

      .= the AcceptS of SuccTuring by Def17;

      hence s is Accept-Halt;

      then

       A60: ( Result s) = Rs by A59, Def9;

      hence (( Result s) `2_3 ) = h by A58;

      (( Result s) `3_3 ) = t3 by A58, A60;

      hence thesis by A40, Th16;

    end;

    theorem :: TURING_1:32

     SuccTuring computes (1 succ 1)

    proof

      now

        set sc = (1 succ 1);

        let s be All-State of SuccTuring , t be Tape of SuccTuring , h be Element of NAT , x be FinSequence of NAT ;

        assume that

         A1: x in ( dom sc) and

         A2: s = [the InitS of SuccTuring , h, t] and

         A3: t storeData ( <*h*> ^ x);

        

         A4: s = [ 0 , h, t] by A2, Def17;

        

         A5: ( dom sc) = (1 -tuples_on NAT ) by COMPUT_1:def 7;

        then x is Tuple of 1, NAT by A1, FINSEQ_2: 131;

        then

        consider i be Element of NAT such that

         A6: x = <*i*> by FINSEQ_2: 97;

        

         A7: ( <*h*> ^ x) = <*h, i*> by A6;

        hence s is Accept-Halt by A3, A4, Th31;

        take h2 = h;

        take y = (i + 1);

        thus (( Result s) `2_3 ) = h2 by A3, A4, A7, Th31;

        

        thus y = ((x /. 1) + 1) by A6, FINSEQ_4: 16

        .= (sc . x) by A1, A5, COMPUT_1:def 7;

        (( Result s) `3_3 ) storeData <*h2, (i + 1)*> by A3, A4, A7, Th31;

        hence (( Result s) `3_3 ) storeData ( <*h2*> ^ <*y*>);

      end;

      hence thesis;

    end;

    begin

    definition

      :: TURING_1:def18

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

      coherence

      proof

        reconsider p0 = 0 , p1 = 1, p2 = 2, p3 = 3, p4 = 4 as Element of ( SegM 4) by Th1;

        set A = [:( SegM 4), { 0 , 1}:], B = {( - 1), 0 , 1}, C = [:( SegM 4), { 0 , 1}, B:];

        reconsider b0 = 0 , b1 = 1 as Element of { 0 , 1} by TARSKI:def 2;

        reconsider L = ( - 1) as Element of B by ENUMSET1:def 1;

        reconsider R = 1 as Element of {( - 1), 0 , 1} by ENUMSET1:def 1;

        C = [:A, B:] by ZFMISC_1:def 3;

        then

        reconsider OP = ( id (A,B,R)) as Function of A, C;

        (((((( id (A,B,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)])) = (((((OP +* ( [p0, b0] .--> [p1, b0, R])) +* ( [p1, b1] .--> [p2, b1, R])) +* ( [p2, b0] .--> [p3, b0, L])) +* ( [p2, b1] .--> [p3, b0, L])) +* ( [p3, b1] .--> [p4, b1, L]));

        hence thesis;

      end;

    end

    theorem :: TURING_1:33

    

     Th33: ( 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

      set x = [1, 1];

      set x1 = [ 0 , 0 ];

      set p1 = ( [ 0 , 0 ] .--> [1, 0 , 1]), p2 = ( [1, 1] .--> [2, 1, 1]), p3 = ( [2, 0 ] .--> [3, 0 , ( - 1)]), p4 = ( [2, 1] .--> [3, 0 , ( - 1)]), f = ( id ( [:( SegM 4), { 0 , 1}:], {( - 1), 0 , 1},1));

      

      thus ( Zero_Tran . x1) = (((((f +* p1) +* p2) +* p3) +* p4) . x1) by Th2

      .= ((((f +* p1) +* p2) +* p3) . x1) by Th2

      .= (((f +* p1) +* p2) . x1) by Th2

      .= ((f +* p1) . x1) by Th3

      .= [1, 0 , 1] by FUNCT_7: 94;

      

      thus ( Zero_Tran . x) = (((((f +* p1) +* p2) +* p3) +* p4) . x) by Th2

      .= ((((f +* p1) +* p2) +* p3) . x) by Th2

      .= (((f +* p1) +* p2) . x) by Th3

      .= [2, 1, 1] by FUNCT_7: 94;

      set x = [2, 0 ];

      

      thus ( Zero_Tran . x) = (((((f +* p1) +* p2) +* p3) +* p4) . x) by Th3

      .= ((((f +* p1) +* p2) +* p3) . x) by Th3

      .= [3, 0 , ( - 1)] by FUNCT_7: 94;

      set x = [2, 1];

      

      thus ( Zero_Tran . x) = (((((f +* p1) +* p2) +* p3) +* p4) . x) by Th2

      .= [3, 0 , ( - 1)] by FUNCT_7: 94;

      thus thesis by FUNCT_7: 94;

    end;

    definition

      :: TURING_1:def19

      func ZeroTuring -> strict TuringStr means

      : Def19: 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

      proof

        set St = ( SegM 4);

        reconsider qF = 4 as Element of St by Th1;

        reconsider p0 = 0 as Element of St by Th1;

        set Sym = { 0 , 1};

        take TuringStr (# Sym, St, Zero_Tran , p0, qF #);

        thus thesis;

      end;

      uniqueness ;

    end

    

     Lm8: for n be Element of NAT st n <= 4 holds n is State of ZeroTuring

    proof

      let n be Element of NAT ;

      assume

       A1: n <= 4;

      the FStates of ZeroTuring = ( SegM 4) by Def19;

      hence thesis by A1, Th1;

    end;

    

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

    proof

       0 in { 0 , 1} & 1 in { 0 , 1} by TARSKI:def 2;

      hence thesis by Def19;

    end;

    

     Lm10: for s be All-State of ZeroTuring , p,h,t be 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

      let s be All-State of ZeroTuring , p,h,t be set;

      assume

       A1: s = [p, h, t] & p <> 4;

      4 = the AcceptS of ZeroTuring by Def19;

      hence thesis by A1, Th25;

    end;

    theorem :: TURING_1:34

    

     Th34: for s be All-State of ZeroTuring , t be Tape of ZeroTuring , head be Element of NAT , f be 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

      reconsider F = 0 as Symbol of ZeroTuring by Lm9;

      let s be All-State of ZeroTuring , t be Tape of ZeroTuring , h be Element of NAT , f be FinSequence of NAT ;

      assume that

       A1: ( len f) >= 1 and

       A2: s = [ 0 , h, t] and

       A3: t storeData ( <*h*> ^ f);

      reconsider s3 = (s `3_3 ) as Tape of ZeroTuring ;

      reconsider h1 = (h + 1) as Element of INT by INT_1:def 2;

      set m = (f /. 1), n = ((h + (f /. 1)) + 2);

      

       A4: h < h1 by XREAL_1: 29;

      reconsider p1 = 1 as State of ZeroTuring by Lm8;

      set s1 = [p1, h1, t];

      reconsider i2 = (h1 + 1) as Element of INT by INT_1:def 2;

      

       A5: h1 < i2 by XREAL_1: 29;

      reconsider T = 1 as Symbol of ZeroTuring by Lm9;

      set t1 = ( Tape-Chg (t,h1,T));

      set t2 = ( Tape-Chg (t1,i2,F));

      set t3 = ( Tape-Chg (t2,h1,T));

      

       A6: t is_1_between (h,n) by A1, A3, Th22;

      then

       A7: (t . h) = 0 ;

      then (t1 . h) = 0 by A4, Th26;

      then (t2 . h) = 0 by A4, A5, Th26;

      then

       A8: (t3 . h) = 0 by A4, Th26;

      

       A9: ( TRAN s) = ( Zero_Tran . [(s `1_3 ), (s3 . ( Head s))]) by Def19

      .= ( Zero_Tran . [ 0 , (s3 . ( Head s))]) by A2

      .= ( Zero_Tran . [ 0 , (t . ( Head s))]) by A2

      .= [1, 0 , 1] by A2, A7, Th33;

      then

       A10: ( offset ( TRAN s)) = 1;

      set Rs = (( Computation s) . (((1 + 1) + 1) + 1));

      reconsider p3 = 3 as State of ZeroTuring by Lm8;

      

       A11: ((h + 1) + 1) = ((h + 0 ) + 2);

      

       A12: (t3 . (h + 1)) = 1 by Th26;

       A13:

      now

        let k be Integer;

        assume h < k & k < ((h + 0 ) + 2);

        then (h + 1) <= k & k <= (h + 1) by A11, INT_1: 7;

        hence (t3 . k) = 1 by A12, XXREAL_0: 1;

      end;

      (t1 . (h + 1)) = 1 by Th26;

      then

       A14: (t2 . (h + 1)) = 1 by A5, Th26;

      set s3 = [p3, h1, t2];

      reconsider s33 = (s3 `3_3 ) as Tape of ZeroTuring ;

      

       A15: ( TRAN s3) = ( Zero_Tran . [(s3 `1_3 ), (s33 . ( Head s3))]) by Def19

      .= ( Zero_Tran . [p3, (s33 . ( Head s3))])

      .= ( Zero_Tran . [p3, (t2 . ( Head s3))])

      .= [4, 1, ( - 1)] by A14, Th33;

      then

       A16: ( offset ( TRAN s3)) = ( - 1);

      reconsider p2 = 2 as State of ZeroTuring by Lm8;

      reconsider s13 = (s1 `3_3 ) as Tape of ZeroTuring ;

      h <= (h + m) by NAT_1: 11;

      then

       A17: (h + 2) <= ((h + m) + 2) by XREAL_1: 7;

      h1 < (h + 2) by XREAL_1: 8;

      then

       A18: h1 < n by A17, XXREAL_0: 2;

      

       A19: ( TRAN s1) = ( Zero_Tran . [(s1 `1_3 ), (s13 . ( Head s1))]) by Def19

      .= ( Zero_Tran . [p1, (s13 . ( Head s1))])

      .= ( Zero_Tran . [p1, (t . ( Head s1))])

      .= ( Zero_Tran . [1, (t . h1)])

      .= [2, 1, 1] by A6, A4, A18, Th33;

      then

       A20: ( offset ( TRAN s1)) = 1;

       A21:

      now

        

         A22: the Symbols of ZeroTuring = { 0 , 1} by Def19;

        per cases by A22, TARSKI:def 2;

          suppose (t1 . i2) = 1;

          hence ( Zero_Tran . [2, (t1 . i2)]) = [3, 0 , ( - 1)] by Th33;

        end;

          suppose (t1 . i2) = 0 ;

          hence ( Zero_Tran . [2, (t1 . i2)]) = [3, 0 , ( - 1)] by Th33;

        end;

      end;

      set s2 = [p2, i2, t1];

      reconsider s23 = (s2 `3_3 ) as Tape of ZeroTuring ;

      

       A23: ( TRAN s2) = ( Zero_Tran . [(s2 `1_3 ), (s23 . ( Head s2))]) by Def19

      .= ( Zero_Tran . [p2, (s23 . ( Head s2))])

      .= ( Zero_Tran . [p2, (t1 . ( Head s2))])

      .= [3, 0 , ( - 1)] by A21;

      then

       A24: ( offset ( TRAN s2)) = ( - 1);

      ( Tape-Chg ((s2 `3_3 ),( Head s2),(( TRAN s2) `2_3 ))) = ( Tape-Chg (t1,( Head s2),(( TRAN s2) `2_3 )))

      .= ( Tape-Chg (t1,i2,(( TRAN s2) `2_3 )))

      .= t2 by A23;

      

      then

       A25: ( Following s2) = [(( TRAN s2) `1_3 ), (( Head s2) + ( offset ( TRAN s2))), t2] by Lm10

      .= [3, (( Head s2) + ( offset ( TRAN s2))), t2] by A23

      .= s3 by A24;

      reconsider p3 = 3 as State of ZeroTuring by Lm8;

      

       A26: ( Tape-Chg ((s3 `3_3 ),( Head s3),(( TRAN s3) `2_3 ))) = ( Tape-Chg (t2,( Head s3),(( TRAN s3) `2_3 )))

      .= ( Tape-Chg (t2,h1,(( TRAN s3) `2_3 )))

      .= t3 by A15;

      set s3 = [p3, h1, t2];

      

       A27: ( Following s3) = [(( TRAN s3) `1_3 ), (( Head s3) + ( offset ( TRAN s3))), t3] by A26, Lm10

      .= [4, (( Head s3) + ( offset ( TRAN s3))), t3] by A15

      .= [4, h, t3] by A16;

      ( Tape-Chg ((s `3_3 ),( Head s),(( TRAN s) `2_3 ))) = ( Tape-Chg (t,( Head s),(( TRAN s) `2_3 ))) by A2

      .= ( Tape-Chg (t,h,(( TRAN s) `2_3 ))) by A2

      .= ( Tape-Chg (t,h,F)) by A9

      .= t by A7, Th24;

      

      then

       A28: ( Following s) = [(( TRAN s) `1_3 ), (( Head s) + ( offset ( TRAN s))), t] by A2, Lm10

      .= [1, (( Head s) + ( offset ( TRAN s))), t] by A9

      .= s1 by A2, A10;

      ( Tape-Chg ((s1 `3_3 ),( Head s1),(( TRAN s1) `2_3 ))) = ( Tape-Chg (t,( Head s1),(( TRAN s1) `2_3 )))

      .= ( Tape-Chg (t,h1,(( TRAN s1) `2_3 )))

      .= t1 by A19;

      

      then

       A29: ( Following s1) = [(( TRAN s1) `1_3 ), (( Head s1) + ( offset ( TRAN s1))), t1] by Lm10

      .= [2, (( Head s1) + ( offset ( TRAN s1))), t1] by A19

      .= s2 by A20;

      

       A30: Rs = ( Following (( Computation s) . ((1 + 1) + 1))) by Def7

      .= ( Following ( Following (( Computation s) . (1 + 1)))) by Def7

      .= ( Following ( Following ( Following (( Computation s) . 1)))) by Def7

      .= [4, h, t3] by A28, A29, A25, A27, Th9;

      

      then

       A31: (Rs `1_3 ) = 4

      .= the AcceptS of ZeroTuring by Def19;

      hence s is Accept-Halt;

      then

       A32: ( Result s) = Rs by A31, Def9;

      hence (( Result s) `2_3 ) = h by A30;

      

       A33: (( Result s) `3_3 ) = t3 by A30, A32;

      (t2 . i2) = 0 by Th26;

      then (t3 . i2) = 0 by A5, Th26;

      then t3 is_1_between (h,((h + 0 ) + 2)) by A8, A13;

      hence thesis by A33, Th16;

    end;

    theorem :: TURING_1:35

    n >= 1 implies ZeroTuring computes (n const 0 )

    proof

      assume

       A1: n >= 1;

      now

        set cs = (n const 0 );

        let s be All-State of ZeroTuring , t be Tape of ZeroTuring , h be Element of NAT , x be FinSequence of NAT ;

        assume that

         A2: x in ( dom cs) and

         A3: s = [the InitS of ZeroTuring , h, t] and

         A4: t storeData ( <*h*> ^ x);

        x in (n -tuples_on NAT ) by A2;

        then x in { f where f be Element of ( NAT * ) : ( len f) = n } by FINSEQ_2:def 4;

        then

         A6: ex f be Element of ( NAT * ) st x = f & ( len f) = n;

        

         A7: s = [ 0 , h, t] by A3, Def19;

        hence s is Accept-Halt by A1, A4, A6, Th34;

        take h2 = h;

        take y = 0 ;

        thus (( Result s) `2_3 ) = h2 by A1, A4, A6, A7, Th34;

        thus y = (cs . x) by A2, FUNCOP_1: 7;

        (( Result s) `3_3 ) storeData <*h2, 0 *> by A1, A4, A6, A7, Th34;

        hence (( Result s) `3_3 ) storeData ( <*h2*> ^ <*y*>);

      end;

      hence thesis;

    end;

    begin

    definition

      :: TURING_1:def20

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

      coherence

      proof

        reconsider p0 = 0 , p1 = 1, p2 = 2, p3 = 3 as Element of ( SegM 3) by Th1;

        set A = [:( SegM 3), { 0 , 1}:], B = {( - 1), 0 , 1}, C = [:( SegM 3), { 0 , 1}, B:];

        reconsider b0 = 0 , b1 = 1 as Element of { 0 , 1} by TARSKI:def 2;

        reconsider h = 0 , R = 1 as Element of B by ENUMSET1:def 1;

        C = [:A, B:] by ZFMISC_1:def 3;

        then

        reconsider OP = ( id (A,B,h)) as Function of A, C;

        (((((( id (A,B, 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 ])) = (((((OP +* ( [p0, b0] .--> [p1, b0, R])) +* ( [p1, b1] .--> [p1, b0, R])) +* ( [p1, b0] .--> [p2, b0, R])) +* ( [p2, b1] .--> [p2, b0, R])) +* ( [p2, b0] .--> [p3, b0, h]));

        hence thesis;

      end;

    end

    theorem :: TURING_1:36

    

     Th36: ( 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

      set x = [1, 1];

      set x1 = [ 0 , 0 ];

      set p1 = ( [ 0 , 0 ] .--> [1, 0 , 1]), p2 = ( [1, 1] .--> [1, 0 , 1]), p3 = ( [1, 0 ] .--> [2, 0 , 1]), p4 = ( [2, 1] .--> [2, 0 , 1]), f = ( id ( [:( SegM 3), { 0 , 1}:], {( - 1), 0 , 1}, 0 ));

      

      thus ( U3(n)Tran . x1) = (((((f +* p1) +* p2) +* p3) +* p4) . x1) by Th2

      .= ((((f +* p1) +* p2) +* p3) . x1) by Th2

      .= (((f +* p1) +* p2) . x1) by Th2

      .= ((f +* p1) . x1) by Th3

      .= [1, 0 , 1] by FUNCT_7: 94;

      

      thus ( U3(n)Tran . x) = (((((f +* p1) +* p2) +* p3) +* p4) . x) by Th2

      .= ((((f +* p1) +* p2) +* p3) . x) by Th2

      .= (((f +* p1) +* p2) . x) by Th3

      .= [1, 0 , 1] by FUNCT_7: 94;

      set x = [1, 0 ];

      

      thus ( U3(n)Tran . x) = (((((f +* p1) +* p2) +* p3) +* p4) . x) by Th2

      .= ((((f +* p1) +* p2) +* p3) . x) by Th3

      .= [2, 0 , 1] by FUNCT_7: 94;

      set x = [2, 1];

      

      thus ( U3(n)Tran . x) = (((((f +* p1) +* p2) +* p3) +* p4) . x) by Th3

      .= [2, 0 , 1] by FUNCT_7: 94;

      thus thesis by FUNCT_7: 94;

    end;

    definition

      :: TURING_1:def21

      func U3(n)Turing -> strict TuringStr means

      : Def21: 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

      proof

        set St = ( SegM 3);

        reconsider qF = 3 as Element of St by Th1;

        reconsider p0 = 0 as Element of St by Th1;

        set Sym = { 0 , 1};

        take TuringStr (# Sym, St, U3(n)Tran , p0, qF #);

        thus thesis;

      end;

      uniqueness ;

    end

    

     Lm11: for n be Element of NAT st n <= 3 holds n is State of U3(n)Turing

    proof

      let n be Element of NAT ;

      assume

       A1: n <= 3;

      the FStates of U3(n)Turing = ( SegM 3) by Def21;

      hence thesis by A1, Th1;

    end;

    

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

    proof

       0 in { 0 , 1} & 1 in { 0 , 1} by TARSKI:def 2;

      hence thesis by Def21;

    end;

    

     Lm13: for s be All-State of U3(n)Turing , p,h,t be 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

      let s be All-State of U3(n)Turing , p,h,t be set;

      assume

       A1: s = [p, h, t] & p <> 3;

      3 = the AcceptS of U3(n)Turing by Def21;

      hence thesis by A1, Th25;

    end;

    

     Lm14: for tm be TuringStr, s be All-State of tm, p be State of tm, h be Element of INT , t be Tape of tm, m,d be 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 be Integer st d <= i & i < (d + m) holds (t . i) = 1) holds ex t1 be Tape of tm st (( Computation s) . m) = [p, (d + m), t1] & (for i be Integer st d <= i & i < (d + m) holds (t1 . i) = 0 ) & for i be Integer st d > i or i >= (d + m) holds (t1 . i) = (t . i)

    proof

      let tm be TuringStr, s be All-State of tm, p be State of tm, h be Element of INT , t be Tape of tm, m,d be Element of NAT ;

      assume that

       A1: d = h and

       A2: 0 is Symbol of tm and

       A3: s = [p, h, t] and

       A4: (the Tran of tm . [p, 1]) = [p, 0 , 1] and

       A5: p <> the AcceptS of tm and

       A6: for i be Integer st d <= i & i < (d + m) holds (t . i) = 1;

      defpred Q[ Nat] means $1 <= m implies ex t1 be Tape of tm st (( Computation s) . $1) = [p, (d + $1), t1] & (for i be Integer st d <= i & i < (d + $1) holds (t1 . i) = 0 ) & (for i be Integer st d > i or i >= (d + $1) holds (t1 . i) = (t . i));

      

       A7: for k be Nat st Q[k] holds Q[(k + 1)]

      proof

        let k be Nat;

        assume

         A8: Q[k];

        now

          reconsider F = 0 as Symbol of tm by A2;

          set dk = (d + k);

          reconsider ik = (d + k) as Element of INT by INT_1:def 2;

          assume

           A9: (k + 1) <= m;

          then

          consider t1 be Tape of tm such that

           A10: (( Computation s) . k) = [p, (d + k), t1] and

           A11: for i be Integer st d <= i & i < (d + k) holds (t1 . i) = 0 and

           A12: for i be Integer st d > i or i >= (d + k) holds (t1 . i) = (t . i) by A8, NAT_1: 13;

          k < m by A9, NAT_1: 13;

          then

           A13: dk < (d + m) by XREAL_1: 8;

          

           A14: (t1 . ik) = (t . ik) by A12

          .= 1 by A6, A13, NAT_1: 11;

          take t2 = ( Tape-Chg (t1,dk,F));

          set sk = [p, ik, t1];

          reconsider tt = (sk `3_3 ) as Tape of tm;

          

           A15: ( TRAN sk) = (the Tran of tm . [p, (tt . ( Head sk))])

          .= (the Tran of tm . [p, (t1 . ( Head sk))])

          .= [p, 0 , 1] by A4, A14;

          then

           A16: ( offset ( TRAN sk)) = 1;

          

           A17: ( Tape-Chg ((sk `3_3 ),( Head sk),(( TRAN sk) `2_3 ))) = ( Tape-Chg (t1,( Head sk),(( TRAN sk) `2_3 )))

          .= ( Tape-Chg (t1,dk,(( TRAN sk) `2_3 )))

          .= t2 by A15;

          

          thus (( Computation s) . (k + 1)) = ( Following sk) by A10, Def7

          .= [(( TRAN sk) `1_3 ), (( Head sk) + ( offset ( TRAN sk))), t2] by A5, A17, Th25

          .= [p, (( Head sk) + ( offset ( TRAN sk))), t2] by A15

          .= [p, (dk + 1), t2] by A16

          .= [p, (d + (k + 1)), t2];

          hereby

            let i be Integer;

            assume that

             A18: d <= i and

             A19: i < (d + (k + 1));

            per cases ;

              suppose i = dk;

              hence (t2 . i) = 0 by Th26;

            end;

              suppose

               A20: i <> dk;

              i < ((d + k) + 1) by A19;

              then i <= (d + k) by INT_1: 7;

              then

               A21: i < dk by A20, XXREAL_0: 1;

              

              thus (t2 . i) = (t1 . i) by A20, Th26

              .= 0 by A11, A18, A21;

            end;

          end;

          hereby

            let i be Integer;

            assume

             A22: d > i or i >= (d + (k + 1));

            per cases by A22;

              suppose

               A23: d > i;

              d <= (d + k) by NAT_1: 12;

              

              hence (t2 . i) = (t1 . i) by A23, Th26

              .= (t . i) by A12, A23;

            end;

              suppose

               A24: i >= (d + (k + 1));

              k < (k + 1) by NAT_1: 13;

              then

               A25: (d + k) < (d + (k + 1)) by XREAL_1: 8;

              then

               A26: i > (d + k) by A24, XXREAL_0: 2;

              

              thus (t2 . i) = (t1 . i) by A24, A25, Th26

              .= (t . i) by A12, A26;

            end;

          end;

        end;

        hence thesis;

      end;

      

       A27: Q[ 0 ]

      proof

        assume 0 <= m;

        take t1 = t;

        thus (( Computation s) . 0 ) = [p, (d + 0 ), t1] by A1, A3, Def7;

        thus for i be Integer st d <= i & i < (d + 0 ) holds (t1 . i) = 0 ;

        thus thesis;

      end;

      for k holds Q[k] from NAT_1:sch 2( A27, A7);

      hence thesis;

    end;

    theorem :: TURING_1:37

    

     Th37: for s be All-State of U3(n)Turing , t be Tape of U3(n)Turing , head be Element of NAT , f be 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

      reconsider F = 0 as Symbol of U3(n)Turing by Lm12;

      let s be All-State of U3(n)Turing , t be Tape of U3(n)Turing , h be Element of NAT , f be FinSequence of NAT ;

      assume that

       A1: ( len f) >= 3 and

       A2: s = [ 0 , h, t] and

       A3: t storeData ( <*h*> ^ f);

      set n1 = ((h + (f /. 1)) + 2), n2 = (((h + (f /. 1)) + (f /. 2)) + 4), n3 = ((((h + (f /. 1)) + (f /. 2)) + (f /. 3)) + 6);

      reconsider s03 = (s `3_3 ) as Tape of U3(n)Turing ;

      

       A4: t is_1_between (h,n1) by A1, A3, Th23;

      then

       A5: (t . h) = 0 ;

      

       A6: ( TRAN s) = ( U3(n)Tran . [(s `1_3 ), (s03 . ( Head s))]) by Def21

      .= ( U3(n)Tran . [ 0 , (s03 . ( Head s))]) by A2

      .= ( U3(n)Tran . [ 0 , (t . ( Head s))]) by A2

      .= [1, 0 , 1] by A2, A5, Th36;

      then

       A7: ( offset ( TRAN s)) = 1;

      reconsider p1 = 1 as State of U3(n)Turing by Lm11;

      set m1 = ((f /. 1) + 1);

      reconsider h1 = (h + 1) as Element of INT by INT_1:def 2;

      set s1 = [p1, h1, t];

      

       A8: t is_1_between (n1,n2) by A1, A3, Th23;

      then

       A9: (t . n2) = 0 ;

      ( Tape-Chg ((s `3_3 ),( Head s),(( TRAN s) `2_3 ))) = ( Tape-Chg (t,( Head s),(( TRAN s) `2_3 ))) by A2

      .= ( Tape-Chg (t,h,(( TRAN s) `2_3 ))) by A2

      .= ( Tape-Chg (t,h,F)) by A6

      .= t by A5, Th24;

      

      then

       A10: ( Following s) = [(( TRAN s) `1_3 ), (( Head s) + ( offset ( TRAN s))), t] by A2, Lm13

      .= [1, (( Head s) + ( offset ( TRAN s))), t] by A6

      .= s1 by A2, A7;

      

       A11: t is_1_between (n2,n3) by A1, A3, Th23;

      then

       A12: (t . n3) = 0 ;

      reconsider p2 = 2 as State of U3(n)Turing by Lm11;

      set s2 = (( Computation s1) . m1);

      reconsider s23 = (s2 `3_3 ) as Tape of U3(n)Turing ;

      set j1 = (((h + 1) + m1) + 1);

      reconsider k1 = j1 as Element of INT by INT_1:def 2;

      set m2 = ((f /. 2) + 1);

      set Rs = (( Computation s) . ((((m2 + 1) + 1) + m1) + 1));

      set m3 = ((n2 + (f /. 3)) + 2);

       A13:

      now

        let i be Integer;

        assume that

         A14: (h + 1) <= i and

         A15: i < ((h + 1) + m1);

        h < (h + 1) by XREAL_1: 29;

        then h < i by A14, XXREAL_0: 2;

        hence (t . i) = 1 by A4, A15;

      end;

      (the Tran of U3(n)Turing . [p1, 1]) = [p1, 0 , 1] & p1 <> the AcceptS of U3(n)Turing by Def21, Th36;

      then

      consider t1 be Tape of U3(n)Turing such that

       A16: s2 = [p1, ((h + 1) + m1), t1] and for i be Integer st (h + 1) <= i & i < ((h + 1) + m1) holds (t1 . i) = 0 and

       A17: for i be Integer st (h + 1) > i or i >= ((h + 1) + m1) holds (t1 . i) = (t . i) by A13, Lm12, Lm14;

      (t . n1) = 0 by A4;

      then

       A18: (t1 . ((h + 1) + m1)) = 0 by A17;

      

       A19: ( TRAN s2) = ( U3(n)Tran . [(s2 `1_3 ), (s23 . ( Head s2))]) by Def21

      .= ( U3(n)Tran . [p1, (s23 . ( Head s2))]) by A16

      .= ( U3(n)Tran . [1, (t1 . ( Head s2))]) by A16

      .= [2, 0 , 1] by A16, A18, Th36;

      then

       A20: ( offset ( TRAN s2)) = 1;

      set s3 = [p2, k1, t1];

      ( Tape-Chg ((s2 `3_3 ),( Head s2),(( TRAN s2) `2_3 ))) = ( Tape-Chg (t1,( Head s2),(( TRAN s2) `2_3 ))) by A16

      .= ( Tape-Chg (t1,((h + 1) + m1),(( TRAN s2) `2_3 ))) by A16

      .= ( Tape-Chg (t1,((h + 1) + m1),F)) by A19

      .= t1 by A18, Th24;

      

      then

       A21: ( Following s2) = [(( TRAN s2) `1_3 ), (( Head s2) + ( offset ( TRAN s2))), t1] by A16, Lm13

      .= [2, (( Head s2) + ( offset ( TRAN s2))), t1] by A19

      .= s3 by A16, A20;

       A22:

      now

        let i be Integer;

        assume that

         A23: j1 <= i and

         A24: i < (j1 + m2);

        ((h + 1) + m1) < j1 by XREAL_1: 29;

        then

         A25: ((h + 1) + m1) < i by A23, XXREAL_0: 2;

        

        hence (t1 . i) = (t . i) by A17

        .= 1 by A8, A24, A25;

      end;

      set s4 = (( Computation s3) . m2);

      reconsider s43 = (s4 `3_3 ) as Tape of U3(n)Turing ;

      (the Tran of U3(n)Turing . [p2, 1]) = [p2, 0 , 1] & p2 <> the AcceptS of U3(n)Turing by Def21, Th36;

      then

      consider t2 be Tape of U3(n)Turing such that

       A26: s4 = [p2, (j1 + m2), t2] and for i be Integer st j1 <= i & i < (j1 + m2) holds (t2 . i) = 0 and

       A27: for i be Integer st j1 > i or i >= (j1 + m2) holds (t2 . i) = (t1 . i) by A22, Lm12, Lm14;

      2 <= ((f /. 2) + 4) by NAT_1: 12;

      then

       A28: n1 <= ((h + (f /. 1)) + ((f /. 2) + 4)) by XREAL_1: 7;

       A29:

      now

        let k be Integer;

        assume that

         A30: n2 < k and

         A31: k < m3;

        

         A32: n1 <= k by A28, A30, XXREAL_0: 2;

        

        thus (t2 . k) = (t1 . k) by A27, A30

        .= (t . k) by A17, A32

        .= 1 by A11, A30, A31;

      end;

      

       A33: (t2 . (j1 + m2)) = (t1 . (j1 + m2)) by A27

      .= 0 by A9, A17, A28;

      

       A34: ( TRAN s4) = ( U3(n)Tran . [(s4 `1_3 ), (s43 . ( Head s4))]) by Def21

      .= ( U3(n)Tran . [p2, (s43 . ( Head s4))]) by A26

      .= ( U3(n)Tran . [2, (t2 . ( Head s4))]) by A26

      .= [3, 0 , 0 ] by A26, A33, Th36;

      then

       A35: ( offset ( TRAN s4)) = 0 ;

      ( Tape-Chg ((s4 `3_3 ),( Head s4),(( TRAN s4) `2_3 ))) = ( Tape-Chg (t2,( Head s4),(( TRAN s4) `2_3 ))) by A26

      .= ( Tape-Chg (t2,(j1 + m2),(( TRAN s4) `2_3 ))) by A26

      .= ( Tape-Chg (t2,(j1 + m2),F)) by A34

      .= t2 by A33, Th24;

      

      then

       A36: ( Following s4) = [(( TRAN s4) `1_3 ), (( Head s4) + ( offset ( TRAN s4))), t2] by A26, Lm13

      .= [3, (( Head s4) + ( offset ( TRAN s4))), t2] by A34

      .= [3, ((j1 + m2) + 0 ), t2] by A26, A35;

      Rs = (( Computation (( Computation s) . 1)) . (((m2 + 1) + 1) + m1)) by Th10

      .= (( Computation s1) . (((m2 + 1) + 1) + m1)) by A10, Th9

      .= (( Computation s2) . ((m2 + 1) + 1)) by Th10;

      

      then

       A37: Rs = (( Computation (( Computation s2) . 1)) . (m2 + 1)) by Th10

      .= (( Computation s3) . (m2 + 1)) by A21, Th9

      .= [3, (j1 + m2), t2] by A36, Def7;

      

      then

       A38: (Rs `1_3 ) = 3

      .= the AcceptS of U3(n)Turing by Def21;

      hence s is Accept-Halt;

      then

       A39: ( Result s) = Rs by A38, Def9;

      hence (( Result s) `2_3 ) = n2 by A37;

      

       A40: (( Result s) `3_3 ) = t2 by A37, A39;

      

       A41: n2 <= (n2 + ((f /. 3) + 2)) by NAT_1: 11;

      then

       A42: n1 <= m3 by A28, XXREAL_0: 2;

      (t2 . m3) = (t1 . m3) by A27, A41

      .= 0 by A12, A17, A42;

      then t2 is_1_between (n2,((n2 + (f /. 3)) + 2)) by A33, A29;

      hence thesis by A40, Th16;

    end;

    theorem :: TURING_1:38

    n >= 3 implies U3(n)Turing computes (n proj 3)

    proof

      assume

       A1: n >= 3;

      now

        set pj = (n proj 3);

        let s be All-State of U3(n)Turing , t be Tape of U3(n)Turing , h be Element of NAT , x be FinSequence of NAT ;

        assume that

         A2: x in ( dom pj) and

         A3: s = [the InitS of U3(n)Turing , h, t] and

         A4: t storeData ( <*h*> ^ x);

        reconsider nn = n as Element of NAT by ORDINAL1:def 12;

        set pj = (nn proj 3);

        ( arity pj) = n by COMPUT_1: 37;

        then

         A5: ( dom pj) c= (n -tuples_on NAT ) by COMPUT_1: 21;

        then x in (n -tuples_on NAT ) by A2;

        then x in { f where f be Element of ( NAT * ) : ( len f) = n } by FINSEQ_2:def 4;

        then

         A6: ex f be Element of ( NAT * ) st x = f & ( len f) = n;

        

         A7: s = [ 0 , h, t] by A3, Def21;

        hence s is Accept-Halt by A1, A4, A6, Th37;

        take h2 = (((h + (x /. 1)) + (x /. 2)) + 4);

        take y = (x /. 3);

        thus (( Result s) `2_3 ) = h2 by A1, A4, A6, A7, Th37;

        

        thus y = (x . 3) by A1, A6, FINSEQ_4: 15

        .= (pj . x) by A2, A5, COMPUT_1: 38

        .= ((n proj 3) . x);

        (( Result s) `3_3 ) storeData <*h2, y*> by A1, A4, A6, A7, Th37;

        hence (( Result s) `3_3 ) storeData ( <*h2*> ^ <*y*>);

      end;

      hence thesis;

    end;

    begin

    definition

      let t1,t2 be TuringStr;

      :: TURING_1:def22

      func UnionSt (t1,t2) -> finite non empty set equals ( [:the FStates of t1, {the InitS of t2}:] \/ [: {the AcceptS of t1}, the FStates of t2:]);

      correctness ;

    end

    theorem :: TURING_1:39

    

     Th39: for t1,t2 be 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

      let t1,t2 be TuringStr;

      set p0 = the InitS of t1, q0 = the InitS of t2, p1 = the AcceptS of t1, q1 = the AcceptS of t2, A = [:the FStates of t1, {q0}:], B = [: {p1}, the FStates of t2:];

      reconsider q = q0 as Element of {q0} by TARSKI:def 1;

      reconsider p = p1 as Element of {p1} by TARSKI:def 1;

       [p0, q] in A;

      hence [p0, q0] in ( UnionSt (t1,t2)) by XBOOLE_0:def 3;

       [p, q1] in B;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: TURING_1:40

    

     Th40: for s,t be TuringStr, x be State of s holds [x, the InitS of t] in ( UnionSt (s,t))

    proof

      let s,t be TuringStr, x be State of s;

      set q0 = the InitS of t, A = [:the FStates of s, {q0}:];

      reconsider q = q0 as Element of {q0} by TARSKI:def 1;

       [x, q] in A;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: TURING_1:41

    

     Th41: for s,t be TuringStr, x be State of t holds [the AcceptS of s, x] in ( UnionSt (s,t))

    proof

      let s,t be TuringStr, x be State of t;

      set p1 = the AcceptS of s, B = [: {p1}, the FStates of t:];

      reconsider p = p1 as Element of {p1} by TARSKI:def 1;

       [p, x] in B;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: TURING_1:42

    

     Th42: for s,t be TuringStr, x be Element of ( UnionSt (s,t)) holds ex x1 be State of s, x2 be State of t st x = [x1, x2]

    proof

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

      set q0 = the InitS of t, p1 = the AcceptS of s, A = [:the FStates of s, {q0}:], B = [: {p1}, the FStates of t:];

      per cases by XBOOLE_0:def 3;

        suppose x in A;

        then

        consider x1 be State of s, x2 be Element of {q0} such that

         A1: x = [x1, x2] by DOMAIN_1: 1;

        take x1, q0;

        thus thesis by A1, TARSKI:def 1;

      end;

        suppose x in B;

        then

        consider x1 be Element of {p1}, x2 be State of t such that

         A2: x = [x1, x2] by DOMAIN_1: 1;

        take p1, x2;

        thus thesis by A2, TARSKI:def 1;

      end;

    end;

    definition

      let s,t be TuringStr, x be Tran-Goal of s;

      :: TURING_1:def23

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

      coherence

      proof

        reconsider y1 = [(x `1_3 ), the InitS of t] as Element of ( UnionSt (s,t)) by Th40;

        set Sym = (the Symbols of s \/ the Symbols of t);

        reconsider y2 = (x `2_3 ) as Element of Sym by XBOOLE_0:def 3;

         [y1, y2, (x `3_3 )] in [:( UnionSt (s,t)), Sym, {( - 1), 0 , 1}:];

        hence thesis;

      end;

    end

    definition

      let s,t be TuringStr, x be Tran-Goal of t;

      :: TURING_1:def24

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

      coherence

      proof

        reconsider y1 = [the AcceptS of s, (x `1_3 )] as Element of ( UnionSt (s,t)) by Th41;

        set Sym = (the Symbols of s \/ the Symbols of t);

        reconsider y2 = (x `2_3 ) as Element of Sym by XBOOLE_0:def 3;

         [y1, y2, (x `3_3 )] in [:( UnionSt (s,t)), Sym, {( - 1), 0 , 1}:];

        hence thesis;

      end;

    end

    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

        consider x1 be State of s, x2 be State of t such that

         A1: x = [x1, x2] by Th42;

        thus thesis by A1;

      end;

      :: original: `2

      redefine

      func x `2 -> State of t ;

      coherence

      proof

        consider x1 be State of s, x2 be State of t such that

         A2: x = [x1, x2] by Th42;

        thus thesis by A2;

      end;

    end

    definition

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

      :: TURING_1:def25

      func FirstTuringState x -> State of s equals ((x `1 ) `1 );

      correctness ;

      :: TURING_1:def26

      func SecondTuringState x -> State of t equals ((x `1 ) `2 );

      correctness ;

    end

    definition

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

      given u be set, y be Element of Y such that

       A1: x = [u, y];

      :: TURING_1:def27

      func FirstTuringSymbol (x) -> Element of Y equals

      : Def27: (x `2 );

      coherence by A1;

    end

    definition

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

      given u be set, z be Element of Z such that

       A1: x = [u, z];

      :: TURING_1:def28

      func SecondTuringSymbol (x) -> Element of Z equals

      : Def28: (x `2 );

      coherence by A1;

    end

    definition

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

      :: TURING_1:def29

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

      : Def29: ( FirstTuringTran (s,t,(the Tran of s . [( FirstTuringState x), ( FirstTuringSymbol x)]))) if ex p be State of s, y be 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 be State of t, y be Symbol of t st x = [ [the AcceptS of s, q], y]

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

      consistency

      proof

        let w be Element of [:( UnionSt (s,t)), (the Symbols of s \/ the Symbols of t), {( - 1), 0 , 1}:];

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

        proof

          given p be State of s, y be Symbol of s such that

           A1: x = [ [p, the InitS of t], y] and

           A2: p <> the AcceptS of s;

          given q be State of t, z be Symbol of t such that

           A3: x = [ [the AcceptS of s, q], z];

           [p, the InitS of t] = [the AcceptS of s, q] by A1, A3, XTUPLE_0: 1;

          hence thesis by A2, XTUPLE_0: 1;

        end;

      end;

      coherence

      proof

        reconsider l = ( - 1) as Element of {( - 1), 0 , 1} by ENUMSET1:def 1;

         [(x `1 ), (x `2 ), l] in [:( UnionSt (s,t)), (the Symbols of s \/ the Symbols of t), {( - 1), 0 , 1}:];

        hence thesis;

      end;

    end

    definition

      let s,t be TuringStr;

      :: TURING_1:def30

      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: for x be Element of [:( UnionSt (s,t)), (the Symbols of s \/ the Symbols of t):] holds (it . x) = ( Uniontran (s,t,x));

      existence

      proof

        set Sm = (the Symbols of s \/ the Symbols of t), X = [:( UnionSt (s,t)), Sm:];

        deffunc U( Element of X) = ( Uniontran (s,t,$1));

        consider f be Function of X, [:( UnionSt (s,t)), Sm, {( - 1), 0 , 1}:] such that

         A1: for x be Element of X holds (f . x) = U(x) from FUNCT_2:sch 4;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        set Sm = (the Symbols of s \/ the Symbols of t), X = [:( UnionSt (s,t)), Sm:];

        let f,g be Function of X, [:( UnionSt (s,t)), Sm, {( - 1), 0 , 1}:] such that

         A2: for x be Element of X holds (f . x) = ( Uniontran (s,t,x)) and

         A3: for x be Element of X holds (g . x) = ( Uniontran (s,t,x));

        now

          let x be Element of X;

          

          thus (f . x) = ( Uniontran (s,t,x)) by A2

          .= (g . x) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let T1,T2 be TuringStr;

      :: TURING_1:def31

      func T1 ';' T2 -> strict TuringStr means

      : Def31: 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

      proof

        set St = ( UnionSt (T1,T2));

        reconsider q1 = [the AcceptS of T1, the AcceptS of T2] as Element of St by Th39;

        reconsider p0 = [the InitS of T1, the InitS of T2] as Element of St by Th39;

        set Sym = (the Symbols of T1 \/ the Symbols of T2);

        take TuringStr (# Sym, St, ( UnionTran (T1,T2)), p0, q1 #);

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: TURING_1:43

    

     Th43: for T1,T2 be TuringStr, g be Tran-Goal of T1, p be State of T1, y be 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

      let t1,t2 be TuringStr, g be Tran-Goal of t1, p be State of t1, y be Symbol of t1;

      assume that

       A1: p <> the AcceptS of t1 and

       A2: g = (the Tran of t1 . [p, y]);

      set q0 = the InitS of t2;

      set x = [ [p, q0], y];

      q0 in {q0} by TARSKI:def 1;

      then [p, q0] in [:the FStates of t1, {q0}:] by ZFMISC_1:def 2;

      then

       A3: [p, q0] in ( [:the FStates of t1, {q0}:] \/ [: {the AcceptS of t1}, the FStates of t2:]) by XBOOLE_0:def 3;

      y in (the Symbols of t1 \/ the Symbols of t2) by XBOOLE_0:def 3;

      then

      reconsider xx = x as Element of [:( UnionSt (t1,t2)), (the Symbols of t1 \/ the Symbols of t2):] by A3, ZFMISC_1:def 2;

      

       A4: ( FirstTuringState xx) = (( [ [p, q0], y] `1 ) `1 )

      .= ( [p, q0] `1 )

      .= p;

      

       A5: ( FirstTuringSymbol xx) = ( [ [p, q0], y] `2 ) by Def27

      .= y;

      

      thus (the Tran of (t1 ';' t2) . x) = (( UnionTran (t1,t2)) . xx) by Def31

      .= ( Uniontran (t1,t2,xx)) by Def30

      .= ( FirstTuringTran (t1,t2,(the Tran of t1 . [p, y]))) by A1, A4, A5, Def29

      .= [ [(g `1_3 ), q0], (g `2_3 ), (g `3_3 )] by A2;

    end;

    theorem :: TURING_1:44

    

     Th44: for T1,T2 be TuringStr, g be Tran-Goal of T2, q be State of T2, y be 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

      let t1,t2 be TuringStr, g be Tran-Goal of t2, q be State of t2, y be Symbol of t2;

      assume

       A1: g = (the Tran of t2 . [q, y]);

      set pF = the AcceptS of t1;

      set x = [ [pF, q], y];

      pF in {pF} by TARSKI:def 1;

      then [pF, q] in [: {pF}, the FStates of t2:] by ZFMISC_1:def 2;

      then

       A2: [pF, q] in ( [:the FStates of t1, {the InitS of t2}:] \/ [: {pF}, the FStates of t2:]) by XBOOLE_0:def 3;

      y in (the Symbols of t1 \/ the Symbols of t2) by XBOOLE_0:def 3;

      then

      reconsider xx = x as Element of [:( UnionSt (t1,t2)), (the Symbols of t1 \/ the Symbols of t2):] by A2, ZFMISC_1:def 2;

      

       A3: ( SecondTuringState xx) = (( [ [pF, q], y] `1 ) `2 )

      .= q;

      

       A4: ( SecondTuringSymbol xx) = ( [ [pF, q], y] `2 ) by Def28

      .= y;

      

      thus (the Tran of (t1 ';' t2) . x) = (( UnionTran (t1,t2)) . xx) by Def31

      .= ( Uniontran (t1,t2,xx)) by Def30

      .= ( SecondTuringTran (t1,t2,(the Tran of t2 . [q, y]))) by A3, A4, Def29

      .= [ [pF, (g `1_3 )], (g `2_3 ), (g `3_3 )] by A1;

    end;

    theorem :: TURING_1:45

    

     Th45: for T1,T2 be TuringStr, s1 be All-State of T1, h be Element of NAT , t be Tape of T1, s2 be All-State of T2, s3 be 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

      let tm1,tm2 be TuringStr, s1 be All-State of tm1, h be Element of NAT , t be Tape of tm1, s2 be All-State of tm2, s3 be All-State of (tm1 ';' tm2);

      set p0 = the InitS of tm1, q0 = the InitS of tm2;

      assume that

       A1: s1 is Accept-Halt and

       A2: s1 = [p0, h, t] and

       A3: s2 is Accept-Halt and

       A4: s2 = [q0, (( Result s1) `2_3 ), (( Result s1) `3_3 )] and

       A5: s3 = [the InitS of (tm1 ';' tm2), h, t];

      set pF = the AcceptS of tm1, qF = the AcceptS of tm2;

      consider k such that

       A6: ((( Computation s1) . k) `1_3 ) = pF and

       A7: ( Result s1) = (( Computation s1) . k) and

       A8: for i be Nat st i < k holds ((( Computation s1) . i) `1_3 ) <> pF by A1, Th13;

      defpred P[ Nat] means $1 <= k implies [((( Computation s1) . $1) `1_3 ), q0] = ((( Computation s3) . $1) `1_3 ) & ((( Computation s1) . $1) `2_3 ) = ((( Computation s3) . $1) `2_3 ) & ((( Computation s1) . $1) `3_3 ) = ((( Computation s3) . $1) `3_3 );

      

       A9: for i st P[i] holds P[(i + 1)]

      proof

        let i;

        assume

         A10: P[i];

        now

          set s1i1 = (( Computation s1) . (i + 1)), s1i = (( Computation s1) . i), s3i1 = (( Computation s3) . (i + 1)), s3i = (( Computation s3) . i);

          

           A11: i < (i + 1) by XREAL_1: 29;

          set f = ( TRAN s3i);

          reconsider h = ( Head s1i) as Element of INT ;

          reconsider ss1 = (s1i `3_3 ) as Tape of tm1;

          reconsider y = (ss1 . h) as Symbol of tm1;

          reconsider ss3 = (s3i `3_3 ) as Tape of (tm1 ';' tm2);

          set p = (s1i `1_3 ), g = ( TRAN s1i);

          assume

           A12: (i + 1) <= k;

          then

           A13: i < k by A11, XXREAL_0: 2;

          then

           A14: p <> pF by A8;

          

           A15: (s3i `1_3 ) <> the AcceptS of (tm1 ';' tm2)

          proof

            assume (s3i `1_3 ) = the AcceptS of (tm1 ';' tm2);

            then [p, q0] = [pF, qF] by A10, A12, A11, Def31, XXREAL_0: 2;

            hence contradiction by A14, XTUPLE_0: 1;

          end;

          

           A16: f = (the Tran of (tm1 ';' tm2) . [ [p, q0], y]) by A10, A12, A11, XXREAL_0: 2

          .= [ [(g `1_3 ), q0], (g `2_3 ), (g `3_3 )] by A8, A13, Th43;

          then

           A17: (g `2_3 ) = (f `2_3 );

          

           A18: s3i1 = ( Following s3i) by Def7

          .= [(f `1_3 ), (( Head s3i) + ( offset f)), ( Tape-Chg (ss3,( Head s3i),(f `2_3 )))] by A15, Def6;

          

           A19: s1i1 = ( Following s1i) by Def7

          .= [(g `1_3 ), (h + ( offset g)), ( Tape-Chg (ss1,h,(g `2_3 )))] by A14, Def6;

          

          hence [(s1i1 `1_3 ), q0] = [(g `1_3 ), q0]

          .= (f `1_3 ) by A16

          .= (s3i1 `1_3 ) by A18;

          ( offset g) = ( offset f) by A16;

          

          hence (s1i1 `2_3 ) = (( Head s3i) + ( offset f)) by A10, A12, A11, A19, XXREAL_0: 2

          .= (s3i1 `2_3 ) by A18;

          

          thus (s1i1 `3_3 ) = (ss3 +* (h .--> (g `2_3 ))) by A10, A12, A11, A19, XXREAL_0: 2

          .= (s3i1 `3_3 ) by A10, A12, A11, A17, A18, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      set s1k = (( Computation s1) . k), s3k = (( Computation s3) . k);

      

       A20: s3 = [ [p0, q0], h, t] by A5, Def31;

      

       A21: P[ 0 ]

      proof

        assume 0 <= k;

        

         A22: ((( Computation s3) . 0 ) `1_3 ) = (s3 `1_3 ) by Def7

        .= [p0, q0] by A20;

        ((( Computation s1) . 0 ) `1_3 ) = (s1 `1_3 ) by Def7

        .= p0 by A2;

        hence [((( Computation s1) . 0 ) `1_3 ), q0] = ((( Computation s3) . 0 ) `1_3 ) by A22;

        

        thus ((( Computation s1) . 0 ) `2_3 ) = (s1 `2_3 ) by Def7

        .= h by A2

        .= (s3 `2_3 ) by A5

        .= ((( Computation s3) . 0 ) `2_3 ) by Def7;

        

        thus ((( Computation s1) . 0 ) `3_3 ) = (s1 `3_3 ) by Def7

        .= t by A2

        .= (s3 `3_3 ) by A5

        .= ((( Computation s3) . 0 ) `3_3 ) by Def7;

      end;

      

       A23: for i holds P[i] from NAT_1:sch 2( A21, A9);

      then

       A24: (s1k `2_3 ) = (s3k `2_3 );

      consider m be Nat such that

       A25: ((( Computation s2) . m) `1_3 ) = qF and

       A26: ( Result s2) = (( Computation s2) . m) and

       A27: for i be Nat st i < m holds ((( Computation s2) . i) `1_3 ) <> qF by A3, Th13;

      defpred Q[ Nat] means $1 <= m implies [pF, ((( Computation s2) . $1) `1_3 )] = ((( Computation s3k) . $1) `1_3 ) & ((( Computation s2) . $1) `2_3 ) = ((( Computation s3k) . $1) `2_3 ) & ((( Computation s2) . $1) `3_3 ) = ((( Computation s3k) . $1) `3_3 );

      

       A28: for i st Q[i] holds Q[(i + 1)]

      proof

        let i;

        assume

         A29: Q[i];

        now

          set s2i1 = (( Computation s2) . (i + 1)), s2i = (( Computation s2) . i), ski1 = (( Computation s3k) . (i + 1)), ski = (( Computation s3k) . i);

          

           A30: i < (i + 1) by XREAL_1: 29;

          reconsider ssk = (ski `3_3 ) as Tape of (tm1 ';' tm2);

          set f = ( TRAN ski);

          set q = (s2i `1_3 ), g = ( TRAN s2i);

          reconsider h = ( Head s2i) as Element of INT ;

          reconsider ss2 = (s2i `3_3 ) as Tape of tm2;

          reconsider y = (ss2 . h) as Symbol of tm2;

          assume

           A31: (i + 1) <= m;

          

          then

           A32: f = (the Tran of (tm1 ';' tm2) . [ [pF, q], y]) by A29, A30, XXREAL_0: 2

          .= [ [pF, (g `1_3 )], (g `2_3 ), (g `3_3 )] by Th44;

          then

           A33: (g `2_3 ) = (f `2_3 );

          i < m by A31, A30, XXREAL_0: 2;

          then

           A34: q <> qF by A27;

          

           A35: (ski `1_3 ) <> the AcceptS of (tm1 ';' tm2)

          proof

            assume (ski `1_3 ) = the AcceptS of (tm1 ';' tm2);

            then [pF, q] = [pF, qF] by A29, A31, A30, Def31, XXREAL_0: 2;

            hence contradiction by A34, XTUPLE_0: 1;

          end;

          

           A36: ski1 = ( Following ski) by Def7

          .= [(f `1_3 ), (( Head ski) + ( offset f)), ( Tape-Chg (ssk,( Head ski),(f `2_3 )))] by A35, Def6;

          

           A37: s2i1 = ( Following s2i) by Def7

          .= [(g `1_3 ), (h + ( offset g)), ( Tape-Chg (ss2,h,(g `2_3 )))] by A34, Def6;

          

          hence [pF, (s2i1 `1_3 )] = [pF, (g `1_3 )]

          .= (f `1_3 ) by A32

          .= (ski1 `1_3 ) by A36;

          ( offset g) = ( offset f) by A32;

          

          hence (s2i1 `2_3 ) = (( Head ski) + ( offset f)) by A29, A31, A30, A37, XXREAL_0: 2

          .= (ski1 `2_3 ) by A36;

          

          thus (s2i1 `3_3 ) = (ssk +* (h .--> (g `2_3 ))) by A29, A31, A30, A37, XXREAL_0: 2

          .= (ski1 `3_3 ) by A29, A31, A30, A33, A36, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      

       A38: (s1k `3_3 ) = (s3k `3_3 ) by A23;

      set s2m = (( Computation s2) . m), skm = (( Computation s3k) . m);

      

       A39: (( Computation s3) . (k + m)) = skm by Th10;

      

       A40: [(s1k `1_3 ), q0] = (s3k `1_3 ) by A23;

      

       A41: Q[ 0 ]

      proof

        assume 0 <= m;

        

        thus [pF, ((( Computation s2) . 0 ) `1_3 )] = [pF, (s2 `1_3 )] by Def7

        .= [pF, q0] by A4

        .= ((( Computation s3k) . 0 ) `1_3 ) by A6, A40, Def7;

        

        thus ((( Computation s2) . 0 ) `2_3 ) = (s2 `2_3 ) by Def7

        .= (s3k `2_3 ) by A4, A7, A24

        .= ((( Computation s3k) . 0 ) `2_3 ) by Def7;

        

        thus ((( Computation s2) . 0 ) `3_3 ) = (s2 `3_3 ) by Def7

        .= (s3k `3_3 ) by A4, A7, A38

        .= ((( Computation s3k) . 0 ) `3_3 ) by Def7;

      end;

      

       A42: for i holds Q[i] from NAT_1:sch 2( A41, A28);

      then [pF, (s2m `1_3 )] = (skm `1_3 );

      then

       A43: ((( Computation s3) . (k + m)) `1_3 ) = the AcceptS of (tm1 ';' tm2) by A25, A39, Def31;

      hence

       A44: s3 is Accept-Halt;

      (s2m `2_3 ) = (skm `2_3 ) & (s2m `3_3 ) = (skm `3_3 ) by A42;

      hence thesis by A26, A39, A43, A44, Def9;

    end;

    theorem :: TURING_1:46

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

    proof

      let tm1,tm2 be TuringStr, t be Tape of tm1;

      set S1 = the Symbols of tm1, S2 = the Symbols of tm2;

      assume

       A1: S1 = S2;

      the Symbols of (tm1 ';' tm2) = (S1 \/ S2) by Def31

      .= S1 by A1;

      hence thesis;

    end;

    theorem :: TURING_1:47

    for tm1,tm2 be TuringStr, t be 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

      let tm1,tm2 be TuringStr, t be Tape of (tm1 ';' tm2);

      set S1 = the Symbols of tm1, S2 = the Symbols of tm2;

      assume

       A1: S1 = S2;

      the Symbols of (tm1 ';' tm2) = (S1 \/ S2) by Def31

      .= S1 by A1;

      hence thesis by A1;

    end;

    theorem :: TURING_1:48

    

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

    proof

      let f be FinSequence of NAT , tm1,tm2 be TuringStr, t1 be Tape of tm1, t2 be Tape of tm2;

      assume that

       A1: t1 = t2 and

       A2: t1 storeData f;

      now

        let i be Nat;

        set m = (( Sum ( Prefix (f,i))) + (2 * (i - 1))), n = (( Sum ( Prefix (f,(i + 1)))) + (2 * i));

        assume 1 <= i & i < ( len f);

        then

         A3: t1 is_1_between (m,n) by A2;

        then

         A4: for k be Integer st m < k & k < n holds (t1 . k) = 1;

        (t1 . m) = 0 & (t1 . n) = 0 by A3;

        hence t2 is_1_between (m,n) by A1, A4;

      end;

      hence thesis;

    end;

    

     Lm15: for s be All-State of ZeroTuring , t be Tape of ZeroTuring , head,n be 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

      let s be All-State of ZeroTuring , t be Tape of ZeroTuring , h,n be Element of NAT ;

      ( len <*n*>) = 1 by FINSEQ_1: 39;

      hence thesis by Th34;

    end;

    theorem :: TURING_1:49

    for s be All-State of ( ZeroTuring ';' SuccTuring ), t be Tape of ZeroTuring , head,n be 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

      let s be All-State of ( ZeroTuring ';' SuccTuring ), t be Tape of ZeroTuring , h,n be Element of NAT ;

      assume that

       A1: s = [ [ 0 , 0 ], h, t] and

       A2: t storeData <*h, n*>;

      reconsider h1 = h as Element of INT by INT_1:def 2;

      set s1 = [the InitS of ZeroTuring , h1, t];

      

       A3: 0 = the InitS of ZeroTuring by Def19;

      then

       A4: s1 is Accept-Halt & (( Result s1) `2_3 ) = h by A2, Lm15;

      the Symbols of ZeroTuring = { 0 , 1} by Def19

      .= the Symbols of SuccTuring by Def17;

      then

      reconsider t2 = (( Result s1) `3_3 ) as Tape of SuccTuring ;

      set s2 = [the InitS of SuccTuring , h1, t2];

      

       A5: 0 = the InitS of SuccTuring by Def17;

      then

       A6: s = [the InitS of ( ZeroTuring ';' SuccTuring ), h, t] by A1, A3, Def31;

      (( Result s1) `3_3 ) storeData <*h, 0 *> by A2, A3, Lm15;

      then

       A7: t2 storeData <*h, 0 *> by Th48;

      then

       A8: (( Result s2) `3_3 ) storeData <*h, ( 0 + 1)*> by A5, Th31;

      

       A9: s2 is Accept-Halt by A7, A5, Th31;

      hence s is Accept-Halt by A4, A6, Th45;

      (( Result s2) `2_3 ) = h by A7, A5, Th31;

      hence (( Result s) `2_3 ) = h by A4, A9, A6, Th45;

      (( Result s) `3_3 ) = (( Result s2) `3_3 ) by A4, A9, A6, Th45;

      hence thesis by A8, Th48;

    end;