:: IDEA_1 semantic presentation

Lemma1: for b₁, b₂ being Nat st b₁ <> 0 & b₁ < b₂ & b₂ is prime holds
b₁,b₂ are_relative_prime

proof end;

Lemma2: for b₁, b₂, b₃ being Nat st b₁ is prime & b₂ < b₁ & b₃ < b₁ & b₂ <> 0 holds
ex b₄ being Nat st (b₄ * b₂) mod b₁ = b₃

proof end;

theorem Th1: :: IDEA_1:1

for b₁, b₂, b₃ being Nat st b₂ is prime & b₁ < b₂ & b₃ < b₂ & b₁ <> 0 holds
ex b₄ being Nat st
( (b₄ * b₁) mod b₂ = b₃ & b₄ < b₂ )

proof end;

theorem Th2: :: IDEA_1:2

for b₁, b₂, b₃ being Nat st b₁ <> 0 & b₂ mod b₁ = b₃ mod b₁ & b₂ <= b₃ holds
ex b₄ being Nat st b₃ - b₂ = b₁ * b₄

proof end;

theorem Th3: :: IDEA_1:3

for b₁, b₂ being Nat holds b₁ - b₂ <= b₁

proof end;

theorem Th4: :: IDEA_1:4

for b₁, b₂, b₃ being Nat st b₂ <= b₃ holds
b₂ - b₁ <= b₃

proof end;

theorem Th5: :: IDEA_1:5

for b₁, b₂, b₃ being Nat st 0 < b₁ & 0 < b₂ & b₁ < b₃ & b₂ < b₃ & b₃ is prime holds
(b₁ * b₂) mod b₃ <> 0

proof end;

definition

let c₁ be Nat;
func ZERO c₁ -> Tuple of a₁,BOOLEAN equals :: IDEA_1:def 1
a₁ |-> FALSE ;
correctness by FINSEQ_2:132;

end;

:: deftheorem Def1 defines ZERO IDEA_1:def 1 :

definition

