:: IDEA_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for i, j being Nat st i <> 0 & i < j & j is prime holds
i,j are_relative_prime
proof end;

Lm2: for j, i, k being Nat st j is prime & i < j & k < j & i <> 0 holds
ex a being Nat st (a * i) mod j = k
proof end;

theorem Th1: :: IDEA_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j, k being Nat st j is prime & i < j & k < j & i <> 0 holds
ex a being Nat st
( (a * i) mod j = k & a < j )
proof end;

theorem Th2: :: IDEA_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k1, k2 being Nat st n <> 0 & k1 mod n = k2 mod n & k1 <= k2 holds
ex t being Nat st k2 - k1 = n * t
proof end;

theorem Th3: :: IDEA_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Nat holds a - b <= a
proof end;

theorem Th4: :: IDEA_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b1, b2, c being Nat st b2 <= c holds
b2 - b1 <= c
proof end;

theorem Th5: :: IDEA_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being Nat st 0 < a & 0 < b & a < c & b < c & c is prime holds
(a * b) mod c <> 0
proof end;

definition
let n be Nat;
func ZERO n -> Tuple of n,BOOLEAN equals :: IDEA_1:def 1
n |-> FALSE ;
correctness
coherence
n |-> FALSE is Tuple of n,BOOLEAN
;
by FINSEQ_2:132;
end;

:: deftheorem defines ZERO IDEA_1:def 1 :
for n being Nat holds ZERO n = n |-> FALSE ;

