let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for f, g being FinSequence of INT
for k0, k being Element of NAT st s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & k = s . (intpos 6) & k0 = ((s . (intpos 4)) - (s . (intpos 6))) - 1 & f is_FinSequence_on s,k0 & g is_FinSequence_on IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),P,s),k0 & len f = len g & len f > k & f is_non_decreasing_on 1,k holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,k + 1 & ( for i being Element of NAT st i > k + 1 & i <= len f holds
f . i = g . i ) & ( for i being Element of NAT st 1 <= i & i <= k + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= k + 1 & g . i = f . j ) ) )
set a = GBP ;
let s be 0 -started State of SCMPDS; :: thesis: for f, g being FinSequence of INT
for k0, k being Element of NAT st s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & k = s . (intpos 6) & k0 = ((s . (intpos 4)) - (s . (intpos 6))) - 1 & f is_FinSequence_on s,k0 & g is_FinSequence_on IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),P,s),k0 & len f = len g & len f > k & f is_non_decreasing_on 1,k holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,k + 1 & ( for i being Element of NAT st i > k + 1 & i <= len f holds
f . i = g . i ) & ( for i being Element of NAT st 1 <= i & i <= k + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= k + 1 & g . i = f . j ) ) )
let f, g be FinSequence of INT ; :: thesis: for k0, k being Element of NAT st s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & k = s . (intpos 6) & k0 = ((s . (intpos 4)) - (s . (intpos 6))) - 1 & f is_FinSequence_on s,k0 & g is_FinSequence_on IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),P,s),k0 & len f = len g & len f > k & f is_non_decreasing_on 1,k holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,k + 1 & ( for i being Element of NAT st i > k + 1 & i <= len f holds
f . i = g . i ) & ( for i being Element of NAT st 1 <= i & i <= k + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= k + 1 & g . i = f . j ) ) )
let m, n be Element of NAT ; :: thesis: ( s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & n = s . (intpos 6) & m = ((s . (intpos 4)) - (s . (intpos 6))) - 1 & f is_FinSequence_on s,m & g is_FinSequence_on IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),P,s),m & len f = len g & len f > n & f is_non_decreasing_on 1,n implies ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n + 1 & ( for i being Element of NAT st i > n + 1 & i <= len f holds
f . i = g . i ) & ( for i being Element of NAT st 1 <= i & i <= n + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= n + 1 & g . i = f . j ) ) ) )
assume A1: ( s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & n = s . (intpos 6) & m = ((s . (intpos 4)) - (s . (intpos 6))) - 1 ) ; :: thesis: ( not f is_FinSequence_on s,m or not g is_FinSequence_on IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),P,s),m or not len f = len g or not len f > n or not f is_non_decreasing_on 1,n or ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n + 1 & ( for i being Element of NAT st i > n + 1 & i <= len f holds
f . i = g . i ) & ( for i being Element of NAT st 1 <= i & i <= n + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= n + 1 & g . i = f . j ) ) ) )
defpred S1[ Element of NAT ] means for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS
for f1, f2 being FinSequence of INT st t . (intpos 4) >= 7 + (t . (intpos 6)) & t . GBP = 0 & $1 = t . (intpos 6) & m = ((t . (intpos 4)) - (t . (intpos 6))) - 1 & f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,t),m & len f1 = len f2 & len f1 > $1 & f1 is_non_decreasing_on 1,$1 holds
( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,$1 + 1 & ( for i being Element of NAT st i > $1 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= $1 + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= $1 + 1 & f2 . i = f1 . j ) ) );
assume A2: ( f is_FinSequence_on s,m & g is_FinSequence_on IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),P,s),m ) ; :: thesis: ( not len f = len g or not len f > n or not f is_non_decreasing_on 1,n or ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n + 1 & ( for i being Element of NAT st i > n + 1 & i <= len f holds
f . i = g . i ) & ( for i being Element of NAT st 1 <= i & i <= n + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= n + 1 & g . i = f . j ) ) ) )
A3: now
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
thus S1[k + 1] :: thesis: verum
proof
let t be 0 -started State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS
for f1, f2 being FinSequence of INT st t . (intpos 4) >= 7 + (t . (intpos 6)) & t . GBP = 0 & k + 1 = t . (intpos 6) & m = ((t . (intpos 4)) - (t . (intpos 6))) - 1 & f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,t),m & len f1 = len f2 & len f1 > k + 1 & f1 is_non_decreasing_on 1,k + 1 holds
( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,(k + 1) + 1 & ( for i being Element of NAT st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
let Q be Instruction-Sequence of SCMPDS; :: thesis: for f1, f2 being FinSequence of INT st t . (intpos 4) >= 7 + (t . (intpos 6)) & t . GBP = 0 & k + 1 = t . (intpos 6) & m = ((t . (intpos 4)) - (t . (intpos 6))) - 1 & f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,t),m & len f1 = len f2 & len f1 > k + 1 & f1 is_non_decreasing_on 1,k + 1 holds
( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,(k + 1) + 1 & ( for i being Element of NAT st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
let f1, f2 be FinSequence of INT ; :: thesis: ( t . (intpos 4) >= 7 + (t . (intpos 6)) & t . GBP = 0 & k + 1 = t . (intpos 6) & m = ((t . (intpos 4)) - (t . (intpos 6))) - 1 & f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,t),m & len f1 = len f2 & len f1 > k + 1 & f1 is_non_decreasing_on 1,k + 1 implies ( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,(k + 1) + 1 & ( for i being Element of NAT st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) ) )
T: Initialize t = t by MEMSTR_0:44;
assume that
A5: t . (intpos 4) >= 7 + (t . (intpos 6)) and
A6: t . GBP = 0 and
A7: k + 1 = t . (intpos 6) and
A8: m = ((t . (intpos 4)) - (t . (intpos 6))) - 1 and
A9: f1 is_FinSequence_on t,m and
A10: f2 is_FinSequence_on IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,t),m and
A11: len f1 = len f2 and
A12: len f1 > k + 1 and
A13: f1 is_non_decreasing_on 1,k + 1 ; :: thesis: ( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,(k + 1) + 1 & ( for i being Element of NAT st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
set Bt = IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t);
set x = DataLoc ((t . (intpos 4)),(- 1));
set y = DataLoc ((t . (intpos 4)),0);
A20: (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . GBP = 0 by A5, A6, A7, Lm7;
(m + 1) + (k + 1) >= 7 + (t . (intpos 6)) by A5, A7, A8;
then A21: m + 1 >= 7 by A7, XREAL_1:6;
A22: DataLoc ((t . (intpos 4)),(- 1)) = DataLoc (m,(k + 1)) by A7, A8
.= intpos (m + (k + 1)) by SCMP_GCD:1 ;
X3: (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (intpos 6) = (Initialize (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t))) . (intpos 6) by SCMPDS_5:15;
X4: (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (intpos 4) = (Initialize (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t))) . (intpos 4) by SCMPDS_5:15;
X5: (Initialize (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t))) . GBP = (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . GBP by SCMPDS_5:15;
A23: ( t . (DataLoc ((t . (intpos 4)),(- 1))) > t . (DataLoc ((t . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (DataLoc ((t . (intpos 4)),(- 1))) = t . (DataLoc ((t . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (DataLoc ((t . (intpos 4)),0)) = t . (DataLoc ((t . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (intpos 6) = (t . (intpos 6)) - 1 & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (intpos 4) = (t . (intpos 4)) - 1 ) ) by A5, A6, A7, Lm8;
A24: ( t . (DataLoc ((t . (intpos 4)),(- 1))) <= t . (DataLoc ((t . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (DataLoc ((t . (intpos 4)),(- 1))) = t . (DataLoc ((t . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (DataLoc ((t . (intpos 4)),0)) = t . (DataLoc ((t . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (intpos 6) = 0 ) ) by A5, A6, A7, Lm8;
A25: DataLoc ((t . (intpos 4)),0) = intpos (m + (k + 2)) by A7, A8, SCMP_GCD:1;
A26: (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (intpos 4) >= 7 + ((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (intpos 6)) by A5, A6, A7, Lm8;
per cases ( t . (DataLoc ((t . (intpos 4)),(- 1))) > t . (DataLoc ((t . (intpos 4)),0)) or t . (DataLoc ((t . (intpos 4)),(- 1))) <= t . (DataLoc ((t . (intpos 4)),0)) ) ;
suppose A27: t . (DataLoc ((t . (intpos 4)),(- 1))) > t . (DataLoc ((t . (intpos 4)),0)) ; :: thesis: ( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,(k + 1) + 1 & ( for i being Element of NAT st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
now
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len f2 implies f2 . i = (IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,(Initialize (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t))))) . (intpos (m + i)) )
assume ( 1 <= i & i <= len f2 ) ; :: thesis: f2 . i = (IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,(Initialize (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t))))) . (intpos (m + i))
hence f2 . i = (IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,t)) . (intpos (m + i)) by A10, Def1
.= (IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,(Initialize (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t))))) . (intpos (m + i)) by A5, A6, A7, Lm15 ;
:: thesis: verum
end;
then A28: f2 is_FinSequence_on IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,(Initialize (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)))),m by Def1;
A29: k + 1 < k + 2 by XREAL_1:6;
consider h being FinSequence of INT such that
A30: len h = len f1 and
A31: for i being Element of NAT st 1 <= i & i <= len h holds
h . i = (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (intpos (m + i)) by Th2;
k + 1 > k by XREAL_1:29;
then A32: len h > k by A12, A30, XXREAL_0:2;
A33: now
let i be Element of NAT ; :: thesis: ( i <> k + 1 & i <> k + 2 & 1 <= i & i <= len f1 implies h . i = f1 . i )
assume that
A34: ( i <> k + 1 & i <> k + 2 ) and
A35: 1 <= i and
A36: i <= len f1 ; :: thesis: h . i = f1 . i
A37: ( m + i <> (t . (intpos 4)) - 1 & m + i <> t . (intpos 4) ) by A7, A8, A34;
m + i >= m + 1 by A35, XREAL_1:6;
then A38: m + i >= 7 by A21, XXREAL_0:2;
thus h . i = (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (intpos (m + i)) by A30, A31, A35, A36
.= t . (intpos (m + i)) by A5, A6, A7, A38, A37, Lm8
.= f1 . i by A9, A35, A36, Def1 ; :: thesis: verum
end;
now
let i, j be Element of NAT ; :: thesis: ( 1 <= i & i <= j & j <= k implies h . i <= h . j )
assume that
A40: 1 <= i and
A41: i <= j and
A42: j <= k ; :: thesis: h . i <= h . j
A43: j <= len f1 by A30, A32, A42, XXREAL_0:2;
then A44: i <= len f1 by A41, XXREAL_0:2;
A45: k < k + 1 by XREAL_1:29;
then A46: j < k + 1 by A42, XXREAL_0:2;
k + 1 < (k + 1) + 1 by XREAL_1:29;
then A47: k < (k + 1) + 1 by A45, XXREAL_0:2;
j >= 1 by A40, A41, XXREAL_0:2;
then A48: h . j = f1 . j by A33, A42, A45, A47, A43;
j < k + 2 by A42, A47, XXREAL_0:2;
then h . i = f1 . i by A33, A40, A41, A46, A44;
hence h . i <= h . j by A13, A40, A41, A46, A48, GRAPH_2:def 12; :: thesis: verum
end;
then A49: h is_non_decreasing_on 1,k by GRAPH_2:def 12;
A50: len f1 >= (k + 1) + 1 by A12, INT_1:7;
A51: 1 <= k + 1 by NAT_1:11;
then A52: 1 <= k + 2 by A29, XXREAL_0:2;
then A53: h . (k + 2) = t . (DataLoc ((t . (intpos 4)),(- 1))) by A25, A23, A27, A30, A31, A50;
then A54: h . (k + 2) = f1 . (k + 1) by A9, A12, A22, A51, Def1;
A55: (((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (intpos 4)) - ((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (intpos 6))) - 1 = m by A8, A23, A27;
A56: h . (k + 1) = t . (DataLoc ((t . (intpos 4)),0)) by A12, A22, A23, A27, A30, A31, NAT_1:11;
then h . (k + 1) = f1 . (k + 2) by A9, A25, A52, A50, Def1;
then A57: f1,h are_fiberwise_equipotent by A12, A30, A33, A51, A52, A50, A54, Th4;
A58: h is_FinSequence_on Initialize (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)),m
proof
let i be Element of NAT ; :: according to SCPISORT:def 1 :: thesis: ( 1 <= i & i <= len h implies h . i = (Initialize (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t))) . (intpos (m + i)) )
assume ( 1 <= i & i <= len h ) ; :: thesis: h . i = (Initialize (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t))) . (intpos (m + i))
then h . i = (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (intpos (m + i)) by A31;
hence h . i = (Initialize (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t))) . (intpos (m + i)) by SCMPDS_5:15; :: thesis: verum
end;
h,f2 are_fiberwise_equipotent by A4, A7, A11, A20, A26, A23, A27, A30, A55, A28, A32, A49, A58, X3, X4, X5;
hence f1,f2 are_fiberwise_equipotent by A57, CLASSES1:76; :: thesis: ( f2 is_non_decreasing_on 1,(k + 1) + 1 & ( for i being Element of NAT st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
A59: f2 is_non_decreasing_on 1,k + 1 by A4, A7, A11, A20, A26, A23, A27, A30, A55, A58, X3, X4, X5, A28, A32, A49;
now
let i, j be Element of NAT ; :: thesis: ( 1 <= i & i <= j & j <= (k + 1) + 1 implies f2 . b1 <= f2 . b2 )
assume that
A60: 1 <= i and
A61: i <= j and
A62: j <= (k + 1) + 1 ; :: thesis: f2 . b1 <= f2 . b2
per cases ( j <= k + 1 or j = (k + 1) + 1 ) by A62, NAT_1:8;
suppose j <= k + 1 ; :: thesis: f2 . b1 <= f2 . b2
hence f2 . i <= f2 . j by A59, A60, A61, GRAPH_2:def 12; :: thesis: verum
end;
suppose A63: j = (k + 1) + 1 ; :: thesis: f2 . b1 <= f2 . b2
hereby :: thesis: verum
per cases ( i = j or i <> j ) ;
suppose i = j ; :: thesis: f2 . i <= f2 . j
hence f2 . i <= f2 . j ; :: thesis: verum
end;
suppose i <> j ; :: thesis: f2 . i <= f2 . j
then i < j by A61, XXREAL_0:1;
then i <= k + 1 by A63, NAT_1:13;
then consider mm being Element of NAT such that
A64: 1 <= mm and
A65: mm <= k + 1 and
A66: f2 . i = h . mm by A4, A7, A11, A20, A26, A23, A27, A30, A55, A58, A28, A32, A49, A60, X3, X4, X5;
A67: f2 . j = h . (k + 2) by A4, A7, A11, A20, A26, A23, A27, A30, A55, A58, A28, A32, A49, A29, A50, A63, X3, X4, X5;
hereby :: thesis: verum
per cases ( mm = k + 1 or mm <> k + 1 ) ;
suppose mm = k + 1 ; :: thesis: f2 . i <= f2 . j
hence f2 . i <= f2 . j by A12, A22, A23, A24, A30, A31, A53, A64, A66, A67; :: thesis: verum
end;
suppose A68: mm <> k + 1 ; :: thesis: f2 . i <= f2 . j
mm < k + 2 by A29, A65, XXREAL_0:2;
then mm < len h by A30, A50, XXREAL_0:2;
then A69: h . mm = f1 . mm by A30, A33, A29, A64, A65, A68;
f2 . j = f1 . (k + 1) by A9, A12, A22, A51, A53, A67, Def1;
hence f2 . i <= f2 . j by A13, A64, A65, A66, A69, GRAPH_2:def 12; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
hence f2 is_non_decreasing_on 1,(k + 1) + 1 by GRAPH_2:def 12; :: thesis: ( ( for i being Element of NAT st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
hereby :: thesis: for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j )
let i be Element of NAT ; :: thesis: ( i > (k + 1) + 1 & i <= len f1 implies f2 . i = f1 . i )
assume that
A70: i > (k + 1) + 1 and
A71: i <= len f1 ; :: thesis: f2 . i = f1 . i
A72: k + 1 < (k + 1) + 1 by XREAL_1:29;
then A73: i > k + 1 by A70, XXREAL_0:2;
1 <= k + 1 by NAT_1:11;
then A74: 1 <= i by A73, XXREAL_0:2;
thus f2 . i = h . i by A4, A7, A11, A20, A26, A23, A27, A30, A55, A58, A28, A32, A49, A71, A73, X3, X4, X5
.= f1 . i by A33, A70, A71, A72, A74 ; :: thesis: verum
end;
hereby :: thesis: verum
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= (k + 1) + 1 implies ex j being Element of NAT st
( 1 <= b2 & b2 <= (k + 1) + 1 & f2 . j = f1 . b2 ) )
assume that
A75: 1 <= i and
A76: i <= (k + 1) + 1 ; :: thesis: ex j being Element of NAT st
( 1 <= b2 & b2 <= (k + 1) + 1 & f2 . j = f1 . b2 )
per cases ( i = (k + 1) + 1 or i <> (k + 1) + 1 ) ;
suppose A77: i = (k + 1) + 1 ; :: thesis: ex j being Element of NAT st
( 1 <= b2 & b2 <= (k + 1) + 1 & f2 . j = f1 . b2 )
take j = k + 1; :: thesis: ( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j )
thus 1 <= j by NAT_1:11; :: thesis: ( j <= (k + 1) + 1 & f2 . i = f1 . j )
thus j <= (k + 1) + 1 by NAT_1:11; :: thesis: f2 . i = f1 . j
thus f2 . i = f1 . j by A4, A7, A11, A20, A26, A23, A27, A30, A55, A58, A28, A32, A49, A29, A50, A54, A77, X3, X4, X5; :: thesis: verum
end;
suppose i <> (k + 1) + 1 ; :: thesis: ex j being Element of NAT st
( 1 <= b2 & b2 <= (k + 1) + 1 & f2 . j = f1 . b2 )
then i < (k + 1) + 1 by A76, XXREAL_0:1;
then i <= k + 1 by NAT_1:13;
then consider mm being Element of NAT such that
A78: 1 <= mm and
A79: mm <= k + 1 and
A80: f2 . i = h . mm by A4, A7, A11, A20, A26, A23, A27, A30, A55, A58, A28, A32, A49, A75, X3, X4, X5;
hereby :: thesis: verum
A81: k + 2 = (k + 1) + 1 ;
per cases ( mm = k + 1 or mm <> k + 1 ) ;
suppose A82: mm = k + 1 ; :: thesis: ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j )
take j = k + 2; :: thesis: ( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j )
thus 1 <= j by A81, NAT_1:11; :: thesis: ( j <= (k + 1) + 1 & f2 . i = f1 . j )
thus j <= (k + 1) + 1 ; :: thesis: f2 . i = f1 . j
thus f2 . i = f1 . j by A9, A25, A52, A50, A56, A80, A82, Def1; :: thesis: verum
end;
suppose A83: mm <> k + 1 ; :: thesis: ex mm being Element of NAT st
( 1 <= mm & mm <= (k + 1) + 1 & f2 . i = f1 . mm )
take mm = mm; :: thesis: ( 1 <= mm & mm <= (k + 1) + 1 & f2 . i = f1 . mm )
thus 1 <= mm by A78; :: thesis: ( mm <= (k + 1) + 1 & f2 . i = f1 . mm )
thus mm <= (k + 1) + 1 by A29, A79, XXREAL_0:2; :: thesis: f2 . i = f1 . mm
mm < k + 2 by A29, A79, XXREAL_0:2;
then mm < len f1 by A50, XXREAL_0:2;
hence f2 . i = f1 . mm by A33, A29, A78, A79, A80, A83; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
suppose A84: t . (DataLoc ((t . (intpos 4)),(- 1))) <= t . (DataLoc ((t . (intpos 4)),0)) ; :: thesis: ( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,(k + 1) + 1 & ( for i being Element of NAT st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
A85: now
let i be Nat; :: thesis: ( i >= 1 & i <= len f1 implies f1 . b1 = f2 . b1 )
assume that
A86: i >= 1 and
A87: i <= len f1 ; :: thesis: f1 . b1 = f2 . b1
A88: i in NAT by ORDINAL1:def 12;
then A89: f1 . i = t . (intpos (m + i)) by A9, A86, A87, Def1;
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (DataLoc (((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . GBP),6)) = 0 by A20, A24, A84, SCMP_GCD:1;
then B90: (Initialize (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t))) . (DataLoc (((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . GBP),6)) = 0 by SCMPDS_5:15;
m + i >= m + 1 by A86, XREAL_1:6;
then A91: m + i >= 7 by A21, XXREAL_0:2;
H2: (Initialize (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t))) . (intpos (m + i)) = (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (intpos (m + i)) by SCMPDS_5:15;
H3: (Initialize (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t))) . (DataLoc (((Initialize (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t))) . GBP),6)) <= 0 by B90, SCMPDS_5:15;
per cases ( m + i = (t . (intpos 4)) - 1 or m + i = t . (intpos 4) or ( m + i <> (t . (intpos 4)) - 1 & m + i <> t . (intpos 4) ) ) ;
suppose A93: m + i = (t . (intpos 4)) - 1 ; :: thesis: f1 . b1 = f2 . b1
hence f1 . i = (IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,(Initialize (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t))))) . (DataLoc ((t . (intpos 4)),(- 1))) by A7, A8, A22, A24, A84, A89, H2, H3, SCMPDS_8:23
.= (IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,(Initialize t))) . (DataLoc ((t . (intpos 4)),(- 1))) by A5, A6, A7, Lm15, T
.= f2 . i by A7, A8, A10, A11, A12, A22, A86, A93, Def1, T ;
:: thesis: verum
end;
suppose A94: m + i = t . (intpos 4) ; :: thesis: f1 . b1 = f2 . b1
hence f1 . i = (IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,(Initialize (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t))))) . (DataLoc ((t . (intpos 4)),0)) by A7, A8, A25, A24, A84, A89, H2, H3, SCMPDS_8:23
.= (IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,(Initialize t))) . (DataLoc ((t . (intpos 4)),0)) by A5, A6, A7, Lm15, T
.= f2 . i by A7, A8, A10, A11, A25, A86, A87, A94, Def1, T ;
:: thesis: verum
end;
suppose ( m + i <> (t . (intpos 4)) - 1 & m + i <> t . (intpos 4) ) ; :: thesis: f1 . b1 = f2 . b1
hence f1 . i = (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t)) . (intpos (m + i)) by A5, A6, A7, A91, A89, Lm8
.= (IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,(Initialize (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),Q,t))))) . (intpos (m + i)) by H2, H3, SCMPDS_8:23
.= (IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,(Initialize t))) . (intpos (m + i)) by A5, A6, A7, Lm15, T
.= f2 . i by A10, A11, A88, A86, A87, Def1, T ;
:: thesis: verum
end;
end;
end;
then A95: f1 = f2 by A11, FINSEQ_1:14;
thus f1,f2 are_fiberwise_equipotent by A11, A85, FINSEQ_1:14; :: thesis: ( f2 is_non_decreasing_on 1,(k + 1) + 1 & ( for i being Element of NAT st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
now
let i, j be Element of NAT ; :: thesis: ( 1 <= i & i <= j & j <= (k + 1) + 1 implies f1 . b1 <= f1 . b2 )
assume that
A96: 1 <= i and
A97: i <= j and
A98: j <= (k + 1) + 1 ; :: thesis: f1 . b1 <= f1 . b2
per cases ( j <= k + 1 or j = (k + 1) + 1 ) by A98, NAT_1:8;
suppose j <= k + 1 ; :: thesis: f1 . b1 <= f1 . b2
hence f1 . i <= f1 . j by A13, A96, A97, GRAPH_2:def 12; :: thesis: verum
end;
suppose A99: j = (k + 1) + 1 ; :: thesis: f1 . b1 <= f1 . b2
hereby :: thesis: verum
per cases ( i = j or i <> j ) ;
suppose i = j ; :: thesis: f1 . i <= f1 . j
hence f1 . i <= f1 . j ; :: thesis: verum
end;
suppose i <> j ; :: thesis: f1 . i <= f1 . j
then i < j by A97, XXREAL_0:1;
then i <= k + 1 by A99, NAT_1:13;
then A100: f1 . i <= f1 . (k + 1) by A13, A96, GRAPH_2:def 12;
1 <= k + 1 by NAT_1:11;
then A101: f1 . (k + 1) = t . (DataLoc ((t . (intpos 4)),(- 1))) by A9, A12, A22, Def1;
( 1 <= (k + 1) + 1 & j <= len f1 ) by A12, A99, INT_1:7, NAT_1:11;
then f1 . j = t . (DataLoc ((t . (intpos 4)),0)) by A9, A25, A99, Def1;
hence f1 . i <= f1 . j by A84, A100, A101, XXREAL_0:2; :: thesis: verum
end;
end;
end;
end;
end;
end;
hence f2 is_non_decreasing_on 1,(k + 1) + 1 by A95, GRAPH_2:def 12; :: thesis: ( ( for i being Element of NAT st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
thus for i being Element of NAT st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i by A11, A85, FINSEQ_1:14; :: thesis: for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j )
thus for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) by A95; :: thesis: verum
end;
end;
end;
end;
A102: S1[ 0 ]
proof
let t be 0 -started State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS
for f1, f2 being FinSequence of INT st t . (intpos 4) >= 7 + (t . (intpos 6)) & t . GBP = 0 & 0 = t . (intpos 6) & m = ((t . (intpos 4)) - (t . (intpos 6))) - 1 & f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,t),m & len f1 = len f2 & len f1 > 0 & f1 is_non_decreasing_on 1, 0 holds
( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,0 + 1 & ( for i being Element of NAT st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= 0 + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j ) ) )
let Q be Instruction-Sequence of SCMPDS; :: thesis: for f1, f2 being FinSequence of INT st t . (intpos 4) >= 7 + (t . (intpos 6)) & t . GBP = 0 & 0 = t . (intpos 6) & m = ((t . (intpos 4)) - (t . (intpos 6))) - 1 & f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,t),m & len f1 = len f2 & len f1 > 0 & f1 is_non_decreasing_on 1, 0 holds
( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,0 + 1 & ( for i being Element of NAT st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= 0 + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j ) ) )
let f1, f2 be FinSequence of INT ; :: thesis: ( t . (intpos 4) >= 7 + (t . (intpos 6)) & t . GBP = 0 & 0 = t . (intpos 6) & m = ((t . (intpos 4)) - (t . (intpos 6))) - 1 & f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,t),m & len f1 = len f2 & len f1 > 0 & f1 is_non_decreasing_on 1, 0 implies ( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,0 + 1 & ( for i being Element of NAT st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= 0 + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j ) ) ) )
T: Initialize t = t by MEMSTR_0:44;
assume that
t . (intpos 4) >= 7 + (t . (intpos 6)) and
A103: ( t . GBP = 0 & 0 = t . (intpos 6) ) and
m = ((t . (intpos 4)) - (t . (intpos 6))) - 1 and
A104: f1 is_FinSequence_on t,m and
A105: f2 is_FinSequence_on IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,t),m and
A106: len f1 = len f2 and
len f1 > 0 and
f1 is_non_decreasing_on 1, 0 ; :: thesis: ( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,0 + 1 & ( for i being Element of NAT st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= 0 + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j ) ) )
A107: t . (DataLoc ((t . GBP),6)) = 0 by A103, SCMP_GCD:1;
A108: now
let i be Nat; :: thesis: ( 1 <= i & i <= len f1 implies f1 . i = f2 . i )
assume A109: ( 1 <= i & i <= len f1 ) ; :: thesis: f1 . i = f2 . i
A110: i in NAT by ORDINAL1:def 12;
hence f1 . i = t . (intpos (m + i)) by A104, A109, Def1
.= (IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,(Initialize t))) . (intpos (m + i)) by A107, T, SCMPDS_8:23
.= f2 . i by A105, A106, A110, A109, Def1, T ;
:: thesis: verum
end;
hence f1,f2 are_fiberwise_equipotent by A106, FINSEQ_1:14; :: thesis: ( f2 is_non_decreasing_on 1,0 + 1 & ( for i being Element of NAT st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= 0 + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j ) ) )
thus f2 is_non_decreasing_on 1,0 + 1 by GRAPH_2:63; :: thesis: ( ( for i being Element of NAT st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= 0 + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j ) ) )
thus for i being Element of NAT st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i by A108; :: thesis: for i being Element of NAT st 1 <= i & i <= 0 + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j )
f1 = f2 by A106, A108, FINSEQ_1:14;
hence for i being Element of NAT st 1 <= i & i <= 0 + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j ) ; :: thesis: verum
end;
A111: for k being Element of NAT holds S1[k] from NAT_1:sch 1(A102, A3);
 assume ( len f = len g & len f > n & f is_non_decreasing_on 1,n ) ; :: thesis: ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n + 1 & ( for i being Element of NAT st i > n + 1 & i <= len f holds
f . i = g . i ) & ( for i being Element of NAT st 1 <= i & i <= n + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= n + 1 & g . i = f . j ) ) )
hence ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n + 1 & ( for i being Element of NAT st i > n + 1 & i <= len f holds
f . i = g . i ) & ( for i being Element of NAT st 1 <= i & i <= n + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= n + 1 & g . i = f . j ) ) ) by A1, A2, A111; :: thesis: verum