:: Logical Correctness of Vector Calculation Programs
::  by Takaya Nishiyama , Hirofumi Fukura and Yatsuka Nakamura
::
:: Received July 13, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, NAT_1, XBOOLE_0, AFINSQ_1, SUBSET_1, TARSKI, CARD_1,
      FUNCT_1, RELAT_1, ORDINAL1, FINSEQ_1, XXREAL_0, ARYTM_3, ARYTM_1,
      FUNCOP_1, ORDINAL4, REAL_1, INT_1, CARD_3, PARTFUN1, RVSUM_1, FINSEQ_2,
      PRGCOR_2;
 notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, RELAT_1, FUNCT_1, ORDINAL1,
      ORDINAL4, REAL_1, NAT_1, PARTFUN1, FINSEQ_1, FUNCOP_1, SEQ_1, AFINSQ_1,
      INT_1, RVSUM_1, NAT_D, FINSEQ_2, XXREAL_0;
 constructors XXREAL_0, REAL_1, NAT_1, PARTFUN1, NAT_D, AFINSQ_1, SEQ_1,
      BINOP_2, INT_1, VALUED_1, RVSUM_1, RELSET_1, ORDINAL4, FUNCOP_1, FUNCT_7;
 registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
      MEMBERED, FINSEQ_1, AFINSQ_1, XBOOLE_0, VALUED_0, FINSEQ_2, CARD_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI;
 theorems FUNCT_1, NAT_1, RELAT_1, ORDINAL1, FINSEQ_1, FUNCOP_1, AFINSQ_1,
      RVSUM_1, FINSEQ_4, FINSEQ_2, XREAL_1, XXREAL_0, PARTFUN1, VALUED_1,
      XREAL_0, FINSEQ_5, CARD_1;
 schemes NAT_1, AFINSQ_1;

begin

reserve k,i for Nat;
reserve D for non empty set;

definition let D;

  let p be XFinSequence of D, q be FinSequence of D;
  pred p is_an_xrep_of q means  :Def1:
  NAT c= D & (p.0)=len q & len q < len p &
  for i st 1<=i & i<=len q holds p.i=q.i;
end;

theorem
  for p being XFinSequence of D st NAT c= D &
  (p.0) is Nat & (p.0) in len p holds p is_an_xrep_of (XFS2FS*(p))
proof
  let p be XFinSequence of D;
  assume that
A1: NAT c= D and
A2: (p.0) is Nat and
A3: (p.0) in len p;
  reconsider m0=(p.0) as Nat by A2;
A4: m0<len p by A3,NAT_1:44;
  len (XFS2FS*(p)) =m0 & for i st 1<=i & i<= m0 holds (XFS2FS*(p)).i=p.i
  by A3,AFINSQ_1:def 11;
  hence thesis by A1,A4,Def1;
end;

definition
  let x,y,a,b,c be set;
  func IFLGT(x,y,a,b,c) -> set equals :Def2:
  a if x in y, b if x = y otherwise
  c;
  correctness;
end;

theorem Th2:
  for q being FinSequence of D, n being Nat st NAT c= D & n>len q
  holds ex p being XFinSequence of D st len p=n & p is_an_xrep_of q
proof
  let q be FinSequence of D, n be Nat;
  assume that
A1: NAT c= D and
A2: n>len q;
  reconsider n as Element of NAT by ORDINAL1:def 12;
  len q in NAT;
  then consider d2 being set such that
A3: d2 in D and
A4: d2=len q by A1;
  reconsider d=d2 as Element of D by A3;
  deffunc F(set)= IFEQ($1,0,d,IFLGT($1,len q,q.$1,q.$1,d));
  ex p being XFinSequence st len p = n & for k be Nat st k
  in n holds p.k=F(k) from AFINSQ_1:sch 2;
  then consider p being XFinSequence such that
A5: len p = n and
A6: for k be Nat st k in n holds p.k=F(k);
  rng p c= D
  proof
    let y be set;
    assume y in rng p;
    then consider x being set such that
A7: x in dom p and
A8: y=p.x by FUNCT_1:def 3;
    reconsider nx=x as Ordinal by A7;
    reconsider kx=nx as Element of NAT by A7;
A9: p.kx=F(kx) by A5,A6,A7;
    now
      per cases;
      case
        x=0;
        then F(x)=d by FUNCOP_1:def 8;
        hence p.x in D by A9;
      end;
      case
A10:    x<>0;
        then
A11:    F(x)=IFLGT(x,len q,q.x,q.x,d) by FUNCOP_1:def 8;
        now
          per cases;
          case
A12:        x in len q;
            then
A13:        kx<len q by NAT_1:44;
            0+1<=kx by A10,NAT_1:13;
            then kx in Seg len q by A13,FINSEQ_1:1;
            then x in dom q by FINSEQ_1:def 3; then
A14:        q.x in rng q by FUNCT_1:def 3;
A15:        rng q c= D by FINSEQ_1:def 4;
            F(x)=q.x by A11,A12,Def2;
            hence p.x in D by A9,A14,A15;
          end;
          case
A16:        x=len q;
            0+1<=kx by A10,NAT_1:13;
            then kx in Seg len q by A16,FINSEQ_1:1;
            then x in dom q by FINSEQ_1:def 3;
            then
A17:        q.x in rng q by FUNCT_1:def 3;
A18:        rng q c= D by FINSEQ_1:def 4;
            F(x)=q.x by A11,A16,Def2;
            hence p.x in D by A9,A17,A18;
          end;
          case
            not (x in len q or x=len q);
            then F(x)=d by A11,Def2;
            hence p.x in D by A9;
          end;
        end;
        hence p.x in D;
      end;
    end;
    hence thesis by A8;
  end;
  then reconsider p as XFinSequence of D by RELAT_1:def 19;
  reconsider p2=Replace(p,0,d) as XFinSequence of D;
