:: Algebraic group on Fixed-length bit integer and its adaptation
::  to {IDEA} Cryptography
::  by Yasushi Fuwa and Yoshinori Fujisawa
::
:: Received September 7, 1998
:: Copyright (c) 1998-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, SUBSET_1, FINSEQ_2, MARGREL1, CARD_1, ARYTM_3, INT_2,
      NAT_1, RELAT_1, XXREAL_0, INT_1, ARYTM_1, GRCAT_1, XBOOLEAN, FINSEQ_1,
      PARTFUN1, FUNCT_1, POWER, BINARI_3, FUNCOP_1, XBOOLE_0, BINARITH,
      MATRIX_1, INCSP_1, ORDINAL4, FUNCT_7, FUNCT_2, TARSKI, TREES_1, IDEA_1;
 notations TARSKI, XBOOLE_0,
      XTUPLE_0, SUBSET_1, NUMBERS, XCMPLX_0, INT_1, INT_2,
      ORDINAL1, NAT_1, NAT_D, MARGREL1, RELAT_1, FUNCT_1, FUNCOP_1, MATRIX_1,
      PARTFUN1, FUNCT_2, FUNCT_7, SERIES_1, FINSEQ_1, FINSEQ_2, RECDEF_1,
      BINARITH, BINARI_3, XXREAL_0;
 constructors NAT_D, SERIES_1, BINARITH, FUNCT_7, MATRIX_1, BINARI_3, RECDEF_1,
      RELSET_1, XTUPLE_0;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, XXREAL_0,
      XREAL_0, NAT_1, INT_1, FINSEQ_1, MARGREL1, FUNCT_7, VALUED_0, CARD_1,
      FINSEQ_2, RELSET_1, XTUPLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions FINSEQ_2, XBOOLEAN, XTUPLE_0;
 theorems NAT_1, NAT_2, NEWTON, INT_1, INT_2, FINSEQ_1, FINSEQ_2, FUNCT_1,
      FUNCT_2, FUNCT_7, FUNCOP_1, POWER, EULER_1, EULER_2, BINARITH, BINARI_3,
      MATRIX_1, RELSET_1, RELAT_1, XBOOLE_1, XREAL_1, XXREAL_0, XBOOLEAN,
      NAT_D, PARTFUN1, ORDINAL1, XREAL_0, CARD_1;
 schemes FINSEQ_1, FINSEQ_2, NAT_1, FUNCT_2;

begin ::Some selected theorems on integers

reserve i,j,k,n for Element of NAT;
reserve x,y,z for Tuple of n, BOOLEAN;

Lm1: i<>0 & i < j & j is prime implies i,j are_relative_prime
proof
  assume that
A1: i<>0 and
A2: i < j and
A3: j is prime;
  now
    set IJ = i gcd j;
A4: IJ <> j
    proof
      assume IJ = j;
      then j divides i by NAT_D:def 5;
      then consider n being Nat such that
A5:   i = j*n by NAT_D:def 3;
      n <> 0 by A1,A5;
      then j*n >= j*1 by NAT_1:14,XREAL_1:64;
      hence contradiction by A2,A5;
    end;
    IJ divides j by NAT_D:def 5;
    then IJ = 1 or IJ = j by A3,INT_2:def 4;
    hence thesis by A4,INT_2:def 3;
  end;
  hence thesis;
end;

Lm2: j is prime & i<j & k<j & i<>0 implies ex a being Element of NAT st (a*i)
mod j = k
proof
  assume that
A1: j is prime and
A2: i<j and
A3: k<j and
A4: i<>0;
  consider a,b being Integer such that
A5: a*i + b*j = k by A1,A2,A4,Lm1,EULER_1:10;
A6: j>0 by A1,INT_2:def 4;
  now
    per cases;
    suppose
A7:   a >= 0;
      now
        per cases;
        suppose
          b >= 0;
          then reconsider a,b as Element of NAT by A7,INT_1:3;
          take a;
          (a*i + b*j) mod j = (a*i + ((b*j) mod j)) mod j by NAT_D:23
            .= (a*i + 0) mod j by NAT_D:13
            .= (a*i) mod j;
          hence thesis by A3,A5,NAT_D:24;
        end;
        suppose
A8:       b < 0;
          reconsider a as Element of NAT by A7,INT_1:3;
          consider b9 being Integer such that
A9:       b9=0-b;
          take a;
          reconsider b9 as Element of NAT by A8,A9,INT_1:3;
          a*i + b*j + b9*j = a*i by A9;
          then (a*i) mod j = k mod j by A5,NAT_D:21
            .= k by A3,NAT_D:24;
          hence thesis;
        end;
      end;
      hence thesis;
    end;
    suppose
A10:  a < 0;
      consider a1 being Integer such that
A11:  a1 = 0 - a;
      reconsider a1 as Element of NAT by A10,A11,INT_1:3;
      consider a2 being Element of NAT such that
A12:  a2=(a1 div j) + 1;
      consider a9 being Integer such that
A13:  a9=a + a2 * j;
A14:  a9 = -a1 + (a1 div j)*j + j by A11,A12,A13;
      consider t being Nat such that
A15:  a1 = j * (a1 div j) + t and
A16:  t < j by A6,NAT_D:def 1;
      -t + t < -t + j by A16,XREAL_1:6;
      then reconsider a9 as Element of NAT by A14,A15,INT_1:3;
      now
        per cases;
        suppose
          b >= 0;
          then reconsider b as Element of NAT by INT_1:3;
          take a9;
A17:      (k + a2*j*i) mod j = (k + a2*i*j) mod j .= k mod j by NAT_D:21
            .= k by A3,NAT_D:24;
          a*i + b*j + a2*j*i = a9*i + b*j by A13;
          hence (a9*i) mod j = k by A5,A17,NAT_D:21;
        end;
        suppose
A18:      b < 0;
          take a9;
          consider b9 being Integer such that
A19:      b9=0-b;
          reconsider b9 as Element of NAT by A18,A19,INT_1:3;
          k + a2*j*i + b9*j = k + (a2*i+ b9)*j;
          hence (a9*i) mod j = k mod j by A5,A13,A19,NAT_D:21
            .= k by A3,NAT_D:24;
        end;
      end;
      hence thesis;
    end;
  end;
  hence thesis;
end;

theorem Th1:
  for i,j,k holds j is prime & i<j & k<j & i<>0 implies ex a being
  Element of NAT st (a*i) mod j = k & a < j
proof
  let i,j,k be Element of NAT;
  assume that
A1: j is prime and
A2: i<j and
A3: k<j & i<>0;
  consider a being Element of NAT such that
A4: (a*i) mod j = k by A1,A2,A3,Lm2;
  consider a9 being Element of NAT such that
A5: a9 = a mod j;
  take a9;
  thus thesis by A2,A4,A5,EULER_2:8,NAT_D:1;
end;

theorem Th2:
  for n,k1,k2 being Element of NAT holds n <> 0 & k1 mod n = k2 mod
  n & k1 <= k2 implies ex t being Element of NAT st k2 - k1 = n*t
proof
  let n,k1,k2 be Element of NAT;
  assume that
A1: n <> 0 and
A2: k1 mod n = k2 mod n and
A3: k1 <= k2;
  consider t being Integer such that
A4: t = (k2 div n) - (k1 div n);
  (k2 div n) >= (k1 div n) by A3,NAT_2:24;
  then (k2 div n) - (k1 div n) >= (k1 div n) - (k1 div n) by XREAL_1:9;
  then reconsider t as Element of NAT by A4,INT_1:3;
  take t;
  k1 = n * (k1 div n) + (k1 mod n) & k2 = n * (k2 div n) + (k2 mod n) by A1,
NAT_D:2;
  hence thesis by A2,A4;
end;

theorem Th3:
  for a, b being Element of NAT holds a - b <= a
proof
  let a, b be Element of NAT;
  a - b <= a - 0 by XREAL_1:13;
  hence thesis;
end;

theorem Th4:
  for b1,b2,c being Element of NAT holds b2 <= c implies b2 - b1 <= c
proof
  let b1,b2,c be Element of NAT;
  assume b2 <= c;
  then
A1: b2 - b1 <= c - b1 by XREAL_1:9;
  c - b1 <= c by Th3;
  hence thesis by A1,XXREAL_0:2;
end;

theorem Th5:
  for a,b,c being Element of NAT holds 0<a & 0<b & a<c & b<c & c is
  prime implies (a * b) mod c <> 0
proof
  let a,b,c be Element of NAT;
  assume that
A1: 0<a & 0<b and
A2: a<c and
A3: b<c and
A4: c is prime;
  assume (a * b) mod c = 0;
  then (a * b) = c * ((a * b) div c) + 0 by A2,NAT_D:2;
  then c divides (a * b) by NAT_D:def 3;
  then c divides a or c divides b by A4,NEWTON:80;
  hence contradiction by A1,A2,A3,NAT_D:7;
end;

begin :: Algebraic group on Fixed-length bit Integer
:: In this section,we construct an algebraic group on
:: Fixed-length bit Integer.
:: IDEA's Basic operators are 'xor', ADD_MOD and MUL_MOD.
:: 'xor' is 16-bitwise XOR. ADD_MOD is addition mod 2^{16}.
:: MUL_MOD is multiplication mod 2^(16)+1. And, we define
:: two functions NEG_MOD and INV_MOD that give inverse
:: element of ADD_MOD and MUL_MOD respectively.

definition
  let n;
  func ZERO( n ) -> Tuple of n, BOOLEAN equals
  n |-> FALSE;
  correctness;
end;

definition
  let n;
  let x, y be Tuple of n, BOOLEAN;
  func x 'xor' y -> Tuple of n, BOOLEAN means
  :Def2:
  for i st i in Seg n holds it/.i = (x/.i) 'xor' (y/.i);
  existence
  proof
    deffunc F(Nat)=(x/.$1) 'xor' (y/.$1);
    consider z being FinSequence of BOOLEAN such that
A1: len z = n and
A2: for j be Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
A3: dom z = Seg n by A1,FINSEQ_1:def 3;
    z is Element of n-tuples_on BOOLEAN by A1,FINSEQ_2:92;
    then reconsider z as Tuple of n, BOOLEAN;
    take z;
    let i;
    assume
A4: i in Seg n;
    then i in dom z by A1,FINSEQ_1:def 3;
    hence z/.i = z.i by PARTFUN1:def 6
      .= (x/.i) 'xor' (y/.i) by A2,A3,A4;
  end;
  uniqueness
  proof
    let z1, z2 be Tuple of n, BOOLEAN such that
A5: for i st i in Seg n holds z1/.i = (x/.i) 'xor' (y/.i) and
A6: for i st i in Seg n holds z2/.i = (x/.i) 'xor' (y/.i);
A7: len z1 = n by CARD_1:def 7;
    then
A8: dom z1 = Seg n by FINSEQ_1:def 3;
A9: len z2 = n by CARD_1:def 7;
    now
      let j be Nat;
      assume
A10:  j in dom z1;
      then
A11:  j in dom z2 by A9,A8,FINSEQ_1:def 3;
      thus z1.j = z1/.j by A10,PARTFUN1:def 6
        .= (x/.j) 'xor' (y/.j) by A5,A8,A10
        .= z2/.j by A6,A8,A10
        .= z2.j by A11,PARTFUN1:def 6;
    end;
    hence thesis by A7,A9,FINSEQ_2:9;
  end;
end;

theorem Th6:
  for n,x holds x 'xor' x = ZERO(n)
proof
  let n;
  let x be Tuple of n, BOOLEAN;
A1: len (x 'xor' x) = n by CARD_1:def 7;
  then
A2: dom (x 'xor' x) = Seg n by FINSEQ_1:def 3;
A3: now
    let j be Nat;
    assume
A4: j in dom (x 'xor' x);
A5: ZERO(n).j = FALSE;
    thus (x 'xor' x).j = (x 'xor' x)/.j by A4,PARTFUN1:def 6
      .= (x/.j) 'xor' (x/.j) by A2,A4,Def2
      .= ZERO(n).j by A5,XBOOLEAN:138;
  end;
  len (ZERO(n)) = n by CARD_1:def 7;
  hence thesis by A1,A3,FINSEQ_2:9;
end;

theorem Th7:
  for n,x,y holds x 'xor' y = y 'xor' x
proof
  let n;
  let x,y be Tuple of n, BOOLEAN;
A1: len (x 'xor' y) = n by CARD_1:def 7;
  then
A2: dom (x 'xor' y) = Seg n by FINSEQ_1:def 3;
A3: len (y 'xor' x) = n by CARD_1:def 7;
  now
    let j be Nat;
    assume
A4: j in dom (x 'xor' y);
    then
A5: j in dom (y 'xor' x) by A3,A2,FINSEQ_1:def 3;
    thus (x 'xor' y).j = (x 'xor' y)/.j by A4,PARTFUN1:def 6
      .= (y/.j) 'xor' (x/.j) by A2,A4,Def2
      .= (y 'xor' x)/.j by A2,A4,Def2
      .= (y 'xor' x).j by A5,PARTFUN1:def 6;
  end;
  hence thesis by A1,A3,FINSEQ_2:9;
end;

definition
  let n;
  let x, y be Tuple of n, BOOLEAN;
  redefine func x 'xor' y;
  commutativity by Th7;
end;

theorem Th8:
  for n,x holds ZERO(n) 'xor' x = x
proof
  let n;
  let x be Tuple of n, BOOLEAN;
A1: len ((ZERO(n)) 'xor' x) = n by CARD_1:def 7;
  then
A2: dom ((ZERO(n)) 'xor' x) = Seg n by FINSEQ_1:def 3;
A3: len x = n by CARD_1:def 7;
  now
    let j be Nat;
    assume
A4: j in dom ((ZERO(n)) 'xor' x);
    then
A5: j in dom x by A3,A2,FINSEQ_1:def 3;
    j in dom (ZERO(n)) by A2,A4,FUNCOP_1:13;
    then
A6: (ZERO(n))/.j = (n |-> FALSE).j by PARTFUN1:def 6
      .= FALSE;
    thus ((ZERO(n)) 'xor' x).j = ((ZERO(n)) 'xor' x)/.j by A4,PARTFUN1:def 6
      .= FALSE 'xor' (x/.j) by A2,A4,A6,Def2
      .= x/.j by BINARITH:8
      .= x.j by A5,PARTFUN1:def 6;
  end;
  hence thesis by A1,A3,FINSEQ_2:9;
end;

theorem Th9:
  for n,x,y,z holds (x 'xor' y) 'xor' z = x 'xor' (y 'xor' z)
proof
  let n;
  let x,y,z be Tuple of n, BOOLEAN;
A1: len ((x 'xor' y) 'xor' z) = n by CARD_1:def 7;
  then
A2: dom ((x 'xor' y) 'xor' z) = Seg n by FINSEQ_1:def 3;
A3: len (x 'xor' (y 'xor' z)) = n by CARD_1:def 7;
  now
    let j be Nat;
    assume
A4: j in dom ((x 'xor' y) 'xor' z);
    then
A5: j in dom (x 'xor' (y 'xor' z)) by A3,A2,FINSEQ_1:def 3;
    thus ((x 'xor' y) 'xor' z).j = ((x 'xor' y) 'xor' z)/.j by A4,
PARTFUN1:def 6
      .= ((x 'xor' y)/.j) 'xor' (z/.j) by A2,A4,Def2
      .= ((x/.j) 'xor' (y/.j)) 'xor' (z/.j) by A2,A4,Def2
      .= (x/.j) 'xor' ((y/.j) 'xor' (z/.j)) by XBOOLEAN:73
      .= (x/.j) 'xor' ((y 'xor' z)/.j) by A2,A4,Def2
      .= ((x 'xor' (y 'xor' z)))/.j by A2,A4,Def2
      .= (x 'xor' (y 'xor' z)).j by A5,PARTFUN1:def 6;
  end;
  hence thesis by A1,A3,FINSEQ_2:9;
end;

definition
  let n;
  let i be Element of NAT;
  pred i is_expressible_by n means
  :Def3:
  i < 2 to_power(n);
end;

theorem
  for n holds n-BinarySequence 0 = ZERO(n)
proof
  let n;
A1: len (n-BinarySequence 0) = n by CARD_1:def 7;
  then
A2: dom (n-BinarySequence 0) = Seg n by FINSEQ_1:def 3;
A3: len (ZERO(n)) = n by CARD_1:def 7;
  then
A4: dom ZERO(n) = Seg n by FINSEQ_1:def 3;
A5: dom (n-BinarySequence 0) = Seg n by A1,FINSEQ_1:def 3;
  now
    let j be Nat;
