idea_1.miz



    begin

    reserve i,j,k,n for Nat;

    reserve x,y,z for Tuple of n, BOOLEAN ;

    

     Lm1: i <> 0 & i < j & j is prime implies (i,j) are_coprime

    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 be 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 be 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 be 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 be 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 be Integer such that

           A11: a1 = ( 0 - a);

          reconsider a1 as Element of NAT by A10, A11, INT_1: 3;

          consider a2 be Nat such that

           A12: a2 = ((a1 div j) + 1);

          consider a9 be Integer such that

           A13: a9 = (a + (a2 * j));

          

           A14: a9 = ((( - a1) + ((a1 div j) * j)) + j) by A11, A12, A13;

          consider t be 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 be 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 :: IDEA_1:1

    

     Th1: for i, j, k holds j is prime & i < j & k < j & i <> 0 implies ex a be Nat st ((a * i) mod j) = k & a < j

    proof

      let i,j,k be Nat;

      assume that

       A1: j is prime and

       A2: i < j and

       A3: k < j & i <> 0 ;

      consider a be Nat such that

       A4: ((a * i) mod j) = k by A1, A2, A3, Lm2;

      consider a9 be Nat such that

       A5: a9 = (a mod j);

      take a9;

      thus thesis by A2, A4, A5, EULER_2: 8, NAT_D: 1;

    end;

    theorem :: IDEA_1:2

    

     Th2: for n,k1,k2 be Nat holds n <> 0 & (k1 mod n) = (k2 mod n) & k1 <= k2 implies ex t be Nat st (k2 - k1) = (n * t)

    proof

      let n,k1,k2 be Nat;

      assume that

       A1: n <> 0 and

       A2: (k1 mod n) = (k2 mod n) and

       A3: k1 <= k2;

      consider t be 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 :: IDEA_1:3

    

     Th3: for a,b be Nat holds (a - b) <= a

    proof

      let a,b be Nat;

      (a - b) <= (a - 0 ) by XREAL_1: 13;

      hence thesis;

    end;

    theorem :: IDEA_1:4

    

     Th4: for b1,b2,c be Nat holds b2 <= c implies (b2 - b1) <= c

    proof

      let b1,b2,c be 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 :: IDEA_1:5

    

     Th5: for a,b,c be 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 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

    definition

      let n;

      :: IDEA_1:def1

      func ZERO (n) -> Tuple of n, BOOLEAN equals (n |-> FALSE );

      correctness ;

    end

    definition

      let n;

      let x,y be Tuple of n, BOOLEAN ;

      :: IDEA_1:def2

      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 be 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 :: IDEA_1:6

    

     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 :: IDEA_1:7

    

     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 ;

      :: original: 'xor'

      redefine

      func x 'xor' y;

      commutativity by Th7;

    end

    theorem :: IDEA_1:8

    

     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 :: IDEA_1:9

    

     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 Nat;

      :: IDEA_1:def3

      pred i is_expressible_by n means i < (2 to_power n);

    end

    theorem :: IDEA_1:10

    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;

      :: IDEA_1:def4

      func ADD_MOD (i,j,n) -> Nat equals ((i + j) mod (2 to_power n));

      coherence ;

    end

    definition

      let n;

      let i be Nat;

      assume

       A1: i is_expressible_by n;

      :: IDEA_1:def5

      func NEG_N (i,n) -> Nat equals

      : Def5: ((2 to_power n) - i);

      coherence

      proof

        i < (2 to_power n) by A1;

        then ((2 to_power n) - i) > (i - i) by XREAL_1: 9;

        then ((2 to_power n) - i) is Element of NAT by INT_1: 3;

        hence thesis;

      end;

    end

    definition

      let n;

      let i be Nat;

      :: IDEA_1:def6

      func NEG_MOD (i,n) -> Nat equals (( NEG_N (i,n)) mod (2 to_power n));

      coherence ;

    end

    theorem :: IDEA_1:11

    

     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 :: IDEA_1:12

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

    theorem :: IDEA_1:13

    

     Th13: i is_expressible_by n implies ( ADD_MOD ( 0 ,i,n)) = i by NAT_D: 24;

    theorem :: IDEA_1:14

    

     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 :: IDEA_1:15

    

     Th15: ( ADD_MOD (i,j,n)) is_expressible_by n by NAT_D: 1, POWER: 34;

    theorem :: IDEA_1:16

    ( NEG_MOD (i,n)) is_expressible_by n by NAT_D: 1, POWER: 34;

    definition

      let n,i be Nat;

      :: IDEA_1:def7

      func ChangeVal_1 (i,n) -> Nat equals

      : Def7: (2 to_power n) if i = 0

      otherwise i;

      coherence ;

      correctness ;

    end

    theorem :: IDEA_1:17

    

     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;

      end;

    end;

    theorem :: IDEA_1:18

    

     Th18: for n,a1,a2 be 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,a1,a2 be 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;

      

       A5: a2 <> (2 to_power n) by A2;

      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,i be Nat;

      :: IDEA_1:def8

      func ChangeVal_2 (i,n) -> Nat equals

      : Def8: 0 if i = (2 to_power n)

      otherwise i;

      correctness ;

    end

    theorem :: IDEA_1:19

    i is_expressible_by n implies ( ChangeVal_2 (i,n)) is_expressible_by n by Def8;

    theorem :: IDEA_1:20

    

     Th20: for n,a1,a2 be Nat holds a1 <> 0 & a2 <> 0 & ( ChangeVal_2 (a1,n)) = ( ChangeVal_2 (a2,n)) implies a1 = a2

    proof

      let n,a1,a2 be 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;

      :: IDEA_1:def9

      func MUL_MOD (i,j,n) -> 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 zero Nat;

      let i be Nat;

      assume that

       A1: i is_expressible_by n and

       A2: ((2 to_power n) + 1) is prime;

      :: IDEA_1:def10

      func INV_MOD (i,n) -> 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 Nat;

        reconsider n2 = (((2 to_power n) + 1) - 1) as 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;

        per cases ;

          suppose

           A7: i = 0 ;

          consider j such that

           A8: j = 0 ;

          take j;

          

           A9: j is_expressible_by n by A3, A8;

          ( 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;

          then i < ((2 to_power n) + 1) by NAT_1: 13;

          then

          consider a be 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;

              ( 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;

              ( 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;

      uniqueness

      proof

        let a1,a2 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 :: IDEA_1:21

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

    theorem :: IDEA_1:22

    

     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);

      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 :: IDEA_1:23

    

     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 :: IDEA_1:24

    

     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;

        end;

          suppose

           A3: CV < (2 to_power n);

          then ( ChangeVal_2 (CV,n)) = CV by Def8;

          hence thesis by A3;

        end;

      end;

      hence thesis;

    end;

    theorem :: IDEA_1:25

    ( 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

    definition

      let n;

      let m,k be FinSequence of NAT ;

      :: IDEA_1:def11

      func IDEAoperationA (m,k,n) -> FinSequence of NAT means

      : Def11: ( len it ) = ( len m) & for i be 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)) holds ex x be 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;

            reconsider M = ( MUL_MOD ((m . 1),(k . 1),n)) as Element of NAT by ORDINAL1:def 12;

            take M;

            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;

            reconsider M = ( MUL_MOD ((m . 4),(k . 4),n)) as Element of NAT by ORDINAL1:def 12;

            take M;

            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 be 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 be 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

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

    definition

      let n be non zero Nat;

      let m,k be FinSequence of NAT ;

      :: IDEA_1:def12

      func IDEAoperationB (m,k,n) -> FinSequence of NAT means

      : Def12: ( len it ) = ( len m) & for i be 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)) holds ex x be Element of NAT st P[j, x]

        proof

          let j be Nat;

          assume j in ( Seg ( len m));

          reconsider j as 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 be 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

    definition

      let m be FinSequence of NAT ;

      :: IDEA_1:def13

      func IDEAoperationC (m) -> FinSequence of NAT means

      : Def13: ( len it ) = ( len m) & for i be 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)) holds ex x be Element of NAT st P[k, x]

        proof

          let k be Nat;

          assume k in ( Seg ( len m));

          reconsider k as 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 be 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 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 :: IDEA_1:26

    

     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 :: IDEA_1:27

    

     Th27: for n be non zero 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 zero 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;

    end;

    

     Lm3: for i st i = 2 & i in ( dom m) holds (( IDEAoperationC m) . i) = (m . 3)

    proof

      let i be 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 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 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 :: IDEA_1:28

    ( 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 :: IDEA_1:29

    

     Th29: for n be non zero 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 zero 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 be FinSequence of NAT such that

       A20: I1 = ( IDEAoperationA (m,k1,n));

      consider I2 be 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 :: IDEA_1:30

    

     Th30: for n be non zero 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 zero 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 be 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 be 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 be 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 be 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 :: IDEA_1:31

    

     Th31: for n be non zero 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 zero 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 be Nat such that

       A8: t10 = ( MUL_MOD (( Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k1 . 5),n));

      consider t11 be 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 be 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 be 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 be 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 be 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 be 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;

            

            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;

            

            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;

            

            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;

            

            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 :: IDEA_1:32

    for m holds ( len m) >= 4 implies ( IDEAoperationC ( IDEAoperationC m)) = m

    proof

      let m be FinSequence of NAT ;

      consider I1 be 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 be 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

    definition

      :: IDEA_1:def14

      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 zero Nat, k;

      :: IDEA_1:def15

      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 be Element of MESSAGES holds ex u be 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 be Function of MESSAGES , MESSAGES such that

         A2: for e be 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 be 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 be FinSequence of NAT holds (m1 . m) = ( IDEAoperationA (( IDEAoperationC ( IDEAoperationB (m,k,n))),k,n)) and

         A4: for m be FinSequence of NAT holds (m2 . m) = ( IDEAoperationA (( IDEAoperationC ( IDEAoperationB (m,k,n))),k,n));

         A5:

        now

          let j be object;

          reconsider jj = j as set by TARSKI: 1;

          assume j in MESSAGES ;

          then

          reconsider jj as FinSequence of NAT by FINSEQ_1:def 11;

          

          thus (m1 . j) = ( IDEAoperationA (( IDEAoperationC ( IDEAoperationB (jj,k,n))),k,n)) by A3

          .= (m2 . j) by A4;

        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 zero Nat, k;

      :: IDEA_1:def16

      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 be Element of MESSAGES holds ex u be 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 be Function of MESSAGES , MESSAGES such that

         A2: for e be 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 be 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 be FinSequence of NAT holds (m1 . m) = ( IDEAoperationB (( IDEAoperationA (( IDEAoperationC m),k,n)),k,n)) and

         A4: for m be FinSequence of NAT holds (m2 . m) = ( IDEAoperationB (( IDEAoperationA (( IDEAoperationC m),k,n)),k,n));

         A5:

        now

          let j be object;

          reconsider jj = j as set by TARSKI: 1;

          assume j in MESSAGES ;

          then

          reconsider jj as FinSequence of NAT by FINSEQ_1:def 11;

          

          thus (m1 . j) = ( IDEAoperationB (( IDEAoperationA (( IDEAoperationC jj),k,n)),k,n)) by A3

          .= (m2 . j) by A4;

        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 Nat, n be non zero Nat, Key be Matrix of lk, 6, NAT ;

      :: IDEA_1:def17

      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 be FinSequence such that

         A1: ( len z) = r & for k be 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 be Nat st i in ( dom z1) holds (z1 . i) = ( IDEA_P (( Line (Key,i)),n)) and

         A4: ( len z2) = r and

         A5: for i be 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 Nat, n be non zero Nat, Key be Matrix of lk, 6, NAT ;

      cluster ( IDEA_P_F (Key,n,r)) -> Function-yielding;

      coherence

      proof

        for x be object st x in ( dom ( IDEA_P_F (Key,n,r))) holds (( IDEA_P_F (Key,n,r)) . x) is Function

        proof

          let x be object;

          assume

           A1: x in ( dom ( IDEA_P_F (Key,n,r)));

          then

          consider xx be 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;

      end;

    end

    definition

      let r,lk be Nat, n be non zero Nat, Key be Matrix of lk, 6, NAT ;

      :: IDEA_1:def18

      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 be FinSequence such that

         A1: ( len z) = r & for k be 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 be 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 be 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 Nat, n be non zero Nat, Key be Matrix of lk, 6, NAT ;

      cluster ( IDEA_Q_F (Key,n,r)) -> Function-yielding;

      coherence

      proof

        let x be object;

        assume

         A1: x in ( dom ( IDEA_Q_F (Key,n,r)));

        then

        consider xx be 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;

    end

    definition

      let k, n;

      :: IDEA_1:def19

      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 be Element of MESSAGES holds ex u be 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 be Function of MESSAGES , MESSAGES such that

         A2: for e be 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 be 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 be FinSequence of NAT holds (m1 . m) = ( IDEAoperationA (m,k,n)) and

         A4: for m be FinSequence of NAT holds (m2 . m) = ( IDEAoperationA (m,k,n));

         A5:

        now

          let j be object;

          reconsider jj = j as set by TARSKI: 1;

          assume j in MESSAGES ;

          then

          reconsider jj as FinSequence of NAT by FINSEQ_1:def 11;

          

          thus (m1 . j) = ( IDEAoperationA (jj,k,n)) by A3

          .= (m2 . j) by A4;

        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;

      :: IDEA_1:def20

      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 be Element of MESSAGES holds ex u be 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 be Function of MESSAGES , MESSAGES such that

         A2: for e be 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 be 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 be FinSequence of NAT holds (m1 . m) = ( IDEAoperationA (m,k,n)) and

         A4: for m be FinSequence of NAT holds (m2 . m) = ( IDEAoperationA (m,k,n));

         A5:

        now

          let j be object;

          reconsider jj = j as set by TARSKI: 1;

          assume j in MESSAGES ;

          then

          reconsider jj as FinSequence of NAT by FINSEQ_1:def 11;

          

          thus (m1 . j) = ( IDEAoperationA (jj,k,n)) by A3

          .= (m2 . j) by A4;

        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 zero Nat, k;

      :: IDEA_1:def21

      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 be Element of MESSAGES holds ex u be 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 be Function of MESSAGES , MESSAGES such that

         A2: for e be 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 be 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 be FinSequence of NAT holds (m1 . m) = ( IDEAoperationA (( IDEAoperationB (m,k,n)),k,n)) and

         A4: for m be FinSequence of NAT holds (m2 . m) = ( IDEAoperationA (( IDEAoperationB (m,k,n)),k,n));

         A5:

        now

          let j be object;

          reconsider jj = j as set by TARSKI: 1;

          assume j in MESSAGES ;

          then

          reconsider jj as FinSequence of NAT by FINSEQ_1:def 11;

          

          thus (m1 . j) = ( IDEAoperationA (( IDEAoperationB (jj,k,n)),k,n)) by A3

          .= (m2 . j) by A4;

        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 zero Nat, k;

      :: IDEA_1:def22

      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 be Element of MESSAGES holds ex u be 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 be Function of MESSAGES , MESSAGES such that

         A2: for e be 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 be 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 be FinSequence of NAT holds (m1 . m) = ( IDEAoperationB (( IDEAoperationA (m,k,n)),k,n)) and

         A4: for m be FinSequence of NAT holds (m2 . m) = ( IDEAoperationB (( IDEAoperationA (m,k,n)),k,n));

         A5:

        now

          let j be object;

          reconsider jj = j as set by TARSKI: 1;

          assume j in MESSAGES ;

          then

          reconsider jj as FinSequence of NAT by FINSEQ_1:def 11;

          

          thus (m1 . j) = ( IDEAoperationB (( IDEAoperationA (jj,k,n)),k,n)) by A3

          .= (m2 . j) by A4;

        end;

        ( dom m1) = MESSAGES & ( dom m2) = MESSAGES by FUNCT_2:def 1;

        hence thesis by A5, FUNCT_1: 2;

      end;

    end

    theorem :: IDEA_1:33

    

     Th33: for n be non zero 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 zero 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 :: IDEA_1:34

    

     Th34: for n be non zero 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 zero 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 :: IDEA_1:35

    

     Th35: for n be non zero 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 zero 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 :: IDEA_1:36

    

     Th36: for n be non zero Nat, lk be Nat, Key be Matrix of lk, 6, NAT , k be 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 zero Nat;

      let lk be Nat;

      let Key be Matrix of lk, 6, NAT ;

      let k be Nat;

      

       A1: for i be 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 :: IDEA_1:37

    

     Th37: for n be non zero Nat, lk be Nat, Key be Matrix of lk, 6, NAT , k be 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 zero Nat;

      let lk be Nat;

      let Key be Matrix of lk, 6, NAT ;

      let k be Nat;

      

       A1: for i be 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 :: IDEA_1:38

    

     Th38: for n be non zero Nat, lk be Nat, Key be Matrix of lk, 6, NAT , k be Nat holds ( IDEA_P_F (Key,n,k)) is FuncSeq-like FinSequence

    proof

      let n be non zero Nat;

      let lk be Nat;

      let Key be Matrix of lk, 6, NAT ;

      let k be Nat;

      set p = (( Seg (k + 1)) --> MESSAGES );

      

       A1: ( dom p) = ( Seg (k + 1)) by FUNCOP_1: 13;

      reconsider p as FinSequence;

      

       A2: for i be 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 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 :: IDEA_1:39

    

     Th39: for n be non zero Nat, lk be Nat, Key be Matrix of lk, 6, NAT , k be Nat holds ( IDEA_Q_F (Key,n,k)) is FuncSeq-like FinSequence

    proof

      let n be non zero Nat;

      let lk be Nat;

      let Key be Matrix of lk, 6, NAT ;

      let k be Nat;

      set p = (( Seg (k + 1)) --> MESSAGES );

      

       A1: ( dom p) = ( Seg (k + 1)) by FUNCOP_1: 13;

      reconsider p as FinSequence;

      

       A2: for i be 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 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 :: IDEA_1:40

    

     Th40: for n be non zero Nat, lk be Nat, Key be Matrix of lk, 6, NAT , k be Nat holds k <> 0 implies ( IDEA_P_F (Key,n,k)) is FuncSequence of MESSAGES , MESSAGES

    proof

      let n be non zero Nat;

      let lk be Nat, Key be Matrix of lk, 6, NAT , k be 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 :: IDEA_1:41

    

     Th41: for n be non zero Nat, lk be Nat, Key be Matrix of lk, 6, NAT , k be Nat holds k <> 0 implies ( IDEA_Q_F (Key,n,k)) is FuncSequence of MESSAGES , MESSAGES

    proof

      let n be non zero Nat, lk be Nat, Key be Matrix of lk, 6, NAT , r be 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 :: IDEA_1:42

    

     Th42: for n be non zero Nat, M be 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 zero 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 :: IDEA_1:43

    

     Th43: for n be non zero Nat, lk be Nat, Key be Matrix of lk, 6, NAT , r be 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 zero Nat, lk be Nat, Key be Matrix of lk, 6, NAT , r be 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;

        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;

        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 :: IDEA_1:44

    for n be non zero Nat, lk be Nat, Key be Matrix of lk, 6, NAT , r be 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 zero Nat, lk be Nat, Key be Matrix of lk, 6, NAT , r be 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;

        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;

        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 :: IDEA_1:45

    

     Th45: for n be non zero Nat, lk be Nat, Key be Matrix of lk, 6, NAT , r be Nat, M be 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 zero Nat, lk be Nat, Key be Matrix of lk, 6, NAT , r be 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 be Integer such that

         A6: r1 = (r - 1);

        defpred P[ Nat] means for M be 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 be Nat st P[k] holds P[(k + 1)]

        proof

          let k be 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 be Nat holds P[k] from NAT_1:sch 2( 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

    theorem :: IDEA_1:46

    

     Th46: for n be non zero Nat, lk be Nat, Key1,Key2 be Matrix of lk, 6, NAT , r be 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 be 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 zero Nat, lk be Nat;

      let Key1,Key2 be Matrix of lk, 6, NAT ;

      for r be 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 be 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[ 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 be 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 be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A3: P[k];

          consider k1 be 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 be 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_0: 23;

          then 1 in ( Seg ( width Key1)) by FINSEQ_1: 1;

          then

           A14: (( Line (Key1,(k + 1))) . 1) = (Key1 * (k1,1)) by A4, MATRIX_0:def 7;

          then

           A15: (( Line (Key1,(k + 1))) . 1) is_expressible_by n by A11, A4;

          

           A16: ( width Key2) = 6 by A8, MATRIX_0: 23;

          then 5 in ( Seg ( width Key2)) by FINSEQ_1: 1;

          then

           A17: (( Line (Key2,(k + 1))) . 5) = (Key2 * (k1,5)) by A4, MATRIX_0: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_0: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_0: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_0: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_0: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_0: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_0: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_0: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_0:def 7;

          6 in ( Seg ( width Key1)) by A13, FINSEQ_1: 1;

          then (( Line (Key1,(k + 1))) . 6) = (Key1 * (k1,6)) by A4, MATRIX_0: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_0: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 be 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 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 be Nat holds P[k] from NAT_1:sch 2( A37, A2);

      end;

      hence thesis;

    end;

    theorem :: IDEA_1:47

    for n be non zero Nat, lk be Nat, Key1,Key2 be Matrix of lk, 6, NAT , r be Nat, ks1,ks2,ke1,ke2 be 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 be 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 zero Nat, lk be Nat, Key1,Key2 be Matrix of lk, 6, NAT , r be 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 be 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;