A19: for i st 1<=i & i<=len q holds p2.i=q.i
  proof
    let i;
    assume that
A20: 1<=i and
A21: i<=len q;
    i<len q or i=len q by A21,XXREAL_0:1;
    then
A22: i in len q or i=len q by NAT_1:44;
    i<n by A2,A21,XXREAL_0:2;
    then
A23: i in n by NAT_1:44;
    i in NAT by ORDINAL1:def 12;
    hence p2.i=p.i by A20,AFINSQ_1:44
      .=F(i) by A6,A23
      .=IFLGT(i,len q,q.i,q.i,d) by A20,FUNCOP_1:def 8
      .=q.i by A22,Def2;
  end;
A24: len p2=len p by AFINSQ_1:44;
  p2.0 =len q by A2,A4,A5,AFINSQ_1:44;
  then p2 is_an_xrep_of q by A1,A2,A5,A24,A19,Def1;
  hence thesis by A5,A24;
end;

:: Non-overwriting program calculating inner product of vectors
::#define V_SIZE 1024
:: float inner_prd_prg(float a[V_SIZE],float b[V_SIZE]){
::    int n,i; float s[V_SIZE];
::        s[0]=0;
::        n=(int)(b[0]);
::        if (n != 0)
::         { for(i=0;i<n;i++)s[i+1]=s[i]+a[i+1]*b[i+1];
::         }
::     return s[n];
::   }

definition
  let a,b be XFinSequence of REAL;
  assume that
A1: b.0 is Nat and
A2: b.0 < len a;
  func inner_prd_prg(a,b) -> Real means
  :Def3:
  ex s being XFinSequence of REAL
  , n being Integer st len s=len a & s.0=0 & n= b.0 & (n<>0 implies for i being
  Nat st i<n holds s.(i+1)=s.i + (a.(i+1))*(b.(i+1)) ) & it=s.n;
  existence
  proof
    reconsider q0=<%0%> as XFinSequence of REAL;
    set n2=len a;
    reconsider nn2=b.0 as Nat by A1;
    reconsider nn=nn2 as Integer;
    defpred P[Nat] means ex q being XFinSequence of REAL st (len q=
$1+1 & q.0=0 & (for k st k<$1 & k<nn2 holds q.(k+1)=q.k+(a.(k+1))*(b.(k+1))));
A3: for k st k< 0 & k<nn2 holds q0.(k+1)=q0.k+(a.(k+1))*(b.(k+1));
A4: for k be Nat st P[k] holds P[k + 1]
    proof
      let k be Nat;
      reconsider k0=k as Nat;
      assume P[k];
      then consider q2 being XFinSequence of REAL such that
A5:   len q2= k+1 and
A6:   q2.0=0 and
A7:   for k2 being Nat st k2<k & k2<nn2 holds q2.(k2+1) =q2.k2+(a.(k2
      +1)) *(b.(k2+1));
      reconsider qab=q2.k0+(a.(k0+1))*(b.(k0+1)) as Real;
      set q3=q2^<% qab %>;
      0 in len q2 by A5,NAT_1:44;
      then
A8:   q3.0 =0 by A6,AFINSQ_1:def 3;
A9:   for k2 being Nat st k2<k+1 & k2<nn2 holds q3.(k2+1) =q3.k2+(a.(k2+1
      ))*(b.(k2+1))
      proof
        let k2 be Nat;
        assume that
A10:    k2<k+1 and
A11:    k2<nn2;
A12:    k2<=k by A10,NAT_1:13;
        now
          per cases by A12,XXREAL_0:1;
          case
A13:        k2<k;
            then k2< len q2 by A5,NAT_1:13;
            then k2 in dom q2 by NAT_1:44;
            then
A14:        q3.(k2)=q2.(k2) by AFINSQ_1:def 3;
            k2+1<k+1 by A13,XREAL_1:6;
            then k2+1 in len q2 by A5,NAT_1:44;
            then q3.(k2+1)=q2.(k2+1) by AFINSQ_1:def 3;
            hence thesis by A7,A11,A13,A14;
          end;
          case
A15:        k2=k;
            0 in 1 by NAT_1:44;
            then
            (<% q2.k0+(a.(k0+1))*(b.(k0+1)) %>).0 = q2.k0+(a.(k0+1))*(b.(
k0+1)) & 0 in dom (<% q2.k0+(a.(k0+1))*(b.(k0+1)) %>) by AFINSQ_1:def 4;
            then
A16:        q3.(k2+1+0) =q2.(k0)+(a.(k0+1))*(b.(k0+1)) by A5,A15,AFINSQ_1:def 3
;
            k2<k2+1 by NAT_1:13;
            then k2 in dom q2 by A5,A15,NAT_1:44;
            hence thesis by A15,A16,AFINSQ_1:def 3;
          end;
        end;
        hence thesis;
      end;
      len q3=len q2+len (<% q2.k0+(a.(k0+1))*(b.(k0+1)) %>) by AFINSQ_1:17
        .=k+1+1 by A5,AFINSQ_1:33;
      hence thesis by A8,A9;
    end;
    len q0=1 & q0.0=0 by AFINSQ_1:def 4;
    then
A17: P[0] by A3;
    for k being Nat holds P[k] from NAT_1:sch 2(A17,A4);
    then consider q being XFinSequence of REAL such that
A18: len q=n2-'1+1 & q.0=0 and
A19: for k3 being Nat st k3<n2-'1 & k3<nn2 holds q.(k3+1)=q.k3+(a.(k3+
    1 ))*(b.(k3+1));
    reconsider ss2=q.nn2 as Real;
    n2>=0+1 by A1,A2,NAT_1:13;
    then n2-1>=0 by XREAL_1:48;
    then
