let T be TuringStr ; :: thesis: for s being All-State of T holds (Computation s) . 1 = Following s

let s be All-State of T; :: thesis: (Computation s) . 1 = Following s

(Computation s) . (0 + 1) = Following ((Computation s) . 0) by Def7

.= Following s by Def7 ;

hence (Computation s) . 1 = Following s ; :: thesis: verum

let s be All-State of T; :: thesis: (Computation s) . 1 = Following s

(Computation s) . (0 + 1) = Following ((Computation s) . 0) by Def7

.= Following s by Def7 ;

hence (Computation s) . 1 = Following s ; :: thesis: verum