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₁[ Nat] means (Computation s) . (i + $1) = (Computation s) . i;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: (Computation s) . (i + k) = (Computation s) . i ; :: thesis: S₁[k + 1]
thus (Computation s) . (i + (k + 1)) = (Computation s) . ((i + k) + 1)
.= (Computation s) . i by A2, A5, Def7 ; :: thesis: verum

end;

A6: S₁[ 0 ] ;
A7: for k being Nat holds S₁[k] from NAT_1:sch 2(A6, A4);
thus (Computation s) . j = (Computation s) . i by A3, A7; :: thesis: verum