begin
begin
theorem
for
V,
C being ( ( ) ( )
set )
for
A,
B being ( ( ) (
functional finite )
Element of
SubstitutionSet (
V : ( ( ) ( )
set ) ,
C : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) st
A : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) )
^ B : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) )
= A : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) holds
for
a being ( ( ) ( )
set ) st
a : ( ( ) ( )
set )
in A : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) holds
ex
b being ( ( ) ( )
set ) st
(
b : ( ( ) ( )
set )
in B : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) &
b : ( ( ) ( )
set )
c= a : ( ( ) ( )
set ) ) ;
theorem
for
V,
C being ( ( ) ( )
set )
for
A,
B being ( ( ) (
functional finite )
Element of
SubstitutionSet (
V : ( ( ) ( )
set ) ,
C : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) st
mi (A : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ^ B : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) )
= A : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) holds
for
a being ( ( ) ( )
set ) st
a : ( ( ) ( )
set )
in A : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) holds
ex
b being ( ( ) ( )
set ) st
(
b : ( ( ) ( )
set )
in B : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) &
b : ( ( ) ( )
set )
c= a : ( ( ) ( )
set ) ) ;
theorem
for
V,
C being ( ( ) ( )
set )
for
A,
B being ( ( ) (
functional finite )
Element of
SubstitutionSet (
V : ( ( ) ( )
set ) ,
C : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) st ( for
a being ( ( ) ( )
set ) st
a : ( ( ) ( )
set )
in A : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) holds
ex
b being ( ( ) ( )
set ) st
(
b : ( ( ) ( )
set )
in B : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) &
b : ( ( ) ( )
set )
c= a : ( ( ) ( )
set ) ) ) holds
mi (A : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ^ B : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) )
= A : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) ;
definition
let V be ( ( ) ( )
set ) ;
let C be ( (
finite ) (
finite )
set ) ;
let A be ( ( ) (
finite )
Element of
Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ;
func - A -> ( ( ) (
finite )
Element of
Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) )
equals
{ f : ( ( ) ( Relation-like Function-like ) Element of PFuncs ((Involved A : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( finite ) set ) ,C : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) ) where f is ( ( ) ( Relation-like Function-like ) Element of PFuncs ((Involved A : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) : for g being ( ( ) ( Relation-like Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) st g : ( ( ) ( Relation-like Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) ) in A : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds
not f : ( ( ) ( Relation-like Function-like ) Element of PFuncs ((Involved A : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( finite ) set ) ,C : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) ) tolerates g : ( ( ) ( Relation-like Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) ) } ;
end;
theorem
for
V being ( ( ) ( )
set )
for
C being ( (
finite ) (
finite )
set )
for
A being ( ( ) (
functional finite )
Element of
SubstitutionSet (
V : ( ( ) ( )
set ) ,
C : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) holds
mi (A : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) ) : ( ( ) ( non empty ) Element of bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ^ (- A : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) ) : ( ( ) ( non empty ) Element of bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) )
= Bottom (SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
V being ( ( non
empty ) ( non
empty )
set )
for
C being ( ( non
empty finite ) ( non
empty finite )
set )
for
A being ( ( ) (
functional finite )
Element of
SubstitutionSet (
V : ( ( non
empty ) ( non
empty )
set ) ,
C : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty finite ) ( non empty finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) st
A : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty finite ) ( non empty finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) )
= {} : ( ( ) (
Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty finite finite-yielding V47() )
set ) holds
mi (- A : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty finite ) ( non empty finite ) set ) ) : ( ( ) ( non empty ) Element of bool (Fin (PFuncs (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty finite ) ( non empty finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty finite ) ( non empty finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty finite ) ( non
empty finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty finite ) ( non empty finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) )
= Top (SubstLatt (V : ( ( non empty ) ( non empty ) set ) ,C : ( ( non empty finite ) ( non empty finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty finite ) ( non empty finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
V being ( ( ) ( )
set )
for
C being ( (
finite ) (
finite )
set )
for
A being ( ( ) (
functional finite )
Element of
SubstitutionSet (
V : ( ( ) ( )
set ) ,
C : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) )
for
a being ( ( ) (
Relation-like Function-like )
Element of
PFuncs (
V : ( ( ) ( )
set ) ,
C : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) )
for
B being ( ( ) (
functional finite )
Element of
SubstitutionSet (
V : ( ( ) ( )
set ) ,
C : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) st
B : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) )
= {a : ( ( ) ( Relation-like Function-like ) Element of PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) ) } : ( ( ) (
functional non
empty finite )
set ) &
A : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) )
^ B : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) )
= {} : ( ( ) (
Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty finite finite-yielding V47() )
set ) holds
ex
b being ( (
finite ) (
finite )
set ) st
(
b : ( (
finite ) (
finite )
set )
in - A : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) &
b : ( (
finite ) (
finite )
set )
c= a : ( ( ) (
Relation-like Function-like )
Element of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) ) ) ;
definition
let V be ( ( ) ( )
set ) ;
let C be ( (
finite ) (
finite )
set ) ;
let A,
B be ( ( ) (
finite )
Element of
Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ;
func A =>> B -> ( ( ) (
finite )
Element of
Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) )
equals
(PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) (
functional non
empty )
set )
/\ { (union { ((f : ( ( ) ( Relation-like Function-like ) Element of PFuncs (A : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,B : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) . i : ( ( ) ( Relation-like Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) ) ) : ( ( ) ( ) set ) \ i : ( ( ) ( Relation-like Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) ) ) : ( ( ) ( ) Element of bool (b1 : ( ( ) ( Relation-like Function-like ) Element of PFuncs (A : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,B : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) . b2 : ( ( ) ( Relation-like Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) where i is ( ( ) ( Relation-like Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( functional non empty ) set ) ) : i : ( ( ) ( Relation-like Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) ) in A : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) } ) : ( ( ) ( ) set ) where f is ( ( ) ( Relation-like Function-like ) Element of PFuncs (A : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,B : ( ( Function-like quasi_total ) ( Relation-like V : ( ( ) ( ) set ) -defined the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like non empty total quasi_total ) Element of bool [:V : ( ( ) ( ) set ) , the carrier of C : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) : dom f : ( ( ) ( Relation-like Function-like ) Element of PFuncs (A : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,B : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) : ( ( ) ( ) set ) = A : ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) } : ( ( ) ( )
set ) ;
end;
theorem
for
V being ( ( ) ( )
set )
for
C being ( (
finite ) (
finite )
set )
for
A,
B being ( ( ) (
finite )
Element of
Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) )
for
s being ( ( ) ( )
set ) st
s : ( ( ) ( )
set )
in A : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) )
=>> B : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) holds
ex
f being ( (
Function-like ) (
Relation-like b3 : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) )
-defined b4 : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) )
-valued Function-like finite )
PartFunc of ,) st
(
s : ( ( ) ( )
set )
= union { ((f : ( ( Function-like ) ( Relation-like b3 : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b4 : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -valued Function-like finite ) PartFunc of ,) . i : ( ( ) ( Relation-like Function-like ) Element of PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) ) ) : ( ( ) ( ) set ) \ i : ( ( ) ( Relation-like Function-like ) Element of PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) ) ) : ( ( ) ( ) Element of bool (b6 : ( ( Function-like ) ( Relation-like b3 : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b4 : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -valued Function-like finite ) PartFunc of ,) . b7 : ( ( ) ( Relation-like Function-like ) Element of PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) where i is ( ( ) ( Relation-like Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) ) : i : ( ( ) ( Relation-like Function-like ) Element of PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) ) in A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) } : ( ( ) ( )
set ) &
dom f : ( (
Function-like ) (
Relation-like b3 : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) )
-defined b4 : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) )
-valued Function-like finite )
PartFunc of ,) : ( ( ) (
finite )
Element of
bool b3 : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean finite V47() )
set ) )
= A : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) ;
begin
definition
let V be ( ( ) ( )
set ) ;
let C be ( (
finite ) (
finite )
set ) ;
func pseudo_compl (
V,
C)
-> ( (
Function-like quasi_total ) (
Relation-like the
carrier of
(SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
UnOp of the
carrier of
(SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) )
means
for
u being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
for
u9 being ( ( ) (
functional finite )
Element of
SubstitutionSet (
V : ( ( ) ( )
set ) ,
C : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) st
u9 : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
= u : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) holds
it : ( ( ) (
finite )
Element of
Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) )
. u : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) )
= mi (- u9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
finite )
Element of
Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) : ( ( ) (
functional finite )
Element of
SubstitutionSet (
V : ( ( ) ( )
set ) ,
C : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) ;
func StrongImpl (
V,
C)
-> ( (
Function-like quasi_total ) (
Relation-like [: the carrier of (SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined the
carrier of
(SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
BinOp of the
carrier of
(SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) )
means
for
u,
v being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
for
u9,
v9 being ( ( ) (
functional finite )
Element of
SubstitutionSet (
V : ( ( ) ( )
set ) ,
C : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) st
u9 : ( ( ) (
functional finite )
Element of
SubstitutionSet (
V : ( ( ) ( )
set ) ,
C : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) )
= u : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) &
v9 : ( ( ) (
functional finite )
Element of
SubstitutionSet (
V : ( ( ) ( )
set ) ,
C : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) )
= v : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) holds
it : ( ( ) (
finite )
Element of
Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) )
. (
u : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ,
v : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) )
= mi (u9 : ( ( ) ( functional finite ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) ) : ( ( ) ( non empty ) Element of bool (Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) =>> v9 : ( ( ) ( functional finite ) Element of SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) ) : ( ( ) ( non empty ) Element of bool (Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) (
finite )
Element of
Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) : ( ( ) (
functional finite )
Element of
SubstitutionSet (
V : ( ( ) ( )
set ) ,
C : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) ;
let u be ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ;
end;
definition
let V be ( ( ) ( )
set ) ;
let C be ( (
finite ) (
finite )
set ) ;
func Atom (
V,
C)
-> ( (
Function-like quasi_total ) (
Relation-like PFuncs (
V : ( ( ) ( )
set ) ,
C : ( ( ) ( )
set ) ) : ( ( ) (
functional non
empty )
set )
-defined the
carrier of
(SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of
PFuncs (
V : ( ( ) ( )
set ) ,
C : ( ( ) ( )
set ) ) : ( ( ) (
functional non
empty )
set ) , the
carrier of
(SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) )
means
for
a being ( ( ) (
Relation-like Function-like )
Element of
PFuncs (
V : ( ( ) ( )
set ) ,
C : ( ( ) ( )
set ) ) : ( ( ) (
functional non
empty )
set ) ) holds
it : ( ( ) (
finite )
Element of
Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) )
. a : ( ( ) (
Relation-like Function-like )
Element of
PFuncs (
V : ( ( ) ( )
set ) ,
C : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) )
= mi {.a : ( ( ) ( Relation-like Function-like ) Element of PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) ) .} : ( ( ) (
functional non
empty finite )
Element of
Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) : ( ( ) (
functional finite )
Element of
SubstitutionSet (
V : ( ( ) ( )
set ) ,
C : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) ;
end;
theorem
for
V being ( ( ) ( )
set )
for
C being ( (
finite ) (
finite )
set )
for
K being ( ( ) (
functional finite )
Element of
SubstitutionSet (
V : ( ( ) ( )
set ) ,
C : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) holds
FinJoin (
K : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) ,
(Atom (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( (
Function-like quasi_total ) (
Relation-like PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set )
-defined the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) , the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) )
= FinUnion (
K : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) ,
(singleton (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
Function-like quasi_total ) (
Relation-like PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set )
-defined Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set )
-valued Function-like non
empty total quasi_total )
Element of
bool [:(PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ,(Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ;
theorem
for
V being ( ( ) ( )
set )
for
C being ( (
finite ) (
finite )
set )
for
u being ( ( ) (
functional finite )
Element of
SubstitutionSet (
V : ( ( ) ( )
set ) ,
C : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) holds
u : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) )
= FinJoin (
u : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) ,
(Atom (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( (
Function-like quasi_total ) (
Relation-like PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set )
-defined the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) , the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
V being ( ( ) ( )
set )
for
C being ( (
finite ) (
finite )
set )
for
a being ( ( ) (
Relation-like Function-like )
Element of
PFuncs (
V : ( ( ) ( )
set ) ,
C : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) ) st
a : ( ( ) (
Relation-like Function-like )
Element of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) ) is
finite holds
for
c being ( ( ) ( )
set ) st
c : ( ( ) ( )
set )
in (Atom (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( (
Function-like quasi_total ) (
Relation-like PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set )
-defined the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) , the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) )
. a : ( ( ) (
Relation-like Function-like )
Element of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) ) holds
c : ( ( ) ( )
set )
= a : ( ( ) (
Relation-like Function-like )
Element of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) ) ;
theorem
for
V being ( ( ) ( )
set )
for
C being ( (
finite ) (
finite )
set )
for
u being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
for
K,
L being ( ( ) (
functional finite )
Element of
SubstitutionSet (
V : ( ( ) ( )
set ) ,
C : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) )
for
a being ( ( ) (
Relation-like Function-like )
Element of
PFuncs (
V : ( ( ) ( )
set ) ,
C : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) ) st
K : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) )
= {a : ( ( ) ( Relation-like Function-like ) Element of PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) ) } : ( ( ) (
functional non
empty finite )
set ) &
L : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) )
= u : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) &
L : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) )
^ K : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) )
= {} : ( ( ) (
Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty finite finite-yielding V47() )
set ) holds
(Atom (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( (
Function-like quasi_total ) (
Relation-like PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set )
-defined the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) , the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) )
. a : ( ( ) (
Relation-like Function-like )
Element of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) )
[= (pseudo_compl (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
UnOp of the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) )
. u : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
V being ( ( ) ( )
set )
for
C being ( (
finite ) (
finite )
set )
for
a being ( (
finite ) (
Relation-like Function-like finite )
Element of
PFuncs (
V : ( ( ) ( )
set ) ,
C : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) ) holds
a : ( (
finite ) (
Relation-like Function-like finite )
Element of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) )
in (Atom (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( (
Function-like quasi_total ) (
Relation-like PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set )
-defined the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) , the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) )
. a : ( (
finite ) (
Relation-like Function-like finite )
Element of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
V being ( ( ) ( )
set )
for
C being ( (
finite ) (
finite )
set )
for
a being ( ( ) (
Relation-like Function-like )
Element of
PFuncs (
V : ( ( ) ( )
set ) ,
C : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) )
for
u,
v being ( ( ) (
functional finite )
Element of
SubstitutionSet (
V : ( ( ) ( )
set ) ,
C : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) st ( for
c being ( ( ) ( )
set ) st
c : ( ( ) ( )
set )
in u : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) holds
ex
b being ( ( ) ( )
set ) st
(
b : ( ( ) ( )
set )
in v : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) &
b : ( ( ) ( )
set )
c= c : ( ( ) ( )
set )
\/ a : ( ( ) (
Relation-like Function-like )
Element of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
set ) ) ) holds
ex
b being ( ( ) ( )
set ) st
(
b : ( ( ) ( )
set )
in u : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) )
=>> v : ( ( ) (
functional finite )
Element of
SubstitutionSet (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) ( non
empty )
Element of
bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) : ( ( ) (
finite )
Element of
Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) (
functional non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) &
b : ( ( ) ( )
set )
c= a : ( ( ) (
Relation-like Function-like )
Element of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) ) ) ;
theorem
for
V being ( ( ) ( )
set )
for
C being ( (
finite ) (
finite )
set )
for
u,
v being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
for
a being ( (
finite ) (
Relation-like Function-like finite )
Element of
PFuncs (
V : ( ( ) ( )
set ) ,
C : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) ) st ( for
b being ( ( ) (
Relation-like Function-like )
Element of
PFuncs (
V : ( ( ) ( )
set ) ,
C : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) ) st
b : ( ( ) (
Relation-like Function-like )
Element of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) )
in u : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) holds
b : ( ( ) (
Relation-like Function-like )
Element of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) )
tolerates a : ( (
finite ) (
Relation-like Function-like finite )
Element of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) ) ) &
u : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
"/\" ((Atom (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) -defined the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) , the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() ) LattStr ) : ( ( ) ( non empty ) set ) ) . a : ( ( finite ) ( Relation-like Function-like finite ) Element of PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) ) : ( ( ) ( functional non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) )
[= v : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) holds
(Atom (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( (
Function-like quasi_total ) (
Relation-like PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set )
-defined the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) , the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) )
. a : ( (
finite ) (
Relation-like Function-like finite )
Element of
PFuncs (
b1 : ( ( ) ( )
set ) ,
b2 : ( (
finite ) (
finite )
set ) ) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) )
[= (StrongImpl (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set )
-defined the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
BinOp of the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) )
. (
u : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ,
v : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
V being ( ( ) ( )
set )
for
C being ( (
finite ) (
finite )
set )
for
u,
v being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) holds
u : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
"/\" ((StrongImpl (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) BinOp of the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() ) LattStr ) : ( ( ) ( non empty ) set ) ) . (u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() )
LattStr ) : ( ( ) ( non
empty )
set ) )
[= v : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ;
theorem
for
V being ( ( ) ( )
set )
for
C being ( (
finite ) (
finite )
set )
for
u,
v being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) holds
u : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
=> v : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80()
implicative Heyting )
LattStr ) : ( ( ) ( non
empty )
set ) )
= FinJoin (
(SUB u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
finite )
Element of
Fin the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80()
implicative Heyting )
LattStr ) : ( ( ) ( non
empty )
set ) : ( (
preBoolean ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ,
( the L_meet of (SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total having_a_unity commutative associative idempotent ) Element of bool [:[: the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) .: ((pseudo_compl (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) UnOp of the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) ) ,((StrongImpl (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) BinOp of the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) ) [:] ((diff u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) UnOp of the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [: the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) )) : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80()
implicative Heyting )
LattStr ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80()
implicative Heyting )
LattStr ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Element of
bool [: the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80() implicative Heyting ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty cup-closed diff-closed preBoolean )
set ) ) ) : ( ( ) ( )
Element of the
carrier of
(SubstLatt (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( (
strict ) ( non
empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V80()
implicative Heyting )
LattStr ) : ( ( ) ( non
empty )
set ) ) ;