:: SUBSTLAT semantic presentation

definition

let c₁, c₂ be set ;
func SubstitutionSet c₁,c₂ -> Subset of (Fin (PFuncs a₁,a₂)) equals :: SUBSTLAT:def 1
{ b₁ where B is Element of Fin (PFuncs a₁,a₂) : ( ( for b₁ being set st b₂ in b₁ holds
b₂ is finite ) & ( for b₁, b₂ being Element of PFuncs a₁,a₂ st b₂ in b₁ & b₃ in b₁ & b₂ c= b₃ holds
b₂ = b₃ ) ) } ;
coherence

proof end;

end;

:: deftheorem Def1 defines SubstitutionSet SUBSTLAT:def 1 :

Lemma1: for b₁, b₂, b₃, b₄ being set st b₄ in SubstitutionSet b₁,b₂ & b₃ in b₄ holds
b₃ is finite

proof end;

theorem Th1: :: SUBSTLAT:1

for b₁, b₂ being set holds {} in SubstitutionSet b₁,b₂

proof end;

theorem Th2: :: SUBSTLAT:2

for b₁, b₂ being set holds {{} } in SubstitutionSet b₁,b₂

proof end;

registration

let c₁, c₂ be set ;
cluster SubstitutionSet a₁,a₂ -> non empty ;
coherence by Th2;

end;

definition

let c₁, c₂ be set ;
let c₃, c₄ be Element of SubstitutionSet c₁,c₂;
redefine func \/ as c₃ \/ c₄ -> Element of Fin (PFuncs a₁,a₂);
coherence

proof end;

end;

registration

let c₁, c₂ be set ;
cluster non empty Element of SubstitutionSet a₁,a₂;
existence

proof end;

end;

registration

let c₁, c₂ be set ;
cluster -> finite Element of SubstitutionSet a₁,a₂;
coherence by FINSUB_1:def 5;

end;

definition

let c₁, c₂ be set ;
let c₃ be Element of Fin (PFuncs c₁,c₂);
func mi c₃ -> Element of SubstitutionSet a₁,a₂ equals :: SUBSTLAT:def 2
{ b₁ where B is Element of PFuncs a₁,a₂ : ( b₁ is finite & ( for b₁ being Element of PFuncs a₁,a₂ holds
( ( b₂ in a₃ & b₂ c= b₁ ) iff b₂ = b₁ ) ) ) } ;
coherence

proof end;

end;

:: deftheorem Def2 defines mi SUBSTLAT:def 2 :

registration

let c₁, c₂ be set ;
cluster -> finite functional Element of SubstitutionSet a₁,a₂;
coherence

proof end;

end;

definition

let c₁, c₂ be set ;
let c₃, c₄ be Element of Fin (PFuncs c₁,c₂);
func c₃ ^ c₄ -> Element of Fin (PFuncs a₁,a₂) equals :: SUBSTLAT:def 3
{ (b₁ \/ b₂) where B is Element of PFuncs a₁,a₂, B is Element of PFuncs a₁,a₂ : ( b₁ in a₃ & b₂ in a₄ & b₁ tolerates b₂ ) } ;
coherence

proof end;

end;

:: deftheorem Def3 defines ^ SUBSTLAT:def 3 :

theorem Th3: :: SUBSTLAT:3

for b₁, b₂ being set
for b₃, b₄ being Element of Fin (PFuncs b₁,b₂) holds b₃ ^ b₄ = b₄ ^ b₃

proof end;

theorem Th4: :: SUBSTLAT:4

for b₁, b₂ being set
for b₃, b₄ being Element of Fin (PFuncs b₁,b₂) st b₃ = {{} } holds
b₄ ^ b₃ = b₄

proof end;

theorem Th5: :: SUBSTLAT:5

for b₁, b₂ being set
for b₃ being Element of Fin (PFuncs b₁,b₂)
for b₄, b₅ being set st b₃ in SubstitutionSet b₁,b₂ & b₄ in b₃ & b₅ in b₃ & b₄ c= b₅ holds
b₄ = b₅

proof end;

theorem Th6: :: SUBSTLAT:6

for b₁, b₂ being set
for b₃ being Element of Fin (PFuncs b₁,b₂)
for b₄ being set st b₄ in mi b₃ holds
( b₄ in b₃ & ( for b₅ being set st b₅ in b₃ & b₅ c= b₄ holds
b₅ = b₄ ) )

proof end;

Lemma8: for b₁, b₂ being set
for b₃, b₄ being Element of Fin (PFuncs b₁,b₂) st ( for b₅ being set st b₅ in b₃ holds
b₅ in b₄ ) holds
b₃ c= b₄

proof end;

registration