let c₁ be Nat;
let c₂, c₃ be Tuple of c₁,BOOLEAN ;
func c₂ 'xor' c₃ -> Tuple of a₁,BOOLEAN means :Def2: :: IDEA_1:def 2
for b₁ being Nat st b₁ in Seg a₁ holds
a₄ /. b₁ = (a₂ /. b₁) 'xor' (a₃ /. b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines 'xor' IDEA_1:def 2 :

theorem Th6: :: IDEA_1:6

canceled;

theorem Th7: :: IDEA_1:7

for b₁ being Nat
for b₂ being Tuple of b₁,BOOLEAN holds b₂ 'xor' b₂ = ZERO b₁

proof end;

theorem Th8: :: IDEA_1:8

for b₁ being Nat
for b₂, b₃ being Tuple of b₁,BOOLEAN holds b₂ 'xor' b₃ = b₃ 'xor' b₂

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Tuple of c₁,BOOLEAN ;
redefine func 'xor' as c₂ 'xor' c₃ -> Tuple of a₁,BOOLEAN ;
commutativity by Th8;

end;

theorem Th9: :: IDEA_1:9

for b₁ being Nat
for b₂ being Tuple of b₁,BOOLEAN holds (ZERO b₁) 'xor' b₂ = b₂

proof end;

theorem Th10: :: IDEA_1:10

for b₁ being Nat
for b₂, b₃, b₄ being Tuple of b₁,BOOLEAN holds (b₂ 'xor' b₃) 'xor' b₄ = b₂ 'xor' (b₃ 'xor' b₄)

proof end;

definition

let c₁, c₂ be Nat;
pred c₂ is_expressible_by c₁ means :Def3: :: IDEA_1:def 3
a₂ < 2 to_power a₁;

end;

:: deftheorem Def3 defines is_expressible_by IDEA_1:def 3 :

theorem Th11: :: IDEA_1:11

for b₁ being Nat holds b₁ -BinarySequence 0 = ZERO b₁

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Nat;
func ADD_MOD c₂,c₃,c₁ -> Nat equals :: IDEA_1:def 4
(a₂ + a₃) mod (2 to_power a₁);
coherence ;

end;

:: deftheorem Def4 defines ADD_MOD IDEA_1:def 4 :

definition

let c₁, c₂ be Nat;
assume E14: c₂ is_expressible_by c₁ ;
func NEG_N c₂,c₁ -> Nat equals :Def5: :: IDEA_1:def 5
(2 to_power a₁) - a₂;
coherence

proof end;

end;

:: deftheorem Def5 defines NEG_N IDEA_1:def 5 :

definition

let c₁, c₂ be Nat;
func NEG_MOD c₂,c₁ -> Nat equals :: IDEA_1:def 6
(NEG_N a₂,a₁) mod (2 to_power a₁);
coherence ;

end;

:: deftheorem Def6 defines NEG_MOD IDEA_1:def 6 :

theorem Th12: :: IDEA_1:12

for b₁, b₂ being Nat st b₁ is_expressible_by b₂ holds
ADD_MOD b₁,(NEG_MOD b₁,b₂),b₂ = 0

proof end;

theorem Th13: :: IDEA_1:13

for b₁, b₂, b₃ being Nat holds ADD_MOD b₁,b₂,b₃ = ADD_MOD b₂,b₁,b₃ ;

theorem Th14: :: IDEA_1:14

for b₁, b₂ being Nat st b₁ is_expressible_by b₂ holds
ADD_MOD 0,b₁,b₂ = b₁

proof end;

theorem Th15: :: IDEA_1:15

for b₁, b₂, b₃, b₄ being Nat holds ADD_MOD (ADD_MOD b₁,b₂,b₃),b₄,b₃ = ADD_MOD b₁,(ADD_MOD b₂,b₄,b₃),b₃

proof end;

theorem Th16: :: IDEA_1:16

for b₁, b₂, b₃ being Nat holds ADD_MOD b₁,b₂,b₃ is_expressible_by b₃

proof end;

theorem Th17: :: IDEA_1:17

for b₁, b₂ being Nat holds NEG_MOD b₁,b₂ is_expressible_by b₂

proof end;

definition

let c₁, c₂ be Nat;
func ChangeVal_1 c₂,c₁ -> Nat equals :Def7: :: IDEA_1:def 7
2 to_power a₁ if a₂ = 0
otherwise a₂;
correctness ;

end;

:: deftheorem Def7 defines ChangeVal_1 IDEA_1:def 7 :

theorem Th18: :: IDEA_1:18

for b₁, b₂ being Nat st b₁ is_expressible_by b₂ holds
( ChangeVal_1 b₁,b₂ <= 2 to_power b₂ & ChangeVal_1 b₁,b₂ > 0 )

proof end;

theorem Th19: :: IDEA_1:19

for b₁, b₂, b₃ being Nat st b₂ is_expressible_by b₁ & b₃ is_expressible_by b₁ & ChangeVal_1 b₂,b₁ = ChangeVal_1 b₃,b₁ holds
b₂ = b₃

proof end;

definition

let c₁, c₂ be Nat;
func ChangeVal_2 c₂,c₁ -> Nat equals :Def8: :: IDEA_1:def 8
0 if a₂ = 2 to_power a₁
otherwise a₂;
correctness ;

end;

:: deftheorem Def8 defines ChangeVal_2 IDEA_1:def 8 :

theorem Th20: :: IDEA_1:20

for b₁, b₂ being Nat st b₁ is_expressible_by b₂ holds
ChangeVal_2 b₁,b₂ is_expressible_by b₂

proof end;

theorem Th21: :: IDEA_1:21

for b₁, b₂, b₃ being Nat st b₂ <> 0 & b₃ <> 0 & ChangeVal_2 b₂,b₁ = ChangeVal_2 b₃,b₁ holds
b₂ = b₃

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Nat;
func MUL_MOD c₂,c₃,c₁ -> Nat equals :: IDEA_1:def 9
ChangeVal_2 (((ChangeVal_1 a₂,a₁) * (ChangeVal_1 a₃,a₁)) mod ((2 to_power a₁) + 1)),a₁;
coherence ;

end;

:: deftheorem Def9 defines MUL_MOD IDEA_1:def 9 :

definition

let c₁ be non empty Nat;
let c₂ be Nat;
assume E24: ( c₂ is_expressible_by c₁ & (2 to_power c₁) + 1 is prime ) ;
func INV_MOD c₂,c₁ -> Nat means :Def10: :: IDEA_1:def 10
( MUL_MOD a₂,a₃,a₁ = 1 & a₃ is_expressible_by a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines INV_MOD IDEA_1:def 10 :

theorem Th22: :: IDEA_1:22

for b₁, b₂, b₃ being Nat holds MUL_MOD b₁,b₂,b₃ = MUL_MOD b₂,b₁,b₃ ;

theorem Th23: :: IDEA_1:23

for b₁, b₂ being Nat st b₁ is_expressible_by b₂ holds
MUL_MOD 1,b₁,b₂ = b₁

proof end;

theorem Th24: :: IDEA_1:24

for b₁, b₂, b₃, b₄ being Nat st (2 to_power b₁) + 1 is prime & b₂ is_expressible_by b₁ & b₃ is_expressible_by b₁ & b₄ is_expressible_by b₁ holds
MUL_MOD (MUL_MOD b₂,b₃,b₁),b₄,b₁ = MUL_MOD b₂,(MUL_MOD b₃,b₄,b₁),b₁

proof end;

theorem Th25: :: IDEA_1:25

for b₁, b₂, b₃ being Nat holds MUL_MOD b₁,b₂,b₃ is_expressible_by b₃

proof end;

theorem Th26: :: IDEA_1:26

for b₁, b₂ being Nat st ChangeVal_2 b₁,b₂ = 1 holds
b₁ = 1

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be FinSequence of NAT ;
func IDEAoperationA c₂,c₃,c₁ -> FinSequence of NAT means :Def11: :: IDEA_1:def 11
( len a₄ = len a₂ & ( for b₁ being Nat st b₁ in dom a₂ holds
( ( b₁ = 1 implies a₄ . b₁ = MUL_MOD (a₂ . 1),(a₃ . 1),a₁ ) & ( b₁ = 2 implies a₄ . b₁ = ADD_MOD (a₂ . 2),(a₃ . 2),a₁ ) & ( b₁ = 3 implies a₄ . b₁ = ADD_MOD (a₂ . 3),(a₃ . 3),a₁ ) & ( b₁ = 4 implies a₄ . b₁ = MUL_MOD (a₂ . 4),(a₃ . 4),a₁ ) & ( b₁ <> 1 & b₁ <> 2 & b₁ <> 3 & b₁ <> 4 implies a₄ . b₁ = a₂ . b₁ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines IDEAoperationA IDEA_1:def 11 :

definition

let c₁ be non empty Nat;
let c₂, c₃ be FinSequence of NAT ;
func IDEAoperationB c₂,c₃,c₁ -> FinSequence of NAT means :Def12: :: IDEA_1:def 12
( len a₄ = len a₂ & ( for b₁ being Nat st b₁ in dom a₂ holds
( ( b₁ = 1 implies a₄ . b₁ = Absval ((a₁ -BinarySequence (a₂ . 1)) 'xor' (a₁ -BinarySequence (MUL_MOD (ADD_MOD (MUL_MOD (Absval ((a₁ -BinarySequence (a₂ . 1)) 'xor' (a₁ -BinarySequence (a₂ . 3)))),(a₃ . 5),a₁),(Absval ((a₁ -BinarySequence (a₂ . 2)) 'xor' (a₁ -BinarySequence (a₂ . 4)))),a₁),(a₃ . 6),a₁))) ) & ( b₁ = 2 implies a₄ . b₁ = Absval ((a₁ -BinarySequence (a₂ . 2)) 'xor' (a₁ -BinarySequence (ADD_MOD (MUL_MOD (Absval ((a₁ -BinarySequence (a₂ . 1)) 'xor' (a₁ -BinarySequence (a₂ . 3)))),(a₃ . 5),a₁),(MUL_MOD (ADD_MOD (MUL_MOD (Absval ((a₁ -BinarySequence (a₂ . 1)) 'xor' (a₁ -BinarySequence (a₂ . 3)))),(a₃ . 5),a₁),(Absval ((a₁ -BinarySequence (a₂ . 2)) 'xor' (a₁ -BinarySequence (a₂ . 4)))),a₁),(a₃ . 6),a₁),a₁))) ) & ( b₁ = 3 implies a₄ . b₁ = Absval ((a₁ -BinarySequence (a₂ . 3)) 'xor' (a₁ -BinarySequence (MUL_MOD (ADD_MOD (MUL_MOD (Absval ((a₁ -BinarySequence (a₂ . 1)) 'xor' (a₁ -BinarySequence (a₂ . 3)))),(a₃ . 5),a₁),(Absval ((a₁ -BinarySequence (a₂ . 2)) 'xor' (a₁ -BinarySequence (a₂ . 4)))),a₁),(a₃ . 6),a₁))) ) & ( b₁ = 4 implies a₄ . b₁ = Absval ((a₁ -BinarySequence (a₂ . 4)) 'xor' (a₁ -BinarySequence (ADD_MOD (MUL_MOD (Absval ((a₁ -BinarySequence (a₂ . 1)) 'xor' (a₁ -BinarySequence (a₂ . 3)))),(a₃ . 5),a₁),(MUL_MOD (ADD_MOD (MUL_MOD (Absval ((a₁ -BinarySequence (a₂ . 1)) 'xor' (a₁ -BinarySequence (a₂ . 3)))),(a₃ . 5),a₁),(Absval ((a₁ -BinarySequence (a₂ . 2)) 'xor' (a₁ -BinarySequence (a₂ . 4)))),a₁),(a₃ . 6),a₁),a₁))) ) & ( b₁ <> 1 & b₁ <> 2 & b₁ <> 3 & b₁ <> 4 implies a₄ . b₁ = a₂ . b₁ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines IDEAoperationB IDEA_1:def 12 :

definition

let c₁ be FinSequence of NAT ;
func IDEAoperationC c₁ -> FinSequence of NAT means :Def13: :: IDEA_1:def 13
( len a₂ = len a₁ & ( for b₁ being Nat st b₁ in dom a₁ holds
a₂ . b₁ = IFEQ b₁,2,(a₁ . 3),(IFEQ b₁,3,(a₁ . 2),(a₁ . b₁)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines IDEAoperationC IDEA_1:def 13 :

theorem Th27: :: IDEA_1:27

for b₁ being Nat
for b₂, b₃ being FinSequence of NAT st len b₂ >= 4 holds
( (IDEAoperationA b₂,b₃,b₁) . 1 is_expressible_by b₁ & (IDEAoperationA b₂,b₃,b₁) . 2 is_expressible_by b₁ & (IDEAoperationA b₂,b₃,b₁) . 3 is_expressible_by b₁ & (IDEAoperationA b₂,b₃,b₁) . 4 is_expressible_by b₁ )

proof end;

theorem Th28: :: IDEA_1:28

for b₁, b₂ being FinSequence of NAT
for b₃ being non empty Nat st len b₁ >= 4 holds
( (IDEAoperationB b₁,b₂,b₃) . 1 is_expressible_by b₃ & (IDEAoperationB b₁,b₂,b₃) . 2 is_expressible_by b₃ & (IDEAoperationB b₁,b₂,b₃) . 3 is_expressible_by b₃ & (IDEAoperationB b₁,b₂,b₃) . 4 is_expressible_by b₃ )

proof end;

Lemma33: for b₁ being FinSequence of NAT
for b₂ being Nat st b₂ = 2 & b₂ in dom b₁ holds
(IDEAoperationC b₁) . b₂ = b₁ . 3

proof end;

Lemma34: for b₁ being FinSequence of NAT
for b₂ being Nat st b₂ = 3 & b₂ in dom b₁ holds
(IDEAoperationC b₁) . b₂ = b₁ . 2

proof end;

Lemma35: for b₁ being FinSequence of NAT
for b₂ being Nat st b₂ <> 2 & b₂ <> 3 & b₂ in dom b₁ holds
(IDEAoperationC b₁) . b₂ = b₁ . b₂

proof end;

theorem Th29: :: IDEA_1:29

for b₁ being Nat
for b₂ being FinSequence of NAT st len b₂ >= 4 & b₂ . 1 is_expressible_by b₁ & b₂ . 2 is_expressible_by b₁ & b₂ . 3 is_expressible_by b₁ & b₂ . 4 is_expressible_by b₁ holds
( (IDEAoperationC b₂) . 1 is_expressible_by b₁ & (IDEAoperationC b₂) . 2 is_expressible_by b₁ & (IDEAoperationC b₂) . 3 is_expressible_by b₁ & (IDEAoperationC b₂) . 4 is_expressible_by b₁ )

proof end;

theorem Th30: :: IDEA_1:30

for b₁ being non empty Nat
for b₂, b₃, b₄ being FinSequence of NAT st (2 to_power b₁) + 1 is prime & len b₂ >= 4 & b₂ . 1 is_expressible_by b₁ & b₂ . 2 is_expressible_by b₁ & b₂ . 3 is_expressible_by b₁ & b₂ . 4 is_expressible_by b₁ & b₃ . 1 is_expressible_by b₁ & b₃ . 2 is_expressible_by b₁ & b₃ . 3 is_expressible_by b₁ & b₃ . 4 is_expressible_by b₁ & b₄ . 1 = INV_MOD (b₃ . 1),b₁ & b₄ . 2 = NEG_MOD (b₃ . 2),b₁ & b₄ . 3 = NEG_MOD (b₃ . 3),b₁ & b₄ . 4 = INV_MOD (b₃ . 4),b₁ holds
IDEAoperationA (IDEAoperationA b₂,b₃,b₁),b₄,b₁ = b₂

proof end;

theorem Th31: :: IDEA_1:31

for b₁ being non empty Nat
for b₂, b₃, b₄ being FinSequence of NAT st (2 to_power b₁) + 1 is prime & len b₂ >= 4 & b₂ . 1 is_expressible_by b₁ & b₂ . 2 is_expressible_by b₁ & b₂ . 3 is_expressible_by b₁ & b₂ . 4 is_expressible_by b₁ & b₃ . 1 is_expressible_by b₁ & b₃ . 2 is_expressible_by b₁ & b₃ . 3 is_expressible_by b₁ & b₃ . 4 is_expressible_by b₁ & b₄ . 1 = INV_MOD (b₃ . 1),b₁ & b₄ . 2 = NEG_MOD (b₃ . 3),b₁ & b₄ . 3 = NEG_MOD (b₃ . 2),b₁ & b₄ . 4 = INV_MOD (b₃ . 4),b₁ holds
IDEAoperationA (IDEAoperationC (IDEAoperationA (IDEAoperationC b₂),b₃,b₁)),b₄,b₁ = b₂

proof end;

theorem Th32: :: IDEA_1:32

proof end;

theorem Th33: :: IDEA_1:33

for b₁ being FinSequence of NAT st len b₁ >= 4 holds
IDEAoperationC (IDEAoperationC b₁) = b₁

proof end;

definition

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

end;

:: deftheorem Def14 defines MESSAGES IDEA_1:def 14 :

registration

cluster MESSAGES -> non empty ;
coherence ;

end;

registration

cluster MESSAGES -> non empty functional ;
coherence ;

end;

registration

cluster -> FinSequence-like Element of MESSAGES ;
coherence by FINSEQ_1:def 11;

end;

definition

let c₁ be non empty Nat;
let c₂ be FinSequence of NAT ;
func IDEA_P c₂,c₁ -> Function of MESSAGES , MESSAGES means :Def15: :: IDEA_1:def 15
for b₁ being FinSequence of NAT holds a₃ . b₁ = IDEAoperationA (IDEAoperationC (IDEAoperationB b₁,a₂,a₁)),a₂,a₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines IDEA_P IDEA_1:def 15 :

definition

let c₁ be non empty Nat;
let c₂ be FinSequence of NAT ;
func IDEA_Q c₂,c₁ -> Function of MESSAGES , MESSAGES means :Def16: :: IDEA_1:def 16
for b₁ being FinSequence of NAT holds a₃ . b₁ = IDEAoperationB (IDEAoperationA (IDEAoperationC b₁),a₂,a₁),a₂,a₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines IDEA_Q IDEA_1:def 16 :

definition

let c₁, c₂ be Nat;
let c₃ be non empty Nat;
let c₄ be Matrix of c₂,6, NAT ;
func IDEA_P_F c₄,c₃,c₁ -> FinSequence means :Def17: :: IDEA_1:def 17
( len a₅ = a₁ & ( for b₁ being Nat st b₁ in dom a₅ holds
a₅ . b₁ = IDEA_P (Line a₄,b₁),a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines IDEA_P_F IDEA_1:def 17 :

registration

let c₁, c₂ be Nat;
let c₃ be non empty Nat;
let c₄ be Matrix of c₂,6, NAT ;
cluster IDEA_P_F a₄,a₃,a₁ -> Function-yielding ;
coherence

proof end;

end;

definition

let c₁, c₂ be Nat;
let c₃ be non empty Nat;
let c₄ be Matrix of c₂,6, NAT ;
func IDEA_Q_F c₄,c₃,c₁ -> FinSequence means :Def18: :: IDEA_1:def 18
( len a₅ = a₁ & ( for b₁ being Nat st b₁ in dom a₅ holds
a₅ . b₁ = IDEA_Q (Line a₄,((a₁ -' b₁) + 1)),a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines IDEA_Q_F IDEA_1:def 18 :

registration

let c₁, c₂ be Nat;
let c₃ be non empty Nat;
let c₄ be Matrix of c₂,6, NAT ;
cluster IDEA_Q_F a₄,a₃,a₁ -> Function-yielding ;
coherence

proof end;

end;

definition

let c₁ be FinSequence of NAT ;
let c₂ be Nat;
func IDEA_PS c₁,c₂ -> Function of MESSAGES , MESSAGES means :Def19: :: IDEA_1:def 19
for b₁ being FinSequence of NAT holds a₃ . b₁ = IDEAoperationA b₁,a₁,a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines IDEA_PS IDEA_1:def 19 :

definition

let c₁ be FinSequence of NAT ;
let c₂ be Nat;
func IDEA_QS c₁,c₂ -> Function of MESSAGES , MESSAGES means :Def20: :: IDEA_1:def 20
for b₁ being FinSequence of NAT holds a₃ . b₁ = IDEAoperationA b₁,a₁,a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines IDEA_QS IDEA_1:def 20 :

definition

let c₁ be non empty Nat;
let c₂ be FinSequence of NAT ;
func IDEA_PE c₂,c₁ -> Function of MESSAGES , MESSAGES means :Def21: :: IDEA_1:def 21
for b₁ being FinSequence of NAT holds a₃ . b₁ = IDEAoperationA (IDEAoperationB b₁,a₂,a₁),a₂,a₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def21 defines IDEA_PE IDEA_1:def 21 :

definition

let c₁ be non empty Nat;
let c₂ be FinSequence of NAT ;
func IDEA_QE c₂,c₁ -> Function of MESSAGES , MESSAGES means :Def22: :: IDEA_1:def 22
for b₁ being FinSequence of NAT holds a₃ . b₁ = IDEAoperationB (IDEAoperationA b₁,a₂,a₁),a₂,a₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def22 defines IDEA_QE IDEA_1:def 22 :

theorem Th34: :: IDEA_1:34

for b₁ being non empty Nat
for b₂, b₃, b₄ being FinSequence of NAT st (2 to_power b₁) + 1 is prime & len b₂ >= 4 & b₂ . 1 is_expressible_by b₁ & b₂ . 2 is_expressible_by b₁ & b₂ . 3 is_expressible_by b₁ & b₂ . 4 is_expressible_by b₁ & b₃ . 1 is_expressible_by b₁ & b₃ . 2 is_expressible_by b₁ & b₃ . 3 is_expressible_by b₁ & b₃ . 4 is_expressible_by b₁ & b₃ . 5 is_expressible_by b₁ & b₃ . 6 is_expressible_by b₁ & b₄ . 1 = INV_MOD (b₃ . 1),b₁ & b₄ . 2 = NEG_MOD (b₃ . 3),b₁ & b₄ . 3 = NEG_MOD (b₃ . 2),b₁ & b₄ . 4 = INV_MOD (b₃ . 4),b₁ & b₄ . 5 = b₃ . 5 & b₄ . 6 = b₃ . 6 holds
((IDEA_Q b₄,b₁) * (IDEA_P b₃,b₁)) . b₂ = b₂

proof end;

theorem Th35: :: IDEA_1:35

for b₁ being non empty Nat
for b₂, b₃, b₄ being FinSequence of NAT st (2 to_power b₁) + 1 is prime & len b₂ >= 4 & b₂ . 1 is_expressible_by b₁ & b₂ . 2 is_expressible_by b₁ & b₂ . 3 is_expressible_by b₁ & b₂ . 4 is_expressible_by b₁ & b₃ . 1 is_expressible_by b₁ & b₃ . 2 is_expressible_by b₁ & b₃ . 3 is_expressible_by b₁ & b₃ . 4 is_expressible_by b₁ & b₄ . 1 = INV_MOD (b₃ . 1),b₁ & b₄ . 2 = NEG_MOD (b₃ . 2),b₁ & b₄ . 3 = NEG_MOD (b₃ . 3),b₁ & b₄ . 4 = INV_MOD (b₃ . 4),b₁ holds
((IDEA_QS b₄,b₁) * (IDEA_PS b₃,b₁)) . b₂ = b₂

proof end;

theorem Th36: :: IDEA_1:36

for b₁ being non empty Nat
for b₂, b₃, b₄ being FinSequence of NAT st (2 to_power b₁) + 1 is prime & len b₂ >= 4 & b₂ . 1 is_expressible_by b₁ & b₂ . 2 is_expressible_by b₁ & b₂ . 3 is_expressible_by b₁ & b₂ . 4 is_expressible_by b₁ & b₃ . 1 is_expressible_by b₁ & b₃ . 2 is_expressible_by b₁ & b₃ . 3 is_expressible_by b₁ & b₃ . 4 is_expressible_by b₁ & b₃ . 5 is_expressible_by b₁ & b₃ . 6 is_expressible_by b₁ & b₄ . 1 = INV_MOD (b₃ . 1),b₁ & b₄ . 2 = NEG_MOD (b₃ . 2),b₁ & b₄ . 3 = NEG_MOD (b₃ . 3),b₁ & b₄ . 4 = INV_MOD (b₃ . 4),b₁ & b₄ . 5 = b₃ . 5 & b₄ . 6 = b₃ . 6 holds
((IDEA_QE b₄,b₁) * (IDEA_PE b₃,b₁)) . b₂ = b₂

proof end;

theorem Th37: :: IDEA_1:37

for b₁ being non empty Nat
for b₂ being Nat
for b₃ being Matrix of b₂,6, NAT
for b₄ being Nat holds IDEA_P_F b₃,b₁,(b₄ + 1) = (IDEA_P_F b₃,b₁,b₄) ^ <*(IDEA_P (Line b₃,(b₄ + 1)),b₁)*>

proof end;

theorem Th38: :: IDEA_1:38

for b₁ being non empty Nat
for b₂ being Nat
for b₃ being Matrix of b₂,6, NAT
for b₄ being Nat holds IDEA_Q_F b₃,b₁,(b₄ + 1) = <*(IDEA_Q (Line b₃,(b₄ + 1)),b₁)*> ^ (IDEA_Q_F b₃,b₁,b₄)

proof end;

theorem Th39: :: IDEA_1:39

for b₁ being non empty Nat
for b₂ being Nat
for b₃ being Matrix of b₂,6, NAT
for b₄ being Nat holds IDEA_P_F b₃,b₁,b₄ is FuncSeq-like FinSequence

proof end;

theorem Th40: :: IDEA_1:40

for b₁ being non empty Nat
for b₂ being Nat
for b₃ being Matrix of b₂,6, NAT
for b₄ being Nat holds IDEA_Q_F b₃,b₁,b₄ is FuncSeq-like FinSequence

proof end;

theorem Th41: :: IDEA_1:41

for b₁ being non empty Nat
for b₂ being Nat
for b₃ being Matrix of b₂,6, NAT
for b₄ being Nat st b₄ <> 0 holds
IDEA_P_F b₃,b₁,b₄ is FuncSequence of MESSAGES , MESSAGES

proof end;

theorem Th42: :: IDEA_1:42

for b₁ being non empty Nat
for b₂ being Nat
for b₃ being Matrix of b₂,6, NAT
for b₄ being Nat st b₄ <> 0 holds
IDEA_Q_F b₃,b₁,b₄ is FuncSequence of MESSAGES , MESSAGES

proof end;

theorem Th43: :: IDEA_1:43

for b₁ being non empty Nat
for b₂, b₃, b₄ being FinSequence of NAT st b₂ = (IDEA_P b₄,b₁) . b₃ & len b₃ >= 4 holds
( len b₂ >= 4 & b₂ . 1 is_expressible_by b₁ & b₂ . 2 is_expressible_by b₁ & b₂ . 3 is_expressible_by b₁ & b₂ . 4 is_expressible_by b₁ )

proof end;

theorem Th44: :: IDEA_1:44

for b₁ being non empty Nat
for b₂ being Nat
for b₃ being Matrix of b₂,6, NAT
for b₄ being Nat holds
( rng (compose (IDEA_P_F b₃,b₁,b₄),MESSAGES ) c= MESSAGES & dom (compose (IDEA_P_F b₃,b₁,b₄),MESSAGES ) = MESSAGES )

proof end;

theorem Th45: :: IDEA_1:45

for b₁ being non empty Nat
for b₂ being Nat
for b₃ being Matrix of b₂,6, NAT
for b₄ being Nat holds
( rng (compose (IDEA_Q_F b₃,b₁,b₄),MESSAGES ) c= MESSAGES & dom (compose (IDEA_Q_F b₃,b₁,b₄),MESSAGES ) = MESSAGES )

proof end;

theorem Th46: :: IDEA_1:46

for b₁ being non empty Nat
for b₂ being FinSequence of NAT
for b₃ being Nat
for b₄ being Matrix of b₃,6, NAT
for b₅ being Nat
for b₆ being FinSequence of NAT st b₆ = (compose (IDEA_P_F b₄,b₁,b₅),MESSAGES ) . b₂ & len b₂ >= 4 holds
len b₆ >= 4

proof end;

theorem Th47: :: IDEA_1:47

for b₁ being non empty Nat
for b₂ being Nat
for b₃ being Matrix of b₂,6, NAT
for b₄ being Nat
for b₅, b₆ being FinSequence of NAT st b₅ = (compose (IDEA_P_F b₃,b₁,b₄),MESSAGES ) . b₆ & len b₆ >= 4 & b₆ . 1 is_expressible_by b₁ & b₆ . 2 is_expressible_by b₁ & b₆ . 3 is_expressible_by b₁ & b₆ . 4 is_expressible_by b₁ holds
( len b₅ >= 4 & b₅ . 1 is_expressible_by b₁ & b₅ . 2 is_expressible_by b₁ & b₅ . 3 is_expressible_by b₁ & b₅ . 4 is_expressible_by b₁ )

proof end;

theorem Th48: :: IDEA_1:48

for b₁ being non empty Nat
for b₂ being Nat
for b₃, b₄ being Matrix of b₂,6, NAT
for b₅ being Nat
for b₆ being FinSequence of NAT st b₂ >= b₅ & (2 to_power b₁) + 1 is prime & len b₆ >= 4 & b₆ . 1 is_expressible_by b₁ & b₆ . 2 is_expressible_by b₁ & b₆ . 3 is_expressible_by b₁ & b₆ . 4 is_expressible_by b₁ & ( for b₇ being Nat st b₇ <= b₅ holds
( b₃ * b₇,1 is_expressible_by b₁ & b₃ * b₇,2 is_expressible_by b₁ & b₃ * b₇,3 is_expressible_by b₁ & b₃ * b₇,4 is_expressible_by b₁ & b₃ * b₇,5 is_expressible_by b₁ & b₃ * b₇,6 is_expressible_by b₁ & b₄ * b₇,1 is_expressible_by b₁ & b₄ * b₇,2 is_expressible_by b₁ & b₄ * b₇,3 is_expressible_by b₁ & b₄ * b₇,4 is_expressible_by b₁ & b₄ * b₇,5 is_expressible_by b₁ & b₄ * b₇,6 is_expressible_by b₁ & b₄ * b₇,1 = INV_MOD (b₃ * b₇,1),b₁ & b₄ * b₇,2 = NEG_MOD (b₃ * b₇,3),b₁ & b₄ * b₇,3 = NEG_MOD (b₃ * b₇,2),b₁ & b₄ * b₇,4 = INV_MOD (b₃ * b₇,4),b₁ & b₃ * b₇,5 = b₄ * b₇,5 & b₃ * b₇,6 = b₄ * b₇,6 ) ) holds
(compose ((IDEA_P_F b₃,b₁,b₅) ^ (IDEA_Q_F b₄,b₁,b₅)),MESSAGES ) . b₆ = b₆

proof end;

theorem Th49: :: IDEA_1:49

for b₁ being non empty Nat
for b₂ being Nat
for b₃, b₄ being Matrix of b₂,6, NAT
for b₅ being Nat
for b₆, b₇, b₈, b₉, b₁₀ being FinSequence of NAT st b₂ >= b₅ & (2 to_power b₁) + 1 is prime & len b₁₀ >= 4 & b₁₀ . 1 is_expressible_by b₁ & b₁₀ . 2 is_expressible_by b₁ & b₁₀ . 3 is_expressible_by b₁ & b₁₀ . 4 is_expressible_by b₁ & ( for b₁₁ being Nat st b₁₁ <= b₅ holds
( b₃ * b₁₁,1 is_expressible_by b₁ & b₃ * b₁₁,2 is_expressible_by b₁ & b₃ * b₁₁,3 is_expressible_by b₁ & b₃ * b₁₁,4 is_expressible_by b₁ & b₃ * b₁₁,5 is_expressible_by b₁ & b₃ * b₁₁,6 is_expressible_by b₁ & b₄ * b₁₁,1 is_expressible_by b₁ & b₄ * b₁₁,2 is_expressible_by b₁ & b₄ * b₁₁,3 is_expressible_by b₁ & b₄ * b₁₁,4 is_expressible_by b₁ & b₄ * b₁₁,5 is_expressible_by b₁ & b₄ * b₁₁,6 is_expressible_by b₁ & b₄ * b₁₁,1 = INV_MOD (b₃ * b₁₁,1),b₁ & b₄ * b₁₁,2 = NEG_MOD (b₃ * b₁₁,3),b₁ & b₄ * b₁₁,3 = NEG_MOD (b₃ * b₁₁,2),b₁ & b₄ * b₁₁,4 = INV_MOD (b₃ * b₁₁,4),b₁ & b₃ * b₁₁,5 = b₄ * b₁₁,5 & b₃ * b₁₁,6 = b₄ * b₁₁,6 ) ) & b₆ . 1 is_expressible_by b₁ & b₆ . 2 is_expressible_by b₁ & b₆ . 3 is_expressible_by b₁ & b₆ . 4 is_expressible_by b₁ & b₇ . 1 = INV_MOD (b₆ . 1),b₁ & b₇ . 2 = NEG_MOD (b₆ . 2),b₁ & b₇ . 3 = NEG_MOD (b₆ . 3),b₁ & b₇ . 4 = INV_MOD (b₆ . 4),b₁ & b₈ . 1 is_expressible_by b₁ & b₈ . 2 is_expressible_by b₁ & b₈ . 3 is_expressible_by b₁ & b₈ . 4 is_expressible_by b₁ & b₈ . 5 is_expressible_by b₁ & b₈ . 6 is_expressible_by b₁ & b₉ . 1 = INV_MOD (b₈ . 1),b₁ & b₉ . 2 = NEG_MOD (b₈ . 2),b₁ & b₉ . 3 = NEG_MOD (b₈ . 3),b₁ & b₉ . 4 = INV_MOD (b₈ . 4),b₁ & b₉ . 5 = b₈ . 5 & b₉ . 6 = b₈ . 6 holds
((IDEA_QS b₇,b₁) * ((compose (IDEA_Q_F b₄,b₁,b₅),MESSAGES ) * ((IDEA_QE b₉,b₁) * ((IDEA_PE b₈,b₁) * ((compose (IDEA_P_F b₃,b₁,b₅),MESSAGES ) * (IDEA_PS b₆,b₁)))))) . b₁₀ = b₁₀

proof end;