:: MSSUBLAT semantic presentation

theorem Th1: :: MSSUBLAT:1

for a being set holds (*--> a) . 0 = {}

proof end;

theorem :: MSSUBLAT:2

for a being set holds (*--> a) . 1 = <*a*>

proof end;

theorem :: MSSUBLAT:3

for a being set holds (*--> a) . 2 = <*a,a*>

proof end;

theorem :: MSSUBLAT:4

for a being set holds (*--> a) . 3 = <*a,a,a*>

proof end;

theorem Th5: :: MSSUBLAT:5

for i being Nat
for f being FinSequence of {0} holds
( f = i |-> 0 iff len f = i )

proof end;

theorem Th6: :: MSSUBLAT:6

for i being Nat
for f being FinSequence st f = (*--> 0) . i holds
len f = i

proof end;

theorem Th7: :: MSSUBLAT:7

for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
MSSign U1 = MSSign U2

proof end;

registration

let U0 be Universal_Algebra;
cluster the charact of U0 -> Function-yielding ;
coherence

proof end;

end;

theorem Th8: :: MSSUBLAT:8

for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
for o being OperSymbol of (MSSign U2)
for a being OperSymbol of (MSSign U1) st a = o holds
Den a,(MSAlg U1) = (Den o,(MSAlg U2)) | (Args a,(MSAlg U1))

proof end;

theorem Th9: :: MSSUBLAT:9

for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2)

proof end;

theorem Th10: :: MSSUBLAT:10

for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
B is opers_closed

proof end;

theorem Th11: :: MSSUBLAT:11

for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
the Charact of (MSAlg U1) = Opers (MSAlg U2),B

proof end;

theorem Th12: :: MSSUBLAT:12

for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
MSAlg U1 is MSSubAlgebra of MSAlg U2

proof end;

theorem Th13: :: MSSUBLAT:13

for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds
the carrier of U1 is Subset of U2

proof end;

theorem Th14: :: MSSUBLAT:14

for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds
for B being non empty Subset of U2 st B = the carrier of U1 holds
B is opers_closed

proof end;

theorem Th15: :: MSSUBLAT:15

for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds
for B being non empty Subset of U2 st B = the carrier of U1 holds
the charact of U1 = Opers U2,B

proof end;

theorem Th16: :: MSSUBLAT:16

for U1, U2 being Universal_Algebra st MSAlg U1 is MSSubAlgebra of MSAlg U2 holds
U1 is SubAlgebra of U2

proof end;

theorem Th17: :: MSSUBLAT:17

for MS being non empty trivial non void segmental ManySortedSign
for A being non-empty MSAlgebra of MS
for B being non-empty MSSubAlgebra of A holds the carrier of (1-Alg B) is Subset of (1-Alg A)

proof end;

theorem Th18: :: MSSUBLAT:18

for MS being non empty trivial non void segmental ManySortedSign
for A being non-empty MSAlgebra of MS
for B being non-empty MSSubAlgebra of A
for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
S is opers_closed

proof end;

theorem Th19: :: MSSUBLAT:19

proof end;

theorem Th20: :: MSSUBLAT:20

for MS being non empty trivial non void segmental ManySortedSign
for A being non-empty MSAlgebra of MS
for B being non-empty MSSubAlgebra of A holds 1-Alg B is SubAlgebra of 1-Alg A

proof end;

theorem Th21: :: MSSUBLAT:21

for S being non empty non void ManySortedSign
for A, B being MSAlgebra of S holds
( A is MSSubAlgebra of B iff A is MSSubAlgebra of MSAlgebra(# the Sorts of B,the Charact of B #) )

proof end;

theorem :: MSSUBLAT:22

for A, B being Universal_Algebra holds
( signature A = signature B iff MSSign A = MSSign B )

proof end;

theorem Th23: :: MSSUBLAT:23

for MS being non empty trivial non void segmental ManySortedSign
for A being non-empty MSAlgebra of MS st the carrier of MS = {0} holds
MSSign (1-Alg A) = ManySortedSign(# the carrier of MS,the OperSymbols of MS,the Arity of MS,the ResultSort of MS #)

proof end;

theorem Th24: :: MSSUBLAT:24

for MS being non empty trivial non void segmental ManySortedSign
for A, B being non-empty MSAlgebra of MS st the carrier of MS = {0} & 1-Alg A = 1-Alg B holds
MSAlgebra(# the Sorts of A,the Charact of A #) = MSAlgebra(# the Sorts of B,the Charact of B #)

proof end;

theorem :: MSSUBLAT:25

for MS being non empty trivial non void segmental ManySortedSign
for A being non-empty MSAlgebra of MS st the carrier of MS = {0} holds
the Sorts of A = the Sorts of (MSAlg (1-Alg A))

proof end;

theorem Th26: :: MSSUBLAT:26

for MS being non empty trivial non void segmental ManySortedSign
for A being non-empty MSAlgebra of MS st the carrier of MS = {0} holds
MSAlg (1-Alg A) = MSAlgebra(# the Sorts of A,the Charact of A #)

proof end;

theorem :: MSSUBLAT:27

for A being Universal_Algebra
for B being strict non-empty MSSubAlgebra of MSAlg A st the carrier of (MSSign A) = {0} holds
1-Alg B is SubAlgebra of A

proof end;

theorem Th28: :: MSSUBLAT:28

for A being Universal_Algebra
for a1, b1 being strict non-empty SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
the Sorts of a2 \/ the Sorts of b2 = 0 .--> (the carrier of a1 \/ the carrier of b1)

proof end;

theorem Th29: :: MSSUBLAT:29

for A being Universal_Algebra
for a1, b1 being strict non-empty SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
the Sorts of a2 /\ the Sorts of b2 = 0 .--> (the carrier of a1 /\ the carrier of b1)

proof end;

theorem Th30: :: MSSUBLAT:30

for A being strict Universal_Algebra
for a1, b1 being strict non-empty SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
MSAlg (a1 "\/" b1) = a2 "\/" b2

proof end;

registration

let A be with_const_op Universal_Algebra;
cluster MSSign A -> all-with_const_op ;
coherence

proof end;

end;

theorem Th31: :: MSSUBLAT:31

for A being with_const_op Universal_Algebra
for a1, b1 being strict non-empty SubAlgebra of A
for a2, b2 being strict non-empty MSSubAlgebra of MSAlg A st a2 = MSAlg a1 & b2 = MSAlg b1 holds
MSAlg (a1 /\ b1) = a2 /\ b2

proof end;

registration

let A be quasi_total UAStr ;
cluster UAStr(# the carrier of A,the charact of A #) -> quasi_total ;
coherence

proof end;

end;

registration

let A be partial UAStr ;
cluster UAStr(# the carrier of A,the charact of A #) -> partial ;
coherence

proof end;

end;

registration

let A be non-empty UAStr ;
cluster UAStr(# the carrier of A,the charact of A #) -> non-empty ;
coherence

proof end;

end;

registration

let A be with_const_op Universal_Algebra;
cluster UAStr(# the carrier of A,the charact of A #) -> partial quasi_total non-empty with_const_op ;
coherence

proof end;

end;

theorem :: MSSUBLAT:32

for A being with_const_op Universal_Algebra holds UnSubAlLattice UAStr(# the carrier of A,the charact of A #), MSSubAlLattice (MSAlg UAStr(# the carrier of A,the charact of A #)) are_isomorphic

proof end;