Quelle  mixed_sigmas.pvs

mixed_sigmas[T, H: TYPE FROM int]: THEORY


BEGIN

  ASSUMING

     connected_domain1: ASSUMPTION (FORALL (x, y: T), (z: integer):
                                       x <= z AND z <= y IMPLIES T_pred(z))

     connected_domain2: ASSUMPTION (FORALL (x, y: H), (z: integer):
                                       x <= z AND z <= y IMPLIES H_pred(z))

  ENDASSUMING

  IMPORTING sigma[T],sigma[H]


  tlow      : VAR T_low[T]
  thigh     : VAR T_high[T]
  hlow      : VAR T_low[H]
  hhigh     : VAR T_high[H]
  i,j       : VAR T
  k,l     : VAR H
  rng, nn   : VAR nat
  pn        : VAR posnat
  z         : VAR int
  a,x,B     : VAR real


  F : VAR [T -> real]

  G : VAR [H -> real]

  mixed_sigmas_const_eq: LEMMA
    thigh-tlow = hhigh-hlow AND 
    (FORALL (i:nat): i<=thigh-tlow IMPLIES F(tlow + i) = G(hlow + i))
    IMPLIES
    x*sigma[T](tlow,thigh,F) = x*sigma[H](hlow,hhigh,G)
    

 mixed_sigmas_eq: LEMMA
    thigh-tlow = hhigh-hlow AND 
    (FORALL (i:nat): i<=thigh-tlow IMPLIES F(tlow + i) = G(hlow + i))
    IMPLIES
    sigma[T](tlow,thigh,F) = sigma[H](hlow,hhigh,G)

END mixed_sigmas