A20: n2-'1=n2-1 by XREAL_0:def 2;
    nn<>0 implies for i being Nat st i<nn holds q.(i+1)=q.i + (a.(i+1))*(
    b.(i+1))
    proof
      assume nn<>0;
      thus for i being Nat st i<nn holds q.(i+1)=q.i + (a.(i+1))*(b.(i+1))
      proof
        let i be Nat;
        assume
A21:    i<nn;
        nn+1<=n2 by A2,NAT_1:13;
        then nn+1-1<=n2-1 by XREAL_1:9;
        then i<n2-'1 by A20,A21,XXREAL_0:2;
        hence thesis by A19,A21;
      end;
    end;
    then
    ex s being XFinSequence of REAL, n being Integer st len s=len a & s.0
=0 & n=b.0 & (n<>0 implies for i being Nat st i<n holds s.(i+1)=s.i + (a.(i+1))
    *(b.(i+1)) ) & ss2=s.n by A18,A20;
    hence thesis;
  end;
  uniqueness
  proof
    thus for w1,w2 being Real st (ex s being XFinSequence of REAL, n1 being
Integer st len s=len a & s.0=0 & n1=b.0 & (n1<>0 implies for i being Nat st i<
    n1 holds s.(i+1)=s.i + (a.(i+1))*(b.(i+1)) ) & w1=s.n1) & ( ex s being
XFinSequence of REAL, n2 being Integer st len s=len a & s.0=0 & n2=b.0 & (n2<>0
implies for i being Nat st i<n2 holds s.(i+1)=s.i + (a.(i+1))*(b.(i+1)) ) & w2=
    s.n2) holds w1=w2
    proof
      let w1,w2 be Real;
      assume that
A22:  ex s being XFinSequence of REAL, n1 being Integer st len s=len
a & s.0 =0 & n1=b.0 & (n1<>0 implies for i being Nat st i<n1 holds s.(i+1)=s.i
      + (a.(i+ 1))*(b.(i+1)) ) & w1=s.n1 and
A23:  ex s being XFinSequence of REAL, n2 being Integer st len s=len
a & s.0=0 & n2=b.0 & (n2<>0 implies for i being Nat st i<n2 holds s.(i+1)=s.i +
      ( a.(i+1))*(b.(i+1))) & w2=s.n2;
      consider s1 being XFinSequence of REAL, n1 being Integer such that
      len s1=len a and
A24:  s1.0=0 and
A25:  n1=b.0 and
A26:  n1<>0 implies for i being Nat st i<n1 holds s1.(i+1)=s1.i + (a.
      (i+ 1))*(b.(i+1)) and
A27:  w1=s1.n1 by A22;
      consider s2 being XFinSequence of REAL, n2 being Integer such that
      len s2 =len a and
A28:  s2.0=0 and
A29:  n2=b.0 and
A30:  n2<>0 implies for i being Nat st i<n2 holds s2.(i+1)=s2.i + (a.
      (i+ 1))*(b.(i+1)) and
A31:  w2=s2.n2 by A23;
      reconsider n=n1 as Nat by A1,A25;
      defpred P2[Nat] means $1<=n implies s1.$1=s2.$1;
A32:  for k being Nat st P2[k] holds P2[k+1]
      proof
        let k be Nat;
        assume
A33:    P2[k];
        now
          assume k+1<=n; then
A34:      k<n by NAT_1:13;
          then s1.(k+1)=s1.k + (a.(k+1))*(b.(k+1)) by A26;
          hence s1.(k+1)=s2.(k+1) by A25,A29,A30,A33,A34;
        end;
        hence thesis;
      end;
A35:  P2[0] by A24,A28;
      for k being Nat holds P2[k] from NAT_1:sch 2(A35,A32);
      hence thesis by A25,A27,A29,A31;
    end;
  end;
end;

theorem Th3:
  for a being FinSequence of REAL, s being XFinSequence of REAL st
  s.0=0 & (for i st i<len a holds s.(i+1)=s.i+a.(i+1)) holds Sum a =s.(len a)
proof
  let a be FinSequence of REAL, s be XFinSequence of REAL;
  assume that
A1: s.0=0 and
A2: for i st i<len a holds s.(i+1)=s.i+a.(i+1);
  defpred P[Nat] means $1<=len a implies Sum (a|$1)=s.($1);
A3: for k st P[k] holds P[k+1]
  proof
    let k;
    reconsider k1=k as Element of NAT by ORDINAL1:def 12;
    reconsider m=k1+1 as Nat;
    assume
A4: P[k];
    k+1<=len a implies Sum (a|m)=s.(k+1)
    proof
      reconsider x0=<*a/.m*> as FinSequence of REAL;
      reconsider rx=a/.m as Element of REAL;
      reconsider q0=a|k as FinSequence of REAL;
      assume
A5:   k+1<=len a;
      then
A6:   a|m = (a|k)^<*a/.m*> by FINSEQ_5:82;
A7:   1<=k+1 by NAT_1:11;
      then m in Seg len a by A5,FINSEQ_1:1;
      then
A8:   m in dom a by FINSEQ_1:def 3;
      m in Seg m by A7,FINSEQ_1:1;
      then m in Seg (len (a|m)) by A5,FINSEQ_1:59;
      then
A9:   m in dom (a|m) by FINSEQ_1:def 3;
      Sum x0=rx by RVSUM_1:73;
      then
A10:  Sum (a|m) =s.(k)+rx by A4,A5,A6,NAT_1:13,RVSUM_1:75;
A11:  len (a|m)=m by A5,FINSEQ_1:59;
A12:  k<len a by A5,NAT_1:13;
      len (a|m) =len q0 + len (<*rx*>) by A6,FINSEQ_1:22
        .=len q0 +1 by FINSEQ_1:40;
      then rx=(a|m).m by A6,A11,FINSEQ_1:42
        .=(a|m)/.m by A9,PARTFUN1:def 6
        .=a/.m by A9,FINSEQ_4:70
        .=a.m by A8,PARTFUN1:def 6;
      hence thesis by A2,A12,A10;
    end;
    hence thesis;
  end;