A6: (0 div 2 to_power(j-'1)) mod 2 = 0 mod 2 by NAT_2:2
      .= 0 by NAT_D:26;
    assume
A7: j in dom (n-BinarySequence 0);
    then j in dom (ZERO(n)) by A2,FUNCOP_1:13;
    then
A8: (ZERO(n))/.j = (n |-> FALSE).j by PARTFUN1:def 6
      .= FALSE;
    thus (n-BinarySequence 0).j = (n-BinarySequence 0)/.j by A7,PARTFUN1:def 6
      .= IFEQ((0 div 2 to_power(j-'1)) mod 2,0,FALSE,TRUE) by A2,A7,
BINARI_3:def 1
      .= (ZERO(n))/.j by A6,A8,FUNCOP_1:def 8
      .= ZERO(n).j by A5,A4,A7,PARTFUN1:def 6;
  end;
  hence thesis by A1,A3,FINSEQ_2:9;
end;

definition
  let n;
  let i, j be Nat;
  func ADD_MOD(i,j,n) -> Element of NAT equals
  (i + j) mod 2 to_power(n);
  coherence;
end;

definition
  let n;
  let i be Element of NAT;
  assume
A1: i is_expressible_by n;
  func NEG_N(i,n) -> Element of NAT equals
  :Def5:
  2 to_power(n) - i;
  coherence
  proof
    i < 2 to_power(n) by A1,Def3;
    then 2 to_power(n) - i > i - i by XREAL_1:9;
    hence thesis by INT_1:3;
  end;
end;

definition
  let n;
  let i be Element of NAT;
  func NEG_MOD(i,n) -> Element of NAT equals
  NEG_N(i,n) mod 2 to_power(n);
  coherence;
end;

theorem Th11:
  i is_expressible_by n implies ADD_MOD(i, NEG_MOD(i,n), n) = 0
proof
  assume i is_expressible_by n;
  then i + NEG_N(i,n) = i + (2 to_power(n) - i) by Def5
    .= 0 + 2 to_power(n);
  hence ADD_MOD(i, NEG_MOD(i,n), n) = 2 to_power(n) mod 2 to_power(n) by
NAT_D:23
    .= 0 by NAT_D:25;
end;

theorem
  ADD_MOD(i,j,n) = ADD_MOD(j,i,n);

theorem Th13:
  i is_expressible_by n implies ADD_MOD(0,i,n) = i
proof
  assume i is_expressible_by n;
  then i < 2 to_power(n) by Def3;
  hence thesis by NAT_D:24;
end;

theorem Th14:
  ADD_MOD(ADD_MOD(i,j,n),k,n) = ADD_MOD(i,ADD_MOD(j,k,n),n)
proof
  thus ADD_MOD(ADD_MOD(i,j,n),k,n) = (i+j+k) mod 2 to_power(n) by NAT_D:23
    .= (i+(j+k)) mod 2 to_power(n)
    .= ADD_MOD(i,ADD_MOD(j,k,n),n) by NAT_D:22;
end;

theorem Th15:
  ADD_MOD(i,j,n) is_expressible_by n
proof
  ADD_MOD(i,j,n) < 2 to_power(n) by NAT_D:1,POWER:34;
  hence thesis by Def3;
end;

theorem
  NEG_MOD(i,n) is_expressible_by n
proof
  NEG_MOD(i,n) < 2 to_power(n) by NAT_D:1,POWER:34;
  hence thesis by Def3;
end;

definition
  let n, i be Nat;
  func ChangeVal_1(i,n) -> Element of NAT equals
  :Def7:
  2 to_power(n) if i = 0
  otherwise i;
  coherence by ORDINAL1:def 12;
  correctness;
end;

theorem Th17:
  i is_expressible_by n implies ChangeVal_1(i,n) <= 2 to_power(n)
  & ChangeVal_1(i,n) > 0
proof
  assume
A1: i is_expressible_by n;
A2: 2 to_power(n) > 0 by POWER:34;
  per cases;
  suppose
    i=0;
    hence thesis by A2,Def7;
  end;
  suppose
A3: i<>0;
    then ChangeVal_1(i,n) = i by Def7;
    hence thesis by A1,A3,Def3;
  end;
end;

theorem Th18:
  for n,a1,a2 be Element of NAT holds a1 is_expressible_by n & a2
  is_expressible_by n & ChangeVal_1(a1,n) = ChangeVal_1(a2,n) implies a1 = a2
proof
  let n;
  let a1,a2 be Element of NAT;
  assume that
A1: a1 is_expressible_by n and
A2: a2 is_expressible_by n and
A3: ChangeVal_1(a1,n) = ChangeVal_1(a2,n);
A4: a1 <> 2 to_power(n) by A1,Def3;
A5: a2 <> 2 to_power(n) by A2,Def3;
  per cases;
  suppose
A6: ChangeVal_1(a1,n) = 2 to_power(n);
    hence a2 = 0 by A3,A5,Def7
      .= a1 by A4,A6,Def7;
  end;
  suppose
A7: ChangeVal_1(a1,n) <> 2 to_power(n);
    hence a2 = ChangeVal_1(a1,n) by A3,Def7
      .= a1 by A7,Def7;
  end;
end;

definition
  let n;
  let i be Element of NAT;
  func ChangeVal_2(i,n) -> Element of NAT equals
  :Def8:
  0 if i = 2 to_power(n)
  otherwise i;
  correctness;
end;

theorem
  i is_expressible_by n implies ChangeVal_2(i,n) is_expressible_by n
proof
  assume i is_expressible_by n;
  then i < 2 to_power(n) by Def3;
  then ChangeVal_2(i,n) < 2 to_power(n) by Def8;
  hence thesis by Def3;
end;

theorem Th20:
  for n,a1,a2 be Element of NAT holds a1 <> 0 & a2 <> 0 &
  ChangeVal_2(a1,n) = ChangeVal_2(a2,n) implies a1 = a2
proof
  let n;
  let a1,a2 be Element of NAT;
  assume that
A1: a1 <> 0 & a2 <> 0 and
A2: ChangeVal_2(a1,n) = ChangeVal_2(a2,n);
  per cases;
  suppose
A3: ChangeVal_2(a1,n) = 0;
    then a2 = 2 to_power(n) or a2 = 0 by A2,Def8;
    hence thesis by A1,A3,Def8;
  end;
  suppose
A4: ChangeVal_2(a1,n) <> 0;
    then
A5: a1 <> 2 to_power(n) by Def8;
    a2 <> 2 to_power(n) by A2,A4,Def8;
    hence a2 = ChangeVal_2(a1,n) by A2,Def8
      .= a1 by A5,Def8;
  end;
end;

definition
  let n;
  let i,j be Nat;
  func MUL_MOD(i,j,n) -> Element of NAT equals
  ChangeVal_2((ChangeVal_1(i,n)*
  ChangeVal_1(j,n)) mod (2 to_power(n)+1),n);
  coherence;
end;

definition
  let n be non empty Element of NAT;
  let i be Element of NAT;
  assume that
A1: i is_expressible_by n and
A2: (2 to_power(n) + 1) is prime;
  func INV_MOD(i,n) -> Element of NAT means
  :Def10:
  MUL_MOD(i,it,n) = 1 & it is_expressible_by n;
  existence
  proof
A3: 2 to_power(n) > 0 by POWER:34;
    then
A4: 2 to_power(n) + 1 > 0 + 1 by XREAL_1:6;
    then 2 to_power(n) + 1 - 1 >= 1 + 1 - 1 by NAT_1:13;
    then 2 to_power(n) + 1 - 1 - 1 >= 1 + 1 - 1 - 1 by XREAL_1:9;
    then reconsider n3=2 to_power(n) + 1 - 1 - 1 as Element of NAT by INT_1:3;
    reconsider nn=2 to_power(n) + 1 as Element of NAT;
    reconsider n2=2 to_power(n) + 1 - 1 as Element of NAT;
A5: 2 to_power(n) <> 1 by POWER:35;
    n2 * n2 = nn*n3 + 1;
    then
A6: (n2*n2) mod nn = 1 mod nn by NAT_D:21
      .= 1 by A4,NAT_D:24;
    now
      per cases;
      suppose
A7:     i=0;
        consider j such that
A8:     j = 0;
        take j;
A9:     j is_expressible_by n by A3,A8,Def3;
        MUL_MOD(i,j,n) = ChangeVal_2((2 to_power(n)*ChangeVal_1(0,n)) mod
        nn,n) by A7,A8,Def7
          .= ChangeVal_2((n2*n2) mod nn,n) by Def7
          .= 1 by A5,A6,Def8;
        hence thesis by A9;
      end;
      suppose
A10:    i<>0;
        i < 2 to_power(n) by A1,Def3;
        then i < 2 to_power(n)+1 by NAT_1:13;
        then consider a being Element of NAT such that
A11:    (a*i) mod (2 to_power(n)+1) = 1 and
A12:    a < (2 to_power(n)+1) by A2,A4,A10,Th1;
        take k=ChangeVal_2(a,n);
A13:    a <> 0 by A11,NAT_D:24;
        now
          per cases;
          suppose
A14:        a <> 2 to_power(n);
            then
A15:        k = a by Def8;
            then k <= 2 to_power(n) by A12,NAT_1:13;
            then k < 2 to_power(n) by A14,A15,XXREAL_0:1;
            then
A16:        k is_expressible_by n by Def3;
            MUL_MOD(i,k,n) = ChangeVal_2((i* ChangeVal_1(k,n)) mod (2
            to_power(n)+1),n) by A10,Def7
              .= ChangeVal_2((i*a)mod (2 to_power(n)+1),n) by A13,A15,Def7
              .= 1 by A5,A11,Def8;
            hence thesis by A16;
          end;
          suppose
A17:        a = 2 to_power(n);
            then
A18:        k = 0 by Def8;
            then
A19:        k is_expressible_by n by A3,Def3;
            MUL_MOD(i,k,n) = ChangeVal_2((i* ChangeVal_1(k,n)) mod (2
            to_power(n)+1),n) by A10,Def7
              .= ChangeVal_2((i*a)mod (2 to_power(n)+1),n) by A17,A18,Def7
              .= 1 by A5,A11,Def8;
            hence thesis by A19;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let a1, a2 be Element of NAT such that
A20: MUL_MOD(i,a1,n) = 1 and
A21: a1 is_expressible_by n and
A22: MUL_MOD(i,a2,n) = 1 and
A23: a2 is_expressible_by n;
    consider b2 being Element of NAT such that
A24: b2 = ChangeVal_1(a2,n);
    b2 <= 2 to_power(n) by A23,A24,Th17;
    then
A25: b2 < 2 to_power(n)+1 by NAT_1:13;
    consider b1 being Element of NAT such that
A26: b1 = ChangeVal_1(a1,n);
    b1 <= 2 to_power(n) by A21,A26,Th17;
    then
A27: b1 < 2 to_power(n)+1 by NAT_1:13;
    consider k being Element of NAT such that
A28: k = ChangeVal_1(i,n);
A29: k <= 2 to_power(n) by A1,A28,Th17;
    then
A30: k < 2 to_power(n)+1 by NAT_1:13;
A31: k > 0 by A1,A28,Th17;
    b2 > 0 by A23,A24,Th17;
    then
A32: (k * b2) mod (2 to_power(n)+1) <> 0 by A2,A31,A30,A25,Th5;
    b1 > 0 by A21,A26,Th17;
    then (k * b1) mod (2 to_power(n)+1) <> 0 by A2,A31,A30,A27,Th5;
    then
A33: (k * b1) mod (2 to_power(n)+1) = (k * b2) mod (2 to_power(n)+1) by A20,A22
,A28,A26,A24,A32,Th20;
    now
      per cases;
      suppose
A34:    b1 <= b2;
        consider b being Integer such that
A35:    b = b2 - b1;
        b1 - b1 <= b2 - b1 by A34,XREAL_1:9;
        then reconsider b as Element of NAT by A35,INT_1:3;
        ex t being Element of NAT st k*b2 - k*b1 = (2 to_power(n)+ 1)*t by A33
,A34,Th2,NAT_1:4;
        then (2 to_power(n)+1) divides k*b by A35,NAT_D:def 3;
        then
A36:    (2 to_power(n)+1) divides k or (2 to_power(n)+1) divides b by A2,
NEWTON:80;
        b <= 2 to_power(n) by A23,A24,A35,Th4,Th17;
        then
A37:    not (2 to_power(n)+1) <= b by NAT_1:13;
        not (2 to_power(n)+1) <= k by A29,NAT_1:13;
        then not 0 < b by A31,A36,A37,NAT_D:7;
        then b2 - b1 + b1 = 0 + b1 by A35;
        hence b1 = b2;
      end;
      suppose
A38:    b2 <= b1;
        consider b being Integer such that
A39:    b = b1 - b2;
        b2 - b2 <= b1 - b2 by A38,XREAL_1:9;
        then reconsider b as Element of NAT by A39,INT_1:3;
        ex t being Element of NAT st k*b1 - k*b2 = (2 to_power(n)+ 1)*t by A33
,A38,Th2,NAT_1:4;
        then (2 to_power(n)+1) divides k*b by A39,NAT_D:def 3;
        then
A40:    (2 to_power(n)+1) divides k or (2 to_power(n)+1) divides b by A2,
NEWTON:80;
        b <= 2 to_power(n) by A21,A26,A39,Th4,Th17;
        then
A41:    not (2 to_power(n)+1) <= b by NAT_1:13;
        not (2 to_power(n)+1) <= k by A29,NAT_1:13;
        then not 0 < b by A31,A40,A41,NAT_D:7;
        then b1 - b2 + b2 = 0 + b2 by A39;
        hence b2 = b1;
      end;
    end;
    hence thesis by A21,A23,A26,A24,Th18;
  end;
end;

theorem
  MUL_MOD(i,j,n) = MUL_MOD(j,i,n);

theorem Th22:
  i is_expressible_by n implies MUL_MOD(1,i,n) = i
proof
A1: ChangeVal_1(1,n) = 1 by Def7;
  assume i is_expressible_by n;
  then
A2: i < 2 to_power n by Def3;
  per cases;
  suppose
A3: i = 0;
    then ChangeVal_1(i,n) = 2 to_power(n) by Def7;
    then (ChangeVal_1(i,n)) mod ((2 to_power n)+1) = 2 to_power(n) by NAT_D:24
,XREAL_1:29;
    hence thesis by A1,A3,Def8;
  end;
  suppose
A4: i <> 0;
    2 to_power n < (2 to_power n)+1 by XREAL_1:29;
    then
A5: i < (2 to_power n)+1 by A2,XXREAL_0:2;
    (ChangeVal_1(i,n)) mod ((2 to_power n)+1) = i mod ((2 to_power n)+1)
    by A4,Def7;
    then (ChangeVal_1(i,n)) mod ((2 to_power n)+1) = i by A5,NAT_D:24;
    hence thesis by A2,A1,Def8;
  end;
end;

theorem Th23:
  (2 to_power(n)+1) is prime & i is_expressible_by n & j
is_expressible_by n & k is_expressible_by n implies MUL_MOD(MUL_MOD(i,j,n),k,n)
  = MUL_MOD(i,MUL_MOD(j,k,n),n)
proof
  assume that
A1: (2 to_power(n)+1) is prime and
A2: i is_expressible_by n and
A3: j is_expressible_by n and
A4: k is_expressible_by n;
  set J = ChangeVal_1(j,n);
A5: J > 0 by A3,Th17;
  set I = ChangeVal_1(i,n);
  I <= 2 to_power(n) by A2,Th17;
  then
A6: I < 2 to_power(n)+1 by NAT_1:13;
  J <= 2 to_power(n) by A3,Th17;
  then
A7: J < 2 to_power(n)+1 by NAT_1:13;
  set K = ChangeVal_1(k,n);
A8: K > 0 by A4,Th17;
  K <= 2 to_power(n) by A4,Th17;
  then
A9: K < 2 to_power(n)+1 by NAT_1:13;
A10: I > 0 by A2,Th17;
  now
    set CV = (I*J) mod (2 to_power(n)+1);
    (I*J) mod (2 to_power(n)+1) < (2 to_power(n)+1) by NAT_D:1;
    then
A11: (I*J) mod (2 to_power(n)+1) <= 2 to_power(n) by NAT_1:13;
A12: CV <> 0 by A1,A6,A10,A7,A5,Th5;
    now
      per cases by A11,XXREAL_0:1;
      suppose
A13:    CV = 2 to_power(n);
        then
A14:    MUL_MOD(MUL_MOD(i,j,n),k,n) = ChangeVal_2((ChangeVal_1(0,n )*K)
        mod (2 to_power(n)+1),n) by Def8
          .= ChangeVal_2((CV*K) mod (2 to_power(n)+1),n) by A13,Def7
          .= ChangeVal_2(((I*J)*K) mod (2 to_power(n)+1),n) by EULER_2:8;
        set CV2 = (J*K) mod (2 to_power(n)+1);
        CV2 < (2 to_power(n)+1) by NAT_D:1;
        then
A15:    CV2 <= 2 to_power(n) by NAT_1:13;
A16:    CV2 <> 0 by A1,A7,A5,A9,A8,Th5;
        now
          per cases by A15,XXREAL_0:1;
          suppose
A17:        CV2 = 2 to_power(n);
            then
            MUL_MOD(i,MUL_MOD(j,k,n),n) = ChangeVal_2((I*ChangeVal_1(0,n)
            ) mod (2 to_power(n)+1),n) by Def8
              .= ChangeVal_2((I*CV2) mod (2 to_power(n)+1),n) by A17,Def7
              .= ChangeVal_2((I*(J*K)) mod (2 to_power(n)+1),n) by EULER_2:8
              .= ChangeVal_2((I*J*K) mod (2 to_power(n)+1),n);
            hence thesis by A14;
          end;
          suppose
            CV2 < 2 to_power(n);
            then MUL_MOD(j,k,n) = CV2 by Def8;
            then MUL_MOD(i,MUL_MOD(j,k,n),n) = ChangeVal_2((I*CV2) mod (2
            to_power(n)+1),n) by A16,Def7
              .= ChangeVal_2((I*(J*K)) mod (2 to_power(n)+1),n) by EULER_2:8
              .= ChangeVal_2((I*J*K) mod (2 to_power(n)+1),n);
            hence thesis by A14;
          end;
        end;
        hence thesis;
      end;
      suppose
        CV < 2 to_power(n);
        then
A18:    MUL_MOD(MUL_MOD(i,j,n),k,n) = ChangeVal_2((ChangeVal_1(CV, n)*K)
        mod (2 to_power(n)+1),n) by Def8
          .= ChangeVal_2((CV*K) mod (2 to_power(n)+1),n) by A12,Def7
          .= ChangeVal_2(((I*J)*K) mod (2 to_power(n)+1),n) by EULER_2:8;
        set CV2 = (J*K) mod (2 to_power(n)+1);
        CV2 < (2 to_power(n)+1) by NAT_D:1;
        then
A19:    CV2 <= 2 to_power(n) by NAT_1:13;
A20:    CV2 <> 0 by A1,A7,A5,A9,A8,Th5;
        now
          per cases by A19,XXREAL_0:1;
          suppose
A21:        CV2 = 2 to_power(n);
            then
            MUL_MOD(i,MUL_MOD(j,k,n),n) = ChangeVal_2((I*ChangeVal_1(0,n)
            ) mod (2 to_power(n)+1),n) by Def8
              .= ChangeVal_2((I*CV2) mod (2 to_power(n)+1),n) by A21,Def7
              .= ChangeVal_2((I*(J*K)) mod (2 to_power(n)+1),n) by EULER_2:8
              .= ChangeVal_2((I*J*K) mod (2 to_power(n)+1),n);
            hence thesis by A18;
          end;
          suppose
            CV2 < 2 to_power(n);
            then MUL_MOD(j,k,n) = CV2 by Def8;
            then MUL_MOD(i,MUL_MOD(j,k,n),n) = ChangeVal_2((I*CV2) mod (2
            to_power(n)+1),n) by A20,Def7
              .= ChangeVal_2((I*(J*K)) mod (2 to_power(n)+1),n) by EULER_2:8
              .= ChangeVal_2((I*J*K) mod (2 to_power(n)+1),n);
            hence thesis by A18;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  hence thesis;
end;

theorem Th24:
  MUL_MOD(i,j,n) is_expressible_by n
proof
  set CV = (ChangeVal_1(i,n)*ChangeVal_1(j,n)) mod (2 to_power(n)+1);
  (ChangeVal_1(i,n)*ChangeVal_1(j,n)) mod (2 to_power(n)+1) < (2 to_power(
  n)+1) by NAT_D:1;
  then
A1: (ChangeVal_1(i,n)*ChangeVal_1(j,n)) mod (2 to_power(n)+1) <= 2 to_power(
  n) by NAT_1:13;
A2: 0 < 2 to_power(n) by POWER:34;
  now
    per cases by A1,XXREAL_0:1;
    suppose
      CV = 2 to_power(n);
      then ChangeVal_2(CV,n) = 0 by Def8;
      hence thesis by A2,Def3;
    end;
    suppose
A3:   CV < 2 to_power(n);
      then ChangeVal_2(CV,n) = CV by Def8;
      hence thesis by A3,Def3;
    end;
  end;
  hence thesis;
end;

theorem
  ChangeVal_2(i,n) = 1 implies i = 1
proof
  assume
A1: ChangeVal_2(i,n) = 1;
  assume
A2: i <> 1;
  now
    per cases;
    suppose
      i = 2 to_power(n);
      hence contradiction by A1,Def8;
    end;
    suppose
      i <> 2 to_power(n);
      hence contradiction by A1,A2,Def8;
    end;
  end;
  hence thesis;
end;

begin :: Operations of IDEA Cryptograms
:: We define three IDEA's operations IDEAoperationA, IDEAoperationB
:: and IDEAoperationC using the basic operators. IDEA Cryptogram
:: encrypts 64-bit plain text to 64-bit ciphertext. These texts
:: are divided into 4 16-bits text blocks. Here, we use m as the
:: text block sequence. And, IDEA's operations use key sequence
:: explains k in this section. n is bit-length of text blocks.
:: Definiton of IDEA Operation A

definition
  let n;
  let m,k be FinSequence of NAT;
  func IDEAoperationA(m, k, n) -> FinSequence of NAT means
  :Def11:
  len(it) =
  len(m) & for i being Element of NAT st i in dom m holds (i=1 implies it.i =
  MUL_MOD(m.1, k.1, n)) & (i=2 implies it.i = ADD_MOD(m.2, k.2, n)) & (i=3
implies it.i = ADD_MOD(m.3, k.3, n)) & (i=4 implies it.i = MUL_MOD(m.4, k.4, n)
  ) & (i<>1 & i <> 2 & i<>3 & i<>4 implies it.i = m.i);
  existence
  proof
    defpred P[set,set] means ($1=1 implies $2 = MUL_MOD(m.1, k.1, n)) & ($1=2
implies $2 = ADD_MOD(m.2, k.2, n)) & ($1=3 implies $2 = ADD_MOD(m.3, k.3, n)) &
    ($1=4 implies $2 = MUL_MOD(m.4, k.4, n)) & ($1<>1 & $1 <> 2 & $1<>3 & $1<>4
    implies $2 = m.$1);
A1: for j be Nat st j in Seg len m ex x being Element of NAT st P[j,x]
    proof
      let j be Nat;
      assume j in Seg len m;
      then reconsider j as Element of NAT;
      per cases;
      suppose
A2:     j = 1;
        take MUL_MOD(m.1, k.1, n);
        thus thesis by A2;
      end;
      suppose
A3:     j = 2;
        take ADD_MOD(m.2, k.2, n);
        thus thesis by A3;
      end;
      suppose
A4:     j = 3;
        take ADD_MOD(m.3, k.3, n);
        thus thesis by A4;
      end;
      suppose
A5:     j = 4;
        take MUL_MOD(m.4, k.4, n);
        thus thesis by A5;
      end;
      suppose
A6:     j<>1 & j<>2 & j<>3 & j<>4;
        take m.j;
        thus thesis by A6;
      end;
    end;
    consider z being FinSequence of NAT such that
A7: dom z = Seg len m & for i be Nat st i in Seg len m holds P[i,z.i]
    from FINSEQ_1:sch 5(A1);
    take z;
    dom m = Seg len m by FINSEQ_1:def 3;
    hence thesis by A7,FINSEQ_1:def 3;
  end;
  uniqueness
  proof
    let z1,z2 be FinSequence of NAT such that
A8: len(z1) = len(m) and
A9: for i being Element of NAT st i in dom m holds (i=1 implies z1.i
    = MUL_MOD(m.1, k.1, n)) & (i=2 implies z1.i = ADD_MOD(m.2, k.2, n)) & (i=3
implies z1.i = ADD_MOD(m.3, k.3, n)) & (i=4 implies z1.i = MUL_MOD(m.4, k.4, n)
    ) & (i<>1 & i <> 2 & i<>3 & i<>4 implies z1.i = m.i) and
A10: len(z2) = len(m) and
A11: for i st i in dom m holds (i=1 implies z2.i = MUL_MOD(m.1, k.1, n
)) & (i=2 implies z2.i = ADD_MOD(m.2, k.2, n)) & (i=3 implies z2.i = ADD_MOD(m.
3, k.3, n)) & (i=4 implies z2.i = MUL_MOD(m.4, k.4, n)) & (i<>1 & i <> 2 & i<>3
    & i<>4 implies z2.i = m.i);
A12: dom m = Seg len z2 by A10,FINSEQ_1:def 3
      .= dom z2 by FINSEQ_1:def 3;
A13: now
      let j be Nat;
      assume
A14:  j in dom m;
      now
        per cases;
        suppose
A15:      j = 1;
          hence z1.j = MUL_MOD(m.1, k.1, n) by A9,A14
            .= z2.j by A11,A14,A15;
        end;
        suppose
A16:      j = 2;
          hence z1.j = ADD_MOD(m.2, k.2, n) by A9,A14
            .= z2.j by A11,A14,A16;
        end;
        suppose
A17:      j = 3;
          hence z1.j = ADD_MOD(m.3, k.3, n) by A9,A14
            .= z2.j by A11,A14,A17;
        end;
        suppose
A18:      j = 4;
          hence z1.j = MUL_MOD(m.4, k.4, n) by A9,A14
            .= z2.j by A11,A14,A18;
        end;
        suppose
A19:      j<>1 & j<>2 & j<>3 & j<>4;
          hence z1.j = m.j by A9,A14
            .= z2.j by A11,A14,A19;
        end;
      end;
      hence z1.j = z2.j;
    end;
    dom m = Seg len z1 by A8,FINSEQ_1:def 3
      .= dom z1 by FINSEQ_1:def 3;
    hence thesis by A12,A13,FINSEQ_1:13;
  end;
end;

:: Definiton of IDEA Operation B

reserve m,k,k1,k2 for FinSequence of NAT;

definition
  let n be non empty Element of NAT;
  let m,k be FinSequence of NAT;
  func IDEAoperationB(m, k, n) -> FinSequence of NAT means
  :Def12:
  len(it) =
  len(m) & for i being Element of NAT st i in dom m holds (i=1 implies it.i =
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence MUL_MOD(ADD_MOD(MUL_MOD(
  Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),k.5,n),Absval((n
  -BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k.6,n))))& (i=2 implies
  it.i = Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence ADD_MOD(MUL_MOD(
  Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),k.5,n),MUL_MOD(
ADD_MOD(MUL_MOD( Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)), k
.5,n),Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k.6,n),n))
  ))& (i=3 implies it.i = Absval((n-BinarySequence m.3) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m
.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k.6,
  n))))& (i=4 implies it.i = Absval((n-BinarySequence m.4) 'xor' (n
  -BinarySequence ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n
-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD( Absval((n-BinarySequence
m.1) 'xor' (n-BinarySequence m.3)), k.5,n),Absval((n-BinarySequence m.2) 'xor'
  (n-BinarySequence m.4)),n),k.6,n),n))))& (i<>1 & i <> 2 & i<>3 & i<>4 implies
  it.i = m.i);
  existence
  proof
    defpred P[set,set] means ($1=1 implies $2 = Absval((n-BinarySequence m.1)
'xor' (n-BinarySequence MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1)
    'xor' (n-BinarySequence m.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor' (n
-BinarySequence m.4)),n),k.6,n))))& ($1=2 implies $2 = Absval((n-BinarySequence
    m.2) 'xor' (n-BinarySequence ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1)
    'xor' (n-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD( Absval((n
    -BinarySequence m.1) 'xor' (n-BinarySequence m.3)), k.5,n),Absval((n
    -BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k.6,n),n))))& ($1=3
    implies $2 = Absval((n-BinarySequence m.3) 'xor' (n-BinarySequence MUL_MOD(
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),k.5
,n),Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k.6,n))))& (
$1=4 implies $2 = Absval((n-BinarySequence m.4) 'xor' (n-BinarySequence ADD_MOD
(MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),k.5,n),
MUL_MOD(ADD_MOD(MUL_MOD( Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence
m.3)), k.5,n),Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k.
    6,n),n))))& ($1<>1 & $1 <> 2 & $1<>3 & $1<>4 implies $2 = m.$1);
