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

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



SPARK Simplifier GPL 2012
Copyright (C) 2012 Altran Praxis Limited, Bath, U.K.

procedure Parser_Utilities.CheckAndAppendOrigin






@@@@@@@@@@  VC: procedure_checkandappendorigin_1.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(target, [i___1]) and element(target, [i___1]) <= 
          character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(origin, [i___1]) and element(origin, [i___1]) <= 
          character__last)
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(currentline, [i___1]) and element(currentline, [i___1]) <= 
          character__last)
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  rr_type__domainnamelength(target) = 1 and (element(target, [1]) 
          = 32 or element(target, [2]) = 32) or (rr_type__domainnamelength(
          target) = rr_type__maxdomainnamelength or element(target, [
          rr_type__domainnamelength(target) + 1]) = 32 and for_all(q_ : 
          integer, 1 <= q_ and q_ <= rr_type__domainnamelength(target) -> 
          element(target, [q_]) <> 32))
***  Proved C1:  rr_type__domainnamelength(target) >= 
          rr_type__domainnamestringtypeindex__first
     using hypothesis H8.
***  Proved C2:  rr_type__domainnamelength(target) <= 
          rr_type__domainnamestringtypeindex__last
     using hypothesis H9.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_checkandappendorigin_2.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(target, [i___1]) and element(target, [i___1]) <= 
          character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(origin, [i___1]) and element(origin, [i___1]) <= 
          character__last)
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(currentline, [i___1]) and element(currentline, [i___1]) <= 
          character__last)
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  rr_type__domainnamelength(target) = 1 and (element(target, [1]) 
          = 32 or element(target, [2]) = 32) or (rr_type__domainnamelength(
          target) = rr_type__maxdomainnamelength or element(target, [
          rr_type__domainnamelength(target) + 1]) = 32 and for_all(q_ : 
          integer, 1 <= q_ and q_ <= rr_type__domainnamelength(target) -> 
          element(target, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
***  Proved C1:  linecount >= unsigned_types__unsigned32__first
     using hypothesis H6.
***  Proved C2:  linecount <= unsigned_types__unsigned32__last
     using hypothesis H7.
-S-  Applied substitution rule checkandappe_rules(15).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New C3:  lastpos >= 0
-S-  Applied substitution rule checkandappe_rules(16).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New C4:  lastpos <= 2147483647
-S-  Applied substitution rule checkandappe_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H10:  rr_type__domainnamelength(target) = 1 and (element(target, [1]) 
          = 32 or element(target, [2]) = 32) or (rr_type__domainnamelength(
          target) = 128 or element(target, [rr_type__domainnamelength(target) + 
          1]) = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= 
          rr_type__domainnamelength(target) -> element(target, [q_]) <> 32))
-S-  Applied substitution rule checkandappe_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(target, [
          i___1]) and element(target, [i___1]) <= character__last)
<S>  New H2:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(origin, [
          i___1]) and element(origin, [i___1]) <= character__last)
<S>  New H3:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          currentline, [i___1]) and element(currentline, [i___1]) <= 
          character__last)
-S-  Applied substitution rule checkandappe_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(target, [
          i___1]) and element(target, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(origin, [
          i___1]) and element(origin, [i___1]) <= 255)
<S>  New H3:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          currentline, [i___1]) and element(currentline, [i___1]) <= 255)
-S-  Applied substitution rule checkandappe_rules(25).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H6:  linecount >= 0
-S-  Applied substitution rule checkandappe_rules(26).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H7:  linecount <= 4294967295
-S-  Applied substitution rule checkandappe_rules(31).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H4:  lastpos >= 1
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(currentline, [i___1]) 
          and element(currentline, [i___1]) <= 255)
-S-  Applied substitution rule checkandappe_rules(32).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H5:  lastpos <= 256
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(currentline, [i___1]) and element(currentline, [i___1]) <= 
          255)
-S-  Applied substitution rule checkandappe_rules(36).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__first by:
          1.
<S>  New H8:  rr_type__domainnamelength(target) >= 1
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(target, [
          i___1]) and element(target, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(origin, [
          i___1]) and element(origin, [i___1]) <= 255)
-S-  Applied substitution rule checkandappe_rules(37).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__last by:
          128.