A13: P[0] by A1,RVSUM_1:72;
  for k holds P[k] from NAT_1:sch 2(A13,A3);
  then P[len a];
  hence thesis by FINSEQ_1:58;
end;

theorem
  for a being FinSequence of REAL holds ex s being XFinSequence of REAL
st len s=len a +1 & s.0=0 & (for i st i<len a holds s.(i+1)=s.i+a.(i+1)) & Sum
  a =s.(len a)
proof
  let a be FinSequence of REAL;
  deffunc F(Nat) = Sum (a|$1);
  ex p being XFinSequence st len p = len a +1 & for k be Nat
  st k in len a+1 holds p.k=F(k) from AFINSQ_1:sch 2;
  then consider p being XFinSequence such that
A1: len p = len a +1 and
A2: for k be Nat st k in len a+1 holds p.k=F(k);
  rng p c= REAL
  proof
    let y be set;
    assume y in rng p;
    then consider x being set such that
A3: x in dom p and
A4: y=p.x by FUNCT_1:def 3;
    reconsider nx=x as Element of NAT by A3;
    p.nx =Sum(a|nx) by A1,A2,A3;
    hence thesis by A4;
  end;
  then reconsider p as XFinSequence of REAL by RELAT_1:def 19;
A5: for i st i<len a holds p.(i+1)=p.i+a.(i+1)
  proof
    let i;
    assume
A6: i<len a;
    reconsider i as Element of NAT by ORDINAL1:def 12;
    reconsider ii=i+1 as Nat;
A7: i+1<=len a by A6,NAT_1:13;
    1<=1+i by NAT_1:11;
    then i+1 in Seg len a by A7,FINSEQ_1:1;
    then
A8: i+1 in dom a by FINSEQ_1:def 3;
    i<len a+1 by A6,NAT_1:13;
    then i in len a+1 by NAT_1:44;
    then
A9: p.i=Sum (a|i) by A2;
    i+1<len a+1 by A6,XREAL_1:6;
    then
A10: i+1 in len a +1 by NAT_1:44;
    a|ii=(a|i)^<*a/.ii*> by A7,FINSEQ_5:82;
    then Sum(a|ii)=Sum(a|i)+Sum(<*a/.ii*>) by RVSUM_1:75
      .=p.i +a/.ii by A9,RVSUM_1:73
      .=p.i +a.ii by A8,PARTFUN1:def 6;
    hence thesis by A2,A10;
  end;
  0 in len a +1 by NAT_1:44;
  then
A11: p.0=F(0) by A2
    .=0 by RVSUM_1:72;
  then Sum a=p.(len a) by A5,Th3;
  hence thesis by A1,A11,A5;
end;

theorem
  for a,b being FinSequence of REAL, n being Nat st len a=len b & n>len
  a holds |(a,b)| = inner_prd_prg(FS2XFS*(a,n),FS2XFS*(b,n))
proof
  let a,b be FinSequence of REAL, n2 be Nat;
  assume that
A1: len a=len b and
A2: n2>len a;
  reconsider rb=b as Element of (len a)-tuples_on REAL by A1,FINSEQ_2:92;
  reconsider ra=a as Element of (len a)-tuples_on REAL by FINSEQ_2:92;
  set ri= inner_prd_prg(FS2XFS*(a,n2),FS2XFS*(b,n2));
  set pa= FS2XFS*(a,n2);
  set pb= FS2XFS*(b,n2);
A3: len b = (pb.0) by A1,A2,AFINSQ_1:def 10;
  len pa=n2 by A2,AFINSQ_1:def 10;
  then consider s being XFinSequence of REAL, n being Integer such that
  len s=len pa and
A4: s.0=0 and
A5: n=pb.0 and
A6: n<>0 implies for i being Nat st i<n holds s.(i+1)=s.i + (pa.(i+1))*
  (pb.(i+1)) and
A7: ri=s.n by A1,A2,A3,Def3;
A8: len mlt(ra,rb)=len a by CARD_1:def 7;
  for i st i<len mlt(a,b) holds s.(i+1)=s.i+(mlt(a,b)).(i+1)
  proof
    let i;
    assume
A9: i<len mlt(a,b);
    then
 1<=i+1 & i+1<=len a by A8,NAT_1:11,13;
then A10: pa.(i+1)=a.(i+1) & pb.(i+1)=b.(i+1) by A1,A2,AFINSQ_1:def 10;
A11: i<n by A1,A2,A5,A8,A9,AFINSQ_1:def 10;
    now
      per cases;
      case n<>0;
        s.(i+1)=s.i + (pa.(i+1))*(pb.(i+1)) by A6,A11
          .=s.i+(mlt(a,b)).(i+1) by A10,RVSUM_1:59;
        hence thesis;
      end;
      case n=0;
        hence contradiction by A1,A2,A5,A8,A9,AFINSQ_1:def 10;
      end;
    end;
    hence thesis;
  end;
  then Sum mlt(a,b) =s.n by A1,A3,A4,A5,A8,Th3;
  hence thesis by A7,RVSUM_1:def 16;
end;

