Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Bille.identcache Sprache: PVS

Original von: PVS^©

vect_cont_2D : THEORY
BEGIN

  IMPORTING analysis@continuous_lambda[real],
            vect2_cont_comp[real],
            vect2_cont_dot[real]

  v,u : VAR Vect2
  x,y : VAR real
  nzx : VAR nzreal

  vv,vv1,vv2 : VAR continuous_vv_fun
  vr,vr1,vr2 : VAR continuous_vr_fun
  rr,rr1,rr2 : VAR continuous_fun
  rv,rv1,rv2 : VAR continuous_rv_fun

%   The following proved in vect2_cont_comp
%
%   comp_vv_vv_cont : LEMMA
%     continuous_vv(vv1 o vv2)
%
%   comp_rv_vr_cont : LEMMA
%     continuous_vv(rv o vr)
%
%   comp_vr_vv_cont : LEMMA
%      continuous_vr(vr o vv)
%
%   comp_rr_vr_cont : LEMMA
%     continuous_vr(rr o vr)
%
%   comp_vv_rv_cont : LEMMA
%     continuous_rv(vv o rv)
%
%   comp_rv_rr_cont : LEMMA
%     continuous_rv(rv o rr)
%
%   comp_vr_rv_cont : LEMMA
%     continuous_rr(vr o rv)

  const_cont_vv : LEMMA
    continuous_vv?(LAMBDA(v):u)

  const_cont_rv : LEMMA
    continuous_rv?(LAMBDA(x):v)

  const_cont_vr : LEMMA
     continuous_vr?(LAMBDA(v):x)

  pair_cont_rv : LEMMA
    continuous_rv?(LAMBDA(x):mk_vect2(rr1(x),rr2(x)))

  pair_cont_vv : LEMMA
    continuous_vv?(LAMBDA(v):mk_vect2(vr1(v),vr2(v)))

  x_cont_vr : LEMMA
    continuous_vr?(LAMBDA(v):x(v))

  y_cont_vr : LEMMA
    continuous_vr?(LAMBDA(v):y(v))

  id_cont_vv : LEMMA
    continuous_vv?(LAMBDA(v):v)

%   The following proved in vect2_continuity
%
%  dot_cont_vr : LEMMA
%    continuous_vr?(LAMBDA(v):vv1(v)*vv2(v))
%
%  dot_cont_rr : LEMMA
%    continuous_rr(LAMBDA(x):rv1(x)*rv2(x))

  mult_cont_vr : LEMMA
    continuous_vr?(LAMBDA(v):vr1(v)*vr2(v))

  scal_mult_cont_vr : LEMMA
    continuous_vr?(LAMBDA(v):x*vr(v))

  div_cont_vr : LEMMA
    FORALL (vnz:[Vect2->nzreal]):
      continuous_vr?(vnz) IMPLIES
      continuous_vr?(LAMBDA(v):vr(v)/vnz(v))

  scal_div1_cont_vr : LEMMA
    continuous_vr?(LAMBDA(v):vr(v)/nzx)

  scal_div2_cont_vr : LEMMA
    FORALL (vnz:[Vect2->nzreal]):
      continuous_vr?(vnz) IMPLIES
      continuous_vr?(LAMBDA(v):x/vnz(v))

  add_cont_vv : LEMMA
    continuous_vv?(LAMBDA(v):vv1(v)+vv2(v))

  add_cont_vr : LEMMA
    continuous_vr?(LAMBDA(v):vr1(v)+vr2(v))

  add_cont_rv : LEMMA
    continuous_rv?(LAMBDA(x):rv1(x)+rv2(x))

  sub_cont_vv : LEMMA
    continuous_vv?(LAMBDA(v):vv1(v)-vv2(v))

  sub_cont_vr : LEMMA
    continuous_vr?(LAMBDA(v):vr1(v)-vr2(v))

  sub_cont_rv : LEMMA
    continuous_rv?(LAMBDA(x):rv1(x)-rv2(x))

  neg_cont_vr : LEMMA
    continuous_vr?(LAMBDA(v):-vr(v))

  neg_cont_vv : LEMMA
    continuous_vv?(LAMBDA(v):-vv(v))

  neg_cont_rv : LEMMA
    continuous_rv?(LAMBDA(x):-rv(x))

%   The following proved in vect2_continuity
%
%  scal_cont_rv : LEMMA
%    continuous_rv?(LAMBDA(x):rr(x)*rv(x))
%
%  scal_cont_vv : LEMMA
%    continuous_vv?(LAMBDA(v):vr(v)*vv(v))
%
%  scal_scal_cont_rv : LEMMA
%    continuous_rv?LAMBDA(x):y*rv(x))

  scal_scal_cont_vv : LEMMA
    continuous_vv?(LAMBDA(v):y*vv(v))

  % Useful judgements

  sqv_cont : JUDGEMENT
    sqv HAS_TYPE continuous_vr_fun

  neg_cont : JUDGEMENT
    vectors_2D.- HAS_TYPE continuous_vv_fun

  % Useful compositons

  abs_cont_vr : LEMMA
    continuous_vr?(LAMBDA(v):abs(vr(v)))

  max_cont_vr : LEMMA
    continuous_vr?(LAMBDA(v):max(vr1(v),vr2(v)))

  min_cont_vr : LEMMA
    continuous_vr?(LAMBDA(v):min(vr1(v),vr2(v)))

  sq_cont_vr : LEMMA
    continuous_vr?(LAMBDA(v):sq(vr(v)))

  sqv_cont_vr : LEMMA
    continuous_vr?(LAMBDA(v):sqv(vv(v)))

  sqv_cont_rr : LEMMA
    continuous_rr?(LAMBDA(x):sqv(rv(x)))

END vect_cont_2D

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.