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

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


                     function Parser_Utilities.isRecord




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

function_isrecord_1.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
        ->
C1:    element(s, [begidx]) >= character__first .
C2:    element(s, [begidx]) <= character__last .
C3:    begidx >= rr_type__linelengthindex__first .
C4:    begidx <= rr_type__linelengthindex__last .
 

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

function_isrecord_2.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
        ->
C1:    ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
C2:    ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
 

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

function_isrecord_3.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
        ->
C1:    element(s, [endidx]) >= character__first .
C2:    element(s, [endidx]) <= character__last .
C3:    endidx >= rr_type__linelengthindex__first .
C4:    endidx <= rr_type__linelengthindex__last .
 

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

function_isrecord_4.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
        ->
C1:    ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
C2:    ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
 

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

function_isrecord_5.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
        ->
C1:    endidx - begidx + 1 >= rr_type__linelengthindex__first .
C2:    endidx - begidx + 1 <= rr_type__linelengthindex__last .
C3:    endidx - begidx >= integer__base__first .
C4:    endidx - begidx <= integer__base__last .
 

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

function_isrecord_6.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
        ->
C1:    endidx - 2 >= integer__base__first .
C2:    endidx - 2 <= integer__base__last .
 

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

function_isrecord_7.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   ada__characters__handling__to_upper(element(s, [
           begidx])) = 80 .
H60:   ada__characters__handling__to_upper(element(s, [
           endidx])) = 82 .
H61:   begidx <= endidx - 2 .
        ->
C1:    element(s, [begidx + 1]) >= character__first .
C2:    element(s, [begidx + 1]) <= character__last .
C3:    begidx + 1 >= rr_type__linelengthindex__first .
C4:    begidx + 1 <= rr_type__linelengthindex__last .
C5:    begidx + 1 >= integer__base__first .
C6:    begidx + 1 <= integer__base__last .
 

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

function_isrecord_8.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
        ->
C1:    endidx - 2 >= integer__base__first .
C2:    endidx - 2 <= integer__base__last .
 

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

function_isrecord_9.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   ada__characters__handling__to_upper(element(s, [
           begidx])) = 83 .
H67:   ada__characters__handling__to_upper(element(s, [
           endidx])) = 65 .
H68:   begidx <= endidx - 2 .
        ->
C1:    element(s, [begidx + 1]) >= character__first .
C2:    element(s, [begidx + 1]) <= character__last .
C3:    begidx + 1 >= rr_type__linelengthindex__first .
C4:    begidx + 1 <= rr_type__linelengthindex__last .
C5:    begidx + 1 >= integer__base__first .
C6:    begidx + 1 <= integer__base__last .
 

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

function_isrecord_10.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
        ->
C1:    endidx - 2 >= integer__base__first .
C2:    endidx - 2 <= integer__base__last .
 

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

function_isrecord_11.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   ada__characters__handling__to_upper(element(s, [
           begidx])) = 83 .
H74:   ada__characters__handling__to_upper(element(s, [
           endidx])) = 86 .
H75:   begidx <= endidx - 2 .
        ->
C1:    element(s, [begidx + 1]) >= character__first .
C2:    element(s, [begidx + 1]) <= character__last .
C3:    begidx + 1 >= rr_type__linelengthindex__first .
C4:    begidx + 1 <= rr_type__linelengthindex__last .
C5:    begidx + 1 >= integer__base__first .
C6:    begidx + 1 <= integer__base__last .
 

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

function_isrecord_12.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
        ->
C1:    endidx - 2 >= integer__base__first .
C2:    endidx - 2 <= integer__base__last .
 

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

function_isrecord_13.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   ada__characters__handling__to_upper(element(s, [
           begidx])) = 84 .
H81:   ada__characters__handling__to_upper(element(s, [
           endidx])) = 84 .
H82:   begidx <= endidx - 2 .
        ->
C1:    element(s, [begidx + 1]) >= character__first .
C2:    element(s, [begidx + 1]) <= character__last .
C3:    begidx + 1 >= rr_type__linelengthindex__first .
C4:    begidx + 1 <= rr_type__linelengthindex__last .
C5:    begidx + 1 >= integer__base__first .
C6:    begidx + 1 <= integer__base__last .
 

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

function_isrecord_14.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
        ->