:: Vector Calculation Program: Scalar Product of Vector
::
:: The following C program is correct if it is used under some limited
::conditions, which are shown in the theorem following the definition
::after this program.
:: But it still remains a possibility of overflow.
:: The following program does not take an explicit function form.
::It means the value of the function does not have a sense.
::The result of the calculation is
::given in a variable c. Precisely speaking, the result is not unique,
::because of the difference of initial value of c.
::  For a model of such a program, we propose the logical predicate form
::(we call such a model, Logical-Model of a program) in the following
::definition.
::
::#define V_SIZE 1024
::void scalar_prd_prg(float c[V_SIZE], float a, float b[V_SIZE])
::{       int n,i;
::        c[0]=b[0];
::        n=(int)(b[0]);
::        if (n != 0)
::         { for(i=1;i<=n;i++)c[i]=a*b[i];
::         }
::        return;
::}
::The following definition is Logical-Model of the above program.

definition
  let b,c be XFinSequence of REAL,a be Real,m be Integer;
  pred m scalar_prd_prg c,a,b means
  :Def4:
  len c =m & len b =m & ex n being
Integer st c.0=b.0 & n=b.0 & (n<>0 implies for i being Nat st 1<=i & i<=n holds
  c.i=a*(b.i));
end;

theorem
  for b being non empty XFinSequence of REAL, a being Real,m being Nat
  st b.0 is Nat & len b=m & b.0 < m holds (ex c being XFinSequence of REAL st m
  scalar_prd_prg c,a,b)& for c being non empty XFinSequence of REAL st m
  scalar_prd_prg c,a,b holds (XFS2FS*(c))=a*(XFS2FS*(b))
proof
  let b be non empty XFinSequence of REAL,a be Real,m be Nat;
  assume that
A1: b.0 is Nat and
A2: len b=m and
A3: b.0 < m;
  reconsider k= b.0 as Nat by A1;
  reconsider c2= a*(XFS2FS*(b)) as FinSequence of REAL;
  dom(a*(XFS2FS*(b))) = dom (XFS2FS*(b)) by VALUED_1:def 5;
  then
A4: Seg len (a*(XFS2FS*(b)))= dom (XFS2FS*(b)) by FINSEQ_1:def 3;
A5: b.0 in m by A1,A3,NAT_1:44;
  then len (XFS2FS*(b)) = b.0 by A2,AFINSQ_1:def 11;
  then
A6: len c2 =k by A4,FINSEQ_1:def 3;
  then consider p being XFinSequence of REAL such that
A7: len p=m and
A8: p is_an_xrep_of c2 by A3,Th2;
  reconsider p2=Replace(p,0,b.0) as XFinSequence of REAL;
A9: now
    assume k<>0;
    thus for i being Nat st 1<=i & i<=k holds p2.i=a*(b.i)
    proof
      let i be Nat;
      assume that
A10:  1<=i and
A11:  i<=k;
      (XFS2FS*(b)).i= b.i by A2,A5,A10,A11,AFINSQ_1:def 11;
      then
A12:  (a*(XFS2FS*(b))).i = a*(b.i) by RVSUM_1:44;
      i in NAT & p.i=c2.i by A6,A8,A10,A11,Def1,ORDINAL1:def 12;
      hence thesis by A10,A12,AFINSQ_1:44;
    end;
  end;
  len p=len p2 & p2.0=b.0 by A1,A3,A7,AFINSQ_1:44;
  then m scalar_prd_prg p2,a,b by A2,A7,A9,Def4;
  hence ex c being XFinSequence of REAL st m scalar_prd_prg c,a,b;
A13: 0 < len b;
  thus for c being non empty XFinSequence of REAL st m scalar_prd_prg c,a,b
  holds (XFS2FS*(c))=a*(XFS2FS*(b))
  proof
    let c be non empty XFinSequence of REAL;
    assume
A14: m scalar_prd_prg c,a,b;
    then consider n being Integer such that
A15: c.0=b.0 and
A16: n=b.0 and
A17: n<>0 implies for i being Nat st 1<=i & i<=n holds c.i=a*(b.i) by Def4;
A18: len c =m & ex n being Integer st c.0=b.0 & n=b.0 & (n<>0 implies for
    i being Nat st 1<=i & i<=n holds c.i=a*(b.i)) by A14,Def4;
    then
A19: len (XFS2FS*(c)) = (c.0) by A5,AFINSQ_1:def 11;
    now
      per cases;
      case
        n=0;
        then
        (XFS2FS*(b))=<*>REAL & (XFS2FS*(c))=<*>REAL by A13,A18,A16,AFINSQ_1:64;
        hence thesis by RVSUM_1:46;
      end;
      case
        n<>0;
        set p3=(XFS2FS*(c));
        for k3 being Nat st 1 <=k3 & k3 <= len p3 holds p3.k3=c2.k3
        proof
          let k3 be Nat;
          assume that
A20:      1 <=k3 and
A21:      k3 <= len p3;
A22:      (c.0) in len c by A1,A3,A18,NAT_1:44;
          then
A23:      k3 <= n by A15,A16,A21,AFINSQ_1:def 11;
          then
A24:      b.k3 = (XFS2FS*(b)).k3 by A2,A5,A16,A20,AFINSQ_1:def 11;
          len p3=n by A15,A16,A22,AFINSQ_1:def 11;
          then p3.k3=c.k3 by A15,A16,A20,A21,A22,AFINSQ_1:def 11
            .=a*(b.k3) by A17,A20,A23;
          hence thesis by A24,RVSUM_1:44;
        end;
        hence thesis by A6,A15,A19,FINSEQ_1:14;
      end;
    end;
    hence thesis;
  end;
end;

:: Vector Calculation Program: Minus Vector
::#define V_SIZE 1024
::void vector_minus_prg(float c[V_SIZE], float b[V_SIZE])
::{       int n,i;
::        c[0]=b[0];
::        n=(int)(b[0]);
::        if (n != 0)
::         { for(i=1;i<=n;i++)c[i]= -b[i];
::         }
::        return;
::}
::The following definition is Logical-Model of the above program.

