let i, j be Nat; :: thesis: for T being TuringStr
for s being All-State of T st i <= j & ((Computation s) . i) `1_3 = the AcceptS of T holds
(Computation s) . j = (Computation s) . i
let T be TuringStr ; :: thesis: for s being All-State of T st i <= j & ((Computation s) . i) `1_3 = the AcceptS of T holds
(Computation s) . j = (Computation s) . i
let s be All-State of T; :: thesis: ( i <= j & ((Computation s) . i) `1_3 = the AcceptS of T implies (Computation s) . j = (Computation s) . i )
assume that
A1: i <= j and
A2: ((Computation s) . i) `1_3 = the AcceptS of T ; :: thesis: (Computation s) . j = (Computation s) . i
Following ((Computation s) . i) = (Computation s) . i by A2, Def6;
hence (Computation s) . j = (Computation s) . i by A1, Th11; :: thesis: verum