C1:    endidx - 3 >= integer__base__first .
C2:    endidx - 3 <= integer__base__last .
 

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

function_isrecord_15.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H85:   endidx - 3 >= integer__base__first .
H86:   endidx - 3 <= integer__base__last .
H87:   ada__characters__handling__to_upper(element(s, [
           begidx])) = 65 .
H88:   ada__characters__handling__to_upper(element(s, [
           endidx])) = 65 .
H89:   begidx <= endidx - 3 .
        ->
C1:    element(s, [begidx + 1]) >= character__first .
C2:    element(s, [begidx + 1]) <= character__last .
C3:    begidx + 1 >= rr_type__linelengthindex__first .
C4:    begidx + 1 <= rr_type__linelengthindex__last .
C5:    begidx + 1 >= integer__base__first .
C6:    begidx + 1 <= integer__base__last .
 

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

function_isrecord_16.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H85:   endidx - 3 >= integer__base__first .
H86:   endidx - 3 <= integer__base__last .
H87:   ada__characters__handling__to_upper(element(s, [
           begidx])) = 65 .
H88:   ada__characters__handling__to_upper(element(s, [
           endidx])) = 65 .
H89:   begidx <= endidx - 3 .
H90:   element(s, [begidx + 1]) >= character__first .
H91:   element(s, [begidx + 1]) <= character__last .
H92:   begidx + 1 >= rr_type__linelengthindex__first .
H93:   begidx + 1 <= rr_type__linelengthindex__last .
H94:   begidx + 1 >= integer__base__first .
H95:   begidx + 1 <= integer__base__last .
H96:   ada__characters__handling__to_upper(element(s, [
           begidx + 1])) >= character__first .
H97:   ada__characters__handling__to_upper(element(s, [
           begidx + 1])) <= character__last .
        ->
C1:    element(s, [begidx + 2]) >= character__first .
C2:    element(s, [begidx + 2]) <= character__last .
C3:    begidx + 2 >= rr_type__linelengthindex__first .
C4:    begidx + 2 <= rr_type__linelengthindex__last .
C5:    begidx + 2 >= integer__base__first .
C6:    begidx + 2 <= integer__base__last .
 

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

function_isrecord_17.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H85:   endidx - 3 >= integer__base__first .
H86:   endidx - 3 <= integer__base__last .
H87:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 3))) .
H88:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H89:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H90:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H91:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
        ->
C1:    endidx - 3 >= integer__base__first .
C2:    endidx - 3 <= integer__base__last .
 

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

function_isrecord_18.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H85:   endidx - 3 >= integer__base__first .
H86:   endidx - 3 <= integer__base__last .
H87:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 3))) .
H88:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H89:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H90:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H91:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H92:   endidx - 3 >= integer__base__first .
H93:   endidx - 3 <= integer__base__last .
H94:   ada__characters__handling__to_upper(element(s, [
           begidx])) = 78 .
H95:   ada__characters__handling__to_upper(element(s, [
           endidx])) = 67 .
H96:   begidx <= endidx - 3 .
        ->
C1:    element(s, [begidx + 1]) >= character__first .
C2:    element(s, [begidx + 1]) <= character__last .
C3:    begidx + 1 >= rr_type__linelengthindex__first .
C4:    begidx + 1 <= rr_type__linelengthindex__last .
C5:    begidx + 1 >= integer__base__first .
C6:    begidx + 1 <= integer__base__last .
 

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

function_isrecord_19.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H85:   endidx - 3 >= integer__base__first .
H86:   endidx - 3 <= integer__base__last .
H87:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 3))) .
H88:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H89:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H90:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H91:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H92:   endidx - 3 >= integer__base__first .
H93:   endidx - 3 <= integer__base__last .
H94:   ada__characters__handling__to_upper(element(s, [
           begidx])) = 78 .
H95:   ada__characters__handling__to_upper(element(s, [
           endidx])) = 67 .
H96:   begidx <= endidx - 3 .
H97:   element(s, [begidx + 1]) >= character__first .
H98:   element(s, [begidx + 1]) <= character__last .
H99:   begidx + 1 >= rr_type__linelengthindex__first .
H100:  begidx + 1 <= rr_type__linelengthindex__last .
H101:  begidx + 1 >= integer__base__first .
H102:  begidx + 1 <= integer__base__last .
H103:  ada__characters__handling__to_upper(element(s, [
           begidx + 1])) >= character__first .