definition
  let b,c be XFinSequence of REAL,m be Integer;
  pred m vector_minus_prg c,b means
  :Def5:
  len c =m & len b =m & ex n being
  Integer st c.0=b.0 & n= b.0 & (n<>0 implies for i being Nat st 1<=i & i<=n
  holds c.i= -(b.i));
end;

theorem
  for b being non empty XFinSequence of REAL,m being Nat st b.0 is Nat &
len b=m & b.0 < m holds (ex c being XFinSequence of REAL st m vector_minus_prg
  c,b)& for c being non empty XFinSequence of REAL st m vector_minus_prg c,b
  holds (XFS2FS*(c))= -(XFS2FS*(b))
proof
  let b be non empty XFinSequence of REAL,m be Nat;
  assume that
A1: b.0 is Nat and
A2: len b=m and
A3: b.0 < m;
  reconsider k= b.0 as Nat by A1;
  reconsider c2= -(XFS2FS*(b)) as FinSequence of REAL;
  dom( -(XFS2FS*(b))) = dom (XFS2FS*(b)) by VALUED_1:8;
  then
A4: Seg len ( -(XFS2FS*(b)))= dom (XFS2FS*(b)) by FINSEQ_1:def 3;
A5: b.0 in m by A1,A3,NAT_1:44;
  then len (XFS2FS*(b)) = b.0 by A2,AFINSQ_1:def 11;
  then
A6: len c2 =k by A4,FINSEQ_1:def 3;
  then consider p being XFinSequence of REAL such that
A7: len p=m and
A8: p is_an_xrep_of c2 by A3,Th2;
  reconsider p2=Replace(p,0,b.0) as XFinSequence of REAL;
A9: k<>0 implies for i being Nat st 1<=i & i<=k holds p2.i= -(b.i)
  proof
    assume k<>0;
    let i be Nat;
    assume that
A10: 1<=i and
A11: i<=k;
    (XFS2FS*(b)).i= b.i by A2,A5,A10,A11,AFINSQ_1:def 11;
    then
A12: ( -(XFS2FS*(b))).i = -(b.i) by RVSUM_1:17;
    i in NAT & p.i=c2.i by A6,A8,A10,A11,Def1,ORDINAL1:def 12;
    hence thesis by A10,A12,AFINSQ_1:44;
  end;
  len p=len p2 & p2.0=b.0 by A1,A3,A7,AFINSQ_1:44;
  then m vector_minus_prg p2,b by A2,A7,A9,Def5;
  hence ex c being XFinSequence of REAL st m vector_minus_prg c,b;
A13: 0 < len b;
  thus for c being non empty XFinSequence of REAL st m vector_minus_prg c,b
  holds (XFS2FS*(c))= -(XFS2FS*(b))
  proof
    let c be non empty XFinSequence of REAL;
    assume
A14: m vector_minus_prg c,b;
    then consider n being Integer such that
A15: c.0=b.0 and
A16: n=b.0 and
A17: n<>0 implies for i being Nat st 1<=i & i<=n holds c.i= -(b.i) by Def5;
A18: len c =m & ex n being Integer st c.0=b.0 & n=b.0 & (n<>0 implies for
    i being Nat st 1<=i & i<=n holds c.i= -(b.i)) by A14,Def5;
    then
A19: len (XFS2FS*(c)) = (c.0) by A5,AFINSQ_1:def 11;
    now
      per cases;
      case
A20:    n=0;
        then (XFS2FS*(b))=<*>REAL by A13,A16,AFINSQ_1:64;
        hence thesis by A18,A16,A20,AFINSQ_1:64,RVSUM_1:19;
      end;
      case
        n<>0;
        set p3=(XFS2FS*(c));
        for k3 being Nat st 1 <=k3 & k3 <= len p3 holds p3.k3=c2.k3
        proof
          let k3 be Nat;
A21:      (c.0) in len c by A1,A3,A18,NAT_1:44;
          then
A22:      len p3=n by A15,A16,AFINSQ_1:def 11;
          assume
A23:      1 <=k3 & k3 <= len p3;
          then
A24:      b.k3 = (XFS2FS*b).k3 by A2,A5,A16,A22,AFINSQ_1:def 11;
          p3.k3=c.k3 by A15,A16,A23,A21,A22,AFINSQ_1:def 11
            .= -(b.k3) by A17,A23,A22;
          hence thesis by A24,RVSUM_1:17;
        end;
        hence thesis by A6,A15,A19,FINSEQ_1:14;
      end;
    end;
    hence thesis;
  end;
end;

:: Vector Calculation Program: Sum of Vectors
::
:: The following program is the same type of scalar_prd_prg, but gives a result
:: a+b in a variable c.
::
::#define V_SIZE 1024
::void vector_add_prg(float c[V_SIZE], float a[V_SIZE], float b[V_SIZE])
::{       int n,i;
::        c[0]=b[0];
::        n=(int)(b[0]);
::        if (n != 0)
::         { for(i=1;i<=n;i++)c[i]=a[i]+b[i];
::         }
::        return;
::}

definition
  let a,b,c be XFinSequence of REAL,m be Integer;
  pred m vector_add_prg c,a,b means
  :Def6:
  len c =m & len a=m & len b =m & ex
n being Integer st c.0=b.0 & n=b.0 & (n<>0 implies for i being Nat st 1<=i & i
  <=n holds c.i=(a.i)+(b.i) );
end;

theorem
  for a,b being non empty XFinSequence of REAL, m being Nat st b.0 is
  Nat & len a=m & len b=m & a.0=b.0 & b.0 < m holds (ex c being XFinSequence of
REAL st m vector_add_prg c,a,b)& for c being non empty XFinSequence of REAL st
  m vector_add_prg c,a,b holds (XFS2FS*(c))=(XFS2FS*(a))+(XFS2FS*(b))
