let s be State of SCM+FSA ; :: thesis: ( s . (intloc (1 + 1)) >= 1 & s . (intloc (1 + 1)) <= len (s . (fsloc 0 )) implies ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (2 + 1)) = s . (intloc (2 + 1)) & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (5 + 1)) = s . (intloc (5 + 1)) & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (fsloc 0 ) = s . (fsloc 0 ) & ex x1 being Integer st
( x1 = (s . (fsloc 0 )) . (s . (intloc (1 + 1))) & ( x1 - (s . (intloc (5 + 1))) > 0 implies ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) = 0 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = s . (intloc (3 + 1)) ) ) & ( x1 - (s . (intloc (5 + 1))) <= 0 implies ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) = (s . (intloc (1 + 1))) - 1 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 ) ) ) ) )
assume A1:
( s . (intloc (1 + 1)) >= 1 & s . (intloc (1 + 1)) <= len (s . (fsloc 0 )) )
; :: thesis: ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (2 + 1)) = s . (intloc (2 + 1)) & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (5 + 1)) = s . (intloc (5 + 1)) & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (fsloc 0 ) = s . (fsloc 0 ) & ex x1 being Integer st
( x1 = (s . (fsloc 0 )) . (s . (intloc (1 + 1))) & ( x1 - (s . (intloc (5 + 1))) > 0 implies ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) = 0 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = s . (intloc (3 + 1)) ) ) & ( x1 - (s . (intloc (5 + 1))) <= 0 implies ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) = (s . (intloc (1 + 1))) - 1 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 ) ) ) )
set s0 = Initialize s;
set s1 = Exec ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))),(Initialize s);
set s2 = IExec (((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))),s;
A2:
intloc (3 + 1) <> intloc (2 + 1)
by AMI_3:52;
A3:
intloc (1 + 1) <> intloc (2 + 1)
by AMI_3:52;
A4:
intloc (4 + 1) <> intloc (2 + 1)
by AMI_3:52;
thus (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (2 + 1)) =
(IExec (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))),(IExec (((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))),s)) . (intloc (2 + 1))
by SCM_HALT:30
.=
(IExec (((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))),s) . (intloc (2 + 1))
by A2, A3, Lm15
.=
(Exec (SubFrom (intloc (4 + 1)),(intloc (5 + 1))),(Exec ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))),(Initialize s))) . (intloc (2 + 1))
by SCMFSA6C:9
.=
(Exec ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))),(Initialize s)) . (intloc (2 + 1))
by A4, SCMFSA_2:91
.=
(Initialize s) . (intloc (2 + 1))
by A4, SCMFSA_2:98
.=
s . (intloc (2 + 1))
by SCMFSA6C:3
; :: thesis: ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (5 + 1)) = s . (intloc (5 + 1)) & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (fsloc 0 ) = s . (fsloc 0 ) & ex x1 being Integer st
( x1 = (s . (fsloc 0 )) . (s . (intloc (1 + 1))) & ( x1 - (s . (intloc (5 + 1))) > 0 implies ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) = 0 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = s . (intloc (3 + 1)) ) ) & ( x1 - (s . (intloc (5 + 1))) <= 0 implies ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) = (s . (intloc (1 + 1))) - 1 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 ) ) ) )
A5:
intloc (3 + 1) <> intloc (5 + 1)
by AMI_3:52;
A6:
intloc (1 + 1) <> intloc (5 + 1)
by AMI_3:52;
A7:
intloc (4 + 1) <> intloc (5 + 1)
by AMI_3:52;
then A8: (Exec ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))),(Initialize s)) . (intloc (5 + 1)) =
(Initialize s) . (intloc (5 + 1))
by SCMFSA_2:98
.=
s . (intloc (5 + 1))
by SCMFSA6C:3
;
thus (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (5 + 1)) =
(IExec (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))),(IExec (((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))),s)) . (intloc (5 + 1))
by SCM_HALT:30
.=
(IExec (((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))),s) . (intloc (5 + 1))
by A5, A6, Lm15
.=
(Exec (SubFrom (intloc (4 + 1)),(intloc (5 + 1))),(Exec ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))),(Initialize s))) . (intloc (5 + 1))
by SCMFSA6C:9
.=
s . (intloc (5 + 1))
by A7, A8, SCMFSA_2:91
; :: thesis: ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (fsloc 0 ) = s . (fsloc 0 ) & ex x1 being Integer st
( x1 = (s . (fsloc 0 )) . (s . (intloc (1 + 1))) & ( x1 - (s . (intloc (5 + 1))) > 0 implies ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) = 0 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = s . (intloc (3 + 1)) ) ) & ( x1 - (s . (intloc (5 + 1))) <= 0 implies ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) = (s . (intloc (1 + 1))) - 1 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 ) ) ) )
thus (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (fsloc 0 ) =
(IExec (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))),(IExec (((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))),s)) . (fsloc 0 )
by SCM_HALT:31
.=
(IExec (((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))),s) . (fsloc 0 )
by Lm13
.=
(Exec (SubFrom (intloc (4 + 1)),(intloc (5 + 1))),(Exec ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))),(Initialize s))) . (fsloc 0 )
by SCMFSA6C:10
.=
(Exec ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))),(Initialize s)) . (fsloc 0 )
by SCMFSA_2:91
.=
(Initialize s) . (fsloc 0 )
by SCMFSA_2:98
.=
s . (fsloc 0 )
by SCMFSA6C:3
; :: thesis: ex x1 being Integer st
( x1 = (s . (fsloc 0 )) . (s . (intloc (1 + 1))) & ( x1 - (s . (intloc (5 + 1))) > 0 implies ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) = 0 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = s . (intloc (3 + 1)) ) ) & ( x1 - (s . (intloc (5 + 1))) <= 0 implies ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) = (s . (intloc (1 + 1))) - 1 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 ) ) )
A9:
intloc (4 + 1) <> intloc (1 + 1)
by AMI_3:52;
A10: (IExec (((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))),s) . (intloc (1 + 1)) =
(Exec (SubFrom (intloc (4 + 1)),(intloc (5 + 1))),(Exec ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))),(Initialize s))) . (intloc (1 + 1))
by SCMFSA6C:9
.=
(Exec ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))),(Initialize s)) . (intloc (1 + 1))
by A9, SCMFSA_2:91
.=
(Initialize s) . (intloc (1 + 1))
by A9, SCMFSA_2:98
.=
s . (intloc (1 + 1))
by SCMFSA6C:3
;
A11:
intloc (4 + 1) <> intloc (3 + 1)
by AMI_3:52;
A12: (IExec (((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))),s) . (intloc (3 + 1)) =
(Exec (SubFrom (intloc (4 + 1)),(intloc (5 + 1))),(Exec ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))),(Initialize s))) . (intloc (3 + 1))
by SCMFSA6C:9
.=
(Exec ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))),(Initialize s)) . (intloc (3 + 1))
by A11, SCMFSA_2:91
.=
(Initialize s) . (intloc (3 + 1))
by A11, SCMFSA_2:98
.=
s . (intloc (3 + 1))
by SCMFSA6C:3
;
A13:
abs (s . (intloc (1 + 1))) = s . (intloc (1 + 1))
by A1, ABSVALUE:def 1;
reconsider k1 = s . (intloc (1 + 1)) as Element of NAT by A1, INT_1:16;
reconsider n = (s . (fsloc 0 )) . k1 as Integer ;
A14:
(s . (fsloc 0 )) /. k1 = n
by A1, FINSEQ_4:24;
A15: (Exec ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))),(Initialize s)) . (intloc (4 + 1)) =
((Initialize s) . (fsloc 0 )) /. (abs ((Initialize s) . (intloc (1 + 1))))
by SCMBSORT:8
.=
((Initialize s) . (fsloc 0 )) /. (abs (s . (intloc (1 + 1))))
by SCMFSA6C:3
.=
n
by A13, A14, SCMFSA6C:3
;
A16: (IExec (((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))),s) . (intloc (4 + 1)) =
(Exec (SubFrom (intloc (4 + 1)),(intloc (5 + 1))),(Exec ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))),(Initialize s))) . (intloc (4 + 1))
by SCMFSA6C:9
.=
n - (s . (intloc (5 + 1)))
by A8, A15, SCMFSA_2:91
;
take
n
; :: thesis: ( n = (s . (fsloc 0 )) . (s . (intloc (1 + 1))) & ( n - (s . (intloc (5 + 1))) > 0 implies ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) = 0 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = s . (intloc (3 + 1)) ) ) & ( n - (s . (intloc (5 + 1))) <= 0 implies ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) = (s . (intloc (1 + 1))) - 1 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 ) ) )
thus
n = (s . (fsloc 0 )) . (s . (intloc (1 + 1)))
; :: thesis: ( ( n - (s . (intloc (5 + 1))) > 0 implies ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) = 0 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = s . (intloc (3 + 1)) ) ) & ( n - (s . (intloc (5 + 1))) <= 0 implies ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) = (s . (intloc (1 + 1))) - 1 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 ) ) )
hereby :: thesis: ( n - (s . (intloc (5 + 1))) <= 0 implies ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) = (s . (intloc (1 + 1))) - 1 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 ) )
assume A17:
n - (s . (intloc (5 + 1))) > 0
;
:: thesis: ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) = 0 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = s . (intloc (3 + 1)) )thus (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) =
(IExec (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))),(IExec (((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))),s)) . (intloc (1 + 1))
by SCM_HALT:30
.=
0
by A16, A17, Lm3
;
:: thesis: (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = s . (intloc (3 + 1))thus (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) =
(IExec (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))),(IExec (((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))),s)) . (intloc (3 + 1))
by SCM_HALT:30
.=
s . (intloc (3 + 1))
by A12, A16, A17, Lm14
;
:: thesis: verum
end;
hereby :: thesis: verum
assume A18:
n - (s . (intloc (5 + 1))) <= 0
;
:: thesis: ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) = (s . (intloc (1 + 1))) - 1 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 )thus (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) =
(IExec (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))),(IExec (((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))),s)) . (intloc (1 + 1))
by SCM_HALT:30
.=
(s . (intloc (1 + 1))) - 1
by A10, A16, A18, Lm3
;
:: thesis: (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1thus (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (3 + 1)) =
(IExec (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))),(IExec (((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))),s)) . (intloc (3 + 1))
by SCM_HALT:30
.=
(s . (intloc (3 + 1))) + 1
by A12, A16, A18, Lm14
;
:: thesis: verum
end;