let n, p0 be Element of NAT ; :: thesis: card (insert-sort n,p0) = 23
set i1 = GBP := 0 ;
set i2 = GBP ,1 := 0 ;
set i3 = GBP ,2 := (n - 1);
set i4 = GBP ,3 := p0;
thus card (insert-sort n,p0) = (card ((((GBP := 0 ) ';' (GBP ,1 := 0 )) ';' (GBP ,2 := (n - 1))) ';' (GBP ,3 := p0))) + (card (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 )))))))) by SCMPDS_4:45
.= ((card (((GBP := 0 ) ';' (GBP ,1 := 0 )) ';' (GBP ,2 := (n - 1)))) + 1) + (card (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 )))))))) by SCMP_GCD:8
.= (((card ((GBP := 0 ) ';' (GBP ,1 := 0 ))) + 1) + 1) + (card (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 )))))))) by SCMP_GCD:8
.= ((2 + 1) + 1) + (card (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 )))))))) by SCMP_GCD:9
.= 4 + ((card (((((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 ))))))) + 3) by SCMPDS_7:60
.= 23 by Lm6 ; :: thesis: verum