A1: for j be Nat st j in Seg len m ex x being Element of NAT st P[j,x]
    proof
      let j be Nat;
      assume j in Seg len m;
      then reconsider j as Element of NAT;
      per cases;
      suppose
A2:     j = 1;
        take Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence MUL_MOD(
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),k.5
,n),Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k.6,n)));
        thus thesis by A2;
      end;
      suppose
A3:     j = 2;
        take Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence ADD_MOD(
MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),k.5,n),
MUL_MOD(ADD_MOD(MUL_MOD( Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence
m.3)), k.5,n),Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k.
        6,n),n)));
        thus thesis by A3;
      end;
      suppose
A4:     j = 3;
        take Absval((n-BinarySequence m.3) 'xor' (n-BinarySequence MUL_MOD(
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),k.5
,n),Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k.6,n)));
        thus thesis by A4;
      end;
      suppose
A5:     j = 4;
        take Absval((n-BinarySequence m.4) 'xor' (n-BinarySequence ADD_MOD(
MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),k.5,n),
MUL_MOD(ADD_MOD(MUL_MOD( Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence
m.3)), k.5,n),Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k.
        6,n),n)));
        thus thesis by A5;
      end;
      suppose
A6:     j<>1 & j<>2 & j<>3 & j<>4;
        take m.j;
        thus thesis by A6;
      end;
    end;
    consider z being FinSequence of NAT such that
A7: dom z = Seg len m & for i be Nat st i in Seg len m holds P[i,z.i]
    from FINSEQ_1:sch 5(A1);
    take z;
    Seg len m = dom m by FINSEQ_1:def 3;
    hence thesis by A7,FINSEQ_1:def 3;
  end;
  uniqueness
  proof
    let z1,z2 be FinSequence of NAT such that
A8: len(z1) = len(m) and
A9: for i st i in dom m holds (i=1 implies z1.i = Absval((n
-BinarySequence m.1) 'xor' (n-BinarySequence MUL_MOD(ADD_MOD(MUL_MOD(Absval((n
    -BinarySequence m.1) 'xor' (n-BinarySequence m.3)),k.5,n),Absval((n
-BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k.6,n))))& (i=2 implies
z1.i = Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence ADD_MOD(MUL_MOD(
    Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),k.5,n),MUL_MOD(
ADD_MOD(MUL_MOD( Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)), k
.5,n),Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k.6,n),n))
))& (i=3 implies z1.i = Absval((n-BinarySequence m.3) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m
.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k.6,
    n))))& (i=4 implies z1.i = Absval((n-BinarySequence m.4) 'xor' (n
    -BinarySequence ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n
-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD( Absval((n-BinarySequence
m.1) 'xor' (n-BinarySequence m.3)), k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n),n))))& (i<>1 & i <> 2 & i<>3 & i<>4 implies
    z1.i = m.i) and
A10: len(z2) = len(m) and
A11: for i st i in dom m holds (i=1 implies z2.i = Absval((n
-BinarySequence m.1) 'xor' (n-BinarySequence MUL_MOD(ADD_MOD(MUL_MOD(Absval((n
    -BinarySequence m.1) 'xor' (n-BinarySequence m.3)),k.5,n),Absval((n
-BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k.6,n))))& (i=2 implies
z2.i = Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence ADD_MOD(MUL_MOD(
    Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),k.5,n),MUL_MOD(
ADD_MOD(MUL_MOD( Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)), k
.5,n),Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k.6,n),n))
))& (i=3 implies z2.i = Absval((n-BinarySequence m.3) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m
.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k.6,
    n))))& (i=4 implies z2.i = Absval((n-BinarySequence m.4) 'xor' (n
    -BinarySequence ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n
-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD( Absval((n-BinarySequence
m.1) 'xor' (n-BinarySequence m.3)), k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n),n))))& (i<>1 & i <> 2 & i<>3 & i<>4 implies
    z2.i = m.i);
A12: dom m = Seg len(z2) by A10,FINSEQ_1:def 3
      .= dom z2 by FINSEQ_1:def 3;
A13: now
      let j be Nat;
      assume
A14:  j in dom m;
      now
        per cases;
        suppose
A15:      j = 1;
          hence z1.j = Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m
.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k.6,
          n))) by A9,A14
            .= z2.j by A11,A14,A15;
        end;
        suppose
A16:      j = 2;
          hence z1.j = Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),k.5
          ,n),MUL_MOD(ADD_MOD(MUL_MOD( Absval((n-BinarySequence m.1) 'xor' (n
          -BinarySequence m.3)), k.5,n),Absval((n-BinarySequence m.2) 'xor' (n
          -BinarySequence m.4)),n),k.6,n),n))) by A9,A14
            .= z2.j by A11,A14,A16;
        end;
        suppose
A17:      j = 3;
          hence z1.j = Absval((n-BinarySequence m.3) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m
.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k.6,
          n))) by A9,A14
            .= z2.j by A11,A14,A17;
        end;
        suppose
A18:      j = 4;
          hence z1.j = Absval((n-BinarySequence m.4) 'xor' (n-BinarySequence
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),k.5
          ,n),MUL_MOD(ADD_MOD(MUL_MOD( Absval((n-BinarySequence m.1) 'xor' (n
          -BinarySequence m.3)), k.5,n),Absval((n-BinarySequence m.2) 'xor' (n
          -BinarySequence m.4)),n),k.6,n),n))) by A9,A14
            .= z2.j by A11,A14,A18;
        end;
        suppose
A19:      j<>1 & j<>2 & j<>3 & j<>4;
          hence z1.j = m.j by A9,A14
            .= z2.j by A11,A14,A19;
        end;
      end;
      hence z1.j = z2.j;
    end;
    dom m = Seg len(z1) by A8,FINSEQ_1:def 3
      .= dom z1 by FINSEQ_1:def 3;
    hence thesis by A12,A13,FINSEQ_1:13;
  end;
end;

:: Definiton of IDEA Operation C

definition
  let m be FinSequence of NAT;
  func IDEAoperationC(m) -> FinSequence of NAT means
  :Def13:
  len(it) = len(m)
& for i being Element of NAT st i in dom m holds it.i = IFEQ(i,2,m.3,IFEQ(i,3,m
  .2,m.i));
  existence
  proof
    defpred P[set,set] means ($1=2 implies $2 = m.3) & ($1=3 implies $2 = m.2)
    & ($1<>2 & $1<>3 implies $2 = m.$1);
A1: for k be Nat st k in Seg len m ex x being Element of NAT st P[k,x]
    proof
      let k be Nat;
      assume k in Seg len m;
      then reconsider k as Element of NAT;
      per cases;
      suppose
A2:     k = 2;
        take m.3;
        thus thesis by A2;
      end;
      suppose
A3:     k = 3;
        take m.2;
        thus thesis by A3;
      end;
      suppose
A4:     k<>2 & k<>3;
        take m.k;
        thus thesis by A4;
      end;
    end;
    consider z being FinSequence of NAT such that
A5: dom z = Seg len m and
A6: for i be Nat st i in Seg len m holds P[i,z.i] from FINSEQ_1:sch 5(
    A1);
A7: for i st i in Seg len m holds IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = z.i
    proof
      let i be Element of NAT;
      assume
A8:   i in Seg len m;
A9:   i = 3 implies IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = m.2
      proof
        assume
A10:    i = 3;
        then IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = IFEQ(i,3,m.2,m.i) by
FUNCOP_1:def 8
          .= m.2 by A10,FUNCOP_1:def 8;
        hence thesis;
      end;
A11:  i = 2 implies IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = m.3 by FUNCOP_1:def 8;
      i<>2 & i<>3 implies IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = m.i
      proof
        assume that
A12:    i <> 2 and
A13:    i <> 3;
        IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = IFEQ(i,3,m.2,m.i) by A12,
FUNCOP_1:def 8
          .= m.i by A13,FUNCOP_1:def 8;
        hence thesis;
      end;
      then i<>2 & i<>3 implies IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = z.i by A6,A8;
      hence thesis by A6,A8,A11,A9;
    end;
    take z;
    Seg len m = dom m by FINSEQ_1:def 3;
    hence thesis by A5,A7,FINSEQ_1:def 3;
  end;
  uniqueness
  proof
    let z1,z2 be FinSequence of NAT such that
A14: len(z1) = len(m) and
A15: for i st i in dom m holds z1.i = IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) and
A16: len(z2) = len(m) and
A17: for i st i in dom m holds z2.i = IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i));
A18: dom m = Seg len(z2) by A16,FINSEQ_1:def 3
      .= dom z2 by FINSEQ_1:def 3;
A19: now
      let j be Nat;
      assume
A20:  j in dom m;
      now
        per cases;
        suppose
          j = 2;
          then
A21:      IFEQ(j,2,m.3,IFEQ(j,3,m.2,m.j)) = m.3 by FUNCOP_1:def 8;
          then z2.j = m.3 by A17,A20;
          hence z1.j = z2.j by A15,A20,A21;
        end;
        suppose
A22:      j = 3;
A23:      j = 3 implies IFEQ(j,2,m.3,IFEQ(j,3,m.2,m.j)) = m.2
          proof
            assume
A24:        j = 3;
            then IFEQ(j,2,m.3,IFEQ(j,3,m.2,m.j)) = IFEQ(j,3,m.2,m.j) by
FUNCOP_1:def 8
              .= m.2 by A24,FUNCOP_1:def 8;
            hence thesis;
          end;
          then z2.j = m.2 by A17,A20,A22;
          hence z1.j = z2.j by A15,A20,A22,A23;
        end;
        suppose
A25:      j<>2 & j<>3;
A26:      j<>2 & j<>3 implies IFEQ(j,2,m.3,IFEQ(j,3,m.2,m.j)) = m.j
          proof
            assume that
A27:        j <> 2 and
A28:        j <> 3;
            IFEQ(j,2,m.3,IFEQ(j,3,m.2,m.j)) = IFEQ(j,3,m.2,m.j) by A27,
FUNCOP_1:def 8
              .= m.j by A28,FUNCOP_1:def 8;
            hence thesis;
          end;
          then z2.j = m.j by A17,A20,A25;
          hence z1.j = z2.j by A15,A20,A25,A26;
        end;
      end;
      hence z1.j = z2.j;
    end;
    dom m = Seg len(z1) by A14,FINSEQ_1:def 3
      .= dom z1 by FINSEQ_1:def 3;
    hence thesis by A18,A19,FINSEQ_1:13;
  end;
end;

theorem Th26:
  len m >= 4 implies IDEAoperationA(m,k,n).1 is_expressible_by n &
  IDEAoperationA(m,k,n).2 is_expressible_by n & IDEAoperationA(m,k,n).3
  is_expressible_by n & IDEAoperationA(m,k,n).4 is_expressible_by n
proof
  assume
A1: len m >= 4;
  then 1 <= len m by XXREAL_0:2;
  then 1 in Seg len m by FINSEQ_1:1;
  then 1 in dom m by FINSEQ_1:def 3;
  then
A2: IDEAoperationA(m,k,n).1 = MUL_MOD(m.1, k.1, n) by Def11;
  3 <= len m by A1,XXREAL_0:2;
  then 3 in Seg len m by FINSEQ_1:1;
  then 3 in dom m by FINSEQ_1:def 3;
  then
A3: IDEAoperationA(m,k,n).3 = ADD_MOD(m.3, k.3, n) by Def11;
  2 <= len m by A1,XXREAL_0:2;
  then 2 in Seg len m by FINSEQ_1:1;
  then 2 in dom m by FINSEQ_1:def 3;
  then
A4: IDEAoperationA(m,k,n).2 = ADD_MOD(m.2, k.2, n) by Def11;
  4 in Seg len m by A1,FINSEQ_1:1;
  then 4 in dom m by FINSEQ_1:def 3;
  then IDEAoperationA(m,k,n).4 = MUL_MOD(m.4, k.4, n) by Def11;
  hence thesis by A2,A4,A3,Th15,Th24;
end;

theorem Th27:
  for n being non empty Element of NAT holds len m >= 4 implies
  IDEAoperationB(m,k,n).1 is_expressible_by n & IDEAoperationB(m,k,n).2
  is_expressible_by n & IDEAoperationB(m,k,n).3 is_expressible_by n &
  IDEAoperationB(m,k,n).4 is_expressible_by n
proof
  let n be non empty Element of NAT;
  assume
A1: len m >= 4;
  then 1 <= len m by XXREAL_0:2;
  then 1 in Seg len m by FINSEQ_1:1;
  then 1 in dom m by FINSEQ_1:def 3;
  then IDEAoperationB(m,k,n).1 = Absval((n-BinarySequence m.1) 'xor' (n
-BinarySequence MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n
  -BinarySequence m.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor' (n
  -BinarySequence m.4)),n),k.6,n))) by Def12;
  then
A2: IDEAoperationB(m,k,n).1 < 2 to_power n by BINARI_3:1;
  3 <= len m by A1,XXREAL_0:2;
  then 3 in Seg len m by FINSEQ_1:1;
  then 3 in dom m by FINSEQ_1:def 3;
  then IDEAoperationB(m,k,n).3 = Absval((n-BinarySequence m.3) 'xor' (n
-BinarySequence MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n
  -BinarySequence m.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor' (n
  -BinarySequence m.4)),n),k.6,n))) by Def12;
  then
A3: IDEAoperationB(m,k,n).3 < 2 to_power n by BINARI_3:1;
  2 <= len m by A1,XXREAL_0:2;
  then 2 in Seg len m by FINSEQ_1:1;
  then 2 in dom m by FINSEQ_1:def 3;
  then IDEAoperationB(m,k,n).2 = Absval((n-BinarySequence m.2) 'xor' (n
  -BinarySequence ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n
-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD( Absval((n-BinarySequence
m.1) 'xor' (n-BinarySequence m.3)), k.5,n),Absval((n-BinarySequence m.2) 'xor'
  (n-BinarySequence m.4)),n),k.6,n),n))) by Def12;
  then
A4: IDEAoperationB(m,k,n).2 < 2 to_power n by BINARI_3:1;
  4 in Seg len m by A1,FINSEQ_1:1;
  then 4 in dom m by FINSEQ_1:def 3;
  then IDEAoperationB(m,k,n).4 = Absval((n-BinarySequence m.4) 'xor' (n
  -BinarySequence ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor' (n
-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD( Absval((n-BinarySequence
m.1) 'xor' (n-BinarySequence m.3)), k.5,n),Absval((n-BinarySequence m.2) 'xor'
  (n-BinarySequence m.4)),n),k.6,n),n))) by Def12;
  then IDEAoperationB(m,k,n).4 < 2 to_power n by BINARI_3:1;
  hence thesis by A2,A4,A3,Def3;
end;

Lm3: for i st i = 2 & i in dom m holds IDEAoperationC(m).i = m.3
proof
  let i be Element of NAT;
  assume that
A1: i = 2 and
A2: i in dom m;
  IDEAoperationC(m).i = IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) by A2,Def13
    .= m.3 by A1,FUNCOP_1:def 8;
  hence thesis;
end;

Lm4: for i st i = 3 & i in dom m holds IDEAoperationC(m).i = m.2
proof
  let i be Element of NAT;
  assume that
A1: i = 3 and
A2: i in dom m;
  IDEAoperationC(m).i = IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) by A2,Def13
    .= IFEQ(i,3,m.2,m.i) by A1,FUNCOP_1:def 8
    .= m.2 by A1,FUNCOP_1:def 8;
  hence thesis;
end;

Lm5: for i st i <> 2 & i <> 3 & i in dom m holds IDEAoperationC(m).i = m.i
proof
  let i be Element of NAT;
  assume that
A1: i <> 2 and
A2: i <> 3 and
A3: i in dom m;
  IDEAoperationC(m).i = IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) by A3,Def13
    .= IFEQ(i,3,m.2,m.i) by A1,FUNCOP_1:def 8
    .= m.i by A2,FUNCOP_1:def 8;
  hence thesis;
end;

theorem
  len m >= 4 & m.1 is_expressible_by n & m.2 is_expressible_by n & m.3
  is_expressible_by n & m.4 is_expressible_by n implies IDEAoperationC(m).1
is_expressible_by n & IDEAoperationC(m).2 is_expressible_by n & IDEAoperationC(
  m).3 is_expressible_by n & IDEAoperationC(m).4 is_expressible_by n
proof
  assume that
A1: len m >= 4 and
A2: m.1 is_expressible_by n & m.2 is_expressible_by n & m.3
  is_expressible_by n & m.4 is_expressible_by n;
  1 <= len m by A1,XXREAL_0:2;
  then 1 in Seg len m by FINSEQ_1:1;
  then
A3: 1 in dom m by FINSEQ_1:def 3;
  3 <= len m by A1,XXREAL_0:2;
  then 3 in Seg len m by FINSEQ_1:1;
  then
A4: 3 in dom m by FINSEQ_1:def 3;
  2 <= len m by A1,XXREAL_0:2;
  then 2 in Seg len m by FINSEQ_1:1;
  then
A5: 2 in dom m by FINSEQ_1:def 3;
  4 in Seg len m by A1,FINSEQ_1:1;
  then 4 in dom m by FINSEQ_1:def 3;
  hence thesis by A2,A3,A5,A4,Lm3,Lm4,Lm5;
end;

theorem Th29:
  for n being non empty Element of NAT,m,k1,k2 holds 2 to_power(n)
+1 is prime & len m >= 4 & m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n & k1.1 is_expressible_by n &
k1.2 is_expressible_by n & k1.3 is_expressible_by n & k1.4 is_expressible_by n
  & k2.1=INV_MOD(k1.1,n) & k2.2=NEG_MOD(k1.2,n) & k2.3=NEG_MOD(k1.3,n) & k2.4=
  INV_MOD(k1.4,n) implies IDEAoperationA( IDEAoperationA(m,k1,n), k2, n) = m
proof
  let n be non empty Element of NAT;
  let m,k1,k2 be FinSequence of NAT;
  assume that
A1: 2 to_power(n)+1 is prime and
A2: len m >= 4 and
A3: m.1 is_expressible_by n and
A4: m.2 is_expressible_by n and
A5: m.3 is_expressible_by n and
A6: m.4 is_expressible_by n and
A7: k1.1 is_expressible_by n and
A8: k1.2 is_expressible_by n and
A9: k1.3 is_expressible_by n and
A10: k1.4 is_expressible_by n and
A11: k2.1=INV_MOD(k1.1,n) and
A12: k2.2=NEG_MOD(k1.2,n) and
A13: k2.3=NEG_MOD(k1.3,n) and
A14: k2.4=INV_MOD(k1.4,n);
A15: k2.4 is_expressible_by n by A1,A10,A14,Def10;
  2 <= len m by A2,XXREAL_0:2;
  then 2 in Seg len m by FINSEQ_1:1;
  then
A16: 2 in dom m by FINSEQ_1:def 3;
  Seg len m = dom m by FINSEQ_1:def 3;
  then
A17: 4 in dom m by A2,FINSEQ_1:1;
  1 <= len m by A2,XXREAL_0:2;
  then 1 in Seg len m by FINSEQ_1:1;
  then
A18: 1 in dom m by FINSEQ_1:def 3;
  3 <= len m by A2,XXREAL_0:2;
  then 3 in Seg len m by FINSEQ_1:1;
  then
A19: 3 in dom m by FINSEQ_1:def 3;
  consider I1 being FinSequence of NAT such that
A20: I1 = IDEAoperationA(m,k1,n);
  consider I2 being FinSequence of NAT such that
A21: I2 = IDEAoperationA(I1,k2,n);
A22: k2.1 is_expressible_by n by A1,A7,A11,Def10;
A23: now
    let j be Nat;
    assume
A24: j in Seg len m;
    then j in Seg len I1 by A20,Def11;
    then
A25: j in dom I1 by FINSEQ_1:def 3;
A26: j in dom m by A24,FINSEQ_1:def 3;
    now
      per cases;
      suppose
