set Mi = Macro (halt SCM+FSA);
let s be State of SCM+FSA; :: according to SCMFSA6B:def 4 :: thesis: ( not Start-At (0,SCM+FSA) c= s or for b₁ being set holds
( not Macro (halt SCM+FSA) c= b₁ or for b₂ being Element of NAT holds (Comput (b₁,s,b₂)) . (intloc 0) = s . (intloc 0) ) )
assume A1: Start-At (0,SCM+FSA) c= s ; :: thesis: for b₁ being set holds
( not Macro (halt SCM+FSA) c= b₁ or for b₂ being Element of NAT holds (Comput (b₁,s,b₂)) . (intloc 0) = s . (intloc 0) )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( not Macro (halt SCM+FSA) c= P or for b₁ being Element of NAT holds (Comput (P,s,b₁)) . (intloc 0) = s . (intloc 0) )
assume A2: Macro (halt SCM+FSA) c= P ; :: thesis: for b₁ being Element of NAT holds (Comput (P,s,b₁)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A3: s = Comput (P,s,0) by EXTPRO_1:3;
A4: P /. (IC s) = P . (IC s) by PBOOLE:158;
A5: 0 in dom (Macro (halt SCM+FSA)) by COMPOS_1:147;
Comput (P,s,0) = s by EXTPRO_1:3;
then CurInstr (P,(Comput (P,s,0))) = P . 0 by A1, A4, COMPOS_1:228
.= (Macro (halt SCM+FSA)) . 0 by GRFUNC_1:8, A2, A5
.= halt SCM+FSA by COMPOS_1:148 ;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A3, EXTPRO_1:6, NAT_1:2; :: thesis: verum