set Ma = Macro (b :=len f);
let s be State of SCM+FSA ; SCMFSA6B:def 4,SCMFSA6C:def 2 ( not (Macro (b :=len f)) +* (Start-At 0 ,SCM+FSA ) c= s or for b1 being Element of NAT holds (Comput (ProgramPart s),s,b1) . (intloc 0 ) = s . (intloc 0 ) )
assume A1:
(Macro (b :=len f)) +* (Start-At 0 ,SCM+FSA ) c= s
; for b1 being Element of NAT holds (Comput (ProgramPart s),s,b1) . (intloc 0 ) = s . (intloc 0 )
then A2:
Macro (b :=len f) c= s
by SCMFSA6B:5;
let k be Element of NAT ; (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 )
dom (Start-At 0 ,SCM+FSA ) = {(IC SCM+FSA )}
by FUNCOP_1:19;
then A3:
IC SCM+FSA in dom (Start-At 0 ,SCM+FSA )
by TARSKI:def 1;
Start-At 0 ,SCM+FSA c= (Macro (b :=len f)) +* (Start-At 0 ,SCM+FSA )
by FUNCT_4:26;
then
Start-At 0 ,SCM+FSA c= s
by A1, XBOOLE_1:1;
then A4: IC s =
(Start-At 0 ,SCM+FSA ) . (IC SCM+FSA )
by A3, GRFUNC_1:8
.=
0
by FUNCOP_1:87
;
0 in dom (Macro (b :=len f))
by SCMFSA6B:32;
then A5:
(Macro (b :=len f)) . 0 = s . 0
by A2, GRFUNC_1:8;
Y:
(ProgramPart s) /. (IC s) = s . (IC s)
by COMPOS_1:38;
Z:
(ProgramPart (Comput (ProgramPart s),s,1)) /. (IC (Comput (ProgramPart s),s,1)) = (Comput (ProgramPart s),s,1) . (IC (Comput (ProgramPart s),s,1))
by COMPOS_1:38;
A6: Comput (ProgramPart s),s,(0 + 1) =
Following (ProgramPart s),(Comput (ProgramPart s),s,0 )
by AMI_1:14
.=
Following (ProgramPart s),s
by AMI_1:13
.=
Exec (b :=len f),s
by A4, A5, Y, SCMFSA6B:33
;
1 in dom (Macro (b :=len f))
by SCMFSA6B:32;
then
(Macro (b :=len f)) . 1 = s . 1
by A2, GRFUNC_1:8;
then A7:
s . 1 = halt SCM+FSA
by SCMFSA6B:33;
IC (Exec (b :=len f),s) =
succ 0
by A4, SCMFSA_2:100
.=
0 + 1
;
then A8:
CurInstr (ProgramPart (Comput (ProgramPart s),s,1)),(Comput (ProgramPart s),s,1) = halt SCM+FSA
by A7, A6, Z, AMI_1:def 13;
T:
ProgramPart s = ProgramPart (Comput (ProgramPart s),s,1)
by AMI_1:123;