let s be State of SCM+FSA; :: thesis: for I being parahalting Program of SCM+FSA st Initialized I c= s holds
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P holds
P halts_on s
let I be parahalting Program of SCM+FSA; :: thesis: ( Initialized I c= s implies for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P holds
P halts_on s )
A1: Initialize I is halting by Def3;
Initialized I = Initialize (I +* ((intloc 0) .--> 1)) by FUNCT_4:15;
then ( Start-At (0,SCM+FSA) c= Initialized I & I c= Initialized I ) by FUNCT_4:26, SCMFSA6A:26;
then ( Initialize I c= I \/ (Start-At (0,SCM+FSA)) & I \/ (Start-At (0,SCM+FSA)) c= Initialized I ) by FUNCT_4:30, XBOOLE_1:8;
then A2: Initialize I c= Initialized I by XBOOLE_1:1;
assume A3: Initialized I c= s ; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P holds
P halts_on s
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( I c= P implies P halts_on s )
assume A4: I c= P ; :: thesis: P halts_on s
A5: Initialize I c= s by A2, XBOOLE_1:1, A3;
ProgramPart (Initialize I) = I by COMPOS_1:144;
hence P halts_on s by A1, EXTPRO_1:def 10, A5, A4; :: thesis: verum