proof
  let a,b be non empty XFinSequence of REAL,m be Nat;
  assume that
A1: b.0 is Nat and
A2: len a=m and
A3: len b=m and
A4: (a.0)=b.0 and
A5: b.0 < m;
  reconsider k= b.0 as Nat by A1;
  reconsider Fb=(XFS2FS*(b)) as FinSequence of REAL;
  reconsider Fa=(XFS2FS*(a)) as FinSequence of REAL;
  reconsider c2= Fa + Fb as FinSequence of REAL;
A6: b.0 in m by A1,A5,NAT_1:44;
  then
A7: len (XFS2FS*(a)) = b.0 by A2,A4,AFINSQ_1:def 11;
A8: len (XFS2FS*(b)) = b.0 by A3,A6,AFINSQ_1:def 11;
  then
A9: len c2=len (XFS2FS*(a)) by A7,RVSUM_1:115;
  then dom c2= Seg len (XFS2FS*(b)) by A8,A7,FINSEQ_1:def 3;
  then dom((XFS2FS*(a))+(XFS2FS*(b))) = dom (XFS2FS*(b)) by FINSEQ_1:def 3;
  then Seg len (c2) = dom (XFS2FS*(b)) by FINSEQ_1:def 3;
  then
A10: len c2 =k by A8,FINSEQ_1:def 3;
  then consider p being XFinSequence of REAL such that
A11: len p=m and
A12: p is_an_xrep_of c2 by A5,Th2;
  reconsider p2=Replace(p,0,b.0) as XFinSequence of REAL;
A13: now
    assume k<>0;
    thus for i being Nat st 1<=i & i<=k holds p2.i=(a.i)+(b.i)
    proof
      let i be Nat;
      assume that
A14:  1<=i and
A15:  i<=k;
      i in Seg len c2 by A7,A9,A14,A15,FINSEQ_1:1;
      then
A16:  i in dom c2 by FINSEQ_1:def 3;
      (XFS2FS*(a)).i= a.i & (XFS2FS*(b)).i= b.i
        by A2,A3,A4,A6,A14,A15,AFINSQ_1:def 11;
      then
A17:  ((XFS2FS*(a))+(XFS2FS*(b))).i = (a.i)+(b.i) by A16,VALUED_1:def 1;
      i in NAT & p.i=c2.i by A10,A12,A14,A15,Def1,ORDINAL1:def 12;
      hence thesis by A14,A17,AFINSQ_1:44;
    end;
  end;
  len p=len p2 & p2.0=b.0 by A1,A5,A11,AFINSQ_1:44;
  then m vector_add_prg p2,a,b by A2,A3,A11,A13,Def6;
  hence ex c being XFinSequence of REAL st m vector_add_prg c,a,b;
A18: 0 < len b;
  thus for c being non empty XFinSequence of REAL st m vector_add_prg c,a,b
  holds (XFS2FS*(c))=(XFS2FS*(a))+(XFS2FS*(b))
  proof
    let c be non empty XFinSequence of REAL;
    assume
A19: m vector_add_prg c,a,b;
    then consider n being Integer such that
A20: c.0=b.0 and
A21: n=b.0 and
A22: n<>0 implies for i being Nat st 1<=i & i<=n holds c.i=(a.i)+(b.i)
    by Def6;
A23: len c =m & ex n being Integer st c.0=b.0 & n=b.0 & (n<>0 implies for
    i being Nat st 1<=i & i<=n holds c.i=(a.i)+(b.i)) by A19,Def6;
    then
A24: len (XFS2FS*(c)) = (c.0) by A6,AFINSQ_1:def 11;
    now
      per cases;
      case
        n=0;
        then
        (XFS2FS*(b))=<*>REAL & (XFS2FS*(c))=<*>REAL by A18,A23,A21,AFINSQ_1:64;
        hence thesis by RVSUM_1:12;
      end;
      case
        n<>0;
        set p3=(XFS2FS*(c));
        for k3 being Nat st 1 <=k3 & k3 <= len p3 holds p3.k3=c2.k3
        proof
          let k3 be Nat;
          assume that
A25:      1 <=k3 and
A26:      k3 <= len p3;
A27:      (c.0) in len c by A1,A5,A23,NAT_1:44;
          then
A28:      k3 <= n by A20,A21,A26,AFINSQ_1:def 11;
          then
A29:      a.k3 = (XFS2FS*(a)).k3 & b.k3 = (XFS2FS*(b)).k3 by A2,A3,A4,A6,A21
,A25,AFINSQ_1:def 11;
          k3 in Seg len c2 by A10,A21,A25,A28,FINSEQ_1:1;
          then
A30:      k3 in dom c2 by FINSEQ_1:def 3;
          len p3=n by A20,A21,A27,AFINSQ_1:def 11;
          then p3.k3=c.k3 by A20,A21,A25,A26,A27,AFINSQ_1:def 11
            .=(a.k3)+(b.k3) by A22,A25,A28;
          hence thesis by A30,A29,VALUED_1:def 1;
        end;
        hence thesis by A10,A20,A24,FINSEQ_1:14;
      end;
    end;
    hence thesis;
  end;
end;

:: Vector Calculation Program: Subtraction of Vectors
::
:: The following program is the same type of scalar_prd_prg, but gives a result
:: a-b in a variable c.
::
::#define V_SIZE 1024
::void vector_sub_prg(float c[V_SIZE], float a[V_SIZE], float b[V_SIZE])
::{       int n,i;
::        c[0]=b[0];
::        n=(int)(b[0]);
::        if (n != 0)
::         { for(i=1;i<=n;i++)c[i]=a[i]-b[i];
::         }
::        return;
::}

