let s be State of SCM+FSA ; :: according to SCMFSA6B:def 4,SCMFSA6C:def 2 :: thesis: ( not (Macro (SubFrom 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 A21:
(Macro (SubFrom 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 (SubFrom a,b);
Start-At (insloc 0 ) c= (Macro (SubFrom a,b)) +* (Start-At (insloc 0 ))
by FUNCT_4:26;
then A22:
Start-At (insloc 0 ) c= s
by A21, 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 A23: IC s =
(Start-At (insloc 0 )) . (IC SCM+FSA )
by A22, GRFUNC_1:8
.=
insloc 0
by FUNCOP_1:87
;
A24:
( insloc 0 in dom (Macro (SubFrom a,b)) & insloc 1 in dom (Macro (SubFrom a,b)) )
by SCMFSA6B:32;
Macro (SubFrom a,b) c= s
by A21, SCMFSA6B:5;
then A25:
( (Macro (SubFrom a,b)) . (insloc 0 ) = s . (insloc 0 ) & (Macro (SubFrom a,b)) . (insloc 1) = s . (insloc 1) )
by A24, GRFUNC_1:8;
then A26:
( s . (insloc 0 ) = SubFrom a,b & s . (insloc 1) = halt SCM+FSA )
by SCMFSA6B:33;
A27: IC (Exec (SubFrom a,b),s) =
Next (insloc 0 )
by A23, SCMFSA_2:91
.=
insloc (0 + 1)
;
A28: Computation s,(0 + 1) =
Following (Computation s,0 )
by AMI_1:14
.=
Following s
by AMI_1:13
.=
Exec (SubFrom a,b),s
by A23, A25, SCMFSA6B:33
;
then A29:
CurInstr (Computation s,1) = halt SCM+FSA
by A26, A27, AMI_1:def 13;