src/HOL/SPARK/Examples/Sqrt/sqrt/isqrt.siv

tuned NEWS;

*****************************************************************************
                       Semantic Analysis of SPARK Text
    Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
             Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
*****************************************************************************


CREATED 29-NOV-2010, 14:30:17  SIMPLIFIED 29-NOV-2010, 14:30:18

SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.

function Sqrt.Isqrt




For path(s) from start to run-time check associated with statement of line 7:

function_isqrt_1.
*** true .          /* all conclusions proved */


For path(s) from start to assertion of line 9:

function_isqrt_2.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 9 to assertion of line 9:

function_isqrt_3.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 9 to run-time check associated with 
          statement of line 10:

function_isqrt_4.
H1:    r * r <= n .
H2:    n >= 0 .
H3:    n <= 2147483647 .
H4:    r >= 0 .
H5:    r <= 2147483647 .
H6:    integer__size >= 0 .
H7:    natural__size >= 0 .
       ->
C1:    2 * r <= 2147483646 .
C2:    2 * r <= 2147483647 .


For path(s) from assertion of line 9 to run-time check associated with 
          statement of line 11:

function_isqrt_5.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 9 to finish:

function_isqrt_6.
*** true .          /* all conclusions proved */