:: MSAFREE1 semantic presentation

theorem Th1: :: MSAFREE1:1
for b1, b2 being Function st b2 in product b1 holds
rng b2 c= Union b1
proof end;

scheme :: MSAFREE1:sch 1
s1{ F1() -> non empty DTConstrStr , F2() -> non empty set , F3( set ) -> Element of F2(), F4( set , set , set ) -> Element of F2(), F5() -> Function of TS F1(),F2(), F6() -> Function of TS F1(),F2() } :
F5() = F6()
provided
E2: for b1 being Symbol of F1() st b1 in Terminals F1() holds
F5() . (root-tree b1) = F3(b1) and
E3: for b1 being Symbol of F1()
for b2 being FinSequence of TS F1() st b1 ==> roots b2 holds
for b3 being FinSequence of F2() st b3 = F5() * b2 holds
F5() . (b1 -tree b2) = F4(b1,b2,b3) and
E4: for b1 being Symbol of F1() st b1 in Terminals F1() holds
F6() . (root-tree b1) = F3(b1) and
E5: for b1 being Symbol of F1()
for b2 being FinSequence of TS F1() st b1 ==> roots b2 holds
for b3 being FinSequence of F2() st b3 = F6() * b2 holds
F6() . (b1 -tree b2) = F4(b1,b2,b3)
proof end;

theorem Th2: :: MSAFREE1:2
for b1 being non empty non void ManySortedSign
for b2 being ManySortedSet of the carrier of b1
for b3, b4 being set st [b3,b4] in REL b2 holds
( b3 in [:the OperSymbols of b1,{the carrier of b1}:] & b4 in ([:the OperSymbols of b1,{the carrier of b1}:] \/ (Union (coprod b2))) * )
proof end;

theorem Th3: :: MSAFREE1:3
for b1 being non empty non void ManySortedSign
for b2 being ManySortedSet of the carrier of b1
for b3 being OperSymbol of b1
for b4 being FinSequence st [[b3,the carrier of b1],b4] in REL b2 holds
( len b4 = len (the_arity_of b3) & ( for b5 being set st b5 in dom b4 holds
( ( b4 . b5 in [:the OperSymbols of b1,{the carrier of b1}:] implies for b6 being OperSymbol of b1 st [b6,the carrier of b1] = b4 . b5 holds
the_result_sort_of b6 = (the_arity_of b3) . b5 ) & ( b4 . b5 in Union (coprod b2) implies b4 . b5 in coprod ((the_arity_of b3) . b5),b2 ) ) ) )
proof end;

definition
let c1 be set ;
redefine mode FinSequence as FinSequence of c1 -> Element of a1 * ;
coherence
for b1 being FinSequence of c1 holds b1 is Element of c1 * by FINSEQ_1:def 11;
end;

registration
let c1 be non empty set ;
let c2 be V2 ManySortedSet of c1;
cluster rng a2 -> non empty with_non-empty_elements ;
coherence
( not rng c2 is empty & rng c2 is with_non-empty_elements ) by RELAT_1:64;
end;

registration
let c1 be non empty with_non-empty_elements set ;
cluster union a1 -> non empty ;
coherence
not union c1 is empty
proof end;
end;

registration
let c1 be set ;
cluster V3 -> disjoint_valued ManySortedSet of a1;
coherence
for b1 being ManySortedSet of c1 st b1 is empty-yielding holds
b1 is disjoint_valued
proof end;
end;

registration
let c1 be set ;
cluster disjoint_valued ManySortedSet of a1;
existence
ex b1 being ManySortedSet of c1 st b1 is disjoint_valued
proof end;
end;

