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

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