H104:  ada__characters__handling__to_upper(element(s, [
           begidx + 1])) <= character__last .
        ->
C1:    element(s, [begidx + 2]) >= character__first .
C2:    element(s, [begidx + 2]) <= character__last .
C3:    begidx + 2 >= rr_type__linelengthindex__first .
C4:    begidx + 2 <= rr_type__linelengthindex__last .
C5:    begidx + 2 >= integer__base__first .
C6:    begidx + 2 <= integer__base__last .
 

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

function_isrecord_20.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H85:   endidx - 3 >= integer__base__first .
H86:   endidx - 3 <= integer__base__last .
H87:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 3))) .
H88:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H89:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H90:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H91:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H92:   endidx - 3 >= integer__base__first .
H93:   endidx - 3 <= integer__base__last .
H94:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 67) and (begidx <= endidx - 3))) .
H95:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H96:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H97:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H98:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
        ->
C1:    endidx - 4 >= integer__base__first .
C2:    endidx - 4 <= integer__base__last .
 

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

function_isrecord_21.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H85:   endidx - 3 >= integer__base__first .
H86:   endidx - 3 <= integer__base__last .
H87:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 3))) .
H88:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H89:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H90:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H91:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H92:   endidx - 3 >= integer__base__first .
H93:   endidx - 3 <= integer__base__last .
H94:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 67) and (begidx <= endidx - 3))) .
H95:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H96:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H97:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H98:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H99:   endidx - 4 >= integer__base__first .
H100:  endidx - 4 <= integer__base__last .
H101:  ada__characters__handling__to_upper(element(s, [
           begidx])) = 67 .
H102:  ada__characters__handling__to_upper(element(s, [
           endidx])) = 69 .
H103:  begidx <= endidx - 4 .
        ->
C1:    element(s, [begidx + 1]) >= character__first .
C2:    element(s, [begidx + 1]) <= character__last .
C3:    begidx + 1 >= rr_type__linelengthindex__first .
C4:    begidx + 1 <= rr_type__linelengthindex__last .
C5:    begidx + 1 >= integer__base__first .
C6:    begidx + 1 <= integer__base__last .
 

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

function_isrecord_22.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H85:   endidx - 3 >= integer__base__first .
H86:   endidx - 3 <= integer__base__last .
H87:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 3))) .
H88:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H89:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H90:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H91:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H92:   endidx - 3 >= integer__base__first .
H93:   endidx - 3 <= integer__base__last .
H94:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 67) and (begidx <= endidx - 3))) .
H95:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H96:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H97:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H98:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H99:   endidx - 4 >= integer__base__first .
H100:  endidx - 4 <= integer__base__last .
H101:  ada__characters__handling__to_upper(element(s, [
           begidx])) = 67 .
H102:  ada__characters__handling__to_upper(element(s, [
           endidx])) = 69 .
H103:  begidx <= endidx - 4 .
H104:  element(s, [begidx + 1]) >= character__first .
H105:  element(s, [begidx + 1]) <= character__last .
H106:  begidx + 1 >= rr_type__linelengthindex__first .
H107:  begidx + 1 <= rr_type__linelengthindex__last .
H108:  begidx + 1 >= integer__base__first .
H109:  begidx + 1 <= integer__base__last .
H110:  ada__characters__handling__to_upper(element(s, [
           begidx + 1])) >= character__first .
H111:  ada__characters__handling__to_upper(element(s, [
           begidx + 1])) <= character__last .
        ->
C1:    element(s, [begidx + 2]) >= character__first .
C2:    element(s, [begidx + 2]) <= character__last .
C3:    begidx + 2 >= rr_type__linelengthindex__first .
C4:    begidx + 2 <= rr_type__linelengthindex__last .
C5:    begidx + 2 >= integer__base__first .
C6:    begidx + 2 <= integer__base__last .
 

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

