begin
deffunc H1( non empty LattStr ) -> set = the carrier of $1;
deffunc H2( LattStr ) -> Element of bool [:[:the carrier of $1,the carrier of $1:],the carrier of $1:] = the L_join of $1;
deffunc H3( LattStr ) -> Element of bool [:[:the carrier of $1,the carrier of $1:],the carrier of $1:] = the L_meet of $1;
deffunc H4( multMagma ) -> Element of bool [:[:the carrier of $1,the carrier of $1:],the carrier of $1:] = the multF of $1;
theorem Th1:
theorem Th2:
:: deftheorem defines directed QUANTAL1:def 1 :
theorem
:: deftheorem defines with_left-zero QUANTAL1:def 2 :
:: deftheorem defines with_right-zero QUANTAL1:def 3 :
:: deftheorem Def4 defines with_zero QUANTAL1:def 4 :
:: deftheorem Def5 defines right-distributive QUANTAL1:def 5 :
:: deftheorem Def6 defines left-distributive QUANTAL1:def 6 :
:: deftheorem defines times-additive QUANTAL1:def 7 :
:: deftheorem defines times-continuous QUANTAL1:def 8 :
theorem Th4:
theorem Th5:
theorem Th6:
registration
let A be non
empty set ;
let b1,
b2,
b3 be
BinOp of
A;
let e be
Element of
A;
cluster QuasiNetStr(#
A,
b1,
b2,
b3,
e #)
-> non
empty ;
coherence
not QuasiNetStr(# A,b1,b2,b3,e #) is empty
;
end;
theorem
theorem Th8:
theorem Th9:
:: deftheorem defines idempotent QUANTAL1:def 9 :
Lm1:
for A being non empty set
for f being UnOp of A st f is idempotent holds
for a being Element of A holds f . (f . a) = f . a
:: deftheorem defines inflationary QUANTAL1:def 10 :
:: deftheorem defines deflationary QUANTAL1:def 11 :
:: deftheorem Def12 defines monotone QUANTAL1:def 12 :
:: deftheorem defines \/-distributive QUANTAL1:def 13 :
theorem Th10:
:: deftheorem defines times-monotone QUANTAL1:def 14 :
:: deftheorem defines -r> QUANTAL1:def 15 :
:: deftheorem defines -l> QUANTAL1:def 16 :
theorem Th11:
theorem Th12:
theorem Th13:
theorem
:: deftheorem Def17 defines dualizing QUANTAL1:def 17 :
:: deftheorem Def18 defines cyclic QUANTAL1:def 18 :
theorem Th15:
theorem Th16:
theorem
theorem
theorem Th19:
theorem
:: deftheorem Def19 defines cyclic QUANTAL1:def 19 :
:: deftheorem Def20 defines dualized QUANTAL1:def 20 :
theorem Th21:
registration
let A be non
empty set ;
let b1,
b2,
b3 be
BinOp of
A;
let e1,
e2 be
Element of
A;
cluster Girard-QuantaleStr(#
A,
b1,
b2,
b3,
e1,
e2 #)
-> non
empty ;
coherence
not Girard-QuantaleStr(# A,b1,b2,b3,e1,e2 #) is empty
;
end;
:: deftheorem defines Bottom QUANTAL1:def 21 :
:: deftheorem defines Top QUANTAL1:def 22 :
:: deftheorem defines Bottom QUANTAL1:def 23 :
:: deftheorem defines Negation QUANTAL1:def 24 :
:: deftheorem defines Bottom QUANTAL1:def 25 :
:: deftheorem defines Bottom QUANTAL1:def 26 :
theorem Th22:
theorem
theorem Th24:
theorem Th25:
theorem Th26:
:: deftheorem defines delta QUANTAL1:def 27 :
theorem
theorem
theorem
theorem
theorem
theorem Th32:
theorem
theorem