The Mizar article:

On Replace Function and Swap Function for Finite Sequences

by
Hiroshi Yamazaki,
Yoshinori Fujisawa, and
Yatsuka Nakamura

Received August 28, 2000

Copyright (c) 2000 Association of Mizar Users

MML identifier: FINSEQ_7
[ MML identifier index ]


environ

 vocabulary FINSEQ_1, ARYTM_1, RELAT_1, FUNCT_1, RFINSEQ, FINSEQ_4, FUNCT_4,
      BOOLE, FINSEQ_7;
 notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, BINARITH,
      FUNCT_1, FINSEQ_1, FINSEQ_4, RFINSEQ, TOPREAL1, FUNCT_7;
 constructors REAL_1, BINARITH, REALSET1, RFINSEQ, TOPREAL1, FINSEQ_4, INT_1,
      FUNCT_7, CQC_LANG, MEMBERED;
 clusters FINSEQ_1, FINSEQ_5, RELSET_1, INT_1, TOPREAL1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 theorems TARSKI, AXIOMS, REAL_1, NAT_1, BINARITH, FINSEQ_1, FINSEQ_3,
      FINSEQ_4, FINSEQ_5, FINSEQ_6, RFINSEQ, JORDAN3, AMI_5, JORDAN8, TOPREAL1,
      RLVECT_1, INT_1, GOBOARD9, GENEALG1, SPRECT_3, POLYNOM4, POLYNOM1,
      REVROT_1, JORDAN4, SCMFSA_7, FUNCT_7, JORDAN2B, XBOOLE_0, XBOOLE_1,
      XCMPLX_0, XCMPLX_1;

begin :: Some Basic Theorems

reserve D for non empty set,
  f, g, h for FinSequence of D,
  p, p1, p2, p3, q for Element of D,
  i, j, k, l, n for Nat;

