set a = GBP ;
let s be 0 -started State of SCMPDS; for f, g being FinSequence of INT
for p0, n being Element of NAT st p0 >= 6 & len f = n & len g = n & f is_FinSequence_on s,p0 & g is_FinSequence_on IExec ((insert-sort (n,(p0 + 1))),s),p0 holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
let f, g be FinSequence of INT ; for p0, n being Element of NAT st p0 >= 6 & len f = n & len g = n & f is_FinSequence_on s,p0 & g is_FinSequence_on IExec ((insert-sort (n,(p0 + 1))),s),p0 holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
let p0, n be Element of NAT ; ( p0 >= 6 & len f = n & len g = n & f is_FinSequence_on s,p0 & g is_FinSequence_on IExec ((insert-sort (n,(p0 + 1))),s),p0 implies ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n ) )
assume that
A1:
p0 >= 6
and
A2:
( len f = n & len g = n )
and
A3:
f is_FinSequence_on s,p0
and
A4:
g is_FinSequence_on IExec ((insert-sort (n,(p0 + 1))),s),p0
; ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
A5:
p0 + 1 >= 6 + 1
by A1, XREAL_1:8;
set i1 = GBP := 0;
set i2 = (GBP,1) := 0;
set i3 = (GBP,2) := (n - 1);
set i4 = (GBP,3) := (p0 + 1);
set t0 = Initialize s;
set I4 = (((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1));
set t1 = IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s);
set t2 = IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s);
set t3 = IExec (((GBP := 0) ';' ((GBP,1) := 0)),s);
set t4 = Exec ((GBP := 0),(Initialize s));
A6:
(Exec ((GBP := 0),(Initialize s))) . GBP = 0
by SCMPDS_2:57;
then A7:
DataLoc (((Exec ((GBP := 0),(Initialize s))) . GBP),1) = intpos (0 + 1)
by SCMP_GCD:5;
A8: (IExec (((GBP := 0) ';' ((GBP,1) := 0)),s)) . GBP =
(Exec (((GBP,1) := 0),(Exec ((GBP := 0),(Initialize s))))) . GBP
by SCMPDS_5:47
.=
0
by A6, A7, AMI_3:52, SCMPDS_2:58
;
then A9:
DataLoc (((IExec (((GBP := 0) ';' ((GBP,1) := 0)),s)) . GBP),2) = intpos (0 + 2)
by SCMP_GCD:5;
A10: (IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)) . GBP =
(Exec (((GBP,2) := (n - 1)),(IExec (((GBP := 0) ';' ((GBP,1) := 0)),s)))) . GBP
by SCMPDS_5:46
.=
0
by A8, A9, AMI_3:52, SCMPDS_2:58
;
then A11:
DataLoc (((IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)) . GBP),3) = intpos (0 + 3)
by SCMP_GCD:5;
A13:
now let i be
Element of
NAT ;
( i > 3 implies (IExec (((GBP := 0) ';' ((GBP,1) := 0)),s)) . (intpos i) = s . (intpos i) )assume A14:
i > 3
;
(IExec (((GBP := 0) ';' ((GBP,1) := 0)),s)) . (intpos i) = s . (intpos i)then A15:
i > 1
by XXREAL_0:2;
thus (IExec (((GBP := 0) ';' ((GBP,1) := 0)),s)) . (intpos i) =
(Exec (((GBP,1) := 0),(Exec ((GBP := 0),(Initialize s))))) . (intpos i)
by SCMPDS_5:47
.=
(Exec ((GBP := 0),(Initialize s))) . (intpos i)
by A7, A15, AMI_3:52, SCMPDS_2:58
.=
s . (intpos i)
by A12, A14
;
verum end;
A16:
now let i be
Element of
NAT ;
( i > 3 implies (IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)) . (intpos i) = s . (intpos i) )assume A17:
i > 3
;
(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)) . (intpos i) = s . (intpos i)then A18:
i > 2
by XXREAL_0:2;
thus (IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)) . (intpos i) =
(Exec (((GBP,2) := (n - 1)),(IExec (((GBP := 0) ';' ((GBP,1) := 0)),s)))) . (intpos i)
by SCMPDS_5:46
.=
(IExec (((GBP := 0) ';' ((GBP,1) := 0)),s)) . (intpos i)
by A9, A18, AMI_3:52, SCMPDS_2:58
.=
s . (intpos i)
by A13, A17
;
verum end;
now let i be
Element of
NAT ;
( 1 <= i & i <= len f implies (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s))) . (intpos (p0 + i)) = f . i )assume that A19:
1
<= i
and A20:
i <= len f
;
(Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s))) . (intpos (p0 + i)) = f . iset pi =
p0 + i;
p0 + i >= p0 + 1
by A19, XREAL_1:8;
then
p0 + i >= 7
by A5, XXREAL_0:2;
then A21:
p0 + i > 3
by XXREAL_0:2;
thus (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s))) . (intpos (p0 + i)) =
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s)) . (intpos (p0 + i))
by SCMPDS_5:40
.=
(Exec (((GBP,3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)))) . (intpos (p0 + i))
by SCMPDS_5:46
.=
(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)) . (intpos (p0 + i))
by A11, A21, AMI_3:52, SCMPDS_2:58
.=
s . (intpos (p0 + i))
by A16, A21
.=
f . i
by A3, A19, A20, Def1
;
verum end;
then A22:
f is_FinSequence_on Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s)),p0
by Def1;
A23: (IExec (((GBP := 0) ';' ((GBP,1) := 0)),s)) . (intpos 1) =
(Exec (((GBP,1) := 0),(Exec ((GBP := 0),(Initialize s))))) . (intpos 1)
by SCMPDS_5:47
.=
0
by A7, SCMPDS_2:58
;
A24: (IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)) . (intpos 1) =
(Exec (((GBP,2) := (n - 1)),(IExec (((GBP := 0) ';' ((GBP,1) := 0)),s)))) . (intpos 1)
by SCMPDS_5:46
.=
0
by A23, A9, AMI_3:52, SCMPDS_2:58
;
A25:
( (((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1)) is_closed_on s & (((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1)) is_halting_on s )
by SCMPDS_6:34, SCMPDS_6:35;
A26: (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s)) . GBP =
(Exec (((GBP,3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)))) . GBP
by SCMPDS_5:46
.=
0
by A10, A11, AMI_3:52, SCMPDS_2:58
;
A27: (IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)) . (intpos 2) =
(Exec (((GBP,2) := (n - 1)),(IExec (((GBP := 0) ';' ((GBP,1) := 0)),s)))) . (intpos 2)
by SCMPDS_5:46
.=
n - 1
by A9, SCMPDS_2:58
;
A28: (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s)) . (intpos 3) =
(Exec (((GBP,3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)))) . (intpos 3)
by SCMPDS_5:46
.=
p0 + 1
by A11, SCMPDS_2:58
;
X1:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s)) . (intpos 3) = (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s))) . (intpos 3)
by SCMPDS_5:40;
X2:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s)) . (intpos 1) = (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s))) . (intpos 1)
by SCMPDS_5:40;
X3:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s)) . GBP = (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s))) . GBP
by SCMPDS_5:40;
X4:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s)) . (intpos 2) = (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s))) . (intpos 2)
by SCMPDS_5:40;
A29: (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s)) . (intpos 1) =
(Exec (((GBP,3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)))) . (intpos 1)
by SCMPDS_5:46
.=
0
by A24, A11, AMI_3:52, SCMPDS_2:58
;
then
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s)) . (intpos 3) >= ((IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s)) . (intpos 1)) + 7
by A28, A5;
then
( for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (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))))))))) is_closed_on Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s)) & for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (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))))))))) is_halting_on Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s)) )
by A26, Lm13, X1, X2, X3;
then A30:
( for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (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))))))))) is_closed_on IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s) & for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (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))))))))) is_halting_on IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s) )
by SCMPDS_6:139, SCMPDS_6:140;
now let i be
Element of
NAT ;
( 1 <= i & i <= len g implies g . i = (IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (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)))))))))),(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s)))) . (intpos (p0 + i)) )assume
( 1
<= i &
i <= len g )
;
g . i = (IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (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)))))))))),(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s)))) . (intpos (p0 + i))hence g . i =
(IExec ((((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))) ';' (for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (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))))))))))),s)) . (intpos (p0 + i))
by A4, Def1
.=
(IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (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)))))))))),(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s)))) . (intpos (p0 + i))
by A25, A30, SCMPDS_7:49
;
verum end;
then A31:
g is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (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)))))))))),(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s))),p0
by Def1;
X5:
IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (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)))))))))),(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s))) = IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (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)))))))))),(Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s))))
by SCMPDS_5:48;
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),s)) . (intpos 2) =
(Exec (((GBP,3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)))) . (intpos 2)
by SCMPDS_5:46
.=
n - 1
by A27, A11, AMI_3:52, SCMPDS_2:58
;
hence
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
by A1, A2, A26, A29, A28, A22, A31, Lm16, X1, X2, X3, X4, X5; verum