:: ALGSTR_3  semantic presentation begin  definitionattr "c1" is  :::"strict"::: ; struct  :::"TernaryFieldStr":::  ->    ($#l4_struct_0 :::"ZeroOneStr"::: )  ; aggr :::"TernaryFieldStr":::(# :::"carrier":::, :::"ZeroF":::, :::"OneF":::, :::"TernOp"::: #) ->    ($#l1_algstr_3 :::"TernaryFieldStr"::: )  ; sel  :::"TernOp"::: "c1" ->   ($#m1_subset_1 :::"TriOp":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "c1"); end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   for    ($#l1_algstr_3 :::"TernaryFieldStr"::: )  ; 
end; 


definitionlet "F" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_algstr_3 :::"TernaryFieldStr"::: )  ; mode Scalar of "F" is   ($#m1_subset_1 :::"Element":::) "of" "F"; end; 




definitionlet "F" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_algstr_3 :::"TernaryFieldStr"::: )  ; let "a", "b", "c" be   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Const "F")); func  :::"Tern":::  "(" "a" "," "b" "," "c" ")"  ->   ($#m1_subset_1 :::"Scalar":::) "of" "F" equals :: ALGSTR_3:def 1 (Set (Set  "the"  ($#u1_algstr_3 :::"TernOp"::: )  "of" "F")  ($#k2_multop_1 :::"."::: )   "(" "a" "," "b" "," "c" ")" ); end; 








:: deftheorem    defines :::"Tern"::: ALGSTR_3:def 1 :  (Bool  "for" (Set (Var "F")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_algstr_3 :::"TernaryFieldStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "F")) "holds"  (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_3 :::"TernOp"::: )  "of" (Set (Var "F")))  ($#k2_multop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )))); 
 definitionfunc  :::"ternaryreal":::  ->   ($#m1_subset_1 :::"TriOp":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) means :: ALGSTR_3:def 2 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set it  ($#k2_multop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "c"))))); end; 




:: deftheorem    defines :::"ternaryreal"::: ALGSTR_3:def 2 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"TriOp":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_algstr_3 :::"ternaryreal"::: )  )) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "b1"))  ($#k2_multop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "c")))))  ")" )); 
 definitionfunc  :::"TernaryFieldEx":::  ->   ($#v1_algstr_3 :::"strict"::: )     ($#l1_algstr_3 :::"TernaryFieldStr"::: )   equals :: ALGSTR_3:def 3 (Set   ($#g1_algstr_3 :::"TernaryFieldStr"::: )  "(#"  (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set  ($#k2_algstr_3 :::"ternaryreal"::: ) ) "#)" ); end; 




:: deftheorem    defines :::"TernaryFieldEx"::: ALGSTR_3:def 3 :  (Bool (Set   ($#k3_algstr_3 :::"TernaryFieldEx"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#g1_algstr_3 :::"TernaryFieldStr"::: )  "(#"  (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set  ($#k2_algstr_3 :::"ternaryreal"::: ) ) "#)" )); 
 registration
cluster (Set   ($#k3_algstr_3 :::"TernaryFieldEx"::: )  ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_algstr_3 :::"strict"::: )   ; 
end; definitionlet "a", "b", "c" be   ($#m1_subset_1 :::"Scalar":::) "of" (Set  ($#k3_algstr_3 :::"TernaryFieldEx"::: ) ); func  :::"tern":::  "(" "a" "," "b" "," "c" ")"  ->   ($#m1_subset_1 :::"Scalar":::) "of" (Set  ($#k3_algstr_3 :::"TernaryFieldEx"::: ) ) equals :: ALGSTR_3:def 4 (Set (Set  "the"  ($#u1_algstr_3 :::"TernOp"::: )  "of" (Set  ($#k3_algstr_3 :::"TernaryFieldEx"::: ) ))  ($#k2_multop_1 :::"."::: )   "(" "a" "," "b" "," "c" ")" ); end; 







:: deftheorem    defines :::"tern"::: ALGSTR_3:def 4 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set  ($#k3_algstr_3 :::"TernaryFieldEx"::: ) ) "holds"  (Bool (Set   ($#k4_algstr_3 :::"tern"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_3 :::"TernOp"::: )  "of" (Set  ($#k3_algstr_3 :::"TernaryFieldEx"::: ) ))  ($#k2_multop_1 :::"."::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ))); 
 
theorem :: ALGSTR_3:1 (Bool  "for" (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "v")) "," (Set (Var "v9")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "u"))  ($#r1_hidden :::"<>"::: )  (Set (Var "u9")))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Set  "(" (Set (Var "u"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "u9"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "v9")))))) ; 
 
theorem :: ALGSTR_3:2 (Bool  "for" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "v")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set  ($#k3_algstr_3 :::"TernaryFieldEx"::: ) )  (Bool  "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "u"))  ($#r1_hidden :::"="::: )  (Set (Var "z"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))) "holds"  (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "z"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "y")))))) ; 
 
theorem :: ALGSTR_3:3 (Bool (Num 1)  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set  ($#k3_algstr_3 :::"TernaryFieldEx"::: ) ))) ; 
 definitionlet "IT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_algstr_3 :::"TernaryFieldStr"::: )  ; attr "IT" is  :::"Ternary-Field-like":::  means :: ALGSTR_3:def 5 (Bool  "("  (Bool (Set   ($#k4_struct_0 :::"0."::: )  "IT")  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_struct_0 :::"1."::: )  "IT")) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" "IT" "holds"  (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k5_struct_0 :::"1."::: )  "IT" ")" ) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  "IT" ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" "IT" "holds"  (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set  "("  ($#k5_struct_0 :::"1."::: )  "IT" ")" ) "," (Set (Var "a")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  "IT" ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" "IT" "holds"  (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  "IT" ")" ) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" "IT" "holds"  (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set  "("  ($#k4_struct_0 :::"0."::: )  "IT" ")" ) "," (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" ) & (Bool  "("   "for" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" "IT" (Bool  "ex" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" "IT" "st" (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b"))))  ")" ) & (Bool  "("   "for" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "v")) "," (Set (Var "v9")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" "IT"  "st" (Bool (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "v9")) ")" ))) "holds"  (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set (Var "v9")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "a9")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" "IT"  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9")))) "holds"  (Bool  "for" (Set (Var "b")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" "IT" (Bool  "ex" (Set (Var "u")) "," (Set (Var "v")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" "IT" "st"  (Bool  "("  (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a9")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b9")))  ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "u")) "," (Set (Var "u9")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" "IT"  "st" (Bool (Bool (Set (Var "u"))  ($#r1_hidden :::"<>"::: )  (Set (Var "u9")))) "holds"  (Bool  "for" (Set (Var "v")) "," (Set (Var "v9")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" "IT" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" "IT" "st" (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u9")) "," (Set (Var "a")) "," (Set (Var "v9")) ")" ))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "v")) "," (Set (Var "v9")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" "IT"  "st" (Bool (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u9")) "," (Set (Var "a")) "," (Set (Var "v9")) ")" )) & (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a9")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u9")) "," (Set (Var "a9")) "," (Set (Var "v9")) ")" )) & (Bool (Bool  "not" (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a9"))))) "holds"  (Bool (Set (Var "u"))  ($#r1_hidden :::"="::: )  (Set (Var "u9")))  ")" )  ")" ); end; 




:: deftheorem    defines :::"Ternary-Field-like"::: ALGSTR_3:def 5 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_algstr_3 :::"TernaryFieldStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_algstr_3 :::"Ternary-Field-like"::: )  ) "iff" (Bool  "("  (Bool (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "IT")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "IT")))) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "IT")) "holds"  (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "IT")) ")" ) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "IT")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "IT")) "holds"  (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set (Var "IT")) ")" ) "," (Set (Var "a")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "IT")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "IT")) "holds"  (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "IT")) ")" ) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "IT")) "holds"  (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "IT")) ")" ) "," (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" ) & (Bool  "("   "for" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "IT")) (Bool  "ex" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "IT")) "st" (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b"))))  ")" ) & (Bool  "("   "for" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "v")) "," (Set (Var "v9")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "v9")) ")" ))) "holds"  (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set (Var "v9")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "a9")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9")))) "holds"  (Bool  "for" (Set (Var "b")) "," (Set (Var "b9")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "IT")) (Bool  "ex" (Set (Var "u")) "," (Set (Var "v")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "IT")) "st"  (Bool  "("  (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a9")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b9")))  ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "u")) "," (Set (Var "u9")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "u"))  ($#r1_hidden :::"<>"::: )  (Set (Var "u9")))) "holds"  (Bool  "for" (Set (Var "v")) "," (Set (Var "v9")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "IT")) (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "IT")) "st" (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u9")) "," (Set (Var "a")) "," (Set (Var "v9")) ")" ))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "u")) "," (Set (Var "u9")) "," (Set (Var "v")) "," (Set (Var "v9")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u9")) "," (Set (Var "a")) "," (Set (Var "v9")) ")" )) & (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a9")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u9")) "," (Set (Var "a9")) "," (Set (Var "v9")) ")" )) & (Bool (Bool  "not" (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a9"))))) "holds"  (Bool (Set (Var "u"))  ($#r1_hidden :::"="::: )  (Set (Var "u9")))  ")" )  ")" )  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_algstr_3 :::"strict"::: )     ($#v2_algstr_3 :::"Ternary-Field-like"::: )    for    ($#l1_algstr_3 :::"TernaryFieldStr"::: )  ; 
end; definitionmode Ternary-Field is  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_algstr_3 :::"Ternary-Field-like"::: )     ($#l1_algstr_3 :::"TernaryFieldStr"::: )  ; end; 
















theorem :: ALGSTR_3:4 (Bool  "for" (Set (Var "F")) "being"   ($#l1_algstr_3 :::"Ternary-Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "a9")) "," (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "u9")) "," (Set (Var "v9")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "a9"))) & (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u9")) "," (Set (Var "a")) "," (Set (Var "v9")) ")" )) & (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u")) "," (Set (Var "a9")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "u9")) "," (Set (Var "a9")) "," (Set (Var "v9")) ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "u"))  ($#r1_hidden :::"="::: )  (Set (Var "u9"))) & (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set (Var "v9")))  ")" ))) ; 
 
theorem :: ALGSTR_3:5 (Bool  "for" (Set (Var "F")) "being"   ($#l1_algstr_3 :::"Ternary-Field":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F"))))) "holds"  (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "F")) (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "F")) "st" (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "c"))))))) ; 
 
theorem :: ALGSTR_3:6 (Bool  "for" (Set (Var "F")) "being"   ($#l1_algstr_3 :::"Ternary-Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "b")) "," (Set (Var "x9")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F")))) & (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "a")) "," (Set (Var "x9")) "," (Set (Var "b")) ")" ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "x9"))))) ; 
 
theorem :: ALGSTR_3:7 (Bool  "for" (Set (Var "F")) "being"   ($#l1_algstr_3 :::"Ternary-Field":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F"))))) "holds"  (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "F")) (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "F")) "st" (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "x")) "," (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "c"))))))) ; 
 
theorem :: ALGSTR_3:8 (Bool  "for" (Set (Var "F")) "being"   ($#l1_algstr_3 :::"Ternary-Field":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "b")) "," (Set (Var "x9")) "being"   ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "F")))) & (Bool (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "x")) "," (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_algstr_3 :::"Tern"::: )   "(" (Set (Var "x9")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "x9"))))) ;