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 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 Nat st i > k + 1 & i <= len f holds
f . i = g . i ) & ( for i being Nat st 1 <= i & i <= k + 1 holds
ex j being 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 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 Nat st i > k + 1 & i <= len f holds
f . i = g . i ) & ( for i being Nat st 1 <= i & i <= k + 1 holds
ex j being Nat st
( 1 <= j & j <= k + 1 & g . i = f . j ) ) )
let f, g be FinSequence of INT ; :: thesis: for k0, k being 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 Nat st i > k + 1 & i <= len f holds
f . i = g . i ) & ( for i being Nat st 1 <= i & i <= k + 1 holds
ex j being Nat st
( 1 <= j & j <= k + 1 & g . i = f . j ) ) )
let m, n be 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 Nat st i > n + 1 & i <= len f holds
f . i = g . i ) & ( for i being Nat st 1 <= i & i <= n + 1 holds
ex j being 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 Nat st i > n + 1 & i <= len f holds
f . i = g . i ) & ( for i being Nat st 1 <= i & i <= n + 1 holds
ex j being Nat st
( 1 <= j & j <= n + 1 & g . i = f . j ) ) ) )
defpred S1[ 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 Nat st i > $1 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Nat st 1 <= i & i <= $1 + 1 holds
ex j being 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 Nat st i > n + 1 & i <= len f holds
f . i = g . i ) & ( for i being Nat st 1 <= i & i <= n + 1 holds
ex j being Nat st
( 1 <= j & j <= n + 1 & g . i = f . j ) ) ) )
A3: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be 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 Nat st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Nat st 1 <= i & i <= (k + 1) + 1 holds
ex j being 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 Nat st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Nat st 1 <= i & i <= (k + 1) + 1 holds
ex j being 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 Nat st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Nat st 1 <= i & i <= (k + 1) + 1 holds
ex j being Nat st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) ) )
A5: Initialize t = t by MEMSTR_0:44;
assume that
A6: t . (intpos 4) >= 7 + (t . (intpos 6)) and
A7: t . GBP = 0 and
A8: k + 1 = t . (intpos 6) and
A9: m = ((t . (intpos 4)) - (t . (intpos 6))) - 1 and
A10: f1 is_FinSequence_on t,m and
A11: 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
A12: len f1 = len f2 and
A13: len f1 > k + 1 and
A14: 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 Nat st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Nat st 1 <= i & i <= (k + 1) + 1 holds
ex j being 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);
A15: (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 A6, A7, A8, Lm6;
(m + 1) + (k + 1) >= 7 + (t . (intpos 6)) by A6, A8, A9;
then A16: m + 1 >= 7 by A8, XREAL_1:6;
A17: DataLoc ((t . (intpos 4)),(- 1)) = DataLoc (m,(k + 1)) by A8, A9
.= intpos (m + (k + 1)) by SCMP_GCD:1 ;
A18: (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;
A19: (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;
A20: (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;
A21: ( 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 A6, A7, A8, Lm7;
A22: ( 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 A6, A7, A8, Lm7;
A23: DataLoc ((t . (intpos 4)),0) = intpos (m + (k + 2)) by A8, A9, SCMP_GCD:1;
A24: (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 A6, A7, A8, Lm7;
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 A25: 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 Nat st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Nat st 1 <= i & i <= (k + 1) + 1 holds
ex j being Nat st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
now :: thesis: for i being Nat st 1 <= i & i <= len f2 holds
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))
let i be 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 A11
.= (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 A6, A7, A8, Lm14 ;
:: thesis: verum
end;
then A26: 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 ;
A27: k + 1 < k + 2 by XREAL_1:6;
consider h being FinSequence of INT such that
A28: len h = len f1 and
A29: for i being 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 Th1;
k + 1 > k by XREAL_1:29;
then A30: len h > k by A13, A28, XXREAL_0:2;
A31: now :: thesis: for i being Nat st i <> k + 1 & i <> k + 2 & 1 <= i & i <= len f1 holds
h . i = f1 . i
let i be Nat; :: thesis: ( i <> k + 1 & i <> k + 2 & 1 <= i & i <= len f1 implies h . i = f1 . i )
assume that
A32: ( i <> k + 1 & i <> k + 2 ) and
A33: 1 <= i and
A34: i <= len f1 ; :: thesis: h . i = f1 . i
A35: ( m + i <> (t . (intpos 4)) - 1 & m + i <> t . (intpos 4) ) by A8, A9, A32;
m + i >= m + 1 by A33, XREAL_1:6;
then A36: m + i >= 7 by A16, 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 A28, A29, A33, A34
.= t . (intpos (m + i)) by A6, A7, A8, A36, A35, Lm7
.= f1 . i by A10, A33, A34 ; :: thesis: verum
end;
now :: thesis: for i, j being Nat st 1 <= i & i <= j & j <= k holds
h . i <= h . j
let i, j be Nat; :: thesis: ( 1 <= i & i <= j & j <= k implies h . i <= h . j )
assume that
A37: 1 <= i and
A38: i <= j and
A39: j <= k ; :: thesis: h . i <= h . j
A40: j <= len f1 by A28, A30, A39, XXREAL_0:2;
then A41: i <= len f1 by A38, XXREAL_0:2;
A42: k < k + 1 by XREAL_1:29;
then A43: j < k + 1 by A39, XXREAL_0:2;
k + 1 < (k + 1) + 1 by XREAL_1:29;
then A44: k < (k + 1) + 1 by A42, XXREAL_0:2;
j >= 1 by A37, A38, XXREAL_0:2;
then A45: h . j = f1 . j by A31, A39, A42, A44, A40;
j < k + 2 by A39, A44, XXREAL_0:2;
then h . i = f1 . i by A31, A37, A38, A43, A41;
hence h . i <= h . j by A14, A37, A38, A43, A45, FINSEQ_6:def 9; :: thesis: verum
end;
then A46: h is_non_decreasing_on 1,k by FINSEQ_6:def 9;
A47: len f1 >= (k + 1) + 1 by A13, INT_1:7;
A48: 1 <= k + 1 by NAT_1:11;
then A49: 1 <= k + 2 by A27, XXREAL_0:2;
then A50: h . (k + 2) = t . (DataLoc ((t . (intpos 4)),(- 1))) by A23, A21, A25, A28, A29, A47;
then A51: h . (k + 2) = f1 . (k + 1) by A10, A13, A17, A48;
A52: (((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 A9, A21, A25;
A53: h . (k + 1) = t . (DataLoc ((t . (intpos 4)),0)) by A13, A17, A21, A25, A28, A29, NAT_1:11;
then h . (k + 1) = f1 . (k + 2) by A10, A23, A49, A47;
then A54: f1,h are_fiberwise_equipotent by A13, A28, A31, A48, A49, A47, A51, Th3;
A55: 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 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 A29;
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, A8, A12, A15, A24, A21, A25, A28, A52, A26, A30, A46, A55, A18, A19, A20;
hence f1,f2 are_fiberwise_equipotent by A54, CLASSES1:76; :: thesis: ( f2 is_non_decreasing_on 1,(k + 1) + 1 & ( for i being Nat st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Nat st 1 <= i & i <= (k + 1) + 1 holds
ex j being Nat st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
A56: f2 is_non_decreasing_on 1,k + 1 by A4, A8, A12, A15, A24, A21, A25, A28, A52, A55, A18, A19, A20, A26, A30, A46;
now :: thesis: for i, j being Nat st 1 <= i & i <= j & j <= (k + 1) + 1 holds
f2 . i <= f2 . j
let i, j be Nat; :: thesis: ( 1 <= i & i <= j & j <= (k + 1) + 1 implies f2 . b1 <= f2 . b2 )
assume that
A57: 1 <= i and
A58: i <= j and
A59: j <= (k + 1) + 1 ; :: thesis: f2 . b1 <= f2 . b2
per cases ( j <= k + 1 or j = (k + 1) + 1 ) by A59, NAT_1:8;
suppose j <= k + 1 ; :: thesis: f2 . b1 <= f2 . b2
hence f2 . i <= f2 . j by A56, A57, A58, FINSEQ_6:def 9; :: thesis: verum
end;
suppose A60: 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 A58, XXREAL_0:1;
then i <= k + 1 by A60, NAT_1:13;
then consider mm being Nat such that
A61: 1 <= mm and
A62: mm <= k + 1 and
A63: f2 . i = h . mm by A4, A8, A12, A15, A24, A21, A25, A28, A52, A55, A26, A30, A46, A57, A18, A19, A20;
A64: f2 . j = h . (k + 2) by A4, A8, A12, A15, A24, A21, A25, A28, A52, A55, A26, A30, A46, A27, A47, A60, A18, A19, A20;
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 A13, A17, A21, A22, A28, A29, A50, A61, A63, A64; :: thesis: verum
end;
suppose A65: mm <> k + 1 ; :: thesis: f2 . i <= f2 . j
mm < k + 2 by A27, A62, XXREAL_0:2;
then mm < len h by A28, A47, XXREAL_0:2;
then A66: h . mm = f1 . mm by A28, A31, A27, A61, A62, A65;
f2 . j = f1 . (k + 1) by A10, A13, A17, A48, A50, A64;
hence f2 . i <= f2 . j by A14, A61, A62, A63, A66, FINSEQ_6:def 9; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
hence f2 is_non_decreasing_on 1,(k + 1) + 1 by FINSEQ_6:def 9; :: thesis: ( ( for i being Nat st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Nat st 1 <= i & i <= (k + 1) + 1 holds
ex j being Nat st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
hereby :: thesis: for i being Nat st 1 <= i & i <= (k + 1) + 1 holds
ex j being Nat st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j )
let i be Nat; :: thesis: ( i > (k + 1) + 1 & i <= len f1 implies f2 . i = f1 . i )
assume that
A67: i > (k + 1) + 1 and
A68: i <= len f1 ; :: thesis: f2 . i = f1 . i
A69: k + 1 < (k + 1) + 1 by XREAL_1:29;
then A70: i > k + 1 by A67, XXREAL_0:2;
1 <= k + 1 by NAT_1:11;
then A71: 1 <= i by A70, XXREAL_0:2;
thus f2 . i = h . i by A4, A8, A12, A15, A24, A21, A25, A28, A52, A55, A26, A30, A46, A68, A70, A18, A19, A20
.= f1 . i by A31, A67, A68, A69, A71 ; :: thesis: verum
end;
hereby :: thesis: verum
let i be Nat; :: thesis: ( 1 <= i & i <= (k + 1) + 1 implies ex j being Nat st
( 1 <= b2 & b2 <= (k + 1) + 1 & f2 . j = f1 . b2 ) )
assume that
A72: 1 <= i and
A73: i <= (k + 1) + 1 ; :: thesis: ex j being Nat st
( 1 <= b2 & b2 <= (k + 1) + 1 & f2 . j = f1 . b2 )
per cases ( i = (k + 1) + 1 or i <> (k + 1) + 1 ) ;
suppose A74: i = (k + 1) + 1 ; :: thesis: ex j being Nat st
( 1 <= b2 & b2 <= (k + 1) + 1 & f2 . j = f1 . b2 )
reconsider j = k + 1 as Nat ;
take j = j; :: 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, A8, A12, A15, A24, A21, A25, A28, A52, A55, A26, A30, A46, A27, A47, A51, A74, A18, A19, A20; :: thesis: verum
end;
suppose i <> (k + 1) + 1 ; :: thesis: ex j being Nat st
( 1 <= b2 & b2 <= (k + 1) + 1 & f2 . j = f1 . b2 )
then i < (k + 1) + 1 by A73, XXREAL_0:1;
then i <= k + 1 by NAT_1:13;
then consider mm being Nat such that
A75: 1 <= mm and
A76: mm <= k + 1 and
A77: f2 . i = h . mm by A4, A8, A12, A15, A24, A21, A25, A28, A52, A55, A26, A30, A46, A72, A18, A19, A20;
hereby :: thesis: verum
A78: k + 2 = (k + 1) + 1 ;
per cases ( mm = k + 1 or mm <> k + 1 ) ;
suppose A79: mm = k + 1 ; :: thesis: ex j being Nat st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j )
reconsider j = k + 2 as Nat ;
take j = j; :: thesis: ( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j )
thus 1 <= j by A78, 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 A10, A23, A49, A47, A53, A77, A79; :: thesis: verum
end;
suppose A80: mm <> k + 1 ; :: thesis: ex mm being Nat st
( 1 <= mm & mm <= (k + 1) + 1 & f2 . i = f1 . mm )
reconsider mm = mm as Nat ;
take mm = mm; :: thesis: ( 1 <= mm & mm <= (k + 1) + 1 & f2 . i = f1 . mm )
thus 1 <= mm by A75; :: thesis: ( mm <= (k + 1) + 1 & f2 . i = f1 . mm )
thus mm <= (k + 1) + 1 by A27, A76, XXREAL_0:2; :: thesis: f2 . i = f1 . mm
mm < k + 2 by A27, A76, XXREAL_0:2;
then mm < len f1 by A47, XXREAL_0:2;
hence f2 . i = f1 . mm by A31, A27, A75, A76, A77, A80; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
suppose A81: 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 Nat st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Nat st 1 <= i & i <= (k + 1) + 1 holds
ex j being Nat st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
A82: now :: thesis: for i being Nat st i >= 1 & i <= len f1 holds
f1 . i = f2 . i
let i be Nat; :: thesis: ( i >= 1 & i <= len f1 implies f1 . b1 = f2 . b1 )
assume that
A83: i >= 1 and
A84: i <= len f1 ; :: thesis: f1 . b1 = f2 . b1
A85: f1 . i = t . (intpos (m + i)) by A10, A83, A84;
(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 A15, A22, A81, SCMP_GCD:1;
then A86: (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 A83, XREAL_1:6;
then A87: m + i >= 7 by A16, XXREAL_0:2;
A88: (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;
A89: (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 A86, 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 A90: 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 A8, A9, A17, A22, A81, A85, A88, A89, 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 A6, A7, A8, Lm14, A5
.= f2 . i by A8, A9, A11, A12, A13, A17, A83, A90, A5 ;
:: thesis: verum
end;
suppose A91: 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 A8, A9, A23, A22, A81, A85, A88, A89, 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 A6, A7, A8, Lm14, A5
.= f2 . i by A8, A9, A11, A12, A23, A83, A84, A91, A5 ;
:: 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 A6, A7, A8, A87, A85, Lm7
.= (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 A88, A89, 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 A6, A7, A8, Lm14, A5
.= f2 . i by A11, A12, A83, A84, A5 ;
:: thesis: verum
end;
end;
end;
then A92: f1 = f2 by A12, FINSEQ_1:14;
thus f1,f2 are_fiberwise_equipotent by A12, A82, FINSEQ_1:14; :: thesis: ( f2 is_non_decreasing_on 1,(k + 1) + 1 & ( for i being Nat st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Nat st 1 <= i & i <= (k + 1) + 1 holds
ex j being Nat st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
now :: thesis: for i, j being Nat st 1 <= i & i <= j & j <= (k + 1) + 1 holds
f1 . i <= f1 . j
let i, j be Nat; :: thesis: ( 1 <= i & i <= j & j <= (k + 1) + 1 implies f1 . b1 <= f1 . b2 )
assume that
A93: 1 <= i and
A94: i <= j and
A95: j <= (k + 1) + 1 ; :: thesis: f1 . b1 <= f1 . b2
per cases ( j <= k + 1 or j = (k + 1) + 1 ) by A95, NAT_1:8;
suppose j <= k + 1 ; :: thesis: f1 . b1 <= f1 . b2
hence f1 . i <= f1 . j by A14, A93, A94, FINSEQ_6:def 9; :: thesis: verum
end;
suppose A96: 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 A94, XXREAL_0:1;
then i <= k + 1 by A96, NAT_1:13;
then A97: f1 . i <= f1 . (k + 1) by A14, A93, FINSEQ_6:def 9;
1 <= k + 1 by NAT_1:11;
then A98: f1 . (k + 1) = t . (DataLoc ((t . (intpos 4)),(- 1))) by A10, A13, A17;
( 1 <= (k + 1) + 1 & j <= len f1 ) by A13, A96, INT_1:7, NAT_1:11;
then f1 . j = t . (DataLoc ((t . (intpos 4)),0)) by A10, A23, A96;
hence f1 . i <= f1 . j by A81, A97, A98, XXREAL_0:2; :: thesis: verum
end;
end;
end;
end;
end;
end;
hence f2 is_non_decreasing_on 1,(k + 1) + 1 by A92, FINSEQ_6:def 9; :: thesis: ( ( for i being Nat st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Nat st 1 <= i & i <= (k + 1) + 1 holds
ex j being Nat st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
thus for i being Nat st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i by A12, A82, FINSEQ_1:14; :: thesis: for i being Nat st 1 <= i & i <= (k + 1) + 1 holds
ex j being Nat st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j )
thus for i being Nat st 1 <= i & i <= (k + 1) + 1 holds
ex j being Nat st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) by A92; :: thesis: verum
end;
end;
end;
end;
A99: 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 Nat st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Nat st 1 <= i & i <= 0 + 1 holds
ex j being 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 Nat st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Nat st 1 <= i & i <= 0 + 1 holds
ex j being 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 Nat st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Nat st 1 <= i & i <= 0 + 1 holds
ex j being Nat st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j ) ) ) )
A100: Initialize t = t by MEMSTR_0:44;
assume that
t . (intpos 4) >= 7 + (t . (intpos 6)) and
A101: ( t . GBP = 0 & 0 = t . (intpos 6) ) and
m = ((t . (intpos 4)) - (t . (intpos 6))) - 1 and
A102: f1 is_FinSequence_on t,m and
A103: 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
A104: 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 Nat st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Nat st 1 <= i & i <= 0 + 1 holds
ex j being Nat st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j ) ) )
A105: t . (DataLoc ((t . GBP),6)) = 0 by A101, SCMP_GCD:1;
A106: now :: thesis: for i being Nat st 1 <= i & i <= len f1 holds
f1 . i = f2 . i
let i be Nat; :: thesis: ( 1 <= i & i <= len f1 implies f1 . i = f2 . i )
assume A107: ( 1 <= i & i <= len f1 ) ; :: thesis: f1 . i = f2 . i
thus f1 . i = t . (intpos (m + i)) by A102, A107
.= (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 A105, A100, SCMPDS_8:23
.= f2 . i by A103, A104, A107, A100 ; :: thesis: verum
end;
hence f1,f2 are_fiberwise_equipotent by A104, FINSEQ_1:14; :: thesis: ( f2 is_non_decreasing_on 1,0 + 1 & ( for i being Nat st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Nat st 1 <= i & i <= 0 + 1 holds
ex j being Nat st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j ) ) )
thus f2 is_non_decreasing_on 1,0 + 1 by FINSEQ_6:165; :: thesis: ( ( for i being Nat st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Nat st 1 <= i & i <= 0 + 1 holds
ex j being Nat st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j ) ) )
thus for i being Nat st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i by A106; :: thesis: for i being Nat st 1 <= i & i <= 0 + 1 holds
ex j being Nat st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j )
f1 = f2 by A104, A106, FINSEQ_1:14;
hence for i being Nat st 1 <= i & i <= 0 + 1 holds
ex j being Nat st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j ) ; :: thesis: verum
end;
A108: for k being Nat holds S1[k] from NAT_1:sch 2(A99, 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 Nat st i > n + 1 & i <= len f holds
f . i = g . i ) & ( for i being Nat st 1 <= i & i <= n + 1 holds
ex j being 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 Nat st i > n + 1 & i <= len f holds
f . i = g . i ) & ( for i being Nat st 1 <= i & i <= n + 1 holds
ex j being Nat st
( 1 <= j & j <= n + 1 & g . i = f . j ) ) ) by A1, A2, A108; :: thesis: verum