           *******************************************************
                       Semantic Analysis of SPARK Text
                             Examiner GPL Edition

           *******************************************************


                 function dns_table_pkg.DNS_Table_Type.Same




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

function_same_1.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           x, [i___1]) >= character__first) and (element(x, [
           i___1]) <= character__last))) .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           y, [i___1]) >= character__first) and (element(y, [
           i___1]) <= character__last))) .
H3:    rr_type__wirenamelength(x) >= 
           rr_type__wirestringtypeindex__first .
H4:    rr_type__wirenamelength(x) <= 
           rr_type__wirestringtypeindex__last .
H5:    (rr_type__wirenamelength(x) = 
           rr_type__maxdomainnamelength + 1) or ((element(x, [
           rr_type__wirenamelength(x)]) = 0) and (for_all(q_: 
           integer, ((q_ >= 1) and (q_ <= 
           rr_type__wirenamelength(x) - 1)) -> (element(x, [
           q_]) <> 0)))) .
        ->
C1:    rr_type__wirenamelength(x) >= 
           rr_type__wirestringtypeindex__first .
C2:    rr_type__wirenamelength(x) <= 
           rr_type__wirestringtypeindex__last .
 

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

function_same_2.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           x, [i___1]) >= character__first) and (element(x, [
           i___1]) <= character__last))) .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           y, [i___1]) >= character__first) and (element(y, [
           i___1]) <= character__last))) .
H3:    rr_type__wirenamelength(x) >= 
           rr_type__wirestringtypeindex__first .
H4:    rr_type__wirenamelength(x) <= 
           rr_type__wirestringtypeindex__last .
H5:    (rr_type__wirenamelength(x) = 
           rr_type__maxdomainnamelength + 1) or ((element(x, [
           rr_type__wirenamelength(x)]) = 0) and (for_all(q_: 
           integer, ((q_ >= 1) and (q_ <= 
           rr_type__wirenamelength(x) - 1)) -> (element(x, [
           q_]) <> 0)))) .
H6:    rr_type__wirenamelength(x) >= 
           rr_type__wirestringtypeindex__first .
H7:    rr_type__wirenamelength(x) <= 
           rr_type__wirestringtypeindex__last .
H8:    rr_type__wirenamelength(x) >= 
           rr_type__wirestringtypeindex__first .
H9:    rr_type__wirenamelength(x) <= 
           rr_type__wirestringtypeindex__last .
        ->
C1:    rr_type__wirenamelength(x) >= integer__first .
C2:    rr_type__wirenamelength(x) <= integer__last .
C3:    1 >= integer__first .
C4:    1 <= integer__last .
 

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

function_same_3.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           x, [i___1]) >= character__first) and (element(x, [
           i___1]) <= character__last))) .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           y, [i___1]) >= character__first) and (element(y, [
           i___1]) <= character__last))) .
H3:    rr_type__wirenamelength(x) >= 
           rr_type__wirestringtypeindex__first .
H4:    rr_type__wirenamelength(x) <= 
           rr_type__wirestringtypeindex__last .
H5:    (rr_type__wirenamelength(x) = 
           rr_type__maxdomainnamelength + 1) or ((element(x, [
           rr_type__wirenamelength(x)]) = 0) and (for_all(q_: 
           integer, ((q_ >= 1) and (q_ <= 
           rr_type__wirenamelength(x) - 1)) -> (element(x, [
           q_]) <> 0)))) .
H6:    rr_type__wirenamelength(x) >= 
           rr_type__wirestringtypeindex__first .
H7:    rr_type__wirenamelength(x) <= 
           rr_type__wirestringtypeindex__last .
H8:    rr_type__wirenamelength(x) >= 
           rr_type__wirestringtypeindex__first .
H9:    rr_type__wirenamelength(x) <= 
           rr_type__wirestringtypeindex__last .
H10:   rr_type__wirenamelength(x) >= integer__first .
H11:   rr_type__wirenamelength(x) <= integer__last .
H12:   1 >= integer__first .
H13:   1 <= integer__last .
        ->
C1:    (1 <= rr_type__wirenamelength(x)) -> ((
           rr_type__wirenamelength(x) >= integer__first) and (
           rr_type__wirenamelength(x) <= integer__last)) .
C2:    (1 <= rr_type__wirenamelength(x)) -> ((1 >= integer__first) and (
           1 <= integer__last)) .
 

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

function_same_4.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           x, [i___1]) >= character__first) and (element(x, [
           i___1]) <= character__last))) .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           y, [i___1]) >= character__first) and (element(y, [
           i___1]) <= character__last))) .
H3:    rr_type__wirenamelength(x) >= 
           rr_type__wirestringtypeindex__first .
H4:    rr_type__wirenamelength(x) <= 
           rr_type__wirestringtypeindex__last .