function_isrecord_23.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H85:   endidx - 3 >= integer__base__first .
H86:   endidx - 3 <= integer__base__last .
H87:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 3))) .
H88:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H89:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H90:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H91:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H92:   endidx - 3 >= integer__base__first .
H93:   endidx - 3 <= integer__base__last .
H94:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 67) and (begidx <= endidx - 3))) .
H95:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H96:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H97:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H98:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H99:   endidx - 4 >= integer__base__first .
H100:  endidx - 4 <= integer__base__last .
H101:  ada__characters__handling__to_upper(element(s, [
           begidx])) = 67 .
H102:  ada__characters__handling__to_upper(element(s, [
           endidx])) = 69 .
H103:  begidx <= endidx - 4 .
H104:  element(s, [begidx + 1]) >= character__first .
H105:  element(s, [begidx + 1]) <= character__last .
H106:  begidx + 1 >= rr_type__linelengthindex__first .
H107:  begidx + 1 <= rr_type__linelengthindex__last .
H108:  begidx + 1 >= integer__base__first .
H109:  begidx + 1 <= integer__base__last .
H110:  ada__characters__handling__to_upper(element(s, [
           begidx + 1])) >= character__first .
H111:  ada__characters__handling__to_upper(element(s, [
           begidx + 1])) <= character__last .
H112:  element(s, [begidx + 2]) >= character__first .
H113:  element(s, [begidx + 2]) <= character__last .
H114:  begidx + 2 >= rr_type__linelengthindex__first .
H115:  begidx + 2 <= rr_type__linelengthindex__last .
H116:  begidx + 2 >= integer__base__first .
H117:  begidx + 2 <= integer__base__last .
H118:  ada__characters__handling__to_upper(element(s, [
           begidx + 2])) >= character__first .
H119:  ada__characters__handling__to_upper(element(s, [
           begidx + 2])) <= character__last .
        ->
C1:    element(s, [begidx + 3]) >= character__first .
C2:    element(s, [begidx + 3]) <= character__last .
C3:    begidx + 3 >= rr_type__linelengthindex__first .
C4:    begidx + 3 <= rr_type__linelengthindex__last .
C5:    begidx + 3 >= integer__base__first .
C6:    begidx + 3 <= integer__base__last .
 

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

function_isrecord_24.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H85:   endidx - 3 >= integer__base__first .
H86:   endidx - 3 <= integer__base__last .
H87:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 3))) .
H88:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H89:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H90:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H91:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H92:   endidx - 3 >= integer__base__first .
H93:   endidx - 3 <= integer__base__last .
H94:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 67) and (begidx <= endidx - 3))) .
H95:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H96:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H97:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H98:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H99:   endidx - 4 >= integer__base__first .
H100:  endidx - 4 <= integer__base__last .
H101:  not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 67) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 69) and (begidx <= endidx - 4))) .
H102:  ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H103:  ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H104:  ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H105:  ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
        ->
C1:    endidx - 4 >= integer__base__first .
C2:    endidx - 4 <= integer__base__last .
 

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

function_isrecord_25.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H85:   endidx - 3 >= integer__base__first .
H86:   endidx - 3 <= integer__base__last .
H87:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 3))) .
H88:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H89:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H90:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H91:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H92:   endidx - 3 >= integer__base__first .
H93:   endidx - 3 <= integer__base__last .
H94:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 67) and (begidx <= endidx - 3))) .
H95:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H96:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H97:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H98:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H99:   endidx - 4 >= integer__base__first .
H100:  endidx - 4 <= integer__base__last .
H101:  not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 67) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 69) and (begidx <= endidx - 4))) .
H102:  ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H103:  ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H104:  ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H105:  ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H106:  endidx - 4 >= integer__base__first .
H107:  endidx - 4 <= integer__base__last .
H108:  ada__characters__handling__to_upper(element(s, [
           begidx])) = 82 .
H109:  ada__characters__handling__to_upper(element(s, [
           endidx])) = 71 .
H110:  begidx <= endidx - 4 .
        ->
C1:    element(s, [begidx + 1]) >= character__first .
C2:    element(s, [begidx + 1]) <= character__last .
C3:    begidx + 1 >= rr_type__linelengthindex__first .
C4:    begidx + 1 <= rr_type__linelengthindex__last .
C5:    begidx + 1 >= integer__base__first .
C6:    begidx + 1 <= integer__base__last .
 

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

