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

theorem Th1: :: MSAFREE1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being Function st g in product f holds
rng g c= Union f
proof end;

scheme :: MSAFREE1:sch 1
DTConstrUniq{ 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
A1: for t being Symbol of F1() st t in Terminals F1() holds
F5() . (root-tree t) = F3(t) and
A2: for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
for x being FinSequence of F2() st x = F5() * ts holds
F5() . (nt -tree ts) = F4(nt,ts,x) and
A3: for t being Symbol of F1() st t in Terminals F1() holds
F6() . (root-tree t) = F3(t) and
A4: for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
for x being FinSequence of F2() st x = F6() * ts holds
F6() . (nt -tree ts) = F4(nt,ts,x)
proof end;

theorem Th2: :: MSAFREE1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S
for o, b being set st [o,b] in REL X holds
( o in [:the OperSymbols of S,{the carrier of S}:] & b in ([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * )
proof end;

theorem :: MSAFREE1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S
for o being OperSymbol of S
for b being FinSequence st [[o,the carrier of S],b] in REL X holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [:the OperSymbols of S,{the carrier of S}:] implies for o1 being OperSymbol of S st [o1,the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod ((the_arity_of o) . x),X ) ) ) )
proof end;

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

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

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

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

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

definition
let I be non empty set ;
let X be disjoint_valued ManySortedSet of I;
let D be V2 ManySortedSet of I;
let F be ManySortedFunction of X,D;
func Flatten F -> Function of Union X, Union D means :Def1: :: MSAFREE1:def 1
for i being Element of I
for x being set st x in X . i holds
it . x = (F . i) . x;
existence
ex b1 being Function of Union X, Union D st
for i being Element of I
for x being set st x in X . i holds
b1 . x = (F . i) . x
proof end;
correctness
uniqueness
for b1, b2 being Function of Union X, Union D st ( for i being Element of I
for x being set st x in X . i holds
b1 . x = (F . i) . x ) & ( for i being Element of I
for x being set st x in X . i holds
b2 . x = (F . i) . x ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def1 defines Flatten MSAFREE1:def 1 :
for I being non empty set
for X being disjoint_valued ManySortedSet of I
for D being V2 ManySortedSet of I
for F being ManySortedFunction of X,D
for b5 being Function of Union X, Union D holds
( b5 = Flatten F iff for i being Element of I
for x being set st x in X . i holds
b5 . x = (F . i) . x );

theorem Th4: :: MSAFREE1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for X being disjoint_valued ManySortedSet of I
for D being V2 ManySortedSet of I
for F1, F2 being ManySortedFunction of X,D st Flatten F1 = Flatten F2 holds
F1 = F2
proof end;

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

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

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

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

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

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

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

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

theorem Th5: :: MSAFREE1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A1 being non-empty disjoint_valued MSAlgebra of S
for A2 being non-empty MSAlgebra of S
for f being ManySortedFunction of A1,A2
for a being Element of Args o,A1 holds (Flatten f) * a = f # a
proof end;

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

scheme :: MSAFREE1:sch 2
FreeSortUniq{ 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
A1: for o being OperSymbol of F1()
for ts being Element of Args o,(FreeMSA F2())
for x being FinSequence of Union F3() st x = (Flatten F6()) * ts holds
(F6() . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts) = F5(o,ts,x) and
A2: for s being SortSymbol of F1()
for y being set st y in FreeGen s,F2() holds
(F6() . s) . y = F4(y) and
A3: for o being OperSymbol of F1()
for ts being Element of Args o,(FreeMSA F2())
for x being FinSequence of Union F3() st x = (Flatten F7()) * ts holds
(F7() . (the_result_sort_of o)) . ((Den o,(FreeMSA F2())) . ts) = F5(o,ts,x) and
A4: for s being SortSymbol of F1()
for y being set st y in FreeGen s,F2() holds
(F7() . s) . y = F4(y)
proof end;

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

registration
let S be non empty non void ManySortedSign ;
let o be OperSymbol of S;
let A be non-empty MSAlgebra of S;
cluster Args o,A -> non empty ;
coherence
not Args o,A is empty ;
cluster Result o,A -> non empty ;
coherence
not Result o,A is empty ;
end;

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

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

scheme :: MSAFREE1:sch 3
ExtFreeGen{ 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
A1: F4() is_homomorphism FreeMSA F2(),F3() and
A2: for s being SortSymbol of F1()
for x, y being set st y in FreeGen s,F2() holds
( (F4() . s) . y = x iff P1[s,x,y] ) and
A3: F5() is_homomorphism FreeMSA F2(),F3() and
A4: for s being SortSymbol of F1()
for x, y being set st y in FreeGen s,F2() holds
( (F5() . s) . y = x iff P1[s,x,y] )
proof end;