let s be State of SCM+FSA ; :: according to SCMFSA6B:def 4,SCMFSA6C:def 2 :: thesis: ( not (Macro (MultBy a,b)) +* (Start-At (insloc 0 )) c= s or for b1 being Element of NAT holds (Computation s,b1) . (intloc 0 ) = s . (intloc 0 ) )
assume A31: (Macro (MultBy a,b)) +* (Start-At (insloc 0 )) c= s ; :: thesis: for b1 being Element of NAT holds (Computation s,b1) . (intloc 0 ) = s . (intloc 0 )
let k be Element of NAT ; :: thesis: (Computation s,k) . (intloc 0 ) = s . (intloc 0 )
set Ma = Macro (MultBy a,b);
Start-At (insloc 0 ) c= (Macro (MultBy a,b)) +* (Start-At (insloc 0 )) by FUNCT_4:26;
then A32: Start-At (insloc 0 ) c= s by A31, XBOOLE_1:1;
dom (Start-At (insloc 0 )) = {(IC SCM+FSA )} by FUNCOP_1:19;
then IC SCM+FSA in dom (Start-At (insloc 0 )) by TARSKI:def 1;
then A33: IC s = (Start-At (insloc 0 )) . (IC SCM+FSA ) by A32, GRFUNC_1:8
.= insloc 0 by FUNCOP_1:87 ;
A34: ( insloc 0 in dom (Macro (MultBy a,b)) & insloc 1 in dom (Macro (MultBy a,b)) ) by SCMFSA6B:32;
Macro (MultBy a,b) c= s by A31, SCMFSA6B:5;
then A35: ( (Macro (MultBy a,b)) . (insloc 0 ) = s . (insloc 0 ) & (Macro (MultBy a,b)) . (insloc 1) = s . (insloc 1) ) by A34, GRFUNC_1:8;
then A36: ( s . (insloc 0 ) = MultBy a,b & s . (insloc 1) = halt SCM+FSA ) by SCMFSA6B:33;
A37: IC (Exec (MultBy a,b),s) = Next (insloc 0 ) by A33, SCMFSA_2:92
.= insloc (0 + 1) ;
A38: Computation s,(0 + 1) = Following (Computation s,0 ) by AMI_1:14
.= Following s by AMI_1:13
.= Exec (MultBy a,b),s by A33, A35, SCMFSA6B:33 ;
then A39: CurInstr (Computation s,1) = halt SCM+FSA by A36, A37, AMI_1:def 13;
per cases ( k = 0 or 1 <= k ) by NAT_1:14;
suppose k = 0 ; :: thesis: (Computation s,k) . (intloc 0 ) = s . (intloc 0 )
hence (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) by AMI_1:13; :: thesis: verum
end;
suppose A40: 1 <= k ; :: thesis: (Computation s,k) . (intloc 0 ) = s . (intloc 0 )
(Computation s,1) . (intloc 0 ) = s . (intloc 0 ) by A38, SCMFSA_2:92;
hence (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) by A39, A40, AMI_1:52; :: thesis: verum
end;
end;