function_isrecord_26.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H85:   endidx - 3 >= integer__base__first .
H86:   endidx - 3 <= integer__base__last .
H87:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 3))) .
H88:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H89:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H90:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H91:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H92:   endidx - 3 >= integer__base__first .
H93:   endidx - 3 <= integer__base__last .
H94:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 67) and (begidx <= endidx - 3))) .
H95:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H96:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H97:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H98:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H99:   endidx - 4 >= integer__base__first .
H100:  endidx - 4 <= integer__base__last .
H101:  not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 67) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 69) and (begidx <= endidx - 4))) .
H102:  ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H103:  ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H104:  ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H105:  ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H106:  endidx - 4 >= integer__base__first .
H107:  endidx - 4 <= integer__base__last .
H108:  ada__characters__handling__to_upper(element(s, [
           begidx])) = 82 .
H109:  ada__characters__handling__to_upper(element(s, [
           endidx])) = 71 .
H110:  begidx <= endidx - 4 .
H111:  element(s, [begidx + 1]) >= character__first .
H112:  element(s, [begidx + 1]) <= character__last .
H113:  begidx + 1 >= rr_type__linelengthindex__first .
H114:  begidx + 1 <= rr_type__linelengthindex__last .
H115:  begidx + 1 >= integer__base__first .
H116:  begidx + 1 <= integer__base__last .
H117:  ada__characters__handling__to_upper(element(s, [
           begidx + 1])) >= character__first .
H118:  ada__characters__handling__to_upper(element(s, [
           begidx + 1])) <= character__last .
        ->
C1:    element(s, [begidx + 2]) >= character__first .
C2:    element(s, [begidx + 2]) <= character__last .
C3:    begidx + 2 >= rr_type__linelengthindex__first .
C4:    begidx + 2 <= rr_type__linelengthindex__last .
C5:    begidx + 2 >= integer__base__first .
C6:    begidx + 2 <= integer__base__last .
 

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

function_isrecord_27.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H85:   endidx - 3 >= integer__base__first .
H86:   endidx - 3 <= integer__base__last .
H87:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 3))) .
H88:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H89:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H90:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H91:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H92:   endidx - 3 >= integer__base__first .
H93:   endidx - 3 <= integer__base__last .
H94:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 67) and (begidx <= endidx - 3))) .
H95:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H96:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H97:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H98:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H99:   endidx - 4 >= integer__base__first .
H100:  endidx - 4 <= integer__base__last .
H101:  not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 67) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 69) and (begidx <= endidx - 4))) .
H102:  ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H103:  ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H104:  ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H105:  ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H106:  endidx - 4 >= integer__base__first .
H107:  endidx - 4 <= integer__base__last .
H108:  ada__characters__handling__to_upper(element(s, [
           begidx])) = 82 .
H109:  ada__characters__handling__to_upper(element(s, [
           endidx])) = 71 .
H110:  begidx <= endidx - 4 .
H111:  element(s, [begidx + 1]) >= character__first .
H112:  element(s, [begidx + 1]) <= character__last .
H113:  begidx + 1 >= rr_type__linelengthindex__first .
H114:  begidx + 1 <= rr_type__linelengthindex__last .
H115:  begidx + 1 >= integer__base__first .
H116:  begidx + 1 <= integer__base__last .
H117:  ada__characters__handling__to_upper(element(s, [
           begidx + 1])) >= character__first .
H118:  ada__characters__handling__to_upper(element(s, [
           begidx + 1])) <= character__last .
H119:  element(s, [begidx + 2]) >= character__first .
H120:  element(s, [begidx + 2]) <= character__last .
H121:  begidx + 2 >= rr_type__linelengthindex__first .
H122:  begidx + 2 <= rr_type__linelengthindex__last .
H123:  begidx + 2 >= integer__base__first .
H124:  begidx + 2 <= integer__base__last .
H125:  ada__characters__handling__to_upper(element(s, [
           begidx + 2])) >= character__first .
H126:  ada__characters__handling__to_upper(element(s, [
           begidx + 2])) <= character__last .
        ->
C1:    element(s, [begidx + 3]) >= character__first .
C2:    element(s, [begidx + 3]) <= character__last .
C3:    begidx + 3 >= rr_type__linelengthindex__first .
C4:    begidx + 3 <= rr_type__linelengthindex__last .
C5:    begidx + 3 >= integer__base__first .
C6:    begidx + 3 <= integer__base__last .
 

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

