let s be State of SCM+FSA; :: thesis: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being InitHalting Program of SCM+FSA st Initialized I c= s & I c= p holds
p halts_on s
let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being InitHalting Program of SCM+FSA st Initialized I c= s & I c= p holds
p halts_on s
let I be InitHalting Program of SCM+FSA; :: thesis: ( Initialized I c= s & I c= p implies p halts_on s )
assume A1: Initialized I c= s ; :: thesis: ( not I c= p or p halts_on s )
assume A2: I c= p ; :: thesis: p halts_on s
A3: ProgramPart (Initialized I) = I by SCMFSA6A:33;
Initialized I is halting by Def2;
hence p halts_on s by A1, EXTPRO_1:def 10, A2, A3; :: thesis: verum