:: by Andrzej Trybulec

::

:: Received December 13, 1994

:: Copyright (c) 1994-2012 Association of Mizar Users

begin

scheme :: MSAFREE1:sch 1

DTConstrUniq{ F_{1}() -> non empty DTConstrStr , F_{2}() -> non empty set , F_{3}( set ) -> Element of F_{2}(), F_{4}( set , set , set ) -> Element of F_{2}(), F_{5}() -> Function of (TS F_{1}()),F_{2}(), F_{6}() -> Function of (TS F_{1}()),F_{2}() } :

provided

DTConstrUniq{ F

provided

A1:
for t being Symbol of F_{1}() st t in Terminals F_{1}() holds

F_{5}() . (root-tree t) = F_{3}(t)
and

A2: for nt being Symbol of F_{1}()

for ts being Element of (TS F_{1}()) * st nt ==> roots ts holds

for x being Element of F_{2}() * st x = F_{5}() * ts holds

F_{5}() . (nt -tree ts) = F_{4}(nt,ts,x)
and

A3: for t being Symbol of F_{1}() st t in Terminals F_{1}() holds

F_{6}() . (root-tree t) = F_{3}(t)
and

A4: for nt being Symbol of F_{1}()

for ts being Element of (TS F_{1}()) * st nt ==> roots ts holds

for x being Element of F_{2}() * st x = F_{6}() * ts holds

F_{6}() . (nt -tree ts) = F_{4}(nt,ts,x)

F

A2: for nt being Symbol of F

for ts being Element of (TS F

for x being Element of F

F

A3: for t being Symbol of F

F

A4: for nt being Symbol of F

for ts being Element of (TS F

for x being Element of F

F

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 set 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))) * )

for X being ManySortedSet of the carrier of S

for o, b being set 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) ) ) ) )

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

registration

let I be set ;

coherence

for b_{1} being ManySortedSet of I st b_{1} is V3() holds

b_{1} is disjoint_valued

end;
coherence

for b

b

proof end;

registration
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;

ex b_{1} 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_{1} . x = (F . i) . x

uniqueness

for b_{1}, b_{2} 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_{1} . x = (F . i) . x ) & ( for i being Element of I

for x being set st x in X . i holds

b_{2} . x = (F . i) . x ) holds

b_{1} = b_{2};

end;
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 for i being Element of I

for x being set st x in X . i holds

it . x = (F . i) . x;

ex b

for i being Element of I

for x being set st x in X . i holds

b

proof end;

correctness uniqueness

for b

for x being set st x in X . i holds

b

for x being set st x in X . i holds

b

b

proof 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_{5} being Function of (Union X),(Union D) holds

( b_{5} = Flatten F iff for i being Element of I

for x being set st x in X . i holds

b_{5} . x = (F . i) . x );

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

( b

for x being set st x in X . i holds

b

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

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;

:: 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 );

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 ;

ex b_{1} being strict MSAlgebra over S st

for i being set st i in the carrier of S holds

the Sorts of b_{1} . i = {i}

for b_{1}, b_{2} being strict MSAlgebra over S st ( for i being set st i in the carrier of S holds

the Sorts of b_{1} . i = {i} ) & ( for i being set st i in the carrier of S holds

the Sorts of b_{2} . i = {i} ) holds

b_{1} = b_{2}

end;
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 for i being set st i in the carrier of S holds

the Sorts of it . i = {i};

ex b

for i being set st i in the carrier of S holds

the Sorts of b

proof end;

uniqueness for b

the Sorts of b

the Sorts of b

b

proof end;

:: deftheorem Def3 defines SingleAlg MSAFREE1:def 3 :

for S being non empty ManySortedSign

for b_{2} being strict MSAlgebra over S holds

( b_{2} = SingleAlg S iff for i being set st i in the carrier of S holds

the Sorts of b_{2} . i = {i} );

for S being non empty ManySortedSign

for b