definition
  let a,b,c be XFinSequence of REAL,m be Integer;
  pred m vector_sub_prg c,a,b means  :Def7:
  len c =m & len a=m & len b =m & ex n being Integer st c.0=b.0 & n=b.0 &
  (n<>0 implies for i being Nat st 1<=i & i <=n holds c.i=(a.i)-(b.i) );
end;

theorem
  for a,b being non empty XFinSequence of REAL, m being Nat st b.0 is
  Nat & len a=m & len b=m & a.0=b.0 & b.0 < m holds (ex c being XFinSequence of
REAL st m vector_sub_prg c,a,b) & for c being non empty XFinSequence of REAL st
  m vector_sub_prg c,a,b holds XFS2FS*(c)=XFS2FS*(a)-XFS2FS*(b)
proof
  let a,b be non empty XFinSequence of REAL,m be Nat;
  assume that
A1: b.0 is Nat and
A2: len a=m and
A3: len b=m and
A4: a.0=b.0 and
A5: b.0 < m;
  reconsider k= b.0 as Nat by A1;
  reconsider Fb=(XFS2FS*(b)) as FinSequence of REAL;
  reconsider Fa=(XFS2FS*(a)) as FinSequence of REAL;
  reconsider c2= Fa - Fb as FinSequence of REAL;
A6: b.0 in m by A1,A5,NAT_1:44;
  then
A7: len (XFS2FS*(a)) = b.0 by A2,A4,AFINSQ_1:def 11;
A8: len (XFS2FS*(b)) = b.0 by A3,A6,AFINSQ_1:def 11;
  then
A9: len c2=len (XFS2FS*(a)) by A7,RVSUM_1:116;
  then dom c2= Seg len (XFS2FS*(b)) by A8,A7,FINSEQ_1:def 3;
  then dom((XFS2FS*(a))-(XFS2FS*(b))) = dom (XFS2FS*(b)) by FINSEQ_1:def 3;
  then Seg len (c2) = dom (XFS2FS*(b)) by FINSEQ_1:def 3;
  then
A10: len c2 =k by A8,FINSEQ_1:def 3;
  then consider p being XFinSequence of REAL such that
A11: len p=m and
A12: p is_an_xrep_of c2 by A5,Th2;
  reconsider p2=Replace(p,0,b.0) as XFinSequence of REAL;
A13: now
    assume k<>0;
    thus for i being Nat st 1<=i & i<=k holds p2.i=(a.i)-(b.i)
    proof
      let i be Nat;
      assume that
A14:  1<=i and
A15:  i<=k;
      i in Seg len c2 by A7,A9,A14,A15,FINSEQ_1:1; then
A16:  i in dom c2 by FINSEQ_1:def 3;
      (XFS2FS*(a)).i= a.i & (XFS2FS*(b)).i= b.i
        by A2,A3,A4,A6,A14,A15,AFINSQ_1:def 11; then
A17:  ((XFS2FS*(a))-(XFS2FS*(b))).i = (a.i)-(b.i) by A16,VALUED_1:13;
      i in NAT & p.i=c2.i by A10,A12,A14,A15,Def1,ORDINAL1:def 12;
      hence thesis by A14,A17,AFINSQ_1:44;
    end;
  end;
  len p=len p2 & p2.0=b.0 by A1,A5,A11,AFINSQ_1:44;
  then m vector_sub_prg p2,a,b by A2,A3,A11,A13,Def7;
  hence ex c being XFinSequence of REAL st m vector_sub_prg c,a,b;
A18: 0 < len b;
  thus for c being non empty XFinSequence of REAL st m vector_sub_prg c,a,b
  holds (XFS2FS*(c))=(XFS2FS*(a))-(XFS2FS*(b))
  proof
    let c be non empty XFinSequence of REAL;
    assume
A19: m vector_sub_prg c,a,b;
    then consider n being Integer such that
A20: c.0=b.0 and
A21: n=b.0 and
A22: n<>0 implies for i being Nat st 1<=i & i<=n holds c.i=(a.i)-(b.i)
    by Def7;
A23: len c =m & ex n being Integer st c.0=b.0 & n=b.0 & (n<>0 implies for
    i being Nat st 1<=i & i<=n holds c.i=(a.i)-(b.i)) by A19,Def7;
    then
A24: len (XFS2FS*(c)) = (c.0) by A6,AFINSQ_1:def 11;
    now
      per cases;
      case n=0;
        then
        (XFS2FS*(b))=<*>REAL & (XFS2FS*(c))=<*>REAL by A18,A23,A21,AFINSQ_1:64;
        hence thesis by RVSUM_1:28;
      end;
      case n<>0;
        set p3=(XFS2FS*(c));
        for k3 being Nat st 1 <=k3 & k3 <= len p3 holds p3.k3=c2.k3
        proof
          let k3 be Nat;
          assume that
A25:      1 <=k3 and
A26:      k3 <= len p3;
A27:      (c.0) in len c by A1,A5,A23,NAT_1:44;
          then
A28:      k3 <= n by A20,A21,A26,AFINSQ_1:def 11;
          then
A29:      a.k3 = (XFS2FS*(a)).k3 & b.k3 = (XFS2FS*(b)).k3 by A2,A3,A4,A6,A21
,A25,AFINSQ_1:def 11;
          k3 in Seg len c2 by A10,A21,A25,A28,FINSEQ_1:1;
          then
A30:      k3 in dom c2 by FINSEQ_1:def 3;
A31:      len p3=n by A20,A21,A27,AFINSQ_1:def 11;
          then p3.k3=c.k3 by A20,A21,A25,A26,A27,AFINSQ_1:def 11
            .=(a.k3)-(b.k3) by A22,A25,A26,A31;
          hence thesis by A30,A29,VALUED_1:13;
        end;
        hence thesis by A10,A20,A24,FINSEQ_1:14;
      end;
    end;
    hence thesis;
  end;
end;