definition
let c1 be non empty set ;
let c2 be disjoint_valued ManySortedSet of c1;
let c3 be V2 ManySortedSet of c1;
let c4 be ManySortedFunction of c2,c3;
func Flatten c4 -> Function of Union a2, Union a3 means :Def1: :: MSAFREE1:def 1
for b1 being Element of a1
for b2 being set st b2 in a2 . b1 holds
a5 . b2 = (a4 . b1) . b2;
existence
ex b1 being Function of Union c2, Union c3 st
for b2 being Element of c1
for b3 being set st b3 in c2 . b2 holds
b1 . b3 = (c4 . b2) . b3
proof end;
correctness
uniqueness
for b1, b2 being Function of Union c2, Union c3 st ( for b3 being Element of c1
for b4 being set st b4 in c2 . b3 holds
b1 . b4 = (c4 . b3) . b4 ) & ( for b3 being Element of c1
for b4 being set st b4 in c2 . b3 holds
b2 . b4 = (c4 . b3) . b4 ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def1 defines Flatten MSAFREE1:def 1 :
for b1 being non empty set
for b2 being disjoint_valued ManySortedSet of b1
for b3 being V2 ManySortedSet of b1
for b4 being ManySortedFunction of b2,b3
for b5 being Function of Union b2, Union b3 holds
( b5 = Flatten b4 iff for b6 being Element of b1
for b7 being set st b7 in b2 . b6 holds
b5 . b7 = (b4 . b6) . b7 );

theorem Th4: :: MSAFREE1:4
for b1 being non empty set
for b2 being disjoint_valued ManySortedSet of b1
for b3 being V2 ManySortedSet of b1
for b4, b5 being ManySortedFunction of b2,b3 st Flatten b4 = Flatten b5 holds
b4 = b5
proof end;

definition
let c1 be non empty ManySortedSign ;
let c2 be MSAlgebra of c1;
attr a2 is disjoint_valued means :Def2: :: MSAFREE1:def 2
the Sorts of a2 is disjoint_valued;
end;

:: deftheorem Def2 defines disjoint_valued MSAFREE1:def 2 :
for b1 being non empty ManySortedSign
for b2 being MSAlgebra of b1 holds
( b2 is disjoint_valued iff the Sorts of b2 is disjoint_valued );

definition
let c1 be non empty ManySortedSign ;
func SingleAlg c1 -> strict MSAlgebra of a1 means :Def3: :: MSAFREE1:def 3
for b1 being set st b1 in the carrier of a1 holds
the Sorts of a2 . b1 = {b1};
existence
ex b1 being strict MSAlgebra of c1 st
for b2 being set st b2 in the carrier of c1 holds
the Sorts of b1 . b2 = {b2}
proof end;
uniqueness
for b1, b2 being strict MSAlgebra of c1 st ( for b3 being set st b3 in the carrier of c1 holds
the Sorts of b1 . b3 = {b3} ) & ( for b3 being set st b3 in the carrier of c1 holds
the Sorts of b2 . b3 = {b3} ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines SingleAlg MSAFREE1:def 3 :
for b1 being non empty ManySortedSign
for b2 being strict MSAlgebra of b1 holds
( b2 = SingleAlg b1 iff for b3 being set st b3 in the carrier of b1 holds
the Sorts of b2 . b3 = {b3} );

Lemma7: for b1 being non empty ManySortedSign holds
( SingleAlg b1 is non-empty & SingleAlg b1 is disjoint_valued )
proof end;

registration
let c1 be non empty ManySortedSign ;
cluster non-empty disjoint_valued MSAlgebra of a1;
existence
ex b1 being MSAlgebra of c1 st
( b1 is non-empty & b1 is disjoint_valued )
proof end;
end;

registration
let c1 be non empty ManySortedSign ;
cluster SingleAlg a1 -> strict non-empty disjoint_valued ;
coherence
( SingleAlg c1 is non-empty & SingleAlg c1 is disjoint_valued ) by Lemma7;
end;

registration
let c1 be non empty ManySortedSign ;
let c2 be disjoint_valued MSAlgebra of c1;
cluster the Sorts of a2 -> disjoint_valued ;
coherence
the Sorts of c2 is disjoint_valued by Def2;
end;

theorem Th5: :: MSAFREE1:5
for b1 being non empty non void ManySortedSign
for b2 being OperSymbol of b1
for b3 being non-empty disjoint_valued MSAlgebra of b1
for b4 being non-empty MSAlgebra of b1
for b5 being ManySortedFunction of b3,b4
for b6 being Element of Args b2,b3 holds (Flatten b5) * b6 = b5 # b6
proof end;

registration
let c1 be non empty non void ManySortedSign ;
let c2 be V2 ManySortedSet of the carrier of c1;
cluster FreeSort a2 -> disjoint_valued ;
coherence
FreeSort c2 is disjoint_valued
proof end;
end;

scheme :: MSAFREE1:sch 2
s2{ F1() -> non empty non void ManySortedSign , F2() -> V2 ManySortedSet of the carrier of F1(), F3() -> V2 ManySortedSet of the carrier of F1(), F4( set ) -> Element of Union F3(), F5( set , set , set ) -> Element of Union F3(), F6() -> ManySortedFunction of FreeSort F2(),F3(), F7() -> ManySortedFunction of FreeSort F2(),F3() } :
F6() = F7()
provided
E9: for b1 being OperSymbol of F1()
for b2 being Element of Args b1,(FreeMSA F2())
for b3 being FinSequence of Union F3() st b3 = (Flatten F6()) * b2 holds
(F6() . (the_result_sort_of b1)) . ((Den b1,(FreeMSA F2())) . b2) = F5(b1,b2,b3) and
E10: for b1 being SortSymbol of F1()
for b2 being set st b2 in FreeGen b1,F2() holds
(F6() . b1) . b2 = F4(b2) and
E11: for b1 being OperSymbol of F1()
for b2 being Element of Args b1,(FreeMSA F2())
for b3 being FinSequence of Union F3() st b3 = (Flatten F7()) * b2 holds
(F7() . (the_result_sort_of b1)) . ((Den b1,(FreeMSA F2())) . b2) = F5(b1,b2,b3) and
E12: for b1 being SortSymbol of F1()
for b2 being set st b2 in FreeGen b1,F2() holds
(F7() . b1) . b2 = F4(b2)
proof end;

registration
let c1 be non empty non void ManySortedSign ;
let c2 be V2 ManySortedSet of the carrier of c1;
cluster FreeMSA a2 -> non-empty ;
coherence
FreeMSA c2 is non-empty ;
end;

registration
let c1 be non empty non void ManySortedSign ;
let c2 be OperSymbol of c1;
let c3 be non-empty MSAlgebra of c1;
cluster Args a2,a3 -> non empty ;
coherence
not Args c2,c3 is empty ;
cluster Result a2,a3 -> non empty ;
coherence
not Result c2,c3 is empty ;
end;

registration
let c1 be non empty non void ManySortedSign ;
let c2 be V2 ManySortedSet of the carrier of c1;
cluster the Sorts of (FreeMSA a2) -> disjoint_valued ;
coherence
the Sorts of (FreeMSA c2) is disjoint_valued
proof end;
end;

registration
let c1 be non empty non void ManySortedSign ;
let c2 be V2 ManySortedSet of the carrier of c1;
cluster FreeMSA a2 -> disjoint_valued ;
coherence
FreeMSA c2 is disjoint_valued
proof end;
end;

scheme :: MSAFREE1:sch 3
s3{ F1() -> non empty non void ManySortedSign , F2() -> V2 ManySortedSet of the carrier of F1(), F3() -> non-empty MSAlgebra of F1(), P1[ set , set , set ], F4() -> ManySortedFunction of (FreeMSA F2()),F3(), F5() -> ManySortedFunction of (FreeMSA F2()),F3() } :
F4() = F5()
provided
E9: F4() is_homomorphism FreeMSA F2(),F3() and
E10: for b1 being SortSymbol of F1()
for b2, b3 being set st b3 in FreeGen b1,F2() holds
( (F4() . b1) . b3 = b2 iff P1[b1,b2,b3] ) and
E11: F5() is_homomorphism FreeMSA F2(),F3() and
E12: for b1 being SortSymbol of F1()
for b2, b3 being set st b3 in FreeGen b1,F2() holds
( (F5() . b1) . b3 = b2 iff P1[b1,b2,b3] )
proof end;