let s be State of SCM+FSA ; :: thesis: ( (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)))),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)))),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 = Initialize s;
set s1 = Exec ((intloc (1 + 1)) := (intloc (2 + 1))),(Initialize s);
set s2 = IExec (((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))),s;
set s3 = IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))),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)))),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)))),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)))),s;
A1: intloc (5 + 1) <> intloc (2 + 1) by AMI_3:52;
A2: intloc (4 + 1) <> intloc (2 + 1) by AMI_3:52;
A3: intloc (1 + 1) <> intloc (2 + 1) by AMI_3:52;
A4: (Exec ((intloc (1 + 1)) := (intloc (2 + 1))),(Initialize s)) . (intloc 0 ) = (Initialize s) . (intloc 0 ) by SCMFSA_2:89
.= 1 by SCMFSA6C:3 ;
A5: (IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))),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 ))),s)) . (intloc (2 + 1)) by SCMFSA6C:7
.= (IExec (((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))),s) . (intloc (2 + 1)) by A2, SCMFSA_2:98
.= (Exec (SubFrom (intloc (2 + 1)),(intloc 0 )),(Exec ((intloc (1 + 1)) := (intloc (2 + 1))),(Initialize s))) . (intloc (2 + 1)) by SCMFSA6C:9
.= ((Exec ((intloc (1 + 1)) := (intloc (2 + 1))),(Initialize s)) . (intloc (2 + 1))) - ((Exec ((intloc (1 + 1)) := (intloc (2 + 1))),(Initialize s)) . (intloc 0 )) by SCMFSA_2:91
.= ((Initialize s) . (intloc (2 + 1))) - ((Exec ((intloc (1 + 1)) := (intloc (2 + 1))),(Initialize s)) . (intloc 0 )) by A3, SCMFSA_2:89
.= (s . (intloc (2 + 1))) - 1 by A4, SCMFSA6C:3 ;
A6: (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)))),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)))),s)) . (intloc (2 + 1)) by SCMFSA6C:7
.= (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)))),s) . (intloc (2 + 1)) by SCMFSA_2:99
.= (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)))),s)) . (intloc (2 + 1)) by SCMFSA6C:7
.= (s . (intloc (2 + 1))) - 1 by A1, A5, SCMFSA_2:98 ;
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)))),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)))),s)) . (intloc (2 + 1)) by SCMFSA6C:7
.= (s . (intloc (2 + 1))) - 1 by A6, SCMFSA_2:99 ; :: thesis: (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)))),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)))))
A7: (IExec (((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))),s) . (fsloc 0 ) = (Exec (SubFrom (intloc (2 + 1)),(intloc 0 )),(Exec ((intloc (1 + 1)) := (intloc (2 + 1))),(Initialize s))) . (fsloc 0 ) by SCMFSA6C:10
.= (Exec ((intloc (1 + 1)) := (intloc (2 + 1))),(Initialize s)) . (fsloc 0 ) by SCMFSA_2:91
.= (Initialize s) . (fsloc 0 ) by SCMFSA_2:89
.= s . (fsloc 0 ) 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)))),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 ))),s)) . (fsloc 0 ) by SCMFSA6C:8
.= s . (fsloc 0 ) by A7, SCMFSA_2:98 ;
A9: (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)))),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)))),s)) . (fsloc 0 ) by SCMFSA6C:8
.= s . (fsloc 0 ) by A8, SCMFSA_2:98 ;
A10: intloc (5 + 1) <> intloc (1 + 1) by AMI_3:52;
A11: intloc (4 + 1) <> intloc (1 + 1) by AMI_3:52;
A12: (IExec (((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))),s) . (intloc (1 + 1)) = (Exec (SubFrom (intloc (2 + 1)),(intloc 0 )),(Exec ((intloc (1 + 1)) := (intloc (2 + 1))),(Initialize s))) . (intloc (1 + 1)) by SCMFSA6C:9
.= (Exec ((intloc (1 + 1)) := (intloc (2 + 1))),(Initialize s)) . (intloc (1 + 1)) by A3, SCMFSA_2:91
.= (Initialize s) . (intloc (2 + 1)) by SCMFSA_2:89
.= s . (intloc (2 + 1)) 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)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))),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)))),s)) . (intloc (1 + 1)) by SCMFSA6C:7
.= (IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))),s) . (intloc (1 + 1)) by A10, SCMFSA_2:98
.= (Exec ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))),(IExec (((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))),s)) . (intloc (1 + 1)) by SCMFSA6C:7
.= s . (intloc (2 + 1)) by A11, A12, SCMFSA_2:98 ;
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)))),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)))),s)) . (intloc (5 + 1)) by SCMFSA6C:7
.= (s . (fsloc 0 )) /. (abs ((s . (intloc (2 + 1))) - 1)) by A5, A8, SCMBSORT:8 ;
A15: intloc (5 + 1) <> intloc (4 + 1) by AMI_3:52;
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)))),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)))),s)) . (intloc (4 + 1)) by SCMFSA6C:7
.= (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)))),s) . (intloc (4 + 1)) by SCMFSA_2:99
.= (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)))),s)) . (intloc (4 + 1)) by SCMFSA6C:7
.= (IExec ((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))),s) . (intloc (4 + 1)) by A15, SCMFSA_2:98
.= (Exec ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))),(IExec (((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))),s)) . (intloc (4 + 1)) by SCMFSA6C:7
.= (s . (fsloc 0 )) /. (abs (s . (intloc (2 + 1)))) by A7, A12, SCMBSORT:8 ;
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)))),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)))),s)) . (fsloc 0 ) by SCMFSA6C:8
.= (s . (fsloc 0 )) +* (abs (s . (intloc (2 + 1)))),((s . (fsloc 0 )) /. (abs ((s . (intloc (2 + 1))) - 1))) by A9, A13, A14, SCMBSORT:9 ;
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)))),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)))),s)) . (fsloc 0 ) by SCMFSA6C:8
.= ((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 A6, A16, A17, SCMBSORT:9 ; :: thesis: verum