:: MSSUBLAT semantic presentation

theorem Th1: :: MSSUBLAT:1

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

proof end;

theorem Th2: :: MSSUBLAT:2

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

proof end;

theorem Th3: :: MSSUBLAT:3

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

proof end;

theorem Th4: :: MSSUBLAT:4

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

proof end;

theorem Th5: :: MSSUBLAT:5

for b₁ being Nat
for b₂ being FinSequence of {0} holds
( b₂ = b₁ |-> 0 iff len b₂ = b₁ )

proof end;

theorem Th6: :: MSSUBLAT:6

for b₁ being Nat
for b₂ being FinSequence st b₂ = (*--> 0) . b₁ holds
len b₂ = b₁

proof end;

theorem Th7: :: MSSUBLAT:7

for b₁, b₂ being Universal_Algebra st b₁ is SubAlgebra of b₂ holds
MSSign b₁ = MSSign b₂

proof end;

registration

let c₁ be Universal_Algebra;
cluster the charact of a₁ -> Function-yielding ;
coherence

proof end;

end;

theorem Th8: :: MSSUBLAT:8

for b₁, b₂ being Universal_Algebra st b₁ is SubAlgebra of b₂ holds
for b₃ being MSSubset of (MSAlg b₂) st b₃ = the Sorts of (MSAlg b₁) holds
for b₄ being OperSymbol of (MSSign b₂)
for b₅ being OperSymbol of (MSSign b₁) st b₅ = b₄ holds
Den b₅,(MSAlg b₁) = (Den b₄,(MSAlg b₂)) | (Args b₅,(MSAlg b₁))

proof end;

theorem Th9: :: MSSUBLAT:9

for b₁, b₂ being Universal_Algebra st b₁ is SubAlgebra of b₂ holds
the Sorts of (MSAlg b₁) is MSSubset of (MSAlg b₂)

proof end;

theorem Th10: :: MSSUBLAT:10

for b₁, b₂ being Universal_Algebra st b₁ is SubAlgebra of b₂ holds
for b₃ being MSSubset of (MSAlg b₂) st b₃ = the Sorts of (MSAlg b₁) holds
b₃ is opers_closed

proof end;

theorem Th11: :: MSSUBLAT:11

for b₁, b₂ being Universal_Algebra st b₁ is SubAlgebra of b₂ holds
for b₃ being MSSubset of (MSAlg b₂) st b₃ = the Sorts of (MSAlg b₁) holds
the Charact of (MSAlg b₁) = Opers (MSAlg b₂),b₃

proof end;

theorem Th12: :: MSSUBLAT:12

for b₁, b₂ being Universal_Algebra st b₁ is SubAlgebra of b₂ holds
MSAlg b₁ is MSSubAlgebra of MSAlg b₂

proof end;

theorem Th13: :: MSSUBLAT:13

for b₁, b₂ being Universal_Algebra st MSAlg b₁ is MSSubAlgebra of MSAlg b₂ holds
the carrier of b₁ is Subset of b₂

proof end;

theorem Th14: :: MSSUBLAT:14

for b₁, b₂ being Universal_Algebra st MSAlg b₁ is MSSubAlgebra of MSAlg b₂ holds
for b₃ being non empty Subset of b₂ st b₃ = the carrier of b₁ holds
b₃ is opers_closed

proof end;

theorem Th15: :: MSSUBLAT:15

for b₁, b₂ being Universal_Algebra st MSAlg b₁ is MSSubAlgebra of MSAlg b₂ holds
for b₃ being non empty Subset of b₂ st b₃ = the carrier of b₁ holds
the charact of b₁ = Opers b₂,b₃

proof end;

theorem Th16: :: MSSUBLAT:16

for b₁, b₂ being Universal_Algebra st MSAlg b₁ is MSSubAlgebra of MSAlg b₂ holds
b₁ is SubAlgebra of b₂

proof end;

theorem Th17: :: MSSUBLAT:17

for b₁ being non empty trivial non void segmental ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being non-empty MSSubAlgebra of b₂ holds the carrier of (1-Alg b₃) is Subset of (1-Alg b₂)

proof end;

theorem Th18: :: MSSUBLAT:18

for b₁ being non empty trivial non void segmental ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being non-empty MSSubAlgebra of b₂
for b₄ being non empty Subset of (1-Alg b₂) st b₄ = the carrier of (1-Alg b₃) holds
b₄ is opers_closed

proof end;

theorem Th19: :: MSSUBLAT:19

proof end;

theorem Th20: :: MSSUBLAT:20

for b₁ being non empty trivial non void segmental ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being non-empty MSSubAlgebra of b₂ holds 1-Alg b₃ is SubAlgebra of 1-Alg b₂

proof end;

theorem Th21: :: MSSUBLAT:21

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being MSAlgebra of b₁ holds
( b₂ is MSSubAlgebra of b₃ iff b₂ is MSSubAlgebra of MSAlgebra(# the Sorts of b₃,the Charact of b₃ #) )

proof end;

theorem Th22: :: MSSUBLAT:22

for b₁, b₂ being Universal_Algebra holds
( signature b₁ = signature b₂ iff MSSign b₁ = MSSign b₂ )

proof end;

theorem Th23: :: MSSUBLAT:23

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

proof end;

theorem Th24: :: MSSUBLAT:24

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

proof end;

theorem Th25: :: MSSUBLAT:25

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

proof end;

theorem Th26: :: MSSUBLAT:26

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

proof end;

theorem Th27: :: MSSUBLAT:27

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

proof end;

theorem Th28: :: MSSUBLAT:28

for b₁ being Universal_Algebra
for b₂, b₃ being strict non-empty SubAlgebra of b₁
for b₄, b₅ being strict non-empty MSSubAlgebra of MSAlg b₁ st b₄ = MSAlg b₂ & b₅ = MSAlg b₃ holds
the Sorts of b₄ \/ the Sorts of b₅ = 0 .--> (the carrier of b₂ \/ the carrier of b₃)

proof end;

theorem Th29: :: MSSUBLAT:29

for b₁ being Universal_Algebra
for b₂, b₃ being strict non-empty SubAlgebra of b₁
for b₄, b₅ being strict non-empty MSSubAlgebra of MSAlg b₁ st b₄ = MSAlg b₂ & b₅ = MSAlg b₃ holds
the Sorts of b₄ /\ the Sorts of b₅ = 0 .--> (the carrier of b₂ /\ the carrier of b₃)

proof end;

theorem Th30: :: MSSUBLAT:30

for b₁ being strict Universal_Algebra
for b₂, b₃ being strict non-empty SubAlgebra of b₁
for b₄, b₅ being strict non-empty MSSubAlgebra of MSAlg b₁ st b₄ = MSAlg b₂ & b₅ = MSAlg b₃ holds
MSAlg (b₂ "\/" b₃) = b₄ "\/" b₅

proof end;

registration

let c₁ be with_const_op Universal_Algebra;
cluster MSSign a₁ -> all-with_const_op ;
coherence

proof end;

end;

theorem Th31: :: MSSUBLAT:31

for b₁ being with_const_op Universal_Algebra
for b₂, b₃ being strict non-empty SubAlgebra of b₁
for b₄, b₅ being strict non-empty MSSubAlgebra of MSAlg b₁ st b₄ = MSAlg b₂ & b₅ = MSAlg b₃ holds
MSAlg (b₂ /\ b₃) = b₄ /\ b₅

proof end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

let c₁ 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 Th32: :: MSSUBLAT:32

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

proof end;