let P be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA holds
( (IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(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 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),P,s)) . (fsloc 0) = ((s . (fsloc 0)) +* ((abs (s . (intloc (2 + 1)))),((s . (fsloc 0)) /. (abs ((s . (intloc (2 + 1))) - 1))))) +* ((abs ((s . (intloc (2 + 1))) - 1)),((s . (fsloc 0)) /. (abs (s . (intloc (2 + 1)))))) )
let s be State of SCM+FSA; ( (IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(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 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),P,s)) . (fsloc 0) = ((s . (fsloc 0)) +* ((abs (s . (intloc (2 + 1)))),((s . (fsloc 0)) /. (abs ((s . (intloc (2 + 1))) - 1))))) +* ((abs ((s . (intloc (2 + 1))) - 1)),((s . (fsloc 0)) /. (abs (s . (intloc (2 + 1)))))) )
set s0 = Initialized s;
set s1 = Exec (((intloc (1 + 1)) := (intloc (2 + 1))),(Initialized s));
set s2 = IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))),P,s);
set s3 = IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))),P,s);
set s4 = IExec ((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))),P,s);
set s5 = IExec (((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))),P,s);
set s6 = IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(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))),(Initialized s))) . (intloc 0) =
(Initialized s) . (intloc 0)
by SCMFSA_2:63
.=
1
by SCMFSA6A:38
;
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)),(intloc 0)))),P,s)) . (intloc (1 + 1)) =
(Exec ((SubFrom ((intloc (2 + 1)),(intloc 0))),(Exec (((intloc (1 + 1)) := (intloc (2 + 1))),(Initialized s))))) . (intloc (1 + 1))
by SCMFSA6C:8
.=
(Exec (((intloc (1 + 1)) := (intloc (2 + 1))),(Initialized s))) . (intloc (1 + 1))
by A4, SCMFSA_2:65
.=
(Initialized s) . (intloc (2 + 1))
by SCMFSA_2:63
.=
s . (intloc (2 + 1))
by SCMFSA6C:3
;
A8: (IExec ((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))),P,s)) . (intloc (1 + 1)) =
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1)))),(IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))),P,s)))) . (intloc (1 + 1))
by SCMFSA6C:6
.=
(IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))),P,s)) . (intloc (1 + 1))
by A3, SCMFSA_2:72
.=
(Exec (((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))),(IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))),P,s)))) . (intloc (1 + 1))
by SCMFSA6C:6
.=
s . (intloc (2 + 1))
by A6, A7, SCMFSA_2:72
;
A9:
intloc (4 + 1) <> intloc (2 + 1)
by SCMFSA_2:101;
A10: (IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))),P,s)) . (intloc (2 + 1)) =
(Exec (((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))),(IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))),P,s)))) . (intloc (2 + 1))
by SCMFSA6C:6
.=
(IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))),P,s)) . (intloc (2 + 1))
by A9, SCMFSA_2:72
.=
(Exec ((SubFrom ((intloc (2 + 1)),(intloc 0))),(Exec (((intloc (1 + 1)) := (intloc (2 + 1))),(Initialized s))))) . (intloc (2 + 1))
by SCMFSA6C:8
.=
((Exec (((intloc (1 + 1)) := (intloc (2 + 1))),(Initialized s))) . (intloc (2 + 1))) - ((Exec (((intloc (1 + 1)) := (intloc (2 + 1))),(Initialized s))) . (intloc 0))
by SCMFSA_2:65
.=
((Initialized s) . (intloc (2 + 1))) - ((Exec (((intloc (1 + 1)) := (intloc (2 + 1))),(Initialized s))) . (intloc 0))
by A4, SCMFSA_2:63
.=
(s . (intloc (2 + 1))) - 1
by A2, SCMFSA6C:3
;
A11: (IExec (((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))),P,s)) . (intloc (2 + 1)) =
(Exec ((((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1))),(IExec ((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))),P,s)))) . (intloc (2 + 1))
by SCMFSA6C:6
.=
(IExec ((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))),P,s)) . (intloc (2 + 1))
by SCMFSA_2:73
.=
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1)))),(IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))),P,s)))) . (intloc (2 + 1))
by SCMFSA6C:6
.=
(s . (intloc (2 + 1))) - 1
by A1, A10, SCMFSA_2:72
;
thus (IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),P,s)) . (intloc (2 + 1)) =
(Exec ((((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1))),(IExec (((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))),P,s)))) . (intloc (2 + 1))
by SCMFSA6C:6
.=
(s . (intloc (2 + 1))) - 1
by A11, SCMFSA_2:73
; (IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),P,s)) . (fsloc 0) = ((s . (fsloc 0)) +* ((abs (s . (intloc (2 + 1)))),((s . (fsloc 0)) /. (abs ((s . (intloc (2 + 1))) - 1))))) +* ((abs ((s . (intloc (2 + 1))) - 1)),((s . (fsloc 0)) /. (abs (s . (intloc (2 + 1))))))
A12: (IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))),P,s)) . (fsloc 0) =
(Exec ((SubFrom ((intloc (2 + 1)),(intloc 0))),(Exec (((intloc (1 + 1)) := (intloc (2 + 1))),(Initialized s))))) . (fsloc 0)
by SCMFSA6C:9
.=
(Exec (((intloc (1 + 1)) := (intloc (2 + 1))),(Initialized s))) . (fsloc 0)
by SCMFSA_2:65
.=
(Initialized s) . (fsloc 0)
by SCMFSA_2:63
.=
s . (fsloc 0)
by SCMFSA6C:3
;
A13: (IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))),P,s)) . (fsloc 0) =
(Exec (((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))),(IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))),P,s)))) . (fsloc 0)
by SCMFSA6C:7
.=
s . (fsloc 0)
by A12, SCMFSA_2:72
;
A14: (IExec ((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))),P,s)) . (fsloc 0) =
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1)))),(IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))),P,s)))) . (fsloc 0)
by SCMFSA6C:7
.=
s . (fsloc 0)
by A13, SCMFSA_2:72
;
A15: (IExec ((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))),P,s)) . (intloc (5 + 1)) =
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1)))),(IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))),P,s)))) . (intloc (5 + 1))
by SCMFSA6C:6
.=
(s . (fsloc 0)) /. (abs ((s . (intloc (2 + 1))) - 1))
by A10, A13, SCMBSORT:2
;
A16: (IExec (((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))),P,s)) . (fsloc 0) =
(Exec ((((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1))),(IExec ((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))),P,s)))) . (fsloc 0)
by SCMFSA6C:7
.=
(s . (fsloc 0)) +* ((abs (s . (intloc (2 + 1)))),((s . (fsloc 0)) /. (abs ((s . (intloc (2 + 1))) - 1))))
by A14, A8, A15, SCMBSORT:3
;
A17: (IExec (((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))),P,s)) . (intloc (4 + 1)) =
(Exec ((((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1))),(IExec ((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))),P,s)))) . (intloc (4 + 1))
by SCMFSA6C:6
.=
(IExec ((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))),P,s)) . (intloc (4 + 1))
by SCMFSA_2:73
.=
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1)))),(IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))),P,s)))) . (intloc (4 + 1))
by SCMFSA6C:6
.=
(IExec (((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))),P,s)) . (intloc (4 + 1))
by A5, SCMFSA_2:72
.=
(Exec (((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))),(IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))),P,s)))) . (intloc (4 + 1))
by SCMFSA6C:6
.=
(s . (fsloc 0)) /. (abs (s . (intloc (2 + 1))))
by A12, A7, SCMBSORT:2
;
thus (IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),P,s)) . (fsloc 0) =
(Exec ((((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1))),(IExec (((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))),P,s)))) . (fsloc 0)
by SCMFSA6C:7
.=
((s . (fsloc 0)) +* ((abs (s . (intloc (2 + 1)))),((s . (fsloc 0)) /. (abs ((s . (intloc (2 + 1))) - 1))))) +* ((abs ((s . (intloc (2 + 1))) - 1)),((s . (fsloc 0)) /. (abs (s . (intloc (2 + 1))))))
by A11, A17, A16, SCMBSORT:3
; verum