definition
let n be Nat;
let x, y be Tuple of n,BOOLEAN ;
func x 'xor' y -> Tuple of n,BOOLEAN means :Def2: :: IDEA_1:def 2
for i being Nat st i in Seg n holds
it /. i = (x /. i) 'xor' (y /. i);
existence
ex b1 being Tuple of n,BOOLEAN st
for i being Nat st i in Seg n holds
b1 /. i = (x /. i) 'xor' (y /. i)
proof end;
uniqueness
for b1, b2 being Tuple of n,BOOLEAN st ( for i being Nat st i in Seg n holds
b1 /. i = (x /. i) 'xor' (y /. i) ) & ( for i being Nat st i in Seg n holds
b2 /. i = (x /. i) 'xor' (y /. i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines 'xor' IDEA_1:def 2 :
for n being Nat
for x, y, b4 being Tuple of n,BOOLEAN holds
( b4 = x 'xor' y iff for i being Nat st i in Seg n holds
b4 /. i = (x /. i) 'xor' (y /. i) );

theorem :: IDEA_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th7: :: IDEA_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for x being Tuple of n,BOOLEAN holds x 'xor' x = ZERO n
proof end;

theorem Th8: :: IDEA_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for x, y being Tuple of n,BOOLEAN holds x 'xor' y = y 'xor' x
proof end;

definition
let n be Nat;
let x, y be Tuple of n,BOOLEAN ;
:: original: 'xor'
redefine func x 'xor' y -> Tuple of n,BOOLEAN ;
commutativity
for x, y being Tuple of n,BOOLEAN holds x 'xor' y = y 'xor' x
by Th8;
end;

theorem Th9: :: IDEA_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for x being Tuple of n,BOOLEAN holds (ZERO n) 'xor' x = x
proof end;

theorem Th10: :: IDEA_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for x, y, z being Tuple of n,BOOLEAN holds (x 'xor' y) 'xor' z = x 'xor' (y 'xor' z)
proof end;

definition
let n, i be Nat;
pred i is_expressible_by n means :Def3: :: IDEA_1:def 3
i < 2 to_power n;
end;

:: deftheorem Def3 defines is_expressible_by IDEA_1:def 3 :
for n, i being Nat holds
( i is_expressible_by n iff i < 2 to_power n );

theorem :: IDEA_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds n -BinarySequence 0 = ZERO n
proof end;

definition
let n be Nat;
let i, j be Nat;
func ADD_MOD i,j,n -> Nat equals :: IDEA_1:def 4
(i + j) mod (2 to_power n);
coherence
(i + j) mod (2 to_power n) is Nat
;
end;

:: deftheorem defines ADD_MOD IDEA_1:def 4 :
for n, i, j being Nat holds ADD_MOD i,j,n = (i + j) mod (2 to_power n);

definition
let n, i be Nat;
assume A1: i is_expressible_by n ;
func NEG_N i,n -> Nat equals :Def5: :: IDEA_1:def 5
(2 to_power n) - i;
coherence
(2 to_power n) - i is Nat
proof end;
end;

:: deftheorem Def5 defines NEG_N IDEA_1:def 5 :
for n, i being Nat st i is_expressible_by n holds
NEG_N i,n = (2 to_power n) - i;

definition
let n, i be Nat;
func NEG_MOD i,n -> Nat equals :: IDEA_1:def 6
(NEG_N i,n) mod (2 to_power n);
coherence
(NEG_N i,n) mod (2 to_power n) is Nat
;
end;

:: deftheorem defines NEG_MOD IDEA_1:def 6 :
for n, i being Nat holds NEG_MOD i,n = (NEG_N i,n) mod (2 to_power n);

theorem Th12: :: IDEA_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat st i is_expressible_by n holds
ADD_MOD i,(NEG_MOD i,n),n = 0
proof end;

theorem :: IDEA_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j, n being Nat holds ADD_MOD i,j,n = ADD_MOD j,i,n ;

theorem Th14: :: IDEA_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat st i is_expressible_by n holds
ADD_MOD 0,i,n = i
proof end;

theorem Th15: :: IDEA_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j, n, k being Nat holds ADD_MOD (ADD_MOD i,j,n),k,n = ADD_MOD i,(ADD_MOD j,k,n),n
proof end;

theorem Th16: :: IDEA_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j, n being Nat holds ADD_MOD i,j,n is_expressible_by n
proof end;

theorem :: IDEA_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat holds NEG_MOD i,n is_expressible_by n
proof end;

definition
let n, i be Nat;
func ChangeVal_1 i,n -> Nat equals :Def7: :: IDEA_1:def 7
2 to_power n if i = 0
otherwise i;
correctness
coherence
( ( i = 0 implies 2 to_power n is Nat ) & ( not i = 0 implies i is Nat ) )
;
consistency
for b1 being Nat holds verum
;
;
end;

:: deftheorem Def7 defines ChangeVal_1 IDEA_1:def 7 :
for n, i being Nat holds
( ( i = 0 implies ChangeVal_1 i,n = 2 to_power n ) & ( not i = 0 implies ChangeVal_1 i,n = i ) );

theorem Th18: :: IDEA_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat st i is_expressible_by n holds
( ChangeVal_1 i,n <= 2 to_power n & ChangeVal_1 i,n > 0 )
proof end;

theorem Th19: :: IDEA_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, a1, a2 being Nat st a1 is_expressible_by n & a2 is_expressible_by n & ChangeVal_1 a1,n = ChangeVal_1 a2,n holds
a1 = a2
proof end;

definition
let n, i be Nat;
func ChangeVal_2 i,n -> Nat equals :Def8: :: IDEA_1:def 8
0 if i = 2 to_power n
otherwise i;
correctness
coherence
( ( i = 2 to_power n implies 0 is Nat ) & ( not i = 2 to_power n implies i is Nat ) )
;
consistency
for b1 being Nat holds verum
;
;
end;

:: deftheorem Def8 defines ChangeVal_2 IDEA_1:def 8 :
for n, i being Nat holds
( ( i = 2 to_power n implies ChangeVal_2 i,n = 0 ) & ( not i = 2 to_power n implies ChangeVal_2 i,n = i ) );

theorem :: IDEA_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat st i is_expressible_by n holds
ChangeVal_2 i,n is_expressible_by n
proof end;

theorem Th21: :: IDEA_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, a1, a2 being Nat st a1 <> 0 & a2 <> 0 & ChangeVal_2 a1,n = ChangeVal_2 a2,n holds
a1 = a2
proof end;

definition
let n be Nat;
let i, j be Nat;
func MUL_MOD i,j,n -> Nat equals :: IDEA_1:def 9
ChangeVal_2 (((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) mod ((2 to_power n) + 1)),n;
coherence
ChangeVal_2 (((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) mod ((2 to_power n) + 1)),n is Nat
;
end;

:: deftheorem defines MUL_MOD IDEA_1:def 9 :
for n, i, j being Nat holds MUL_MOD i,j,n = ChangeVal_2 (((ChangeVal_1 i,n) * (ChangeVal_1 j,n)) mod ((2 to_power n) + 1)),n;

definition
let n be non empty Nat;
let i be Nat;
assume A1: ( i is_expressible_by n & (2 to_power n) + 1 is prime ) ;
func INV_MOD i,n -> Nat means :Def10: :: IDEA_1:def 10
( MUL_MOD i,it,n = 1 & it is_expressible_by n );
existence
ex b1 being Nat st
( MUL_MOD i,b1,n = 1 & b1 is_expressible_by n )
proof end;
uniqueness
for b1, b2 being Nat st MUL_MOD i,b1,n = 1 & b1 is_expressible_by n & MUL_MOD i,b2,n = 1 & b2 is_expressible_by n holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines INV_MOD IDEA_1:def 10 :
for n being non empty Nat
for i being Nat st i is_expressible_by n & (2 to_power n) + 1 is prime holds
for b3 being Nat holds
( b3 = INV_MOD i,n iff ( MUL_MOD i,b3,n = 1 & b3 is_expressible_by n ) );

theorem :: IDEA_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j, n being Nat holds MUL_MOD i,j,n = MUL_MOD j,i,n ;

theorem Th23: :: IDEA_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat st i is_expressible_by n holds
MUL_MOD 1,i,n = i
proof end;

theorem Th24: :: IDEA_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i, j, k being Nat st (2 to_power n) + 1 is prime & i is_expressible_by n & j is_expressible_by n & k is_expressible_by n holds
MUL_MOD (MUL_MOD i,j,n),k,n = MUL_MOD i,(MUL_MOD j,k,n),n
proof end;

theorem Th25: :: IDEA_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j, n being Nat holds MUL_MOD i,j,n is_expressible_by n
proof end;

theorem :: IDEA_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat st ChangeVal_2 i,n = 1 holds
i = 1
proof end;

definition
let n be Nat;
let m, k be FinSequence of NAT ;
func IDEAoperationA m,k,n -> FinSequence of NAT means :Def11: :: IDEA_1:def 11
( len it = len m & ( for i being 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
ex b1 being FinSequence of NAT st
( len b1 = len m & ( for i being Nat st i in dom m holds
( ( i = 1 implies b1 . i = MUL_MOD (m . 1),(k . 1),n ) & ( i = 2 implies b1 . i = ADD_MOD (m . 2),(k . 2),n ) & ( i = 3 implies b1 . i = ADD_MOD (m . 3),(k . 3),n ) & ( i = 4 implies b1 . i = MUL_MOD (m . 4),(k . 4),n ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies b1 . i = m . i ) ) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of NAT st len b1 = len m & ( for i being Nat st i in dom m holds
( ( i = 1 implies b1 . i = MUL_MOD (m . 1),(k . 1),n ) & ( i = 2 implies b1 . i = ADD_MOD (m . 2),(k . 2),n ) & ( i = 3 implies b1 . i = ADD_MOD (m . 3),(k . 3),n ) & ( i = 4 implies b1 . i = MUL_MOD (m . 4),(k . 4),n ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies b1 . i = m . i ) ) ) & len b2 = len m & ( for i being Nat st i in dom m holds
( ( i = 1 implies b2 . i = MUL_MOD (m . 1),(k . 1),n ) & ( i = 2 implies b2 . i = ADD_MOD (m . 2),(k . 2),n ) & ( i = 3 implies b2 . i = ADD_MOD (m . 3),(k . 3),n ) & ( i = 4 implies b2 . i = MUL_MOD (m . 4),(k . 4),n ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies b2 . i = m . i ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines IDEAoperationA IDEA_1:def 11 :
for n being Nat
for m, k, b4 being FinSequence of NAT holds
( b4 = IDEAoperationA m,k,n iff ( len b4 = len m & ( for i being Nat st i in dom m holds
( ( i = 1 implies b4 . i = MUL_MOD (m . 1),(k . 1),n ) & ( i = 2 implies b4 . i = ADD_MOD (m . 2),(k . 2),n ) & ( i = 3 implies b4 . i = ADD_MOD (m . 3),(k . 3),n ) & ( i = 4 implies b4 . i = MUL_MOD (m . 4),(k . 4),n ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies b4 . i = m . i ) ) ) ) );

definition
let n be non empty Nat;
let m, k be FinSequence of NAT ;
func IDEAoperationB m,k,n -> FinSequence of NAT means :Def12: :: IDEA_1:def 12
( len it = len m & ( for i being 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
ex b1 being FinSequence of NAT st
( len b1 = len m & ( for i being Nat st i in dom m holds
( ( i = 1 implies b1 . 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 b1 . 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 b1 . 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 b1 . 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 b1 . i = m . i ) ) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of NAT st len b1 = len m & ( for i being Nat st i in dom m holds
( ( i = 1 implies b1 . 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 b1 . 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 b1 . 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 b1 . 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 b1 . i = m . i ) ) ) & len b2 = len m & ( for i being Nat st i in dom m holds
( ( i = 1 implies b2 . 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 b2 . 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 b2 . 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 b2 . 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 b2 . i = m . i ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines IDEAoperationB IDEA_1:def 12 :
for n being non empty Nat
for m, k, b4 being FinSequence of NAT holds
( b4 = IDEAoperationB m,k,n iff ( len b4 = len m & ( for i being Nat st i in dom m holds
( ( i = 1 implies b4 . 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 b4 . 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 b4 . 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 b4 . 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 b4 . i = m . i ) ) ) ) );

definition
let m be FinSequence of NAT ;
func IDEAoperationC m -> FinSequence of NAT means :Def13: :: IDEA_1:def 13
( len it = len m & ( for i being Nat st i in dom m holds
it . i = IFEQ i,2,(m . 3),(IFEQ i,3,(m . 2),(m . i)) ) );
existence
ex b1 being FinSequence of NAT st
( len b1 = len m & ( for i being Nat st i in dom m holds
b1 . i = IFEQ i,2,(m . 3),(IFEQ i,3,(m . 2),(m . i)) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of NAT st len b1 = len m & ( for i being Nat st i in dom m holds
b1 . i = IFEQ i,2,(m . 3),(IFEQ i,3,(m . 2),(m . i)) ) & len b2 = len m & ( for i being Nat st i in dom m holds
b2 . i = IFEQ i,2,(m . 3),(IFEQ i,3,(m . 2),(m . i)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines IDEAoperationC IDEA_1:def 13 :
for m, b2 being FinSequence of NAT holds
( b2 = IDEAoperationC m iff ( len b2 = len m & ( for i being Nat st i in dom m holds
b2 . i = IFEQ i,2,(m . 3),(IFEQ i,3,(m . 2),(m . i)) ) ) );

theorem Th27: :: IDEA_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for m, k being FinSequence of NAT st len m >= 4 holds
( (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 end;

theorem Th28: :: IDEA_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, k being FinSequence of NAT
for n being non empty Nat st len m >= 4 holds
( (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 end;

Lm3: for m being FinSequence of NAT
for i being Nat st i = 2 & i in dom m holds
(IDEAoperationC m) . i = m . 3
proof end;

Lm4: for m being FinSequence of NAT
for i being Nat st i = 3 & i in dom m holds
(IDEAoperationC m) . i = m . 2
proof end;

Lm5: for m being FinSequence of NAT
for i being Nat st i <> 2 & i <> 3 & i in dom m holds
(IDEAoperationC m) . i = m . i
proof end;

theorem :: IDEA_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for m being FinSequence of NAT st 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
( (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 end;

theorem Th30: :: IDEA_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for m, k1, k2 being FinSequence of NAT st (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 holds
IDEAoperationA (IDEAoperationA m,k1,n),k2,n = m
proof end;

theorem Th31: :: IDEA_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for m, k1, k2 being FinSequence of NAT st (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 holds
IDEAoperationA (IDEAoperationC (IDEAoperationA (IDEAoperationC m),k1,n)),k2,n = m
proof end;

theorem Th32: :: IDEA_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for m, k1, k2 being FinSequence of NAT st (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 . 5 is_expressible_by n & k1 . 6 is_expressible_by n & k2 . 5 = k1 . 5 & k2 . 6 = k1 . 6 holds
IDEAoperationB (IDEAoperationB m,k1,n),k2,n = m
proof end;

theorem :: IDEA_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being FinSequence of NAT st len m >= 4 holds
IDEAoperationC (IDEAoperationC m) = m
proof end;

definition
func MESSAGES -> set equals :: IDEA_1:def 14
NAT * ;
coherence
NAT * is set
;
end;

:: deftheorem defines MESSAGES IDEA_1:def 14 :
MESSAGES = NAT * ;

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

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

registration
cluster -> FinSequence-like Element of MESSAGES ;
coherence
for b1 being Element of MESSAGES holds b1 is FinSequence-like
by FINSEQ_1:def 11;
end;

definition
let n be non empty Nat;
let k be FinSequence of NAT ;
func IDEA_P k,n -> Function of MESSAGES , MESSAGES means :Def15: :: IDEA_1:def 15
for m being FinSequence of NAT holds it . m = IDEAoperationA (IDEAoperationC (IDEAoperationB m,k,n)),k,n;
existence
ex b1 being Function of MESSAGES , MESSAGES st
for m being FinSequence of NAT holds b1 . m = IDEAoperationA (IDEAoperationC (IDEAoperationB m,k,n)),k,n
proof end;
uniqueness
for b1, b2 being Function of MESSAGES , MESSAGES st ( for m being FinSequence of NAT holds b1 . m = IDEAoperationA (IDEAoperationC (IDEAoperationB m,k,n)),k,n ) & ( for m being FinSequence of NAT holds b2 . m = IDEAoperationA (IDEAoperationC (IDEAoperationB m,k,n)),k,n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines IDEA_P IDEA_1:def 15 :
for n being non empty Nat
for k being FinSequence of NAT
for b3 being Function of MESSAGES , MESSAGES holds
( b3 = IDEA_P k,n iff for m being FinSequence of NAT holds b3 . m = IDEAoperationA (IDEAoperationC (IDEAoperationB m,k,n)),k,n );

definition
let n be non empty Nat;
let k be FinSequence of NAT ;
func IDEA_Q k,n -> Function of MESSAGES , MESSAGES means :Def16: :: IDEA_1:def 16
for m being FinSequence of NAT holds it . m = IDEAoperationB (IDEAoperationA (IDEAoperationC m),k,n),k,n;
existence
ex b1 being Function of MESSAGES , MESSAGES st
for m being FinSequence of NAT holds b1 . m = IDEAoperationB (IDEAoperationA (IDEAoperationC m),k,n),k,n
proof end;
uniqueness
for b1, b2 being Function of MESSAGES , MESSAGES st ( for m being FinSequence of NAT holds b1 . m = IDEAoperationB (IDEAoperationA (IDEAoperationC m),k,n),k,n ) & ( for m being FinSequence of NAT holds b2 . m = IDEAoperationB (IDEAoperationA (IDEAoperationC m),k,n),k,n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines IDEA_Q IDEA_1:def 16 :
for n being non empty Nat
for k being FinSequence of NAT
for b3 being Function of MESSAGES , MESSAGES holds
( b3 = IDEA_Q k,n iff for m being FinSequence of NAT holds b3 . m = IDEAoperationB (IDEAoperationA (IDEAoperationC m),k,n),k,n );

definition
let r, lk be Nat;
let n be non empty Nat;
let Key be Matrix of lk,6, NAT ;
func IDEA_P_F Key,n,r -> FinSequence means :Def17: :: IDEA_1:def 17
( len it = r & ( for i being Nat st i in dom it holds
it . i = IDEA_P (Line Key,i),n ) );
existence
ex b1 being FinSequence st
( len b1 = r & ( for i being Nat st i in dom b1 holds
b1 . i = IDEA_P (Line Key,i),n ) )
proof end;
uniqueness
for b1, b2 being FinSequence st len b1 = r & ( for i being Nat st i in dom b1 holds
b1 . i = IDEA_P (Line Key,i),n ) & len b2 = r & ( for i being Nat st i in dom b2 holds
b2 . i = IDEA_P (Line Key,i),n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines IDEA_P_F IDEA_1:def 17 :
for r, lk being Nat
for n being non empty Nat
for Key being Matrix of lk,6, NAT
for b5 being FinSequence holds
( b5 = IDEA_P_F Key,n,r iff ( len b5 = r & ( for i being Nat st i in dom b5 holds
b5 . i = IDEA_P (Line Key,i),n ) ) );

registration
let r, lk be Nat;
let n be non empty Nat;
let Key be Matrix of lk,6, NAT ;
cluster IDEA_P_F Key,n,r -> Function-yielding ;
coherence
IDEA_P_F Key,n,r is Function-yielding
proof end;
end;

definition
let r, lk be Nat;
let n be non empty Nat;
let Key be Matrix of lk,6, NAT ;
func IDEA_Q_F Key,n,r -> FinSequence means :Def18: :: IDEA_1:def 18
( len it = r & ( for i being Nat st i in dom it holds
it . i = IDEA_Q (Line Key,((r -' i) + 1)),n ) );
existence
ex b1 being FinSequence st
( len b1 = r & ( for i being Nat st i in dom b1 holds
b1 . i = IDEA_Q (Line Key,((r -' i) + 1)),n ) )
proof end;
uniqueness
for b1, b2 being FinSequence st len b1 = r & ( for i being Nat st i in dom b1 holds
b1 . i = IDEA_Q (Line Key,((r -' i) + 1)),n ) & len b2 = r & ( for i being Nat st i in dom b2 holds
b2 . i = IDEA_Q (Line Key,((r -' i) + 1)),n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines IDEA_Q_F IDEA_1:def 18 :
for r, lk being Nat
for n being non empty Nat
for Key being Matrix of lk,6, NAT
for b5 being FinSequence holds
( b5 = IDEA_Q_F Key,n,r iff ( len b5 = r & ( for i being Nat st i in dom b5 holds
b5 . i = IDEA_Q (Line Key,((r -' i) + 1)),n ) ) );

registration
let r, lk be Nat;
let n be non empty Nat;
let Key be Matrix of lk,6, NAT ;
cluster IDEA_Q_F Key,n,r -> Function-yielding ;
coherence
IDEA_Q_F Key,n,r is Function-yielding
proof end;
end;

definition
let k be FinSequence of NAT ;
let n be Nat;
func IDEA_PS k,n -> Function of MESSAGES , MESSAGES means :Def19: :: IDEA_1:def 19
for m being FinSequence of NAT holds it . m = IDEAoperationA m,k,n;
existence
ex b1 being Function of MESSAGES , MESSAGES st
for m being FinSequence of NAT holds b1 . m = IDEAoperationA m,k,n
proof end;
uniqueness
for b1, b2 being Function of MESSAGES , MESSAGES st ( for m being FinSequence of NAT holds b1 . m = IDEAoperationA m,k,n ) & ( for m being FinSequence of NAT holds b2 . m = IDEAoperationA m,k,n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines IDEA_PS IDEA_1:def 19 :
for k being FinSequence of NAT
for n being Nat
for b3 being Function of MESSAGES , MESSAGES holds
( b3 = IDEA_PS k,n iff for m being FinSequence of NAT holds b3 . m = IDEAoperationA m,k,n );

definition
let k be FinSequence of NAT ;
let n be Nat;
func IDEA_QS k,n -> Function of MESSAGES , MESSAGES means :Def20: :: IDEA_1:def 20
for m being FinSequence of NAT holds it . m = IDEAoperationA m,k,n;
existence
ex b1 being Function of MESSAGES , MESSAGES st
for m being FinSequence of NAT holds b1 . m = IDEAoperationA m,k,n
proof end;
uniqueness
for b1, b2 being Function of MESSAGES , MESSAGES st ( for m being FinSequence of NAT holds b1 . m = IDEAoperationA m,k,n ) & ( for m being FinSequence of NAT holds b2 . m = IDEAoperationA m,k,n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines IDEA_QS IDEA_1:def 20 :
for k being FinSequence of NAT
for n being Nat
for b3 being Function of MESSAGES , MESSAGES holds
( b3 = IDEA_QS k,n iff for m being FinSequence of NAT holds b3 . m = IDEAoperationA m,k,n );

definition
let n be non empty Nat;
let k be FinSequence of NAT ;
func IDEA_PE k,n -> Function of MESSAGES , MESSAGES means :Def21: :: IDEA_1:def 21
for m being FinSequence of NAT holds it . m = IDEAoperationA (IDEAoperationB m,k,n),k,n;
existence
ex b1 being Function of MESSAGES , MESSAGES st
for m being FinSequence of NAT holds b1 . m = IDEAoperationA (IDEAoperationB m,k,n),k,n
proof end;
uniqueness
for b1, b2 being Function of MESSAGES , MESSAGES st ( for m being FinSequence of NAT holds b1 . m = IDEAoperationA (IDEAoperationB m,k,n),k,n ) & ( for m being FinSequence of NAT holds b2 . m = IDEAoperationA (IDEAoperationB m,k,n),k,n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def21 defines IDEA_PE IDEA_1:def 21 :
for n being non empty Nat
for k being FinSequence of NAT
for b3 being Function of MESSAGES , MESSAGES holds
( b3 = IDEA_PE k,n iff for m being FinSequence of NAT holds b3 . m = IDEAoperationA (IDEAoperationB m,k,n),k,n );

definition
let n be non empty Nat;
let k be FinSequence of NAT ;
func IDEA_QE k,n -> Function of MESSAGES , MESSAGES means :Def22: :: IDEA_1:def 22
for m being FinSequence of NAT holds it . m = IDEAoperationB (IDEAoperationA m,k,n),k,n;
existence
ex b1 being Function of MESSAGES , MESSAGES st
for m being FinSequence of NAT holds b1 . m = IDEAoperationB (IDEAoperationA m,k,n),k,n
proof end;
uniqueness
for b1, b2 being Function of MESSAGES , MESSAGES st ( for m being FinSequence of NAT holds b1 . m = IDEAoperationB (IDEAoperationA m,k,n),k,n ) & ( for m being FinSequence of NAT holds b2 . m = IDEAoperationB (IDEAoperationA m,k,n),k,n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines IDEA_QE IDEA_1:def 22 :
for n being non empty Nat
for k being FinSequence of NAT
for b3 being Function of MESSAGES , MESSAGES holds
( b3 = IDEA_QE k,n iff for m being FinSequence of NAT holds b3 . m = IDEAoperationB (IDEAoperationA m,k,n),k,n );

theorem Th34: :: IDEA_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for m, k1, k2 being FinSequence of NAT st (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 & k1 . 5 is_expressible_by n & k1 . 6 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 holds
((IDEA_Q k2,n) * (IDEA_P k1,n)) . m = m
proof end;

theorem Th35: :: IDEA_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for m, k1, k2 being FinSequence of NAT st (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 holds
((IDEA_QS k2,n) * (IDEA_PS k1,n)) . m = m
proof end;

theorem Th36: :: IDEA_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for m, k1, k2 being FinSequence of NAT st (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 & k1 . 5 is_expressible_by n & k1 . 6 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 holds
((IDEA_QE k2,n) * (IDEA_PE k1,n)) . m = m
proof end;

theorem Th37: :: IDEA_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for lk being Nat
for Key being Matrix of lk,6, NAT
for k being Nat holds IDEA_P_F Key,n,(k + 1) = (IDEA_P_F Key,n,k) ^ <*(IDEA_P (Line Key,(k + 1)),n)*>
proof end;

theorem Th38: :: IDEA_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for lk being Nat
for Key being Matrix of lk,6, NAT
for k being Nat holds IDEA_Q_F Key,n,(k + 1) = <*(IDEA_Q (Line Key,(k + 1)),n)*> ^ (IDEA_Q_F Key,n,k)
proof end;

theorem Th39: :: IDEA_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for lk being Nat
for Key being Matrix of lk,6, NAT
for k being Nat holds IDEA_P_F Key,n,k is FuncSeq-like FinSequence
proof end;

theorem Th40: :: IDEA_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for lk being Nat
for Key being Matrix of lk,6, NAT
for k being Nat holds IDEA_Q_F Key,n,k is FuncSeq-like FinSequence
proof end;

theorem Th41: :: IDEA_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for lk being Nat
for Key being Matrix of lk,6, NAT
for k being Nat st k <> 0 holds
IDEA_P_F Key,n,k is FuncSequence of MESSAGES , MESSAGES
proof end;

theorem Th42: :: IDEA_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for lk being Nat
for Key being Matrix of lk,6, NAT
for k being Nat st k <> 0 holds
IDEA_Q_F Key,n,k is FuncSequence of MESSAGES , MESSAGES
proof end;

theorem Th43: :: IDEA_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for M, m, k being FinSequence of NAT 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 end;

theorem Th44: :: IDEA_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for lk being Nat
for Key being Matrix of lk,6, NAT
for r being Nat holds
( rng (compose (IDEA_P_F Key,n,r),MESSAGES ) c= MESSAGES & dom (compose (IDEA_P_F Key,n,r),MESSAGES ) = MESSAGES )
proof end;

theorem :: IDEA_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for lk being Nat
for Key being Matrix of lk,6, NAT
for r being Nat holds
( rng (compose (IDEA_Q_F Key,n,r),MESSAGES ) c= MESSAGES & dom (compose (IDEA_Q_F Key,n,r),MESSAGES ) = MESSAGES )
proof end;

theorem Th46: :: IDEA_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for m being FinSequence of NAT
for lk being Nat
for Key being Matrix of lk,6, NAT
for r being Nat
for M being FinSequence of NAT st M = (compose (IDEA_P_F Key,n,r),MESSAGES ) . m & len m >= 4 holds
len M >= 4
proof end;

theorem Th47: :: IDEA_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for lk being Nat
for Key being Matrix of lk,6, NAT
for r being Nat
for M, m being FinSequence of NAT 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 end;

theorem Th48: :: IDEA_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for lk being Nat
for Key1, Key2 being Matrix of lk,6, NAT
for r being Nat
for m being FinSequence of NAT st lk >= r & (2 to_power n) + 1 is prime & len m >= 4 & m . 1 is_expressible_by n & m . 2 is_expressible_by n & m . 3 is_expressible_by n & m . 4 is_expressible_by n & ( for i being Nat st i <= r holds
( 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 end;

theorem :: IDEA_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being non empty Nat
for lk being Nat
for Key1, Key2 being Matrix of lk,6, NAT
for r being Nat
for ks1, ks2, ke1, ke2, m being FinSequence of NAT st lk >= r & (2 to_power n) + 1 is prime & len m >= 4 & m . 1 is_expressible_by n & m . 2 is_expressible_by n & m . 3 is_expressible_by n & m . 4 is_expressible_by n & ( for i being Nat st i <= r holds
( 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 & ke1 . 5 is_expressible_by n & ke1 . 6 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 end;