let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for md, p0, n being Nat
for f, f1 being FinSequence of INT st s . GBP = 0 & (s . (intpos 4)) - (s . (intpos 2)) > 0 & s . (intpos 2) = md & md >= p0 + 1 & s . (intpos 4) <= p0 + n & p0 >= 7 & f is_FinSequence_on s,p0 & len f = n & f1 is_FinSequence_on IExec (Partition,P,s),p0 & len f1 = n holds
( (IExec (Partition,P,s)) . GBP = 0 & (IExec (Partition,P,s)) . (intpos 1) = s . (intpos 1) & f,f1 are_fiberwise_equipotent & ex m4 being Nat st
( m4 = (IExec (Partition,P,s)) . (intpos 4) & md <= m4 & m4 <= s . (intpos 4) & ( for i being Nat st md <= i & i < m4 holds
(IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st m4 < i & i <= s . (intpos 4) holds
(IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st i >= p0 + 1 & ( i < s . (intpos 2) or i > s . (intpos 4) ) holds
(IExec (Partition,P,s)) . (intpos i) = s . (intpos i) ) ) )
set KW = (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))));
let s be 0 -started State of SCMPDS; :: thesis: for md, p0, n being Nat
for f, f1 being FinSequence of INT st s . GBP = 0 & (s . (intpos 4)) - (s . (intpos 2)) > 0 & s . (intpos 2) = md & md >= p0 + 1 & s . (intpos 4) <= p0 + n & p0 >= 7 & f is_FinSequence_on s,p0 & len f = n & f1 is_FinSequence_on IExec (Partition,P,s),p0 & len f1 = n holds
( (IExec (Partition,P,s)) . GBP = 0 & (IExec (Partition,P,s)) . (intpos 1) = s . (intpos 1) & f,f1 are_fiberwise_equipotent & ex m4 being Nat st
( m4 = (IExec (Partition,P,s)) . (intpos 4) & md <= m4 & m4 <= s . (intpos 4) & ( for i being Nat st md <= i & i < m4 holds
(IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st m4 < i & i <= s . (intpos 4) holds
(IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st i >= p0 + 1 & ( i < s . (intpos 2) or i > s . (intpos 4) ) holds
(IExec (Partition,P,s)) . (intpos i) = s . (intpos i) ) ) )
let md, n0, n be Nat; :: thesis: for f, f1 being FinSequence of INT st s . GBP = 0 & (s . (intpos 4)) - (s . (intpos 2)) > 0 & s . (intpos 2) = md & md >= n0 + 1 & s . (intpos 4) <= n0 + n & n0 >= 7 & f is_FinSequence_on s,n0 & len f = n & f1 is_FinSequence_on IExec (Partition,P,s),n0 & len f1 = n holds
( (IExec (Partition,P,s)) . GBP = 0 & (IExec (Partition,P,s)) . (intpos 1) = s . (intpos 1) & f,f1 are_fiberwise_equipotent & ex m4 being Nat st
( m4 = (IExec (Partition,P,s)) . (intpos 4) & md <= m4 & m4 <= s . (intpos 4) & ( for i being Nat st md <= i & i < m4 holds
(IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st m4 < i & i <= s . (intpos 4) holds
(IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st i >= n0 + 1 & ( i < s . (intpos 2) or i > s . (intpos 4) ) holds
(IExec (Partition,P,s)) . (intpos i) = s . (intpos i) ) ) )
let f, f1 be FinSequence of INT ; :: thesis: ( s . GBP = 0 & (s . (intpos 4)) - (s . (intpos 2)) > 0 & s . (intpos 2) = md & md >= n0 + 1 & s . (intpos 4) <= n0 + n & n0 >= 7 & f is_FinSequence_on s,n0 & len f = n & f1 is_FinSequence_on IExec (Partition,P,s),n0 & len f1 = n implies ( (IExec (Partition,P,s)) . GBP = 0 & (IExec (Partition,P,s)) . (intpos 1) = s . (intpos 1) & f,f1 are_fiberwise_equipotent & ex m4 being Nat st
( m4 = (IExec (Partition,P,s)) . (intpos 4) & md <= m4 & m4 <= s . (intpos 4) & ( for i being Nat st md <= i & i < m4 holds
(IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st m4 < i & i <= s . (intpos 4) holds
(IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st i >= n0 + 1 & ( i < s . (intpos 2) or i > s . (intpos 4) ) holds
(IExec (Partition,P,s)) . (intpos i) = s . (intpos i) ) ) ) )
A1: Initialize s = s by MEMSTR_0:44;
set s1 = IExec (Partition,P,s);
set s2 = IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s);
set P2 = P;
set s3 = IExec (((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))),P,s);
set a = GBP ;
A2: (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . GBP = (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) . GBP by SCMPDS_5:15;
A3: (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 1) = (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) . (intpos 1) by SCMPDS_5:15;
A4: (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 2) = (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) . (intpos 2) by SCMPDS_5:15;
A5: (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 3) = (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) . (intpos 3) by SCMPDS_5:15;
A6: (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 4) = (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) . (intpos 4) by SCMPDS_5:15;
A7: (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 5) = (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) . (intpos 5) by SCMPDS_5:15;
assume that
A8: s . GBP = 0 and
A9: (s . (intpos 4)) - (s . (intpos 2)) > 0 and
A10: s . (intpos 2) = md and
A11: md >= n0 + 1 and
A12: s . (intpos 4) <= n0 + n and
A13: n0 >= 7 ; :: thesis: ( not f is_FinSequence_on s,n0 or not len f = n or not f1 is_FinSequence_on IExec (Partition,P,s),n0 or not len f1 = n or ( (IExec (Partition,P,s)) . GBP = 0 & (IExec (Partition,P,s)) . (intpos 1) = s . (intpos 1) & f,f1 are_fiberwise_equipotent & ex m4 being Nat st
( m4 = (IExec (Partition,P,s)) . (intpos 4) & md <= m4 & m4 <= s . (intpos 4) & ( for i being Nat st md <= i & i < m4 holds
(IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st m4 < i & i <= s . (intpos 4) holds
(IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st i >= n0 + 1 & ( i < s . (intpos 2) or i > s . (intpos 4) ) holds
(IExec (Partition,P,s)) . (intpos i) = s . (intpos i) ) ) ) )
A14: (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . GBP = 0 by A8, Lm27, A1;
A15: (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 1) = s . (intpos 1) by A8, Lm27, A1;
A16: n0 + 1 >= 7 + 1 by A13, XREAL_1:6;
then A17: md >= 8 by A11, XXREAL_0:2;
then A18: md > 1 by XXREAL_0:2;
A19: md > 4 by A17, XXREAL_0:2;
A20: md - n0 >= 1 by A11, XREAL_1:19;
then reconsider n1 = md - n0 as Element of NAT by INT_1:3;
A21: md = n0 + n1 ;
A22: (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 4) = s . (intpos 4) by A8, Lm27, A1;
set m3 = md;
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) by A8, Lm27, A1;
then A23: (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 4) = md + ((IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 5)) by A8, A10, Lm27, A1;
set s4 = IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))));
consider f3 being FinSequence of INT such that
A24: len f3 = n and
A25: for i being Nat st 1 <= i & i <= len f3 holds
f3 . i = (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos (n0 + i)) by SCPISORT:1;
A26: f3 is_FinSequence_on IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)))),n0 by A25;
md < s . (intpos 4) by A9, A10, XREAL_1:47;
then md < n0 + n by A12, XXREAL_0:2;
then A27: n1 <= len f3 by A24, XREAL_1:20;
A28: (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 2) = s . (intpos 2) by A8, Lm27, A1;
A29: (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 3) = (s . (intpos 2)) + 1 by A8, Lm27, A1;
then A30: s . (intpos 2) = ((IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 3)) - 1 ;
A31: (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) . GBP = (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . GBP by SCMPDS_5:15;
A32: (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) . (intpos 2) = (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 2) by SCMPDS_5:15;
A33: (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) . (intpos 3) = (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 3) by SCMPDS_5:15;
A34: (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) . (intpos 4) = (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 4) by SCMPDS_5:15;
A35: (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) . (intpos 5) = (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 5) by SCMPDS_5:15;
A36: while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))) is_halting_on Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)),P by A10, A11, A13, A14, A28, A23, Lm26, A30, A31, A32, A33, A34, A35;
A37: while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))) is_halting_on IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s),P
proof
P +* (stop (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) halts_on Initialize (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) by A36, SCMPDS_6:def 3;
hence while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))) is_halting_on IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s),P by SCMPDS_6:def 3; :: thesis: verum
end;
s . (intpos 2) < (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 3) by A29, XREAL_1:29;
then A38: n0 + 1 <= (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 3) by A10, A11, XXREAL_0:2;
A39: while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))) is_closed_on Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)),P by A10, A11, A13, A14, A28, A30, A23, Lm26, A31, A32, A33, A34, A35;
A40: while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))) is_closed_on IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s),P
proof
for k being Nat holds IC (Comput ((P +* (stop (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))))),(Initialize (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)))),k)) in dom (stop (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) by A39, SCMPDS_6:def 2;
hence while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))) is_closed_on IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s),P by SCMPDS_6:def 2; :: thesis: verum
end;
then A41: (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))) is_halting_on s,P by A37, A1, SCPISORT:9;
consider f2 being FinSequence of INT such that
A42: len f2 = n and
A43: for i being Nat st 1 <= i & i <= len f2 holds
f2 . i = (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos (n0 + i)) by SCPISORT:1;
A44: f2 is_FinSequence_on Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)),n0
proof
let i be Nat; :: according to SCPISORT:def 1 :: thesis: ( not 1 <= i or not i <= len f2 or f2 . i = (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) . (intpos (n0 + i)) )
assume ( 1 <= i & i <= len f2 ) ; :: thesis: f2 . i = (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) . (intpos (n0 + i))
then f2 . i = (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos (n0 + i)) by A43;
hence f2 . i = (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) . (intpos (n0 + i)) by SCMPDS_5:15; :: thesis: verum
end;
then A45: f2,f3 are_fiberwise_equipotent by A9, A10, A11, A12, A13, A14, A28, A22, A30, A23, A38, A42, A24, A26, Lm25, A2, A4, A5, A6, A7;
(IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos 4) > 0 by A9, A10, A11, A12, A13, A14, A28, A22, A30, A23, A38, A42, A44, A24, A26, Lm25, A2, A4, A5, A6, A7;
then reconsider m4 = (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos 4) as Element of NAT by INT_1:3;
A46: (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos 4) >= md by A9, A10, A11, A12, A13, A14, A28, A22, A30, A23, A38, A42, A44, A24, A26, Lm25, A2, A4, A5, A6, A7;
then A47: m4 - n0 >= md - n0 by XREAL_1:9;
then reconsider n2 = m4 - n0 as Element of NAT by A20, INT_1:3;
A48: m4 - n0 >= 1 by A20, A47, XXREAL_0:2;
(IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos 2) = md by A9, A10, A11, A12, A13, A14, A28, A22, A30, A23, A38, A42, A44, A24, A26, Lm25, A2, A4, A5, A6, A7;
then A49: (IExec (((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))),P,s)) . (intpos 2) = md by A40, A37, SCPISORT:7;
A50: (IExec (((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))),P,s)) . (intpos 4) = m4 by A40, A37, SCPISORT:7;
(IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . GBP = 0 by A9, A10, A11, A12, A13, A14, A28, A22, A30, A23, A38, A42, A44, A24, A26, Lm25, A2, A4, A5, A6, A7;
then A51: (IExec (((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))),P,s)) . GBP = 0 by A40, A37, SCPISORT:7;
then A52: DataLoc (((IExec (((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))),P,s)) . GBP),6) = intpos (0 + 6) by SCMP_GCD:1;
set t2 = IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s);
set t3 = IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s);
assume that
A53: f is_FinSequence_on s,n0 and
A54: len f = n ; :: thesis: ( not f1 is_FinSequence_on IExec (Partition,P,s),n0 or not len f1 = n or ( (IExec (Partition,P,s)) . GBP = 0 & (IExec (Partition,P,s)) . (intpos 1) = s . (intpos 1) & f,f1 are_fiberwise_equipotent & ex m4 being Nat st
( m4 = (IExec (Partition,P,s)) . (intpos 4) & md <= m4 & m4 <= s . (intpos 4) & ( for i being Nat st md <= i & i < m4 holds
(IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st m4 < i & i <= s . (intpos 4) holds
(IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st i >= n0 + 1 & ( i < s . (intpos 2) or i > s . (intpos 4) ) holds
(IExec (Partition,P,s)) . (intpos i) = s . (intpos i) ) ) ) )
assume that
A55: f1 is_FinSequence_on IExec (Partition,P,s),n0 and
A56: len f1 = n ; :: thesis: ( (IExec (Partition,P,s)) . GBP = 0 & (IExec (Partition,P,s)) . (intpos 1) = s . (intpos 1) & f,f1 are_fiberwise_equipotent & ex m4 being Nat st
( m4 = (IExec (Partition,P,s)) . (intpos 4) & md <= m4 & m4 <= s . (intpos 4) & ( for i being Nat st md <= i & i < m4 holds
(IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st m4 < i & i <= s . (intpos 4) holds
(IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st i >= n0 + 1 & ( i < s . (intpos 2) or i > s . (intpos 4) ) holds
(IExec (Partition,P,s)) . (intpos i) = s . (intpos i) ) ) )
A57: dom f2 = Seg n by A42, FINSEQ_1:def 3;
A58: now :: thesis: for i being Nat st i in dom f2 holds
f2 . i = f . i
let i be Nat; :: thesis: ( i in dom f2 implies f2 . i = f . i )
reconsider a = i as Nat ;
assume A59: i in dom f2 ; :: thesis: f2 . i = f . i
then A60: 1 <= i by A57, FINSEQ_1:1;
then i + n0 >= n0 + 1 by XREAL_1:6;
then A61: n0 + i >= 8 by A16, XXREAL_0:2;
A62: i <= n by A57, A59, FINSEQ_1:1;
hence f2 . i = (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos (n0 + a)) by A42, A43, A60
.= s . (intpos (n0 + a)) by A8, A61, Lm27, A1
.= f . i by A53, A54, A60, A62 ;
:: thesis: verum
end;
A63: (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))) is_closed_on s,P by A40, A37, A1, SCPISORT:9;
then A64: ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0)) is_closed_on s,P by A41, SCPISORT:10;
A65: (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos 4) <= (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 4) by A9, A10, A11, A12, A13, A14, A28, A22, A30, A23, A38, A42, A44, A24, A26, Lm25, A2, A4, A5, A6, A7;
then m4 <= n0 + n by A12, A22, XXREAL_0:2;
then A66: n2 <= len f3 by A24, XREAL_1:20;
A67: (IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos 6) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec (((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))),P,s)))) . (intpos 6) by A63, A41, SCMPDS_7:31
.= (IExec (((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))),P,s)) . (DataLoc (((IExec (((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))),P,s)) . (intpos 4)),0)) by A52, SCMPDS_2:47
.= (IExec (((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))),P,s)) . (intpos (m4 + 0)) by A50, SCMP_GCD:1
.= (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos m4) by A40, A37, SCPISORT:7 ;
A68: (IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos 4) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec (((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))),P,s)))) . (intpos 4) by A63, A41, SCMPDS_7:31
.= m4 by A50, A52, AMI_3:10, SCMPDS_2:47 ;
then A69: DataLoc (((IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos 4)),0) = intpos (m4 + 0) by SCMP_GCD:1;
A70: (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos 1) = (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 1) by A9, A10, A11, A12, A13, A14, A28, A22, A30, A23, A38, A42, A44, A24, A26, Lm25, A2, A3, A4, A5, A6, A7;
A71: (IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos 1) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec (((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))),P,s)))) . (intpos 1) by A63, A41, SCMPDS_7:31
.= (IExec (((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))),P,s)) . (intpos 1) by A52, AMI_3:10, SCMPDS_2:47
.= s . (intpos 1) by A15, A70, A40, A37, SCPISORT:7 ;
A72: (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos 4) >= 8 by A46, A17, XXREAL_0:2;
then A73: m4 > 2 by XXREAL_0:2;
A74: (IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . GBP = (Exec (((GBP,6) := ((intpos 4),0)),(IExec (((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))),P,s)))) . GBP by A63, A41, SCMPDS_7:31
.= 0 by A51, A52, AMI_3:10, SCMPDS_2:47 ;
A75: (IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos 2) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec (((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))),P,s)))) . (intpos 2) by A63, A41, SCMPDS_7:31
.= md by A49, A52, AMI_3:10, SCMPDS_2:47 ;
A76: ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0)) is_halting_on s,P by A63, A41, SCPISORT:10;
then A77: (((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0)) is_halting_on s,P by A64, SCPISORT:10;
(IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)) . (intpos 2) = (Exec ((((intpos 4),0) := ((intpos 2),0)),(IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)))) . (intpos 2) by A64, A76, SCMPDS_7:31
.= md by A75, A69, A73, AMI_3:10, SCMPDS_2:47 ;
then A78: DataLoc (((IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)) . (intpos 2)),0) = intpos (md + 0) by SCMP_GCD:1;
A79: m4 > 6 by A72, XXREAL_0:2;
A80: m4 > 1 by A72, XXREAL_0:2;
A81: (IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)) . (intpos 6) = (Exec ((((intpos 4),0) := ((intpos 2),0)),(IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)))) . (intpos 6) by A64, A76, SCMPDS_7:31
.= (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos m4) by A67, A69, A79, AMI_3:10, SCMPDS_2:47 ;
A82: (IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)) . GBP = (Exec ((((intpos 4),0) := ((intpos 2),0)),(IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)))) . GBP by A64, A76, SCMPDS_7:31
.= 0 by A11, A46, A74, A69, AMI_3:10, SCMPDS_2:47 ;
A83: (((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0)) is_closed_on s,P by A64, A76, SCPISORT:10;
then A84: (IExec (Partition,P,s)) . (intpos md) = (Exec ((((intpos 2),0) := (GBP,6)),(IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)))) . (intpos md) by A77, SCMPDS_7:31
.= (IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)) . (DataLoc (((IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)) . GBP),6)) by A78, SCMPDS_2:47
.= (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos m4) by A82, A81, SCMP_GCD:1 ;
A85: now :: thesis: for i being Nat st i >= 8 holds
(IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos i) = (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos i)
let i be Nat; :: thesis: ( i >= 8 implies (IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos i) = (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos i) )
assume i >= 8 ; :: thesis: (IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos i) = (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos i)
then A86: i > 6 by XXREAL_0:2;
thus (IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos i) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec (((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))),P,s)))) . (intpos i) by A63, A41, SCMPDS_7:31
.= (IExec (((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))),P,s)) . (intpos i) by A52, A86, AMI_3:10, SCMPDS_2:47
.= (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos i) by A40, A37, SCPISORT:7 ; :: thesis: verum
end;
A87: now :: thesis: for i being Nat st i >= 8 & i <> m4 holds
(IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)) . (intpos i) = (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos i)
let i be Nat; :: thesis: ( i >= 8 & i <> m4 implies (IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)) . (intpos i) = (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos i) )
assume that
A88: i >= 8 and
A89: i <> m4 ; :: thesis: (IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)) . (intpos i) = (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos i)
thus (IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)) . (intpos i) = (Exec ((((intpos 4),0) := ((intpos 2),0)),(IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)))) . (intpos i) by A64, A76, SCMPDS_7:31
.= (IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos i) by A69, A89, AMI_3:10, SCMPDS_2:47
.= (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos i) by A85, A88 ; :: thesis: verum
end;
A90: now :: thesis: for i being Nat st i >= 8 & i <> m4 & i <> md holds
(IExec (Partition,P,s)) . (intpos i) = (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos i)
let i be Nat; :: thesis: ( i >= 8 & i <> m4 & i <> md implies (IExec (Partition,P,s)) . (intpos i) = (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos i) )
assume that
A91: i >= 8 and
A92: i <> m4 and
A93: i <> md ; :: thesis: (IExec (Partition,P,s)) . (intpos i) = (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos i)
thus (IExec (Partition,P,s)) . (intpos i) = (Exec ((((intpos 2),0) := (GBP,6)),(IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)))) . (intpos i) by A83, A77, SCMPDS_7:31
.= (IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)) . (intpos i) by A78, A93, AMI_3:10, SCMPDS_2:47
.= (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos i) by A87, A91, A92 ; :: thesis: verum
end;
A94: now :: thesis: for k being Nat st k <> n1 & k <> n2 & 1 <= k & k <= len f3 holds
f3 . k = f1 . k
let k be Nat; :: thesis: ( k <> n1 & k <> n2 & 1 <= k & k <= len f3 implies f3 . k = f1 . k )
assume that
A95: k <> n1 and
A96: k <> n2 and
A97: 1 <= k and
A98: k <= len f3 ; :: thesis: f3 . k = f1 . k
A99: k + n0 <> md by A95;
A100: k + n0 >= n0 + 1 by A97, XREAL_1:6;
A101: k + n0 <> m4 by A96;
thus f3 . k = (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos (n0 + k)) by A25, A97, A98
.= (IExec (Partition,P,s)) . (intpos (n0 + k)) by A16, A90, A99, A101, A100, XXREAL_0:2
.= f1 . k by A55, A56, A24, A97, A98 ; :: thesis: verum
end;
A102: m4 = n0 + n2 ;
then A103: f3 . n2 = (IExec (Partition,P,s)) . (intpos md) by A25, A84, A48, A66
.= f1 . n1 by A55, A56, A24, A20, A27, A21 ;
A104: (IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)) . (intpos 1) = (Exec ((((intpos 4),0) := ((intpos 2),0)),(IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)))) . (intpos 1) by A64, A76, SCMPDS_7:31
.= s . (intpos 1) by A71, A69, A80, AMI_3:10, SCMPDS_2:47 ;
thus (IExec (Partition,P,s)) . GBP = (Exec ((((intpos 2),0) := (GBP,6)),(IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)))) . GBP by A83, A77, SCMPDS_7:31
.= 0 by A11, A82, A78, AMI_3:10, SCMPDS_2:47 ; :: thesis: ( (IExec (Partition,P,s)) . (intpos 1) = s . (intpos 1) & f,f1 are_fiberwise_equipotent & ex m4 being Nat st
( m4 = (IExec (Partition,P,s)) . (intpos 4) & md <= m4 & m4 <= s . (intpos 4) & ( for i being Nat st md <= i & i < m4 holds
(IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st m4 < i & i <= s . (intpos 4) holds
(IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st i >= n0 + 1 & ( i < s . (intpos 2) or i > s . (intpos 4) ) holds
(IExec (Partition,P,s)) . (intpos i) = s . (intpos i) ) ) )
thus (IExec (Partition,P,s)) . (intpos 1) = (Exec ((((intpos 2),0) := (GBP,6)),(IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)))) . (intpos 1) by A83, A77, SCMPDS_7:31
.= s . (intpos 1) by A104, A78, A18, AMI_3:10, SCMPDS_2:47 ; :: thesis: ( f,f1 are_fiberwise_equipotent & ex m4 being Nat st
( m4 = (IExec (Partition,P,s)) . (intpos 4) & md <= m4 & m4 <= s . (intpos 4) & ( for i being Nat st md <= i & i < m4 holds
(IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st m4 < i & i <= s . (intpos 4) holds
(IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st i >= n0 + 1 & ( i < s . (intpos 2) or i > s . (intpos 4) ) holds
(IExec (Partition,P,s)) . (intpos i) = s . (intpos i) ) ) )
A105: m4 > 4 by A72, XXREAL_0:2;
A106: (IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)) . (intpos 4) = (Exec ((((intpos 4),0) := ((intpos 2),0)),(IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)))) . (intpos 4) by A64, A76, SCMPDS_7:31
.= m4 by A68, A69, A105, AMI_3:10, SCMPDS_2:47 ;
A107: (IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)) . (intpos m4) = (Exec ((((intpos 4),0) := ((intpos 2),0)),(IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)))) . (intpos m4) by A64, A76, SCMPDS_7:31
.= (IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (DataLoc (((IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos 2)),0)) by A69, SCMPDS_2:47
.= (IExec ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos (md + 0)) by A75, SCMP_GCD:1
.= (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos md) by A11, A16, A85, XXREAL_0:2 ;
A108: now :: thesis: (IExec (Partition,P,s)) . (intpos m4) = (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos md)
per cases ( m4 = md or m4 <> md ) ;
suppose m4 = md ; :: thesis: (IExec (Partition,P,s)) . (intpos m4) = (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos md)
hence (IExec (Partition,P,s)) . (intpos m4) = (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos md) by A84; :: thesis: verum
end;
suppose A109: m4 <> md ; :: thesis: (IExec (Partition,P,s)) . (intpos m4) = (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos md)
thus (IExec (Partition,P,s)) . (intpos m4) = (Exec ((((intpos 2),0) := (GBP,6)),(IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)))) . (intpos m4) by A83, A77, SCMPDS_7:31
.= (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos md) by A107, A78, A109, AMI_3:10, SCMPDS_2:47 ; :: thesis: verum
end;
end;
end;
then f3 . n1 = (IExec (Partition,P,s)) . (intpos m4) by A25, A20, A27, A21
.= f1 . n2 by A55, A56, A24, A48, A66, A102 ;
then f3,f1 are_fiberwise_equipotent by A56, A24, A20, A27, A48, A66, A103, A94, SCPISORT:3;
then f2,f1 are_fiberwise_equipotent by A45, CLASSES1:76;
hence f,f1 are_fiberwise_equipotent by A54, A42, A58, FINSEQ_2:9; :: thesis: ex m4 being Nat st
( m4 = (IExec (Partition,P,s)) . (intpos 4) & md <= m4 & m4 <= s . (intpos 4) & ( for i being Nat st md <= i & i < m4 holds
(IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st m4 < i & i <= s . (intpos 4) holds
(IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st i >= n0 + 1 & ( i < s . (intpos 2) or i > s . (intpos 4) ) holds
(IExec (Partition,P,s)) . (intpos i) = s . (intpos i) ) )
take m4 ; :: thesis: ( m4 = (IExec (Partition,P,s)) . (intpos 4) & md <= m4 & m4 <= s . (intpos 4) & ( for i being Nat st md <= i & i < m4 holds
(IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st m4 < i & i <= s . (intpos 4) holds
(IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st i >= n0 + 1 & ( i < s . (intpos 2) or i > s . (intpos 4) ) holds
(IExec (Partition,P,s)) . (intpos i) = s . (intpos i) ) )
thus (IExec (Partition,P,s)) . (intpos 4) = (Exec ((((intpos 2),0) := (GBP,6)),(IExec (((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))),P,s)))) . (intpos 4) by A83, A77, SCMPDS_7:31
.= m4 by A106, A78, A19, AMI_3:10, SCMPDS_2:47 ; :: thesis: ( md <= m4 & m4 <= s . (intpos 4) & ( for i being Nat st md <= i & i < m4 holds
(IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st m4 < i & i <= s . (intpos 4) holds
(IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st i >= n0 + 1 & ( i < s . (intpos 2) or i > s . (intpos 4) ) holds
(IExec (Partition,P,s)) . (intpos i) = s . (intpos i) ) )
A110: md = ((IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 3)) - 1 by A10, A29;
hence md <= m4 by A9, A10, A11, A12, A13, A14, A28, A22, A23, A38, A42, A44, A24, A26, Lm25, A2, A4, A5, A6, A7; :: thesis: ( m4 <= s . (intpos 4) & ( for i being Nat st md <= i & i < m4 holds
(IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st m4 < i & i <= s . (intpos 4) holds
(IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st i >= n0 + 1 & ( i < s . (intpos 2) or i > s . (intpos 4) ) holds
(IExec (Partition,P,s)) . (intpos i) = s . (intpos i) ) )
thus m4 <= s . (intpos 4) by A9, A10, A11, A12, A13, A14, A28, A22, A30, A23, A38, A42, A44, A24, A26, Lm25, A2, A4, A5, A6, A7; :: thesis: ( ( for i being Nat st md <= i & i < m4 holds
(IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st m4 < i & i <= s . (intpos 4) holds
(IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st i >= n0 + 1 & ( i < s . (intpos 2) or i > s . (intpos 4) ) holds
(IExec (Partition,P,s)) . (intpos i) = s . (intpos i) ) )
A111: (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 3) = md + 1 by A8, A10, Lm27, A1;
hereby :: thesis: ( ( for i being Nat st m4 < i & i <= s . (intpos 4) holds
(IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st i >= n0 + 1 & ( i < s . (intpos 2) or i > s . (intpos 4) ) holds
(IExec (Partition,P,s)) . (intpos i) = s . (intpos i) ) )
let i be Nat; :: thesis: ( md <= i & i < m4 implies (IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos b1) )
assume that
A112: md <= i and
A113: i < m4 ; :: thesis: (IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos b1)
per cases ( i = md or i <> md ) ;
suppose A114: i = md ; :: thesis: (IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos b1)
then (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 3) <= m4 by A111, A113, INT_1:7;
hence (IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos i) by A114, A84, A9, A10, A11, A12, A13, A14, A28, A22, A110, A23, A38, A42, A44, A24, A26, A108, Lm25, A2, A4, A5, A6, A7; :: thesis: verum
end;
suppose A115: i <> md ; :: thesis: (IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos b1)
then md < i by A112, XXREAL_0:1;
then (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 3) <= i by A10, A29, INT_1:7;
then (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos md) >= (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos i) by A9, A10, A11, A12, A13, A14, A28, A22, A110, A23, A38, A42, A44, A24, A26, A113, Lm25, A2, A4, A5, A6, A7;
hence (IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos i) by A17, A108, A90, A112, A115, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hereby :: thesis: for i being Nat st i >= n0 + 1 & ( i < s . (intpos 2) or i > s . (intpos 4) ) holds
(IExec (Partition,P,s)) . (intpos i) = s . (intpos i)
let i be Nat; :: thesis: ( m4 < i & i <= s . (intpos 4) implies (IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i) )
assume that
A116: m4 < i and
A117: i <= s . (intpos 4) ; :: thesis: (IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i)
A118: md < i by A46, A116, XXREAL_0:2;
(IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos md) <= (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos i) by A9, A10, A11, A12, A13, A14, A28, A22, A30, A23, A38, A42, A44, A24, A26, A116, A117, Lm25, A2, A4, A5, A6, A7;
hence (IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i) by A17, A108, A90, A118, XXREAL_0:2; :: thesis: verum
end;
hereby :: thesis: verum
let i be Nat; :: thesis: ( i >= n0 + 1 & ( i < s . (intpos 2) or i > s . (intpos 4) ) implies (IExec (Partition,P,s)) . (intpos i) = s . (intpos i) )
assume that
A119: i >= n0 + 1 and
A120: ( i < s . (intpos 2) or i > s . (intpos 4) ) ; :: thesis: (IExec (Partition,P,s)) . (intpos i) = s . (intpos i)
A121: i >= 8 by A16, A119, XXREAL_0:2;
A122: now :: thesis: ( ( i < s . (intpos 2) & i < (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 3) ) or ( i > s . (intpos 4) & i > (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 4) ) )
per cases ( i < s . (intpos 2) or i > s . (intpos 4) ) by A120;
case A123: i < s . (intpos 2) ; :: thesis: i < (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 3)
s . (intpos 2) < (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 3) by A29, XREAL_1:29;
hence i < (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 3) by A123, XXREAL_0:2; :: thesis: verum
end;
case i > s . (intpos 4) ; :: thesis: i > (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 4)
hence i > (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos 4) by A8, Lm27, A1; :: thesis: verum
end;
end;
end;
A124: (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos i) = (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) . (intpos i) by SCMPDS_5:15;
A125: for i being Nat st i >= n0 + 1 & ( i < (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) . (intpos 3) or i > (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) . (intpos 4) ) holds
(IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos i) = (Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))) . (intpos i) by A9, A10, A11, A12, A13, A14, A28, A22, A110, A23, A38, A42, A44, A24, A26, Lm25, A2, A4, A5, A6, A7;
( i <> md & i <> m4 )
proof
per cases ( i < s . (intpos 2) or i > s . (intpos 4) ) by A120;
suppose i < s . (intpos 2) ; :: thesis: ( i <> md & i <> m4 )
hence ( i <> md & i <> m4 ) by A9, A10, A11, A12, A13, A14, A28, A22, A30, A23, A38, A42, A44, A24, A26, Lm25, A2, A4, A5, A6, A7; :: thesis: verum
end;
suppose i > s . (intpos 4) ; :: thesis: ( i <> md & i <> m4 )
hence ( i <> md & i <> m4 ) by A22, A46, A65, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence (IExec (Partition,P,s)) . (intpos i) = (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,(Initialize (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s))))) . (intpos i) by A16, A90, A119, XXREAL_0:2
.= (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,s)) . (intpos i) by A119, A122, A125, A5, A6, A124
.= s . (intpos i) by A8, A121, Lm27, A1 ;
:: thesis: verum
end;