:: Reper Algebras
::  by Micha{\l} Muzalewski
::
:: Received May 28, 1992
:: Copyright (c) 1992-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 SUBSET_1, NUMBERS, XBOOLE_0, FINSEQ_1, ARYTM_3, ORDINAL4,
      XXREAL_0, NAT_1, FUNCT_1, ARYTM_1, RELAT_1, FINSEQ_2, FUNCT_4, MIDSP_1,
      STRUCT_0, BINOP_1, QC_LANG1, PRE_TOPC, CARD_1, TARSKI, MIDSP_2, VECTSP_1,
      GROUP_4, SUPINF_2, ROBBINS1, MIDSP_3;
 notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, FUNCT_1, FUNCT_2, BINOP_1,
      STRUCT_0, ALGSTR_0, PRE_TOPC, FINSEQ_1, FINSEQ_2, NUMBERS, ORDINAL1,
      NAT_1, FUNCT_7, MIDSP_1, MIDSP_2, XXREAL_0;
 constructors BINOP_1, NAT_1, FINSEQ_2, FUNCT_7, MIDSP_2, RELSET_1;
 registrations RELSET_1, XREAL_0, NAT_1, FINSEQ_2, STRUCT_0, ORDINAL1,
      XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions MIDSP_1;
 theorems FINSEQ_1, FINSEQ_2, FUNCT_1, MIDSP_1, MIDSP_2, NAT_1, ZFMISC_1,
      FINSEQ_3, XREAL_1, FUNCT_7, XBOOLE_0, TARSKI, ORDINAL1, XXREAL_0, CARD_1;
 schemes FINSEQ_2, FUNCT_2;

begin

reserve n,i,j,k,l for Element of NAT;
reserve D for non empty set;
reserve c,d for Element of D;
reserve p,q,q9,r for FinSequence of D;

theorem
  len p = j+1+k implies ex q,r,c st len q = j & len r = k & p = q^<*c*>^ r
proof
  assume len p = j+1+k;
  then consider q9,r such that
A1: len q9 = j+1 and
A2: len r = k & p = q9^r by FINSEQ_2:23;
  consider q,c such that
A3: q9 = q^<*c*> by A1,FINSEQ_2:19;
  take q,r,c;
  len q9 = len q + 1 by A3,FINSEQ_2:16;
  hence thesis by A1,A2,A3;
end;

theorem
  i in Seg n implies ex j,k st n = j+1+k & i = j+1
proof
  assume
A1: i in Seg(n);
  then 1<=i by FINSEQ_1:1;
  then consider j being Nat such that
A2: i = 1+j by NAT_1:10;
  reconsider j as Element of NAT by ORDINAL1:def 12;
  i<=n by A1,FINSEQ_1:1;
  then consider k being Nat such that
A3: n = j+1+k by A2,NAT_1:10;
  reconsider k as Element of NAT by ORDINAL1:def 12;
  take j,k;
  thus thesis by A2,A3;
end;

theorem
  p = q^<*c*>^r & i = len q + 1 implies (for l st 1 <= l & l <= len q
holds p.l = q.l) & p.i = c & for l st i + 1 <= l & l <= len p holds p.l = r.(l-
  i)
proof
  set q9 = q^<*c*>;
  assume that
A1: p = q9^r and
A2: i = len q + 1;
A3: p = q^(<*c*>^r) by A1,FINSEQ_1:32;
  thus for l st 1 <= l & l <= len q holds p.l = q.l
  proof
    let l;
    assume 1 <= l & l <= len q;
    then l in dom q by FINSEQ_3:25;
    hence thesis by A3,FINSEQ_1:def 7;
  end;
A4: len q9 = i by A2,FINSEQ_2:16;
  i in Seg(i) by A2,FINSEQ_1:3;
  then i in dom q9 by A4,FINSEQ_1:def 3;
  hence p.i = q9.i by A1,FINSEQ_1:def 7
    .= c by A2,FINSEQ_1:42;
  len p = len q9 + len r by A1,FINSEQ_1:22;
  hence thesis by A1,A4,FINSEQ_1:23;
end;

theorem Th4:
  l<=j or l=j+1 or j+2<=l
proof
A1: j+1+1 = j+2;
  l<j+1 or l = j+1 or j+1<l by XXREAL_0:1;
  hence thesis by A1,NAT_1:13;
end;

theorem
  l in Seg(n)\{i} & i=j+1 implies 1<=l & l<=j or i+1<=l & l<=n
proof
  assume that
A1: l in Seg(n)\{i} and
A2: i=j+1;
A3: i+1 = j+2 by A2;
  l in Seg(n) & l<>i by A1,ZFMISC_1:56;
  hence thesis by A2,A3,Th4,FINSEQ_1:1;
end;

definition
  let D,n;
  let p be Element of n-tuples_on D;
  let i,d;
  redefine func p+*(i,d) -> Element of n-tuples_on D;
  coherence
  proof
    dom(p+*(i,d)) = dom p by FUNCT_7:30;
    then len(p+*(i,d)) = len p by FINSEQ_3:29
      .= n by CARD_1:def 7;
    hence p+*(i,d) is Element of n-tuples_on D by FINSEQ_2:92;
  end;
end;

Lm1: for p being Element of n-tuples_on D st i in Seg n holds p+*(i,d).i = d
proof
  let p be Element of n-tuples_on D;
  Seg n = dom p by FINSEQ_2:124;
  hence thesis by FUNCT_7:31;
