:: by Grzegorz Bancerek

::

:: Received May 9, 1994

:: Copyright (c) 1994-2018 Association of Mizar Users

scheme :: QUANTAL1:sch 1

DenestFraenkel{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}( set ) -> set , F_{4}( set ) -> Element of F_{2}(), P_{1}[ set ] } :

DenestFraenkel{ F

{ F_{3}(a) where a is Element of F_{2}() : a in { F_{4}(b) where b is Element of F_{1}() : P_{1}[b] } } = { F_{3}(F_{4}(a)) where a is Element of F_{1}() : P_{1}[a] }

proof end;

deffunc H

deffunc H

deffunc H

deffunc H

theorem :: QUANTAL1:1

for L1, L2 being non empty LattStr st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds

for a1, b1 being Element of L1

for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds

( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) ;

for a1, b1 being Element of L1

for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds

( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) ;

theorem Th2: :: QUANTAL1:2

for L1, L2 being non empty LattStr st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds

for a being Element of L1

for b being Element of L2

for X being set st a = b holds

( ( a is_less_than X implies b is_less_than X ) & ( b is_less_than X implies a is_less_than X ) & ( a is_greater_than X implies b is_greater_than X ) & ( b is_greater_than X implies a is_greater_than X ) )

for a being Element of L1

for b being Element of L2

for X being set st a = b holds

( ( a is_less_than X implies b is_less_than X ) & ( b is_less_than X implies a is_less_than X ) & ( a is_greater_than X implies b is_greater_than X ) & ( b is_greater_than X implies a is_greater_than X ) )

proof end;

:: deftheorem defines directed QUANTAL1:def 1 :

for L being non empty LattStr

for X being Subset of L holds

( X is directed iff for Y being finite Subset of X ex x being Element of L st

( "\/" (Y,L) [= x & x in X ) );

for L being non empty LattStr

for X being Subset of L holds

( X is directed iff for Y being finite Subset of X ex x being Element of L st

( "\/" (Y,L) [= x & x in X ) );

definition

attr c_{1} is strict ;

struct QuantaleStr -> LattStr , multMagma ;

aggr QuantaleStr(# carrier, L_join, L_meet, multF #) -> QuantaleStr ;

end;
struct QuantaleStr -> LattStr , multMagma ;

aggr QuantaleStr(# carrier, L_join, L_meet, multF #) -> QuantaleStr ;

definition

attr c_{1} is strict ;

struct QuasiNetStr -> QuantaleStr , multLoopStr ;

aggr QuasiNetStr(# carrier, L_join, L_meet, multF, OneF #) -> QuasiNetStr ;

end;
struct QuasiNetStr -> QuantaleStr , multLoopStr ;

aggr QuasiNetStr(# carrier, L_join, L_meet, multF, OneF #) -> QuasiNetStr ;

definition

let IT be non empty multMagma ;

end;
attr IT is with_left-zero means :: QUANTAL1:def 2

ex a being Element of IT st

for b being Element of IT holds a * b = a;

ex a being Element of IT st

for b being Element of IT holds a * b = a;

attr IT is with_right-zero means :: QUANTAL1:def 3

ex b being Element of IT st

for a being Element of IT holds a * b = b;

ex b being Element of IT st

for a being Element of IT holds a * b = b;

:: deftheorem defines with_left-zero QUANTAL1:def 2 :

for IT being non empty multMagma holds

( IT is with_left-zero iff ex a being Element of IT st

for b being Element of IT holds a * b = a );

for IT being non empty multMagma holds

( IT is with_left-zero iff ex a being Element of IT st

for b being Element of IT holds a * b = a );

:: deftheorem defines with_right-zero QUANTAL1:def 3 :

for IT being non empty multMagma holds

( IT is with_right-zero iff ex b being Element of IT st

for a being Element of IT holds a * b = b );

for IT being non empty multMagma holds

( IT is with_right-zero iff ex b being Element of IT st

for a being Element of IT holds a * b = b );

:: deftheorem defines with_zero QUANTAL1:def 4 :

for IT being non empty multMagma holds

( IT is with_zero iff ( IT is with_left-zero & IT is with_right-zero ) );

for IT being non empty multMagma holds

( IT is with_zero iff ( IT is with_left-zero & IT is with_right-zero ) );

registration

coherence

for b_{1} being non empty multMagma st b_{1} is with_zero holds

( b_{1} is with_left-zero & b_{1} is with_right-zero )
;

coherence

for b_{1} being non empty multMagma st b_{1} is with_left-zero & b_{1} is with_right-zero holds

b_{1} is with_zero
;

end;
for b

( b

coherence

for b

b

definition

let IT be non empty QuantaleStr ;

end;
attr IT is right-distributive means :Def5: :: QUANTAL1:def 5

for a being Element of IT

for X being set holds a [*] ("\/" (X,IT)) = "\/" ( { (a [*] b) where b is Element of IT : b in X } ,IT);

for a being Element of IT

for X being set holds a [*] ("\/" (X,IT)) = "\/" ( { (a [*] b) where b is Element of IT : b in X } ,IT);

attr IT is left-distributive means :Def6: :: QUANTAL1:def 6

for a being Element of IT

for X being set holds ("\/" (X,IT)) [*] a = "\/" ( { (b [*] a) where b is Element of IT : b in X } ,IT);

for a being Element of IT

for X being set holds ("\/" (X,IT)) [*] a = "\/" ( { (b [*] a) where b is Element of IT : b in X } ,IT);

:: deftheorem Def5 defines right-distributive QUANTAL1:def 5 :

for IT being non empty QuantaleStr holds

( IT is right-distributive iff for a being Element of IT

for X being set holds a [*] ("\/" (X,IT)) = "\/" ( { (a [*] b) where b is Element of IT : b in X } ,IT) );

for IT being non empty QuantaleStr holds

( IT is right-distributive iff for a being Element of IT

for X being set holds a [*] ("\/" (X,IT)) = "\/" ( { (a [*] b) where b is Element of IT : b in X } ,IT) );

:: deftheorem Def6 defines left-distributive QUANTAL1:def 6 :

for IT being non empty QuantaleStr holds

( IT is left-distributive iff for a being Element of IT

for X being set holds ("\/" (X,IT)) [*] a = "\/" ( { (b [*] a) where b is Element of IT : b in X } ,IT) );

for IT being non empty QuantaleStr holds

( IT is left-distributive iff for a being Element of IT

for X being set holds ("\/" (X,IT)) [*] a = "\/" ( { (b [*] a) where b is Element of IT : b in X } ,IT) );

:: deftheorem defines times-additive QUANTAL1:def 7 :

for IT being non empty QuantaleStr holds

( IT is times-additive iff for a, b, c being Element of IT holds

( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) ) );

for IT being non empty QuantaleStr holds

( IT is times-additive iff for a, b, c being Element of IT holds

( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) ) );

:: deftheorem defines times-continuous QUANTAL1:def 8 :

for IT being non empty QuantaleStr holds

( IT is times-continuous iff for X1, X2 being Subset of IT st X1 is directed & X2 is directed holds

("\/" X1) [*] ("\/" X2) = "\/" ( { (a [*] b) where a, b is Element of IT : ( a in X1 & b in X2 ) } ,IT) );

for IT being non empty QuantaleStr holds

( IT is times-continuous iff for X1, X2 being Subset of IT st X1 is directed & X2 is directed holds

("\/" X1) [*] ("\/" X2) = "\/" ( { (a [*] b) where a, b is Element of IT : ( a in X1 & b in X2 ) } ,IT) );

theorem Th4: :: QUANTAL1:4

for Q being non empty QuantaleStr st LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {} holds

( Q is associative & Q is commutative & Q is unital & Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like )

( Q is associative & Q is commutative & Q is unital & Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like )

proof end;

registration

let A be non empty set ;

let b1, b2, b3 be BinOp of A;

coherence

not QuantaleStr(# A,b1,b2,b3 #) is empty ;

end;
let b1, b2, b3 be BinOp of A;

coherence

not QuantaleStr(# A,b1,b2,b3 #) is empty ;

registration

ex b_{1} being non empty QuantaleStr st

( b_{1} is associative & b_{1} is commutative & b_{1} is unital & b_{1} is with_zero & b_{1} is left-distributive & b_{1} is right-distributive & b_{1} is complete & b_{1} is Lattice-like )
end;

cluster non empty Lattice-like complete unital associative commutative with_zero right-distributive left-distributive for QuantaleStr ;

existence ex b

( b

proof end;

scheme :: QUANTAL1:sch 3

LUBFraenkelDistr{ F_{1}() -> non empty Lattice-like complete QuantaleStr , F_{2}( set , set ) -> Element of F_{1}(), F_{3}() -> set , F_{4}() -> set } :

LUBFraenkelDistr{ F

"\/" ( { ("\/" ( { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } ,F_{1}())) where a is Element of F_{1}() : a in F_{3}() } ,F_{1}()) = "\/" ( { F_{2}(a,b) where a, b is Element of F_{1}() : ( a in F_{3}() & b in F_{4}() ) } ,F_{1}())

proof end;

theorem Th5: :: QUANTAL1:5

for Q being non empty Lattice-like complete right-distributive left-distributive QuantaleStr

for X, Y being set holds ("\/" (X,Q)) [*] ("\/" (Y,Q)) = "\/" ( { (a [*] b) where a, b is Element of Q : ( a in X & b in Y ) } ,Q)

for X, Y being set holds ("\/" (X,Q)) [*] ("\/" (Y,Q)) = "\/" ( { (a [*] b) where a, b is Element of Q : ( a in X & b in Y ) } ,Q)

proof end;

theorem Th6: :: QUANTAL1:6

for Q being non empty Lattice-like complete right-distributive left-distributive QuantaleStr

for a, b, c being Element of Q holds

( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) )

for a, b, c being Element of Q holds

( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) )

proof end;

registration

let A be non empty set ;

let b1, b2, b3 be BinOp of A;

let e be Element of A;

coherence

not QuasiNetStr(# A,b1,b2,b3,e #) is empty ;

end;
let b1, b2, b3 be BinOp of A;

let e be Element of A;

coherence

not QuasiNetStr(# A,b1,b2,b3,e #) is empty ;

registration

existence

ex b_{1} being non empty QuasiNetStr st

( b_{1} is complete & b_{1} is Lattice-like )

end;
ex b

( b

proof end;

registration

for b_{1} being non empty Lattice-like complete QuasiNetStr st b_{1} is left-distributive & b_{1} is right-distributive holds

( b_{1} is times-continuous & b_{1} is times-additive )
by Th5, Th6;

end;

cluster non empty Lattice-like complete right-distributive left-distributive -> non empty Lattice-like complete times-additive times-continuous for QuasiNetStr ;

coherence for b

( b

registration

ex b_{1} being non empty QuasiNetStr st

( b_{1} is associative & b_{1} is commutative & b_{1} is unital & b_{1} is with_zero & b_{1} is with_left-zero & b_{1} is left-distributive & b_{1} is right-distributive & b_{1} is complete & b_{1} is Lattice-like )
end;

cluster non empty Lattice-like complete unital associative commutative with_left-zero with_zero right-distributive left-distributive for QuasiNetStr ;

existence ex b

( b

proof end;

definition

mode Quantale is non empty Lattice-like complete associative right-distributive left-distributive QuantaleStr ;

mode QuasiNet is non empty Lattice-like complete unital associative with_left-zero times-additive times-continuous QuasiNetStr ;

end;
mode QuasiNet is non empty Lattice-like complete unital associative with_left-zero times-additive times-continuous QuasiNetStr ;

:: deftheorem defines idempotent QUANTAL1:def 9 :

for f being Function holds

( f is idempotent iff f * f = f );

for f being Function holds

( f is idempotent iff f * f = f );

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

by FUNCT_2:15;

definition

let L be non empty LattStr ;

let IT be UnOp of L;

end;
let IT be UnOp of L;

:: deftheorem defines inflationary QUANTAL1:def 10 :

for L being non empty LattStr

for IT being UnOp of L holds

( IT is inflationary iff for p being Element of L holds p [= IT . p );

for L being non empty LattStr

for IT being UnOp of L holds

( IT is inflationary iff for p being Element of L holds p [= IT . p );

:: deftheorem defines deflationary QUANTAL1:def 11 :

for L being non empty LattStr

for IT being UnOp of L holds

( IT is deflationary iff for p being Element of L holds IT . p [= p );

for L being non empty LattStr

for IT being UnOp of L holds

( IT is deflationary iff for p being Element of L holds IT . p [= p );

:: deftheorem defines monotone QUANTAL1:def 12 :

for L being non empty LattStr

for IT being UnOp of L holds

( IT is monotone iff for p, q being Element of L st p [= q holds

IT . p [= IT . q );

for L being non empty LattStr

for IT being UnOp of L holds

( IT is monotone iff for p, q being Element of L st p [= q holds

IT . p [= IT . q );

:: deftheorem defines \/-distributive QUANTAL1:def 13 :

for L being non empty LattStr

for IT being UnOp of L holds

( IT is \/-distributive iff for X being Subset of L holds IT . ("\/" X) [= "\/" ( { (IT . a) where a is Element of L : a in X } ,L) );

for L being non empty LattStr

for IT being UnOp of L holds

( IT is \/-distributive iff for X being Subset of L holds IT . ("\/" X) [= "\/" ( { (IT . a) where a is Element of L : a in X } ,L) );

registration

let L be Lattice;

ex b_{1} being UnOp of L st

( b_{1} is inflationary & b_{1} is deflationary & b_{1} is monotone )

end;
cluster non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V17( the carrier of L) V21( the carrier of L, the carrier of L) inflationary deflationary monotone for UnOp of ;

existence ex b

( b

proof end;

theorem Th10: :: QUANTAL1:10

for L being complete Lattice

for j being UnOp of L st j is monotone holds

( j is \/-distributive iff for X being Subset of L holds j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L) )

for j being UnOp of L st j is monotone holds

( j is \/-distributive iff for X being Subset of L holds j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L) )

proof end;

definition

let Q be non empty QuantaleStr ;

let IT be UnOp of Q;

end;
let IT be UnOp of Q;

attr IT is times-monotone means :: QUANTAL1:def 14

for a, b being Element of Q holds (IT . a) [*] (IT . b) [= IT . (a [*] b);

for a, b being Element of Q holds (IT . a) [*] (IT . b) [= IT . (a [*] b);

:: deftheorem defines times-monotone QUANTAL1:def 14 :

for Q being non empty QuantaleStr

for IT being UnOp of Q holds

( IT is times-monotone iff for a, b being Element of Q holds (IT . a) [*] (IT . b) [= IT . (a [*] b) );

for Q being non empty QuantaleStr

for IT being UnOp of Q holds

( IT is times-monotone iff for a, b being Element of Q holds (IT . a) [*] (IT . b) [= IT . (a [*] b) );

definition

let Q be non empty QuantaleStr ;

let a, b be Element of Q;

coherence

"\/" ( { c where c is Element of Q : c [*] a [= b } ,Q) is Element of Q;

;

coherence

"\/" ( { c where c is Element of Q : a [*] c [= b } ,Q) is Element of Q;

;

end;
let a, b be Element of Q;

func a -r> b -> Element of Q equals :: QUANTAL1:def 15

"\/" ( { c where c is Element of Q : c [*] a [= b } ,Q);

correctness "\/" ( { c where c is Element of Q : c [*] a [= b } ,Q);

coherence

"\/" ( { c where c is Element of Q : c [*] a [= b } ,Q) is Element of Q;

;

func a -l> b -> Element of Q equals :: QUANTAL1:def 16

"\/" ( { c where c is Element of Q : a [*] c [= b } ,Q);

correctness "\/" ( { c where c is Element of Q : a [*] c [= b } ,Q);

coherence

"\/" ( { c where c is Element of Q : a [*] c [= b } ,Q) is Element of Q;

;

:: deftheorem defines -r> QUANTAL1:def 15 :

for Q being non empty QuantaleStr

for a, b being Element of Q holds a -r> b = "\/" ( { c where c is Element of Q : c [*] a [= b } ,Q);

for Q being non empty QuantaleStr

for a, b being Element of Q holds a -r> b = "\/" ( { c where c is Element of Q : c [*] a [= b } ,Q);

:: deftheorem defines -l> QUANTAL1:def 16 :

for Q being non empty QuantaleStr

for a, b being Element of Q holds a -l> b = "\/" ( { c where c is Element of Q : a [*] c [= b } ,Q);

for Q being non empty QuantaleStr

for a, b being Element of Q holds a -l> b = "\/" ( { c where c is Element of Q : a [*] c [= b } ,Q);

theorem Th13: :: QUANTAL1:13

for Q being Quantale

for s, a, b being Element of Q st a [= b holds

( b -r> s [= a -r> s & b -l> s [= a -l> s )

for s, a, b being Element of Q st a [= b holds

( b -r> s [= a -r> s & b -l> s [= a -l> s )

proof end;

theorem :: QUANTAL1:14

for Q being Quantale

for s being Element of Q

for j being UnOp of Q st ( for a being Element of Q holds j . a = (a -r> s) -r> s ) holds

j is monotone

for s being Element of Q

for j being UnOp of Q st ( for a being Element of Q holds j . a = (a -r> s) -r> s ) holds

j is monotone

proof end;

definition

let Q be non empty QuantaleStr ;

let IT be Element of Q;

end;
let IT be Element of Q;

:: deftheorem defines dualizing QUANTAL1:def 17 :

for Q being non empty QuantaleStr

for IT being Element of Q holds

( IT is dualizing iff for a being Element of Q holds

( (a -r> IT) -l> IT = a & (a -l> IT) -r> IT = a ) );

for Q being non empty QuantaleStr

for IT being Element of Q holds

( IT is dualizing iff for a being Element of Q holds

( (a -r> IT) -l> IT = a & (a -l> IT) -r> IT = a ) );

:: deftheorem defines cyclic QUANTAL1:def 18 :

for Q being non empty QuantaleStr

for IT being Element of Q holds

( IT is cyclic iff for a being Element of Q holds a -r> IT = a -l> IT );

for Q being non empty QuantaleStr

for IT being Element of Q holds

( IT is cyclic iff for a being Element of Q holds a -r> IT = a -l> IT );

theorem Th15: :: QUANTAL1:15

for Q being Quantale

for c being Element of Q holds

( c is cyclic iff for a, b being Element of Q st a [*] b [= c holds

b [*] a [= c )

for c being Element of Q holds

( c is cyclic iff for a, b being Element of Q st a [*] b [= c holds

b [*] a [= c )

proof end;

theorem Th16: :: QUANTAL1:16

for Q being Quantale

for s, a being Element of Q st s is cyclic holds

( a [= (a -r> s) -r> s & a [= (a -l> s) -l> s )

for s, a being Element of Q st s is cyclic holds

( a [= (a -r> s) -r> s & a [= (a -l> s) -l> s )

proof end;

theorem :: QUANTAL1:17

for Q being Quantale

for s, a being Element of Q st s is cyclic holds

( a -r> s = ((a -r> s) -r> s) -r> s & a -l> s = ((a -l> s) -l> s) -l> s )

for s, a being Element of Q st s is cyclic holds

( a -r> s = ((a -r> s) -r> s) -r> s & a -l> s = ((a -l> s) -l> s) -l> s )

proof end;

theorem :: QUANTAL1:18

for Q being Quantale

for s, a, b being Element of Q holds ((a -r> s) -r> s) [*] ((b -r> s) -r> s) [= ((a [*] b) -r> s) -r> s

for s, a, b being Element of Q holds ((a -r> s) -r> s) [*] ((b -r> s) -r> s) [= ((a [*] b) -r> s) -r> s

proof end;

theorem Th19: :: QUANTAL1:19

for Q being Quantale

for D being Element of Q st D is dualizing holds

( Q is unital & the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D )

for D being Element of Q st D is dualizing holds

( Q is unital & the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D )

proof end;

theorem :: QUANTAL1:20

for Q being Quantale

for a, b, c being Element of Q st a is dualizing holds

( b -r> c = (b [*] (c -l> a)) -r> a & b -l> c = ((c -r> a) [*] b) -l> a )

for a, b, c being Element of Q st a is dualizing holds

( b -r> c = (b [*] (c -l> a)) -r> a & b -l> c = ((c -r> a) [*] b) -l> a )

proof end;

definition

attr c_{1} is strict ;

struct Girard-QuantaleStr -> QuasiNetStr ;

aggr Girard-QuantaleStr(# carrier, L_join, L_meet, multF, OneF, absurd #) -> Girard-QuantaleStr ;

sel absurd c_{1} -> Element of the carrier of c_{1};

end;
struct Girard-QuantaleStr -> QuasiNetStr ;

aggr Girard-QuantaleStr(# carrier, L_join, L_meet, multF, OneF, absurd #) -> Girard-QuantaleStr ;

sel absurd c

:: deftheorem Def19 defines cyclic QUANTAL1:def 19 :

for IT being non empty Girard-QuantaleStr holds

( IT is cyclic iff the absurd of IT is cyclic );

for IT being non empty Girard-QuantaleStr holds

( IT is cyclic iff the absurd of IT is cyclic );

:: deftheorem Def20 defines dualized QUANTAL1:def 20 :

for IT being non empty Girard-QuantaleStr holds

( IT is dualized iff the absurd of IT is dualizing );

for IT being non empty Girard-QuantaleStr holds

( IT is dualized iff the absurd of IT is dualizing );

theorem Th21: :: QUANTAL1:21

for Q being non empty Girard-QuantaleStr st LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {} holds

( Q is cyclic & Q is dualized )

( Q is cyclic & Q is dualized )

proof end;

registration

let A be non empty set ;

let b1, b2, b3 be BinOp of A;

let e1, e2 be Element of A;

coherence

not Girard-QuantaleStr(# A,b1,b2,b3,e1,e2 #) is empty ;

end;
let b1, b2, b3 be BinOp of A;

let e1, e2 be Element of A;

coherence

not Girard-QuantaleStr(# A,b1,b2,b3,e1,e2 #) is empty ;

registration

ex b_{1} being non empty Girard-QuantaleStr st

( b_{1} is associative & b_{1} is commutative & b_{1} is unital & b_{1} is left-distributive & b_{1} is right-distributive & b_{1} is complete & b_{1} is Lattice-like & b_{1} is cyclic & b_{1} is dualized & b_{1} is strict )
end;

cluster non empty Lattice-like complete unital associative commutative right-distributive left-distributive strict cyclic dualized for Girard-QuantaleStr ;

existence ex b

( b

proof end;

definition

mode Girard-Quantale is non empty Lattice-like complete unital associative right-distributive left-distributive cyclic dualized Girard-QuantaleStr ;

end;
definition
end;

:: deftheorem defines Bottom QUANTAL1:def 21 :

for G being Girard-QuantaleStr holds Bottom G = the absurd of G;

for G being Girard-QuantaleStr holds Bottom G = the absurd of G;

definition

let G be non empty Girard-QuantaleStr ;

correctness

coherence

(Bottom G) -r> (Bottom G) is Element of G;

;

let a be Element of G;

correctness

coherence

a -r> (Bottom G) is Element of G;

;

end;
correctness

coherence

(Bottom G) -r> (Bottom G) is Element of G;

;

let a be Element of G;

correctness

coherence

a -r> (Bottom G) is Element of G;

;

:: deftheorem defines Top QUANTAL1:def 22 :

for G being non empty Girard-QuantaleStr holds Top G = (Bottom G) -r> (Bottom G);

for G being non empty Girard-QuantaleStr holds Top G = (Bottom G) -r> (Bottom G);

:: deftheorem defines Bottom QUANTAL1:def 23 :

for G being non empty Girard-QuantaleStr

for a being Element of G holds Bottom a = a -r> (Bottom G);

for G being non empty Girard-QuantaleStr

for a being Element of G holds Bottom a = a -r> (Bottom G);

definition

let G be non empty Girard-QuantaleStr ;

ex b_{1} being UnOp of G st

for a being Element of G holds b_{1} . a = Bottom a

for b_{1}, b_{2} being UnOp of G st ( for a being Element of G holds b_{1} . a = Bottom a ) & ( for a being Element of G holds b_{2} . a = Bottom a ) holds

b_{1} = b_{2}

end;
func Negation G -> UnOp of G means :: QUANTAL1:def 24

for a being Element of G holds it . a = Bottom a;

existence for a being Element of G holds it . a = Bottom a;

ex b

for a being Element of G holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines Negation QUANTAL1:def 24 :

for G being non empty Girard-QuantaleStr

for b_{2} being UnOp of G holds

( b_{2} = Negation G iff for a being Element of G holds b_{2} . a = Bottom a );

for G being non empty Girard-QuantaleStr

for b

( b

definition

let G be non empty Girard-QuantaleStr ;

let u be UnOp of G;

correctness

coherence

(Negation G) * u is UnOp of G;

;

end;
let u be UnOp of G;

correctness

coherence

(Negation G) * u is UnOp of G;

;

:: deftheorem defines Bottom QUANTAL1:def 25 :

for G being non empty Girard-QuantaleStr

for u being UnOp of G holds Bottom u = (Negation G) * u;

for G being non empty Girard-QuantaleStr

for u being UnOp of G holds Bottom u = (Negation G) * u;

definition

let G be non empty Girard-QuantaleStr ;

let o be BinOp of G;

correctness

coherence

(Negation G) * o is BinOp of G;

;

end;
let o be BinOp of G;

correctness

coherence

(Negation G) * o is BinOp of G;

;

:: deftheorem defines Bottom QUANTAL1:def 26 :

for G being non empty Girard-QuantaleStr

for o being BinOp of G holds Bottom o = (Negation G) * o;

for G being non empty Girard-QuantaleStr

for o being BinOp of G holds Bottom o = (Negation G) * o;

theorem :: QUANTAL1:23

theorem Th24: :: QUANTAL1:24

for Q being Girard-Quantale

for X being set holds Bottom ("\/" (X,Q)) = "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)

for X being set holds Bottom ("\/" (X,Q)) = "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)

proof end;

theorem Th25: :: QUANTAL1:25

for Q being Girard-Quantale

for X being set holds Bottom ("/\" (X,Q)) = "\/" ( { (Bottom a) where a is Element of Q : a in X } ,Q)

for X being set holds Bottom ("/\" (X,Q)) = "\/" ( { (Bottom a) where a is Element of Q : a in X } ,Q)

proof end;

theorem Th26: :: QUANTAL1:26

for Q being Girard-Quantale

for a, b being Element of Q holds

( Bottom (a "\/" b) = (Bottom a) "/\" (Bottom b) & Bottom (a "/\" b) = (Bottom a) "\/" (Bottom b) )

for a, b being Element of Q holds

( Bottom (a "\/" b) = (Bottom a) "/\" (Bottom b) & Bottom (a "/\" b) = (Bottom a) "\/" (Bottom b) )

proof end;

definition

let Q be Girard-Quantale;

let a, b be Element of Q;

correctness

coherence

Bottom ((Bottom a) [*] (Bottom b)) is Element of Q;

;

end;
let a, b be Element of Q;

correctness

coherence

Bottom ((Bottom a) [*] (Bottom b)) is Element of Q;

;

:: deftheorem defines delta QUANTAL1:def 27 :

for Q being Girard-Quantale

for a, b being Element of Q holds a delta b = Bottom ((Bottom a) [*] (Bottom b));

for Q being Girard-Quantale

for a, b being Element of Q holds a delta b = Bottom ((Bottom a) [*] (Bottom b));

theorem :: QUANTAL1:27

for Q being Girard-Quantale

for a being Element of Q

for X being set holds

( a [*] ("\/" (X,Q)) = "\/" ( { (a [*] b) where b is Element of Q : b in X } ,Q) & a delta ("/\" (X,Q)) = "/\" ( { (a delta c) where c is Element of Q : c in X } ,Q) )

for a being Element of Q

for X being set holds

( a [*] ("\/" (X,Q)) = "\/" ( { (a [*] b) where b is Element of Q : b in X } ,Q) & a delta ("/\" (X,Q)) = "/\" ( { (a delta c) where c is Element of Q : c in X } ,Q) )

proof end;

theorem :: QUANTAL1:28

for Q being Girard-Quantale

for a being Element of Q

for X being set holds

( ("\/" (X,Q)) [*] a = "\/" ( { (b [*] a) where b is Element of Q : b in X } ,Q) & ("/\" (X,Q)) delta a = "/\" ( { (c delta a) where c is Element of Q : c in X } ,Q) )

for a being Element of Q

for X being set holds

( ("\/" (X,Q)) [*] a = "\/" ( { (b [*] a) where b is Element of Q : b in X } ,Q) & ("/\" (X,Q)) delta a = "/\" ( { (c delta a) where c is Element of Q : c in X } ,Q) )

proof end;

theorem :: QUANTAL1:29

for Q being Girard-Quantale

for a, b, c being Element of Q holds

( a delta (b "/\" c) = (a delta b) "/\" (a delta c) & (b "/\" c) delta a = (b delta a) "/\" (c delta a) )

for a, b, c being Element of Q holds

( a delta (b "/\" c) = (a delta b) "/\" (a delta c) & (b "/\" c) delta a = (b delta a) "/\" (c delta a) )

proof end;

theorem :: QUANTAL1:30

for Q being Girard-Quantale

for a1, a2, b1, b2 being Element of Q st a1 [= b1 & a2 [= b2 holds

a1 delta a2 [= b1 delta b2

for a1, a2, b1, b2 being Element of Q st a1 [= b1 & a2 [= b2 holds

a1 delta a2 [= b1 delta b2

proof end;

theorem :: QUANTAL1:31

for Q being Girard-Quantale

for a, b, c being Element of Q holds (a delta b) delta c = a delta (b delta c)

for a, b, c being Element of Q holds (a delta b) delta c = a delta (b delta c)

proof end;

theorem Th32: :: QUANTAL1:32

for Q being Girard-Quantale

for a being Element of Q holds

( a [*] (Top Q) = a & (Top Q) [*] a = a )

for a being Element of Q holds

( a [*] (Top Q) = a & (Top Q) [*] a = a )

proof end;

theorem :: QUANTAL1:33

for Q being Girard-Quantale

for a being Element of Q holds

( a delta (Bottom Q) = a & (Bottom Q) delta a = a )

for a being Element of Q holds

( a delta (Bottom Q) = a & (Bottom Q) delta a = a )

proof end;

theorem :: QUANTAL1:34

for Q being Quantale

for j being UnOp of Q st j is monotone & j is idempotent & j is \/-distributive holds

ex L being complete Lattice st

( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) )

for j being UnOp of Q st j is monotone & j is idempotent & j is \/-distributive holds

ex L being complete Lattice st

( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) )

proof end;