A27:    j = 1;
        hence I2.j = MUL_MOD(I1.1, k2.1, n) by A21,A25,Def11
          .= MUL_MOD(MUL_MOD(m.1, k1.1, n),k2.1,n) by A20,A18,Def11
          .= MUL_MOD(m.1, MUL_MOD(k1.1,k2.1,n), n) by A1,A3,A7,A22,Th23
          .= MUL_MOD(1, m.1, n) by A1,A7,A11,Def10
          .= m.j by A3,A27,Th22;
      end;
      suppose
A28:    j = 2;
        hence I2.j = ADD_MOD(I1.2, k2.2, n) by A21,A25,Def11
          .= ADD_MOD(ADD_MOD(m.2, k1.2, n), k2.2, n) by A20,A16,Def11
          .= ADD_MOD(m.2, ADD_MOD(k1.2, k2.2, n), n) by Th14
          .= ADD_MOD(0, m.2, n) by A8,A12,Th11
          .= m.j by A4,A28,Th13;
      end;
      suppose
A29:    j = 3;
        hence I2.j = ADD_MOD(I1.3, k2.3, n) by A21,A25,Def11
          .= ADD_MOD(ADD_MOD(m.3, k1.3, n), k2.3, n) by A20,A19,Def11
          .= ADD_MOD(m.3, ADD_MOD(k1.3, k2.3, n), n) by Th14
          .= ADD_MOD(0, m.3, n) by A9,A13,Th11
          .= m.j by A5,A29,Th13;
      end;
      suppose
A30:    j = 4;
        hence I2.j = MUL_MOD(I1.4, k2.4, n) by A21,A25,Def11
          .= MUL_MOD(MUL_MOD(m.4, k1.4, n),k2.4,n) by A20,A17,Def11
          .= MUL_MOD(m.4, MUL_MOD(k1.4,k2.4,n), n) by A1,A6,A10,A15,Th23
          .= MUL_MOD(1, m.4, n) by A1,A10,A14,Def10
          .= m.j by A6,A30,Th22;
      end;
      suppose
A31:    j<>1 & j<>2 & j<>3 & j<>4;
        hence I2.j = I1.j by A21,A25,Def11
          .= m.j by A20,A26,A31,Def11;
      end;
    end;
    hence I2.j = m.j;
  end;
A32: Seg len m = dom m by FINSEQ_1:def 3;
  Seg len m = Seg len(I1) by A20,Def11
    .= Seg len(I2) by A21,Def11
    .= dom I2 by FINSEQ_1:def 3;
  hence thesis by A20,A21,A32,A23,FINSEQ_1:13;
end;

theorem Th30:
  for n being non empty Element of NAT,m,k1,k2 holds 2 to_power(n)
+1 is prime & len m >= 4 & m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n & k1.1 is_expressible_by n &
k1.2 is_expressible_by n & k1.3 is_expressible_by n & k1.4 is_expressible_by n
  & k2.1=INV_MOD(k1.1,n) & k2.2=NEG_MOD(k1.3,n) & k2.3=NEG_MOD(k1.2,n) & k2.4=
  INV_MOD(k1.4,n) implies IDEAoperationA(IDEAoperationC(IDEAoperationA(
  IDEAoperationC(m),k1,n)),k2,n) = m
proof
  let n be non empty Element of NAT;
  let m,k1,k2 be FinSequence of NAT;
  assume that
A1: 2 to_power(n)+1 is prime and
A2: len m >= 4 and
A3: m.1 is_expressible_by n and
A4: m.2 is_expressible_by n and
A5: m.3 is_expressible_by n and
A6: m.4 is_expressible_by n and
A7: k1.1 is_expressible_by n and
A8: k1.2 is_expressible_by n and
A9: k1.3 is_expressible_by n and
A10: k1.4 is_expressible_by n and
A11: k2.1=INV_MOD(k1.1,n) and
A12: k2.2=NEG_MOD(k1.3,n) and
A13: k2.3=NEG_MOD(k1.2,n) and
A14: k2.4=INV_MOD(k1.4,n);
A15: k2.1 is_expressible_by n by A1,A7,A11,Def10;
  1 <= len m by A2,XXREAL_0:2;
  then
A16: 1 in Seg len m by FINSEQ_1:1;
  then
A17: 1 in dom m by FINSEQ_1:def 3;
A18: 4 in Seg len m by A2,FINSEQ_1:1;
  then
A19: 4 in dom m by FINSEQ_1:def 3;
  3 <= len m by A2,XXREAL_0:2;
  then
A20: 3 in Seg len m by FINSEQ_1:1;
  then
A21: 3 in dom m by FINSEQ_1:def 3;
A22: k2.4 is_expressible_by n by A1,A10,A14,Def10;
  consider I1 being FinSequence of NAT such that
A23: I1 = IDEAoperationC(m);
  4 in Seg len(I1) by A23,A18,Def13;
  then
A24: 4 in dom(I1) by FINSEQ_1:def 3;
  1 in Seg len(I1) by A23,A16,Def13;
  then
A25: 1 in dom(I1) by FINSEQ_1:def 3;
  2 <= len m by A2,XXREAL_0:2;
  then
A26: 2 in Seg len m by FINSEQ_1:1;
  then
A27: 2 in dom m by FINSEQ_1:def 3;
  3 in Seg len(I1) by A23,A20,Def13;
  then
A28: 3 in dom(I1) by FINSEQ_1:def 3;
  2 in Seg len(I1) by A23,A26,Def13;
  then
A29: 2 in dom(I1) by FINSEQ_1:def 3;
  consider I2 being FinSequence of NAT such that
A30: I2 = IDEAoperationA(I1,k1,n);
A31: len(I2) = len(I1) by A30,Def11;
  then 2 in Seg len(I2) by A23,A26,Def13;
  then
A32: 2 in dom(I2) by FINSEQ_1:def 3;
  4 in Seg len(I2) by A23,A31,A18,Def13;
  then
A33: 4 in dom(I2) by FINSEQ_1:def 3;
  1 in Seg len(I2) by A23,A31,A16,Def13;
  then
A34: 1 in dom(I2) by FINSEQ_1:def 3;
  3 in Seg len(I2) by A23,A31,A20,Def13;
  then
A35: 3 in dom(I2) by FINSEQ_1:def 3;
  consider I3 being FinSequence of NAT such that
A36: I3 = IDEAoperationC(I2);
A37: len(I3) = len(I2) by A36,Def13;
  then 2 in Seg len(I3) by A23,A31,A26,Def13;
  then
A38: 2 in dom(I3) by FINSEQ_1:def 3;
  4 in Seg len(I3) by A23,A31,A37,A18,Def13;
  then
A39: 4 in dom(I3) by FINSEQ_1:def 3;
  3 in Seg len(I3) by A23,A31,A37,A20,Def13;
  then
A40: 3 in dom(I3) by FINSEQ_1:def 3;
  consider I4 being FinSequence of NAT such that
A41: I4 = IDEAoperationA(I3,k2,n);
  1 in Seg len(I3) by A23,A31,A37,A16,Def13;
  then
A42: 1 in dom(I3) by FINSEQ_1:def 3;
A43: now
    let j be Nat;
    assume
A44: j in Seg len m;
    then
A45: j in dom m by FINSEQ_1:def 3;
A46: j in Seg len I1 by A23,A44,Def13;
    then
A47: j in Seg len I2 by A30,Def11;
    then
A48: j in dom I2 by FINSEQ_1:def 3;
    j in Seg len I3 by A36,A47,Def13;
    then
A49: j in dom I3 by FINSEQ_1:def 3;
A50: j in dom I1 by A46,FINSEQ_1:def 3;
    now
      per cases;
      suppose
A51:    j = 1;
        hence I4.j = MUL_MOD(I3.1, k2.1, n) by A41,A42,Def11
          .= MUL_MOD(I2.1, k2.1, n) by A36,A34,Lm5
          .= MUL_MOD(MUL_MOD(I1.1, k1.1, n), k2.1, n) by A30,A25,Def11
          .= MUL_MOD(MUL_MOD(m.1, k1.1, n), k2.1, n) by A23,A17,Lm5
          .= MUL_MOD(m.1, MUL_MOD(k1.1, k2.1, n), n) by A1,A3,A7,A15,Th23
          .= MUL_MOD(1, m.1, n) by A1,A7,A11,Def10
          .= m.j by A3,A51,Th22;
      end;
      suppose
A52:    j = 2;
        hence I4.j = ADD_MOD(I3.2, k2.2, n) by A41,A38,Def11
          .= ADD_MOD(I2.3, k2.2, n) by A36,A32,Lm3
          .= ADD_MOD(ADD_MOD(I1.3, k1.3, n), k2.2, n) by A30,A28,Def11
          .= ADD_MOD(ADD_MOD(m.2, k1.3, n), k2.2, n) by A23,A21,Lm4
          .= ADD_MOD(m.2, ADD_MOD(k1.3, k2.2, n), n) by Th14
          .= ADD_MOD(0, m.2, n) by A9,A12,Th11
          .= m.j by A4,A52,Th13;
      end;
      suppose
A53:    j = 3;
        hence I4.j = ADD_MOD(I3.3, k2.3, n) by A41,A40,Def11
          .= ADD_MOD(I2.2, k2.3, n) by A36,A35,Lm4
          .= ADD_MOD(ADD_MOD(I1.2, k1.2, n), k2.3, n) by A30,A29,Def11
          .= ADD_MOD(ADD_MOD(m.3, k1.2, n), k2.3, n) by A23,A27,Lm3
          .= ADD_MOD(m.3, ADD_MOD(k1.2, k2.3, n), n) by Th14
          .= ADD_MOD(0, m.3, n) by A8,A13,Th11
          .= m.j by A5,A53,Th13;
      end;
      suppose
A54:    j = 4;
        hence I4.j = MUL_MOD(I3.4, k2.4, n) by A41,A39,Def11
          .= MUL_MOD(I2.4, k2.4, n) by A36,A33,Lm5
          .= MUL_MOD(MUL_MOD(I1.4, k1.4, n), k2.4, n) by A30,A24,Def11
          .= MUL_MOD(MUL_MOD(m.4, k1.4, n), k2.4, n) by A23,A19,Lm5
          .= MUL_MOD(m.4, MUL_MOD(k1.4, k2.4, n), n) by A1,A6,A10,A22,Th23
          .= MUL_MOD(1, m.4, n) by A1,A10,A14,Def10
          .= m.j by A6,A54,Th22;
      end;
      suppose
A55:    j<>1 & j<>2 & j<>3 & j<>4;
        hence I4.j = I3.j by A41,A49,Def11
          .= I2.j by A36,A48,A55,Lm5
          .= I1.j by A30,A50,A55,Def11
          .= m.j by A23,A45,A55,Lm5;
      end;
    end;
    hence I4.j = m.j;
  end;
A56: Seg len m = dom m by FINSEQ_1:def 3;
  Seg len m = Seg len(I1) by A23,Def13
    .= Seg len(I2) by A30,Def11
    .= Seg len(I3) by A36,Def13
    .= Seg len(I4) by A41,Def11
    .= dom I4 by FINSEQ_1:def 3;
  hence thesis by A23,A30,A36,A41,A56,A43,FINSEQ_1:13;
end;

theorem Th31:
  for n being non empty Element of NAT,m,k1,k2 holds len m >= 4 &
m.1 is_expressible_by n & m.2 is_expressible_by n & m.3 is_expressible_by n & m
  .4 is_expressible_by n & k2.5=k1.5 & k2.6=k1.6 implies IDEAoperationB(
  IDEAoperationB(m,k1,n), k2, n) = m
proof
  let n be non empty Element of NAT;
  let m,k1,k2 be FinSequence of NAT;
  assume that
A1: len m >= 4 and
A2: m.1 is_expressible_by n and
A3: m.2 is_expressible_by n and
A4: m.3 is_expressible_by n and
A5: m.4 is_expressible_by n and
A6: k2.5= k1.5 and
A7: k2.6= k1.6;
  consider t10 being Element of NAT such that
A8: t10 = MUL_MOD( Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence
  m.3)),k1.5,n);
  consider t11 being Element of NAT such that
A9: t11 = MUL_MOD(ADD_MOD(t10, Absval((n-BinarySequence m.2) 'xor' (n
  -BinarySequence m.4)),n),k1.6,n);
  consider I1 being FinSequence of NAT such that
A10: I1 = IDEAoperationB(m,k1,n);
  1 <= len m by A1,XXREAL_0:2;
  then 1 in Seg len m by FINSEQ_1:1;
  then 1 in dom m by FINSEQ_1:def 3;
  then
A11: I1.1 = Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence t11)) by A8
,A9,A10,Def12;
  consider t20 being Element of NAT such that
A12: t20 = MUL_MOD( Absval((n-BinarySequence I1.1) 'xor' (n
  -BinarySequence I1.3)),k2.5,n);
  3 <= len m by A1,XXREAL_0:2;
  then 3 in Seg len m by FINSEQ_1:1;
  then 3 in dom m by FINSEQ_1:def 3;
  then
A13: I1.3 = Absval((n-BinarySequence m.3) 'xor' (n-BinarySequence t11)) by A8
,A9,A10,Def12;
  then
A14: t20 = MUL_MOD( Absval(((n-BinarySequence m.1) 'xor' (n-BinarySequence
  t11)) 'xor' (n-BinarySequence Absval((n-BinarySequence m.3) 'xor' (n
  -BinarySequence t11)))),k2.5,n) by A12,A11,BINARI_3:36
    .= MUL_MOD( Absval(((n-BinarySequence m.1) 'xor' (n-BinarySequence t11))
  'xor' ((n-BinarySequence m.3) 'xor' (n-BinarySequence t11))),k2.5,n) by
BINARI_3:36
    .= MUL_MOD( Absval((n-BinarySequence m.1) 'xor' ((n-BinarySequence t11)
  'xor' ((n-BinarySequence t11) 'xor' (n-BinarySequence m.3)))),k2.5,n) by Th9
    .= MUL_MOD( Absval((n-BinarySequence m.1) 'xor' (((n-BinarySequence t11)
  'xor' (n-BinarySequence t11)) 'xor' (n-BinarySequence m.3))),k2.5,n) by Th9
    .= MUL_MOD( Absval((n-BinarySequence m.1) 'xor' (ZERO(n) 'xor' (n
  -BinarySequence m.3))),k2.5,n) by Th6
    .= t10 by A6,A8,Th8;
  consider t21 being Element of NAT such that
A15: t21 = MUL_MOD(ADD_MOD(t20, Absval((n-BinarySequence I1.2) 'xor' (n
  -BinarySequence I1.4)),n),k2.6,n);
  consider t12 being Element of NAT such that
A16: t12 = ADD_MOD(t10, t11, n);
  2 <= len m by A1,XXREAL_0:2;
  then 2 in Seg len m by FINSEQ_1:1;
  then 2 in dom m by FINSEQ_1:def 3;
  then
A17: I1.2 = Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence t12)) by A8
,A9,A16,A10,Def12;
  consider I2 being FinSequence of NAT such that
A18: I2 = IDEAoperationB(I1,k2,n);
  4 in Seg len m by A1,FINSEQ_1:1;
  then 4 in dom m by FINSEQ_1:def 3;
  then
A19: I1.4 = Absval((n-BinarySequence m.4) 'xor' (n-BinarySequence t12)) by A8
,A9,A16,A10,Def12;
  then
A20: t21 = MUL_MOD(ADD_MOD(t10, Absval(((n-BinarySequence m.2) 'xor' (n
  -BinarySequence t12) ) 'xor' (n-BinarySequence Absval( (n-BinarySequence m.4)
  'xor' (n-BinarySequence t12) ) ) ),n),k2.6,n) by A15,A17,A14,BINARI_3:36
    .= MUL_MOD(ADD_MOD(t10, Absval(((n-BinarySequence m.2) 'xor' (n
  -BinarySequence t12) ) 'xor' ((n-BinarySequence m.4) 'xor' (n-BinarySequence
  t12) ) ),n),k2.6,n) by BINARI_3:36
    .= MUL_MOD(ADD_MOD(t10, Absval( (n-BinarySequence m.2) 'xor' ((n
-BinarySequence t12) 'xor' ((n-BinarySequence t12) 'xor' (n-BinarySequence m.4)
  ) ) ),n),k2.6,n) by Th9
    .= MUL_MOD(ADD_MOD(t10, Absval( (n-BinarySequence m.2) 'xor' ((n
-BinarySequence t12) 'xor' (n-BinarySequence t12) 'xor' (n-BinarySequence m.4)
  ) ),n),k2.6,n) by Th9
    .= MUL_MOD(ADD_MOD(t10, Absval( (n-BinarySequence m.2) 'xor' (ZERO(n)
  'xor' (n-BinarySequence m.4) ) ),n),k2.6,n) by Th6
    .= t11 by A7,A9,Th8;
A21: now
    let j be Nat;
    assume
A22: j in Seg len m;
    then j in Seg len I1 by A10,Def12;
    then
A23: j in dom I1 by FINSEQ_1:def 3;
A24: j in dom m by A22,FINSEQ_1:def 3;
    now
      per cases;
      suppose
A25:    j = 1;
A26:    m.1 < 2 to_power n by A2,Def3;
        thus I2.j = Absval((n-BinarySequence I1.1) 'xor' (n-BinarySequence t11
        )) by A12,A15,A18,A20,A23,A25,Def12
          .= Absval(((n-BinarySequence m.1) 'xor' (n-BinarySequence t11))
        'xor' (n-BinarySequence t11)) by A11,BINARI_3:36
          .= Absval((n-BinarySequence m.1) 'xor' ((n-BinarySequence t11)
        'xor' (n-BinarySequence t11))) by Th9
          .= Absval(ZERO(n) 'xor' (n-BinarySequence m.1)) by Th6
          .= Absval(n-BinarySequence m.1) by Th8
          .= m.j by A25,A26,BINARI_3:35;
      end;
      suppose
A27:    j = 2;
A28:    m.2 < 2 to_power n by A3,Def3;
        thus I2.j = Absval((n-BinarySequence I1.2) 'xor' (n-BinarySequence t12
        )) by A16,A12,A15,A18,A14,A20,A23,A27,Def12
          .= Absval(((n-BinarySequence m.2) 'xor' (n-BinarySequence t12))
        'xor' (n-BinarySequence t12)) by A17,BINARI_3:36
          .= Absval((n-BinarySequence m.2) 'xor' ((n-BinarySequence t12)
        'xor' (n-BinarySequence t12)))by Th9
          .= Absval(ZERO(n) 'xor' (n-BinarySequence m.2)) by Th6
          .= Absval(n-BinarySequence m.2) by Th8
          .= m.j by A27,A28,BINARI_3:35;
      end;
      suppose
A29:    j = 3;
A30:    m.3 < 2 to_power n by A4,Def3;
        thus I2.j = Absval((n-BinarySequence I1.3) 'xor' (n-BinarySequence t11
        )) by A12,A15,A18,A20,A23,A29,Def12
          .= Absval(((n-BinarySequence m.3) 'xor' (n-BinarySequence t11))
        'xor' (n-BinarySequence t11)) by A13,BINARI_3:36
          .= Absval((n-BinarySequence m.3) 'xor' ((n-BinarySequence t11)
        'xor' (n-BinarySequence t11))) by Th9
          .= Absval(ZERO(n) 'xor' (n-BinarySequence m.3)) by Th6
          .= Absval(n-BinarySequence m.3) by Th8
          .= m.j by A29,A30,BINARI_3:35;
      end;
      suppose
A31:    j = 4;
A32:    m.4 < 2 to_power n by A5,Def3;
        thus I2.j = Absval((n-BinarySequence I1.4) 'xor' (n-BinarySequence t12
        )) by A16,A12,A15,A18,A14,A20,A23,A31,Def12
          .= Absval(((n-BinarySequence m.4) 'xor' (n-BinarySequence t12))
        'xor' (n-BinarySequence t12)) by A19,BINARI_3:36
          .= Absval((n-BinarySequence m.4) 'xor' ((n-BinarySequence t12)
        'xor' (n-BinarySequence t12))) by Th9
          .= Absval(ZERO(n) 'xor' (n-BinarySequence m.4)) by Th6
          .= Absval(n-BinarySequence m.4) by Th8
          .= m.j by A31,A32,BINARI_3:35;
      end;
      suppose
A33:    j<>1 & j<>2 & j<>3 & j<>4;
        hence I2.j = I1.j by A18,A23,Def12
          .= m.j by A10,A24,A33,Def12;
      end;
    end;
    hence I2.j = m.j;
  end;
A34: Seg len m = dom m by FINSEQ_1:def 3;
  Seg len m = Seg len(I1) by A10,Def12
    .= Seg len(I2) by A18,Def12
    .= dom I2 by FINSEQ_1:def 3;
  hence thesis by A10,A18,A34,A21,FINSEQ_1:13;
end;

theorem
  for m holds len m >= 4 implies IDEAoperationC( IDEAoperationC(m) ) = m
proof
  let m be FinSequence of NAT;
  consider I1 being FinSequence of NAT such that
A1: I1 = IDEAoperationC(m);
  assume
A2: len m >= 4;
  then 2 <= len m by XXREAL_0:2;
  then 2 in Seg len m by FINSEQ_1:1;
  then 2 in dom m by FINSEQ_1:def 3;
  then
A3: I1.2 = m.3 by A1,Lm3;
  consider I2 being FinSequence of NAT such that
A4: I2 = IDEAoperationC(I1);
  3 <= len m by A2,XXREAL_0:2;
  then 3 in Seg len m by FINSEQ_1:1;
  then 3 in dom m by FINSEQ_1:def 3;
  then
A5: I1.3 = m.2 by A1,Lm4;
A6: now
    let j be Nat;
    assume
A7: j in Seg len m;
    then j in Seg len I1 by A1,Def13;
    then
A8: j in dom I1 by FINSEQ_1:def 3;
A9: j in dom m by A7,FINSEQ_1:def 3;
    now
      per cases;
      suppose
        j = 2;
        hence I2.j = m.j by A4,A5,A8,Lm3;
      end;
      suppose
        j = 3;
        hence I2.j = m.j by A4,A3,A8,Lm4;
      end;
      suppose
