let p be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA st s . (intloc (2 + 1)) <= len (s . (fsloc 0)) & s . (intloc (2 + 1)) >= 2 holds
( (IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - 1 & s . (fsloc 0),(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0) are_fiberwise_equipotent & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) ) & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( for k being set st k <> (s . (intloc (2 + 1))) - 1 & k <> s . (intloc (2 + 1)) & k in dom (s . (fsloc 0)) holds
(s . (fsloc 0)) . k = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k ) & ex x1, x2 being Integer st
( x1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & x1 >= x2 ) )
let s be State of SCM+FSA; ( s . (intloc (2 + 1)) <= len (s . (fsloc 0)) & s . (intloc (2 + 1)) >= 2 implies ( (IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - 1 & s . (fsloc 0),(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0) are_fiberwise_equipotent & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) ) & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( for k being set st k <> (s . (intloc (2 + 1))) - 1 & k <> s . (intloc (2 + 1)) & k in dom (s . (fsloc 0)) holds
(s . (fsloc 0)) . k = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k ) & ex x1, x2 being Integer st
( x1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & x1 >= x2 ) ) )
assume that
A1:
s . (intloc (2 + 1)) <= len (s . (fsloc 0))
and
A2:
s . (intloc (2 + 1)) >= 2
; ( (IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - 1 & s . (fsloc 0),(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0) are_fiberwise_equipotent & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) ) & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( for k being set st k <> (s . (intloc (2 + 1))) - 1 & k <> s . (intloc (2 + 1)) & k in dom (s . (fsloc 0)) holds
(s . (fsloc 0)) . k = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k ) & ex x1, x2 being Integer st
( x1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & x1 >= x2 ) )
A3:
(s . (intloc (2 + 1))) - 1 >= 2 - 1
by A2, XREAL_1:9;
then A4:
|.((s . (intloc (2 + 1))) - 1).| = (s . (intloc (2 + 1))) - 1
by ABSVALUE:def 1;
A5:
(s . (intloc (2 + 1))) - 1 <= len (s . (fsloc 0))
by A1, XREAL_1:146, XXREAL_0:2;
A6:
s . (intloc (2 + 1)) >= 1
by A2, XXREAL_0:2;
A7:
|.(s . (intloc (2 + 1))).| = s . (intloc (2 + 1))
by A2, ABSVALUE:def 1;
reconsider k1 = (s . (intloc (2 + 1))) - 1 as Element of NAT by A3, INT_1:3;
reconsider k2 = s . (intloc (2 + 1)) as Element of NAT by A2, INT_1:3;
A8:
k1 in dom (s . (fsloc 0))
by A3, A5, FINSEQ_3:25;
reconsider n1 = (s . (fsloc 0)) . k1 as Integer ;
A9:
k2 in dom (s . (fsloc 0))
by A1, A6, FINSEQ_3:25;
reconsider n2 = (s . (fsloc 0)) . k2 as Integer ;
set s0 = Initialized s;
set s1 = Exec (((intloc (3 + 1)) := (intloc (2 + 1))),(Initialized s));
set s2 = IExec ((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))),p,s);
set s3 = IExec (((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))),p,s);
set s4 = IExec ((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))),p,s);
set s5 = IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))),p,s);
set s6 = IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s);
A10: (Exec (((intloc (3 + 1)) := (intloc (2 + 1))),(Initialized s))) . (intloc (3 + 1)) =
(Initialized s) . (intloc (2 + 1))
by SCMFSA_2:63
.=
s . (intloc (2 + 1))
by SCMFSA_M:37
;
A11: (Exec (((intloc (3 + 1)) := (intloc (2 + 1))),(Initialized s))) . (fsloc 0) =
(Initialized s) . (fsloc 0)
by SCMFSA_2:63
.=
s . (fsloc 0)
by SCMFSA_M:37
;
A12:
(Exec (((intloc (3 + 1)) := (intloc (2 + 1))),(Initialized s))) . (intloc (2 + 1)) = s . (intloc (2 + 1))
by Th4;
A13: (Exec (((intloc (3 + 1)) := (intloc (2 + 1))),(Initialized s))) . (intloc 0) =
(Initialized s) . (intloc 0)
by SCMFSA_2:63
.=
1
by SCMFSA_M:9
;
A14: (IExec ((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))),p,s)) . (fsloc 0) =
(Exec ((SubFrom ((intloc (2 + 1)),(intloc 0))),(Exec (((intloc (3 + 1)) := (intloc (2 + 1))),(Initialized s))))) . (fsloc 0)
by SCMFSA6C:9
.=
s . (fsloc 0)
by A11, SCMFSA_2:65
;
A15: (IExec ((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))),p,s)) . (intloc (2 + 1)) =
(Exec ((SubFrom ((intloc (2 + 1)),(intloc 0))),(Exec (((intloc (3 + 1)) := (intloc (2 + 1))),(Initialized s))))) . (intloc (2 + 1))
by SCMFSA6C:8
.=
(s . (intloc (2 + 1))) - 1
by A12, A13, SCMFSA_2:65
;
A16: (IExec ((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))),p,s)) . (intloc (3 + 1)) =
(Exec ((SubFrom ((intloc (2 + 1)),(intloc 0))),(Exec (((intloc (3 + 1)) := (intloc (2 + 1))),(Initialized s))))) . (intloc (3 + 1))
by SCMFSA6C:8
.=
s . (intloc (2 + 1))
by A10, Lm14, SCMFSA_2:65
;
A17: (IExec (((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))),p,s)) . (fsloc 0) =
(Exec (((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1)))),(IExec ((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))),p,s)))) . (fsloc 0)
by SCMFSA6C:7
.=
s . (fsloc 0)
by A14, SCMFSA_2:72
;
A18:
(s . (fsloc 0)) /. k1 = n1
by A3, A5, FINSEQ_4:15;
A19: (IExec (((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))),p,s)) . (intloc (4 + 1)) =
(Exec (((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1)))),(IExec ((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))),p,s)))) . (intloc (4 + 1))
by SCMFSA6C:6
.=
n1
by A4, A14, A15, A18, Th1
;
A20: (IExec (((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))),p,s)) . (intloc (3 + 1)) =
(Exec (((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1)))),(IExec ((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))),p,s)))) . (intloc (3 + 1))
by SCMFSA6C:6
.=
s . (intloc (2 + 1))
by A16, Lm17, SCMFSA_2:72
;
A21: (IExec (((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))),p,s)) . (intloc (2 + 1)) =
(Exec (((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1)))),(IExec ((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))),p,s)))) . (intloc (2 + 1))
by SCMFSA6C:6
.=
(s . (intloc (2 + 1))) - 1
by A15, Lm15, SCMFSA_2:72
;
A22: (IExec ((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))),p,s)) . (fsloc 0) =
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(IExec (((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))),p,s)))) . (fsloc 0)
by SCMFSA6C:7
.=
s . (fsloc 0)
by A17, SCMFSA_2:72
;
A23:
(s . (fsloc 0)) /. k2 = n2
by A1, A6, FINSEQ_4:15;
A24: (IExec ((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))),p,s)) . (intloc (5 + 1)) =
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(IExec (((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))),p,s)))) . (intloc (5 + 1))
by SCMFSA6C:6
.=
n2
by A7, A17, A20, A23, Th1
;
A25: (IExec ((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))),p,s)) . (intloc (2 + 1)) =
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(IExec (((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))),p,s)))) . (intloc (2 + 1))
by SCMFSA6C:6
.=
(s . (intloc (2 + 1))) - 1
by A21, Lm16, SCMFSA_2:72
;
A26: (IExec ((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))),p,s)) . (intloc (3 + 1)) =
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(IExec (((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))),p,s)))) . (intloc (3 + 1))
by SCMFSA6C:6
.=
s . (intloc (2 + 1))
by A20, Lm18, SCMFSA_2:72
;
A27: (IExec ((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))),p,s)) . (intloc (4 + 1)) =
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(IExec (((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))),p,s)))) . (intloc (4 + 1))
by SCMFSA6C:6
.=
(s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1)
by A19, Lm19, SCMFSA_2:72
;
A28: (IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))),p,s)) . (fsloc 0) =
(Exec ((SubFrom ((intloc (5 + 1)),(intloc (4 + 1)))),(IExec ((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))),p,s)))) . (fsloc 0)
by SCMFSA6C:7
.=
s . (fsloc 0)
by A22, SCMFSA_2:65
;
A29: (IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))),p,s)) . (intloc (2 + 1)) =
(Exec ((SubFrom ((intloc (5 + 1)),(intloc (4 + 1)))),(IExec ((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))),p,s)))) . (intloc (2 + 1))
by SCMFSA6C:6
.=
(s . (intloc (2 + 1))) - 1
by A25, Lm16, SCMFSA_2:65
;
A30: (IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))),p,s)) . (intloc (3 + 1)) =
(Exec ((SubFrom ((intloc (5 + 1)),(intloc (4 + 1)))),(IExec ((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))),p,s)))) . (intloc (3 + 1))
by SCMFSA6C:6
.=
s . (intloc (2 + 1))
by A26, Lm18, SCMFSA_2:65
;
A31: (IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))),p,s)) . (intloc (4 + 1)) =
(Exec ((SubFrom ((intloc (5 + 1)),(intloc (4 + 1)))),(IExec ((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))),p,s)))) . (intloc (4 + 1))
by SCMFSA6C:6
.=
n1
by A27, Lm19, SCMFSA_2:65
;
A32: (IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))),p,s)) . (intloc (5 + 1)) =
(Exec ((SubFrom ((intloc (5 + 1)),(intloc (4 + 1)))),(IExec ((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))),p,s)))) . (intloc (5 + 1))
by SCMFSA6C:6
.=
n2 - n1
by A24, A27, SCMFSA_2:65
;
A33:
(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0) = (IExec ((if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))),p,(IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))),p,s)))) . (fsloc 0)
by SCMFSA6C:2;
thus (IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (intloc (2 + 1)) =
(IExec ((if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))),p,(IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))),p,s)))) . (intloc (2 + 1))
by SCMFSA6C:1
.=
(s . (intloc (2 + 1))) - 1
by A29, Lm28
; ( s . (fsloc 0),(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0) are_fiberwise_equipotent & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) ) & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( for k being set st k <> (s . (intloc (2 + 1))) - 1 & k <> s . (intloc (2 + 1)) & k in dom (s . (fsloc 0)) holds
(s . (fsloc 0)) . k = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k ) & ex x1, x2 being Integer st
( x1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & x1 >= x2 ) )
per cases
( (IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))),p,s)) . (intloc (5 + 1)) > 0 or (IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))),p,s)) . (intloc (5 + 1)) <= 0 )
;
suppose A34:
(IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))),p,s)) . (intloc (5 + 1)) > 0
;
( s . (fsloc 0),(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0) are_fiberwise_equipotent & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) ) & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( for k being set st k <> (s . (intloc (2 + 1))) - 1 & k <> s . (intloc (2 + 1)) & k in dom (s . (fsloc 0)) holds
(s . (fsloc 0)) . k = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k ) & ex x1, x2 being Integer st
( x1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & x1 >= x2 ) )then A35:
(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0) = ((s . (fsloc 0)) +* (k1,n2)) +* (
k2,
n1)
by A4, A7, A23, A28, A29, A30, A31, A33, Lm27;
A36:
dom ((s . (fsloc 0)) +* (k1,n2)) = dom (s . (fsloc 0))
by FUNCT_7:30;
then A37:
dom ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) = dom (s . (fsloc 0))
by A35, FUNCT_7:30;
A38:
k2 in dom ((s . (fsloc 0)) +* (k1,n2))
by A1, A6, A36, FINSEQ_3:25;
A39:
((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k2 = (s . (fsloc 0)) . k1
by A9, A35, A36, FUNCT_7:31;
A40:
now ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k1 = (s . (fsloc 0)) . k2per cases
( k1 = k2 or k1 <> k2 )
;
suppose
k1 = k2
;
((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k1 = (s . (fsloc 0)) . k2hence
((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k1 = (s . (fsloc 0)) . k2
;
verum end; suppose
k1 <> k2
;
((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k1 = (s . (fsloc 0)) . k2hence ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k1 =
((s . (fsloc 0)) +* (k1,n2)) . k1
by A35, FUNCT_7:32
.=
(s . (fsloc 0)) . k2
by A8, FUNCT_7:31
;
verum end; A41:
now for k being set st k <> k1 & k <> k2 & k in dom (s . (fsloc 0)) holds
((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k = (s . (fsloc 0)) . klet k be
set ;
( k <> k1 & k <> k2 & k in dom (s . (fsloc 0)) implies ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k = (s . (fsloc 0)) . k )assume that A42:
k <> k1
and A43:
k <> k2
and
k in dom (s . (fsloc 0))
;
((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k = (s . (fsloc 0)) . kthus ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k =
((s . (fsloc 0)) +* (k1,n2)) . k
by A35, A43, FUNCT_7:32
.=
(s . (fsloc 0)) . k
by A42, FUNCT_7:32
;
verum end; hence
s . (fsloc 0),
(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0) are_fiberwise_equipotent
by A8, A9, A37, A39, A40, RFINSEQ:28;
( ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) ) & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( for k being set st k <> (s . (intloc (2 + 1))) - 1 & k <> s . (intloc (2 + 1)) & k in dom (s . (fsloc 0)) holds
(s . (fsloc 0)) . k = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k ) & ex x1, x2 being Integer st
( x1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & x1 >= x2 ) )thus
(
(s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or
(s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) )
by A40;
( ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) ) & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( for k being set st k <> (s . (intloc (2 + 1))) - 1 & k <> s . (intloc (2 + 1)) & k in dom (s . (fsloc 0)) holds
(s . (fsloc 0)) . k = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k ) & ex x1, x2 being Integer st
( x1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & x1 >= x2 ) )thus
(
(s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or
(s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) )
by A35, A38, FUNCT_7:31;
( ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( for k being set st k <> (s . (intloc (2 + 1))) - 1 & k <> s . (intloc (2 + 1)) & k in dom (s . (fsloc 0)) holds
(s . (fsloc 0)) . k = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k ) & ex x1, x2 being Integer st
( x1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & x1 >= x2 ) )thus
(
(s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) or
(s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) )
by A40;
( ( for k being set st k <> (s . (intloc (2 + 1))) - 1 & k <> s . (intloc (2 + 1)) & k in dom (s . (fsloc 0)) holds
(s . (fsloc 0)) . k = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k ) & ex x1, x2 being Integer st
( x1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & x1 >= x2 ) )thus
for
k being
set st
k <> (s . (intloc (2 + 1))) - 1 &
k <> s . (intloc (2 + 1)) &
k in dom (s . (fsloc 0)) holds
(s . (fsloc 0)) . k = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k
by A41;
ex x1, x2 being Integer st
( x1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & x1 >= x2 )A44:
(n2 - n1) + n1 > 0 + n1
by A32, A34, XREAL_1:6;
take
n2
;
ex x2 being Integer st
( n2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & n2 >= x2 )take
n1
;
( n2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & n1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & n2 >= n1 )thus
(
n2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) &
n1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) &
n2 >= n1 )
by A9, A35, A36, A40, A44, FUNCT_7:31;
verum end; suppose A45:
(IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))),p,s)) . (intloc (5 + 1)) <= 0
;
( s . (fsloc 0),(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0) are_fiberwise_equipotent & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) ) & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( for k being set st k <> (s . (intloc (2 + 1))) - 1 & k <> s . (intloc (2 + 1)) & k in dom (s . (fsloc 0)) holds
(s . (fsloc 0)) . k = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k ) & ex x1, x2 being Integer st
( x1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & x1 >= x2 ) )hence
s . (fsloc 0),
(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0) are_fiberwise_equipotent
by A28, A33, Lm27;
( ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) ) & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( for k being set st k <> (s . (intloc (2 + 1))) - 1 & k <> s . (intloc (2 + 1)) & k in dom (s . (fsloc 0)) holds
(s . (fsloc 0)) . k = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k ) & ex x1, x2 being Integer st
( x1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & x1 >= x2 ) )thus
(
(s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or
(s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) )
by A28, A33, A45, Lm27;
( ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) ) & ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( for k being set st k <> (s . (intloc (2 + 1))) - 1 & k <> s . (intloc (2 + 1)) & k in dom (s . (fsloc 0)) holds
(s . (fsloc 0)) . k = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k ) & ex x1, x2 being Integer st
( x1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & x1 >= x2 ) )thus
(
(s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) or
(s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) )
by A28, A33, A45, Lm27;
( ( (s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) or (s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) ) & ( for k being set st k <> (s . (intloc (2 + 1))) - 1 & k <> s . (intloc (2 + 1)) & k in dom (s . (fsloc 0)) holds
(s . (fsloc 0)) . k = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k ) & ex x1, x2 being Integer st
( x1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & x1 >= x2 ) )thus
(
(s . (fsloc 0)) . (s . (intloc (2 + 1))) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) or
(s . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) )
by A28, A33, A45, Lm27;
( ( for k being set st k <> (s . (intloc (2 + 1))) - 1 & k <> s . (intloc (2 + 1)) & k in dom (s . (fsloc 0)) holds
(s . (fsloc 0)) . k = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k ) & ex x1, x2 being Integer st
( x1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & x1 >= x2 ) )thus
for
k being
set st
k <> (s . (intloc (2 + 1))) - 1 &
k <> s . (intloc (2 + 1)) &
k in dom (s . (fsloc 0)) holds
(s . (fsloc 0)) . k = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . k
by A28, A33, A45, Lm27;
ex x1, x2 being Integer st
( x1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & x1 >= x2 )A46:
(n2 - n1) + n1 <= 0 + n1
by A32, A45, XREAL_1:6;
take
n1
;
ex x2 being Integer st
( n1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & x2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & n1 >= x2 )take
n2
;
( n1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) & n2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) & n1 >= n2 )thus
(
n1 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 1) &
n2 = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))),p,s)) . (fsloc 0)) . (s . (intloc (2 + 1))) &
n1 >= n2 )
by A28, A33, A45, A46, Lm27;
verum end;