:: Lattice of Substitutions
:: by Adam Grabowski
::
:: Received May 21, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users


begin

definition
let V, C be set ;
func SubstitutionSet (V,C) ->  Subset of (Fin (PFuncs (V,C))) equals :: SUBSTLAT:def 1
 {  A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) )  }  ;
coherence
  {  A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) )  }  is Subset of (Fin (PFuncs (V,C)))
proofend;
end;

:: deftheorem  defines SubstitutionSet SUBSTLAT:def_1_:_
 for V, C being set holds SubstitutionSet (V,C) =  {  A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) )  }  ;

Lm1:  for V, C, a, b being set st b in SubstitutionSet (V,C) & a in b holds
a is finite
proofend;

theorem Th1: :: SUBSTLAT:1
for V, C being set holds {} in SubstitutionSet (V,C)
proofend;

theorem Th2: :: SUBSTLAT:2
for V, C being set holds {{}} in SubstitutionSet (V,C)
proofend;

registration
let V, C be set ;
cluster SubstitutionSet (V,C) ->  non empty ;
coherence
 not SubstitutionSet (V,C) is empty by Th2;
end;

definition
let V, C be set ;
let A, B be Element of SubstitutionSet (V,C);
:: original:\/
redefine funcA \/ B ->  Element of Fin (PFuncs (V,C));
coherence
 A \/ B is Element of Fin (PFuncs (V,C))
proofend;
end;

registration
let V, C be set ;
cluster non empty for Element of SubstitutionSet (V,C);
existence
 not for b1 being Element of SubstitutionSet (V,C) holds b1 is empty
proofend;
end;

registration
let V, C be set ;
cluster  ->  finite for Element of SubstitutionSet (V,C);
coherence
 for b1 being Element of SubstitutionSet (V,C) holds b1 is finite ;
end;

definition
let V, C be set ;
let A be Element of Fin (PFuncs (V,C));
func mi A ->  Element of SubstitutionSet (V,C) equals :: SUBSTLAT:def 2
 {  t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) )  }  ;
coherence
  {  t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) )  }  is Element of SubstitutionSet (V,C)
proofend;
end;

:: deftheorem  defines mi SUBSTLAT:def_2_:_
 for V, C being set
for A being Element of Fin (PFuncs (V,C)) holds mi A =  {  t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) )  }  ;

registration
let V, C be set ;
cluster  ->  functional for Element of SubstitutionSet (V,C);
coherence
 for b1 being Element of SubstitutionSet (V,C) holds b1 is functional
proofend;
end;

definition
let V, C be set ;
let A, B be Element of Fin (PFuncs (V,C));
funcA ^ B ->  Element of Fin (PFuncs (V,C)) equals :: SUBSTLAT:def 3
 {  (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t )  }  ;
coherence
  {  (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t )  }  is Element of Fin (PFuncs (V,C))
proofend;
end;

:: deftheorem  defines ^ SUBSTLAT:def_3_:_
 for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds A ^ B =  {  (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t )  }  ;

theorem Th3: :: SUBSTLAT:3
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds A ^ B = B ^ A
proofend;

theorem Th4: :: SUBSTLAT:4
for V, C being set
for B, A being Element of Fin (PFuncs (V,C)) st B = {{}} holds
A ^ B = A
proofend;

theorem Th5: :: SUBSTLAT:5
for V, C being set
for B being Element of Fin (PFuncs (V,C))
for a, b being set st B in SubstitutionSet (V,C) & a in B & b in B & a c= b holds
a = b
proofend;

theorem Th6: :: SUBSTLAT:6
for V, C being set
for B being Element of Fin (PFuncs (V,C))
for a being set st a in mi B holds
( a in B & ( for b being set st b in B & b c= a holds
b = a ) )
proofend;

Lm2:  for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) st ( for a being set st a in A holds
a in B ) holds
A c= B
proofend;

registration
let V, C be set ;
clusterV1() Function-like finite for Element of PFuncs (V,C);
existence
 ex b1 being Element of PFuncs (V,C) st b1 is finite
proofend;
end;

theorem Th7: :: SUBSTLAT:7
for V, C being set
for B being Element of Fin (PFuncs (V,C))
for a being finite set st a in B & ( for b being finite set st b in B & b c= a holds
b = a ) holds
a in mi B
proofend;

theorem Th8: :: SUBSTLAT:8
for V, C being set
for A being Element of Fin (PFuncs (V,C)) holds mi A c= A
proofend;

theorem :: SUBSTLAT:9
for V, C being set
for A being Element of Fin (PFuncs (V,C)) st A = {} holds
mi A = {} by Th8, XBOOLE_1:3;

theorem Th10: :: SUBSTLAT:10
for V, C being set
for B being Element of Fin (PFuncs (V,C))
for b being finite set st b in B holds
ex c being set st
( c c= b & c in mi B )
proofend;

theorem Th11: :: SUBSTLAT:11
for V, C being set
for K being Element of SubstitutionSet (V,C) holds mi K = K
proofend;

theorem Th12: :: SUBSTLAT:12
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi (A \/ B) c= (mi A) \/ B
proofend;

