let s be State of SCM+FSA; for P being Instruction-Sequence of SCM+FSA holds
( (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))))),P,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))))),P,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))))),P,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))))),P,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))))),P,s)) . (intloc (5 + 1)) = (s . (fsloc 0)) /. |.(((len (s . (fsloc 0))) - (s . (intloc (0 + 1)))) + 1).| )
let P be Instruction-Sequence 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))))),P,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))))),P,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))))),P,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))))),P,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))))),P,s)) . (intloc (5 + 1)) = (s . (fsloc 0)) /. |.(((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))))),P,s);
set s3 = IExec (((((intloc (1 + 1)) :=len (fsloc 0)) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))),P,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)))),P,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))))),P,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))))),P,s);
A1:
intloc (3 + 1) <> intloc (2 + 1)
by SCMFSA_2:101;
A2:
intloc (3 + 1) <> intloc (1 + 1)
by SCMFSA_2:101;
A3:
intloc (5 + 1) <> intloc (1 + 1)
by SCMFSA_2:101;
A4:
intloc (5 + 1) <> intloc (2 + 1)
by SCMFSA_2:101;
A5:
intloc (1 + 1) <> intloc (0 + 1)
by SCMFSA_2:101;
A6:
intloc (1 + 1) <> intloc (2 + 1)
by SCMFSA_2:101;
A7: (IExec ((((intloc (1 + 1)) :=len (fsloc 0)) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))),P,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:8
.=
((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:65
.=
(len ((Initialized s) . (fsloc 0))) - ((Exec (((intloc (1 + 1)) :=len (fsloc 0)),(Initialized s))) . (intloc (0 + 1)))
by SCMFSA_2:74
.=
(len ((Initialized s) . (fsloc 0))) - ((Initialized s) . (intloc (0 + 1)))
by A5, SCMFSA_2:74
.=
(len (s . (fsloc 0))) - ((Initialized s) . (intloc (0 + 1)))
by SCMFSA_M:37
.=
(len (s . (fsloc 0))) - (s . (intloc (0 + 1)))
by SCMFSA_M:37
;
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))))),P,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))))),P,s)))) . (intloc (1 + 1))
by SCMFSA6C:6
.=
(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))))),P,s)) . (intloc (1 + 1))
by A2, SCMFSA_2:65
.=
(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)))),P,s)))) . (intloc (1 + 1))
by SCMFSA6C:6
.=
(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)))),P,s)) . (intloc (1 + 1))
by A3, SCMFSA_2:72
.=
(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)))),P,s)))) . (intloc (1 + 1))
by SCMFSA6C:6
.=
(IExec (((((intloc (1 + 1)) :=len (fsloc 0)) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))),P,s)) . (intloc (1 + 1))
by A6, SCMFSA_2:64
.=
(Exec (((intloc (2 + 1)) := (intloc (1 + 1))),(IExec ((((intloc (1 + 1)) :=len (fsloc 0)) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))),P,s)))) . (intloc (1 + 1))
by SCMFSA6C:6
.=
(len (s . (fsloc 0))) - (s . (intloc (0 + 1)))
by A6, A7, SCMFSA_2:63
; ( (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))))),P,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))))),P,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))))),P,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))))),P,s)) . (intloc (5 + 1)) = (s . (fsloc 0)) /. |.(((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)))),P,s)) . (intloc 0) = 1
by SCMFSA6B:11;
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)))),P,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)))),P,s)))) . (intloc (2 + 1))
by SCMFSA6C:6
.=
((IExec (((((intloc (1 + 1)) :=len (fsloc 0)) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))),P,s)) . (intloc (2 + 1))) + 1
by A8, SCMFSA_2:64
.=
((Exec (((intloc (2 + 1)) := (intloc (1 + 1))),(IExec ((((intloc (1 + 1)) :=len (fsloc 0)) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))),P,s)))) . (intloc (2 + 1))) + 1
by SCMFSA6C:6
.=
((len (s . (fsloc 0))) - (s . (intloc (0 + 1)))) + 1
by A7, SCMFSA_2:63
;
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))))),P,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))))),P,s)))) . (intloc (2 + 1))
by SCMFSA6C:6
.=
(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))))),P,s)) . (intloc (2 + 1))
by A1, SCMFSA_2:65
.=
(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)))),P,s)))) . (intloc (2 + 1))
by SCMFSA6C:6
.=
((len (s . (fsloc 0))) - (s . (intloc (0 + 1)))) + 1
by A4, A9, SCMFSA_2:72
; ( (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))))),P,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))))),P,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))))),P,s)) . (intloc (5 + 1)) = (s . (fsloc 0)) /. |.(((len (s . (fsloc 0))) - (s . (intloc (0 + 1)))) + 1).| )
A10:
intloc (5 + 1) <> intloc (3 + 1)
by SCMFSA_2:101;
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)))),P,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)))),P,s)))) . (fsloc 0)
by SCMFSA6C:7
.=
(IExec (((((intloc (1 + 1)) :=len (fsloc 0)) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))),P,s)) . (fsloc 0)
by SCMFSA_2:64
.=
(Exec (((intloc (2 + 1)) := (intloc (1 + 1))),(IExec ((((intloc (1 + 1)) :=len (fsloc 0)) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))),P,s)))) . (fsloc 0)
by SCMFSA6C:7
.=
(IExec ((((intloc (1 + 1)) :=len (fsloc 0)) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))),P,s)) . (fsloc 0)
by SCMFSA_2:63
.=
(Exec ((SubFrom ((intloc (1 + 1)),(intloc (0 + 1)))),(Exec (((intloc (1 + 1)) :=len (fsloc 0)),(Initialized s))))) . (fsloc 0)
by SCMFSA6C:9
.=
(Exec (((intloc (1 + 1)) :=len (fsloc 0)),(Initialized s))) . (fsloc 0)
by SCMFSA_2:65
.=
(Initialized s) . (fsloc 0)
by SCMFSA_2:74
.=
s . (fsloc 0)
by SCMFSA_M:37
;
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))))),P,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))))),P,s)))) . (fsloc 0)
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))))),P,s)) . (fsloc 0)
by SCMFSA_2:65
.=
(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)))),P,s)))) . (fsloc 0)
by SCMFSA6C:7
.=
s . (fsloc 0)
by A11, SCMFSA_2:72
; ( (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))))),P,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))))),P,s)) . (intloc (5 + 1)) = (s . (fsloc 0)) /. |.(((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))))),P,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))))),P,s)))) . (intloc (3 + 1))
by SCMFSA6C:6
.=
((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))))),P,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))))),P,s)) . (intloc (3 + 1)))
by SCMFSA_2:65
.=
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))))),P,s)) . (intloc (5 + 1)) = (s . (fsloc 0)) /. |.(((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))))),P,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))))),P,s)))) . (intloc (5 + 1))
by SCMFSA6C:6
.=
(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))))),P,s)) . (intloc (5 + 1))
by A10, SCMFSA_2:65
.=
(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)))),P,s)))) . (intloc (5 + 1))
by SCMFSA6C:6
.=
(s . (fsloc 0)) /. |.(((len (s . (fsloc 0))) - (s . (intloc (0 + 1)))) + 1).|
by A9, A11, SCMBSORT:2
; verum