let c₁, c₂ be set ;
cluster finite Element of PFuncs a₁,a₂;
existence

proof end;

end;

theorem Th7: :: SUBSTLAT:7

for b₁, b₂ being set
for b₃ being Element of Fin (PFuncs b₁,b₂)
for b₄ being finite set st b₄ in b₃ & ( for b₅ being finite set st b₅ in b₃ & b₅ c= b₄ holds
b₅ = b₄ ) holds
b₄ in mi b₃

proof end;

theorem Th8: :: SUBSTLAT:8

for b₁, b₂ being set
for b₃ being Element of Fin (PFuncs b₁,b₂) holds mi b₃ c= b₃

proof end;

theorem Th9: :: SUBSTLAT:9

for b₁, b₂ being set
for b₃ being Element of Fin (PFuncs b₁,b₂) st b₃ = {} holds
mi b₃ = {}

proof end;

theorem Th10: :: SUBSTLAT:10

for b₁, b₂ being set
for b₃ being Element of Fin (PFuncs b₁,b₂)
for b₄ being finite set st b₄ in b₃ holds
ex b₅ being set st
( b₅ c= b₄ & b₅ in mi b₃ )

proof end;

theorem Th11: :: SUBSTLAT:11

for b₁, b₂ being set
for b₃ being Element of SubstitutionSet b₁,b₂ holds mi b₃ = b₃

proof end;

theorem Th12: :: SUBSTLAT:12

for b₁, b₂ being set
for b₃, b₄ being Element of Fin (PFuncs b₁,b₂) holds mi (b₃ \/ b₄) c= (mi b₃) \/ b₄

proof end;

theorem Th13: :: SUBSTLAT:13

for b₁, b₂ being set
for b₃, b₄ being Element of Fin (PFuncs b₁,b₂) holds mi ((mi b₃) \/ b₄) = mi (b₃ \/ b₄)

proof end;

theorem Th14: :: SUBSTLAT:14

for b₁, b₂ being set
for b₃, b₄, b₅ being Element of Fin (PFuncs b₁,b₂) st b₃ c= b₄ holds
b₃ ^ b₅ c= b₄ ^ b₅

proof end;

theorem Th15: :: SUBSTLAT:15

for b₁, b₂ being set
for b₃, b₄ being Element of Fin (PFuncs b₁,b₂)
for b₅ being set st b₅ in b₃ ^ b₄ holds
ex b₆, b₇ being set st
( b₆ in b₃ & b₇ in b₄ & b₅ = b₆ \/ b₇ )

proof end;

theorem Th16: :: SUBSTLAT:16

for b₁, b₂ being set
for b₃, b₄ being Element of Fin (PFuncs b₁,b₂)
for b₅, b₆ being Element of PFuncs b₁,b₂ st b₅ in b₃ & b₆ in b₄ & b₅ tolerates b₆ holds
b₅ \/ b₆ in b₃ ^ b₄ ;

Lemma17: for b₁, b₂ being set
for b₃, b₄ being Element of Fin (PFuncs b₁,b₂)
for b₅ being finite set st b₅ in b₃ ^ b₄ holds
ex b₆ being finite set st
( b₆ c= b₅ & b₆ in (mi b₃) ^ b₄ )

proof end;

theorem Th17: :: SUBSTLAT:17

for b₁, b₂ being set
for b₃, b₄ being Element of Fin (PFuncs b₁,b₂) holds mi (b₃ ^ b₄) c= (mi b₃) ^ b₄

proof end;

theorem Th18: :: SUBSTLAT:18

for b₁, b₂ being set
for b₃, b₄, b₅ being Element of Fin (PFuncs b₁,b₂) st b₃ c= b₄ holds
b₅ ^ b₃ c= b₅ ^ b₄

proof end;

theorem Th19: :: SUBSTLAT:19

for b₁, b₂ being set
for b₃, b₄ being Element of Fin (PFuncs b₁,b₂) holds mi ((mi b₃) ^ b₄) = mi (b₃ ^ b₄)

proof end;

theorem Th20: :: SUBSTLAT:20

for b₁, b₂ being set
for b₃, b₄ being Element of Fin (PFuncs b₁,b₂) holds mi (b₃ ^ (mi b₄)) = mi (b₃ ^ b₄)

proof end;

theorem Th21: :: SUBSTLAT:21

for b₁, b₂ being set
for b₃, b₄, b₅ being Element of Fin (PFuncs b₁,b₂) holds b₃ ^ (b₄ ^ b₅) = (b₃ ^ b₄) ^ b₅

proof end;

theorem Th22: :: SUBSTLAT:22

