let s be State of SCM+FSA ; ( (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (1 + 1)) = (len (s . (fsloc 0 ))) - (s . (intloc (0 + 1))) & (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (2 + 1)) = ((len (s . (fsloc 0 ))) - (s . (intloc (0 + 1)))) + 1 & (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (fsloc 0 ) = s . (fsloc 0 ) & (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (3 + 1)) = 0 & (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (5 + 1)) = (s . (fsloc 0 )) /. (abs (((len (s . (fsloc 0 ))) - (s . (intloc (0 + 1)))) + 1)) )
set s0 = Initialized s;
set s1 = Exec ((intloc (1 + 1)) :=len (fsloc 0 )),(Initialized s);
set s2 = IExec (((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))),s;
set s3 = IExec ((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))),s;
set s4 = IExec (((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))),s;
set s5 = IExec ((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))),s;
set s6 = IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s;
A1:
intloc (3 + 1) <> intloc (2 + 1)
by AMI_3:52;
A2:
intloc (3 + 1) <> intloc (1 + 1)
by AMI_3:52;
A3:
intloc (5 + 1) <> intloc (1 + 1)
by AMI_3:52;
A4:
intloc (5 + 1) <> intloc (2 + 1)
by AMI_3:52;
A5:
intloc (1 + 1) <> intloc (0 + 1)
by AMI_3:52;
A6:
intloc (1 + 1) <> intloc (2 + 1)
by AMI_3:52;
A7: (IExec (((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))),s) . (intloc (1 + 1)) =
(Exec (SubFrom (intloc (1 + 1)),(intloc (0 + 1))),(Exec ((intloc (1 + 1)) :=len (fsloc 0 )),(Initialized s))) . (intloc (1 + 1))
by SCMFSA6C:9
.=
((Exec ((intloc (1 + 1)) :=len (fsloc 0 )),(Initialized s)) . (intloc (1 + 1))) - ((Exec ((intloc (1 + 1)) :=len (fsloc 0 )),(Initialized s)) . (intloc (0 + 1)))
by SCMFSA_2:91
.=
(len ((Initialized s) . (fsloc 0 ))) - ((Exec ((intloc (1 + 1)) :=len (fsloc 0 )),(Initialized s)) . (intloc (0 + 1)))
by SCMFSA_2:100
.=
(len ((Initialized s) . (fsloc 0 ))) - ((Initialized s) . (intloc (0 + 1)))
by A5, SCMFSA_2:100
.=
(len (s . (fsloc 0 ))) - ((Initialized s) . (intloc (0 + 1)))
by SCMFSA6C:3
.=
(len (s . (fsloc 0 ))) - (s . (intloc (0 + 1)))
by SCMFSA6C:3
;
thus (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (1 + 1)) =
(Exec (SubFrom (intloc (3 + 1)),(intloc (3 + 1))),(IExec ((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))),s)) . (intloc (1 + 1))
by SCMFSA6C:7
.=
(IExec ((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))),s) . (intloc (1 + 1))
by A2, SCMFSA_2:91
.=
(Exec ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1))),(IExec (((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))),s)) . (intloc (1 + 1))
by SCMFSA6C:7
.=
(IExec (((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))),s) . (intloc (1 + 1))
by A3, SCMFSA_2:98
.=
(Exec (AddTo (intloc (2 + 1)),(intloc 0 )),(IExec ((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))),s)) . (intloc (1 + 1))
by SCMFSA6C:7
.=
(IExec ((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))),s) . (intloc (1 + 1))
by A6, SCMFSA_2:90
.=
(Exec ((intloc (2 + 1)) := (intloc (1 + 1))),(IExec (((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))),s)) . (intloc (1 + 1))
by SCMFSA6C:7
.=
(len (s . (fsloc 0 ))) - (s . (intloc (0 + 1)))
by A6, A7, SCMFSA_2:89
; ( (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (2 + 1)) = ((len (s . (fsloc 0 ))) - (s . (intloc (0 + 1)))) + 1 & (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (fsloc 0 ) = s . (fsloc 0 ) & (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (3 + 1)) = 0 & (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (5 + 1)) = (s . (fsloc 0 )) /. (abs (((len (s . (fsloc 0 ))) - (s . (intloc (0 + 1)))) + 1)) )
A8:
(IExec ((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))),s) . (intloc 0 ) = 1
by SCMFSA6B:35;
A9: (IExec (((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))),s) . (intloc (2 + 1)) =
(Exec (AddTo (intloc (2 + 1)),(intloc 0 )),(IExec ((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))),s)) . (intloc (2 + 1))
by SCMFSA6C:7
.=
((IExec ((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))),s) . (intloc (2 + 1))) + 1
by A8, SCMFSA_2:90
.=
((Exec ((intloc (2 + 1)) := (intloc (1 + 1))),(IExec (((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))),s)) . (intloc (2 + 1))) + 1
by SCMFSA6C:7
.=
((len (s . (fsloc 0 ))) - (s . (intloc (0 + 1)))) + 1
by A7, SCMFSA_2:89
;
thus (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (2 + 1)) =
(Exec (SubFrom (intloc (3 + 1)),(intloc (3 + 1))),(IExec ((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))),s)) . (intloc (2 + 1))
by SCMFSA6C:7
.=
(IExec ((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))),s) . (intloc (2 + 1))
by A1, SCMFSA_2:91
.=
(Exec ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1))),(IExec (((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))),s)) . (intloc (2 + 1))
by SCMFSA6C:7
.=
((len (s . (fsloc 0 ))) - (s . (intloc (0 + 1)))) + 1
by A4, A9, SCMFSA_2:98
; ( (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (fsloc 0 ) = s . (fsloc 0 ) & (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (3 + 1)) = 0 & (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (5 + 1)) = (s . (fsloc 0 )) /. (abs (((len (s . (fsloc 0 ))) - (s . (intloc (0 + 1)))) + 1)) )
A10:
intloc (5 + 1) <> intloc (3 + 1)
by AMI_3:52;
A11: (IExec (((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))),s) . (fsloc 0 ) =
(Exec (AddTo (intloc (2 + 1)),(intloc 0 )),(IExec ((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))),s)) . (fsloc 0 )
by SCMFSA6C:8
.=
(IExec ((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))),s) . (fsloc 0 )
by SCMFSA_2:90
.=
(Exec ((intloc (2 + 1)) := (intloc (1 + 1))),(IExec (((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))),s)) . (fsloc 0 )
by SCMFSA6C:8
.=
(IExec (((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))),s) . (fsloc 0 )
by SCMFSA_2:89
.=
(Exec (SubFrom (intloc (1 + 1)),(intloc (0 + 1))),(Exec ((intloc (1 + 1)) :=len (fsloc 0 )),(Initialized s))) . (fsloc 0 )
by SCMFSA6C:10
.=
(Exec ((intloc (1 + 1)) :=len (fsloc 0 )),(Initialized s)) . (fsloc 0 )
by SCMFSA_2:91
.=
(Initialized s) . (fsloc 0 )
by SCMFSA_2:100
.=
s . (fsloc 0 )
by SCMFSA6C:3
;
thus (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (fsloc 0 ) =
(Exec (SubFrom (intloc (3 + 1)),(intloc (3 + 1))),(IExec ((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))),s)) . (fsloc 0 )
by SCMFSA6C:8
.=
(IExec ((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))),s) . (fsloc 0 )
by SCMFSA_2:91
.=
(Exec ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1))),(IExec (((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))),s)) . (fsloc 0 )
by SCMFSA6C:8
.=
s . (fsloc 0 )
by A11, SCMFSA_2:98
; ( (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (3 + 1)) = 0 & (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (5 + 1)) = (s . (fsloc 0 )) /. (abs (((len (s . (fsloc 0 ))) - (s . (intloc (0 + 1)))) + 1)) )
thus (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (3 + 1)) =
(Exec (SubFrom (intloc (3 + 1)),(intloc (3 + 1))),(IExec ((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))),s)) . (intloc (3 + 1))
by SCMFSA6C:7
.=
((IExec ((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))),s) . (intloc (3 + 1))) - ((IExec ((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))),s) . (intloc (3 + 1)))
by SCMFSA_2:91
.=
0
; (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (5 + 1)) = (s . (fsloc 0 )) /. (abs (((len (s . (fsloc 0 ))) - (s . (intloc (0 + 1)))) + 1))
thus (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (5 + 1)) =
(Exec (SubFrom (intloc (3 + 1)),(intloc (3 + 1))),(IExec ((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))),s)) . (intloc (5 + 1))
by SCMFSA6C:7
.=
(IExec ((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))),s) . (intloc (5 + 1))
by A10, SCMFSA_2:91
.=
(Exec ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1))),(IExec (((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))),s)) . (intloc (5 + 1))
by SCMFSA6C:7
.=
(s . (fsloc 0 )) /. (abs (((len (s . (fsloc 0 ))) - (s . (intloc (0 + 1)))) + 1))
by A9, A11, SCMBSORT:8
; verum