( b

the Sorts of b

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 ;

existence

ex b_{1} being MSAlgebra over S st

( b_{1} is non-empty & b_{1} is disjoint_valued )

end;
existence

ex b

( b

proof end;

registration

let S be non empty ManySortedSign ;

coherence

( SingleAlg S is non-empty & SingleAlg S is disjoint_valued ) by Lm1;

end;
coherence

( SingleAlg S is non-empty & SingleAlg S is disjoint_valued ) by Lm1;

registration

let S be non empty ManySortedSign ;

let A be disjoint_valued MSAlgebra over S;

coherence

the Sorts of A is disjoint_valued by Def2;

end;
let A be disjoint_valued MSAlgebra over S;

coherence

the Sorts of A is disjoint_valued by Def2;

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

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;

coherence

FreeSort X is disjoint_valued

end;
let X be V2() ManySortedSet of the carrier of S;

coherence

FreeSort X is disjoint_valued

proof end;

scheme :: MSAFREE1:sch 2

FreeSortUniq{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> V2() ManySortedSet of the carrier of F_{1}(), F_{3}() -> V2() ManySortedSet of the carrier of F_{1}(), F_{4}( set ) -> Element of Union F_{3}(), F_{5}( set , set , set ) -> Element of Union F_{3}(), F_{6}() -> ManySortedFunction of FreeSort F_{2}(),F_{3}(), F_{7}() -> ManySortedFunction of FreeSort F_{2}(),F_{3}() } :

provided

FreeSortUniq{ F

provided

A1:
for o being OperSymbol of F_{1}()

for ts being Element of Args (o,(FreeMSA F_{2}()))

for x being Element of (Union F_{3}()) * st x = (Flatten F_{6}()) * ts holds

(F_{6}() . (the_result_sort_of o)) . ((Den (o,(FreeMSA F_{2}()))) . ts) = F_{5}(o,ts,x)
and

A2: for s being SortSymbol of F_{1}()

for y being set st y in FreeGen (s,F_{2}()) holds

(F_{6}() . s) . y = F_{4}(y)
and

A3: for o being OperSymbol of F_{1}()

for ts being Element of Args (o,(FreeMSA F_{2}()))

for x being Element of (Union F_{3}()) * st x = (Flatten F_{7}()) * ts holds

(F_{7}() . (the_result_sort_of o)) . ((Den (o,(FreeMSA F_{2}()))) . ts) = F_{5}(o,ts,x)
and

A4: for s being SortSymbol of F_{1}()

for y being set st y in FreeGen (s,F_{2}()) holds

(F_{7}() . s) . y = F_{4}(y)

for ts being Element of Args (o,(FreeMSA F

for x being Element of (Union F

(F

A2: for s being SortSymbol of F

for y being set st y in FreeGen (s,F

(F

A3: for o being OperSymbol of F

for ts being Element of Args (o,(FreeMSA F

for x being Element of (Union F

(F

A4: for s being SortSymbol of F

for y being set st y in FreeGen (s,F

(F

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V2() ManySortedSet of the carrier of S;

coherence

FreeMSA X is non-empty ;

end;
let X be V2() ManySortedSet of the carrier of S;

coherence

FreeMSA X is non-empty ;

registration

let S be non empty non void ManySortedSign ;

let o be OperSymbol of S;

let A be non-empty MSAlgebra over S;

coherence

not Args (o,A) is empty ;

coherence

not Result (o,A) is empty ;

end;
let o be OperSymbol of S;

let A be non-empty MSAlgebra over S;

coherence

not Args (o,A) is empty ;

coherence

not Result (o,A) is empty ;

registration

let S be non empty non void ManySortedSign ;

let X be V2() ManySortedSet of the carrier of S;

coherence

the Sorts of (FreeMSA X) is disjoint_valued

end;
let X be V2() ManySortedSet of the carrier of S;

coherence

the Sorts of (FreeMSA X) is disjoint_valued

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V2() ManySortedSet of the carrier of S;

coherence

FreeMSA X is disjoint_valued

end;
let X be V2() ManySortedSet of the carrier of S;

coherence

FreeMSA X is disjoint_valued

proof end;

scheme :: MSAFREE1:sch 3

ExtFreeGen{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> V2() ManySortedSet of the carrier of F_{1}(), F_{3}() -> non-empty MSAlgebra over F_{1}(), P_{1}[ set , set , set ], F_{4}() -> ManySortedFunction of (FreeMSA F_{2}()),F_{3}(), F_{5}() -> ManySortedFunction of (FreeMSA F_{2}()),F_{3}() } :

provided

ExtFreeGen{ F

provided

A1:
F_{4}() is_homomorphism FreeMSA F_{2}(),F_{3}()
and

A2: for s being SortSymbol of F_{1}()

for x, y being set st y in FreeGen (s,F_{2}()) holds

( (F_{4}() . s) . y = x iff P_{1}[s,x,y] )
and

A3: F_{5}() is_homomorphism FreeMSA F_{2}(),F_{3}()
and

A4: for s being SortSymbol of F_{1}()

for x, y being set st y in FreeGen (s,F_{2}()) holds

( (F_{5}() . s) . y = x iff P_{1}[s,x,y] )

A2: for s being SortSymbol of F

for x, y being set st y in FreeGen (s,F

( (F

A3: F

A4: for s being SortSymbol of F

for x, y being set st y in FreeGen (s,F

( (F

proof end;