function_isrecord_28.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H85:   endidx - 3 >= integer__base__first .
H86:   endidx - 3 <= integer__base__last .
H87:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 3))) .
H88:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H89:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H90:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H91:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H92:   endidx - 3 >= integer__base__first .
H93:   endidx - 3 <= integer__base__last .
H94:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 67) and (begidx <= endidx - 3))) .
H95:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H96:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H97:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H98:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H99:   endidx - 4 >= integer__base__first .
H100:  endidx - 4 <= integer__base__last .
H101:  not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 67) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 69) and (begidx <= endidx - 4))) .
H102:  ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H103:  ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H104:  ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H105:  ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H106:  endidx - 4 >= integer__base__first .
H107:  endidx - 4 <= integer__base__last .
H108:  not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 71) and (begidx <= endidx - 4))) .
H109:  ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H110:  ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H111:  ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H112:  ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
        ->
C1:    endidx - 5 >= integer__base__first .
C2:    endidx - 5 <= integer__base__last .
 

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

function_isrecord_29.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H85:   endidx - 3 >= integer__base__first .
H86:   endidx - 3 <= integer__base__last .
H87:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 3))) .
H88:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H89:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H90:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H91:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H92:   endidx - 3 >= integer__base__first .
H93:   endidx - 3 <= integer__base__last .
H94:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 67) and (begidx <= endidx - 3))) .
H95:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H96:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H97:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H98:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H99:   endidx - 4 >= integer__base__first .
H100:  endidx - 4 <= integer__base__last .
H101:  not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 67) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 69) and (begidx <= endidx - 4))) .
H102:  ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H103:  ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H104:  ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H105:  ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H106:  endidx - 4 >= integer__base__first .
H107:  endidx - 4 <= integer__base__last .
H108:  not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 71) and (begidx <= endidx - 4))) .
H109:  ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H110:  ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H111:  ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H112:  ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H113:  endidx - 5 >= integer__base__first .
H114:  endidx - 5 <= integer__base__last .
H115:  ada__characters__handling__to_upper(element(s, [
           begidx])) = 68 .
H116:  ada__characters__handling__to_upper(element(s, [
           endidx])) = 89 .
H117:  begidx <= endidx - 5 .
        ->
C1:    element(s, [begidx + 1]) >= character__first .
C2:    element(s, [begidx + 1]) <= character__last .
C3:    begidx + 1 >= rr_type__linelengthindex__first .
C4:    begidx + 1 <= rr_type__linelengthindex__last .
C5:    begidx + 1 >= integer__base__first .
C6:    begidx + 1 <= integer__base__last .
 

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

function_isrecord_30.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H85:   endidx - 3 >= integer__base__first .
H86:   endidx - 3 <= integer__base__last .
H87:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 3))) .
H88:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H89:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H90:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H91:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H92:   endidx - 3 >= integer__base__first .
H93:   endidx - 3 <= integer__base__last .
H94:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 67) and (begidx <= endidx - 3))) .
H95:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H96:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H97:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H98:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H99:   endidx - 4 >= integer__base__first .
H100:  endidx - 4 <= integer__base__last .
H101:  not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 67) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 69) and (begidx <= endidx - 4))) .
H102:  ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H103:  ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H104:  ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H105:  ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H106:  endidx - 4 >= integer__base__first .
H107:  endidx - 4 <= integer__base__last .
H108:  not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 71) and (begidx <= endidx - 4))) .
H109:  ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H110:  ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H111:  ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H112:  ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H113:  endidx - 5 >= integer__base__first .
H114:  endidx - 5 <= integer__base__last .
H115:  ada__characters__handling__to_upper(element(s, [
           begidx])) = 68 .
H116:  ada__characters__handling__to_upper(element(s, [
           endidx])) = 89 .
H117:  begidx <= endidx - 5 .
H118:  element(s, [begidx + 1]) >= character__first .
H119:  element(s, [begidx + 1]) <= character__last .
H120:  begidx + 1 >= rr_type__linelengthindex__first .
H121:  begidx + 1 <= rr_type__linelengthindex__last .
H122:  begidx + 1 >= integer__base__first .
H123:  begidx + 1 <= integer__base__last .
H124:  ada__characters__handling__to_upper(element(s, [
           begidx + 1])) >= character__first .
