set Mi = Macro (halt SCM+FSA);
dom (Macro (halt SCM+FSA)) = {0,1} by COMPOS_1:149;
then A1: 0 in dom (Macro (halt SCM+FSA)) by TARSKI:def 2;
let s be State of SCM+FSA; :: according to SCMFSA6B:def 4 :: thesis: ( Start-At (0,SCM+FSA) c= s implies for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st Macro (halt SCM+FSA) c= P holds
for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) )
assume A2: Start-At (0,SCM+FSA) c= s ; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st Macro (halt SCM+FSA) c= P holds
for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( Macro (halt SCM+FSA) c= P implies for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) )
assume A3: Macro (halt SCM+FSA) c= P ; :: thesis: for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A4: s = Comput (P,s,0) by EXTPRO_1:3;
dom P = NAT by PARTFUN1:def 4;
then A5: P /. (IC s) = P . (IC s) by PARTFUN1:def 8;
CurInstr (P,s) = P . 0 by A2, A5, COMPOS_1:228
.= (Macro (halt SCM+FSA)) . 0 by A1, A3, GRFUNC_1:8
.= halt SCM+FSA by COMPOS_1:148 ;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A4, EXTPRO_1:6; :: thesis: verum