set Ma = Macro (AddTo (a,b));
let s be State of SCM+FSA; :: according to SCMFSA6B:def 4,SCMFSA6C:def 2 :: thesis: ( not Start-At (0,SCM+FSA) c= s or for b₁ being set holds
( not Macro (AddTo (a,b)) c= b₁ or for b₂ being Element of NAT holds (Comput (b₁,s,b₂)) . (intloc 0) = s . (intloc 0) ) )
assume A11: Start-At (0,SCM+FSA) c= s ; :: thesis: for b₁ being set holds
( not Macro (AddTo (a,b)) 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 (AddTo (a,b)) c= P or for b₁ being Element of NAT holds (Comput (P,s,b₁)) . (intloc 0) = s . (intloc 0) )
assume A12: Macro (AddTo (a,b)) 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)
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:19;
then A13: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
A14: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A13, GRFUNC_1:8, A11
.= 0 by FUNCOP_1:87 ;
0 in dom (Macro (AddTo (a,b))) by COMPOS_1:147;
then A15: (Macro (AddTo (a,b))) . 0 = P . 0 by A12, GRFUNC_1:8;
A16: P /. (IC s) = P . (IC s) by PBOOLE:158;
A17: Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:4
.= Following (P,s) by EXTPRO_1:3
.= Exec ((AddTo (a,b)),s) by A14, A15, A16, COMPOS_1:148 ;
1 in dom (Macro (AddTo (a,b))) by COMPOS_1:147;
then (Macro (AddTo (a,b))) . 1 = P . 1 by A12, GRFUNC_1:8;
then A18: P . 1 = halt SCM+FSA by COMPOS_1:148;
IC (Exec ((AddTo (a,b)),s)) = succ 0 by A14, SCMFSA_2:90
.= 0 + 1 ;
then A19: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A18, A17, PBOOLE:158;

per cases ( k = 0 or 1 <= k ) by NAT_1:14;

suppose k = 0 ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)

hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by EXTPRO_1:3; :: thesis: verum

end;

suppose A20: 1 <= k ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)

(Comput (P,s,1)) . (intloc 0) = s . (intloc 0) by A17, SCMFSA_2:90;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A19, A20, EXTPRO_1:6; :: thesis: verum

end;

end;