H125:  ada__characters__handling__to_upper(element(s, [
           begidx + 1])) <= character__last .
        ->
C1:    element(s, [begidx + 2]) >= character__first .
C2:    element(s, [begidx + 2]) <= character__last .
C3:    begidx + 2 >= rr_type__linelengthindex__first .
C4:    begidx + 2 <= rr_type__linelengthindex__last .
C5:    begidx + 2 >= integer__base__first .
C6:    begidx + 2 <= integer__base__last .
 

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

function_isrecord_31.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H85:   endidx - 3 >= integer__base__first .
H86:   endidx - 3 <= integer__base__last .
H87:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 3))) .
H88:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H89:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H90:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H91:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H92:   endidx - 3 >= integer__base__first .
H93:   endidx - 3 <= integer__base__last .
H94:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 67) and (begidx <= endidx - 3))) .
H95:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H96:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H97:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H98:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H99:   endidx - 4 >= integer__base__first .
H100:  endidx - 4 <= integer__base__last .
H101:  not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 67) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 69) and (begidx <= endidx - 4))) .
H102:  ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H103:  ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H104:  ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H105:  ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H106:  endidx - 4 >= integer__base__first .
H107:  endidx - 4 <= integer__base__last .
H108:  not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 71) and (begidx <= endidx - 4))) .
H109:  ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H110:  ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H111:  ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H112:  ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H113:  endidx - 5 >= integer__base__first .
H114:  endidx - 5 <= integer__base__last .
H115:  ada__characters__handling__to_upper(element(s, [
           begidx])) = 68 .
H116:  ada__characters__handling__to_upper(element(s, [
           endidx])) = 89 .
H117:  begidx <= endidx - 5 .
H118:  element(s, [begidx + 1]) >= character__first .
H119:  element(s, [begidx + 1]) <= character__last .
H120:  begidx + 1 >= rr_type__linelengthindex__first .
H121:  begidx + 1 <= rr_type__linelengthindex__last .
H122:  begidx + 1 >= integer__base__first .
H123:  begidx + 1 <= integer__base__last .
H124:  ada__characters__handling__to_upper(element(s, [
           begidx + 1])) >= character__first .
H125:  ada__characters__handling__to_upper(element(s, [
           begidx + 1])) <= character__last .
H126:  element(s, [begidx + 2]) >= character__first .
H127:  element(s, [begidx + 2]) <= character__last .
H128:  begidx + 2 >= rr_type__linelengthindex__first .
H129:  begidx + 2 <= rr_type__linelengthindex__last .
H130:  begidx + 2 >= integer__base__first .
H131:  begidx + 2 <= integer__base__last .
H132:  ada__characters__handling__to_upper(element(s, [
           begidx + 2])) >= character__first .
H133:  ada__characters__handling__to_upper(element(s, [
           begidx + 2])) <= character__last .
        ->
C1:    element(s, [begidx + 3]) >= character__first .
C2:    element(s, [begidx + 3]) <= character__last .
C3:    begidx + 3 >= rr_type__linelengthindex__first .
C4:    begidx + 3 <= rr_type__linelengthindex__last .
C5:    begidx + 3 >= integer__base__first .
C6:    begidx + 3 <= integer__base__last .
 

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

