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

let s be State of SCM+FSA; :: thesis: ( (IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))),P,s)) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - 1 & (IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))),P,s)) . () = ((s . ()) +* (|.(s . (intloc (2 + 1))).|,((s . ()) /. |.((s . (intloc (2 + 1))) - 1).|))) +* (|.((s . (intloc (2 + 1))) - 1).|,((s . ()) /. |.(s . (intloc (2 + 1))).|)) )
set s0 = Initialized s;
set s1 = Exec (((intloc (1 + 1)) := (intloc (2 + 1))),());
set s2 = IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))),P,s);
set s3 = IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))),P,s);
set s4 = IExec ((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s);
set s5 = IExec (((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))),P,s);
set s6 = IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))),P,s);
A1: intloc (5 + 1) <> intloc (2 + 1) by SCMFSA_2:101;
A2: (Exec (((intloc (1 + 1)) := (intloc (2 + 1))),())) . () = () . () by SCMFSA_2:63
.= 1 by SCMFSA_M:9 ;
A3: intloc (5 + 1) <> intloc (1 + 1) by SCMFSA_2:101;
A4: intloc (1 + 1) <> intloc (2 + 1) by SCMFSA_2:101;
A5: intloc (5 + 1) <> intloc (4 + 1) by SCMFSA_2:101;
A6: intloc (4 + 1) <> intloc (1 + 1) by SCMFSA_2:101;
A7: (IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))),P,s)) . (intloc (1 + 1)) = (Exec ((SubFrom ((intloc (2 + 1)),())),(Exec (((intloc (1 + 1)) := (intloc (2 + 1))),())))) . (intloc (1 + 1)) by SCMFSA6C:8
.= (Exec (((intloc (1 + 1)) := (intloc (2 + 1))),())) . (intloc (1 + 1)) by
.= () . (intloc (2 + 1)) by SCMFSA_2:63
.= s . (intloc (2 + 1)) by SCMFSA_M:37 ;
A8: (IExec ((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)) . (intloc (1 + 1)) = (Exec (((intloc (5 + 1)) := ((),(intloc (2 + 1)))),(IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))),P,s)))) . (intloc (1 + 1)) by SCMFSA6C:6
.= (IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))),P,s)) . (intloc (1 + 1)) by
.= (Exec (((intloc (4 + 1)) := ((),(intloc (1 + 1)))),(IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))),P,s)))) . (intloc (1 + 1)) by SCMFSA6C:6
.= s . (intloc (2 + 1)) by ;
A9: intloc (4 + 1) <> intloc (2 + 1) by SCMFSA_2:101;
A10: (IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))),P,s)) . (intloc (2 + 1)) = (Exec (((intloc (4 + 1)) := ((),(intloc (1 + 1)))),(IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))),P,s)))) . (intloc (2 + 1)) by SCMFSA6C:6
.= (IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))),P,s)) . (intloc (2 + 1)) by
.= (Exec ((SubFrom ((intloc (2 + 1)),())),(Exec (((intloc (1 + 1)) := (intloc (2 + 1))),())))) . (intloc (2 + 1)) by SCMFSA6C:8
.= ((Exec (((intloc (1 + 1)) := (intloc (2 + 1))),())) . (intloc (2 + 1))) - ((Exec (((intloc (1 + 1)) := (intloc (2 + 1))),())) . ()) by SCMFSA_2:65
.= (() . (intloc (2 + 1))) - ((Exec (((intloc (1 + 1)) := (intloc (2 + 1))),())) . ()) by
.= (s . (intloc (2 + 1))) - 1 by ;
A11: (IExec (((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))),P,s)) . (intloc (2 + 1)) = (Exec ((((),(intloc (1 + 1))) := (intloc (5 + 1))),(IExec ((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)))) . (intloc (2 + 1)) by SCMFSA6C:6
.= (IExec ((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)) . (intloc (2 + 1)) by SCMFSA_2:73
.= (Exec (((intloc (5 + 1)) := ((),(intloc (2 + 1)))),(IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))),P,s)))) . (intloc (2 + 1)) by SCMFSA6C:6
.= (s . (intloc (2 + 1))) - 1 by ;
thus (IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))),P,s)) . (intloc (2 + 1)) = (Exec ((((),(intloc (2 + 1))) := (intloc (4 + 1))),(IExec (((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))),P,s)))) . (intloc (2 + 1)) by SCMFSA6C:6
.= (s . (intloc (2 + 1))) - 1 by ; :: thesis: (IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))),P,s)) . () = ((s . ()) +* (|.(s . (intloc (2 + 1))).|,((s . ()) /. |.((s . (intloc (2 + 1))) - 1).|))) +* (|.((s . (intloc (2 + 1))) - 1).|,((s . ()) /. |.(s . (intloc (2 + 1))).|))
A12: (IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))),P,s)) . () = (Exec ((SubFrom ((intloc (2 + 1)),())),(Exec (((intloc (1 + 1)) := (intloc (2 + 1))),())))) . () by SCMFSA6C:9
.= (Exec (((intloc (1 + 1)) := (intloc (2 + 1))),())) . () by SCMFSA_2:65
.= () . () by SCMFSA_2:63
.= s . () by SCMFSA_M:37 ;
A13: (IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))),P,s)) . () = (Exec (((intloc (4 + 1)) := ((),(intloc (1 + 1)))),(IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))),P,s)))) . () by SCMFSA6C:7
.= s . () by ;
A14: (IExec ((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)) . () = (Exec (((intloc (5 + 1)) := ((),(intloc (2 + 1)))),(IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))),P,s)))) . () by SCMFSA6C:7
.= s . () by ;
A15: (IExec ((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)) . (intloc (5 + 1)) = (Exec (((intloc (5 + 1)) := ((),(intloc (2 + 1)))),(IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))),P,s)))) . (intloc (5 + 1)) by SCMFSA6C:6
.= (s . ()) /. |.((s . (intloc (2 + 1))) - 1).| by ;
A16: (IExec (((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))),P,s)) . () = (Exec ((((),(intloc (1 + 1))) := (intloc (5 + 1))),(IExec ((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)))) . () by SCMFSA6C:7
.= (s . ()) +* (|.(s . (intloc (2 + 1))).|,((s . ()) /. |.((s . (intloc (2 + 1))) - 1).|)) by ;
A17: (IExec (((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))),P,s)) . (intloc (4 + 1)) = (Exec ((((),(intloc (1 + 1))) := (intloc (5 + 1))),(IExec ((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)))) . (intloc (4 + 1)) by SCMFSA6C:6
.= (IExec ((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))),P,s)) . (intloc (4 + 1)) by SCMFSA_2:73
.= (Exec (((intloc (5 + 1)) := ((),(intloc (2 + 1)))),(IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))),P,s)))) . (intloc (4 + 1)) by SCMFSA6C:6
.= (IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))),P,s)) . (intloc (4 + 1)) by
.= (Exec (((intloc (4 + 1)) := ((),(intloc (1 + 1)))),(IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))),P,s)))) . (intloc (4 + 1)) by SCMFSA6C:6
.= (s . ()) /. |.(s . (intloc (2 + 1))).| by ;
thus (IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))),P,s)) . () = (Exec ((((),(intloc (2 + 1))) := (intloc (4 + 1))),(IExec (((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))),P,s)))) . () by SCMFSA6C:7
.= ((s . ()) +* (|.(s . (intloc (2 + 1))).|,((s . ()) /. |.((s . (intloc (2 + 1))) - 1).|))) +* (|.((s . (intloc (2 + 1))) - 1).|,((s . ()) /. |.(s . (intloc (2 + 1))).|)) by ; :: thesis: verum