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

registration
let I be set ;
let X be ManySortedSet of I;
let Y be V6 ManySortedSet of I;
cluster X \/ Y -> V6 ;
coherence
X \/ Y is non-empty
proof end;
cluster Y \/ X -> V6 ;
coherence
Y \/ X is non-empty
;
end;

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

theorem Th2: :: MSUALG_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for X, Y being ManySortedSet of I
for i being Element of I * holds product ((X /\ Y) * i) = (product (X * i)) /\ (product (Y * i))
proof end;

definition
let S be non empty ManySortedSign ;
let U0 be MSAlgebra of S;
mode MSSubset of U0 is ManySortedSubset of the Sorts of U0;
end;

definition
let S be non empty ManySortedSign ;
let IT be SortSymbol of S;
canceled;
attr IT is with_const_op means :Def2: :: MSUALG_2:def 2
ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = IT );
end;

:: deftheorem MSUALG_2:def 1 :
canceled;

:: deftheorem Def2 defines with_const_op MSUALG_2:def 2 :
for S being non empty ManySortedSign
for IT being SortSymbol of S holds
( IT is with_const_op iff ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = IT ) );

definition
let IT be non empty ManySortedSign ;
attr IT is all-with_const_op means :Def3: :: MSUALG_2:def 3
for s being SortSymbol of IT holds s is with_const_op;
end;

:: deftheorem Def3 defines all-with_const_op MSUALG_2:def 3 :
for IT being non empty ManySortedSign holds
( IT is all-with_const_op iff for s being SortSymbol of IT holds s is with_const_op );

registration
let A be non empty set ;
let B be set ;
let a be Function of B,A * ;
let r be Function of B,A;
cluster ManySortedSign(# A,B,a,r #) -> non empty ;
coherence
not ManySortedSign(# A,B,a,r #) is empty
by STRUCT_0:def 1;
end;

registration
cluster non empty strict non void all-with_const_op ManySortedSign ;
existence
ex b1 being non empty ManySortedSign st
( not b1 is void & b1 is all-with_const_op & b1 is strict )
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let s be SortSymbol of S;
func Constants U0,s -> Subset of (the Sorts of U0 . s) means :Def4: :: MSUALG_2:def 4
ex A being non empty set st
( A = the Sorts of U0 . s & it = { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den o,U0) )
}
) if the Sorts of U0 . s <> {}
otherwise it = {} ;
existence
( ( the Sorts of U0 . s <> {} implies ex b1 being Subset of (the Sorts of U0 . s) ex A being non empty set st
( A = the Sorts of U0 . s & b1 = { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den o,U0) )
}
) ) & ( not the Sorts of U0 . s <> {} implies ex b1 being Subset of (the Sorts of U0 . s) st b1 = {} ) )
proof end;
correctness
consistency
for b1 being Subset of (the Sorts of U0 . s) holds verum
;
uniqueness
for b1, b2 being Subset of (the Sorts of U0 . s) holds
( ( the Sorts of U0 . s <> {} & ex A being non empty set st
( A = the Sorts of U0 . s & b1 = { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den o,U0) )
}
) & ex A being non empty set st
( A = the Sorts of U0 . s & b2 = { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den o,U0) )
}
) implies b1 = b2 ) & ( not the Sorts of U0 . s <> {} & b1 = {} & b2 = {} implies b1 = b2 ) )
;
;
end;