<S>  New H9:  rr_type__domainnamelength(target) <= 128
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(target, [i___1]) and element(target, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(origin, [i___1]) and element(origin, [i___1]) <= 255)
***  Proved C3:  lastpos >= 0
     using hypothesis H4.
***  Proved C4:  lastpos <= 2147483647
     using hypothesis H5.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_checkandappendorigin_3.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(target, [i___1]) and element(target, [i___1]) <= 
          character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(origin, [i___1]) and element(origin, [i___1]) <= 
          character__last)
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(currentline, [i___1]) and element(currentline, [i___1]) <= 
          character__last)
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  rr_type__domainnamelength(target) = 1 and (element(target, [1]) 
          = 32 or element(target, [2]) = 32) or (rr_type__domainnamelength(
          target) = rr_type__maxdomainnamelength or element(target, [
          rr_type__domainnamelength(target) + 1]) = 32 and for_all(q_ : 
          integer, 1 <= q_ and q_ <= rr_type__domainnamelength(target) -> 
          element(target, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(target__2, [i___1]) and element(target__2, [i___1]) <= 
          character__last)
***  Proved C1:  linecount >= unsigned_types__unsigned32__first
     using hypothesis H6.
***  Proved C2:  linecount <= unsigned_types__unsigned32__last
     using hypothesis H7.
-S-  Applied substitution rule checkandappe_rules(15).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New C3:  lastpos >= 0
-S-  Applied substitution rule checkandappe_rules(16).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New C4:  lastpos <= 2147483647
>>>  Restructured hypothesis H14 into:
     >>>  H14:  origin <> rr_type__blankdomainname
-S-  Applied substitution rule checkandappe_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H10:  rr_type__domainnamelength(target) = 1 and (element(target, [1]) 
          = 32 or element(target, [2]) = 32) or (rr_type__domainnamelength(
          target) = 128 or element(target, [rr_type__domainnamelength(target) + 
          1]) = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= 
          rr_type__domainnamelength(target) -> element(target, [q_]) <> 32))
-S-  Applied substitution rule checkandappe_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(target, [
          i___1]) and element(target, [i___1]) <= character__last)
<S>  New H2:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(origin, [
          i___1]) and element(origin, [i___1]) <= character__last)
<S>  New H3:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          currentline, [i___1]) and element(currentline, [i___1]) <= 
          character__last)
<S>  New H15:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(target__2, [
          i___1]) and element(target__2, [i___1]) <= character__last)
-S-  Applied substitution rule checkandappe_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(target, [
          i___1]) and element(target, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(origin, [
          i___1]) and element(origin, [i___1]) <= 255)
<S>  New H3:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          currentline, [i___1]) and element(currentline, [i___1]) <= 255)
<S>  New H15:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(target__2, [
          i___1]) and element(target__2, [i___1]) <= 255)
-S-  Applied substitution rule checkandappe_rules(25).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H6:  linecount >= 0
-S-  Applied substitution rule checkandappe_rules(26).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H7:  linecount <= 4294967295
-S-  Applied substitution rule checkandappe_rules(31).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H4:  lastpos >= 1
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(currentline, [i___1]) 
          and element(currentline, [i___1]) <= 255)
-S-  Applied substitution rule checkandappe_rules(32).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H5:  lastpos <= 256
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(currentline, [i___1]) and element(currentline, [i___1]) <= 
          255)
-S-  Applied substitution rule checkandappe_rules(36).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__first by:
          1.
<S>  New H8:  rr_type__domainnamelength(target) >= 1
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(target, [
          i___1]) and element(target, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(origin, [
          i___1]) and element(origin, [i___1]) <= 255)
<S>  New H15:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(target__2, [
          i___1]) and element(target__2, [i___1]) <= 255)
-S-  Applied substitution rule checkandappe_rules(37).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__last by:
          128.
<S>  New H9:  rr_type__domainnamelength(target) <= 128
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(target, [i___1]) and element(target, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(origin, [i___1]) and element(origin, [i___1]) <= 255)
<S>  New H15:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(target__2, [i___1]) and element(target__2, [i___1]) <= 255)
***  Proved C3:  lastpos >= 0
     using hypothesis H4.
***  Proved C4:  lastpos <= 2147483647
     using hypothesis H5.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_checkandappendorigin_4.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_checkandappendorigin_5.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_checkandappendorigin_6.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_checkandappendorigin_7.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.

