let i, j be Nat; :: thesis: for T being TuringStr

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

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

let T be TuringStr ; :: thesis: for s being All-State of T st i <= j & Following ((Computation s) . i) = (Computation s) . i holds

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

let s be All-State of T; :: thesis: ( i <= j & Following ((Computation s) . i) = (Computation s) . i implies (Computation s) . j = (Computation s) . i )

assume that

A1: i <= j and

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

consider k being Nat such that

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

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

A4: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

A7: for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A6, A4);

thus (Computation s) . j = (Computation s) . i by A3, A7; :: thesis: verum

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

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

let T be TuringStr ; :: thesis: for s being All-State of T st i <= j & Following ((Computation s) . i) = (Computation s) . i holds

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

let s be All-State of T; :: thesis: ( i <= j & Following ((Computation s) . i) = (Computation s) . i implies (Computation s) . j = (Computation s) . i )

assume that

A1: i <= j and

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

consider k being Nat such that

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

defpred S

A4: for k being Nat st S

S

proof

A6:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A5: (Computation s) . (i + k) = (Computation s) . i ; :: thesis: S_{1}[k + 1]

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

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

end;assume A5: (Computation s) . (i + k) = (Computation s) . i ; :: thesis: S

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

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

A7: for k being Nat holds S

thus (Computation s) . j = (Computation s) . i by A3, A7; :: thesis: verum