:: deftheorem Def4 defines Constants MSUALG_2:def 4 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for s being SortSymbol of S
for b4 being Subset of (the Sorts of U0 . s) holds
( ( the Sorts of U0 . s <> {} implies ( b4 = Constants U0,s iff ex A being non empty set st
( A = the Sorts of U0 . s & b4 = { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den o,U0) )
}
) ) ) & ( not the Sorts of U0 . s <> {} implies ( b4 = Constants U0,s iff b4 = {} ) ) );

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
func Constants U0 -> MSSubset of U0 means :Def5: :: MSUALG_2:def 5
for s being SortSymbol of S holds it . s = Constants U0,s;
existence
ex b1 being MSSubset of U0 st
for s being SortSymbol of S holds b1 . s = Constants U0,s
proof end;
uniqueness
for b1, b2 being MSSubset of U0 st ( for s being SortSymbol of S holds b1 . s = Constants U0,s ) & ( for s being SortSymbol of S holds b2 . s = Constants U0,s ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Constants MSUALG_2:def 5 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for b3 being MSSubset of U0 holds
( b3 = Constants U0 iff for s being SortSymbol of S holds b3 . s = Constants U0,s );

registration
let S be non empty non void all-with_const_op ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
let s be SortSymbol of S;
cluster Constants U0,s -> non empty ;
coherence
not Constants U0,s is empty
proof end;
end;

registration
let S be non empty non void all-with_const_op ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
cluster Constants U0 -> V6 ;
coherence
Constants U0 is non-empty
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let o be OperSymbol of S;
let A be MSSubset of U0;
pred A is_closed_on o means :Def6: :: MSUALG_2:def 6
rng ((Den o,U0) | (((A # ) * the Arity of S) . o)) c= (A * the ResultSort of S) . o;
end;

:: deftheorem Def6 defines is_closed_on MSUALG_2:def 6 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for o being OperSymbol of S
for A being MSSubset of U0 holds
( A is_closed_on o iff rng ((Den o,U0) | (((A # ) * the Arity of S) . o)) c= (A * the ResultSort of S) . o );

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let A be MSSubset of U0;
attr A is opers_closed means :Def7: :: MSUALG_2:def 7
for o being OperSymbol of S holds A is_closed_on o;
end;

:: deftheorem Def7 defines opers_closed MSUALG_2:def 7 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0 holds
( A is opers_closed iff for o being OperSymbol of S holds A is_closed_on o );

theorem Th3: :: MSUALG_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U0 being MSAlgebra of S
for B0, B1 being MSSubset of U0 st B0 c= B1 holds
((B0 # ) * the Arity of S) . o c= ((B1 # ) * the Arity of S) . o
proof end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let o be OperSymbol of S;
let A be MSSubset of U0;
assume A1: A is_closed_on o ;
func o /. A -> Function of ((A # ) * the Arity of S) . o,(A * the ResultSort of S) . o equals :Def8: :: MSUALG_2:def 8
(Den o,U0) | (((A # ) * the Arity of S) . o);
coherence
(Den o,U0) | (((A # ) * the Arity of S) . o) is Function of ((A # ) * the Arity of S) . o,(A * the ResultSort of S) . o
proof end;
end;

:: deftheorem Def8 defines /. MSUALG_2:def 8 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for o being OperSymbol of S
for A being MSSubset of U0 st A is_closed_on o holds
o /. A = (Den o,U0) | (((A # ) * the Arity of S) . o);

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let A be MSSubset of U0;
func Opers U0,A -> ManySortedFunction of (A # ) * the Arity of S,A * the ResultSort of S means :Def9: :: MSUALG_2:def 9
for o being OperSymbol of S holds it . o = o /. A;
existence
ex b1 being ManySortedFunction of (A # ) * the Arity of S,A * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = o /. A
proof end;
uniqueness
for b1, b2 being ManySortedFunction of (A # ) * the Arity of S,A * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = o /. A ) & ( for o being OperSymbol of S holds b2 . o = o /. A ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines Opers MSUALG_2:def 9 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0
for b4 being ManySortedFunction of (A # ) * the Arity of S,A * the ResultSort of S holds
( b4 = Opers U0,A iff for o being OperSymbol of S holds b4 . o = o /. A );

theorem Th4: :: MSUALG_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for B being MSSubset of U0 st B = the Sorts of U0 holds
( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den o,U0 ) )
proof end;

theorem Th5: :: MSUALG_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for B being MSSubset of U0 st B = the Sorts of U0 holds
Opers U0,B = the Charact of U0
proof end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
mode MSSubAlgebra of U0 -> MSAlgebra of S means :Def10: :: MSUALG_2:def 10
( the Sorts of it is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of it holds
( B is opers_closed & the Charact of it = Opers U0,B ) ) );
existence
ex b1 being MSAlgebra of S st
( the Sorts of b1 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of b1 holds
( B is opers_closed & the Charact of b1 = Opers U0,B ) ) )
proof end;
end;

:: deftheorem Def10 defines MSSubAlgebra MSUALG_2:def 10 :
for S being non empty non void ManySortedSign
for U0, b3 being MSAlgebra of S holds
( b3 is MSSubAlgebra of U0 iff ( the Sorts of b3 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of b3 holds
( B is opers_closed & the Charact of b3 = Opers U0,B ) ) ) );

Lm1: for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S holds MSAlgebra(# the Sorts of U0,the Charact of U0 #) is MSSubAlgebra of U0
proof end;

registration
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
cluster strict MSSubAlgebra of U0;
existence
ex b1 being MSSubAlgebra of U0 st b1 is strict
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
cluster MSAlgebra(# the Sorts of U0,the Charact of U0 #) -> non-empty ;
coherence
MSAlgebra(# the Sorts of U0,the Charact of U0 #) is non-empty
by MSUALG_1:def 8;
end;

registration
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
cluster strict non-empty MSSubAlgebra of U0;
existence
ex b1 being MSSubAlgebra of U0 st
( b1 is non-empty & b1 is strict )
proof end;
end;

theorem :: MSUALG_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S holds U0 is MSSubAlgebra of U0
proof end;

theorem :: MSUALG_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0, U1, U2 being MSAlgebra of S st U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 holds
U0 is MSSubAlgebra of U2
proof end;

theorem Th8: :: MSUALG_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra of S st U1 is strict MSSubAlgebra of U2 & U2 is strict MSSubAlgebra of U1 holds
U1 = U2
proof end;

theorem Th9: :: MSUALG_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 c= the Sorts of U2 holds
U1 is MSSubAlgebra of U2
proof end;

theorem Th10: :: MSUALG_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for U1, U2 being strict MSSubAlgebra of U0 st the Sorts of U1 = the Sorts of U2 holds
U1 = U2
proof end;

theorem Th11: :: MSUALG_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1
proof end;

theorem :: MSUALG_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void all-with_const_op ManySortedSign
for U0 being non-empty MSAlgebra of S
for U1 being non-empty MSSubAlgebra of U0 holds Constants U0 is V6 MSSubset of U1 by Th11;

theorem :: MSUALG_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void all-with_const_op ManySortedSign
for U0 being non-empty MSAlgebra of S
for U1, U2 being non-empty MSSubAlgebra of U0 holds the Sorts of U1 /\ the Sorts of U2 is non-empty
proof end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let A be MSSubset of U0;
func SubSort A -> set means :Def11: :: MSUALG_2:def 11
for x being set holds
( x in it iff ( x in Funcs the carrier of S,(bool (Union the Sorts of U0)) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x in Funcs the carrier of S,(bool (Union the Sorts of U0)) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in Funcs the carrier of S,(bool (Union the Sorts of U0)) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) ) & ( for x being set holds
( x in b2 iff ( x in Funcs the carrier of S,(bool (Union the Sorts of U0)) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines SubSort MSUALG_2:def 11 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0
for b4 being set holds
( b4 = SubSort A iff for x being set holds
( x in b4 iff ( x in Funcs the carrier of S,(bool (Union the Sorts of U0)) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) );

Lm2: for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0 holds the Sorts of U0 in SubSort A
proof end;

registration
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let A be MSSubset of U0;
cluster SubSort A -> non empty ;
coherence
not SubSort A is empty
by Lm2;
end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
func SubSort U0 -> set means :Def12: :: MSUALG_2:def 12
for x being set holds
( x in it iff ( x in Funcs the carrier of S,(bool (Union the Sorts of U0)) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
B is opers_closed ) ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x in Funcs the carrier of S,(bool (Union the Sorts of U0)) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
B is opers_closed ) ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in Funcs the carrier of S,(bool (Union the Sorts of U0)) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
B is opers_closed ) ) ) ) & ( for x being set holds
( x in b2 iff ( x in Funcs the carrier of S,(bool (Union the Sorts of U0)) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
B is opers_closed ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines SubSort MSUALG_2:def 12 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for b3 being set holds
( b3 = SubSort U0 iff for x being set holds
( x in b3 iff ( x in Funcs the carrier of S,(bool (Union the Sorts of U0)) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
B is opers_closed ) ) ) );

registration
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
cluster SubSort U0 -> non empty ;
coherence
not SubSort U0 is empty
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let e be Element of SubSort U0;
func @ e -> MSSubset of U0 equals :: MSUALG_2:def 13
e;
coherence
e is MSSubset of U0
by Def12;
end;

:: deftheorem defines @ MSUALG_2:def 13 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for e being Element of SubSort U0 holds @ e = e;

theorem Th14: :: MSUALG_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A, B being MSSubset of U0 holds
( B in SubSort A iff ( B is opers_closed & Constants U0 c= B & A c= B ) )
proof end;

theorem Th15: :: MSUALG_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for B being MSSubset of U0 holds
( B in SubSort U0 iff B is opers_closed )
proof end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let A be MSSubset of U0;
let s be SortSymbol of S;
func SubSort A,s -> set means :Def14: :: MSUALG_2:def 14
for x being set holds
( x in it iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) ) & ( for x being set holds
( x in b2 iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines SubSort MSUALG_2:def 14 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0
for s being SortSymbol of S
for b5 being set holds
( b5 = SubSort A,s iff for x being set holds
( x in b5 iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) );

registration
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let A be MSSubset of U0;
let s be SortSymbol of S;
cluster SubSort A,s -> non empty ;
coherence
not SubSort A,s is empty
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let A be MSSubset of U0;
func MSSubSort A -> MSSubset of U0 means :Def15: :: MSUALG_2:def 15
for s being SortSymbol of S holds it . s = meet (SubSort A,s);
existence
ex b1 being MSSubset of U0 st
for s being SortSymbol of S holds b1 . s = meet (SubSort A,s)
proof end;
uniqueness
for b1, b2 being MSSubset of U0 st ( for s being SortSymbol of S holds b1 . s = meet (SubSort A,s) ) & ( for s being SortSymbol of S holds b2 . s = meet (SubSort A,s) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines MSSubSort MSUALG_2:def 15 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A, b4 being MSSubset of U0 holds
( b4 = MSSubSort A iff for s being SortSymbol of S holds b4 . s = meet (SubSort A,s) );

theorem Th16: :: MSUALG_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0 holds (Constants U0) \/ A c= MSSubSort A
proof end;

theorem Th17: :: MSUALG_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0 st (Constants U0) \/ A is non-empty holds
MSSubSort A is non-empty
proof end;

theorem Th18: :: MSUALG_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U0 being MSAlgebra of S
for A, B being MSSubset of U0 st B in SubSort A holds
(((MSSubSort A) # ) * the Arity of S) . o c= ((B # ) * the Arity of S) . o
proof end;

theorem Th19: :: MSUALG_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U0 being MSAlgebra of S
for A, B being MSSubset of U0 st B in SubSort A holds
rng ((Den o,U0) | ((((MSSubSort A) # ) * the Arity of S) . o)) c= (B * the ResultSort of S) . o
proof end;

theorem Th20: :: MSUALG_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U0 being MSAlgebra of S
for A being MSSubset of U0 holds rng ((Den o,U0) | ((((MSSubSort A) # ) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o
proof end;

theorem Th21: :: MSUALG_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0 holds
( MSSubSort A is opers_closed & A c= MSSubSort A )
proof end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let A be MSSubset of U0;
assume A1: A is opers_closed ;
func U0 | A -> strict MSSubAlgebra of U0 equals :Def16: :: MSUALG_2:def 16
MSAlgebra(# A,(Opers U0,A) #);
coherence
MSAlgebra(# A,(Opers U0,A) #) is strict MSSubAlgebra of U0
proof end;
end;

:: deftheorem Def16 defines | MSUALG_2:def 16 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0 st A is opers_closed holds
U0 | A = MSAlgebra(# A,(Opers U0,A) #);

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let U1, U2 be MSSubAlgebra of U0;
func U1 /\ U2 -> strict MSSubAlgebra of U0 means :Def17: :: MSUALG_2:def 17
( the Sorts of it = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of it holds
( B is opers_closed & the Charact of it = Opers U0,B ) ) );
existence
ex b1 being strict MSSubAlgebra of U0 st
( the Sorts of b1 = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b1 holds
( B is opers_closed & the Charact of b1 = Opers U0,B ) ) )
proof end;
uniqueness
for b1, b2 being strict MSSubAlgebra of U0 st the Sorts of b1 = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b1 holds
( B is opers_closed & the Charact of b1 = Opers U0,B ) ) & the Sorts of b2 = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b2 holds
( B is opers_closed & the Charact of b2 = Opers U0,B ) ) holds
b1 = b2
by Th10;
end;

:: deftheorem Def17 defines /\ MSUALG_2:def 17 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for U1, U2 being MSSubAlgebra of U0
for b5 being strict MSSubAlgebra of U0 holds
( b5 = U1 /\ U2 iff ( the Sorts of b5 = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b5 holds
( B is opers_closed & the Charact of b5 = Opers U0,B ) ) ) );

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let A be MSSubset of U0;
func GenMSAlg A -> strict MSSubAlgebra of U0 means :Def18: :: MSUALG_2:def 18
( A is MSSubset of it & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
it is MSSubAlgebra of U1 ) );
existence
ex b1 being strict MSSubAlgebra of U0 st
( A is MSSubset of b1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b1 is MSSubAlgebra of U1 ) )
proof end;
uniqueness
for b1, b2 being strict MSSubAlgebra of U0 st A is MSSubset of b1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b1 is MSSubAlgebra of U1 ) & A is MSSubset of b2 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b2 is MSSubAlgebra of U1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines GenMSAlg MSUALG_2:def 18 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0
for b4 being strict MSSubAlgebra of U0 holds
( b4 = GenMSAlg A iff ( A is MSSubset of b4 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b4 is MSSubAlgebra of U1 ) ) );

registration
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
let A be V6 MSSubset of U0;
cluster GenMSAlg A -> strict non-empty ;
coherence
GenMSAlg A is non-empty
proof end;
end;

theorem Th22: :: MSUALG_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being strict MSAlgebra of S
for B being MSSubset of U0 st B = the Sorts of U0 holds
GenMSAlg B = U0
proof end;

theorem Th23: :: MSUALG_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for U1 being strict MSSubAlgebra of U0
for B being MSSubset of U0 st B = the Sorts of U1 holds
GenMSAlg B = U1
proof end;

theorem Th24: :: MSUALG_2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for U1 being MSSubAlgebra of U0 holds (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0)
proof end;

definition
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
let U1, U2 be MSSubAlgebra of U0;
func U1 "\/" U2 -> strict MSSubAlgebra of U0 means :Def19: :: MSUALG_2:def 19
for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
it = GenMSAlg A;
existence
ex b1 being strict MSSubAlgebra of U0 st
for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b1 = GenMSAlg A
proof end;
uniqueness
for b1, b2 being strict MSSubAlgebra of U0 st ( for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b1 = GenMSAlg A ) & ( for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b2 = GenMSAlg A ) holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines "\/" MSUALG_2:def 19 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for U1, U2 being MSSubAlgebra of U0
for b5 being strict MSSubAlgebra of U0 holds
( b5 = U1 "\/" U2 iff for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b5 = GenMSAlg A );

theorem Th25: :: MSUALG_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for U1 being MSSubAlgebra of U0
for A, B being MSSubset of U0 st B = A \/ the Sorts of U1 holds
(GenMSAlg A) "\/" U1 = GenMSAlg B
proof end;

theorem Th26: :: MSUALG_2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for U1 being MSSubAlgebra of U0
for B being MSSubset of U0 st B = the Sorts of U0 holds
(GenMSAlg B) "\/" U1 = GenMSAlg B
proof end;

theorem Th27: :: MSUALG_2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for U1, U2 being MSSubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1
proof end;

theorem Th28: :: MSUALG_2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for U1, U2 being strict MSSubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = U1
proof end;

theorem Th29: :: MSUALG_2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for U1, U2 being strict MSSubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = U2
proof end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
func MSSub U0 -> set means :Def20: :: MSUALG_2:def 20
for x being set holds
( x in it iff x is strict MSSubAlgebra of U0 );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is strict MSSubAlgebra of U0 )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict MSSubAlgebra of U0 ) ) & ( for x being set holds
( x in b2 iff x is strict MSSubAlgebra of U0 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines MSSub MSUALG_2:def 20 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for b3 being set holds
( b3 = MSSub U0 iff for x being set holds
( x in b3 iff x is strict MSSubAlgebra of U0 ) );

registration
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
cluster MSSub U0 -> non empty ;
coherence
not MSSub U0 is empty
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
func MSAlg_join U0 -> BinOp of MSSub U0 means :Def21: :: MSUALG_2:def 21
for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
it . x,y = U1 "\/" U2;
existence
ex b1 being BinOp of MSSub U0 st
for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 "\/" U2
proof end;
uniqueness
for b1, b2 being BinOp of MSSub U0 st ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 "\/" U2 ) & ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b2 . x,y = U1 "\/" U2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def21 defines MSAlg_join MSUALG_2:def 21 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for b3 being BinOp of MSSub U0 holds
( b3 = MSAlg_join U0 iff for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b3 . x,y = U1 "\/" U2 );

definition
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
func MSAlg_meet U0 -> BinOp of MSSub U0 means :Def22: :: MSUALG_2:def 22
for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
it . x,y = U1 /\ U2;
existence
ex b1 being BinOp of MSSub U0 st
for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 /\ U2
proof end;
uniqueness
for b1, b2 being BinOp of MSSub U0 st ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . x,y = U1 /\ U2 ) & ( for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b2 . x,y = U1 /\ U2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines MSAlg_meet MSUALG_2:def 22 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for b3 being BinOp of MSSub U0 holds
( b3 = MSAlg_meet U0 iff for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b3 . x,y = U1 /\ U2 );

theorem Th30: :: MSUALG_2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S holds MSAlg_join U0 is commutative
proof end;

theorem Th31: :: MSUALG_2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S holds MSAlg_join U0 is associative
proof end;

theorem Th32: :: MSUALG_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S holds MSAlg_meet U0 is commutative
proof end;

theorem Th33: :: MSUALG_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S holds MSAlg_meet U0 is associative
proof end;

definition
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
func MSSubAlLattice U0 -> strict Lattice equals :: MSUALG_2:def 23
LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #);
coherence
LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is strict Lattice
proof end;
end;

:: deftheorem defines MSSubAlLattice MSUALG_2:def 23 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S holds MSSubAlLattice U0 = LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #);

theorem Th34: :: MSUALG_2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S holds MSSubAlLattice U0 is bounded
proof end;

registration
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
cluster MSSubAlLattice U0 -> strict bounded ;
coherence
MSSubAlLattice U0 is bounded
by Th34;
end;

theorem :: MSUALG_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S holds Bottom (MSSubAlLattice U0) = GenMSAlg (Constants U0)
proof end;

theorem Th36: :: MSUALG_2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for B being MSSubset of U0 st B = the Sorts of U0 holds
Top (MSSubAlLattice U0) = GenMSAlg B
proof end;

theorem :: MSUALG_2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being strict non-empty MSAlgebra of S holds Top (MSSubAlLattice U0) = U0
proof end;

theorem :: MSUALG_2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S holds MSAlgebra(# the Sorts of U0,the Charact of U0 #) is MSSubAlgebra of U0 by Lm1;

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

theorem :: MSUALG_2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0 holds the Sorts of U0 in SubSort A by Lm2;

theorem :: MSUALG_2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0 holds SubSort A c= SubSort U0
proof end;