:: ALGSTR_3 semantic presentation

definition

attr a₁ is strict;
struct TernaryFieldStr -> ZeroStr ;
aggr TernaryFieldStr(# carrier, Zero, unity, ternary #) -> TernaryFieldStr ;
sel unity c₁ -> Element of the carrier of a₁;
sel ternary c₁ -> TriOp of the carrier of a₁;

end;

registration

cluster non empty TernaryFieldStr ;
existence

proof end;

end;

definition

let c₁ be non empty TernaryFieldStr ;
mode Scalar of a₁ is Element of a₁;

end;

definition

let c₁ be non empty TernaryFieldStr ;
let c₂, c₃, c₄ be Scalar of c₁;
func Tern c₂,c₃,c₄ -> Scalar of a₁ equals :: ALGSTR_3:def 1
the ternary of a₁ . a₂,a₃,a₄;
correctness ;

end;

:: deftheorem Def1 defines Tern ALGSTR_3:def 1 :

definition

let c₁ be non empty TernaryFieldStr ;
canceled;
func 1_ c₁ -> Scalar of a₁ equals :: ALGSTR_3:def 3
the unity of a₁;
correctness ;

end;

:: deftheorem Def2 ALGSTR_3:def 2 :

:: deftheorem Def3 defines 1_ ALGSTR_3:def 3 :

definition

func ternaryreal -> TriOp of REAL means :Def4: :: ALGSTR_3:def 4
for b₁, b₂, b₃ being Real holds a₁ . b₁,b₂,b₃ = (b₁ * b₂) + b₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines ternaryreal ALGSTR_3:def 4 :

definition

func TernaryFieldEx -> strict TernaryFieldStr equals :: ALGSTR_3:def 5
TernaryFieldStr(# REAL ,0,1,ternaryreal #);
correctness ;

end;

:: deftheorem Def5 defines TernaryFieldEx ALGSTR_3:def 5 :

registration

cluster TernaryFieldEx -> non empty strict ;
coherence

proof end;

end;

definition

let c₁, c₂, c₃ be Scalar of TernaryFieldEx ;
func tern c₁,c₂,c₃ -> Scalar of TernaryFieldEx equals :: ALGSTR_3:def 6
the ternary of TernaryFieldEx . a₁,a₂,a₃;
correctness ;

end;

:: deftheorem Def6 defines tern ALGSTR_3:def 6 :

theorem Th1: :: ALGSTR_3:1

canceled;

theorem Th2: :: ALGSTR_3:2

canceled;

theorem Th3: :: ALGSTR_3:3

for b₁, b₂, b₃, b₄ being Real st b₁ <> b₂ holds
ex b₅ being Real st (b₁ * b₅) + b₃ = (b₂ * b₅) + b₄

proof end;

theorem Th4: :: ALGSTR_3:4

canceled;

theorem Th5: :: ALGSTR_3:5

for b₁, b₂, b₃ being Scalar of TernaryFieldEx
for b₄, b₅, b₆ being Real st b₁ = b₄ & b₂ = b₅ & b₃ = b₆ holds
Tern b₁,b₂,b₃ = (b₄ * b₅) + b₆ by Def4;

theorem Th6: :: ALGSTR_3:6

0 = 0. TernaryFieldEx by RLVECT_1:def 2;

theorem Th7: :: ALGSTR_3:7

1 = 1_ TernaryFieldEx ;

Lemma5: for b₁ being Scalar of TernaryFieldEx holds Tern b₁,(1_ TernaryFieldEx ),(0. TernaryFieldEx ) = b₁

proof end;

Lemma6: for b₁ being Scalar of TernaryFieldEx holds Tern (1_ TernaryFieldEx ),b₁,(0. TernaryFieldEx ) = b₁

proof end;

Lemma7: for b₁, b₂ being Scalar of TernaryFieldEx holds Tern b₁,(0. TernaryFieldEx ),b₂ = b₂

proof end;

Lemma8: for b₁, b₂ being Scalar of TernaryFieldEx holds Tern (0. TernaryFieldEx ),b₁,b₂ = b₂

proof end;

Lemma9: for b₁, b₂, b₃ being Scalar of TernaryFieldEx ex b₄ being Scalar of TernaryFieldEx st Tern b₁,b₂,b₄ = b₃

proof end;

Lemma10: for b₁, b₂, b₃, b₄ being Scalar of TernaryFieldEx st Tern b₁,b₂,b₃ = Tern b₁,b₂,b₄ holds
b₃ = b₄

proof end;

Lemma11: for b₁, b₂ being Scalar of TernaryFieldEx st b₁ <> b₂ holds
for b₃, b₄ being Scalar of TernaryFieldEx ex b₅, b₆ being Scalar of TernaryFieldEx st
( Tern b₅,b₁,b₆ = b₃ & Tern b₅,b₂,b₆ = b₄ )

proof end;

Lemma12: for b₁, b₂ being Scalar of TernaryFieldEx st b₁ <> b₂ holds
for b₃, b₄ being Scalar of TernaryFieldEx ex b₅ being Scalar of TernaryFieldEx st Tern b₁,b₅,b₃ = Tern b₂,b₅,b₄

proof end;

Lemma13: for b₁, b₂, b₃, b₄, b₅, b₆ being Scalar of TernaryFieldEx st Tern b₃,b₁,b₅ = Tern b₄,b₁,b₆ & Tern b₃,b₂,b₅ = Tern b₄,b₂,b₆ & not b₁ = b₂ holds
b₃ = b₄

proof end;

definition

let c₁ be non empty TernaryFieldStr ;
attr a₁ is Ternary-Field-like means :Def7: :: ALGSTR_3:def 7
( 0. a₁ <> 1_ a₁ & ( for b₁ being Scalar of a₁ holds Tern b₁,(1_ a₁),(0. a₁) = b₁ ) & ( for b₁ being Scalar of a₁ holds Tern (1_ a₁),b₁,(0. a₁) = b₁ ) & ( for b₁, b₂ being Scalar of a₁ holds Tern b₁,(0. a₁),b₂ = b₂ ) & ( for b₁, b₂ being Scalar of a₁ holds Tern (0. a₁),b₁,b₂ = b₂ ) & ( for b₁, b₂, b₃ being Scalar of a₁ ex b₄ being Scalar of a₁ st Tern b₁,b₂,b₄ = b₃ ) & ( for b₁, b₂, b₃, b₄ being Scalar of a₁ st Tern b₁,b₂,b₃ = Tern b₁,b₂,b₄ holds
b₃ = b₄ ) & ( for b₁, b₂ being Scalar of a₁ st b₁ <> b₂ holds
for b₃, b₄ being Scalar of a₁ ex b₅, b₆ being Scalar of a₁ st
( Tern b₅,b₁,b₆ = b₃ & Tern b₅,b₂,b₆ = b₄ ) ) & ( for b₁, b₂ being Scalar of a₁ st b₁ <> b₂ holds
for b₃, b₄ being Scalar of a₁ ex b₅ being Scalar of a₁ st Tern b₁,b₅,b₃ = Tern b₂,b₅,b₄ ) & ( for b₁, b₂, b₃, b₄, b₅, b₆ being Scalar of a₁ st Tern b₃,b₁,b₅ = Tern b₄,b₁,b₆ & Tern b₃,b₂,b₅ = Tern b₄,b₂,b₆ & not b₁ = b₂ holds
b₃ = b₄ ) );

end;

:: deftheorem Def7 defines Ternary-Field-like ALGSTR_3:def 7 :

registration

cluster non empty strict Ternary-Field-like TernaryFieldStr ;
existence

proof end;

end;

definition

mode Ternary-Field is non empty Ternary-Field-like TernaryFieldStr ;

end;

theorem Th8: :: ALGSTR_3:8

for b₁ being Ternary-Field
for b₂, b₃, b₄, b₅, b₆, b₇ being Scalar of b₁ st b₂ <> b₃ & Tern b₄,b₂,b₅ = Tern b₆,b₂,b₇ & Tern b₄,b₃,b₅ = Tern b₆,b₃,b₇ holds
( b₄ = b₆ & b₅ = b₇ )

proof end;

theorem Th9: :: ALGSTR_3:9

canceled;

theorem Th10: :: ALGSTR_3:10

canceled;

theorem Th11: :: ALGSTR_3:11

for b₁ being Ternary-Field
for b₂ being Scalar of b₁ st b₂ <> 0. b₁ holds
for b₃, b₄ being Scalar of b₁ ex b₅ being Scalar of b₁ st Tern b₂,b₅,b₃ = b₄

proof end;

theorem Th12: :: ALGSTR_3:12

for b₁ being Ternary-Field
for b₂, b₃, b₄, b₅ being Scalar of b₁ st b₂ <> 0. b₁ & Tern b₂,b₃,b₄ = Tern b₂,b₅,b₄ holds
b₃ = b₅

proof end;

theorem Th13: :: ALGSTR_3:13

for b₁ being Ternary-Field
for b₂ being Scalar of b₁ st b₂ <> 0. b₁ holds
for b₃, b₄ being Scalar of b₁ ex b₅ being Scalar of b₁ st Tern b₅,b₂,b₃ = b₄

proof end;

theorem Th14: :: ALGSTR_3:14

for b₁ being Ternary-Field
for b₂, b₃, b₄, b₅ being Scalar of b₁ st b₂ <> 0. b₁ & Tern b₃,b₂,b₄ = Tern b₅,b₂,b₄ holds
b₃ = b₅

proof end;