let i be Instruction of SCM+FSA ; :: thesis: ( (Macro i) . (insloc 0 ) = i & (Macro i) . (insloc 1) = halt SCM+FSA & (Initialized (Macro i)) . (insloc 0 ) = i & (Initialized (Macro i)) . (insloc 1) = halt SCM+FSA & ((Macro i) +* (Start-At (insloc 0 ))) . (insloc 0 ) = i )
thus A1: (Macro i) . (insloc 0 ) = i by FUNCT_4:66; :: thesis: ( (Macro i) . (insloc 1) = halt SCM+FSA & (Initialized (Macro i)) . (insloc 0 ) = i & (Initialized (Macro i)) . (insloc 1) = halt SCM+FSA & ((Macro i) +* (Start-At (insloc 0 ))) . (insloc 0 ) = i )
thus A2: (Macro i) . (insloc 1) = halt SCM+FSA by FUNCT_4:66; :: thesis: ( (Initialized (Macro i)) . (insloc 0 ) = i & (Initialized (Macro i)) . (insloc 1) = halt SCM+FSA & ((Macro i) +* (Start-At (insloc 0 ))) . (insloc 0 ) = i )
A3: ( insloc 0 in dom (Macro i) & insloc 1 in dom (Macro i) ) by Th32;
A4: Macro i c= Initialized (Macro i) by SCMFSA6A:26;
hence (Initialized (Macro i)) . (insloc 0 ) = i by A1, A3, GRFUNC_1:8; :: thesis: ( (Initialized (Macro i)) . (insloc 1) = halt SCM+FSA & ((Macro i) +* (Start-At (insloc 0 ))) . (insloc 0 ) = i )
thus (Initialized (Macro i)) . (insloc 1) = halt SCM+FSA by A2, A3, A4, GRFUNC_1:8; :: thesis: ((Macro i) +* (Start-At (insloc 0 ))) . (insloc 0 ) = i
dom (Macro i) misses dom (Start-At (insloc 0 )) by SF_MASTR:64;
then Macro i c= (Macro i) +* (Start-At (insloc 0 )) by FUNCT_4:33;
hence ((Macro i) +* (Start-At (insloc 0 ))) . (insloc 0 ) = i by A1, A3, GRFUNC_1:8; :: thesis: verum