reconsider F = 0 as Symbol of U3(n)Turing by Lm12;
let s be All-State of U3(n)Turing; :: thesis: for t being Tape of U3(n)Turing
for head being Element of NAT
for f being FinSequence of NAT st len f >= 3 & s = [0,head,t] & t storeData <*head*> ^ f holds
( s is Accept-Halt & (Result s) `2_3 = ((head + (f /. 1)) + (f /. 2)) + 4 & (Result s) `3_3 storeData <*(((head + (f /. 1)) + (f /. 2)) + 4),(f /. 3)*> )
let t be Tape of U3(n)Turing; :: thesis: for head being Element of NAT
for f being FinSequence of NAT st len f >= 3 & s = [0,head,t] & t storeData <*head*> ^ f holds
( s is Accept-Halt & (Result s) `2_3 = ((head + (f /. 1)) + (f /. 2)) + 4 & (Result s) `3_3 storeData <*(((head + (f /. 1)) + (f /. 2)) + 4),(f /. 3)*> )
let h be Element of NAT ; :: thesis: for f being FinSequence of NAT st len f >= 3 & s = [0,h,t] & t storeData <*h*> ^ f holds
( s is Accept-Halt & (Result s) `2_3 = ((h + (f /. 1)) + (f /. 2)) + 4 & (Result s) `3_3 storeData <*(((h + (f /. 1)) + (f /. 2)) + 4),(f /. 3)*> )
let f be FinSequence of NAT ; :: thesis: ( len f >= 3 & s = [0,h,t] & t storeData <*h*> ^ f implies ( s is Accept-Halt & (Result s) `2_3 = ((h + (f /. 1)) + (f /. 2)) + 4 & (Result s) `3_3 storeData <*(((h + (f /. 1)) + (f /. 2)) + 4),(f /. 3)*> ) )
assume that
A1: len f >= 3 and
A2: s = [0,h,t] and
A3: t storeData <*h*> ^ f ; :: thesis: ( s is Accept-Halt & (Result s) `2_3 = ((h + (f /. 1)) + (f /. 2)) + 4 & (Result s) `3_3 storeData <*(((h + (f /. 1)) + (f /. 2)) + 4),(f /. 3)*> )
set n1 = (h + (f /. 1)) + 2;
set n2 = ((h + (f /. 1)) + (f /. 2)) + 4;
set 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,(h + (f /. 1)) + 2 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 (h + (f /. 1)) + 2,((h + (f /. 1)) + (f /. 2)) + 4 by A1, A3, Th23;
then A9: t . (((h + (f /. 1)) + (f /. 2)) + 4) = 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
.= [p1,h1,t] by A2, A7 ;
A11: t is_1_between ((h + (f /. 1)) + (f /. 2)) + 4,(((h + (f /. 1)) + (f /. 2)) + (f /. 3)) + 6 by A1, A3, Th23;
then A12: t . ((((h + (f /. 1)) + (f /. 2)) + (f /. 3)) + 6) = 0 ;
reconsider p2 = 2 as State of U3(n)Turing by Lm11;
set s2 = (Computation [p1,h1,t]) . ((f /. 1) + 1);
reconsider s23 = ((Computation [p1,h1,t]) . ((f /. 1) + 1)) `3_3 as Tape of U3(n)Turing ;
set j1 = ((h + 1) + ((f /. 1) + 1)) + 1;
reconsider k1 = ((h + 1) + ((f /. 1) + 1)) + 1 as Element of INT by INT_1:def 2;
set m2 = (f /. 2) + 1;
set Rs = (Computation s) . ((((((f /. 2) + 1) + 1) + 1) + ((f /. 1) + 1)) + 1);
set m3 = ((((h + (f /. 1)) + (f /. 2)) + 4) + (f /. 3)) + 2;

A13: now :: thesis: for i being Integer st h + 1 <= i & i < (h + 1) + ((f /. 1) + 1) holds
t . i = 1

let i be Integer; :: thesis: ( h + 1 <= i & i < (h + 1) + ((f /. 1) + 1) implies t . i = 1 )
assume that
A14: h + 1 <= i and
A15: i < (h + 1) + ((f /. 1) + 1) ; :: thesis: t . i = 1
h < h + 1 by XREAL_1:29;
then h < i by A14, XXREAL_0:2;
hence t . i = 1 by A4, A15; :: thesis: verum

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 being Tape of U3(n)Turing such that
A16: (Computation [p1,h1,t]) . ((f /. 1) + 1) = [p1,((h + 1) + ((f /. 1) + 1)),t1] and
for i being Integer st h + 1 <= i & i < (h + 1) + ((f /. 1) + 1) holds
t1 . i = 0 and
A17: for i being Integer st ( h + 1 > i or i >= (h + 1) + ((f /. 1) + 1) ) holds
t1 . i = t . i by A13, Lm12, Lm14;
t . ((h + (f /. 1)) + 2) = 0 by A4;
then A18: t1 . ((h + 1) + ((f /. 1) + 1)) = 0 by A17;
A19: TRAN ((Computation [p1,h1,t]) . ((f /. 1) + 1)) = U3(n)Tran . [(((Computation [p1,h1,t]) . ((f /. 1) + 1)) `1_3),(s23 . (Head ((Computation [p1,h1,t]) . ((f /. 1) + 1))))] by Def21
.= U3(n)Tran . [p1,(s23 . (Head ((Computation [p1,h1,t]) . ((f /. 1) + 1))))] by A16
.= U3(n)Tran . [1,(t1 . (Head ((Computation [p1,h1,t]) . ((f /. 1) + 1))))] by A16
.= [2,0,1] by A16, A18, Th36 ;
then A20: offset (TRAN ((Computation [p1,h1,t]) . ((f /. 1) + 1))) = 1 ;
set s3 = [p2,k1,t1];
Tape-Chg ((((Computation [p1,h1,t]) . ((f /. 1) + 1)) `3_3),(Head ((Computation [p1,h1,t]) . ((f /. 1) + 1))),((TRAN ((Computation [p1,h1,t]) . ((f /. 1) + 1))) `2_3)) = Tape-Chg (t1,(Head ((Computation [p1,h1,t]) . ((f /. 1) + 1))),((TRAN ((Computation [p1,h1,t]) . ((f /. 1) + 1))) `2_3)) by A16
.= Tape-Chg (t1,((h + 1) + ((f /. 1) + 1)),((TRAN ((Computation [p1,h1,t]) . ((f /. 1) + 1))) `2_3)) by A16
.= Tape-Chg (t1,((h + 1) + ((f /. 1) + 1)),F) by A19
.= t1 by A18, Th24 ;
then A21: Following ((Computation [p1,h1,t]) . ((f /. 1) + 1)) = [((TRAN ((Computation [p1,h1,t]) . ((f /. 1) + 1))) `1_3),((Head ((Computation [p1,h1,t]) . ((f /. 1) + 1))) + (offset (TRAN ((Computation [p1,h1,t]) . ((f /. 1) + 1))))),t1] by A16, Lm13
.= [2,((Head ((Computation [p1,h1,t]) . ((f /. 1) + 1))) + (offset (TRAN ((Computation [p1,h1,t]) . ((f /. 1) + 1))))),t1] by A19
.= [p2,k1,t1] by A16, A20 ;

A22: now :: thesis: for i being Integer st ((h + 1) + ((f /. 1) + 1)) + 1 <= i & i < (((h + 1) + ((f /. 1) + 1)) + 1) + ((f /. 2) + 1) holds
t1 . i = 1

let i be Integer; :: thesis: ( ((h + 1) + ((f /. 1) + 1)) + 1 <= i & i < (((h + 1) + ((f /. 1) + 1)) + 1) + ((f /. 2) + 1) implies t1 . i = 1 )
assume that
A23: ((h + 1) + ((f /. 1) + 1)) + 1 <= i and
A24: i < (((h + 1) + ((f /. 1) + 1)) + 1) + ((f /. 2) + 1) ; :: thesis: t1 . i = 1
(h + 1) + ((f /. 1) + 1) < ((h + 1) + ((f /. 1) + 1)) + 1 by XREAL_1:29;
then A25: (h + 1) + ((f /. 1) + 1) < i by A23, XXREAL_0:2;
hence t1 . i = t . i by A17
.= 1 by A8, A24, A25 ;
:: thesis: verum

end;

set s4 = (Computation [p2,k1,t1]) . ((f /. 2) + 1);
reconsider s43 = ((Computation [p2,k1,t1]) . ((f /. 2) + 1)) `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 being Tape of U3(n)Turing such that
A26: (Computation [p2,k1,t1]) . ((f /. 2) + 1) = [p2,((((h + 1) + ((f /. 1) + 1)) + 1) + ((f /. 2) + 1)),t2] and
for i being Integer st ((h + 1) + ((f /. 1) + 1)) + 1 <= i & i < (((h + 1) + ((f /. 1) + 1)) + 1) + ((f /. 2) + 1) holds
t2 . i = 0 and
A27: for i being Integer st ( ((h + 1) + ((f /. 1) + 1)) + 1 > i or i >= (((h + 1) + ((f /. 1) + 1)) + 1) + ((f /. 2) + 1) ) holds
t2 . i = t1 . i by A22, Lm12, Lm14;
2 <= (f /. 2) + 4 by NAT_1:12;
then A28: (h + (f /. 1)) + 2 <= (h + (f /. 1)) + ((f /. 2) + 4) by XREAL_1:7;

A29: now :: thesis: for k being Integer st ((h + (f /. 1)) + (f /. 2)) + 4 < k & k < ((((h + (f /. 1)) + (f /. 2)) + 4) + (f /. 3)) + 2 holds
t2 . k = 1

let k be Integer; :: thesis: ( ((h + (f /. 1)) + (f /. 2)) + 4 < k & k < ((((h + (f /. 1)) + (f /. 2)) + 4) + (f /. 3)) + 2 implies t2 . k = 1 )
assume that
A30: ((h + (f /. 1)) + (f /. 2)) + 4 < k and
A31: k < ((((h + (f /. 1)) + (f /. 2)) + 4) + (f /. 3)) + 2 ; :: thesis: t2 . k = 1
A32: (h + (f /. 1)) + 2 <= 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 ; :: thesis: verum

end;

A33: t2 . ((((h + 1) + ((f /. 1) + 1)) + 1) + ((f /. 2) + 1)) = t1 . ((((h + 1) + ((f /. 1) + 1)) + 1) + ((f /. 2) + 1)) by A27
.= 0 by A9, A17, A28 ;
A34: TRAN ((Computation [p2,k1,t1]) . ((f /. 2) + 1)) = U3(n)Tran . [(((Computation [p2,k1,t1]) . ((f /. 2) + 1)) `1_3),(s43 . (Head ((Computation [p2,k1,t1]) . ((f /. 2) + 1))))] by Def21
.= U3(n)Tran . [p2,(s43 . (Head ((Computation [p2,k1,t1]) . ((f /. 2) + 1))))] by A26
.= U3(n)Tran . [2,(t2 . (Head ((Computation [p2,k1,t1]) . ((f /. 2) + 1))))] by A26
.= [3,0,0] by A26, A33, Th36 ;
then A35: offset (TRAN ((Computation [p2,k1,t1]) . ((f /. 2) + 1))) = 0 ;
Tape-Chg ((((Computation [p2,k1,t1]) . ((f /. 2) + 1)) `3_3),(Head ((Computation [p2,k1,t1]) . ((f /. 2) + 1))),((TRAN ((Computation [p2,k1,t1]) . ((f /. 2) + 1))) `2_3)) = Tape-Chg (t2,(Head ((Computation [p2,k1,t1]) . ((f /. 2) + 1))),((TRAN ((Computation [p2,k1,t1]) . ((f /. 2) + 1))) `2_3)) by A26
.= Tape-Chg (t2,((((h + 1) + ((f /. 1) + 1)) + 1) + ((f /. 2) + 1)),((TRAN ((Computation [p2,k1,t1]) . ((f /. 2) + 1))) `2_3)) by A26
.= Tape-Chg (t2,((((h + 1) + ((f /. 1) + 1)) + 1) + ((f /. 2) + 1)),F) by A34
.= t2 by A33, Th24 ;
then A36: Following ((Computation [p2,k1,t1]) . ((f /. 2) + 1)) = [((TRAN ((Computation [p2,k1,t1]) . ((f /. 2) + 1))) `1_3),((Head ((Computation [p2,k1,t1]) . ((f /. 2) + 1))) + (offset (TRAN ((Computation [p2,k1,t1]) . ((f /. 2) + 1))))),t2] by A26, Lm13
.= [3,((Head ((Computation [p2,k1,t1]) . ((f /. 2) + 1))) + (offset (TRAN ((Computation [p2,k1,t1]) . ((f /. 2) + 1))))),t2] by A34
.= [3,(((((h + 1) + ((f /. 1) + 1)) + 1) + ((f /. 2) + 1)) + 0),t2] by A26, A35 ;
(Computation s) . ((((((f /. 2) + 1) + 1) + 1) + ((f /. 1) + 1)) + 1) = (Computation ((Computation s) . 1)) . (((((f /. 2) + 1) + 1) + 1) + ((f /. 1) + 1)) by Th10
.= (Computation [p1,h1,t]) . (((((f /. 2) + 1) + 1) + 1) + ((f /. 1) + 1)) by A10, Th9
.= (Computation ((Computation [p1,h1,t]) . ((f /. 1) + 1))) . ((((f /. 2) + 1) + 1) + 1) by Th10 ;
then A37: (Computation s) . ((((((f /. 2) + 1) + 1) + 1) + ((f /. 1) + 1)) + 1) = (Computation ((Computation ((Computation [p1,h1,t]) . ((f /. 1) + 1))) . 1)) . (((f /. 2) + 1) + 1) by Th10
.= (Computation [p2,k1,t1]) . (((f /. 2) + 1) + 1) by A21, Th9
.= [3,((((h + 1) + ((f /. 1) + 1)) + 1) + ((f /. 2) + 1)),t2] by A36, Def7 ;
then A38: ((Computation s) . ((((((f /. 2) + 1) + 1) + 1) + ((f /. 1) + 1)) + 1)) `1_3 = 3
.= the AcceptS of U3(n)Turing by Def21 ;
hence s is Accept-Halt ; :: thesis: ( (Result s) `2_3 = ((h + (f /. 1)) + (f /. 2)) + 4 & (Result s) `3_3 storeData <*(((h + (f /. 1)) + (f /. 2)) + 4),(f /. 3)*> )
then A39: Result s = (Computation s) . ((((((f /. 2) + 1) + 1) + 1) + ((f /. 1) + 1)) + 1) by A38, Def9;
hence (Result s) `2_3 = ((h + (f /. 1)) + (f /. 2)) + 4 by A37; :: thesis: (Result s) `3_3 storeData <*(((h + (f /. 1)) + (f /. 2)) + 4),(f /. 3)*>
A40: (Result s) `3_3 = t2 by A37, A39;
A41: ((h + (f /. 1)) + (f /. 2)) + 4 <= (((h + (f /. 1)) + (f /. 2)) + 4) + ((f /. 3) + 2) by NAT_1:11;
then A42: (h + (f /. 1)) + 2 <= ((((h + (f /. 1)) + (f /. 2)) + 4) + (f /. 3)) + 2 by A28, XXREAL_0:2;
t2 . (((((h + (f /. 1)) + (f /. 2)) + 4) + (f /. 3)) + 2) = t1 . (((((h + (f /. 1)) + (f /. 2)) + 4) + (f /. 3)) + 2) by A27, A41
.= 0 by A12, A17, A42 ;
then t2 is_1_between ((h + (f /. 1)) + (f /. 2)) + 4,((((h + (f /. 1)) + (f /. 2)) + 4) + (f /. 3)) + 2 by A33, A29;
hence (Result s) `3_3 storeData <*(((h + (f /. 1)) + (f /. 2)) + 4),(f /. 3)*> by A40, Th16; :: thesis: verum