H5:    (rr_type__wirenamelength(x) = 
           rr_type__maxdomainnamelength + 1) or ((element(x, [
           rr_type__wirenamelength(x)]) = 0) and (for_all(q_: 
           integer, ((q_ >= 1) and (q_ <= 
           rr_type__wirenamelength(x) - 1)) -> (element(x, [
           q_]) <> 0)))) .
H6:    rr_type__wirenamelength(x) >= 
           rr_type__wirestringtypeindex__first .
H7:    rr_type__wirenamelength(x) <= 
           rr_type__wirestringtypeindex__last .
H8:    rr_type__wirenamelength(x) >= 
           rr_type__wirestringtypeindex__first .
H9:    rr_type__wirenamelength(x) <= 
           rr_type__wirestringtypeindex__last .
H10:   rr_type__wirenamelength(x) >= integer__first .
H11:   rr_type__wirenamelength(x) <= integer__last .
H12:   1 >= integer__first .
H13:   1 <= integer__last .
H14:   (1 <= rr_type__wirenamelength(x)) -> ((
           rr_type__wirenamelength(x) >= integer__first) and (
           rr_type__wirenamelength(x) <= integer__last)) .
H15:   (1 <= rr_type__wirenamelength(x)) -> ((1 >= integer__first) and (
           1 <= integer__last)) .
H16:   rr_type__wirenamelength(x) >= 
           rr_type__wirestringtypeindex__first .
H17:   rr_type__wirenamelength(x) <= 
           rr_type__wirestringtypeindex__last .
H18:   1 <= rr_type__wirenamelength(x) .
        ->
C1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           x, [i___1]) >= character__first) and (element(x, [
           i___1]) <= character__last))) .
C2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           y, [i___1]) >= character__first) and (element(y, [
           i___1]) <= character__last))) .
C3:    1 >= integer__first .
C4:    1 <= integer__last .
C5:    1 >= 1 .
C6:    1 <= rr_type__wirenamelength(x) .
C7:    rr_type__wirenamelength(x) >= 
           rr_type__wirestringtypeindex__first .
C8:    rr_type__wirenamelength(x) <= 
           rr_type__wirestringtypeindex__last .
 

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

function_same_5.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           x, [i___1]) >= character__first) and (element(x, [
           i___1]) <= character__last))) .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           y, [i___1]) >= character__first) and (element(y, [
           i___1]) <= character__last))) .
H3:    loop__1__i >= integer__first .
H4:    loop__1__i <= integer__last .
H5:    loop__1__i >= 1 .
H6:    loop__1__i <= length__entry__loop__1 .
H7:    length__entry__loop__1 >= rr_type__wirestringtypeindex__first .
H8:    length__entry__loop__1 <= rr_type__wirestringtypeindex__last .
H9:    loop__1__i >= rr_type__wirestringtypeindex__first .
H10:   loop__1__i <= rr_type__wirestringtypeindex__last .
H11:   loop__1__i >= rr_type__wirestringtypeindex__first .
H12:   loop__1__i <= rr_type__wirestringtypeindex__last .
H13:   not (element(x, [loop__1__i]) <> element(y, [
           loop__1__i])) .
H14:   not (loop__1__i = length__entry__loop__1) .
        ->
C1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           x, [i___1]) >= character__first) and (element(x, [
           i___1]) <= character__last))) .
C2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           y, [i___1]) >= character__first) and (element(y, [
           i___1]) <= character__last))) .
C3:    loop__1__i + 1 >= integer__first .
C4:    loop__1__i + 1 <= integer__last .
C5:    loop__1__i + 1 >= 1 .
C6:    loop__1__i + 1 <= length__entry__loop__1 .
C7:    length__entry__loop__1 >= rr_type__wirestringtypeindex__first .
C8:    length__entry__loop__1 <= rr_type__wirestringtypeindex__last .
 

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

function_same_6.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           x, [i___1]) >= character__first) and (element(x, [
           i___1]) <= character__last))) .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           y, [i___1]) >= character__first) and (element(y, [
           i___1]) <= character__last))) .
H3:    loop__1__i >= integer__first .
H4:    loop__1__i <= integer__last .
H5:    loop__1__i >= 1 .
H6:    loop__1__i <= length__entry__loop__1 .
H7:    length__entry__loop__1 >= rr_type__wirestringtypeindex__first .
H8:    length__entry__loop__1 <= rr_type__wirestringtypeindex__last .
        ->
C1:    loop__1__i >= rr_type__wirestringtypeindex__first .
C2:    loop__1__i <= rr_type__wirestringtypeindex__last .
C3:    loop__1__i >= rr_type__wirestringtypeindex__first .
C4:    loop__1__i <= rr_type__wirestringtypeindex__last .
 

For path(s) from start to finish:

function_same_7.
*** true .          /* trivially true VC removed by Examiner */


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

function_same_8.
*** true .          /* trivially true VC removed by Examiner */


function_same_9.
*** true .          /* trivially true VC removed by Examiner */