theorem Th13: :: SUBSTLAT:13
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) \/ B) = mi (A \/ B)
proofend;

theorem Th14: :: SUBSTLAT:14
for V, C being set
for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds
A ^ D c= B ^ D
proofend;

theorem Th15: :: SUBSTLAT:15
for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for a being set st a in A ^ B holds
ex b, c being set st
( b in A & c in B & a = b \/ c )
proofend;

theorem :: SUBSTLAT:16
for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for b, c being Element of PFuncs (V,C) st b in A & c in B & b tolerates c holds
b \/ c in A ^ B ;

Lm3:  for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for a being finite set st a in A ^ B holds
ex b being finite set st
( b c= a & b in (mi A) ^ B )
proofend;

theorem Th17: :: SUBSTLAT:17
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ B) c= (mi A) ^ B
proofend;

theorem Th18: :: SUBSTLAT:18
for V, C being set
for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds
D ^ A c= D ^ B
proofend;

theorem Th19: :: SUBSTLAT:19
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) ^ B) = mi (A ^ B)
proofend;

theorem Th20: :: SUBSTLAT:20
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ (mi B)) = mi (A ^ B)
proofend;

theorem Th21: :: SUBSTLAT:21
for V, C being set
for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L ^ M) = (K ^ L) ^ M
proofend;

theorem Th22: :: SUBSTLAT:22
for V, C being set
for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M)
proofend;

Lm4:  for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for a being set st a in A ^ B holds
ex c being set st
( c in B & c c= a )
proofend;

Lm5:  for V, C being set
for K, L being Element of Fin (PFuncs (V,C)) holds mi ((K ^ L) \/ L) = mi L
proofend;

theorem Th23: :: SUBSTLAT:23
for V, C being set
for B being Element of Fin (PFuncs (V,C)) holds B c= B ^ B
proofend;

theorem Th24: :: SUBSTLAT:24
for V, C being set
for A being Element of Fin (PFuncs (V,C)) holds mi (A ^ A) = mi A
proofend;

theorem :: SUBSTLAT:25
for V, C being set
for K being Element of SubstitutionSet (V,C) holds mi (K ^ K) = K
proofend;

begin

definition
let V, C be set ;
func SubstLatt (V,C) ->  strict LattStr  means :Def4: :: SUBSTLAT:def 4
( the carrier of it = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of it . (A,B) = mi (A \/ B) & the L_meet of it . (A,B) = mi (A ^ B) ) ) );
existence
 ex b1 being strict LattStr st
( the carrier of b1 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of b1 . (A,B) = mi (A \/ B) & the L_meet of b1 . (A,B) = mi (A ^ B) ) ) )
proofend;
uniqueness
 for b1, b2 being strict LattStr st the carrier of b1 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of b1 . (A,B) = mi (A \/ B) & the L_meet of b1 . (A,B) = mi (A ^ B) ) ) & the carrier of b2 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of b2 . (A,B) = mi (A \/ B) & the L_meet of b2 . (A,B) = mi (A ^ B) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines SubstLatt SUBSTLAT:def_4_:_
 for V, C being set
for b3 being strict LattStr holds
( b3 = SubstLatt (V,C) iff ( the carrier of b3 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of b3 . (A,B) = mi (A \/ B) & the L_meet of b3 . (A,B) = mi (A ^ B) ) ) ) );

registration
let V, C be set ;
cluster SubstLatt (V,C) ->  non empty strict ;
coherence
 not SubstLatt (V,C) is empty
proofend;
end;

Lm6:  for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds a "\/" b = b "\/" a
proofend;

Lm7:  for V, C being set
for a, b, c being Element of (SubstLatt (V,C)) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proofend;

Lm8:  for V, C being set
for K, L being Element of SubstitutionSet (V,C) holds the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),L) = L
proofend;

Lm9:  for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds (a "/\" b) "\/" b = b
proofend;

Lm10:  for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds a "/\" b = b "/\" a
proofend;

Lm11:  for V, C being set
for a, b, c being Element of (SubstLatt (V,C)) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proofend;

Lm12:  for V, C being set
for K, L, M being Element of SubstitutionSet (V,C) holds the L_meet of (SubstLatt (V,C)) . (K,( the L_join of (SubstLatt (V,C)) . (L,M))) = the L_join of (SubstLatt (V,C)) . (( the L_meet of (SubstLatt (V,C)) . (K,L)),( the L_meet of (SubstLatt (V,C)) . (K,M)))
proofend;

Lm13:  for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds a "/\" (a "\/" b) = a
proofend;

registration
let V, C be set ;
cluster SubstLatt (V,C) ->  strict Lattice-like ;
coherence
 SubstLatt (V,C) is Lattice-like
proofend;
end;

registration
let V, C be set ;
cluster SubstLatt (V,C) ->  strict distributive bounded ;
coherence
 ( SubstLatt (V,C) is distributive & SubstLatt (V,C) is bounded )
proofend;
end;

theorem :: SUBSTLAT:26
for V, C being set holds Bottom (SubstLatt (V,C)) = {}
proofend;

theorem :: SUBSTLAT:27
for V, C being set holds Top (SubstLatt (V,C)) = {{}}
proofend;