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

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))
proof end;
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
proof end;

theorem Th1: :: SUBSTLAT:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set holds {} in SubstitutionSet V,C
proof end;

theorem Th2: :: SUBSTLAT:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set holds {{} } in SubstitutionSet V,C
proof end;

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 func A \/ B -> Element of Fin (PFuncs V,C);
coherence
A \/ B is Element of Fin (PFuncs V,C)
proof end;
end;

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

registration
let V, C be set ;
cluster -> finite Element of SubstitutionSet V,C;
coherence
for b1 being Element of SubstitutionSet V,C holds b1 is finite by FINSUB_1:def 5;
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
proof end;
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 -> finite functional Element of SubstitutionSet V,C;
coherence
for b1 being Element of SubstitutionSet V,C holds b1 is functional
proof end;
end;

definition
let V, C be set ;
let A, B be Element of Fin (PFuncs V,C);
func A ^ 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)
proof end;
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set
for A, B being Element of Fin (PFuncs V,C) holds A ^ B = B ^ A
proof end;

theorem Th4: :: SUBSTLAT:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set
for B, A being Element of Fin (PFuncs V,C) st B = {{} } holds
A ^ B = A
proof end;

theorem Th5: :: SUBSTLAT:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th6: :: SUBSTLAT:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

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
proof end;

registration
let V, C be set ;
cluster finite Element of PFuncs V,C;
existence
ex b1 being Element of PFuncs V,C st b1 is finite
proof end;
end;

theorem Th7: :: SUBSTLAT:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th8: :: SUBSTLAT:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set
for A being Element of Fin (PFuncs V,C) holds mi A c= A
proof end;

theorem :: SUBSTLAT:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set
for A being Element of Fin (PFuncs V,C) st A = {} holds
mi A = {}
proof end;

theorem Th10: :: SUBSTLAT:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th11: :: SUBSTLAT:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set
for K being Element of SubstitutionSet V,C holds mi K = K
proof end;

theorem Th12: :: SUBSTLAT:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set
for A, B being Element of Fin (PFuncs V,C) holds mi (A \/ B) c= (mi A) \/ B
proof end;

theorem Th13: :: SUBSTLAT:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set
for A, B being Element of Fin (PFuncs V,C) holds mi ((mi A) \/ B) = mi (A \/ B)
proof end;

theorem Th14: :: SUBSTLAT:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th15: :: SUBSTLAT:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: SUBSTLAT:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th17: :: SUBSTLAT:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set
for A, B being Element of Fin (PFuncs V,C) holds mi (A ^ B) c= (mi A) ^ B
proof end;

theorem Th18: :: SUBSTLAT:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th19: :: SUBSTLAT:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set
for A, B being Element of Fin (PFuncs V,C) holds mi ((mi A) ^ B) = mi (A ^ B)
proof end;

theorem Th20: :: SUBSTLAT:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set
for A, B being Element of Fin (PFuncs V,C) holds mi (A ^ (mi B)) = mi (A ^ B)
proof end;

theorem Th21: :: SUBSTLAT:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set
for K, L, M being Element of Fin (PFuncs V,C) holds K ^ (L ^ M) = (K ^ L) ^ M
proof end;

theorem Th22: :: SUBSTLAT:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set
for K, L, M being Element of Fin (PFuncs V,C) holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M)
proof end;

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 )
proof end;

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

theorem Th23: :: SUBSTLAT:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set
for B being Element of Fin (PFuncs V,C) holds B c= B ^ B
proof end;

theorem Th24: :: SUBSTLAT:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set
for A being Element of Fin (PFuncs V,C) holds mi (A ^ A) = mi A
proof end;

theorem :: SUBSTLAT:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set
for K being Element of SubstitutionSet V,C holds mi (K ^ K) = K
proof end;

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) ) ) )
proof end;
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
proof end;
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
proof end;
end;

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

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

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
proof end;

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

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

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

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)
proof end;

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

registration
let V, C be set ;
cluster SubstLatt V,C -> non empty strict Lattice-like ;
coherence
SubstLatt V,C is Lattice-like
proof end;
end;

registration
let V, C be set ;
cluster SubstLatt V,C -> non empty strict Lattice-like distributive bounded ;
coherence
( SubstLatt V,C is distributive & SubstLatt V,C is bounded )
proof end;
end;

theorem :: SUBSTLAT:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set holds Bottom (SubstLatt V,C) = {}
proof end;

theorem :: SUBSTLAT:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, C being set holds Top (SubstLatt V,C) = {{} }
proof end;