for b₁, b₂ being set
for b₃, b₄, b₅ being Element of Fin (PFuncs b₁,b₂) holds b₃ ^ (b₄ \/ b₅) = (b₃ ^ b₄) \/ (b₃ ^ b₅)

proof end;

Lemma24: for b₁, b₂ being set
for b₃, b₄ being Element of Fin (PFuncs b₁,b₂)
for b₅ being set st b₅ in b₃ ^ b₄ holds
ex b₆ being set st
( b₆ in b₄ & b₆ c= b₅ )

proof end;

Lemma25: for b₁, b₂ being set
for b₃, b₄ being Element of Fin (PFuncs b₁,b₂) holds mi ((b₃ ^ b₄) \/ b₄) = mi b₄

proof end;

theorem Th23: :: SUBSTLAT:23

for b₁, b₂ being set
for b₃ being Element of Fin (PFuncs b₁,b₂) holds b₃ c= b₃ ^ b₃

proof end;

theorem Th24: :: SUBSTLAT:24

for b₁, b₂ being set
for b₃ being Element of Fin (PFuncs b₁,b₂) holds mi (b₃ ^ b₃) = mi b₃

proof end;

theorem Th25: :: SUBSTLAT:25

for b₁, b₂ being set
for b₃ being Element of SubstitutionSet b₁,b₂ holds mi (b₃ ^ b₃) = b₃

proof end;

definition

let c₁, c₂ be set ;
func SubstLatt c₁,c₂ -> strict LattStr means :Def4: :: SUBSTLAT:def 4
( the carrier of a₃ = SubstitutionSet a₁,a₂ & ( for b₁, b₂ being Element of SubstitutionSet a₁,a₂ holds
( the L_join of a₃ . b₁,b₂ = mi (b₁ \/ b₂) & the L_meet of a₃ . b₁,b₂ = mi (b₁ ^ b₂) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines SubstLatt SUBSTLAT:def 4 :

registration

let c₁, c₂ be set ;
cluster SubstLatt a₁,a₂ -> non empty strict ;
coherence

proof end;

end;

Lemma29: for b₁, b₂ being set
for b₃, b₄ being Element of (SubstLatt b₁,b₂) holds b₃ "\/" b₄ = b₄ "\/" b₃

proof end;

Lemma30: for b₁, b₂ being set
for b₃, b₄, b₅ being Element of (SubstLatt b₁,b₂) holds b₃ "\/" (b₄ "\/" b₅) = (b₃ "\/" b₄) "\/" b₅

proof end;

Lemma31: for b₁, b₂ being set
for b₃, b₄ being Element of SubstitutionSet b₁,b₂ holds the L_join of (SubstLatt b₁,b₂) . (the L_meet of (SubstLatt b₁,b₂) . b₃,b₄),b₄ = b₄

proof end;

Lemma32: for b₁, b₂ being set
for b₃, b₄ being Element of (SubstLatt b₁,b₂) holds (b₃ "/\" b₄) "\/" b₄ = b₄

proof end;

Lemma33: for b₁, b₂ being set
for b₃, b₄ being Element of (SubstLatt b₁,b₂) holds b₃ "/\" b₄ = b₄ "/\" b₃

proof end;

Lemma34: for b₁, b₂ being set
for b₃, b₄, b₅ being Element of (SubstLatt b₁,b₂) holds b₃ "/\" (b₄ "/\" b₅) = (b₃ "/\" b₄) "/\" b₅

proof end;

Lemma35: for b₁, b₂ being set
for b₃, b₄, b₅ being Element of SubstitutionSet b₁,b₂ holds the L_meet of (SubstLatt b₁,b₂) . b₃,(the L_join of (SubstLatt b₁,b₂) . b₄,b₅) = the L_join of (SubstLatt b₁,b₂) . (the L_meet of (SubstLatt b₁,b₂) . b₃,b₄),(the L_meet of (SubstLatt b₁,b₂) . b₃,b₅)

proof end;

Lemma36: for b₁, b₂ being set
for b₃, b₄ being Element of (SubstLatt b₁,b₂) holds b₃ "/\" (b₃ "\/" b₄) = b₃

proof end;

registration

let c₁, c₂ be set ;
cluster SubstLatt a₁,a₂ -> non empty strict Lattice-like ;
coherence

proof end;

end;

registration

let c₁, c₂ be set ;
cluster SubstLatt a₁,a₂ -> non empty strict Lattice-like distributive bounded ;
coherence

proof end;

end;

theorem Th26: :: SUBSTLAT:26

for b₁, b₂ being set holds Bottom (SubstLatt b₁,b₂) = {}

proof end;

theorem Th27: :: SUBSTLAT:27

for b₁, b₂ being set holds Top (SubstLatt b₁,b₂) = {{} }

proof end;