let P be Instruction-Sequence of SCMPDS; 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; 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 ; 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; ( 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 )
; ( 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 )
; ( 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 for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A4:
S1[
k]
;
S1[k + 1]thus
S1[
k + 1]
verumproof
let t be
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 & 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;
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 ;
( 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
;
( 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))
;
( 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 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;
( 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 )
;
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
;
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 for i being Nat st i <> k + 1 & i <> k + 2 & 1 <= i & i <= len f1 holds
h . i = f1 . ilet i be
Nat;
( 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
;
h . i = f1 . iA35:
(
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
;
verum end; now for i, j being Nat st 1 <= i & i <= j & j <= k holds
h . i <= h . jlet i,
j be
Nat;
( 1 <= i & i <= j & j <= k implies h . i <= h . j )assume that A37:
1
<= i
and A38:
i <= j
and A39:
j <= k
;
h . i <= h . jA40:
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;
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;
SCPISORT:def 1 ( 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 )
;
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;
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;
( 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 for i, j being Nat st 1 <= i & i <= j & j <= (k + 1) + 1 holds
f2 . i <= f2 . jlet i,
j be
Nat;
( 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
;
f2 . b1 <= f2 . b2per cases
( j <= k + 1 or j = (k + 1) + 1 )
by A59, NAT_1:8;
suppose A60:
j = (k + 1) + 1
;
f2 . b1 <= f2 . b2hereby verum
per cases
( i = j or i <> j )
;
suppose
i <> j
;
f2 . i <= f2 . jthen
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 verum
per cases
( mm = k + 1 or mm <> k + 1 )
;
suppose A65:
mm <> k + 1
;
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;
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;
( ( 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 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;
( i > (k + 1) + 1 & i <= len f1 implies f2 . i = f1 . i )assume that A67:
i > (k + 1) + 1
and A68:
i <= len f1
;
f2 . i = f1 . iA69:
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
;
verum
end; hereby verum
let i be
Nat;
( 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
;
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
;
ex j being Nat st
( 1 <= b2 & b2 <= (k + 1) + 1 & f2 . j = f1 . b2 )reconsider j =
k + 1 as
Nat ;
take j =
j;
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j )thus
1
<= j
by NAT_1:11;
( j <= (k + 1) + 1 & f2 . i = f1 . j )thus
j <= (k + 1) + 1
by NAT_1:11;
f2 . i = f1 . jthus
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;
verum end; suppose
i <> (k + 1) + 1
;
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 verum
A78:
k + 2
= (k + 1) + 1
;
per cases
( mm = k + 1 or mm <> k + 1 )
;
suppose A80:
mm <> k + 1
;
ex mm being Nat st
( 1 <= mm & mm <= (k + 1) + 1 & f2 . i = f1 . mm )reconsider mm =
mm as
Nat ;
take mm =
mm;
( 1 <= mm & mm <= (k + 1) + 1 & f2 . i = f1 . mm )thus
1
<= mm
by A75;
( mm <= (k + 1) + 1 & f2 . i = f1 . mm )thus
mm <= (k + 1) + 1
by A27, A76, XXREAL_0:2;
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;
verum end; end;
end; end; end;
end; end; suppose A81:
t . (DataLoc ((t . (intpos 4)),(- 1))) <= t . (DataLoc ((t . (intpos 4)),0))
;
( 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 for i being Nat st i >= 1 & i <= len f1 holds
f1 . i = f2 . ilet i be
Nat;
( i >= 1 & i <= len f1 implies f1 . b1 = f2 . b1 )assume that A83:
i >= 1
and A84:
i <= len f1
;
f1 . b1 = f2 . b1A85:
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
;
f1 . b1 = f2 . b1hence 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
;
verum end; suppose A91:
m + i = t . (intpos 4)
;
f1 . b1 = f2 . b1hence 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
;
verum end; suppose
(
m + i <> (t . (intpos 4)) - 1 &
m + i <> t . (intpos 4) )
;
f1 . b1 = f2 . b1hence 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
;
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;
( 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 for i, j being Nat st 1 <= i & i <= j & j <= (k + 1) + 1 holds
f1 . i <= f1 . jlet i,
j be
Nat;
( 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
;
f1 . b1 <= f1 . b2per cases
( j <= k + 1 or j = (k + 1) + 1 )
by A95, NAT_1:8;
suppose A96:
j = (k + 1) + 1
;
f1 . b1 <= f1 . b2hereby verum
per cases
( i = j or i <> j )
;
suppose
i <> j
;
f1 . i <= f1 . jthen
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;
verum end; end;
end; end; end; end; hence
f2 is_non_decreasing_on 1,
(k + 1) + 1
by A92, FINSEQ_6:def 9;
( ( 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;
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;
verum end; end;
end; end;
A99:
S1[ 0 ]
proof
let t be
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 & 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;
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 ;
( 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
;
( 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 for i being Nat st 1 <= i & i <= len f1 holds
f1 . i = f2 . ilet i be
Nat;
( 1 <= i & i <= len f1 implies f1 . i = f2 . i )assume A107:
( 1
<= i &
i <= len f1 )
;
f1 . i = f2 . ithus 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
;
verum end;
hence
f1,
f2 are_fiberwise_equipotent
by A104, FINSEQ_1:14;
( 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;
( ( 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;
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 )
;
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 )
; ( 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; verum