A10:    j<>2 & j<>3;
        hence I2.j = I1.j by A4,A8,Lm5
          .= m.j by A1,A9,A10,Lm5;
      end;
    end;
    hence I2.j = m.j;
  end;
A11: Seg len m = dom m by FINSEQ_1:def 3;
  Seg len m = Seg len(I1) by A1,Def13
    .= Seg len(I2) by A4,Def13
    .= dom I2 by FINSEQ_1:def 3;
  hence thesis by A1,A4,A11,A6,FINSEQ_1:13;
end;

begin :: Sequences of IDEA Cryptogram's operations
:: For making a model of IDEA, we define sequences of IDEA's
:: operations IDEA_P, IDEA_PS, IDEA_PE, IDEA_Q, IDEA_QS and
:: IDEA_QE. And, we define MESSAGES as plain and cipher text.

definition
  func MESSAGES -> set equals
  NAT*;
  coherence;
end;

registration
  cluster MESSAGES -> non empty;
  coherence;
end;

registration
  cluster MESSAGES -> functional;
  coherence;
end;

registration
  cluster -> FinSequence-like for Element of MESSAGES;
  coherence;
end;

definition
  let n be non empty Element of NAT,k;
  func IDEA_P(k,n) -> Function of MESSAGES, MESSAGES means
  :Def15:
  for m holds it.m = IDEAoperationA(IDEAoperationC(IDEAoperationB(m,k,n)),k,n);
  existence
  proof
    defpred P[set,set] means ex F be FinSequence of NAT st $1 = F & $2 =
    IDEAoperationA(IDEAoperationC( IDEAoperationB(F,k,n)),k,n);
A1: for e being Element of MESSAGES ex u being Element of MESSAGES st P[e, u]
    proof
      let e be Element of MESSAGES;
      reconsider F = e as FinSequence of NAT by FINSEQ_1:def 11;
      reconsider u = IDEAoperationA(IDEAoperationC( IDEAoperationB(F,k,n)),k,n
      ) as Element of MESSAGES by FINSEQ_1:def 11;
      take u;
      thus thesis;
    end;
    consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds P[e,m1.e] from FUNCT_2:sch 3
    (A1);
    take m1;
    let m be FinSequence of NAT;
    m is Element of MESSAGES by FINSEQ_1:def 11;
    then ex F being FinSequence of NAT st m = F & m1.m = IDEAoperationA(
    IDEAoperationC( IDEAoperationB(F,k,n)),k,n) by A2;
    hence thesis;
  end;
  uniqueness
  proof
    let m1,m2 be Function of MESSAGES, MESSAGES such that
A3: for m being FinSequence of NAT holds m1.m = IDEAoperationA(
    IDEAoperationC( IDEAoperationB(m,k,n)),k,n) and
A4: for m being FinSequence of NAT holds m2.m = IDEAoperationA(
    IDEAoperationC( IDEAoperationB(m,k,n)),k,n);
A5: now
      let j be set;
      consider jj being set such that
A6:   jj = j;
      assume j in MESSAGES;
      then reconsider jj as FinSequence of NAT by A6,FINSEQ_1:def 11;
      thus m1.j = IDEAoperationA(IDEAoperationC( IDEAoperationB(jj,k,n)),k,n)
      by A3,A6
        .= m2.j by A4,A6;
    end;
    dom m1 = MESSAGES & dom m2 = MESSAGES by FUNCT_2:def 1;
    hence thesis by A5,FUNCT_1:2;
  end;
end;

definition
  let n be non empty Element of NAT,k;
  func IDEA_Q(k,n) -> Function of MESSAGES, MESSAGES means
  :Def16:
  for m holds it.m = IDEAoperationB(IDEAoperationA(IDEAoperationC(m),k,n),k,n);
  existence
  proof
    defpred P[set,set] means ex F be FinSequence of NAT st $1 = F & $2 =
    IDEAoperationB(IDEAoperationA( IDEAoperationC(F),k,n),k,n);
A1: for e being Element of MESSAGES ex u being Element of MESSAGES st P[e, u]
    proof
      let e be Element of MESSAGES;
      reconsider F = e as FinSequence of NAT by FINSEQ_1:def 11;
      reconsider u = IDEAoperationB(IDEAoperationA( IDEAoperationC(F),k,n),k,n
      ) as Element of MESSAGES by FINSEQ_1:def 11;
      take u;
      thus thesis;
    end;
    consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds P[e,m1.e] from FUNCT_2:sch 3
    (A1);
    take m1;
    let m be FinSequence of NAT;
    m is Element of MESSAGES by FINSEQ_1:def 11;
    then ex F being FinSequence of NAT st m = F & m1.m = IDEAoperationB(
    IDEAoperationA( IDEAoperationC(F),k,n),k,n) by A2;
    hence thesis;
  end;
  uniqueness
  proof
    let m1,m2 be Function of MESSAGES, MESSAGES such that
A3: for m being FinSequence of NAT holds m1.m = IDEAoperationB(
    IDEAoperationA( IDEAoperationC(m),k,n),k,n) and
A4: for m being FinSequence of NAT holds m2.m = IDEAoperationB(
    IDEAoperationA( IDEAoperationC(m),k,n),k,n);
A5: now
      let j be set;
      consider jj being set such that
A6:   jj = j;
      assume j in MESSAGES;
      then reconsider jj as FinSequence of NAT by A6,FINSEQ_1:def 11;
      thus m1.j = IDEAoperationB(IDEAoperationA( IDEAoperationC(jj),k,n),k,n)
      by A3,A6
        .= m2.j by A4,A6;
    end;
    dom m1 = MESSAGES & dom m2 = MESSAGES by FUNCT_2:def 1;
    hence thesis by A5,FUNCT_1:2;
  end;
end;

definition
  let r,lk be Element of NAT,n be non empty Element of NAT, Key be Matrix of
  lk,6,NAT;
  func IDEA_P_F(Key,n,r) -> FinSequence means
  :Def17:
  len it = r & for i st i in dom it holds it.i = IDEA_P(Line(Key,i),n);
  existence
  proof
    deffunc F(Nat)=IDEA_P(Line(Key,$1),n);
    consider z being FinSequence such that
A1: len z = r & for k being Nat st k in dom z holds z.k= F(k) from
    FINSEQ_1:sch 2;
    take z;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let z1,z2 be FinSequence such that
A2: len z1 = r and
A3: for i being Element of NAT st i in dom z1 holds z1.i = IDEA_P(Line
    ( Key,i),n) and
A4: len z2 = r and
A5: for i being Element of NAT st i in dom z2 holds z2.i = IDEA_P(Line
    ( Key,i),n);
A6: now
      let j be Nat;
      assume
A7:   j in Seg r;
      then
A8:   j in dom z2 by A4,FINSEQ_1:def 3;
      j in dom z1 by A2,A7,FINSEQ_1:def 3;
      then z1.j = IDEA_P(Line(Key,j),n) by A3
        .= z2.j by A5,A8;
      hence z1.j = z2.j;
    end;
    Seg r = dom z1 & Seg r = dom z2 by A2,A4,FINSEQ_1:def 3;
    hence thesis by A6,FINSEQ_1:13;
  end;
end;

registration
  let r,lk be Element of NAT,n be non empty Element of NAT, Key be Matrix of
  lk,6,NAT;
  cluster IDEA_P_F(Key,n,r) -> Function-yielding;
  coherence
  proof
    for x being set st x in dom IDEA_P_F(Key,n,r) holds IDEA_P_F(Key,n,r).
    x is Function
    proof
      let x be set;
      assume
A1:   x in dom IDEA_P_F(Key,n,r);
      then consider xx being Element of NAT such that
A2:   xx = x;
      IDEA_P_F(Key,n,r).xx = IDEA_P(Line(Key,xx),n) by A1,A2,Def17;
      hence thesis by A2;
    end;
    hence thesis by FUNCOP_1:def 6;
  end;
end;