end;

Lm2: for p being Element of n-tuples_on D for l st l in (dom p)\{i} holds (p+*
(i,d)).l = p.l
proof
  let p being Element of n-tuples_on D;
  let l;
  assume l in (dom p)\{i};
  then not l in {i} by XBOOLE_0:def 5;
  then l <> i by TARSKI:def 1;
  hence thesis by FUNCT_7:32;
end;

::Section 2: Reper Algebra Structure and its properties

begin

definition
  let n;
  struct(MidStr) ReperAlgebraStr over n (#carrier -> set, MIDPOINT -> BinOp of
    the carrier, reper -> Function of n-tuples_on the carrier, the carrier#);
end;

registration
  let n;
  let A be non empty set, m be BinOp of A, r be Function of n-tuples_on A,A;
  cluster ReperAlgebraStr(#A,m,r#) -> non empty;
  coherence;
end;

Lm3: now
  let n;
  let M be MidSp;
  let R be Function of (n+2)-tuples_on the carrier of M, the carrier of M;
  set RA = ReperAlgebraStr (# the carrier of M, the MIDPOINT of M, R #);
  thus RA is MidSp-like
  proof
    let a,b,c,d be Element of RA;
    reconsider a9=a,b9=b,c9=c,d9=d as Element of M;
    thus a@a = a9@a9 .= a by MIDSP_1:def 3;
    consider x9 being Element of M such that
A1: x9@a9 = b9 by MIDSP_1:def 3;
    for a,b be Element of RA, a9,b9 be Element of M st a=a9 & b=b9 holds a
    @b = a9@b9;
    hence a@b = b9@a9 .= b@a;
    reconsider x = x9 as Element of RA;
    thus (a@b)@(c@d) = (a9@b9)@(c9@d9) .= (a9@c9)@(b9@d9) by MIDSP_1:def 3
      .= (a@c)@(b@d);
    take x;
    thus thesis by A1;
  end;
end;

registration
  let n;
  cluster non empty for ReperAlgebraStr over n;
  existence
  proof

set A = the non empty set,m = the BinOp of A,r = the Function of n -tuples_on A
,A;
    take ReperAlgebraStr(#A,m,r#);
    thus thesis;
  end;
end;

registration
  let n;
  cluster MidSp-like for non empty ReperAlgebraStr over n+2;
  existence
  proof
    set M = the MidSp;
    set R = the Function of (n+2)-tuples_on the carrier of M, the carrier of M;
    take ReperAlgebraStr (# the carrier of M, the MIDPOINT of M, R #);
    thus thesis by Lm3;
  end;
end;

reserve RAS for MidSp-like non empty ReperAlgebraStr over n+2;
reserve a,b,d,pii,p9i for Point of RAS;

definition
  let n,RAS,i;
  mode Tuple of i,RAS is Element of i-tuples_on the carrier of RAS;
end;

reserve p,q for Tuple of (n+1),RAS;

definition
  let n,RAS,a;
  redefine func <*a*> -> Tuple of 1,RAS;
  coherence by FINSEQ_2:98;
end;

definition
  let n,RAS,i,j;
  let p be Tuple of i,RAS, q be Tuple of j,RAS;
  redefine func p^q -> Tuple of (i+j),RAS;
  coherence
   proof
     reconsider p as Tuple of i,the carrier of RAS;
     reconsider q as Tuple of j,the carrier of RAS;
     p^q is Tuple of i+j,the carrier of RAS by FINSEQ_2:107;
    hence thesis by FINSEQ_2:131;
   end;
end;

definition
  let n,RAS,a,p;
  func *'(a,p) -> Point of RAS equals
  (the reper of RAS).(<*a*>^p);
  coherence
  proof
    reconsider p9 = <*a*>^p as Tuple of (n+2),RAS;
    (the reper of RAS).p9 is Point of RAS;
    hence thesis;
  end;
end;

theorem
  i in Seg(n+1) implies (p+*(i,d)).i = d & for l st l in (dom p)\{i}
  holds (p+*(i,d)).l = p.l by Lm1,Lm2;

definition
  let n;
  mode Nat of n -> Element of NAT means
    :Def2:
    1<=it & it<=n+1;
  existence
  proof
    take 1;
    0 <= n by NAT_1:2;
    then 0+1 <= n+1 by XREAL_1:7;
    hence thesis;
  end;
end;

reserve m for Nat of n;

theorem Th7:
  i is Nat of n iff i in Seg(n+1)
proof
  i is Nat of n iff 1<=i & i<=n+1 by Def2;
  hence thesis by FINSEQ_1:1;
end;

theorem Th8:
  i<=n implies i+1 is Nat of n
proof
  assume i<=n;
  then
A1: i+1<=n+1 by XREAL_1:7;
  1<=i+1 by NAT_1:11;
  hence thesis by A1,Def2;
end;

theorem Th9:
  (for m holds p.m = q.m) implies p = q
proof
  assume
A1: for m holds p.m = q.m;
  for j be Nat st j in Seg(n+1) holds p.j = q.j
  proof
    let j be Nat;
    assume j in Seg(n+1);
    then reconsider j as Nat of n by Th7;
    p.j = q.j by A1;
    hence thesis;
  end;
  hence thesis by FINSEQ_2:119;
end;

theorem Th10:
  for l being Nat of n st l=i holds (p+*(i,d)).l = d
proof
  let l be Nat of n such that
A1: l = i;
  l in Seg(n+1) by Th7;
  hence thesis by A1,Lm1;
end;

definition
  let n,D;
  let p be Element of (n+1)-tuples_on D;
  let m;
  redefine func p.m -> Element of D;
  coherence
  proof
    reconsider S = Seg(n+1) as non empty set by FINSEQ_1:4;
    m in S & len p = n+1 by Th7,CARD_1:def 7;
    then m in dom p by FINSEQ_1:def 3;
    then rng p c= D & p.m in rng p by FINSEQ_1:def 4,FUNCT_1:def 3;
    hence thesis;
  end;
end;

definition
  let n,RAS;
  attr RAS is being_invariance means
  :Def3:
  for a,b,p,q st (for m holds a@(q.m ) = b@(p.m)) holds a@*'(b,q) = b@*'(a,p);
end;

definition
 let n,RAS,p,i,a;
 redefine func p+*(i,a) -> Tuple of (n+1),RAS;
 coherence
  proof
   thus p+*(i,a) is Tuple of (n+1),RAS;
  end;
end;

definition
  let n,i,RAS;
  pred RAS has_property_of_zero_in i means
  :Def4:
  for a,p holds *'(a,(p+*(i,a) )) = a;
end;

definition
  let n,i,RAS;
  pred RAS is_semi_additive_in i means
  :Def5:
  for a,pii,p st p.i = pii holds *'(a,(p+*(i,a@pii))) = a@*'(a,p);
end;

theorem Th11:
  RAS is_semi_additive_in m implies for a,d,p,q st q = (p+*(m,d))
  holds *'(a,(p+*(m,a@d))) = a@*'(a,q)
proof
  assume
A1: RAS is_semi_additive_in m;
  let a,d,p,q;
  set qq = (q+*(m,a@d));
  assume
A2: q = (p+*(m,d));
A3: qq = (p+*(m,a@d))
  proof
    set pp = (p+*(m,a@d));
    for k being Nat of n holds qq.k = pp.k
    proof
      let k be Nat of n;
      now
        per cases;
        suppose
A4:       k = m;
          pp.m = a@d by Th10;
          hence thesis by A4,Th10;
        end;
        suppose
A5:       k <> m;
          hence qq.k = q.k by FUNCT_7:32
            .= p.k by A2,A5,FUNCT_7:32
            .= pp.k by A5,FUNCT_7:32;
        end;
      end;
      hence thesis;
    end;
    hence thesis by Th9;
  end;
  q.m = d by A2,Th10;
  hence thesis by A1,A3,Def5;
end;

definition
  let n,i,RAS;
  pred RAS is_additive_in i means
  :Def6:
  for a,pii,p9i,p st p.i = pii holds *'
  (a,(p+*(i,pii@p9i))) = *'(a,p)@*'(a,(p+*(i,p9i)));
end;

definition
  let n,i,RAS;
  pred RAS is_alternative_in i means
  :Def7:
  for a,p,pii st p.i = pii holds *'( a,(p+*(i+1,pii))) = a;
end;

reserve W for ATLAS of RAS;
reserve v for Vector of W;

definition
  let n,RAS,W,i;
  mode Tuple of i,W is Element of i-tuples_on the carrier of the algebra of W;
end;

reserve x,y for Tuple of (n+1),W;

theorem
  i in Seg(n+1) implies (x+*(i,v)).i = v & for l st l in (dom x)\{i}
  holds (x+*(i,v)).l = x.l by Lm1,Lm2;

theorem Th13:
  (for l being Nat of n st l=i holds (x+*(i,v)).l = v) & for l,i
  being Nat of n st l<>i holds (x+*(i,v)).l = x.l
proof
  thus for l being Nat of n st l=i holds (x+*(i,v)).l = v
  proof
    let l be Nat of n such that
A1: l = i;
    l in Seg(n+1) by Th7;
    hence thesis by A1,Lm1;
  end;
  thus thesis by FUNCT_7:32;
end;

theorem Th14:
  (for m holds x.m = y.m) implies x = y
proof
  assume
A1: for m holds x.m = y.m;
  for j be Nat st j in Seg(n+1) holds x.j = y.j
  proof
    let j be Nat;
    assume j in Seg(n+1);
    then reconsider j as Nat of n by Th7;
    x.j = y.j by A1;
    hence thesis;
  end;
  hence thesis by FINSEQ_2:119;
end;

scheme
  SeqLambdaD9{n()->Element of NAT,D()->non empty set, F(set)->Element of D()}:
ex z being FinSequence of D() st len z = n()+1 & for j being Nat of n() holds z
  .j = F(j) proof
  reconsider S = Seg(n()+1) as non empty set by FINSEQ_1:4;
  consider z being FinSequence of D() such that
A1: len z = n()+1 and
A2: for j be Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
  take z;
A3: dom z = Seg(n()+1) by A1,FINSEQ_1:def 3;
  for j being Nat of n() holds z.j = F(j)
  proof
    let j be Nat of n();
    j in S by Th7;
    hence thesis by A2,A3;
  end;
  hence thesis by A1;
end;

definition
  let n,RAS,W,a,x;

  func (a,x).W -> Tuple of (n+1),RAS means
  :Def8:
  it.m = (a,x.m).W;
  existence
  proof
    deffunc F(Nat of n)=(a,x.$1).W;
    consider z being FinSequence of (the carrier of RAS) such that
A1: len z = n+1 and
A2: z.m = F(m) from SeqLambdaD9;
    reconsider z as Tuple of (n+1),RAS by A1,FINSEQ_2:92;
    take z;
    thus thesis by A2;
  end;
  uniqueness
  proof
    let p,q such that
A3: for m holds p.m = (a,x.m).W and
A4: for m holds q.m = (a,x.m).W;
    for m holds p.m = q.m
    proof
      let m;
      p.m = (a,x.m).W by A3;
      hence thesis by A4;
    end;
    hence thesis by Th9;
  end;
end;

definition
  let n,RAS,W,a,p;
  func W.(a,p) -> Tuple of (n+1),W means
  :Def9:
  it.m = W.(a,p.m);
  existence
  proof
    deffunc F(Nat of n)=W.(a,p.$1);
    consider z being FinSequence of (the carrier of the algebra of W) such
    that
A1: len z = n+1 and
A2: z.m = F(m) from SeqLambdaD9;
    reconsider z as Tuple of (n+1),W by A1,FINSEQ_2:92;
    take z;
    thus thesis by A2;
  end;
  uniqueness
  proof
    let x,y such that
A3: for m holds x.m = W.(a,p.m) and
A4: for m holds y.m = W.(a,p.m);
    for m holds x.m = y.m
    proof
      let m;
      W.(a,p.m) = x.m by A3;
      hence thesis by A4;
    end;
    hence thesis by Th14;
  end;
end;

theorem Th15:
  W.(a,p) = x iff (a,x).W = p
proof
  thus W.(a,p) = x implies (a,x).W = p
  proof
    assume
A1: W.(a,p) = x;
    now
      let m;
      W.(a,p.m) = x.m by A1,Def9;
      hence (a,x.m).W = p.m by MIDSP_2:33;
    end;
    hence thesis by Def8;
  end;
  thus (a,x).W = p implies W.(a,p) = x
  proof
    assume
A2: (a,x).W = p;
    now
      let m;
      (a,x.m).W = p.m by A2,Def8;
      hence W.(a,p.m) = x.m by MIDSP_2:33;
    end;
    hence thesis by Def9;
  end;
end;

theorem
  W.(a,(a,x).W) = x by Th15;

theorem
  (a,W.(a,p)).W = p by Th15;

definition
  let n,RAS,W,a,x;
  func Phi(a,x) -> Vector of W equals
  W.(a,*'(a,(a,x).W));
  coherence;
end;

theorem Th18:
  W.(a,p) = x & W.(a,b) = v implies (*'(a,p) = b iff Phi(a,x) = v)
proof
  assume that
A1: W.(a,p) = x and
A2: W.(a,b) = v;
  Phi(a,x) = W.(a,*'(a,p)) by A1,Th15;
  hence thesis by A2,MIDSP_2:32;
end;

theorem Th19:
  RAS is being_invariance iff for a,b,x holds Phi(a,x) = Phi(b,x)
proof
A1: (for a,b,x holds Phi(a,x) = Phi(b,x)) implies RAS is being_invariance
  proof
    assume
A2: for a,b,x holds Phi(a,x) = Phi(b,x);
    let a,b,p,q;
A3: W.(a,*'(a,(a,W.(a,p)).W)) = Phi(a,W.(a,p)) .= Phi(b,W.(a,p)) by A2
      .= W.(b,*'(b,(b,W.(a,p)).W));
    assume
A4: for m holds a@(q.m) = b@(p.m);
A5: now
      let m;
      a@(q.m) = b@(p.m) by A4;
      then
A6:   W.(a,p.m) = W.(b,q.m) by MIDSP_2:33;
      thus W.(a,p).m = W.(a,p.m) by Def9
        .= W.(b,q).m by A6,Def9;
    end;
    W.(a,*'(a,p)) = W.(a,*'(a,(a,W.(a,p)).W)) by Th15
      .= W.(b,*'(b,(b,W.(b,q)).W)) by A5,A3,Th14
      .= W.(b,*'(b,q)) by Th15;
    hence thesis by MIDSP_2:33;
  end;
  now
    assume
A7: RAS is being_invariance;
    let a,b,x;
    set p = (a,x).W, q = (b,x).W;
A8: W.(a,p) = x by Th15
      .= W.(b,q) by Th15;
    now
      let m;
      W.(a,p.m) = W.(a,p).m by Def9
        .= W.(b,q.m) by A8,Def9;
      hence a@(q.m) = b@(p.m) by MIDSP_2:33;
    end;
    then a@*'(b,q) = b@*'(a,p) by A7,Def3;
    hence Phi(a,x) = Phi(b,x) by MIDSP_2:33;
  end;
  hence thesis by A1;
end;

theorem Th20:
  1 in Seg(n+1)
proof
  0 <= n by NAT_1:2;
  then 0+1 <= n+1 by XREAL_1:7;
  hence thesis by FINSEQ_1:1;
end;

theorem Th21:
  1 is Nat of n
proof
  1 in Seg(n+1) by Th20;
  hence thesis by Th7;
end;

::Section 3: Reper Algebra and its atlas

begin

definition
  let n;
  mode ReperAlgebra of n -> MidSp-like non empty ReperAlgebraStr over n+2
    means
    :Def11:
    it is being_invariance;
  existence
  proof
    reconsider one1 = 1 as Nat of n+1 by Th21;
    set M = the MidSp;
    set D = the carrier of M, k = (n+1)+1;
    set C = k-tuples_on D;
    deffunc F(Element of C)=$1.one1;
    consider R being Function of C,D such that
A1: for p being Element of C holds R.p = F(p) from FUNCT_2:sch 4;
    reconsider R as Function of (n+2)-tuples_on D,D;
    reconsider RA = ReperAlgebraStr (# the carrier of M, the MIDPOINT of M, R
    #) as MidSp-like non empty ReperAlgebraStr over n+2 by Lm3;
    take RA;
    for a,b being Point of RA, p,q being Tuple of (n+1),RA st for m holds
    a@(q.m) = b@(p.m) holds a@*'(b,q) = b@*'(a,p)
    proof
      let a,b be Point of RA, p,q be Tuple of (n+1),RA such that
      for m holds a@(q.m) = b@(p.m);
A2:   *'(a,p) = (<*a*>^p).one1 by A1
        .= a by FINSEQ_1:41;
      *'(b,q) = (<*b*>^q).one1 by A1
        .= b by FINSEQ_1:41;
      hence thesis by A2;
    end;
    hence thesis by Def3;
  end;
end;

reserve RAS for ReperAlgebra of n;
reserve a,b,pm,p9m,p99m for Point of RAS;
reserve p for Tuple of (n+1),RAS;
reserve W for ATLAS of RAS;
reserve v for Vector of W;
reserve x for Tuple of (n+1),W;

theorem Th22:
  Phi(a,x) = Phi(b,x)
proof
  RAS is being_invariance by Def11;
  hence thesis by Th19;
end;

definition
  let n,RAS,W,x;
  func Phi(x) -> Vector of W means
  :Def12:
  for a holds it = Phi(a,x);
  existence
  proof
    set a = the Point of RAS;
    take Phi(a,x);
    thus thesis by Th22;
  end;
  uniqueness
  proof
    set a = the Point of RAS;
    let y,z be Vector of W such that
A1: for a holds y = Phi(a,x) and
A2: for a holds z = Phi(a,x);
    y = Phi(a,x) by A1;
    hence thesis by A2;
  end;
end;

Lm4: W.(a,p) = x implies Phi(x) = W.(a,*'(a,p))
proof
  assume
A1: W.(a,p) = x;
  thus Phi(x) = Phi(a,x) by Def12
    .= W.(a,*'(a,p)) by A1,Th15;
end;

Lm5: (a,x).W = p implies Phi(x) = W.(a,*'(a,p))
proof
  assume (a,x).W = p;
  then W.(a,p) = x by Th15;
  hence thesis by Lm4;
end;

theorem Th23:
  W.(a,p) = x & W.(a,b) = v & Phi(x) = v implies *'(a,p) = b
proof
  assume
A1: W.(a,p) = x & W.(a,b) = v & Phi(x) = v;
  Phi(x) = Phi(a,x) by Def12;
  hence thesis by A1,Th18;
end;

theorem Th24:
  (a,x).W = p & (a,v).W = b & *'(a,p) = b implies Phi(x) = v
proof
  assume (a,x).W = p & (a,v).W = b & *'(a,p) = b;
  then Phi(a,x) = v by MIDSP_2:33;
  hence thesis by Def12;
end;

theorem Th25:
  W.(a,p) = x & W.(a,b) = v implies W.(a,(p+*(m,b))) = (x+*(m,v))
proof
  assume that
A1: W.(a,p) = x and
A2: W.(a,b) = v;
  set q = (p+*(m,b));
  set y = W.(a,q), z = (x+*(m,v));
  for k being Nat of n holds y.k = z.k
  proof
    let k be Nat of n;
    now
      per cases;
      suppose
A3:     k = m;
        thus y.k = W.(a,q.k) by Def9
          .= W.(a,b) by A3,Th10
          .= z.k by A2,A3,Th13;
      end;
      suppose
A4:     k <> m;
        thus y.k = W.(a,q.k) by Def9
          .= W.(a,p.k) by A4,FUNCT_7:32
          .= x.k by A1,Def9
          .= z.k by A4,FUNCT_7:32;
      end;
    end;
    hence thesis;
  end;
  hence thesis by Th14;
end;

theorem Th26:
  (a,x).W = p & (a,v).W = b implies (a,(x+*(m,v))).W = (p+*(m,b))
proof
  assume (a,x).W = p & (a,v).W = b;
  then W.(a,p) = x & W.(a,b) = v by Th15,MIDSP_2:33;
  then W.(a,(p+*(m,b))) = (x+*(m,v)) by Th25;
  hence thesis by Th15;
end;

theorem
  RAS has_property_of_zero_in m iff for x holds Phi((x+*(m,0.W))) = 0.W
proof
  thus RAS has_property_of_zero_in m implies for x holds Phi((x+*(m,0.W))) =
  0.W
  proof
    set a = the Point of RAS;
    assume
A1: RAS has_property_of_zero_in m;
    set b = (a,(0.W)).W;
    let x;
    set p9 = ((a,x).W)+*(m,a);
A2: b = a by MIDSP_2:34;
    then
A3: (a,((x+*(m,0.W)))).W = p9 by Th26;
    *'(a,p9) = b by A1,A2,Def4;
    hence thesis by A3,Th24;
  end;
  thus (for x holds Phi((x+*(m,0.W))) = 0.W) implies RAS
  has_property_of_zero_in m
  proof
    assume
A4: for x holds Phi((x+*(m,0.W))) = 0.W;
    for a,p holds *'(a,(p+*(m,a))) = a
    proof
      let a,p;
      set v = W.(a,a);
      set x9 = ((W.(a,p))+*(m,0.W));
      v = 0.W by MIDSP_2:33;
      then W.(a,((p+*(m,a)))) = x9 & Phi(x9) = v by A4,Th25;
      hence thesis by Th23;
    end;
    hence thesis by Def4;
  end;
end;

theorem Th28:
  RAS is_semi_additive_in m iff for x holds Phi((x+*(m,Double(x.m)
  ))) = Double Phi(x)
proof
  thus RAS is_semi_additive_in m implies for x holds Phi((x+*(m,Double(x.m))))
  = Double Phi(x)
  proof
    set a = the Point of RAS;
    assume
A1: RAS is_semi_additive_in m;
    let x;
    set x9 = (x+*(m,Double(x.m)));
    set p = (a,x).W, p9 = (a,x9).W;
    set q = (p9+*(m,a@(p9.m)));
    for i being Nat of n holds p.i = q.i
    proof
      let i be Nat of n;
      now
        per cases;
        suppose
A2:       i = m;
          W.(a,p) = x by Th15;
          then
A3:       W.(a,p.m) = x.m by Def9;
          W.(a,p9) = x9 by Th15;
          then
A4:       W.(a,p9.m) = x9.m by Def9;
          x9.m = Double (x.m) by Th13;
          then p.m = a@(p9.m) by A3,A4,MIDSP_2:31
            .= q.m by Th10;
          hence thesis by A2;
        end;
        suppose
A5:       i <> m;
          thus p.i = (a,x.i).W by Def8
            .= (a,x9.i).W by A5,FUNCT_7:32
            .= p9.i by Def8
            .= q.i by A5,FUNCT_7:32;
        end;
      end;
      hence thesis;
    end;
    then p = q by Th9;
    then *'(a,p) = a@*'(a,p9) by A1,Def5;
    then
A6: W.(a,*'(a,p9)) = Double W.(a,*'(a,p)) by MIDSP_2:31;
    Phi(x9) = W.(a,*'(a,p9)) by Lm5;
    hence thesis by A6,Lm5;
  end;
  thus (for x holds Phi((x+*(m,Double(x.m)))) = Double Phi(x)) implies RAS
  is_semi_additive_in m
  proof
    assume
A7: for x holds Phi((x+*(m,Double(x.m)))) = Double Phi(x);
    let a;
    let p9m be Point of RAS, p9 be Tuple of (n+1),RAS such that
A8: p9.m = p9m;
    set p = (p9+*(m,a@(p9.m)));
    set x = W.(a,p);
    set x9 = (x+*(m,Double(x.m)));
    W.(a,p9) = x9
    proof
      set y = W.(a,p9);
      for i being Nat of n holds x9.i = y.i
      proof
        let i be Nat of n;
        now
          per cases;
          suppose
A9:         i = m;
A10:        W.(a,p.m) = x.m & p.m = a@(p9.m) by Def9,Th10;
            x9.m = Double (x.m) & W.(a,p9.m) = y.m by Def9,Th13;
            hence thesis by A9,A10,MIDSP_2:31;
          end;
          suppose
A11:        i <> m;
            hence x9.i = x.i by FUNCT_7:32
              .= W.(a,p.i) by Def9
              .= W.(a,p9.i) by A11,FUNCT_7:32
              .= y.i by Def9;
          end;
        end;
        hence thesis;
      end;
      hence thesis by Th14;
    end;
    then
A12: Phi(x9) = W.(a,*'(a,p9)) by Lm4;
    Phi(x) = W.(a,*'(a,p)) by Lm4;
    then W.(a,*'(a,p9)) = Double W.(a,*'(a,p)) by A7,A12;
    hence thesis by A8,MIDSP_2:31;
  end;
end;

theorem Th29:
  RAS has_property_of_zero_in m & RAS is_additive_in m implies RAS
  is_semi_additive_in m
proof
  assume that
A1: RAS has_property_of_zero_in m and
A2: RAS is_additive_in m;
  let a,pm,p;
  assume p.m = pm;
  then *'(a,(p+*(m,a@pm))) = *'(a,p)@*'(a,(p+*(m,a))) by A2,Def6
    .= a@*'(a,p) by A1,Def4;
  hence thesis;
end;

Lm6: RAS is_semi_additive_in m implies for a,p9m, p99m,p st a@(p99m) = (p.m)@(
p9m) holds *'(a,(p+*(m,(p.m)@p9m))) = *'(a,p)@*'(a,(p+*(m,p9m))) iff W.(a,*'(a,
(p+*(m,p99m)))) = W.(a,*'(a,p)) + W.(a,*'(a,(p+*(m,p9m))))
proof
  assume
A1: RAS is_semi_additive_in m;
  let a,p9m, p99m,p;
  assume a@(p99m) = (p.m)@(p9m);
  then *'(a,(p+*(m,(p.m)@p9m))) = a@*'(a,(p+*(m,p99m))) by A1,Th11;
  hence thesis by MIDSP_2:30;
end;

Lm7: (for x,v holds Phi((x+*(m,(x.m)+v))) = Phi(x) + Phi((x+*(m,v)))) implies
RAS is_semi_additive_in m
proof
  assume
A1: for x,v holds Phi((x+*(m,(x.m)+v))) = Phi(x) + Phi((x+*(m,v)));
  for x holds Phi((x+*(m,Double(x.m)))) = Double Phi(x)
  proof
    let x;
    set v = x.m;
    set y = (x+*(m,v));
    for k being Nat of n holds y.k = x.k
    proof
      let k be Nat of n;
      now
        per cases;
        suppose
          k = m;
          hence thesis by Th13;
        end;
        suppose
          k <> m;
          hence thesis by FUNCT_7:32;
        end;
      end;
      hence thesis;
    end;
    then
A2: y = x by Th14;
    thus Phi((x+*(m,Double v))) = Phi((x+*(m,v+v))) by MIDSP_2:def 1
      .= Phi(x) + Phi((x+*(m,v))) by A1
      .= Double Phi(x) by A2,MIDSP_2:def 1;
  end;
  hence thesis by Th28;
end;

theorem
  RAS has_property_of_zero_in m implies (RAS is_additive_in m iff for x,
  v holds Phi((x+*(m,(x.m)+v))) = Phi(x) + Phi ((x+*(m,v))))
proof
  assume
A1: RAS has_property_of_zero_in m;
  thus RAS is_additive_in m implies for x,v holds Phi((x+*(m,(x.m)+v))) = Phi(
  x) + Phi((x+*(m,v)))
  proof
    set a = the Point of RAS;
    assume
A2: RAS is_additive_in m;
    let x,v;
    set p = (a,x).W, p9m = (a,v).W;
    consider p99m such that
A3: (p99m)@a = (p.m)@(p9m) by MIDSP_1:def 3;
A4: W.(a,p) = x & W.(a,p9m) = v by Th15,MIDSP_2:33;
A5: W.(a,p99m) = W.(a,p.m) + W.(a,p9m) by A3,MIDSP_2:30
      .= x.m + v by A4,Def9;
    (p+*(m,p99m)) = (a,(x+*(m,(x.m)+v))).W
    proof
      set pp = (p+*(m,p99m)), xx = (x+*(m,(x.m)+v));
      set qq = (a,xx).W;
      for i being Nat of n holds pp.i = qq.i
      proof
        let i be Nat of n;
        per cases;
        suppose
A6:       i = m;
          hence pp.i = p99m by Th10
            .= (a,(x.m)+v).W by A5,MIDSP_2:33
            .= (a,xx.m).W by Th13
            .= qq.i by A6,Def8;
        end;
        suppose
A7:       i <> m;
          hence pp.i = p.i by FUNCT_7:32
            .= (a,x.i).W by Def8
            .= (a,xx.i).W by A7,FUNCT_7:32
            .= qq.i by Def8;
        end;
      end;
      hence thesis by Th9;
    end;
    then
A8: Phi((x+*(m,(x.m)+v))) = W.(a,*'(a,(p+*(m,p99m)))) by Lm5;
A9: (p+*(m,p9m)) = (a,(x+*(m,v))).W
    proof
      set pp = (p+*(m,p9m)), qq = (a,(x+*(m,v))).W;
      for i being Nat of n holds pp.i = qq.i
      proof
        let i be Nat of n;
        per cases;
        suppose
A10:      i = m;
          hence pp.i = p9m by Th10
            .= (a,(x+*(m,v)).m).W by Th13
            .= qq.i by A10,Def8;
        end;
        suppose
A11:      i <> m;
          hence pp.i = p.i by FUNCT_7:32
            .= (a,x.i).W by Def8
            .= (a,(x+*(m,v)).i).W by A11,FUNCT_7:32
            .= qq.i by Def8;
        end;
      end;
      hence thesis by Th9;
    end;
    RAS is_semi_additive_in m & *'(a,(p+*(m,(p.m)@p9m))) = *'(a,p)@*'(a,(p
    +*(m, p9m))) by A1,A2,Def6,Th29;
    then
A12: W.(a,*'(a,(p+*(m,p99m)))) = W.(a,*'(a,p)) + W.(a,*'(a,(p+*(m,p9m)) ))
    by A3,Lm6;
    Phi(x) = W.(a,*'(a,p)) by Lm5;
    hence thesis by A12,A8,A9,Lm5;
  end;
  thus (for x,v holds Phi((x+*(m,(x.m)+v))) = Phi(x) + Phi((x+*(m,v))))
  implies RAS is_additive_in m
  proof
    assume
A13: for x,v holds Phi((x+*(m,(x.m)+v))) = Phi(x) + Phi ((x+*(m,v)));
    then
A14: RAS is_semi_additive_in m by Lm7;
    for a,pm,p9m,p st p.m = pm holds *'(a,(p+*(m,pm@p9m))) = *'(a,p)@*'(a
    ,(p+*(m,p9m)))
    proof
      let a,pm,p9m,p such that
A15:  p.m = pm;
      set x = W.(a,p), v = W.(a,p9m);
      consider p99m such that
A16:  (p99m)@a = (p.m)@(p9m) by MIDSP_1:def 3;
A17:  (a,x).W = p by Th15;
A18:  W.(a,p99m) = W.(a,p.m) + W.(a,p9m) by A16,MIDSP_2:30
        .= x.m + v by Def9;
      (p+*(m,p99m)) = (a,(x+*(m,(x.m)+v))).W
      proof
        set pp = (p+*(m,p99m)), xx = (x+*(m,(x.m)+v));
        set qq = (a,xx).W;
        for i being Nat of n holds pp.i = qq.i
        proof
          let i be Nat of n;
          per cases;
          suppose
A19:        i = m;
            hence pp.i = p99m by Th10
              .= (a,(x.m)+v).W by A18,MIDSP_2:33
              .= (a,xx.m).W by Th13
              .= qq.i by A19,Def8;
          end;
          suppose
A20:        i <> m;
            hence pp.i = p.i by FUNCT_7:32
              .= (a,x.i).W by A17,Def8
              .= (a,xx.i).W by A20,FUNCT_7:32
              .= qq.i by Def8;
          end;
        end;
        hence thesis by Th9;
      end;
      then
A21:  Phi((x+*(m,(x.m)+v))) = W.(a,*'(a,(p+*(m,p99m)))) by Lm5;
A22:  (a,v).W = p9m by MIDSP_2:33;
      (p+*(m,p9m)) = (a,(x+*(m,v))).W
      proof
        set pp = (p+*(m,p9m)), qq = (a,(x+*(m,v))).W;
        for i being Nat of n holds pp.i = qq.i
        proof
          let i be Nat of n;
          per cases;
          suppose
A23:        i = m;
            hence pp.i = p9m by Th10
              .= (a,(x+*(m,v)).m).W by A22,Th13
              .= qq.i by A23,Def8;
          end;
          suppose
A24:        i <> m;
            hence pp.i = p.i by FUNCT_7:32
              .= (a,x.i).W by A17,Def8
              .= (a,(x+*(m,v)).i).W by A24,FUNCT_7:32
              .= qq.i by Def8;
          end;
        end;
        hence thesis by Th9;
      end;
      then
A25:  Phi((x+*(m,v))) = W.(a,*'(a,(p+*(m,p9m)))) by Lm5;
      Phi(x) = W.(a,*'(a,p)) by Lm4;
      then
      W.(a,*'(a,(p+*(m,p99m)))) = W.(a,*'(a,p)) + W.(a,*' (a,(p+*(m,p9m))
      )) by A13,A21,A25;
      hence thesis by A14,A15,A16,Lm6;
    end;
    hence thesis by Def6;
  end;
end;

theorem Th31:
  W.(a,p) = x & m<= n implies W.(a,(p+*(m+1,p.m))) = (x+*(m+1,x.m) )
proof
  assume that
A1: W.(a,p) = x and
A2: m<=n;
  reconsider m9 = m+1 as Nat of n by A2,Th8;
  set y = W.(a,(p+*(m9,p.m))), z = (x+*(m9,x.m));
  for k being Nat of n holds y.k = z.k
  proof
    let k be Nat of n;
    now
      per cases;
      suppose
A3:     k = m9;
        thus y.k = W.(a,(p+*(m9,p.m)).k) by Def9
          .= W.(a,p.m) by A3,Th10
          .= x.m by A1,Def9
          .= z.k by A3,Th13;
      end;
      suppose
A4:     k <> m9;
        thus y.k = W.(a,(p+*(m9,p.m)).k) by Def9
          .= W.(a,p.k) by A4,FUNCT_7:32
          .= x.k by A1,Def9
          .= z.k by A4,FUNCT_7:32;
      end;
    end;
    hence thesis;
  end;
  hence thesis by Th14;
end;

theorem Th32:
  (a,x).W = p & m<=n implies (a,(x+*(m+1,x.m))).W = (p+*(m+1,p.m))
proof
  assume that
A1: (a,x).W = p and
A2: m<=n;
  W.(a,p) = x by A1,Th15;
  then W.(a,(p+*(m+1,p.m))) = (x+*(m+1,x.m)) by A2,Th31;
  hence thesis by Th15;
end;

theorem
  m<=n implies (RAS is_alternative_in m iff for x holds Phi((x+*(m+1,x.m
  ))) = 0. W )
proof
  assume
A1: m<=n;
  thus RAS is_alternative_in m implies for x holds Phi((x+*(m+1,x.m))) = 0.W
  proof
    set a = the Point of RAS;
    assume
A2: RAS is_alternative_in m;
    let x;
    set p = (a,x).W, b = (a,(0.W)).W;
    set p9 = (p+*(m+1,p.m));
    b = a by MIDSP_2:34;
    then
A3: *'(a,p9) = b by A2,Def7;
    (a,((x+*(m+1,x.m)))).W = p9 by A1,Th32;
    hence thesis by A3,Th24;
  end;
    assume
A4: for x holds Phi((x+*(m+1,x.m))) = 0.W;
    for a,p,pm st p.m = pm holds *'(a,p+*(m+1,pm)) = a
    proof
      let a,p,pm such that
A5:   p.m = pm;
      set x = W.(a,p), v = W.(a,a);
      set x9 = (x+*(m+1,x.m));
      v = 0.W by MIDSP_2:33;
      then
A6:   Phi(x9) = v by A4;
      W.(a,((p+*(m+1,p.m)))) = x9 by A1,Th31;
      hence thesis by A5,A6,Th23;
    end;
    hence thesis by Def7;
end;