let i, k be Nat; :: thesis: for T being TuringStr
for s being All-State of T holds (Computation s) . (i + k) = (Computation ((Computation s) . i)) . k
let T be TuringStr ; :: thesis: for s being All-State of T holds (Computation s) . (i + k) = (Computation ((Computation s) . i)) . k
let s be All-State of T; :: thesis: (Computation s) . (i + k) = (Computation ((Computation s) . i)) . k
defpred S₁[ Nat] means (Computation s) . (i + $1) = (Computation ((Computation s) . i)) . $1;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: (Computation s) . (i + k) = (Computation ((Computation s) . i)) . k ; :: thesis: S₁[k + 1]
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 ; :: thesis: verum

end;

A3: S₁[ 0 ] by Def7;
for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A1);
hence (Computation s) . (i + k) = (Computation ((Computation s) . i)) . k ; :: thesis: verum