definition
  let r,lk be Element of NAT,n be non empty Element of NAT, Key be Matrix of
  lk,6,NAT;
  func IDEA_Q_F(Key,n,r) -> FinSequence means
  :Def18:
  len it = r & for i st i in dom it holds it.i = IDEA_Q(Line(Key,r-'i+1),n);
  existence
  proof
    deffunc F(Nat)=IDEA_Q(Line(Key,r-'$1+1),n);
    consider z being FinSequence such that
A1: len z = r & for k being Nat st k in dom z holds z.k= F(k) from
    FINSEQ_1:sch 2;
    take z;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let z1,z2 be FinSequence such that
A2: len z1 = r and
A3: for i being Element of NAT st i in dom z1 holds z1.i = IDEA_Q(Line
    ( Key,r-'i+1),n) and
A4: len z2 = r and
A5: for i being Element of NAT st i in dom z2 holds z2.i = IDEA_Q(Line
    ( Key,r-'i+1),n);
A6: now
      let j be Nat;
      assume
A7:   j in Seg r;
      then
A8:   j in dom z2 by A4,FINSEQ_1:def 3;
      j in dom z1 by A2,A7,FINSEQ_1:def 3;
      then z1.j = IDEA_Q(Line(Key,r-'j+1),n) by A3
        .= z2.j by A5,A8;
      hence z1.j = z2.j;
    end;
    Seg r = dom z1 & Seg r = dom z2 by A2,A4,FINSEQ_1:def 3;
    hence thesis by A6,FINSEQ_1:13;
  end;
end;

registration
  let r,lk be Element of NAT,n be non empty Element of NAT, Key be Matrix of
  lk,6,NAT;
  cluster IDEA_Q_F(Key,n,r) -> Function-yielding;
  coherence
  proof
    for x being set st x in dom IDEA_Q_F(Key,n,r) holds IDEA_Q_F(Key,n,r).
    x is Function
    proof
      let x be set;
      assume
A1:   x in dom IDEA_Q_F(Key,n,r);
      then consider xx being Element of NAT such that
A2:   xx = x;
      IDEA_Q_F(Key,n,r).xx = IDEA_Q(Line(Key,r-'xx+1),n) by A1,A2,Def18;
      hence thesis by A2;
    end;
    hence thesis by FUNCOP_1:def 6;
  end;
end;

definition
  let k,n;
  func IDEA_PS(k,n) -> Function of MESSAGES, MESSAGES means
  :Def19:
  for m holds it.m = IDEAoperationA(m,k,n);
  existence
  proof
    defpred P[set,set] means ex F be FinSequence of NAT st $1 = F & $2 =
    IDEAoperationA(F,k,n);
A1: for e being Element of MESSAGES ex u being Element of MESSAGES st P[e, u]
    proof
      let e be Element of MESSAGES;
      reconsider F = e as FinSequence of NAT by FINSEQ_1:def 11;
      reconsider u = IDEAoperationA(F,k,n) as Element of MESSAGES by
FINSEQ_1:def 11;
      take u;
      thus thesis;
    end;
    consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds P[e,m1.e] from FUNCT_2:sch 3
    (A1);
    take m1;
    let m be FinSequence of NAT;
    m is Element of MESSAGES by FINSEQ_1:def 11;
    then ex F being FinSequence of NAT st m = F & m1.m = IDEAoperationA(F,k,n)
    by A2;
    hence thesis;
  end;
  uniqueness
  proof
    let m1,m2 be Function of MESSAGES, MESSAGES such that
A3: for m being FinSequence of NAT holds m1.m = IDEAoperationA(m,k,n) and
A4: for m being FinSequence of NAT holds m2.m = IDEAoperationA(m,k,n);
A5: now
      let j be set;
      consider jj being set such that
A6:   jj = j;
      assume j in MESSAGES;
      then reconsider jj as FinSequence of NAT by A6,FINSEQ_1:def 11;
      thus m1.j = IDEAoperationA(jj,k,n) by A3,A6
        .= m2.j by A4,A6;
    end;
    dom m1 = MESSAGES & dom m2 = MESSAGES by FUNCT_2:def 1;
    hence thesis by A5,FUNCT_1:2;
  end;
end;

definition
  let k,n;
  func IDEA_QS(k,n) -> Function of MESSAGES, MESSAGES means
  :Def20:
  for m holds it.m = IDEAoperationA(m,k,n);
  existence
  proof
    defpred P[set,set] means ex F be FinSequence of NAT st $1 = F & $2 =
    IDEAoperationA(F,k,n);
A1: for e being Element of MESSAGES ex u being Element of MESSAGES st P[e, u]
    proof
      let e be Element of MESSAGES;
      reconsider F = e as FinSequence of NAT by FINSEQ_1:def 11;
      reconsider u = IDEAoperationA(F,k,n) as Element of MESSAGES by
FINSEQ_1:def 11;
      take u;
      thus thesis;
    end;
    consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds P[e,m1.e] from FUNCT_2:sch 3
    (A1);
    take m1;
    let m be FinSequence of NAT;
    m is Element of MESSAGES by FINSEQ_1:def 11;
    then ex F being FinSequence of NAT st m = F & m1.m = IDEAoperationA(F,k,n)
    by A2;
    hence thesis;
  end;
  uniqueness
  proof
    let m1,m2 be Function of MESSAGES, MESSAGES such that
A3: for m being FinSequence of NAT holds m1.m = IDEAoperationA(m,k,n) and
A4: for m being FinSequence of NAT holds m2.m = IDEAoperationA(m,k,n);
A5: now
      let j be set;
      consider jj being set such that
A6:   jj = j;
      assume j in MESSAGES;
      then reconsider jj as FinSequence of NAT by A6,FINSEQ_1:def 11;
      thus m1.j = IDEAoperationA(jj,k,n) by A3,A6
        .= m2.j by A4,A6;
    end;
    dom m1 = MESSAGES & dom m2 = MESSAGES by FUNCT_2:def 1;
    hence thesis by A5,FUNCT_1:2;
  end;
end;

definition
  let n be non empty Element of NAT,k;
  func IDEA_PE(k,n) -> Function of MESSAGES, MESSAGES means
  :Def21:
  for m holds it.m = IDEAoperationA(IDEAoperationB(m,k,n),k,n);
  existence
  proof
    defpred P[set,set] means ex F be FinSequence of NAT st $1 = F & $2 =
    IDEAoperationA(IDEAoperationB(F,k,n),k,n);
A1: for e being Element of MESSAGES ex u being Element of MESSAGES st P[e, u]
    proof
      let e be Element of MESSAGES;
      reconsider F = e as FinSequence of NAT by FINSEQ_1:def 11;
      reconsider u = IDEAoperationA( IDEAoperationB(F,k,n),k,n) as Element of
      MESSAGES by FINSEQ_1:def 11;
      take u;
      thus thesis;
    end;
    consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds P[e,m1.e] from FUNCT_2:sch 3
    (A1);
    take m1;
    let m be FinSequence of NAT;
    m is Element of MESSAGES by FINSEQ_1:def 11;
    then ex F being FinSequence of NAT st m = F & m1.m = IDEAoperationA(
    IDEAoperationB(F,k,n),k,n) by A2;
    hence thesis;
  end;
  uniqueness
  proof
    let m1,m2 be Function of MESSAGES, MESSAGES such that
A3: for m being FinSequence of NAT holds m1.m = IDEAoperationA(
    IDEAoperationB(m,k,n),k,n) and
A4: for m being FinSequence of NAT holds m2.m = IDEAoperationA(
    IDEAoperationB(m,k,n),k,n);
A5: now
      let j be set;
      consider jj being set such that
A6:   jj = j;
      assume j in MESSAGES;
      then reconsider jj as FinSequence of NAT by A6,FINSEQ_1:def 11;
      thus m1.j = IDEAoperationA( IDEAoperationB(jj,k,n),k,n) by A3,A6
        .= m2.j by A4,A6;
    end;
    dom m1 = MESSAGES & dom m2 = MESSAGES by FUNCT_2:def 1;
    hence thesis by A5,FUNCT_1:2;
  end;
end;

definition
  let n be non empty Element of NAT,k;
  func IDEA_QE(k,n) -> Function of MESSAGES, MESSAGES means
  :Def22:
  for m holds it.m = IDEAoperationB(IDEAoperationA(m,k,n),k,n);
  existence
  proof
    defpred P[set,set] means ex F be FinSequence of NAT st $1 = F & $2 =
    IDEAoperationB(IDEAoperationA(F,k,n),k,n);
A1: for e being Element of MESSAGES ex u being Element of MESSAGES st P[e, u]
    proof
      let e be Element of MESSAGES;
      reconsider F = e as FinSequence of NAT by FINSEQ_1:def 11;
      reconsider u = IDEAoperationB( IDEAoperationA(F,k,n),k,n) as Element of
      MESSAGES by FINSEQ_1:def 11;
      take u;
      thus thesis;
    end;
    consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds P[e,m1.e] from FUNCT_2:sch 3
    (A1);
    take m1;
    let m be FinSequence of NAT;
    m is Element of MESSAGES by FINSEQ_1:def 11;
    then ex F being FinSequence of NAT st m = F & m1.m = IDEAoperationB(
    IDEAoperationA(F,k,n),k,n) by A2;
    hence thesis;
  end;
  uniqueness
  proof
    let m1,m2 be Function of MESSAGES, MESSAGES such that
A3: for m being FinSequence of NAT holds m1.m = IDEAoperationB(
    IDEAoperationA(m,k,n),k,n) and
A4: for m being FinSequence of NAT holds m2.m = IDEAoperationB(
    IDEAoperationA(m,k,n),k,n);
A5: now
      let j be set;
      consider jj being set such that
A6:   jj = j;
      assume j in MESSAGES;
      then reconsider jj as FinSequence of NAT by A6,FINSEQ_1:def 11;
      thus m1.j = IDEAoperationB( IDEAoperationA(jj,k,n),k,n) by A3,A6
        .= m2.j by A4,A6;
    end;
    dom m1 = MESSAGES & dom m2 = MESSAGES by FUNCT_2:def 1;
    hence thesis by A5,FUNCT_1:2;
  end;
end;

theorem Th33:
  for n being non empty Element of NAT,m,k1,k2 holds 2 to_power(n)
+1 is prime & len m >= 4 & m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n & k1.1 is_expressible_by n &
k1.2 is_expressible_by n & k1.3 is_expressible_by n & k1.4 is_expressible_by n
& k2.1 = INV_MOD(k1.1,n) & k2.2 = NEG_MOD(k1.3,n) & k2.3 = NEG_MOD(k1.2,n) & k2
.4 = INV_MOD(k1.4,n) & k2.5 = k1.5 & k2.6 = k1.6 implies (IDEA_Q(k2,n)*IDEA_P(
  k1,n)).m = m
proof
  let n be non empty Element of NAT;
  let m,k1,k2;
  assume that
A1: 2 to_power(n)+1 is prime and
A2: len m >= 4 and
A3: m.1 is_expressible_by n & m.2 is_expressible_by n & m.3
  is_expressible_by n & m.4 is_expressible_by n and
A4: k1.1 is_expressible_by n & k1.2 is_expressible_by n & k1.3
is_expressible_by n & k1.4 is_expressible_by n & k2.1 = INV_MOD(k1.1,n) & k2.2
  = NEG_MOD(k1.3,n) & k2.3 = NEG_MOD(k1.2, n) & k2.4 = INV_MOD(k1.4,n) and
A5: k2.5 = k1.5 & k2.6 = k1.6;
A6: IDEAoperationB(m,k1,n).2 is_expressible_by n & IDEAoperationB(m,k1,n).3
  is_expressible_by n by A2,Th27;
A7: IDEAoperationB(m,k1,n).4 is_expressible_by n by A2,Th27;
A8: len IDEAoperationB(m,k1,n) >= 4 & IDEAoperationB(m,k1,n).1
  is_expressible_by n by A2,Def12,Th27;
  dom IDEA_P(k1,n) = MESSAGES by FUNCT_2:def 1;
  then m in dom IDEA_P(k1,n) by FINSEQ_1:def 11;
  then (IDEA_Q(k2,n)*IDEA_P(k1,n)).m = IDEA_Q(k2,n).(IDEA_P(k1,n).m) by
FUNCT_1:13
    .= IDEA_Q(k2,n). IDEAoperationA(IDEAoperationC(IDEAoperationB(m,k1,n)),
  k1,n) by Def15
    .= IDEAoperationB(IDEAoperationA(IDEAoperationC( IDEAoperationA(
  IDEAoperationC(IDEAoperationB(m,k1,n)),k1,n) ),k2,n),k2,n) by Def16
    .= IDEAoperationB(IDEAoperationB(m,k1,n),k2,n) by A1,A4,A8,A6,A7,Th30
    .= m by A2,A3,A5,Th31;
  hence thesis;
end;

theorem Th34:
  for n being non empty Element of NAT,m,k1,k2 holds 2 to_power(n)
+1 is prime & len m >= 4 & m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n & k1.1 is_expressible_by n &
k1.2 is_expressible_by n & k1.3 is_expressible_by n & k1.4 is_expressible_by n
& k2.1 = INV_MOD(k1.1,n) & k2.2 = NEG_MOD(k1.2,n) & k2.3 = NEG_MOD(k1.3,n) & k2
  .4 = INV_MOD(k1.4,n) implies (IDEA_QS(k2,n)*IDEA_PS(k1,n)).m = m
proof
  let n be non empty Element of NAT;
  let m,k1,k2;
  assume
A1: 2 to_power(n)+1 is prime & len m >= 4 & m.1 is_expressible_by n & m.
2 is_expressible_by n & m.3 is_expressible_by n & m.4 is_expressible_by n & k1.
  1 is_expressible_by n & k1.2 is_expressible_by n & k1.3 is_expressible_by n &
k1.4 is_expressible_by n & k2.1 = INV_MOD( k1. 1,n) & k2.2 = NEG_MOD(k1.2,n ) &
  k2.3 = NEG_MOD(k1.3,n) & k2.4 = INV_MOD(k1.4 ,n);
  dom IDEA_PS(k1,n) = MESSAGES by FUNCT_2:def 1;
  then m in dom IDEA_PS(k1,n) by FINSEQ_1:def 11;
  then (IDEA_QS(k2,n)*IDEA_PS(k1,n)).m = IDEA_QS(k2,n).(IDEA_PS(k1,n).m) by
FUNCT_1:13
    .= IDEA_QS(k2,n).IDEAoperationA(m,k1,n) by Def19
    .= IDEAoperationA(IDEAoperationA(m,k1,n),k2,n) by Def20
    .= m by A1,Th29;
  hence thesis;
end;

theorem Th35:
  for n being non empty Element of NAT,m,k1,k2 holds 2 to_power(n)
+1 is prime & len m >= 4 & m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n & k1.1 is_expressible_by n &
k1.2 is_expressible_by n & k1.3 is_expressible_by n & k1.4 is_expressible_by n
& k2.1 = INV_MOD(k1.1,n) & k2.2 = NEG_MOD(k1.2,n) & k2.3 = NEG_MOD(k1.3,n) & k2
.4 = INV_MOD(k1.4,n) & k2.5 = k1.5 & k2.6 = k1.6 implies (IDEA_QE(k2,n)*IDEA_PE
  (k1,n)).m = m
proof
  let n be non empty Element of NAT;
  let m,k1,k2;
  assume that
A1: 2 to_power(n)+1 is prime and
A2: len m >= 4 and
A3: m.1 is_expressible_by n & m.2 is_expressible_by n & m.3
  is_expressible_by n & m.4 is_expressible_by n and
A4: k1.1 is_expressible_by n & k1.2 is_expressible_by n & k1.3
is_expressible_by n & k1.4 is_expressible_by n & k2.1 = INV_MOD(k1.1,n) & k2.2
  = NEG_MOD(k1.2,n) & k2.3 = NEG_MOD(k1.3, n) & k2.4 = INV_MOD(k1.4,n) and
A5: k2.5 = k1.5 & k2.6 = k1.6;
A6: IDEAoperationB(m,k1,n).2 is_expressible_by n & IDEAoperationB(m,k1,n).3
  is_expressible_by n by A2,Th27;
A7: IDEAoperationB(m,k1,n).4 is_expressible_by n by A2,Th27;
A8: len IDEAoperationB(m,k1,n) >= 4 & IDEAoperationB(m,k1,n).1
  is_expressible_by n by A2,Def12,Th27;
  dom IDEA_PE(k1,n) = MESSAGES by FUNCT_2:def 1;
  then m in dom IDEA_PE(k1,n) by FINSEQ_1:def 11;
  then (IDEA_QE(k2,n)*IDEA_PE(k1,n)).m = IDEA_QE(k2,n).(IDEA_PE(k1,n).m) by
FUNCT_1:13
    .= IDEA_QE(k2,n). IDEAoperationA(IDEAoperationB(m,k1,n),k1,n) by Def21
    .= IDEAoperationB(IDEAoperationA( IDEAoperationA(IDEAoperationB(m,k1,n),
  k1,n),k2,n),k2,n) by Def22
    .= IDEAoperationB(IDEAoperationB(m,k1,n),k2,n) by A1,A4,A8,A6,A7,Th29
    .= m by A2,A3,A5,Th31;
  hence thesis;
end;

theorem Th36:
  for n being non empty Element of NAT,lk being Element of NAT,
Key being Matrix of lk,6,NAT, k being Element of NAT holds IDEA_P_F(Key,n,(k+1)
  ) = IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>
proof
  let n be non empty Element of NAT;
  let lk be Element of NAT;
  let Key be Matrix of lk,6,NAT;
  let k be Element of NAT;
A1: for i being Nat st 1 <= i & i <= len IDEA_P_F(Key,n,(k+1)) holds
IDEA_P_F(Key,n,(k+1)).i = (IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>).i
  proof
    dom <* IDEA_P(Line(Key,(k+1)),n) *> = Seg 1 by FINSEQ_1:def 8;
    then
A2: 1 in dom <*IDEA_P(Line(Key,(k+1)),n)*> by FINSEQ_1:1;
    let i be Nat;
    assume that
A3: 1 <= i and
A4: i <= len IDEA_P_F(Key,n,(k+1));
    i in Seg len IDEA_P_F(Key,n,(k+1)) by A3,A4,FINSEQ_1:1;
    then
A5: i in dom IDEA_P_F(Key,n,(k+1)) by FINSEQ_1:def 3;
A6: i <= k+1 by A4,Def17;
    now
      per cases;
      suppose
        i <> k+1;
        then i <= k by A6,NAT_1:8;
        then i in Seg k by A3,FINSEQ_1:1;
        then i in Seg len IDEA_P_F(Key,n,k) by Def17;
        then
A7:     i in dom IDEA_P_F(Key,n,k) by FINSEQ_1:def 3;
        hence
        (IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>).i = IDEA_P_F(
        Key,n,k).i by FINSEQ_1:def 7
          .= IDEA_P(Line(Key,i),n) by A7,Def17
          .= IDEA_P_F(Key,n,(k+1)).i by A5,Def17;
      end;
      suppose
A8:     i = k+1;
        hence
        (IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>).i =(IDEA_P_F(
Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>). (len IDEA_P_F(Key,n,k) + 1) by Def17
          .= <* IDEA_P(Line(Key,(k+1)),n) *>.1 by A2,FINSEQ_1:def 7
          .= IDEA_P(Line(Key,(k+1)),n) by FINSEQ_1:40
          .= IDEA_P_F(Key,n,(k+1)).i by A5,A8,Def17;
      end;
    end;
    hence thesis;
  end;
  len (IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>) = len IDEA_P_F(
  Key,n,k) + len <* IDEA_P(Line(Key,(k+1)),n) *> by FINSEQ_1:22
    .= k + len <* IDEA_P(Line(Key,(k+1)),n) *> by Def17
    .= k + 1 by FINSEQ_1:39;
  then
  len IDEA_P_F(Key,n,(k+1)) = len (IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k
  +1)),n) *>) by Def17;
  hence thesis by A1,FINSEQ_1:14;
end;

theorem Th37:
  for n being non empty Element of NAT,lk being Element of NAT,
Key being Matrix of lk,6,NAT, k being Element of NAT holds IDEA_Q_F(Key,n,(k+1)
  ) = <* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k)
proof
  let n be non empty Element of NAT;
  let lk be Element of NAT;
  let Key be Matrix of lk,6,NAT;
  let k be Element of NAT;
A1: for i being Nat st 1 <= i & i <= len IDEA_Q_F(Key,n,(k+1)) holds
  IDEA_Q_F(Key,n,(k+1)).i = (<* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k)).i
  proof
    dom <* IDEA_Q(Line(Key,(k+1)),n) *> = Seg 1 by FINSEQ_1:def 8;
    then
A2: 1 in dom <*IDEA_Q(Line(Key,(k+1)),n)*> by FINSEQ_1:1;
    let i be Nat;
    assume that
A3: 1 <= i and
A4: i <= len IDEA_Q_F(Key,n,(k+1));
A5: i <= k+1 by A4,Def18;
    1 <= len IDEA_Q_F(Key,n,(k+1)) by A3,A4,XXREAL_0:2;
    then 1 in Seg len IDEA_Q_F(Key,n,(k+1)) by FINSEQ_1:1;
    then
A6: 1 in dom IDEA_Q_F(Key,n,(k+1)) by FINSEQ_1:def 3;
    i in Seg len IDEA_Q_F(Key,n,(k+1)) by A3,A4,FINSEQ_1:1;
    then
A7: i in dom IDEA_Q_F(Key,n,(k+1)) by FINSEQ_1:def 3;
    now
      per cases;
      suppose
A8:     i <> 1;
        consider ii be Integer such that
A9:     ii = i - 1;
A10:    ii + 1 = i by A9;
A11:    (k+1) - i >= i - i by A5,XREAL_1:9;
        1 - 1 <= i - 1 by A3,XREAL_1:9;
        then reconsider ii as Element of NAT by A9,INT_1:3;
A12:    i-1 <= k+1-1 by A5,XREAL_1:9;
        then ii - ii <= k - ii by A9,XREAL_1:9;
        then
A13:    k -' ii = (k+1) + -i by A9,XREAL_0:def 2
          .=(k+1) -' i by A11,XREAL_0:def 2;
        1 < i by A3,A8,XXREAL_0:1;
        then 1 + 1 <= i by NAT_1:13;
        then 1 + 1 - 1 <= i - 1 by XREAL_1:9;
        then ii in Seg k by A9,A12,FINSEQ_1:1;
        then ii in Seg len IDEA_Q_F(Key,n,k) by Def18;
        then
A14:    ii in dom IDEA_Q_F(Key,n,k) by FINSEQ_1:def 3;
        thus (<* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k)).i =(<* IDEA_Q(
Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k)). (len <*IDEA_Q(Line(Key,(k+1)),n)*>+ii)
        by A10,FINSEQ_1:40
          .=IDEA_Q_F(Key,n,k).ii by A14,FINSEQ_1:def 7
          .=IDEA_Q(Line(Key,(k+1)-'i+1),n) by A14,A13,Def18
          .=IDEA_Q_F(Key,n,k+1).i by A7,Def18;
      end;
      suppose
A15:    i = 1;
        hence (<* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k)).i = <* IDEA_Q(
        Line(Key,k+1),n) *>.1 by A2,FINSEQ_1:def 7
          .= IDEA_Q(Line(Key,k+1),n) by FINSEQ_1:40
          .= IDEA_Q(Line(Key,(k+1)-'1 + 1),n) by A3,A5,XREAL_1:235,XXREAL_0:2
          .= IDEA_Q_F(Key,n,k+1).i by A6,A15,Def18;
      end;
    end;
    hence thesis;
  end;
  len (<* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k)) = len <* IDEA_Q(
  Line(Key,k+1),n) *> + len IDEA_Q_F(Key,n,k) by FINSEQ_1:22
    .= len <* IDEA_Q(Line(Key,k+1),n) *> + k by Def18
    .= k + 1 by FINSEQ_1:39;
  then
  len IDEA_Q_F(Key,n,(k+1)) = len (<* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(
  Key,n,k)) by Def18;
  hence thesis by A1,FINSEQ_1:14;
end;

theorem Th38:
  for n being non empty Element of NAT,lk being Element of NAT,
Key being Matrix of lk,6,NAT, k being Element of NAT holds IDEA_P_F(Key,n,k) is
  FuncSeq-like FinSequence
proof
  let n be non empty Element of NAT;
  let lk be Element of NAT;
  let Key be Matrix of lk,6,NAT;
  let k be Element of NAT;
  set p = Seg(k+1) --> MESSAGES;
A1: dom p = Seg(k+1) by FUNCOP_1:13;
  reconsider p as FinSequence;
A2: for i being Element of NAT st i in dom IDEA_P_F(Key,n,k) holds IDEA_P_F(
  Key,n,k).i in Funcs(p.i, p.(i+1))
  proof
    let i be Element of NAT;
    assume
A3: i in dom IDEA_P_F(Key,n,k);
    then
A4: i in Seg len IDEA_P_F(Key,n,k) by FINSEQ_1:def 3;
    then i in Seg k by Def17;
    then
A5: i <= k by FINSEQ_1:1;
    then
A6: i <= k+1 by NAT_1:12;
    1 <= (i+1) & (i+1) <= k+1 by A5,NAT_1:12,XREAL_1:6;
    then (i+1) in Seg (k+1) by FINSEQ_1:1;
    then
A7: p.(i+1) = MESSAGES by FUNCOP_1:7;
    1 <= i by A4,FINSEQ_1:1;
    then i in Seg (k+1) by A6,FINSEQ_1:1;
    then
A8: p.i = MESSAGES by FUNCOP_1:7;
    IDEA_P_F(Key,n,k).i = IDEA_P(Line(Key,i),n) by A3,Def17;
    hence thesis by A8,A7,FUNCT_2:9;
  end;
  len p = k+1 by A1,FINSEQ_1:def 3;
  then len p = len IDEA_P_F(Key,n,k)+1 by Def17;
  hence thesis by A2,FUNCT_7:def 8;
end;

theorem Th39:
  for n being non empty Element of NAT,lk being Element of NAT,
Key being Matrix of lk,6,NAT, k being Element of NAT holds IDEA_Q_F(Key,n,k) is
  FuncSeq-like FinSequence
proof
  let n be non empty Element of NAT;
  let lk be Element of NAT;
  let Key be Matrix of lk,6,NAT;
  let k be Element of NAT;
  set p = Seg(k+1) --> MESSAGES;
A1: dom p = Seg(k+1) by FUNCOP_1:13;
  reconsider p as FinSequence;
A2: for i being Element of NAT st i in dom IDEA_Q_F(Key,n,k) holds IDEA_Q_F(
  Key,n,k).i in Funcs(p.i, p.(i+1))
  proof
    let i be Element of NAT;
    assume
A3: i in dom IDEA_Q_F(Key,n,k);
    then
A4: i in Seg len IDEA_Q_F(Key,n,k) by FINSEQ_1:def 3;
    then i in Seg k by Def18;
    then
A5: i <= k by FINSEQ_1:1;
    then
A6: i <= k+1 by NAT_1:12;
    1 <= (i+1) & (i+1) <= k+1 by A5,NAT_1:12,XREAL_1:6;
    then (i+1) in Seg (k+1) by FINSEQ_1:1;
    then
A7: p.(i+1) = MESSAGES by FUNCOP_1:7;
    1 <= i by A4,FINSEQ_1:1;
    then i in Seg (k+1) by A6,FINSEQ_1:1;
    then
A8: p.i = MESSAGES by FUNCOP_1:7;
    IDEA_Q_F(Key,n,k).i = IDEA_Q(Line(Key,k-'i+1),n) by A3,Def18;
    hence thesis by A8,A7,FUNCT_2:9;
  end;
  len p = k+1 by A1,FINSEQ_1:def 3;
  then len p = len IDEA_Q_F(Key,n,k)+1 by Def18;
  hence thesis by A2,FUNCT_7:def 8;
end;

theorem Th40:
  for n being non empty Element of NAT,lk being Element of NAT,
  Key being Matrix of lk,6,NAT, k being Element of NAT holds k <> 0 implies
  IDEA_P_F(Key,n,k) is FuncSequence of MESSAGES,MESSAGES
proof
  let n be non empty Element of NAT;
  let lk be Element of NAT, Key be Matrix of lk,6,NAT, k be Element of NAT;
A1: k = len IDEA_P_F(Key,n,k) by Def17;
  assume
A2: k<>0;
  then 0+1 < k+1 by XREAL_1:6;
  then
A3: 1 <= k by NAT_1:13;
  0+1 < k+1 by A2,XREAL_1:6;
  then 1 <= k by NAT_1:13;
  then 1 in Seg len IDEA_P_F(Key,n,k) by A1,FINSEQ_1:1;
  then
A4: 1 in dom IDEA_P_F(Key,n,k) by FINSEQ_1:def 3;
  len (IDEA_P_F(Key,n,k)) = k by Def17;
  then not IDEA_P_F(Key,n,k)=<*>MESSAGES by A2;
  then
A5: firstdom IDEA_P_F(Key,n,k) = proj1 (IDEA_P_F(Key,n,k).1) by FUNCT_7:def 6
    .= proj1 (IDEA_P(Line(Key,1),n)) by A4,Def17
    .= dom IDEA_P(Line(Key,1),n)
    .= MESSAGES by FUNCT_2:def 1;
  k = len IDEA_P_F(Key,n,k) by Def17;
  then k in Seg len IDEA_P_F(Key,n,k) by A3,FINSEQ_1:1;
  then
A6: k in dom IDEA_P_F(Key,n,k) by FINSEQ_1:def 3;
  len (IDEA_P_F(Key,n,k)) <> 0 by A2,Def17;
  then not IDEA_P_F(Key,n,k)=<*>MESSAGES;
  then
  lastrng IDEA_P_F(Key,n,k) = proj2 (IDEA_P_F(Key,n,k). len (IDEA_P_F(Key
  ,n,k))) by FUNCT_7:def 7
    .= proj2 (IDEA_P_F(Key,n,k).k) by Def17
    .= proj2 (IDEA_P(Line(Key,k),n)) by A6,Def17
    .= rng IDEA_P(Line(Key,k),n);
  then
A7: lastrng IDEA_P_F(Key,n,k) c= MESSAGES by RELAT_1:def 19;
  IDEA_P_F(Key,n,k) is FuncSequence by Th38;
  hence thesis by A7,A5,FUNCT_7:def 9;
end;

theorem Th41:
  for n being non empty Element of NAT,lk being Element of NAT,
  Key being Matrix of lk,6,NAT, k being Element of NAT holds k <> 0 implies
  IDEA_Q_F(Key,n,k) is FuncSequence of MESSAGES,MESSAGES
proof
  let n be non empty Element of NAT, lk be Element of NAT, Key be Matrix of lk
  ,6,NAT, r be Element of NAT;
  assume
A1: r<>0;
  then 0+1 < r+1 by XREAL_1:6;
  then
A2: 1 <= r by NAT_1:13;
  0+1 < r+1 by A1,XREAL_1:6;
  then
A3: 1 <= r by NAT_1:13;
  r = len IDEA_Q_F(Key,n,r) by Def18;
  then 1 in Seg len IDEA_Q_F(Key,n,r) by A3,FINSEQ_1:1;
  then
A4: 1 in dom IDEA_Q_F(Key,n,r) by FINSEQ_1:def 3;
  len (IDEA_Q_F(Key,n,r)) <> 0 by A1,Def18;
  then not IDEA_Q_F(Key,n,r)=<*>MESSAGES;
  then
A5: firstdom IDEA_Q_F(Key,n,r) = proj1 (IDEA_Q_F(Key,n,r).1) by FUNCT_7:def 6
    .= proj1 (IDEA_Q(Line(Key,r-'1+1),n)) by A4,Def18
    .= dom IDEA_Q(Line(Key,r-'1+1),n)
    .= MESSAGES by FUNCT_2:def 1;
  r = len IDEA_Q_F(Key,n,r) by Def18;
  then r in Seg len IDEA_Q_F(Key,n,r) by A2,FINSEQ_1:1;
  then
A6: r in dom IDEA_Q_F(Key,n,r) by FINSEQ_1:def 3;
  len (IDEA_Q_F(Key,n,r)) <> 0 by A1,Def18;
  then not IDEA_Q_F(Key,n,r)=<*>MESSAGES;
  then
  lastrng IDEA_Q_F(Key,n,r) = proj2 (IDEA_Q_F(Key,n,r). len (IDEA_Q_F(Key
  ,n,r))) by FUNCT_7:def 7
    .= proj2 (IDEA_Q_F(Key,n,r).r) by Def18
    .= proj2 (IDEA_Q(Line(Key,r-'r+1),n)) by A6,Def18
    .= rng IDEA_Q(Line(Key,r-'r+1),n);
  then
A7: lastrng IDEA_Q_F(Key,n,r) c= MESSAGES by RELAT_1:def 19;
  IDEA_Q_F(Key,n,r) is FuncSequence by Th39;
  hence thesis by A7,A5,FUNCT_7:def 9;
end;

theorem Th42:
  for n being non empty Element of NAT,M being FinSequence of NAT,
m,k st M = IDEA_P(k,n).m & len m >= 4 holds len M >= 4 & M.1 is_expressible_by
n & M.2 is_expressible_by n & M.3 is_expressible_by n & M.4 is_expressible_by n
proof
  let n be non empty Element of NAT, M be FinSequence of NAT,m,k;
  assume that
A1: M = IDEA_P(k,n).m and
A2: len m >= 4;
A3: len m = len IDEAoperationB(m,k,n) by Def12
    .= len IDEAoperationC(IDEAoperationB(m,k,n)) by Def13;
  M = IDEAoperationA(IDEAoperationC(IDEAoperationB(m,k,n)),k,n) by A1,Def15;
  hence thesis by A2,A3,Def11,Th26;
end;

theorem Th43:
  for n being non empty Element of NAT,lk being Element of NAT,
Key being Matrix of lk,6,NAT, r being Element of NAT holds rng compose(IDEA_P_F
  (Key,n,r),MESSAGES) c=MESSAGES & dom compose(IDEA_P_F(Key,n,r),MESSAGES) =
  MESSAGES
proof
  let n be non empty Element of NAT, lk be Element of NAT, Key be Matrix of lk
  ,6,NAT, r be Element of NAT;
A1: rng compose(IDEA_P_F(Key,n,r),MESSAGES) c= MESSAGES
  proof
    per cases;
    suppose
A2:   r<>0;
      then 0+1 < r+1 by XREAL_1:6;
      then
A3:   1 <= r by NAT_1:13;
      r = len IDEA_P_F(Key,n,r) by Def17;
      then r in Seg len IDEA_P_F(Key,n,r) by A3,FINSEQ_1:1;
      then
A4:   r in dom IDEA_P_F(Key,n,r) by FINSEQ_1:def 3;
      len (IDEA_P_F(Key,n,r)) <> 0 by A2,Def17;
      then
A5:   not IDEA_P_F(Key,n,r)=<*>MESSAGES;
      then
      lastrng IDEA_P_F(Key,n,r) = proj2 (IDEA_P_F(Key,n,r). len (IDEA_P_F
      (Key,n,r))) by FUNCT_7:def 7
        .= proj2 (IDEA_P_F(Key,n,r).r) by Def17
        .= proj2 (IDEA_P(Line(Key,r),n)) by A4,Def17
        .= rng IDEA_P(Line(Key,r),n);
      then
A6:   lastrng IDEA_P_F(Key,n,r) c= MESSAGES by RELAT_1:def 19;
      rng compose(IDEA_P_F(Key,n,r),MESSAGES) c= lastrng IDEA_P_F(Key,n,r
      ) by A5,FUNCT_7:59;
      hence thesis by A6,XBOOLE_1:1;
    end;
    suppose
      r=0;
      then len IDEA_P_F(Key,n,r) = 0 by Def17;
      then IDEA_P_F(Key,n,r) = {};
      then compose(IDEA_P_F(Key,n,r),MESSAGES) = id MESSAGES by FUNCT_7:39;
      hence thesis by RELAT_1:def 19;
    end;
  end;
A7: IDEA_P_F(Key,n,r) is FuncSequence by Th38;
  dom compose(IDEA_P_F(Key,n,r),MESSAGES) = MESSAGES
  proof
    per cases;
    suppose
      r=0;
      then len IDEA_P_F(Key,n,r) = 0 by Def17;
      then IDEA_P_F(Key,n,r) = {};
      then compose(IDEA_P_F(Key,n,r),MESSAGES) = id MESSAGES by FUNCT_7:39;
      hence thesis by FUNCT_2:52;
    end;
    suppose
A8:   r<>0;
      then 0+1 < r+1 by XREAL_1:6;
      then
A9:   1 <= r by NAT_1:13;
      r = len IDEA_P_F(Key,n,r) by Def17;
      then 1 in Seg len IDEA_P_F(Key,n,r) by A9,FINSEQ_1:1;
      then
A10:  1 in dom IDEA_P_F(Key,n,r) by FINSEQ_1:def 3;
      len (IDEA_P_F(Key,n,r)) <> 0 by A8,Def17;
      then not IDEA_P_F(Key,n,r)=<*>MESSAGES;
      then firstdom IDEA_P_F(Key,n,r) = proj1 (IDEA_P_F(Key,n,r).1) by
FUNCT_7:def 6
        .= proj1 (IDEA_P(Line(Key,1),n)) by A10,Def17
        .= dom IDEA_P(Line(Key,1),n)
        .= MESSAGES by FUNCT_2:def 1;
      hence thesis by A7,FUNCT_7:62;
    end;
  end;
  hence thesis by A1;
end;

theorem
  for n being non empty Element of NAT,lk being Element of NAT, Key
being Matrix of lk,6,NAT, r being Element of NAT holds rng compose(IDEA_Q_F(Key
,n,r),MESSAGES) c=MESSAGES & dom compose(IDEA_Q_F(Key,n,r),MESSAGES) =MESSAGES
proof
  let n be non empty Element of NAT, lk be Element of NAT, Key be Matrix of lk
  ,6,NAT, r be Element of NAT;
A1: rng compose(IDEA_Q_F(Key,n,r),MESSAGES) c= MESSAGES
  proof
    per cases;
    suppose
A2:   r<>0;
      then 0+1 < r+1 by XREAL_1:6;
      then
A3:   1 <= r by NAT_1:13;
      r = len IDEA_Q_F(Key,n,r) by Def18;
      then r in Seg len IDEA_Q_F(Key,n,r) by A3,FINSEQ_1:1;
      then
A4:   r in dom IDEA_Q_F(Key,n,r) by FINSEQ_1:def 3;
      len (IDEA_Q_F(Key,n,r)) <> 0 by A2,Def18;
      then
A5:   not IDEA_Q_F(Key,n,r)=<*>MESSAGES;
      then
      lastrng IDEA_Q_F(Key,n,r) = proj2 (IDEA_Q_F(Key,n,r). len (IDEA_Q_F
      (Key,n,r))) by FUNCT_7:def 7
        .= proj2 (IDEA_Q_F(Key,n,r).r) by Def18
        .= proj2 (IDEA_Q(Line(Key,r-'r+1),n)) by A4,Def18
        .= rng IDEA_Q(Line(Key,r-'r+1),n);
      then
A6:   lastrng IDEA_Q_F(Key,n,r) c= MESSAGES by RELAT_1:def 19;
      rng compose(IDEA_Q_F(Key,n,r),MESSAGES) c= lastrng IDEA_Q_F(Key,n,r
      ) by A5,FUNCT_7:59;
      hence thesis by A6,XBOOLE_1:1;
    end;
    suppose
      r=0;
      then len IDEA_Q_F(Key,n,r) = 0 by Def18;
      then IDEA_Q_F(Key,n,r) = {};
      then compose(IDEA_Q_F(Key,n,r),MESSAGES) = id MESSAGES by FUNCT_7:39;
      hence thesis by RELAT_1:def 19;
    end;
  end;
A7: IDEA_Q_F(Key,n,r) is FuncSequence by Th39;
  dom compose(IDEA_Q_F(Key,n,r),MESSAGES) = MESSAGES
  proof
    per cases;
    suppose
      r=0;
      then len IDEA_Q_F(Key,n,r) = 0 by Def18;
      then IDEA_Q_F(Key,n,r) = {};
      then compose(IDEA_Q_F(Key,n,r),MESSAGES) = id MESSAGES by FUNCT_7:39;
      hence thesis by FUNCT_2:52;
    end;
    suppose
A8:   r<>0;
      then 0+1 < r+1 by XREAL_1:6;
      then
A9:   1 <= r by NAT_1:13;
      r = len IDEA_Q_F(Key,n,r) by Def18;
      then 1 in Seg len IDEA_Q_F(Key,n,r) by A9,FINSEQ_1:1;
      then
A10:  1 in dom IDEA_Q_F(Key,n,r) by FINSEQ_1:def 3;
      len (IDEA_Q_F(Key,n,r)) <> 0 by A8,Def18;
      then not IDEA_Q_F(Key,n,r)=<*>MESSAGES;
      then firstdom IDEA_Q_F(Key,n,r) = proj1 (IDEA_Q_F(Key,n,r).1) by
FUNCT_7:def 6
        .= proj1 (IDEA_Q(Line(Key,r-'1+1),n)) by A10,Def18
        .= dom IDEA_Q(Line(Key,r-'1+1),n)
        .= MESSAGES by FUNCT_2:def 1;
      hence thesis by A7,FUNCT_7:62;
    end;
  end;
  hence thesis by A1;
end;

theorem Th45:
  for n being non empty Element of NAT,lk being Element of NAT,
Key being Matrix of lk,6,NAT, r being Element of NAT,M being FinSequence of NAT
  ,m st M = compose(IDEA_P_F(Key,n,r),MESSAGES).m & len m >= 4 & m.1
  is_expressible_by n & m.2 is_expressible_by n & m.3 is_expressible_by n & m.4
  is_expressible_by n holds len M >= 4 & M.1 is_expressible_by n & M.2
  is_expressible_by n & M.3 is_expressible_by n & M.4 is_expressible_by n
proof
  let n be non empty Element of NAT, lk be Element of NAT, Key be Matrix of lk
  ,6,NAT, r be Element of NAT, M be FinSequence of NAT,m;
  assume that
A1: M = compose(IDEA_P_F(Key,n,r),MESSAGES).m and
A2: len m >= 4 and
A3: m.1 is_expressible_by n & m.2 is_expressible_by n & m.3
  is_expressible_by n & m.4 is_expressible_by n;
A4: m in MESSAGES by FINSEQ_1:def 11;
  per cases;
  suppose
    r = 0;
    then len IDEA_P_F(Key,n,r) = 0 by Def17;
    then IDEA_P_F(Key,n,r) = {};
    then M = (id MESSAGES).m by A1,FUNCT_7:39
      .= m by A4,FUNCT_1:18;
    hence thesis by A2,A3;
  end;
  suppose
A5: r <> 0;
    consider r1 being Integer such that
A6: r1=r-1;
    defpred P[Element of NAT] means for M being FinSequence of NAT st M =
    compose(IDEA_P_F(Key,n,$1),MESSAGES).m holds len M >= 4;
A7: m in MESSAGES by FINSEQ_1:def 11;
A8: for k being Element of NAT st P[k] holds P[k + 1]
    proof
      let k be Element of NAT;
A9:   dom compose(IDEA_P_F(Key,n,k),MESSAGES) = MESSAGES by Th43;
A10:  rng compose(IDEA_P_F(Key,n,k),MESSAGES) c= MESSAGES by Th43;
      then
      rng compose(IDEA_P_F(Key,n,k),MESSAGES) c= dom IDEA_P(Line(Key,(k+1
      )),n) by FUNCT_2:def 1;
      then
A11:  dom (IDEA_P(Line(Key,(k+1)),n)* compose(IDEA_P_F(Key,n,k),MESSAGES)
      )= MESSAGES by A9,RELAT_1:27;
      compose(IDEA_P_F(Key,n,k),MESSAGES).m in rng(compose(IDEA_P_F(Key,n
      ,k),MESSAGES)) by A7,A9,FUNCT_1:def 3;
      then reconsider
      M1 = compose(IDEA_P_F(Key,n,k),MESSAGES).m as FinSequence of
      NAT by A10,FINSEQ_1:def 11;
      assume P[k];
      then
A12:  len M1 >= 4;
      let M be FinSequence of NAT;
      assume M = compose(IDEA_P_F(Key,n,k+1),MESSAGES).m;
      then M = compose(IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>,
      MESSAGES).m by Th36;
      then
      M = (IDEA_P(Line(Key,(k+1)),n)* compose(IDEA_P_F(Key,n,k),MESSAGES)
      ).m by FUNCT_7:41;
      then
      M = IDEA_P(Line(Key,(k+1)),n). (compose(IDEA_P_F(Key,n,k),MESSAGES)
      .m) by A7,A11,FUNCT_1:12;
      hence thesis by A12,Th42;
    end;
    1 <= r by A5,NAT_1:14;
    then 1 - 1 <= r - 1 by XREAL_1:9;
    then reconsider r1 as Element of NAT by A6,INT_1:3;
    dom compose(IDEA_P_F(Key,n,r1),MESSAGES) = MESSAGES by Th43;
    then
A13: compose(IDEA_P_F(Key,n,r1),MESSAGES).m in rng(compose(IDEA_P_F(Key,n,
    r1),MESSAGES)) by A4,FUNCT_1:def 3;
    rng compose(IDEA_P_F(Key,n,r1),MESSAGES) c= MESSAGES by Th43;
    then reconsider
    M1 = compose(IDEA_P_F(Key,n,r1),MESSAGES).m as FinSequence of
    NAT by A13,FINSEQ_1:def 11;
A14: P[0]
    proof
      let M be FinSequence of NAT;
      len IDEA_P_F(Key,n,0) = 0 by Def17;
      then
A15:  IDEA_P_F(Key,n,0) = {};
      assume M = compose(IDEA_P_F(Key,n,0),MESSAGES).m;
      then M = (id MESSAGES).m by A15,FUNCT_7:39
        .= m by A7,FUNCT_1:18;
      hence thesis by A2;
    end;
    for k being Element of NAT holds P[k] from NAT_1:sch 1(A14,A8);
    then
A16: len M1 >= 4;
    IDEA_P_F(Key,n,(r1+1)) = IDEA_P_F(Key,n,r1)^<* IDEA_P(Line(Key,(r1+1)
    ),n) *> by Th36;
    then
A17: compose(IDEA_P_F(Key,n,r),MESSAGES) = IDEA_P(Line(Key,r),n)*compose(
    IDEA_P_F(Key,n,r1),MESSAGES) by A6,FUNCT_7:41;
    then
    m in dom(IDEA_P(Line(Key,r),n)* compose(IDEA_P_F(Key,n,r1),MESSAGES))
    by A4,Th43;
    then
    M = IDEA_P(Line(Key,r),n).(compose(IDEA_P_F(Key,n,r1),MESSAGES).m) by A1
,A17,FUNCT_1:12;
    hence thesis by A16,Th42;
  end;
end;

begin :: Modeling of IDEA Cryptogram
:: IDEA encryption algorithm is as follows:
::     IDEA_PS -> IDEA_P -> IDEA_P -> ... -> IDEA_P -> IDEA_PE
:: IDEA decryption algorithm is as follows:
::     IDEA_QE -> IDEA_Q -> IDEA_Q -> ... -> IDEA_Q -> IDEA_QS
:: Theorem 49 ensures that the ciphertext that is encrypted by IDEA
:: encryption algorithm can be decrypted by IDEA decryption algorithm.

theorem Th46:
  for n being non empty Element of NAT,lk being Element of NAT,
  Key1,Key2 being Matrix of lk,6,NAT, r being Element of NAT,m st lk >= r & 2
  to_power(n)+1 is prime & len m >= 4 & m.1 is_expressible_by n & m.2
is_expressible_by n & m.3 is_expressible_by n & m.4 is_expressible_by n & (for
  i being Element of NAT holds i <= r implies Key1*(i,1) is_expressible_by n &
  Key1*(i,2) is_expressible_by n & Key1*(i,3) is_expressible_by n & Key1*(i,4)
  is_expressible_by n & Key1*(i,5) is_expressible_by n & Key1*(i,6)
  is_expressible_by n & Key2*(i,1) is_expressible_by n & Key2*(i,2)
  is_expressible_by n & Key2*(i,3) is_expressible_by n & Key2*(i,4)
  is_expressible_by n & Key2*(i,5) is_expressible_by n & Key2*(i,6)
  is_expressible_by n & Key2*(i,1)=INV_MOD(Key1*(i,1),n) & Key2*(i,2)=NEG_MOD(
Key1* (i,3),n) & Key2*(i,3)=NEG_MOD(Key1*(i,2),n) & Key2*(i,4)=INV_MOD(Key1* (i
,4),n) & Key1*(i,5)=Key2*(i,5) & Key1*(i,6)=Key2*(i,6)) holds compose(IDEA_P_F(
  Key1,n,r)^IDEA_Q_F(Key2,n,r),MESSAGES).m = m
proof
  let n be non empty Element of NAT, lk be Element of NAT;
  let Key1,Key2 be Matrix of lk,6,NAT;
  for r being Element of NAT st lk >= r & 2 to_power(n)+1 is prime & len m
  >= 4 & m.1 is_expressible_by n & m.2 is_expressible_by n & m.3
  is_expressible_by n & m.4 is_expressible_by n & (for i being Element of NAT
  holds i <= r implies Key1*(i,1) is_expressible_by n & Key1*(i,2)
  is_expressible_by n & Key1*(i,3) is_expressible_by n & Key1*(i,4)
  is_expressible_by n & Key1*(i,5) is_expressible_by n & Key1*(i,6)
  is_expressible_by n & Key2*(i,1) is_expressible_by n & Key2*(i,2)
  is_expressible_by n & Key2*(i,3) is_expressible_by n & Key2*(i,4)
  is_expressible_by n & Key2*(i,5) is_expressible_by n & Key2*(i,6)
is_expressible_by n & Key2*(i,1) = INV_MOD(Key1*(i,1),n) & Key2*(i,2) = NEG_MOD
(Key1*(i,3),n) & Key2*(i,3) = NEG_MOD(Key1*(i,2),n) & Key2*(i,4) = INV_MOD(Key1
  *(i,4),n) & Key1*(i,5) = Key2*(i,5) & Key1*(i,6) = Key2*(i,6)) holds compose(
  IDEA_P_F(Key1,n,r)^IDEA_Q_F(Key2,n,r), MESSAGES).m = m
  proof
    defpred P[Element of NAT] means lk >= $1 & 2 to_power(n)+1 is prime & len
    m >= 4 & m.1 is_expressible_by n & m.2 is_expressible_by n & m.3
    is_expressible_by n & m.4 is_expressible_by n & (for i being Element of NAT
    holds i <= $1 implies Key1*(i,1) is_expressible_by n & Key1*(i,2)
    is_expressible_by n & Key1*(i,3) is_expressible_by n & Key1*(i,4)
    is_expressible_by n & Key1*(i,5) is_expressible_by n & Key1*(i,6)
    is_expressible_by n & Key2*(i,1) is_expressible_by n & Key2*(i,2)
    is_expressible_by n & Key2*(i,3) is_expressible_by n & Key2*(i,4)
    is_expressible_by n & Key2*(i,5) is_expressible_by n & Key2*(i,6)
is_expressible_by n & Key2*(i,1) = INV_MOD(Key1*(i,1),n) & Key2*(i,2) = NEG_MOD
(Key1*(i,3),n) & Key2*(i,3) = NEG_MOD(Key1*(i,2),n) & Key2*(i,4) = INV_MOD(Key1
*(i,4),n) & Key1*(i,5) = Key2*(i,5) & Key1*(i,6) = Key2*(i,6)) implies compose(
    IDEA_P_F(Key1,n,$1)^IDEA_Q_F(Key2,n,$1),MESSAGES).m = m;
A1: len IDEA_P_F(Key1,n,0) = 0 by Def17;
A2: for k being Element of NAT st P[k] holds P[k + 1]
    proof
      let k be Element of NAT;
      assume
A3:   P[k];
      consider k1 being Element of NAT such that
A4:   k1 = k+1;
A5:   dom compose(IDEA_P_F(Key1,n,k),MESSAGES) = MESSAGES by Th43;
A6:   rng compose(IDEA_P_F(Key1,n,k),MESSAGES) c= MESSAGES by Th43;
A7:   m in MESSAGES by FINSEQ_1:def 11;
      then
      compose(IDEA_P_F(Key1,n,k),MESSAGES).m in rng(compose(IDEA_P_F(Key1
      ,n,k),MESSAGES)) by A5,FUNCT_1:def 3;
      then reconsider
      M = compose(IDEA_P_F(Key1,n,k),MESSAGES).m as FinSequence of
      NAT by A6,FINSEQ_1:def 11;
      assume that
A8:   lk >= k+1 and
A9:   2 to_power(n)+1 is prime and
A10:  len m >= 4 & m.1 is_expressible_by n & m.2 is_expressible_by n
      & m.3 is_expressible_by n & m.4 is_expressible_by n and
A11:  for i being Element of NAT holds i <= k+1 implies Key1*(i,1)
      is_expressible_by n & Key1*(i,2) is_expressible_by n & Key1*(i,3)
      is_expressible_by n & Key1*(i,4) is_expressible_by n & Key1*(i,5)
      is_expressible_by n & Key1*(i,6) is_expressible_by n & Key2*(i,1)
      is_expressible_by n & Key2*(i,2) is_expressible_by n & Key2*(i,3)
      is_expressible_by n & Key2*(i,4) is_expressible_by n & Key2*(i,5)
is_expressible_by n & Key2*(i,6) is_expressible_by n & Key2*(i,1) = INV_MOD(
Key1*(i,1),n) & Key2*(i,2) = NEG_MOD(Key1*(i,3),n) & Key2*(i,3) = NEG_MOD(Key1*
(i,2),n) & Key2*(i,4) = INV_MOD(Key1*(i,4),n) & Key1*(i,5) = Key2*(i,5) & Key1*
      (i,6) = Key2*(i,6);
A12:  len M >= 4 & M.1 is_expressible_by n by A10,Th45;
A13:  width Key1 = 6 by A8,MATRIX_1:23;
      then 1 in Seg(width Key1) by FINSEQ_1:1;
      then
A14:  Line(Key1,(k+1)).1 = Key1*(k1,1) by A4,MATRIX_1:def 7;
      then
A15:  Line(Key1,(k+1)).1 is_expressible_by n by A11,A4;
A16:  width Key2 = 6 by A8,MATRIX_1:23;
      then 5 in Seg(width Key2) by FINSEQ_1:1;
      then
A17:  Line(Key2,(k+1)).5 = Key2*(k1,5) by A4,MATRIX_1:def 7;
      3 in Seg(width Key1) by A13,FINSEQ_1:1;
      then
A18:  Line(Key1,(k+1)).3 = Key1*(k1,3) by A4,MATRIX_1:def 7;
      then
A19:  Line(Key1,(k+1)).3 is_expressible_by n by A11,A4;
      2 in Seg(width Key1) by A13,FINSEQ_1:1;
      then
A20:  Line(Key1,(k+1)).2 = Key1*(k1,2) by A4,MATRIX_1:def 7;
      then
A21:  Line(Key1,(k+1)).2 is_expressible_by n by A11,A4;
      3 in Seg(width Key2) by A16,FINSEQ_1:1;
      then Line(Key2,(k+1)).3 = Key2*(k1,3) by A4,MATRIX_1:def 7;
      then
A22:  Line(Key2,(k+1)).3 = NEG_MOD(Line(Key1,(k+1)).2,n) by A11,A4,A20;
      2 in Seg(width Key2) by A16,FINSEQ_1:1;
      then Line(Key2,(k+1)).2 = Key2*(k1,2) by A4,MATRIX_1:def 7;
      then
A23:  Line(Key2,(k+1)).2 = NEG_MOD(Line(Key1,(k+1)).3,n) by A11,A4,A18;
      5 in Seg(width Key1) by A13,FINSEQ_1:1;
      then Line(Key1,(k+1)).5 = Key1*(k1,5) by A4,MATRIX_1:def 7;
      then
A24:  Line(Key2,(k+1)).5 = Line(Key1,(k+1)).5 by A11,A4,A17;
A25:  M.4 is_expressible_by n by A10,Th45;
A26:  M.2 is_expressible_by n & M.3 is_expressible_by n by A10,Th45;
      4 in Seg(width Key1) by A13,FINSEQ_1:1;
      then
A27:  Line(Key1,(k+1)).4 = Key1*(k1,4) by A4,MATRIX_1:def 7;
      then
A28:  Line(Key1,(k+1)).4 is_expressible_by n by A11,A4;
      4 in Seg(width Key2) by A16,FINSEQ_1:1;
      then Line(Key2,(k+1)).4 = Key2*(k1,4) by A4,MATRIX_1:def 7;
      then
A29:  Line(Key2,(k+1)).4 = INV_MOD(Line(Key1,(k+1)).4,n) by A11,A4,A27;
      6 in Seg(width Key2) by A16,FINSEQ_1:1;
      then
A30:  Line(Key2,(k+1)).6 = Key2*(k1,6) by A4,MATRIX_1:def 7;
      6 in Seg(width Key1) by A13,FINSEQ_1:1;
      then Line(Key1,(k+1)).6 = Key1*(k1,6) by A4,MATRIX_1:def 7;
      then
A31:  Line(Key2,(k+1)).6 = Line(Key1,(k+1)).6 by A11,A4,A30;
      dom (IDEA_Q(Line(Key2,(k+1)),n) * IDEA_P(Line(Key1,(k+1)),n)) =
      MESSAGES by FUNCT_2:def 1;
      then
A32:  dom ((IDEA_Q(Line(Key2,(k+1)),n) * IDEA_P(Line(Key1,(k+1)),n))*
      compose( IDEA_P_F(Key1,n,k),MESSAGES))=MESSAGES by A6,A5,RELAT_1:27;
      rng compose(IDEA_P_F(Key1,n,k)^ (<*IDEA_P(Line(Key1,(k+1)),n)*>^ <*
IDEA_Q(Line(Key2,k+1),n)*>),MESSAGES) = rng compose(IDEA_P_F(Key1,n,k)^ <*
      IDEA_P(Line(Key1,(k+1)),n)*>^ <*IDEA_Q(Line(Key2,k+1),n)*>,MESSAGES) by
FINSEQ_1:32
        .= rng (IDEA_Q(Line(Key2,k+1),n)* compose(IDEA_P_F(Key1,n,k)^ <*
      IDEA_P(Line(Key1,(k+1)),n)*>,MESSAGES)) by FUNCT_7:41;
      then
A33:  rng compose(IDEA_P_F(Key1,n,k)^ (<*IDEA_P(Line(Key1,(k+1)),n)*>^ <*
      IDEA_Q( Line(Key2,k+1),n)*>),MESSAGES) c= MESSAGES by RELAT_1:def 19;
      1 in Seg(width Key2) by A16,FINSEQ_1:1;
      then Line(Key2,(k+1)).1 = Key2*(k1,1) by A4,MATRIX_1:def 7;
      then
A34:  Line(Key2,(k+1)).1 = INV_MOD(Line(Key1,(k+1)).1,n) by A11,A4,A14;
A35:  k+1 >= k by NAT_1:11;
A36:  for i being Element of NAT holds i <= k implies Key1*(i,1)
      is_expressible_by n & Key1* (i,2) is_expressible_by n & Key1*(i,3)
      is_expressible_by n & Key1* (i,4) is_expressible_by n & Key1*(i,5)
      is_expressible_by n & Key1* (i,6) is_expressible_by n & Key2*(i,1)
      is_expressible_by n & Key2* (i,2) is_expressible_by n & Key2*(i,3)
      is_expressible_by n & Key2* (i,4) is_expressible_by n & Key2*(i,5)
is_expressible_by n & Key2* (i,6) is_expressible_by n & Key2*(i,1) = INV_MOD(
Key1*(i,1),n) & Key2*(i,2) = NEG_MOD(Key1*(i,3),n) & Key2*(i,3) = NEG_MOD(Key1*
(i,2),n) & Key2*(i,4) = INV_MOD(Key1*(i,4),n) & Key1*(i,5) = Key2*(i,5) & Key1*
      (i,6) = Key2*(i,6)
      proof
        let i be Element of NAT;
        assume i <= k;
        then i <= k+1 by A35,XXREAL_0:2;
        hence thesis by A11;
      end;
      compose(IDEA_P_F(Key1,n,(k+1))^IDEA_Q_F(Key2,n,(k+1)), MESSAGES).m
= compose((IDEA_P_F(Key1,n,k)^<* IDEA_P(Line(Key1,(k+1)),n) *>) ^IDEA_Q_F(Key2,
      n,(k+1)),MESSAGES).m by Th36
        .= compose((IDEA_P_F(Key1,n,k)^<*IDEA_P(Line(Key1,(k+1)),n)*>)^ (<*
      IDEA_Q(Line(Key2,(k+1)),n)*>^IDEA_Q_F(Key2,n,k)),MESSAGES).m by Th37
        .= compose(IDEA_P_F(Key1,n,k)^<*IDEA_P(Line(Key1,(k+1)),n)*>^ <*
IDEA_Q(Line(Key2,(k+1)),n)*>^IDEA_Q_F(Key2,n,k),MESSAGES).m by FINSEQ_1:32
        .= compose(IDEA_P_F(Key1,n,k)^ (<*IDEA_P(Line(Key1,(k+1)),n)*>^<*
IDEA_Q(Line(Key2,(k+1)),n)*>)^ IDEA_Q_F(Key2,n,k),MESSAGES).m by FINSEQ_1:32
        .=(compose(IDEA_Q_F(Key2,n,k),MESSAGES) * compose(IDEA_P_F(Key1,n,k)
^ (<*IDEA_P(Line(Key1,(k+1)),n)*>^<*IDEA_Q(Line(Key2,(k+1)),n)*>) ,MESSAGES)).m
      by A33,FUNCT_7:48
        .=(compose(IDEA_Q_F(Key2,n,k),MESSAGES) * (compose(<*IDEA_P(Line(
Key1,(k+1)),n)*>^ <*IDEA_Q(Line(Key2,(k+1)),n)*>,MESSAGES) * compose(IDEA_P_F(
      Key1,n,k),MESSAGES))).m by A6,FUNCT_7:48
        .=(compose(IDEA_Q_F(Key2,n,k),MESSAGES) * (compose(<*IDEA_P(Line(
Key1,(k+1)),n), IDEA_Q(Line(Key2,(k+1)),n)*>,MESSAGES) * compose(IDEA_P_F(Key1,
      n,k),MESSAGES))).m by FINSEQ_1:def 9
        .=(compose(IDEA_Q_F(Key2,n,k),MESSAGES) * ((IDEA_Q(Line(Key2,(k+1)),
n) * IDEA_P(Line(Key1,(k+1)),n) * id MESSAGES) * compose(IDEA_P_F(Key1,n,k),
      MESSAGES))).m by FUNCT_7:51
        .=(compose(IDEA_Q_F(Key2,n,k),MESSAGES) * ((IDEA_Q(Line(Key2,(k+1)),
n) * IDEA_P(Line(Key1,(k+1)),n))* compose(IDEA_P_F(Key1,n,k),MESSAGES))).m by
FUNCT_2:17
        .= compose(IDEA_Q_F(Key2,n,k),MESSAGES). (((IDEA_Q(Line(Key2,(k+1)),
n) * IDEA_P(Line(Key1,(k+1)),n))* compose(IDEA_P_F(Key1,n,k),MESSAGES)).m) by
A32,A7,FUNCT_1:13
        .= compose(IDEA_Q_F(Key2,n,k),MESSAGES). ((IDEA_Q(Line(Key2,(k+1)),n
) * IDEA_P(Line(Key1,(k+1)),n)). ((compose(IDEA_P_F(Key1,n,k),MESSAGES)).m))
by A5,A7,FUNCT_1:13
        .= compose(IDEA_Q_F(Key2,n,k),MESSAGES). (compose(IDEA_P_F(Key1,n,k)
,MESSAGES).m) by A9,A12,A26,A25,A15,A21,A19,A28,A34,A23,A22,A29,A24,A31,Th33
        .=(compose(IDEA_Q_F(Key2,n,k),MESSAGES) * compose(IDEA_P_F(Key1,n,k)
      ,MESSAGES)).m by A5,A7,FUNCT_1:13
        .= m by A3,A8,A9,A10,A35,A36,A6,FUNCT_7:48,XXREAL_0:2;
      hence thesis;
    end;
    len IDEA_Q_F(Key2,n,0) = 0 by Def18;
    then IDEA_Q_F(Key2,n,0) = {};
    then IDEA_P_F(Key1,n,0)^IDEA_Q_F(Key2,n,0) = IDEA_P_F(Key1,n,0) by
FINSEQ_1:34
      .= {} by A1;
    then
    m in MESSAGES & compose(IDEA_P_F(Key1,n,0)^IDEA_Q_F(Key2,n,0),MESSAGES
    ) = id MESSAGES by FINSEQ_1:def 11,FUNCT_7:39;
    then
A37: P[0] by FUNCT_1:18;
    thus for k being Element of NAT holds P[k] from NAT_1:sch 1(A37, A2);
  end;
  hence thesis;
end;

theorem
  for n being non empty Element of NAT,lk being Element of NAT, Key1,
  Key2 being Matrix of lk,6,NAT, r being Element of NAT,ks1,ks2,ke1,ke2 being
  FinSequence of NAT,m st lk >= r & 2 to_power(n)+1 is prime & len m >= 4 & m.1
  is_expressible_by n & m.2 is_expressible_by n & m.3 is_expressible_by n & m.4
is_expressible_by n & (for i being Element of NAT holds i <= r implies Key1*(i,
  1) is_expressible_by n & Key1*(i,2) is_expressible_by n & Key1*(i,3)
  is_expressible_by n & Key1*(i,4) is_expressible_by n & Key1*(i,5)
  is_expressible_by n & Key1*(i,6) is_expressible_by n & Key2*(i,1)
  is_expressible_by n & Key2*(i,2) is_expressible_by n & Key2*(i,3)
  is_expressible_by n & Key2*(i,4) is_expressible_by n & Key2*(i,5)
is_expressible_by n & Key2*(i,6) is_expressible_by n & Key2*(i,1)=INV_MOD(Key1*
(i,1),n) & Key2*(i,2)=NEG_MOD(Key1* (i,3),n) & Key2*(i,3)=NEG_MOD(Key1*(i,2),n)
& Key2*(i,4)=INV_MOD(Key1* (i,4),n) & Key1*(i,5)=Key2*(i,5) & Key1*(i,6)=Key2*(
  i,6))& ks1.1 is_expressible_by n & ks1.2 is_expressible_by n & ks1.3
  is_expressible_by n & ks1.4 is_expressible_by n & ks2.1 = INV_MOD(ks1.1,n) &
ks2.2 = NEG_MOD(ks1.2,n) & ks2.3 = NEG_MOD(ks1.3,n) & ks2.4 = INV_MOD(ks1.4,n)
  & ke1.1 is_expressible_by n & ke1.2 is_expressible_by n & ke1.3
  is_expressible_by n & ke1.4 is_expressible_by n & ke2.1 = INV_MOD(ke1.1,n) &
ke2.2 = NEG_MOD(ke1.2,n) & ke2.3 = NEG_MOD(ke1.3,n) & ke2.4 = INV_MOD(ke1.4,n)
& ke2.5 = ke1.5 & ke2.6 = ke1.6 holds (IDEA_QS(ks2,n)*(compose(IDEA_Q_F(Key2,n,
  r),MESSAGES)* (IDEA_QE(ke2,n)*(IDEA_PE(ke1,n)*(compose(IDEA_P_F(Key1,n,r),
  MESSAGES)* IDEA_PS(ks1,n)))))).m = m
proof
  let n be non empty Element of NAT, lk be Element of NAT, Key1,Key2 be Matrix
  of lk,6,NAT, r be Element of NAT, ks1,ks2,ke1,ke2 be FinSequence of NAT,m;
  assume that
A1: lk >= r and
A2: 2 to_power(n)+1 is prime and
A3: len m >= 4 and
A4: m.1 is_expressible_by n & m.2 is_expressible_by n & m.3
  is_expressible_by n & m.4 is_expressible_by n and
A5: for i being Element of NAT holds i <= r implies Key1*(i,1)
  is_expressible_by n & Key1*(i,2) is_expressible_by n & Key1*(i,3)
  is_expressible_by n & Key1*(i,4) is_expressible_by n & Key1*(i,5)
  is_expressible_by n & Key1*(i,6) is_expressible_by n & Key2*(i,1)
  is_expressible_by n & Key2*(i,2) is_expressible_by n & Key2*(i,3)
  is_expressible_by n & Key2*(i,4) is_expressible_by n & Key2*(i,5)
  is_expressible_by n & Key2*(i,6) is_expressible_by n & Key2*(i,1) = INV_MOD(
Key1*(i,1),n) & Key2*(i,2) = NEG_MOD(Key1*(i,3),n) & Key2*(i,3) = NEG_MOD(Key1*
(i,2),n) & Key2*(i,4) = INV_MOD(Key1*(i,4),n) & Key1*(i,5) = Key2*(i,5) & Key1*
  (i,6) = Key2*(i,6) and
A6: ks1.1 is_expressible_by n & ks1.2 is_expressible_by n & ks1.3
  is_expressible_by n & ks1.4 is_expressible_by n & ks2.1 = INV_MOD(ks1.1,n) &
ks2.2 = NEG_MOD(ks1.2,n) & ks2.3 = NEG_MOD( ks1.3,n) & ks2.4 = INV_MOD(ks1. 4,n
  ) and
A7: ke1.1 is_expressible_by n & ke1.2 is_expressible_by n & ke1.3
  is_expressible_by n & ke1.4 is_expressible_by n & ke2.1 = INV_MOD(ke1.1,n) &
ke2.2 = NEG_MOD(ke1.2,n) & ke2.3 = NEG_MOD( ke1.3,n) & ke2.4 = INV_MOD(ke1. 4,n
  ) & ke2.5 = ke1.5 & ke2.6 = ke1.6;
A8: m in MESSAGES by FINSEQ_1:def 11;
  then IDEA_PS(ks1,n).m in MESSAGES by FUNCT_2:5;
  then reconsider m1 = IDEA_PS(ks1,n).m as FinSequence of NAT by
FINSEQ_1:def 11;
A9: m1 in MESSAGES by FINSEQ_1:def 11;
A10: len m1 = len IDEAoperationA(m,ks1,n) by Def19
    .= len m by Def11;
  m1.4 = IDEAoperationA(m,ks1,n).4 by Def19;
  then
A11: m1.4 is_expressible_by n by A3,Th26;
  m1.3 = IDEAoperationA(m,ks1,n).3 by Def19;
  then
A12: m1.3 is_expressible_by n by A3,Th26;
  m1.2 = IDEAoperationA(m,ks1,n).2 by Def19;
  then
A13: m1.2 is_expressible_by n by A3,Th26;
  m1.1 = IDEAoperationA(m,ks1,n).1 by Def19;
  then
A14: m1.1 is_expressible_by n by A3,Th26;
  per cases;
  suppose
A15: r = 0;
    then len IDEA_Q_F(Key2,n,r) = 0 by Def18;
    then
A16: IDEA_Q_F(Key2,n,r) = {};
    len IDEA_P_F(Key1,n,r) = 0 by A15,Def17;
    then IDEA_P_F(Key1,n,r) = {};
    hence
    (IDEA_QS(ks2,n)*(compose(IDEA_Q_F(Key2,n,r),MESSAGES)* (IDEA_QE(ke2,n
)*(IDEA_PE(ke1,n)*(compose(IDEA_P_F(Key1,n,r),MESSAGES)* IDEA_PS(ks1,n)))))).m
    =(IDEA_QS(ks2,n)*(compose({},MESSAGES)* (IDEA_QE(ke2,n)*(IDEA_PE(ke1,n)*(
    compose({},MESSAGES)* IDEA_PS(ks1,n)))))).m by A16
      .=(IDEA_QS(ks2,n)*((id MESSAGES)* (IDEA_QE(ke2,n)*(IDEA_PE(ke1,n)*(
    compose({},MESSAGES)* IDEA_PS(ks1,n)))))).m by FUNCT_7:39
      .=(IDEA_QS(ks2,n)*((id MESSAGES)* (IDEA_QE(ke2,n)*(IDEA_PE(ke1,n)*((id
    MESSAGES)* IDEA_PS(ks1,n)))))).m by FUNCT_7:39
      .=(IDEA_QS(ks2,n)*((IDEA_QE(ke2,n)*(IDEA_PE(ke1,n)*((id MESSAGES)*
    IDEA_PS(ks1,n)))))).m by FUNCT_2:17
      .=(IDEA_QS(ks2,n)*(IDEA_QE(ke2,n)* (IDEA_PE(ke1,n)*IDEA_PS(ks1,n)))).m
    by FUNCT_2:17
      .=IDEA_QS(ks2,n).((IDEA_QE(ke2,n)*(IDEA_PE(ke1,n)* IDEA_PS(ks1,n))).m)
    by A8,FUNCT_2:15
      .=IDEA_QS(ks2,n).(IDEA_QE(ke2,n).((IDEA_PE(ke1,n)* IDEA_PS(ks1,n)).m))
    by A8,FUNCT_2:15
      .=IDEA_QS(ks2,n).(IDEA_QE(ke2,n).(IDEA_PE(ke1,n).m1)) by A8,FUNCT_2:15
      .=IDEA_QS(ks2,n).((IDEA_QE(ke2,n)*IDEA_PE(ke1,n)).m1) by A9,FUNCT_2:15
      .=IDEA_QS(ks2,n).(IDEA_PS(ks1,n).m) by A2,A3,A7,A10,A14,A13,A12,A11,Th35
      .=(IDEA_QS(ks2,n)*IDEA_PS(ks1,n)).m by A8,FUNCT_2:15
      .= m by A2,A3,A4,A6,Th34;
  end;
  suppose
A17: r <> 0;
    then
A18: IDEA_P_F(Key1,n,r) is FuncSequence of MESSAGES,MESSAGES by Th40;
    then
A19: firstdom IDEA_P_F(Key1,n,r) = MESSAGES by FUNCT_7:def 9;
    then
A20: dom compose(IDEA_P_F(Key1,n,r),MESSAGES) = MESSAGES by A18,FUNCT_7:62;
    IDEA_P_F(Key1,n,r) = {} implies rng compose(IDEA_P_F(Key1,n,r),
    MESSAGES) = {} by A19,FUNCT_7:def 6;
    then
A21: rng compose(IDEA_P_F(Key1,n,r),MESSAGES) c= lastrng IDEA_P_F(Key1,n,r
    ) by FUNCT_7:59,XBOOLE_1:2;
    lastrng IDEA_P_F(Key1,n,r) c= MESSAGES by A18,FUNCT_7:def 9;
    then rng compose(IDEA_P_F(Key1,n,r),MESSAGES) c= MESSAGES by A21,XBOOLE_1:1
;
    then reconsider
    PF=compose(IDEA_P_F(Key1,n,r),MESSAGES) as Function of MESSAGES
    ,MESSAGES by A20,FUNCT_2:def 1,RELSET_1:4;
A22: rng PF c= MESSAGES by RELAT_1:def 19;
    PF.m1 in MESSAGES by A9,FUNCT_2:5;
    then reconsider m2 = PF.m1 as FinSequence of NAT by FINSEQ_1:def 11;
A23: len m2 >= 4 & m2.1 is_expressible_by n by A3,A10,A14,A13,A12,A11,Th45;
A24: IDEA_Q_F(Key2,n,r) is FuncSequence of MESSAGES,MESSAGES by A17,Th41;
    then
A25: firstdom IDEA_Q_F(Key2,n,r) = MESSAGES by FUNCT_7:def 9;
    then
A26: dom compose(IDEA_Q_F(Key2,n,r),MESSAGES) = MESSAGES by A24,FUNCT_7:62;
    IDEA_Q_F(Key2,n,r) = {} implies rng compose(IDEA_Q_F(Key2,n,r),
    MESSAGES) = {} by A25,FUNCT_7:def 6;
    then
A27: rng compose(IDEA_Q_F(Key2,n,r),MESSAGES) c= lastrng IDEA_Q_F(Key2,n,r
    ) by FUNCT_7:59,XBOOLE_1:2;
    lastrng IDEA_Q_F(Key2,n,r) c= MESSAGES by A24,FUNCT_7:def 9;
    then rng compose(IDEA_Q_F(Key2,n,r),MESSAGES) c= MESSAGES by A27,XBOOLE_1:1
;
    then reconsider
    QF=compose(IDEA_Q_F(Key2,n,r),MESSAGES) as Function of MESSAGES
    ,MESSAGES by A26,FUNCT_2:def 1,RELSET_1:4;
A28: m2 in MESSAGES by FINSEQ_1:def 11;
A29: QF.(PF.m1) = (QF*PF).m1 by A9,FUNCT_2:15
      .= compose(IDEA_P_F(Key1,n,r)^IDEA_Q_F(Key2,n,r),MESSAGES).m1 by A22,
FUNCT_7:48
      .= m1 by A1,A2,A3,A5,A10,A14,A13,A12,A11,Th46;
A30: m2.4 is_expressible_by n by A3,A10,A14,A13,A12,A11,Th45;
A31: m2.2 is_expressible_by n & m2.3 is_expressible_by n by A3,A10,A14,A13,A12
,A11,Th45;
    thus (IDEA_QS(ks2,n)*(compose(IDEA_Q_F(Key2,n,r),MESSAGES)* (IDEA_QE(ke2,n
)*(IDEA_PE(ke1,n)*(compose(IDEA_P_F(Key1,n,r),MESSAGES)* IDEA_PS(ks1,n)))))).m
=IDEA_QS(ks2,n).((QF*(IDEA_QE(ke2,n)*(IDEA_PE(ke1,n)*(PF* (IDEA_PS(ks1,n)))))).
    m) by A8,FUNCT_2:15
      .=IDEA_QS(ks2,n).(QF.((IDEA_QE(ke2,n)*(IDEA_PE(ke1,n)*(PF* (IDEA_PS(
    ks1,n))))).m)) by A8,FUNCT_2:15
      .=IDEA_QS(ks2,n).(QF.(IDEA_QE(ke2,n).((IDEA_PE(ke1,n)*(PF* (IDEA_PS(
    ks1,n)))).m))) by A8,FUNCT_2:15
      .=IDEA_QS(ks2,n).(QF.(IDEA_QE(ke2,n).(IDEA_PE(ke1,n).((PF* (IDEA_PS(
    ks1,n))).m)))) by A8,FUNCT_2:15
      .=IDEA_QS(ks2,n).(QF.(IDEA_QE(ke2,n).(IDEA_PE(ke1,n).(PF. (IDEA_PS(ks1
    ,n).m))))) by A8,FUNCT_2:15
      .=IDEA_QS(ks2,n).(QF.((IDEA_QE(ke2,n)*IDEA_PE(ke1,n)).m2)) by A28,
FUNCT_2:15
      .=IDEA_QS(ks2,n).(m1) by A2,A7,A23,A31,A30,A29,Th35
      .=(IDEA_QS(ks2,n)*IDEA_PS(ks1,n)).m by A8,FUNCT_2:15
      .= m by A2,A3,A4,A6,Th34;
  end;
end;