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

definition
attr c1 is strict;
struct TernaryFieldStr -> ZeroStr ;
aggr TernaryFieldStr(# carrier, Zero, unity, ternary #) -> TernaryFieldStr ;
sel unity c1 -> Element of the carrier of c1;
sel ternary c1 -> TriOp of the carrier of c1;
end;

registration
cluster non empty TernaryFieldStr ;
existence
not for b1 being TernaryFieldStr holds b1 is empty
proof end;
end;

definition
let F be non empty TernaryFieldStr ;
mode Scalar of F is Element of F;
end;

definition
let F be non empty TernaryFieldStr ;
let a, b, c be Scalar of F;
func Tern a,b,c -> Scalar of F equals :: ALGSTR_3:def 1
the ternary of F . a,b,c;
correctness
coherence
the ternary of F . a,b,c is Scalar of F
;
;
end;

:: deftheorem defines Tern ALGSTR_3:def 1 :
for F being non empty TernaryFieldStr
for a, b, c being Scalar of F holds Tern a,b,c = the ternary of F . a,b,c;

definition
let F be non empty TernaryFieldStr ;
canceled;
func 1_ F -> Scalar of F equals :: ALGSTR_3:def 3
the unity of F;
correctness
coherence
the unity of F is Scalar of F
;
;
end;

:: deftheorem ALGSTR_3:def 2 :
canceled;

:: deftheorem defines 1_ ALGSTR_3:def 3 :
for F being non empty TernaryFieldStr holds 1_ F = the unity of F;

definition
func ternaryreal -> TriOp of REAL means :Def4: :: ALGSTR_3:def 4
for a, b, c being Real holds it . a,b,c = (a * b) + c;
existence
ex b1 being TriOp of REAL st
for a, b, c being Real holds b1 . a,b,c = (a * b) + c
proof end;
uniqueness
for b1, b2 being TriOp of REAL st ( for a, b, c being Real holds b1 . a,b,c = (a * b) + c ) & ( for a, b, c being Real holds b2 . a,b,c = (a * b) + c ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines ternaryreal ALGSTR_3:def 4 :
for b1 being TriOp of REAL holds
( b1 = ternaryreal iff for a, b, c being Real holds b1 . a,b,c = (a * b) + c );

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

:: deftheorem defines TernaryFieldEx ALGSTR_3:def 5 :
TernaryFieldEx = TernaryFieldStr(# REAL ,0,1,ternaryreal #);

registration
cluster TernaryFieldEx -> non empty strict ;
coherence
not TernaryFieldEx is empty
proof end;
end;

definition
let a, b, c be Scalar of TernaryFieldEx ;
func tern a,b,c -> Scalar of TernaryFieldEx equals :: ALGSTR_3:def 6
the ternary of TernaryFieldEx . a,b,c;
correctness
coherence
the ternary of TernaryFieldEx . a,b,c is Scalar of TernaryFieldEx
;
;
end;

:: deftheorem defines tern ALGSTR_3:def 6 :
for a, b, c being Scalar of TernaryFieldEx holds tern a,b,c = the ternary of TernaryFieldEx . a,b,c;

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

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

theorem Th3: :: ALGSTR_3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for u, u', v, v' being Real st u <> u' holds
ex x being Real st (u * x) + v = (u' * x) + v'
proof end;

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

theorem Th5: :: ALGSTR_3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for u, a, v being Scalar of TernaryFieldEx
for z, x, y being Real st u = z & a = x & v = y holds
Tern u,a,v = (z * x) + y by Def4;

theorem Th6: :: ALGSTR_3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
0 = 0. TernaryFieldEx by RLVECT_1:def 2;

theorem :: ALGSTR_3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
1 = 1_ TernaryFieldEx ;

Lm1: for a being Scalar of TernaryFieldEx holds Tern a,(1_ TernaryFieldEx ),(0. TernaryFieldEx ) = a
proof end;

Lm2: for a being Scalar of TernaryFieldEx holds Tern (1_ TernaryFieldEx ),a,(0. TernaryFieldEx ) = a
proof end;

Lm3: for a, b being Scalar of TernaryFieldEx holds Tern a,(0. TernaryFieldEx ),b = b
proof end;

Lm4: for a, b being Scalar of TernaryFieldEx holds Tern (0. TernaryFieldEx ),a,b = b
proof end;

Lm5: for u, a, b being Scalar of TernaryFieldEx ex v being Scalar of TernaryFieldEx st Tern u,a,v = b
proof end;

Lm6: for u, a, v, v' being Scalar of TernaryFieldEx st Tern u,a,v = Tern u,a,v' holds
v = v'
proof end;

Lm7: for a, a' being Scalar of TernaryFieldEx st a <> a' holds
for b, b' being Scalar of TernaryFieldEx ex u, v being Scalar of TernaryFieldEx st
( Tern u,a,v = b & Tern u,a',v = b' )
proof end;

Lm8: for u, u' being Scalar of TernaryFieldEx st u <> u' holds
for v, v' being Scalar of TernaryFieldEx ex a being Scalar of TernaryFieldEx st Tern u,a,v = Tern u',a,v'
proof end;

Lm9: for a, a', u, u', v, v' being Scalar of TernaryFieldEx st Tern u,a,v = Tern u',a,v' & Tern u,a',v = Tern u',a',v' & not a = a' holds
u = u'
proof end;

definition
let IT be non empty TernaryFieldStr ;
attr IT is Ternary-Field-like means :Def7: :: ALGSTR_3:def 7
( 0. IT <> 1_ IT & ( for a being Scalar of IT holds Tern a,(1_ IT),(0. IT) = a ) & ( for a being Scalar of IT holds Tern (1_ IT),a,(0. IT) = a ) & ( for a, b being Scalar of IT holds Tern a,(0. IT),b = b ) & ( for a, b being Scalar of IT holds Tern (0. IT),a,b = b ) & ( for u, a, b being Scalar of IT ex v being Scalar of IT st Tern u,a,v = b ) & ( for u, a, v, v' being Scalar of IT st Tern u,a,v = Tern u,a,v' holds
v = v' ) & ( for a, a' being Scalar of IT st a <> a' holds
for b, b' being Scalar of IT ex u, v being Scalar of IT st
( Tern u,a,v = b & Tern u,a',v = b' ) ) & ( for u, u' being Scalar of IT st u <> u' holds
for v, v' being Scalar of IT ex a being Scalar of IT st Tern u,a,v = Tern u',a,v' ) & ( for a, a', u, u', v, v' being Scalar of IT st Tern u,a,v = Tern u',a,v' & Tern u,a',v = Tern u',a',v' & not a = a' holds
u = u' ) );
end;

:: deftheorem Def7 defines Ternary-Field-like ALGSTR_3:def 7 :
for IT being non empty TernaryFieldStr holds
( IT is Ternary-Field-like iff ( 0. IT <> 1_ IT & ( for a being Scalar of IT holds Tern a,(1_ IT),(0. IT) = a ) & ( for a being Scalar of IT holds Tern (1_ IT),a,(0. IT) = a ) & ( for a, b being Scalar of IT holds Tern a,(0. IT),b = b ) & ( for a, b being Scalar of IT holds Tern (0. IT),a,b = b ) & ( for u, a, b being Scalar of IT ex v being Scalar of IT st Tern u,a,v = b ) & ( for u, a, v, v' being Scalar of IT st Tern u,a,v = Tern u,a,v' holds
v = v' ) & ( for a, a' being Scalar of IT st a <> a' holds
for b, b' being Scalar of IT ex u, v being Scalar of IT st
( Tern u,a,v = b & Tern u,a',v = b' ) ) & ( for u, u' being Scalar of IT st u <> u' holds
for v, v' being Scalar of IT ex a being Scalar of IT st Tern u,a,v = Tern u',a,v' ) & ( for a, a', u, u', v, v' being Scalar of IT st Tern u,a,v = Tern u',a,v' & Tern u,a',v = Tern u',a',v' & not a = a' holds
u = u' ) ) );

registration
cluster non empty strict Ternary-Field-like TernaryFieldStr ;
existence
ex b1 being non empty TernaryFieldStr st
( b1 is strict & b1 is Ternary-Field-like )
proof end;
end;

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

theorem :: ALGSTR_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Ternary-Field
for a, a', u, v, u', v' being Scalar of F st a <> a' & Tern u,a,v = Tern u',a,v' & Tern u,a',v = Tern u',a',v' holds
( u = u' & v = v' )
proof end;

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

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

theorem :: ALGSTR_3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Ternary-Field
for a being Scalar of F st a <> 0. F holds
for b, c being Scalar of F ex x being Scalar of F st Tern a,x,b = c
proof end;

theorem :: ALGSTR_3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Ternary-Field
for a, x, b, x' being Scalar of F st a <> 0. F & Tern a,x,b = Tern a,x',b holds
x = x'
proof end;

theorem :: ALGSTR_3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Ternary-Field
for a being Scalar of F st a <> 0. F holds
for b, c being Scalar of F ex x being Scalar of F st Tern x,a,b = c
proof end;

theorem :: ALGSTR_3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Ternary-Field
for a, x, b, x' being Scalar of F st a <> 0. F & Tern x,a,b = Tern x',a,b holds
x = x'
proof end;