set a = GBP ;
let s be State of SCMPDS ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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;

A12: now

let i be Element of NAT ; :: thesis: ( i > 3 implies (Exec (GBP := 0 ),(Initialize s)) . (intpos i) = s . (intpos i) )
assume i > 3 ; :: thesis: (Exec (GBP := 0 ),(Initialize s)) . (intpos i) = s . (intpos i)
hence (Exec (GBP := 0 ),(Initialize s)) . (intpos i) = (Initialize s) . (intpos i) by AMI_3:52, SCMPDS_2:57
.= s . (intpos i) by SCMPDS_5:40 ;
:: thesis: verum

end;

A13: now

let i be Element of NAT ; :: thesis: ( i > 3 implies (IExec ((GBP := 0 ) ';' (GBP ,1 := 0 )),s) . (intpos i) = s . (intpos i) )
assume A14: i > 3 ; :: thesis: (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 ; :: thesis: verum

end;

A16: now

let i be Element of NAT ; :: thesis: ( i > 3 implies (IExec (((GBP := 0 ) ';' (GBP ,1 := 0 )) ';' (GBP ,2 := (n - 1))),s) . (intpos i) = s . (intpos i) )
assume A17: i > 3 ; :: thesis: (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 ; :: thesis: verum

end;

now

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len f implies (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 ; :: thesis: (IExec ((((GBP := 0 ) ';' (GBP ,1 := 0 )) ';' (GBP ,2 := (n - 1))) ';' (GBP ,3 := (p0 + 1))),s) . (intpos (p0 + i)) = f . i
set 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 (IExec ((((GBP := 0 ) ';' (GBP ,1 := 0 )) ';' (GBP ,2 := (n - 1))) ';' (GBP ,3 := (p0 + 1))),s) . (intpos (p0 + i)) = (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 ; :: thesis: verum

end;

then A22: f is_FinSequence_on 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 ;
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 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 A26, Lm13;

now

let i be Element of NAT ; :: thesis: ( 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 ) ; :: thesis: 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 ;
:: thesis: 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;
(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; :: thesis: verum