:: A Scheme for Extensions of Homomorphisms of Manysorted Algebras
:: by Andrzej Trybulec
::
:: Received December 13, 1994
:: Copyright (c) 1994-2021 Association of Mizar Users

theorem Th1: :: MSAFREE1:1

for f, g being Function st g in product f holds
rng g c= Union f

proof end;

scheme :: MSAFREE1:sch 1
DTConstrUniq{ F₁() -> non empty DTConstrStr , F₂() -> non empty set , F₃( set ) -> Element of F₂(), F₄( set , set , set ) -> Element of F₂(), F₅() -> Function of (TS F₁()),F₂(), F₆() -> Function of (TS F₁()),F₂() } :

F₅() = F₆()

provided

A1: for t being Symbol of F₁() st t in Terminals F₁() holds
F₅() . (root-tree t) = F₃(t) and
A2: for nt being Symbol of F₁()
for ts being Element of (TS F₁()) * st nt ==> roots ts holds
for x being Element of F₂() * st x = F₅() * ts holds
F₅() . (nt -tree ts) = F₄(nt,ts,x) and
A3: for t being Symbol of F₁() st t in Terminals F₁() holds
F₆() . (root-tree t) = F₃(t) and
A4: for nt being Symbol of F₁()
for ts being Element of (TS F₁()) * st nt ==> roots ts holds
for x being Element of F₂() * st x = F₆() * ts holds
F₆() . (nt -tree ts) = F₄(nt,ts,x)

proof end;

theorem Th2: :: MSAFREE1:2

for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S
for o, b being object st [o,b] in REL X holds
( o in [: the carrier' of S,{ the carrier of S}:] & b in ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * )

proof end;

theorem :: MSAFREE1:3

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 carrier' 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;

registration

let I be non empty set ;
let M be ManySortedSet of I;

cluster rng M -> non empty ;

coherence
not rng M is empty ;

end;

registration

let I be set ;

cluster Relation-like V3() I -defined Function-like total -> disjoint_valued for set ;

coherence
for b₁ being ManySortedSet of I st b₁ is V3() holds
b₁ is disjoint_valued

proof end;

end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total disjoint_valued for set ;

existence
ex b₁ being ManySortedSet of I st b₁ 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 b₁ being Function of (Union X),(Union D) st
for i being Element of I
for x being set st x in X . i holds
b₁ . x = (F . i) . x

proof end;

correctness
uniqueness
for b₁, b₂ being Function of (Union X),(Union D) st ( for i being Element of I
for x being set st x in X . i holds
b₁ . x = (F . i) . x ) & ( for i being Element of I
for x being set st x in X . i holds
b₂ . x = (F . i) . x ) holds
b₁ = b₂;

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 b₅ being Function of (Union X),(Union D) holds
( b₅ = Flatten F iff for i being Element of I
for x being set st x in X . i holds
b₅ . x = (F . i) . x );

theorem Th4: :: MSAFREE1:4

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 over 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 over 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 over 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 b₁ being strict MSAlgebra over S st
for i being set st i in the carrier of S holds
the Sorts of b₁ . i = {i}

proof end;

uniqueness
for b₁, b₂ being strict MSAlgebra over S st ( for i being set st i in the carrier of S holds
the Sorts of b₁ . i = {i} ) & ( for i being set st i in the carrier of S holds
the Sorts of b₂ . i = {i} ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines SingleAlg MSAFREE1:def 3 :
for S being non empty ManySortedSign
for b₂ being strict MSAlgebra over S holds
( b₂ = SingleAlg S iff for i being set st i in the carrier of S holds
the Sorts of b₂ . 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 for MSAlgebra over S;

existence
ex b₁ being MSAlgebra over S st
( b₁ is non-empty & b₁ 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 over S;

cluster the Sorts of A -> disjoint_valued ;

coherence
the Sorts of A is disjoint_valued by Def2;

end;

theorem Th5: :: MSAFREE1:5

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A1 being non-empty disjoint_valued MSAlgebra over S
for A2 being non-empty MSAlgebra over 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{ F₁() -> non empty non void ManySortedSign , F₂() -> V2() ManySortedSet of the carrier of F₁(), F₃() -> V2() ManySortedSet of the carrier of F₁(), F₄( set ) -> Element of Union F₃(), F₅( object , object , object ) -> Element of Union F₃(), F₆() -> ManySortedFunction of FreeSort F₂(),F₃(), F₇() -> ManySortedFunction of FreeSort F₂(),F₃() } :

F₆() = F₇()

provided

A1: for o being OperSymbol of F₁()
for ts being Element of Args (o,(FreeMSA F₂()))
for x being Element of (Union F₃()) * st x = (Flatten F₆()) * ts holds
(F₆() . (the_result_sort_of o)) . ((Den (o,(FreeMSA F₂()))) . ts) = F₅(o,ts,x) and
A2: for s being SortSymbol of F₁()
for y being set st y in FreeGen (s,F₂()) holds
(F₆() . s) . y = F₄(y) and
A3: for o being OperSymbol of F₁()
for ts being Element of Args (o,(FreeMSA F₂()))
for x being Element of (Union F₃()) * st x = (Flatten F₇()) * ts holds
(F₇() . (the_result_sort_of o)) . ((Den (o,(FreeMSA F₂()))) . ts) = F₅(o,ts,x) and
A4: for s being SortSymbol of F₁()
for y being set st y in FreeGen (s,F₂()) holds
(F₇() . s) . y = F₄(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 over 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 ;

end;

scheme :: MSAFREE1:sch 3
ExtFreeGen{ F₁() -> non empty non void ManySortedSign , F₂() -> V2() ManySortedSet of the carrier of F₁(), F₃() -> non-empty MSAlgebra over F₁(), P₁[ object , object , object ], F₄() -> ManySortedFunction of (FreeMSA F₂()),F₃(), F₅() -> ManySortedFunction of (FreeMSA F₂()),F₃() } :

F₄() = F₅()

provided

A1: F₄() is_homomorphism FreeMSA F₂(),F₃() and
A2: for s being SortSymbol of F₁()
for x, y being set st y in FreeGen (s,F₂()) holds
( (F₄() . s) . y = x iff P₁[s,x,y] ) and
A3: F₅() is_homomorphism FreeMSA F₂(),F₃() and
A4: for s being SortSymbol of F₁()
for x, y being set st y in FreeGen (s,F₂()) holds
( (F₅() . s) . y = x iff P₁[s,x,y] )

proof end;