let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA holds
( (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (1 + 1)) = (len (s . ())) - (s . (intloc (0 + 1))) & (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (2 + 1)) = ((len (s . ())) - (s . (intloc (0 + 1)))) + 1 & (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . () = s . () & (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (3 + 1)) = 0 & (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (5 + 1)) = (s . ()) /. |.(((len (s . ())) - (s . (intloc (0 + 1)))) + 1).| )

let P be Instruction-Sequence of SCM+FSA; :: thesis: ( (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (1 + 1)) = (len (s . ())) - (s . (intloc (0 + 1))) & (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (2 + 1)) = ((len (s . ())) - (s . (intloc (0 + 1)))) + 1 & (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . () = s . () & (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (3 + 1)) = 0 & (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (5 + 1)) = (s . ()) /. |.(((len (s . ())) - (s . (intloc (0 + 1)))) + 1).| )
set s0 = Initialized s;
set s1 = Exec (((intloc (1 + 1)) :=len ()),());
set s2 = IExec ((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))),P,s);
set s3 = IExec (((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))),P,s);
set s4 = IExec ((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))),P,s);
set s5 = IExec (((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s);
set s6 = IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(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 ()) ";" (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 ()),())))) . (intloc (1 + 1)) by SCMFSA6C:8
.= ((Exec (((intloc (1 + 1)) :=len ()),())) . (intloc (1 + 1))) - ((Exec (((intloc (1 + 1)) :=len ()),())) . (intloc (0 + 1))) by SCMFSA_2:65
.= (len (() . ())) - ((Exec (((intloc (1 + 1)) :=len ()),())) . (intloc (0 + 1))) by SCMFSA_2:74
.= (len (() . ())) - (() . (intloc (0 + 1))) by
.= (len (s . ())) - (() . (intloc (0 + 1))) by SCMFSA_M:37
.= (len (s . ())) - (s . (intloc (0 + 1))) by SCMFSA_M:37 ;
thus (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(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 ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)))) . (intloc (1 + 1)) by SCMFSA6C:6
.= (IExec (((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)) . (intloc (1 + 1)) by
.= (Exec (((intloc (5 + 1)) := ((),(intloc (2 + 1)))),(IExec ((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))),P,s)))) . (intloc (1 + 1)) by SCMFSA6C:6
.= (IExec ((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))),P,s)) . (intloc (1 + 1)) by
.= (Exec ((AddTo ((intloc (2 + 1)),())),(IExec (((((intloc (1 + 1)) :=len ()) ";" (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 ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))),P,s)) . (intloc (1 + 1)) by
.= (Exec (((intloc (2 + 1)) := (intloc (1 + 1))),(IExec ((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))),P,s)))) . (intloc (1 + 1)) by SCMFSA6C:6
.= (len (s . ())) - (s . (intloc (0 + 1))) by ; :: thesis: ( (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (2 + 1)) = ((len (s . ())) - (s . (intloc (0 + 1)))) + 1 & (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . () = s . () & (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (3 + 1)) = 0 & (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (5 + 1)) = (s . ()) /. |.(((len (s . ())) - (s . (intloc (0 + 1)))) + 1).| )
A8: (IExec (((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))),P,s)) . () = 1 by SCMFSA6B:11;
A9: (IExec ((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))),P,s)) . (intloc (2 + 1)) = (Exec ((AddTo ((intloc (2 + 1)),())),(IExec (((((intloc (1 + 1)) :=len ()) ";" (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 ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))),P,s)) . (intloc (2 + 1))) + 1 by
.= ((Exec (((intloc (2 + 1)) := (intloc (1 + 1))),(IExec ((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))),P,s)))) . (intloc (2 + 1))) + 1 by SCMFSA6C:6
.= ((len (s . ())) - (s . (intloc (0 + 1)))) + 1 by ;
thus (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(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 ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)))) . (intloc (2 + 1)) by SCMFSA6C:6
.= (IExec (((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)) . (intloc (2 + 1)) by
.= (Exec (((intloc (5 + 1)) := ((),(intloc (2 + 1)))),(IExec ((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))),P,s)))) . (intloc (2 + 1)) by SCMFSA6C:6
.= ((len (s . ())) - (s . (intloc (0 + 1)))) + 1 by ; :: thesis: ( (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . () = s . () & (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (3 + 1)) = 0 & (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (5 + 1)) = (s . ()) /. |.(((len (s . ())) - (s . (intloc (0 + 1)))) + 1).| )
A10: intloc (5 + 1) <> intloc (3 + 1) by SCMFSA_2:101;
A11: (IExec ((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))),P,s)) . () = (Exec ((AddTo ((intloc (2 + 1)),())),(IExec (((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))),P,s)))) . () by SCMFSA6C:7
.= (IExec (((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))),P,s)) . () by SCMFSA_2:64
.= (Exec (((intloc (2 + 1)) := (intloc (1 + 1))),(IExec ((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))),P,s)))) . () by SCMFSA6C:7
.= (IExec ((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))),P,s)) . () by SCMFSA_2:63
.= (Exec ((SubFrom ((intloc (1 + 1)),(intloc (0 + 1)))),(Exec (((intloc (1 + 1)) :=len ()),())))) . () by SCMFSA6C:9
.= (Exec (((intloc (1 + 1)) :=len ()),())) . () by SCMFSA_2:65
.= () . () by SCMFSA_2:74
.= s . () by SCMFSA_M:37 ;
thus (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . () = (Exec ((SubFrom ((intloc (3 + 1)),(intloc (3 + 1)))),(IExec (((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)))) . () by SCMFSA6C:7
.= (IExec (((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)) . () by SCMFSA_2:65
.= (Exec (((intloc (5 + 1)) := ((),(intloc (2 + 1)))),(IExec ((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))),P,s)))) . () by SCMFSA6C:7
.= s . () by ; :: thesis: ( (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (3 + 1)) = 0 & (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (5 + 1)) = (s . ()) /. |.(((len (s . ())) - (s . (intloc (0 + 1)))) + 1).| )
thus (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(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 ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)))) . (intloc (3 + 1)) by SCMFSA6C:6
.= ((IExec (((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)) . (intloc (3 + 1))) - ((IExec (((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)) . (intloc (3 + 1))) by SCMFSA_2:65
.= 0 ; :: thesis: (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (5 + 1)) = (s . ()) /. |.(((len (s . ())) - (s . (intloc (0 + 1)))) + 1).|
thus (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(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 ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)))) . (intloc (5 + 1)) by SCMFSA6C:6
.= (IExec (((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)) . (intloc (5 + 1)) by
.= (Exec (((intloc (5 + 1)) := ((),(intloc (2 + 1)))),(IExec ((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))),P,s)))) . (intloc (5 + 1)) by SCMFSA6C:6
.= (s . ()) /. |.(((len (s . ())) - (s . (intloc (0 + 1)))) + 1).| by ; :: thesis: verum