theorem Th1:
  1 <= i & j <= len f & i < j implies
    f = (f|(i-'1))^<*f.i*>^((f/^i)|(j-'i-'1))^<*f.j*>^(f/^j)
proof
  assume that
    A1:1 <= i and
    A2:j <= len f and
    A3:i < j;
    i -'i < j -'i by A3,SPRECT_3:10;
  then A4:0 < j -'i by GOBOARD9:1;
  set I = j-'i-'1;
  A5:j -'i >= 1 by A4,RLVECT_1:99;
  then A6:I + 1 = j -'i by AMI_5:4;
    j -'i <= len f -'i by A2,JORDAN3:5;
  then A7:I+1 <= len (f/^i) by A6,JORDAN3:19;
  A8:i <= len f by A2,A3,AXIOMS:22;
    1 <= j by A1,A3,AXIOMS:22;
  then A9:j in dom f by A2,FINSEQ_3:27;
  A10:(I+1)+i = j by A3,A6,AMI_5:4;
    1 <= I+1 by A5,AMI_5:4;
  then I+1 in dom (f/^i) by A7,FINSEQ_3:27;
  then A11:(f/^i)/.(I+1) = f/.j by A10,FINSEQ_5:30;
  A12:i < len (f|j) by A2,A3,TOPREAL1:3;
  A13:f/^i = ((f|j)^(f/^j))/^i by RFINSEQ:21
           .= ((f|j)/^i)^(f/^j) by A12,GENEALG1:1
           .= ((f/^i)|(I+1))^(f/^j) by A6,JORDAN3:21
           .= ((f/^i)|I)^<*(f/^i)/.(I+1)*>^(f/^j) by A7,JORDAN8:2
           .= ((f/^i)|I)^<*f.j*>^(f/^j) by A9,A11,FINSEQ_4:def 4;
    f = (f|(i-'1))^<*f.i*>^(f/^i) by A1,A8,POLYNOM4:3
        .= (f|(i-'1))^<*f.i*>^(((f/^i)|I)^(<*f.j*>^(f/^j))) by A13,FINSEQ_1:45
        .= (f|(i-'1))^<*f.i*>^((f/^i)|I)^(<*f.j*>^(f/^j)) by FINSEQ_1:45
        .= (f|(i-'1))^<*f.i*>^((f/^i)|I)^<*f.j*>^(f/^j) by FINSEQ_1:45;
  hence thesis;
end;

theorem
    len g = len h & len g < i & i <= len (g^f) implies (g^f).i = (h^f).i
proof
    assume
A1:     len g = len h & len g < i & i <= len (g^f);
      then len g - len g < i - len g by REAL_1:54;
then A2:    len g + (-len g) < i - len g by XCMPLX_0:def 8;
        then 0 < i - len g by XCMPLX_0:def 6;
then A3:     0 + 1 <= i - len g by INT_1:20;
        i <= len g + len f by A1,FINSEQ_1:35;
      then i - len g <= len g + len f - len g by REAL_1:49;
then A4:     (i - len g) <= len f by XCMPLX_1:26;
      set k = i - len g;
        0 <= k by A2,XCMPLX_0:def 6;
      then reconsider k as Nat by INT_1:16;
A5:     k in dom f by A3,A4,FINSEQ_3:27;
        (g^f).i = (g^f).(k + len g) by XCMPLX_1:27
        .= f.k by A5,FINSEQ_1:def 7
        .= (h^f).(len h + k) by A5,FINSEQ_1:def 7;
    hence thesis by A1,XCMPLX_1:27;
  end;

theorem
    1 <= i & i <= len f implies f.i = (g^f).(len g + i)
proof
    assume 1 <= i & i <= len f;
    then i in dom f by FINSEQ_3:27;
    hence thesis by FINSEQ_1:def 7;
  end;

theorem
    i in dom(f/^n) implies (f/^n).i = f.(n+i)
proof
  assume A1: i in dom(f/^n);
  then A2: (f/^n)/.i = f/.(n+i) by FINSEQ_5:30;
  A3: (f/^n)/.i = (f/^n).i by A1,FINSEQ_4:def 4;
    n+i in dom f by A1,FINSEQ_5:29;
  hence thesis by A2,A3,FINSEQ_4:def 4;
end;

Lm1:
  j -'i -'1 = j -'1 -'i
proof
    j -'i -'1 = j -'(i+1) by POLYNOM1:3;
  hence thesis by POLYNOM1:3;
end;

begin :: Definition of Replace Function and its properties

definition
  let D be non empty set;
  let f be FinSequence of D;
  let i be Nat;
  let p be Element of D;
  redefine func f +* (i, p) -> FinSequence of D equals :Def1:
    (f|(i-'1))^<*p*>^(f/^i) if 1 <= i & i <= len f
    otherwise f;
  compatibility
  proof
A1: 1 <= i & i <= len f implies f +* (i, p) = (f|(i-'1))^<*p*>^(f/^i)
    proof
      assume 1 <= i & i <= len f;
      then i in dom f by FINSEQ_3:27;
      hence thesis by JORDAN2B:13;
    end;
      not (1 <= i & i <= len f) implies f +* (i, p) = f
    proof
      assume not (1 <= i & i <= len f);
      then not i in dom f by FINSEQ_3:27;
      hence thesis by FUNCT_7:def 3;
    end;
    hence thesis by A1;
  end;
  correctness
  proof
      f +* (i, p) is FinSequence of D;
    hence thesis;
  end;
  synonym Replace(f, i, p);
end;

canceled 2;

theorem Th7:
  len Replace(f, i, p) = len f
proof
    Seg len (f+*(i,p)) = dom (f+*(i,p)) by FINSEQ_1:def 3
                    .= dom f by FUNCT_7:32
                    .= Seg len f by FINSEQ_1:def 3;
  hence thesis by FINSEQ_1:8;
end;

theorem
    rng Replace(f, i, p) c= rng f \/ {p}
proof
    rng <*p*> = {p} by FINSEQ_1:56;
  then A1:rng f \/ {p}
   = rng (f^<*p*>) by FINSEQ_1:44;
  set P = f|(i-'1);
  set Q = f/^i;
  set F = <*f.i*>;
  per cases;
    suppose not i in Seg (len f);
      then not (1 <= i & i <= len f) by FINSEQ_1:3;
      then rng Replace(f,i,p) = rng f by Def1;
      hence thesis by A1,FINSEQ_1:42;
    suppose i in Seg len f;
      then A2:1 <= i & i <= len f by FINSEQ_1:3;
      then A3:rng Replace(f, i, p)
        = rng (P^<*p*>^Q) by Def1
       .= rng (P^(<*p*>^Q)) by FINSEQ_1:45
       .= rng P \/ rng (<*p*>^Q) by FINSEQ_1:44
       .= rng P \/ (rng <*p*> \/ rng Q) by FINSEQ_1:44
       .= rng P \/ rng (Q^<*p*>) by FINSEQ_1:44
       .= rng (P^(Q^<*p*>)) by FINSEQ_1:44;
       rng f \/ {p}
        = rng ((P^F^Q)^<*p*>) by A1,A2,POLYNOM4:3
       .= rng (P^F^Q) \/ rng <*p*> by FINSEQ_1:44
       .= rng (P^(F^Q)) \/ rng <*p*> by FINSEQ_1:45
       .= rng P \/ rng (F^Q) \/ rng <*p*> by FINSEQ_1:44
       .= rng P \/ (rng F \/ rng Q) \/ rng <*p*> by FINSEQ_1:44
       .= rng P \/ ((rng Q \/ rng F) \/ rng <*p*>) by XBOOLE_1:4
       .= rng P \/ ((rng Q \/ rng <*p*>) \/ rng F) by XBOOLE_1:4
       .= (rng P \/ (rng Q \/ rng <*p*>)) \/ rng F by XBOOLE_1:4
       .= (rng P \/ rng (Q^<*p*>)) \/ rng F by FINSEQ_1:44
       .= (rng (P^(Q^<*p*>))) \/ rng F by FINSEQ_1:44
       .= rng ((P^(Q^<*p*>))^F) by FINSEQ_1:44;
    hence thesis by A3,FINSEQ_1:42;
end;

theorem
    1 <= i & i <= len f implies p in rng Replace(f, i, p)
proof
    assume
A1:   1 <= i & i <= len f;
        rng ((f|(i-'1))^<*p*>^(f/^i))
         = rng (f|(i-'1)^(<*p*>^(f/^i))) by FINSEQ_1:45
        .= rng (f|(i-'1)) \/ rng (<*p*>^(f/^i)) by FINSEQ_1:44
        .= rng (f|(i-'1)) \/ (rng <*p*> \/ rng (f/^i)) by FINSEQ_1:44;
then A2:   rng Replace(f, i, p)
           = rng (f|(i-'1)) \/ (rng <*p*> \/ rng (f/^i)) by A1,Def1
          .= rng <*p*> \/ (rng (f/^i) \/ rng (f|(i-'1))) by XBOOLE_1:4;
        p in {p} by TARSKI:def 1;
      then p in rng <*p*> by FINSEQ_1:56;
    hence thesis by A2,XBOOLE_0:def 2;
  end;

Lm2:
  1 <= i & i <= len f implies Replace(f, i, p).i = p
proof
    assume 1 <= i & i <= len f;
    then i in dom f by FINSEQ_3:27;
    hence thesis by FUNCT_7:33;
  end;

theorem
    1 <= i & i <= len f implies Replace(f, i, p)/.i = p
proof
  assume A1:1 <= i & i <= len f;
  then 1 <= i & i <= len Replace(f,i,p) by Th7;
  then i in dom Replace(f,i,p) by FINSEQ_3:27;
  then Replace(f, i, p)/.i = Replace(f,i,p).i by FINSEQ_4:def 4;
  hence thesis by A1,Lm2;
end;

theorem
    1 <= i & i <= len f implies
    for k st (0 < k & k <= len f - i)
      holds Replace(f, i, p).(i + k) = (f/^i).k
proof
    assume
A1:   1 <= i & i <= len f;
        i - 1 < i by INT_1:26;
      then i -' 1 < i by A1,SCMFSA_7:3;
then A2:   i -' 1 <= len f by A1,AXIOMS:22;
A3:   len ((f|(i-'1))^<*p*>) = len (f|(i-'1)) + len <*p*> by FINSEQ_1:35
        .= (i -' 1) + len <*p*> by A2,TOPREAL1:3
        .= i -' 1 + 1 by FINSEQ_1:56
        .= i by A1,AMI_5:4;
        len f = len Replace(f, i, p) by Th7
        .= len ((f|(i-'1))^<*p*>^(f/^i)) by A1,Def1
        .= i + len (f/^i) by A3,FINSEQ_1:35;
then A4:   len (f/^i) = len f - i by XCMPLX_1:26;
      let k be Nat;
      assume
A5:   0 < k & k <= len f - i;
      then 0 + 1 <= k by INT_1:20;
then A6:   k in dom (f/^i) by A4,A5,FINSEQ_3:27;
        Replace(f, i, p).(i + k)
            = ((f|(i-'1))^<*p*>^(f/^i)).(len ((f|(i-'1))^<*p*>) + k)
              by A1,A3,Def1;
      hence thesis by A6,FINSEQ_1:def 7;
  end;

theorem Th12:
  1 <= k & k <= len f & k <> i implies Replace(f, i, p)/.k = f/.k
proof
  assume A1: 1 <= k & k <= len f & k <> i;
  then k in dom f by FINSEQ_3:27;
  hence thesis by A1,FUNCT_7:39;
end;

theorem Th13:
  1 <= i & i < j & j <= len f implies
    Replace(Replace(f, j, q), i, p)
      = (f|(i-'1))^<*p*>^(f/^i)|(j-'i-'1)^<*q*>^(f/^j)
proof
  assume A1:1 <= i & i < j & j <= len f;
  then A2:1 <= i & i <= len f & 1 <= j & j <= len f by AXIOMS:22;
  set F = Replace(f,j,q);
  A3:i <= len F by A2,Th7;
  set fp = f|(j-'1);
  set fj = <*q*>;
  set P = fp^fj;
  set Q = f/^j;
    j -'1 <= j by GOBOARD9:2;
  then A4:j -'1 <= len f by A1,AXIOMS:22;
  A5: len P = len fp + len fj by FINSEQ_1:35
            .= len fp + 1 by FINSEQ_1:56
            .= j -'1 + 1 by A4,TOPREAL1:3
            .= j by A2,AMI_5:4;
    1 + i <= j by A1,INT_1:20;
  then i <= j -' 1 by SPRECT_3:8;
  then A6:i <= len fp by A4,TOPREAL1:3;
  A7:i-'1 <= len P by A1,A5,JORDAN3:7;
  A8:i -'1 < j -'1 by A1,SPRECT_3:9;
  then A9:i-'1 <= len fp by A4,TOPREAL1:3;
    Replace(F,i,p) = (F|(i-'1))^<*p*>^(F/^i) by A1,A3,Def1
   .= (F|(i-'1))^<*p*>^((P^Q)/^i) by A2,Def1
   .= (F|(i-'1))^<*p*>^((P/^i)^Q) by A1,A5,GENEALG1:1
   .= (F|(i-'1))^<*p*>^(((fp/^i)^fj)^Q) by A6,GENEALG1:1
   .= (F|(i-'1))^<*p*>^((((f/^i)|((j-'1)-'i))^fj)^Q) by JORDAN3:21
   .= (F|(i-'1))^<*p*>^(((f/^i)|((j-'1)-'i))^fj)^Q by FINSEQ_1:45
   .= (F|(i-'1))^<*p*>^((f/^i)|((j-'1)-'i))^fj^Q by FINSEQ_1:45
   .= ((P^Q)|(i-'1))^<*p*>^(f/^i)|((j-'1)-'i)^fj^Q by A2,Def1
   .= (P|(i-'1))^<*p*>^(f/^i)|((j-'1)-'i)^fj^Q by A7,FINSEQ_5:25
   .= (fp|(i-'1))^<*p*>^(f/^i)|((j-'1)-'i)^fj^Q by A9,FINSEQ_5:25
   .= (f|(i-'1))^<*p*>^(f/^i)|((j-'1)-'i)^fj^Q by A8,JORDAN4:15
   .= (f|(i-'1))^<*p*>^(f/^i)|(j-'i-'1)^<*q*>^Q by Lm1;
  hence thesis;
end;

theorem
    Replace(<*p*>, 1, q) = <*q*>
proof
A1:   1 - 1 = 0;
      reconsider P = <*p*>^{} as FinSequence of D by FINSEQ_1:47;
      reconsider g = {} as FinSequence of D by FINSEQ_1:29;
A2:   (<*p*>^g)/^1 = g by FINSEQ_6:49;
        1 <= 1 & 1 <= len <*p*> by FINSEQ_1:56;
      hence Replace(<*p*>, 1, q) = (<*p*>|(1-'1))^<*q*>^(<*p*>/^1) by Def1
        .= (<*p*>|0)^<*q*>^(<*p*>/^1) by A1,BINARITH:def 3
        .= <*q*>^(<*p*>/^1) by FINSEQ_1:47
        .= <*q*>^(P/^1) by FINSEQ_1:47
        .= <*q*> by A2,FINSEQ_1:47;
  end;

theorem Th15:
  Replace(<*p1, p2*>, 1, q) = <*q, p2*>
proof
  set f = <*p1,p2*>;
  A1:len f = 2 by FINSEQ_1:61;
  then A2:2 in dom f by FINSEQ_3:27;
    1 + 1 = len f by FINSEQ_1:61;
  then A3:f/^1 = <*f/.2*> by FINSEQ_5:33
               .= <*f.2*> by A2,FINSEQ_4:def 4;
    Replace(f,1,q) = (f|(1-'1))^<*q*>^(f/^1) by A1,Def1
                .= (f|0)^<*q*>^(f/^1) by GOBOARD9:1
                .= {}^<*q*>^<*p2*> by A3,FINSEQ_1:61
                .= <*q*>^<*p2*> by FINSEQ_1:47;
  hence thesis by FINSEQ_1:def 9;
end;

theorem Th16:
  Replace(<*p1, p2*>, 2, q) = <*p1, q*>
proof
  set f = <*p1,p2*>;
  A1:len f = 2 by FINSEQ_1:61;
  A2:1 <= 2 & 2 <= len f by FINSEQ_1:61;
  A3:1 in dom f by A1,FINSEQ_3:27;
  A4:2 -'1 = 1 + 1 -'1
          .= 1 by BINARITH:39;
    Replace(f,2,q) = (f|(2-'1))^<*q*>^(f/^2) by A2,Def1
                .= (f|1)^<*q*>^(f/^len f) by A4,FINSEQ_1:61
                .= (f|1)^<*q*>^{} by REVROT_1:2
                .= <*f/.1*>^<*q*>^{} by FINSEQ_5:23
                .= <*f/.1*>^<*q*> by FINSEQ_1:47
                .= <*f.1*>^<*q*> by A3,FINSEQ_4:def 4
                .= <*p1*>^<*q*> by FINSEQ_1:61;
  hence thesis by FINSEQ_1:def 9;
end;

theorem Th17:
  Replace(<*p1, p2, p3*>, 1, q) = <*q, p2, p3*>
proof
  set f = <*p1,p2,p3*>;
   len f = 3 by FINSEQ_1:62;
  then Replace(f,1,q) = (f|(1-'1))^<*q*>^(f/^1) by Def1
                .= (f|0)^<*q*>^(f/^1) by GOBOARD9:1
                .= <*q*>^(f/^1) by FINSEQ_1:47
                .= <*q*>^<*p2,p3*> by FINSEQ_6:51
                .= <*q*>^(<*p2*>^<*p3*>) by FINSEQ_1:def 9
                .= <*q*>^<*p2*>^<*p3*> by FINSEQ_1:45;
  hence thesis by FINSEQ_1:def 10;
end;

theorem Th18:
  Replace(<*p1, p2, p3*>, 2, q) = <*p1, q, p3*>
proof
  set f = <*p1,p2,p3*>;
  A1:len f = 3 by FINSEQ_1:62;
    1 <= 3 & 3 <= len f by FINSEQ_1:62;
  then A2:3 in dom f by FINSEQ_3:27;
  A3:1 in dom f by A1,FINSEQ_3:27;
  A4:2 -'1 = 1 + 1 -'1
          .= 1 by BINARITH:39;
  A5:len f = 2 + 1 by FINSEQ_1:62;
  A6:f is non empty by A1,FINSEQ_1:25;
    Replace(f,2,q) = (f|(2-'1))^<*q*>^(f/^2) by A1,Def1
                .= (f|1)^<*q*>^<*f/.3*> by A4,A5,FINSEQ_5:33
                .= (f|1)^<*q*>^<*f.3*> by A2,FINSEQ_4:def 4
                .= (f|1)^<*q*>^<*p3*> by FINSEQ_1:62
                .= <*f/.1*>^<*q*>^<*p3*> by A6,FINSEQ_5:23
                .= <*f.1*>^<*q*>^<*p3*> by A3,FINSEQ_4:def 4
                .= <*p1*>^<*q*>^<*p3*> by FINSEQ_1:62;
  hence thesis by FINSEQ_1:def 10;
end;

theorem Th19:
  Replace(<*p1, p2, p3*>, 3, q) = <*p1, p2, q*>
proof
  set f = <*p1,p2,p3*>;
  A1:len f = 3 by FINSEQ_1:62;
  A2:1 <= 3 & 3 <= len f by FINSEQ_1:62;
  A3:1 in dom f by A1,FINSEQ_3:27;
  A4:2 in dom f by A1,FINSEQ_3:27;
  A5:3 -'1 = 2 + 1 -'1
          .= 2 by BINARITH:39;
    Replace(f,3,q) = (f|(3-'1))^<*q*>^(f/^3) by A2,Def1
                .= (f|2)^<*q*>^(f/^len f) by A5,FINSEQ_1:62
                .= (f|2)^<*q*>^{} by REVROT_1:2
                .= (f|2)^<*q*> by FINSEQ_1:47
                .= <*f/.1,f/.2*>^<*q*> by A1,JORDAN8:1
                .= (<*f/.1*>^<*f/.2*>)^<*q*> by FINSEQ_1:def 9
                .= <*f.1*>^<*f/.2*>^<*q*> by A3,FINSEQ_4:def 4
                .= <*f.1*>^<*f.2*>^<*q*> by A4,FINSEQ_4:def 4
                .= <*p1*>^<*f.2*>^<*q*> by FINSEQ_1:62
                .= <*p1*>^<*p2*>^<*q*> by FINSEQ_1:62;
  hence thesis by FINSEQ_1:def 10;
end;

begin :: Definition of Swap Function and its properties

definition
  let D be non empty set;
  let f be FinSequence of D;
  let i, j be Nat;
  func Swap(f, i, j) -> FinSequence of D equals :Def2:
      Replace(Replace(f, i, f/.j), j, f/.i)
        if 1 <= i & i <= len f & 1 <= j & j <= len f
      otherwise f;
  correctness;
end;

theorem Th20:
  len Swap(f, i, j) = len f
proof
    per cases;
      suppose 1 <= i & i <= len f & 1 <= j & j <= len f;
        then Swap(f, i, j)
          = Replace(Replace(f, i, f/.j), j, f/.i) by Def2;
        then len Swap(f, i, j)
           = len Replace(f, i, f/.j) by Th7;
      hence thesis by Th7;
      suppose not (1 <= i & i <= len f & 1 <= j & j <= len f);
     hence thesis by Def2;
  end;

Lm3:
  1 <= i & i <= len f & 1 <= j & j <= len f
    implies Swap(f, i, j).i = f.j & Swap(f, i, j).j = f.i
  proof
    assume
A1:     1 <= i & i <= len f & 1 <= j & j <= len f;
then A2:    i in dom f & j in dom f by FINSEQ_3:27;
      set F = Replace (f,i,f/.j);
A3:     1 <= i & i <= len F & 1 <= j & j <= len F by A1,Th7;
      per cases;
        suppose A4:i = j;
          Swap(f, i, j).i
          = Replace(F, j, f/.i).i by A1,Def2
         .= f/.i by A3,A4,Lm2
         .= f.i by A2,FINSEQ_4:def 4;
         hence thesis by A4;
        suppose A5:i <> j;
        A6:Swap(f, i, j).i
          = Replace(F, j, f/.i).i by A1,Def2
         .= F.i by A5,FUNCT_7:34
         .= f/.j by A1,Lm2;
          Swap(f, i, j).j
          = Replace(F, j, f/.i).j by A1,Def2
         .= f/.i by A3,Lm2;
         hence thesis by A2,A6,FINSEQ_4:def 4;
  end;

theorem Th21:
  Swap(f, i, i) = f
  proof
    per cases;
      suppose
        1 <= i & i <= len f;
        then Swap(f, i, i)
          = Replace(Replace(f, i, f/.i), i, f/.i) by Def2
         .= Replace(f, i, f/.i) by FUNCT_7:40;
      hence thesis by FUNCT_7:40;
      suppose not (1 <= i & i <= len f);
      hence thesis by Def2;
  end;

theorem
    Swap(Swap(f,i,j),j,i) = f
proof
  per cases;
  suppose A1:1 <= i & i <= len f & 1 <= j & j <= len f;
    A2:len Swap(Swap(f,i,j),j,i) = len Swap(f,i,j) by Th20
                               .= len f by Th20;
      for k be Nat st 1 <= k & k <= len f
      holds f.k = Swap(Swap(f,i,j),j,i).k
    proof
      let k;
      assume A3: 1 <= k & k <= len f;
      then A4:k <= len Swap(f,i,j) by Th20;
      A5:j <= len Swap(f,i,j) by A1,Th20;
      A6:i <= len Swap(f,i,j) by A1,Th20;
            now per cases;
            suppose A7:i = k;
                now
                    Swap(Swap(f,i,j),j,i).k
                         = Swap(f,k,j).j by A1,A4,A5,A7,Lm3;
                  hence thesis by A1,A3,Lm3;
              end;
              hence thesis;
            suppose A8:i <> k;
                now per cases;
                suppose j = k;
                  then Swap(Swap(f,i,j),j,i).k
                         = Swap(f,i,k).i by A1,A4,A6,Lm3;
                  hence thesis by A1,A3,Lm3;
                suppose A9:j <> k;
                  set S = Swap(f,i,j);
                    Swap(S,j,i).k
                    = Replace(Replace(S,j,S/.i),i,S/.j).k by A1,A5,A6,Def2
                   .= Replace(S,j,S/.i).k by A8,FUNCT_7:34
                   .= S.k by A9,FUNCT_7:34
                   .= Replace(Replace(f,i,f/.j),j,f/.i).k by A1,Def2
                   .= Replace(f,i,f/.j).k by A9,FUNCT_7:34;
                  hence thesis by A8,FUNCT_7:34;
              end;
              hence thesis;
      end;
      hence thesis;
    end;
    hence thesis by A2,FINSEQ_1:18;
  suppose A10: not (1 <= i & i <= len f & 1 <= j & j <= len f);
    then Swap(Swap(f,i,j),j,i) = Swap(f,j,i) by Def2;
    hence thesis by A10,Def2;
end;

theorem Th23:
  Swap(f, i, j) = Swap(f, j, i)
proof
  per cases;
  suppose A1: 1 <= i & i <= len f & 1 <= j & j <= len f;
    set FI = Replace(f,i,f/.j);
    set FJ = Replace(f,j,f/.i);
    A2:len Swap(f,i,j) = len f by Th20
                     .= len Swap(f,j,i) by Th20;
      for k st 1 <= k & k <= len Swap(f,i,j)
      holds Swap(f,i,j).k = Swap(f,j,i).k
    proof
      let k;
      assume A3:1 <= k & k <= len Swap(f,i,j);
      then A4:1 <= k & k <= len f by Th20;
A5:   len Swap(f,i,j) = len f by Th20
                     .= len FI by Th7;
A6:   len Swap(f,i,j) = len f by Th20
                     .= len FJ by Th7;
            now per cases;
            suppose A7:i = k;
                now per cases;
                suppose A8:j = k;
                  then Swap(f,i,k).k
                    = Replace(FI,k,f/.i).k by A1,Def2
                   .= f/.i by A3,A5,Lm2
                   .= Replace(FJ,k,f/.i).k by A3,A6,Lm2
                   .= Swap(f,k,i).k by A1,A7,A8,Def2;
                  hence thesis by A8;
                suppose A9:j <> k;
                    Swap(f,i,j).k
                    = Replace(FI,j,f/.i).k by A1,Def2
                   .= Replace(f,k,f/.j).k by A7,A9,FUNCT_7:34
                   .= f/.j by A4,Lm2
                   .= Replace(FJ,k,f/.j).k by A3,A6,Lm2;
                  hence thesis by A1,A7,Def2;
              end;
              hence thesis;
            suppose A10:i <> k;
                now per cases;
                suppose A11:j = k;
                  then Swap(f,i,j).k
                    = Replace(FI,k,f/.i).k by A1,Def2
                   .= f/.i by A3,A5,Lm2
                   .= FJ.k by A4,A11,Lm2
                   .= Replace(FJ,i,f/.j).k by A10,FUNCT_7:34;
                  hence thesis by A1,Def2;
                suppose A12:j <> k;
                    Swap(f,i,j).k
                    = Replace(FI,j,f/.i).k by A1,Def2
                   .= FI.k by A12,FUNCT_7:34
                   .= f.k by A10,FUNCT_7:34
                   .= Replace(f,j,f/.i).k by A12,FUNCT_7:34
                   .= Replace(FJ,i,f/.j).k by A10,FUNCT_7:34;
                  hence thesis by A1,Def2;
              end;
              hence thesis;
          end;
      hence thesis;
    end;
    hence thesis by A2,FINSEQ_1:18;
  suppose A13: not (1 <= i & i <= len f & 1 <= j & j <= len f);
    then Swap(f, i, j) = f by Def2;
    hence thesis by A13,Def2;
end;

theorem
    rng Swap(f,i,j) = rng f
proof
  per cases;
  suppose A1: 1 <= i & i <= len f & 1 <= j & j <= len f;
    then A2:i in dom f by FINSEQ_3:27;
    A3:j in dom f by A1,FINSEQ_3:27;
      now per cases by AXIOMS:21;
    suppose A4:j < i;
      set F = Replace(f,i,f/.j);
      A5:j <= len F by A1,Th7;
      set fp = f|(i-'1);
      set fj = <*f/.j*>;
      set P = fp^fj;
      set Q = f/^i;
        i -'1 <= i by GOBOARD9:2;
      then A6:i -'1 <= len f by A1,AXIOMS:22;
      A7: len P = len fp + len fj by FINSEQ_1:35
                .= len fp + 1 by FINSEQ_1:56
                .= i -'1 + 1 by A6,TOPREAL1:3
                .= i by A1,AMI_5:4;
        1 + j <= i by A4,INT_1:20;
      then j <= i -' 1 by SPRECT_3:8;
      then A8:j <= len fp by A6,TOPREAL1:3;
      A9:j-'1 <= len P by A4,A7,JORDAN3:7;
      A10:j -'1 < i -'1 by A1,A4,SPRECT_3:9;
      then A11:j-'1 <= len fp by A6,TOPREAL1:3;
        rng Swap(f,i,j) = rng Replace(F,j,f/.i) by A1,Def2
       .= rng ((F|(j-'1))^<*f/.i*>^(F/^j)) by A1,A5,Def1
       .= rng ((F|(j-'1))^<*f.i*>^(F/^j)) by A2,FINSEQ_4:def 4
       .= rng ((F|(j-'1))^<*f.i*>^((P^Q)/^j)) by A1,Def1
       .= rng ((F|(j-'1))^<*f.i*>^((P/^j)^Q)) by A4,A7,GENEALG1:1
       .= rng ((F|(j-'1))^<*f.i*>^(((fp/^j)^fj)^Q)) by A8,GENEALG1:1
       .= rng ((F|(j-'1))^<*f.i*>^((((f/^j)|((i-'1)-'j))^fj)^Q)) by JORDAN3:21
       .= rng ((F|(j-'1))^<*f.i*>^(((f/^j)|((i-'1)-'j))^fj)^Q) by FINSEQ_1:45
       .= rng ((F|(j-'1))^<*f.i*>^((f/^j)|((i-'1)-'j))^fj^Q) by FINSEQ_1:45
       .= rng (((P^Q)|(j-'1))^<*f.i*>^(f/^j)|((i-'1)-'j)^fj^Q) by A1,Def1
       .= rng ((P|(j-'1))^<*f.i*>^(f/^j)|((i-'1)-'j)^fj^Q) by A9,FINSEQ_5:25
       .= rng ((fp|(j-'1))^<*f.i*>^(f/^j)|((i-'1)-'j)^fj^Q) by A11,FINSEQ_5:25
       .= rng ((f|(j-'1))^<*f.i*>^(f/^j)|((i-'1)-'j)^fj^Q) by A10,JORDAN4:15
       .= rng ((f|(j-'1))^<*f.i*>^(f/^j)|((i-'1)-'j)^<*f.j*>^Q)
                                                        by A3,FINSEQ_4:def 4
       .= rng ((f|(j-'1))^<*f.i*>^(f/^j)|(i-'j-'1)^<*f.j*>^Q) by Lm1
       .= rng (((f|(j-'1))^<*f.i*>^(f/^j)|(i-'j-'1))^(<*f.j*>^Q))
                                                        by FINSEQ_1:45
       .= rng ((f|(j-'1))^<*f.i*>^(f/^j)|(i-'j-'1)) \/ rng (<*f.j*>^Q)
                                                        by FINSEQ_1:44
       .= rng (((f|(j-'1)))^(<*f.i*>^(f/^j)|(i-'j-'1))) \/ rng (<*f.j*>^Q)
                                                        by FINSEQ_1:45
       .= rng (f|(j-'1)) \/ rng (<*f.i*>^(f/^j)|(i-'j-'1)) \/ rng (<*f.j*>^Q)
                                                        by FINSEQ_1:44
       .= rng (f|(j-'1)) \/ (rng <*f.i*> \/ rng ((f/^j)|(i-'j-'1)))
                                      \/ rng (<*f.j*>^Q) by FINSEQ_1:44
       .= rng (f|(j-'1)) \/ (rng <*f.i*> \/ rng ((f/^j)|(i-'j-'1)))
                                 \/ (rng <*f.j*> \/ rng Q) by FINSEQ_1:44
       .= rng (f|(j-'1)) \/ rng ((f/^j)|(i-'j-'1)) \/ rng <*f.i*>
                                 \/ (rng <*f.j*> \/ rng Q) by XBOOLE_1:4
       .= rng (f|(j-'1)) \/ rng ((f/^j)|(i-'j-'1)) \/ rng <*f.i*>
                                 \/ rng <*f.j*> \/ rng Q by XBOOLE_1:4
       .= rng (f|(j-'1)) \/ rng ((f/^j)|(i-'j-'1)) \/ rng <*f.j*>
                                 \/ rng <*f.i*> \/ rng Q by XBOOLE_1:4
       .= rng (f|(j-'1)) \/ (rng ((f/^j)|(i-'j-'1)) \/ rng <*f.j*>)
                                 \/ rng <*f.i*> \/ rng Q by XBOOLE_1:4
       .= rng (f|(j-'1)) \/ rng (<*f.j*>^((f/^j)|(i-'j-'1)))
                                 \/ rng <*f.i*> \/ rng Q by FINSEQ_1:44
       .= rng (f|(j-'1)) \/ rng (<*f.j*>^((f/^j)|(i-'j-'1)))
                                 \/ (rng <*f.i*> \/ rng Q) by XBOOLE_1:4
       .= rng (f|(j-'1)) \/ rng (<*f.j*>^((f/^j)|(i-'j-'1)))
                                 \/ rng (<*f.i*>^Q) by FINSEQ_1:44
       .= rng (f|(j-'1)) \/ (rng (<*f.j*>^((f/^j)|(i-'j-'1)))
                                 \/ rng (<*f.i*>^Q)) by XBOOLE_1:4
       .= rng (f|(j-'1)) \/ rng ((<*f.j*>^((f/^j)|(i-'j-'1)))^(<*f.i*>^Q))
                                                    by FINSEQ_1:44
       .= rng ((f|(j-'1))^((<*f.j*>^((f/^j)|(i-'j-'1)))^(<*f.i*>^Q)))
                                                    by FINSEQ_1:44
       .= rng ((f|(j-'1))^(<*f.j*>^(((f/^j)|(i-'j-'1))^(<*f.i*>^Q))))
                                                    by FINSEQ_1:45
       .= rng ((f|(j-'1))^(<*f.j*>^(((f/^j)|(i-'j-'1))^<*f.i*>^Q)))
                                                    by FINSEQ_1:45
       .= rng ((f|(j-'1))^<*f.j*>^(((f/^j)|(i-'j-'1))^<*f.i*>^Q))
                                                    by FINSEQ_1:45
       .= rng ((f|(j-'1))^<*f.j*>^((f/^j)|(i-'j-'1)^(<*f.i*>^Q)))
                                                    by FINSEQ_1:45
       .= rng ((f|(j-'1))^<*f.j*>^(f/^j)|(i-'j-'1)^(<*f.i*>^Q))
                                                    by FINSEQ_1:45
       .= rng ((f|(j-'1))^<*f.j*>^(f/^j)|(i-'j-'1)^<*f.i*>^Q)
                                                    by FINSEQ_1:45
       .= rng f by A1,A4,Th1;
      hence thesis;
    suppose A12:i < j;
      set F = Replace(f,j,f/.i);
      A13:i <= len F by A1,Th7;
      set fp = f|(j-'1);
      set fj = <*f/.i*>;
      set P = fp^fj;
      set Q = f/^j;
        j -'1 <= j by GOBOARD9:2;
      then A14:j -'1 <= len f by A1,AXIOMS:22;
      A15: len P = len fp + len fj by FINSEQ_1:35
                .= len fp + 1 by FINSEQ_1:56
                .= j -'1 + 1 by A14,TOPREAL1:3
                .= j by A1,AMI_5:4;
        1 + i <= j by A12,INT_1:20;
      then i <= j -' 1 by SPRECT_3:8;
      then A16:i <= len fp by A14,TOPREAL1:3;
      A17:i-'1 <= len P by A12,A15,JORDAN3:7;
      A18:i -'1 < j -'1 by A1,A12,SPRECT_3:9;
      then A19:i-'1 <= len fp by A14,TOPREAL1:3;
        rng Swap(f,i,j)
        = rng Swap(f,j,i) by Th23
       .= rng Replace(F,i,f/.j) by A1,Def2
       .= rng ((F|(i-'1))^<*f/.j*>^(F/^i)) by A1,A13,Def1
       .= rng ((F|(i-'1))^<*f.j*>^(F/^i)) by A3,FINSEQ_4:def 4
       .= rng ((F|(i-'1))^<*f.j*>^((P^Q)/^i)) by A1,Def1
       .= rng ((F|(i-'1))^<*f.j*>^((P/^i)^Q)) by A12,A15,GENEALG1:1
       .= rng ((F|(i-'1))^<*f.j*>^(((fp/^i)^fj)^Q)) by A16,GENEALG1:1
       .= rng ((F|(i-'1))^<*f.j*>^((((f/^i)|((j-'1)-'i))^fj)^Q)) by JORDAN3:21
       .= rng ((F|(i-'1))^<*f.j*>^(((f/^i)|((j-'1)-'i))^fj)^Q) by FINSEQ_1:45
       .= rng ((F|(i-'1))^<*f.j*>^((f/^i)|((j-'1)-'i))^fj^Q) by FINSEQ_1:45
       .= rng (((P^Q)|(i-'1))^<*f.j*>^(f/^i)|((j-'1)-'i)^fj^Q) by A1,Def1
       .= rng ((P|(i-'1))^<*f.j*>^(f/^i)|((j-'1)-'i)^fj^Q) by A17,FINSEQ_5:25
       .= rng ((fp|(i-'1))^<*f.j*>^(f/^i)|((j-'1)-'i)^fj^Q) by A19,FINSEQ_5:25
       .= rng ((f|(i-'1))^<*f.j*>^(f/^i)|((j-'1)-'i)^fj^Q) by A18,JORDAN4:15
       .= rng ((f|(i-'1))^<*f.j*>^(f/^i)|((j-'1)-'i)^<*f.i*>^Q)
                                                        by A2,FINSEQ_4:def 4
       .= rng ((f|(i-'1))^<*f.j*>^(f/^i)|(j-'i-'1)^<*f.i*>^Q) by Lm1
       .= rng (((f|(i-'1))^<*f.j*>^(f/^i)|(j-'i-'1))^(<*f.i*>^Q))
                                                        by FINSEQ_1:45
       .= rng ((f|(i-'1))^<*f.j*>^(f/^i)|(j-'i-'1)) \/ rng (<*f.i*>^Q)
                                                        by FINSEQ_1:44
       .= rng (((f|(i-'1)))^(<*f.j*>^(f/^i)|(j-'i-'1))) \/ rng (<*f.i*>^Q)
                                                        by FINSEQ_1:45
       .= rng (f|(i-'1)) \/ rng (<*f.j*>^(f/^i)|(j-'i-'1)) \/ rng (<*f.i*>^Q)
                                                        by FINSEQ_1:44
       .= rng (f|(i-'1)) \/ (rng <*f.j*> \/ rng ((f/^i)|(j-'i-'1)))
                                      \/ rng (<*f.i*>^Q) by FINSEQ_1:44
       .= rng (f|(i-'1)) \/ (rng <*f.j*> \/ rng ((f/^i)|(j-'i-'1)))
                                 \/ (rng <*f.i*> \/ rng Q) by FINSEQ_1:44
       .= rng (f|(i-'1)) \/ rng ((f/^i)|(j-'i-'1)) \/ rng <*f.j*>
                                 \/ (rng <*f.i*> \/ rng Q) by XBOOLE_1:4
       .= rng (f|(i-'1)) \/ rng ((f/^i)|(j-'i-'1)) \/ rng <*f.j*>
                                 \/ rng <*f.i*> \/ rng Q by XBOOLE_1:4
       .= rng (f|(i-'1)) \/ rng ((f/^i)|(j-'i-'1)) \/ rng <*f.i*>
                                 \/ rng <*f.j*> \/ rng Q by XBOOLE_1:4
       .= rng (f|(i-'1)) \/ (rng ((f/^i)|(j-'i-'1)) \/ rng <*f.i*>)
                                 \/ rng <*f.j*> \/ rng Q by XBOOLE_1:4
       .= rng (f|(i-'1)) \/ rng (<*f.i*>^((f/^i)|(j-'i-'1)))
                                 \/ rng <*f.j*> \/ rng Q by FINSEQ_1:44
       .= rng (f|(i-'1)) \/ rng (<*f.i*>^((f/^i)|(j-'i-'1)))
                                 \/ (rng <*f.j*> \/ rng Q) by XBOOLE_1:4
       .= rng (f|(i-'1)) \/ rng (<*f.i*>^((f/^i)|(j-'i-'1)))
                                 \/ rng (<*f.j*>^Q) by FINSEQ_1:44
       .= rng (f|(i-'1)) \/ (rng (<*f.i*>^((f/^i)|(j-'i-'1)))
                                 \/ rng (<*f.j*>^Q)) by XBOOLE_1:4
       .= rng (f|(i-'1)) \/ rng ((<*f.i*>^((f/^i)|(j-'i-'1)))^(<*f.j*>^Q))
                                                    by FINSEQ_1:44
       .= rng ((f|(i-'1))^((<*f.i*>^((f/^i)|(j-'i-'1)))^(<*f.j*>^Q)))
                                                    by FINSEQ_1:44
       .= rng ((f|(i-'1))^(<*f.i*>^(((f/^i)|(j-'i-'1))^(<*f.j*>^Q))))
                                                    by FINSEQ_1:45
       .= rng ((f|(i-'1))^(<*f.i*>^(((f/^i)|(j-'i-'1))^<*f.j*>^Q)))
                                                    by FINSEQ_1:45
       .= rng ((f|(i-'1))^<*f.i*>^(((f/^i)|(j-'i-'1))^<*f.j*>^Q))
                                                    by FINSEQ_1:45
       .= rng ((f|(i-'1))^<*f.i*>^((f/^i)|(j-'i-'1)^(<*f.j*>^Q)))
                                                    by FINSEQ_1:45
       .= rng ((f|(i-'1))^<*f.i*>^(f/^i)|(j-'i-'1)^(<*f.j*>^Q)) by FINSEQ_1:45
       .= rng ((f|(i-'1))^<*f.i*>^(f/^i)|(j-'i-'1)^<*f.j*>^Q) by FINSEQ_1:45
       .= rng f by A1,A12,Th1;

      hence thesis;
    suppose i = j;
      hence thesis by Th21;
    end;
    hence thesis;
  suppose not (1 <= i & i <= len f & 1 <= j & j <= len f);
    hence thesis by Def2;
end;

theorem
    Swap(<*p1, p2*>, 1, 2) = <*p2, p1*>
proof
  set f = <*p1,p2*>;
  A1:len f = 2 by FINSEQ_1:61;
  then 1 in dom f by FINSEQ_3:27;
  then A2:f/.1 = f.1 by FINSEQ_4:def 4
            .= p1 by FINSEQ_1:61;
    2 in dom f by A1,FINSEQ_3:27;
  then A3:f/.2 = f.2 by FINSEQ_4:def 4
            .= p2 by FINSEQ_1:61;
    Swap(f,1,2) = Replace(Replace(f,1,f/.2),2,f/.1) by A1,Def2
             .= Replace(<*p2,p2*>,2,f/.1) by A3,Th15;
  hence thesis by A2,Th16;
end;

theorem
    Swap(<*p1, p2, p3*>, 1, 2) = <*p2, p1, p3*>
proof
  set f = <*p1,p2,p3*>;
  A1:len f = 3 by FINSEQ_1:62;
  then 1 in dom f by FINSEQ_3:27;
  then A2:f/.1 = f.1 by FINSEQ_4:def 4
            .= p1 by FINSEQ_1:62;
    2 in dom f by A1,FINSEQ_3:27;
  then A3:f/.2 = f.2 by FINSEQ_4:def 4
            .= p2 by FINSEQ_1:62;
    Swap(f,1,2) = Replace(Replace(f,1,f/.2),2,f/.1) by A1,Def2
             .= Replace(<*p2,p2,p3*>,2,f/.1) by A3,Th17;
  hence thesis by A2,Th18;
end;

theorem
    Swap(<*p1, p2, p3*>, 1, 3) = <*p3, p2, p1*>
proof
  set f = <*p1,p2,p3*>;
  A1:len f = 3 by FINSEQ_1:62;
  then 1 in dom f by FINSEQ_3:27;
  then A2:f/.1 = f.1 by FINSEQ_4:def 4
            .= p1 by FINSEQ_1:62;
    3 in dom f by A1,FINSEQ_3:27;
  then A3:f/.3 = f.3 by FINSEQ_4:def 4
            .= p3 by FINSEQ_1:62;
    Swap(f,1,3) = Replace(Replace(f,1,f/.3),3,f/.1) by A1,Def2
             .= Replace(<*p3,p2,p3*>,3,f/.1) by A3,Th17;
  hence thesis by A2,Th19;
end;

theorem
    Swap(<*p1, p2, p3*>, 2, 3) = <*p1, p3, p2*>
proof
  set f = <*p1,p2,p3*>;
  A1:len f = 3 by FINSEQ_1:62;
  then 2 in dom f by FINSEQ_3:27;
  then A2:f/.2 = f.2 by FINSEQ_4:def 4
            .= p2 by FINSEQ_1:62;
    3 in dom f by A1,FINSEQ_3:27;
  then A3:f/.3 = f.3 by FINSEQ_4:def 4
            .= p3 by FINSEQ_1:62;
    Swap(f,2,3) = Replace(Replace(f,2,f/.3),3,f/.2) by A1,Def2
             .= Replace(<*p1,p3,p3*>,3,f/.2) by A3,Th18;
  hence thesis by A2,Th19;
end;

theorem Th29:
  1 <= i & i < j & j <= len f implies
    Swap(f, i, j) = (f|(i-'1))^<*f/.j*>^(f/^i)|(j-'i-'1)^<*f/.i*>^(f/^j)
proof
  assume A1:1 <= i & i < j & j <= len f;
  then A2:1 <= i & i <= len f & 1 <= j & j <= len f by AXIOMS:22;
    Swap(f,i,j) = Swap(f,j,i) by Th23
   .= Replace(Replace(f,j,f/.i),i,f/.j) by A2,Def2;
  hence thesis by A1,Th13;
end;

theorem
    1 < i & i <= len f implies
    Swap(f, 1, i) = <*f/.i*>^((f/^1)|(i-'2))^<*f/.1*>^(f/^i)
proof
  assume 1 < i & i <= len f;
  then Swap(f,1,i)
    = (f|(1-'1))^<*f/.i*>^(f/^1)|(i-'1-'1)^<*f/.1*>^(f/^i) by Th29
   .= (f|0)^<*f/.i*>^(f/^1)|(i-'1-'1)^<*f/.1*>^(f/^i) by GOBOARD9:1
   .= <*f/.i*>^(f/^1)|(i-'1-'1)^<*f/.1*>^(f/^i) by FINSEQ_1:47;
  hence thesis by JORDAN3:8;
end;

theorem
    1 <= i & i < len f implies
    Swap(f, i, len f)
      = (f|(i-'1))^<*f/.len f*>^((f/^i)|(len f-'i-'1))^<*f/.i*>
proof
  assume 1 <= i & i < len f;
  then Swap(f,i,len f)
    = (f|(i-'1))^<*f/.len f*>^(f/^i)|(len f-'i-'1)^<*f/.i*>^(f/^len f)
                                                               by Th29
   .= (f|(i-'1))^<*f/.len f*>^(f/^i)|(len f-'i-'1)^<*f/.i*>^{}
                                                               by REVROT_1:2;
  hence thesis by FINSEQ_1:47;
end;

Lm4:
  i <> k & j <> k implies Swap(f, i, j).k = f.k
proof
  per cases;
  suppose A1: 1 <= i & i <= len f & 1 <= j & j <= len f;
  assume A2: i <> k & j <> k;
  then Replace(Replace(f, i, f/.j), j, f/.i).k
      = Replace(f, i, f/.j).k by FUNCT_7:34
     .= f.k by A2,FUNCT_7:34;
  hence thesis by A1,Def2;
  suppose not (1 <= i & i <= len f & 1 <= j & j <= len f);
  hence thesis by Def2;
end;

theorem Th32:
  i <> k & j <> k & 1 <= k & k <= len f implies
    Swap(f, i, j)/.k = f/.k
proof
  assume A1: i <> k & j <> k & 1 <= k & k <= len f;
  then k <= len Swap(f, i, j) by Th20;
  then A2: k in dom Swap(f, i, j) by A1,FINSEQ_3:27;
  A3: k in dom f by A1,FINSEQ_3:27;
  thus Swap(f, i, j)/.k = Swap(f, i, j).k by A2,FINSEQ_4:def 4
   .= f.k by A1,Lm4
   .= f/.k by A3,FINSEQ_4:def 4;
end;

theorem Th33:
  1 <= i & i <= len f & 1 <= j & j <= len f
    implies Swap(f, i, j)/.i = f/.j & Swap(f, i, j)/.j = f/.i
proof
  assume A1: 1 <= i & i <= len f & 1 <= j & j <= len f;
  then A2:i in dom f & j in dom f by FINSEQ_3:27;
  set F = Swap(f,i,j);
    1 <= i & i <= len F & 1 <= j & j <= len F by A1,Th20;
  then A3:i in dom F & j in dom F by FINSEQ_3:27;
  then A4:F/.i = F.i by FINSEQ_4:def 4
        .= f.j by A1,Lm3
        .= f/.j by A2,FINSEQ_4:def 4;
    F/.j = F.j by A3,FINSEQ_4:def 4
        .= f.i by A1,Lm3
        .= f/.i by A2,FINSEQ_4:def 4;
  hence thesis by A4;
end;

begin :: Properties of composed function of Replace Function and Swap Function

theorem Th34:
  1 <= i & i <= len f & 1 <= j & j <= len f
    implies Replace(Swap(f, i, j), i, p) = Swap(Replace(f, j, p), i, j)
proof
  assume A1:1 <= i & i <= len f & 1 <= j & j <= len f;
  then A2:i in dom f by FINSEQ_3:27;
  per cases by AXIOMS:21;
    suppose A3:i = j;
      then Replace(Swap(f,i,j),i,p) = Replace(f,i,p) by Th21;
      hence thesis by A3,Th21;
    suppose A4:i < j;
      set F = Swap(f,i,j);
      set M = (f|(i-'1));
      set N = <*f/.j*>;
      set P = M^N;
      set Q = (f/^i)|(j-'i-'1)^(<*f/.i*>^(f/^j));
      A5:F = P^(f/^i)|(j-'i-'1)^<*f/.i*>^(f/^j) by A1,A4,Th29
           .= P^(f/^i)|(j-'i-'1)^(<*f/.i*>^(f/^j)) by FINSEQ_1:45
           .= P^((f/^i)|(j-'i-'1)^(<*f/.i*>^(f/^j))) by FINSEQ_1:45;
        i -'1 <= i by GOBOARD9:2;
      then A6:i -'1 <= len f by A1,AXIOMS:22;
      A7:len P = len M + len N by FINSEQ_1:35
               .= len M + 1 by FINSEQ_1:56
               .= i -'1 + 1 by A6,TOPREAL1:3
               .= i by A1,AMI_5:4;
        1 <= i & i <= len F & 1 <= j & j <= len F by A1,Th20;
      then A8:Replace(F,i,p)
        = (F|(i-'1))^<*p*>^(F/^len P) by A7,Def1
       .= (F|(i-'1))^<*p*>^Q by A5,FINSEQ_5:40
       .= ((M^(N^Q))|(i-'1))^<*p*>^Q by A5,FINSEQ_1:45
       .= ((M^(N^Q))|len M)^<*p*>^Q by A6,TOPREAL1:3
       .= M^<*p*>^Q by FINSEQ_5:26;
      set F1 = Replace(f,j,p);
      set G1 = (f|(j -'1));
      set H1 = <*p*>;
        j -'1 <= j by GOBOARD9:2;
      then A9:j -'1 <= len f by A1,AXIOMS:22;
      A10:len (G1^H1) = len G1 + len H1 by FINSEQ_1:35
               .= len G1 + 1 by FINSEQ_1:56
               .= j -'1 + 1 by A9,TOPREAL1:3
               .= j by A1,AMI_5:4;
      A11:i-'1 < j-'1 by A1,A4,SPRECT_3:9;
      then A12:i -'1 <= len G1 by A9,TOPREAL1:3;
      A13:F1/^j = (G1^H1^(f/^j))/^j by A1,Def1
           .= (f/^j) by A10,FINSEQ_5:40;
      A14:F1|(i-'1) = (G1^H1^(f/^j))|(i-'1) by A1,Def1
               .= (G1^(H1^(f/^j)))|(i-'1) by FINSEQ_1:45
               .= G1|(i-'1) by A12,FINSEQ_5:25
               .= f|(i-'1) by A11,JORDAN4:15;
      A15:(F1/^i)|(j-'i-'1) = (F1/^i)|(j-'(i+1)) by POLYNOM1:3
                       .= (F1/^i)|(j-'1-'i) by POLYNOM1:3
                       .= (F1|(j-'1))/^i by JORDAN3:21
                       .= ((G1^H1^(f/^j))|(j-'1))/^i by A1,Def1
                       .= ((G1^(H1^(f/^j)))|(j-'1))/^i by FINSEQ_1:45
                       .= ((G1^(H1^(f/^j)))|len G1)/^i by A9,TOPREAL1:3
                       .= G1/^i by FINSEQ_5:26
                       .= (f/^i)|((j-'1)-'i) by JORDAN3:21
                       .= (f/^i)|(j-'(1+i)) by POLYNOM1:3
                       .= (f/^i)|(j-'i-'1) by POLYNOM1:3;
      A16:1 <= i & i <= len F1 & 1 <= j & j <= len F1 by A1,Th7;
      then A17:i in dom F1 by FINSEQ_3:27;
      A18:j in dom F1 by A16,FINSEQ_3:27;
      A19:f.i = F1.i by A4,FUNCT_7:34
         .= F1/.i by A17,FINSEQ_4:def 4;
      A20:p = F1.j by A1,Lm2
       .= F1/.j by A18,FINSEQ_4:def 4;
        Swap(F1,i,j)
        = (F1|(i-'1))^<*F1/.j*>^(F1/^i)|(j-'i-'1)^<*F1/.i*>^(F1/^j)
                                                           by A4,A16,Th29
       .= M^<*p*>^(f/^i)|(j-'i-'1)^(<*f.i*>^(f/^j))
            by A13,A14,A15,A19,A20,FINSEQ_1:45
       .= M^<*p*>^(f/^i)|(j-'i-'1)^(<*f/.i*>^(f/^j)) by A2,FINSEQ_4:def 4
       .= M^<*p*>^((f/^i)|(j-'i-'1)^(<*f/.i*>^(f/^j))) by FINSEQ_1:45;
      hence thesis by A8;
    suppose A21:i > j;
      then consider k such that
        A22:i = j + k by NAT_1:28;
        i - j > j - j by A21,REAL_1:54;
      then A23:i - j > 0 by XCMPLX_1:14;
      A24:k = i - j by A22,XCMPLX_1:26
           .= i -'j by A23,BINARITH:def 3;
      A25:i-'j <> 0 by A23,BINARITH:def 3;
      then A26:i -'j >= 1 by RLVECT_1:99;
      A27:k >= 1 by A24,A25,RLVECT_1:99;
      set F = Swap(f,j,i);
      set M = (f|(j-'1));
      set N = <*f/.i*>;
      set P = M^N;
      set V = (f/^j)|(i-'j-'1);
      set W = <*f/.j*>;
      set X = f/^i;
      set Q = V^W^X;
      A28:F = P^V^W^X by A1,A21,Th29
           .= P^V^(W^X) by FINSEQ_1:45
           .= P^(V^(W^X)) by FINSEQ_1:45
           .= P^(V^W^X) by FINSEQ_1:45;
        j -'1 <= j by GOBOARD9:2;
      then A29:j -'1 <= len f by A1,AXIOMS:22;
      A30:len P = len M + len N by FINSEQ_1:35
               .= len M + 1 by FINSEQ_1:56
               .= j -'1 + 1 by A29,TOPREAL1:3
               .= j by A1,AMI_5:4;
        i -'1 <= i by GOBOARD9:2;
      then i -'1 <= len f by A1,AXIOMS:22;
      then i -'1-'j <= len f -'j by JORDAN3:5;
      then i -'1-'j <= len (f/^j) by JORDAN3:19;
      then i -'(1+j) <= len (f/^j) by POLYNOM1:3;
      then A31:i-'j-'1 <= len (f/^j) by POLYNOM1:3;
      A32:len (V^W) = len V + len W by FINSEQ_1:35
               .= len V + 1 by FINSEQ_1:56
               .= i-'j-'1 + 1 by A31,TOPREAL1:3
               .= i-'j by A26,AMI_5:4;
      A33:j - 1 >= 1 - 1 by A1,REAL_1:49;
      A34:k+j-'1 = k+j-1 by A27,JORDAN4:2
            .= k+(j-1) by XCMPLX_1:29
            .= k+(j-'1) by A33,BINARITH:def 3;
      A35:k = 1+(k-'1) by A27,AMI_5:4;
      A36:len V = k-'1 by A24,A31,TOPREAL1:3;
      A37:1 <= i & i <= len F & 1 <= j & j <= len F by A1,Th20;
      A38:Replace(Swap(f,i,j),i,p) = Replace(F,i,p) by Th23
       .= (F|(i-'1))^<*p*>^((P^Q)/^(j+k)) by A22,A28,A37,Def1
       .= (F|(i-'1))^<*p*>^(((V^W)^X)/^len (V^W)) by A24,A30,A32,FINSEQ_5:39
       .= (F|(k+(j-'1)))^<*p*>^X by A22,A34,FINSEQ_5:40
       .= ((M^(N^Q))|((j-'1)+k))^<*p*>^X by A28,FINSEQ_1:45
       .= ((M^(N^Q))|(len M +k))^<*p*>^X by A29,TOPREAL1:3
       .= (M^((N^Q)|k))^<*p*>^X by GENEALG1:2
       .= (M^((N^Q)|(len N+(k-'1))))^<*p*>^X by A35,FINSEQ_1:56
       .= (M^(N^(Q|(k-'1))))^<*p*>^X by GENEALG1:2
       .= (M^(N^((V^(W^X))|(k-'1))))^<*p*>^X by FINSEQ_1:45
       .= (M^(N^V))^<*p*>^X by A36,FINSEQ_5:26
       .= (M^N^V)^<*p*>^X by FINSEQ_1:45;
      set F1 = Replace(f,j,p);
      set G1 = (f|(j -'1));
      set H1 = <*p*>;
        j -'1 <= j by GOBOARD9:2;
      then A39:j -'1 <= len f by A1,AXIOMS:22;
      A40:len (G1^H1) = len G1 + len H1 by FINSEQ_1:35
               .= len G1 + 1 by FINSEQ_1:56
               .= j -'1 + 1 by A39,TOPREAL1:3
               .= j by A1,AMI_5:4;
      then A41:F1/^i = ((G1^H1)^(f/^j))/^(len (G1^H1)+k) by A1,A22,Def1
             .= f/^j/^k by FINSEQ_5:39
             .= f/^i by A22,FINSEQ_6:87;
      A42:k - 1 >= 1 - 1 by A27,REAL_1:49;
      A43:j+k-'1 = j+k-1 by A1,JORDAN4:2
            .= j+(k-1) by XCMPLX_1:29
            .= j+(k-'1) by A42,BINARITH:def 3;
      A44:F1|(j-'1) = (G1^H1^(f/^j))|(j-'1) by A1,Def1
                  .= (G1^(H1^(f/^j)))|(j-'1) by FINSEQ_1:45
                  .= (G1^(H1^(f/^j)))|len G1 by A39,TOPREAL1:3
                  .= G1 by FINSEQ_5:26;
      A45:(F1/^j)|(i-'j-'1)
        = (F1/^j)|(i-'(j+1)) by POLYNOM1:3
       .= (F1/^j)|(i-'1-'j) by POLYNOM1:3
       .= (F1|(i-'1))/^j by JORDAN3:21
       .= (((G1^H1)^(f/^j))|(j+(k-'1)))/^j by A1,A22,A43,Def1
       .= ((G1^H1)^((f/^j)|(k-'1)))/^len (G1^H1) by A40,GENEALG1:2
       .= (f/^j)|(i-'j-'1) by A24,FINSEQ_5:40;
      A46:1 <= i & i <= len F1 & 1 <= j & j <= len F1 by A1,Th7;
      then A47:i in dom F1 by FINSEQ_3:27;
      A48:j in dom F1 by A46,FINSEQ_3:27;
      A49:f.i = F1.i by A21,FUNCT_7:34
            .= F1/.i by A47,FINSEQ_4:def 4;
      A50:p = F1.j by A1,Lm2
          .= F1/.j by A48,FINSEQ_4:def 4;
        Swap(F1,i,j) = Swap(F1,j,i) by Th23
       .= (F1|(j-'1))^<*F1/.i*>^(F1/^j)|(i-'j-'1)^<*F1/.j*>^(F1/^i)
                                                   by A21,A46,Th29
       .= (f|(j-'1))^<*f/.i*>^(f/^j)|(i-'j-'1)^<*p*>^(f/^i)
                                        by A2,A41,A44,A45,A49,A50,FINSEQ_4:def
4;
      hence thesis by A38;
end;

theorem Th35:
  i <> k & j <> k & 1 <= i & i <= len f & 1 <= j
    & j <= len f & 1 <= k & k <= len f implies
    Swap(Replace(f, k, p), i, j) = Replace(Swap(f, i, j), k, p)
proof
  assume A1: i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f
      & 1 <= k & k <= len f;
    then A2: i <= len Replace(f, k, p) by Th7;
      j <= len Replace(f, k, p) by A1,Th7;
    hence Swap(Replace(f, k, p), i, j)
      = Replace(Replace(Replace(f, k, p), i,
        Replace(f, k, p)/.j), j, Replace(f, k, p)/.i) by A1,A2,Def2
     .= Replace(Replace(
        Replace(f, k, p), i, f/.j), j, Replace(f, k, p)/.i) by A1,Th12
     .= Replace(Replace(Replace(f, k, p), i, f/.j), j, f/.i) by A1,Th12
     .= Replace(Replace(Replace(f, i, f/.j), k, p), j, f/.i) by A1,FUNCT_7:35
     .= Replace(Replace(Replace(f, i, f/.j), j, f/.i), k, p) by A1,FUNCT_7:35
     .= Replace(Swap(f, i, j), k, p) by A1,Def2;
end;

theorem
    i <> k & j <> k & 1 <= i & i <= len f &
    1 <= j & j <= len f & 1 <= k & k <= len f implies
    Swap(Swap(f, i, j), j, k) = Swap(Swap(f, i, k), i, j)
proof
  assume A1: i <> k & j <> k & 1 <= i & i <= len f &
      1 <= j & j <= len f & 1 <= k & k <= len f;
    then A2: j <= len Swap(f, i, j) & k <= len Swap(f, i, j) by Th20;
    A3:i <= len Replace(f, i, f/.k) &
    j <= len Replace(f, i, f/.k) &
    k <= len Replace(f, i, f/.k) by A1,Th7;
    thus Swap(Swap(f, i, j), j, k)
      = Replace(Replace(Swap(f, i, j), j,
          Swap(f, i, j)/.k), k, Swap(f, i, j)/.j) by A1,A2,Def2
     .= Replace(Replace(Swap(f, i, j), j,
          Swap(f, i, j)/.k), k, f/.i) by A1,Th33
     .= Replace(Replace(Swap(f, i, j), j, f/.k), k, f/.i) by A1,Th32
     .= Replace(Replace(Swap(f, j, i), j, f/.k), k, f/.i) by Th23
     .= Replace(Swap(Replace(f, i, f/.k), j, i), k, f/.i) by A1,Th34
     .= Swap(Replace(Replace(f, i, f/.k), k, f/.i), j, i) by A1,A3,Th35
     .= Swap(Swap(f, i, k), j, i) by A1,Def2
     .= Swap(Swap(f, i, k), i, j) by Th23;
end;

theorem
      i <> k & j <> k & l <> i & l <> j &
    1 <= i & i <= len f & 1 <= j & j <= len f &
    1 <= k & k <= len f & 1 <= l & l <= len f implies
      Swap(Swap(f, i, j), k, l) = Swap(Swap(f, k, l), i, j)
proof
  assume A1: i <> k & j <> k & l <> i & l <> j &
    1 <= i & i <= len f & 1 <= j & j <= len f &
      1 <= k & k <= len f & 1 <= l & l <= len f;
  set F = Swap(f,i,j);
  A2: i <= len F & j <= len F & k <= len F & l <= len F by A1,Th20;
  A3:i <= len Replace(f,k,f/.l) & j <= len Replace(f,k,f/.l) &
  k <= len Replace(f,k,f/.l) & l <= len Replace(f,k,f/.l) by A1,Th7;
    Swap(F,k,l) = Replace(Replace(F,k,F/.l),l,F/.k) by A1,A2,Def2
   .= Replace(Replace(F,k,F/.l),l,f/.k) by A1,Th32
   .= Replace(Replace(F,k,f/.l),l,f/.k) by A1,Th32
   .= Replace(Replace(Swap(f,j,i),k,f/.l),l,f/.k) by Th23
   .= Replace(Swap(Replace(f,k,f/.l),j,i),l,f/.k) by A1,Th35
   .= Swap(Replace(Replace(f,k,f/.l),l,f/.k),j,i) by A1,A3,Th35
   .= Swap(Swap(f,k,l),j,i) by A1,Def2
   .= Swap(Swap(f,k,l),i,j) by Th23;
  hence thesis;
end;


Back to top