function_isrecord_32.
H1:    begidx <= endidx .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H3:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    element(s, [begidx]) >= character__first .
H8:    element(s, [begidx]) <= character__last .
H9:    begidx >= rr_type__linelengthindex__first .
H10:   begidx <= rr_type__linelengthindex__last .
H11:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H12:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H13:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H14:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H15:   element(s, [endidx]) >= character__first .
H16:   element(s, [endidx]) <= character__last .
H17:   endidx >= rr_type__linelengthindex__first .
H18:   endidx <= rr_type__linelengthindex__last .
H19:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H20:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H21:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H22:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H23:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx - begidx >= integer__base__first .
H26:   endidx - begidx <= integer__base__last .
H27:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H28:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H29:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H33:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H34:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H35:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H36:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H40:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H41:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H42:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H43:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 77) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H47:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H48:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H49:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H50:   endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51:   endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H54:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H55:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H56:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H57:   endidx - 2 >= integer__base__first .
H58:   endidx - 2 <= integer__base__last .
H59:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 80) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 82) and (begidx <= endidx - 2))) .
H60:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H61:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H62:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H63:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H64:   endidx - 2 >= integer__base__first .
H65:   endidx - 2 <= integer__base__last .
H66:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 2))) .
H67:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H68:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H69:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H70:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H71:   endidx - 2 >= integer__base__first .
H72:   endidx - 2 <= integer__base__last .
H73:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 83) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 86) and (begidx <= endidx - 2))) .
H74:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H75:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H76:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H77:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H78:   endidx - 2 >= integer__base__first .
H79:   endidx - 2 <= integer__base__last .
H80:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 84) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 84) and (begidx <= endidx - 2))) .
H81:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H82:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H83:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H84:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H85:   endidx - 3 >= integer__base__first .
H86:   endidx - 3 <= integer__base__last .
H87:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 65) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 65) and (begidx <= endidx - 3))) .
H88:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H89:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H90:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H91:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H92:   endidx - 3 >= integer__base__first .
H93:   endidx - 3 <= integer__base__last .
H94:   not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 78) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 67) and (begidx <= endidx - 3))) .
H95:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H96:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H97:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H98:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H99:   endidx - 4 >= integer__base__first .
H100:  endidx - 4 <= integer__base__last .
H101:  not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 67) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 69) and (begidx <= endidx - 4))) .
H102:  ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H103:  ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H104:  ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H105:  ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H106:  endidx - 4 >= integer__base__first .
H107:  endidx - 4 <= integer__base__last .
H108:  not ((ada__characters__handling__to_upper(element(s, [
           begidx])) = 82) and ((
           ada__characters__handling__to_upper(element(s, [
           endidx])) = 71) and (begidx <= endidx - 4))) .
H109:  ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H110:  ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H111:  ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H112:  ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
H113:  endidx - 5 >= integer__base__first .
H114:  endidx - 5 <= integer__base__last .
H115:  ada__characters__handling__to_upper(element(s, [
           begidx])) = 68 .
H116:  ada__characters__handling__to_upper(element(s, [
           endidx])) = 89 .
H117:  begidx <= endidx - 5 .
H118:  element(s, [begidx + 1]) >= character__first .
H119:  element(s, [begidx + 1]) <= character__last .
H120:  begidx + 1 >= rr_type__linelengthindex__first .
H121:  begidx + 1 <= rr_type__linelengthindex__last .
H122:  begidx + 1 >= integer__base__first .
H123:  begidx + 1 <= integer__base__last .
H124:  ada__characters__handling__to_upper(element(s, [
           begidx + 1])) >= character__first .
H125:  ada__characters__handling__to_upper(element(s, [
           begidx + 1])) <= character__last .
H126:  element(s, [begidx + 2]) >= character__first .
H127:  element(s, [begidx + 2]) <= character__last .
H128:  begidx + 2 >= rr_type__linelengthindex__first .
H129:  begidx + 2 <= rr_type__linelengthindex__last .
H130:  begidx + 2 >= integer__base__first .
H131:  begidx + 2 <= integer__base__last .
H132:  ada__characters__handling__to_upper(element(s, [
           begidx + 2])) >= character__first .
H133:  ada__characters__handling__to_upper(element(s, [
           begidx + 2])) <= character__last .
H134:  element(s, [begidx + 3]) >= character__first .
H135:  element(s, [begidx + 3]) <= character__last .
H136:  begidx + 3 >= rr_type__linelengthindex__first .
H137:  begidx + 3 <= rr_type__linelengthindex__last .
H138:  begidx + 3 >= integer__base__first .
H139:  begidx + 3 <= integer__base__last .
H140:  ada__characters__handling__to_upper(element(s, [
           begidx + 3])) >= character__first .
H141:  ada__characters__handling__to_upper(element(s, [
           begidx + 3])) <= character__last .
        ->
C1:    element(s, [begidx + 4]) >= character__first .
C2:    element(s, [begidx + 4]) <= character__last .
C3:    begidx + 4 >= rr_type__linelengthindex__first .
C4:    begidx + 4 <= rr_type__linelengthindex__last .
C5:    begidx + 4 >= integer__base__first .
C6:    begidx + 4 <= integer__base__last .
 

For path(s) from start to finish:

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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


