let P be Instruction-Sequence of SCMPDS; for s being 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))),P,s),p0 holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
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))),P,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))),P,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))),P,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))),P,s),p0
; ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
A5:
p0 + 1 >= 6 + 1
by A1, XREAL_1:6;
set i1 = GBP := 0;
set i2 = (GBP,1) := 0;
set i3 = (GBP,2) := (n - 1);
set i4 = (GBP,3) := (p0 + 1);
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))),P,s);
set t2 = IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s);
set t3 = IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s);
set t4 = Exec ((GBP := 0),s);
A6:
(Exec ((GBP := 0),s)) . GBP = 0
by SCMPDS_2:45;
then A7:
DataLoc (((Exec ((GBP := 0),s)) . GBP),1) = intpos (0 + 1)
by SCMP_GCD:1;
A8: (IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)) . GBP =
(Exec (((GBP,1) := 0),(Exec ((GBP := 0),s)))) . GBP
by SCMPDS_5:42
.=
0
by A6, A7, AMI_3:10, SCMPDS_2:46
;
then A9:
DataLoc (((IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)) . GBP),2) = intpos (0 + 2)
by SCMP_GCD:1;
A10: (IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)) . GBP =
(Exec (((GBP,2) := (n - 1)),(IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)))) . GBP
by SCMPDS_5:41
.=
0
by A8, A9, AMI_3:10, SCMPDS_2:46
;
then A11:
DataLoc (((IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)) . GBP),3) = intpos (0 + 3)
by SCMP_GCD:1;
A13:
now let i be
Element of
NAT ;
( i > 3 implies (IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)) . (intpos i) = s . (intpos i) )assume A14:
i > 3
;
(IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)) . (intpos i) = s . (intpos i)then A15:
i > 1
by XXREAL_0:2;
thus (IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)) . (intpos i) =
(Exec (((GBP,1) := 0),(Exec ((GBP := 0),s)))) . (intpos i)
by SCMPDS_5:42
.=
(Exec ((GBP := 0),s)) . (intpos i)
by A7, A15, AMI_3:10, SCMPDS_2:46
.=
s . (intpos i)
by A14, AMI_3:10, SCMPDS_2:45
;
verum end;
A16:
now let i be
Element of
NAT ;
( i > 3 implies (IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)) . (intpos i) = s . (intpos i) )assume A17:
i > 3
;
(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,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))),P,s)) . (intpos i) =
(Exec (((GBP,2) := (n - 1)),(IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)))) . (intpos i)
by SCMPDS_5:41
.=
(IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)) . (intpos i)
by A9, A18, AMI_3:10, SCMPDS_2:46
.=
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))),P,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))),P,s))) . (intpos (p0 + i)) = f . iset pi =
p0 + i;
p0 + i >= p0 + 1
by A19, XREAL_1:6;
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))),P,s))) . (intpos (p0 + i)) =
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . (intpos (p0 + i))
by SCMPDS_5:15
.=
(Exec (((GBP,3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)))) . (intpos (p0 + i))
by SCMPDS_5:41
.=
(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)) . (intpos (p0 + i))
by A11, A21, AMI_3:10, SCMPDS_2:46
.=
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))),P,s)),p0
by Def1;
A23: (IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)) . (intpos 1) =
(Exec (((GBP,1) := 0),(Exec ((GBP := 0),s)))) . (intpos 1)
by SCMPDS_5:42
.=
0
by A7, SCMPDS_2:46
;
A24: (IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)) . (intpos 1) =
(Exec (((GBP,2) := (n - 1)),(IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)))) . (intpos 1)
by SCMPDS_5:41
.=
0
by A23, A9, AMI_3:10, SCMPDS_2:46
;
A25:
( (((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1)) is_closed_on s,P & (((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1)) is_halting_on s,P )
by SCMPDS_6:20, SCMPDS_6:21;
A26: (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . GBP =
(Exec (((GBP,3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)))) . GBP
by SCMPDS_5:41
.=
0
by A10, A11, AMI_3:10, SCMPDS_2:46
;
A27: (IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)) . (intpos 2) =
(Exec (((GBP,2) := (n - 1)),(IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)))) . (intpos 2)
by SCMPDS_5:41
.=
n - 1
by A9, SCMPDS_2:46
;
A28: (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . (intpos 3) =
(Exec (((GBP,3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)))) . (intpos 3)
by SCMPDS_5:41
.=
p0 + 1
by A11, SCMPDS_2:46
;
A29:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . (intpos 3) = (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s))) . (intpos 3)
by SCMPDS_5:15;
A30:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . (intpos 1) = (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s))) . (intpos 1)
by SCMPDS_5:15;
A31:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . GBP = (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s))) . GBP
by SCMPDS_5:15;
A32:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . (intpos 2) = (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s))) . (intpos 2)
by SCMPDS_5:15;
A33: (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . (intpos 1) =
(Exec (((GBP,3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)))) . (intpos 1)
by SCMPDS_5:41
.=
0
by A24, A11, AMI_3:10, SCMPDS_2:46
;
then
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . (intpos 3) >= ((IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,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))),P,s)),P & 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))),P,s)),P )
by A26, Lm13, A29, A30, A31;
then A34:
( 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))),P,s),P & 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))),P,s),P )
by SCMPDS_6:125, SCMPDS_6:126;
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)))))))))),P,(Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,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)))))))))),P,(Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,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))))))))))),P,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)))))))))),P,(Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s))))) . (intpos (p0 + i))
by A25, A34, SCMPDS_7:30
;
verum end;
then A35:
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)))))))))),P,(Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)))),p0
by Def1;
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . (intpos 2) =
(Exec (((GBP,3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)))) . (intpos 2)
by SCMPDS_5:41
.=
n - 1
by A27, A11, AMI_3:10, SCMPDS_2:46
;
hence
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
by A1, A2, A26, A33, A28, A22, A35, Lm16, A29, A30, A31, A32; verum