:: INSTALG1 semantic presentation
begin
theorem Th1: :: INSTALG1:1
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for V being V16() ManySortedSet of the carrier of S
for x being set holds
( x is ArgumentSeq of Sym (o,V) iff x is Element of Args (o,(FreeMSA V)) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S
for V being V16() ManySortedSet of the carrier of S
for x being set holds
( x is ArgumentSeq of Sym (o,V) iff x is Element of Args (o,(FreeMSA V)) )
let o be OperSymbol of S; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for x being set holds
( x is ArgumentSeq of Sym (o,V) iff x is Element of Args (o,(FreeMSA V)) )
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for x being set holds
( x is ArgumentSeq of Sym (o,V) iff x is Element of Args (o,(FreeMSA V)) )
let x be set ; ::_thesis: ( x is ArgumentSeq of Sym (o,V) iff x is Element of Args (o,(FreeMSA V)) )
A1: TS (DTConMSA V) = S -Terms V by MSATERM:def_1;
A2: FreeMSA V = MSAlgebra(# (FreeSort V),(FreeOper V) #) by MSAFREE:def_14;
hereby ::_thesis: ( x is Element of Args (o,(FreeMSA V)) implies x is ArgumentSeq of Sym (o,V) )
assume x is ArgumentSeq of Sym (o,V) ; ::_thesis: x is Element of Args (o,(FreeMSA V))
then reconsider p = x as ArgumentSeq of Sym (o,V) ;
reconsider p = p as FinSequence of TS (DTConMSA V) by MSATERM:def_1;
Sym (o,V) ==> roots p by MSATERM:21;
hence x is Element of Args (o,(FreeMSA V)) by A2, MSAFREE:10; ::_thesis: verum
end;
assume x is Element of Args (o,(FreeMSA V)) ; ::_thesis: x is ArgumentSeq of Sym (o,V)
then reconsider x = x as Element of Args (o,(FreeMSA V)) ;
rng x c= TS (DTConMSA V)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng x or y in TS (DTConMSA V) )
assume y in rng x ; ::_thesis: y in TS (DTConMSA V)
then consider z being set such that
A3: z in dom x and
A4: y = x . z by FUNCT_1:def_3;
reconsider z = z as Element of NAT by A3;
A5: (FreeSort V) . ((the_arity_of o) /. z) = FreeSort (V,((the_arity_of o) /. z)) by MSAFREE:def_11;
dom x = dom (the_arity_of o) by MSUALG_6:2;
then y in (FreeSort V) . ((the_arity_of o) /. z) by A2, A3, A4, MSUALG_6:2;
hence y in TS (DTConMSA V) by A5; ::_thesis: verum
end;
then reconsider x = x as FinSequence of TS (DTConMSA V) by FINSEQ_1:def_4;
Sym (o,V) ==> roots x by A2, MSAFREE:10;
hence x is ArgumentSeq of Sym (o,V) by A1, MSATERM:21; ::_thesis: verum
end;
registration
let S be non empty non void ManySortedSign ;
let V be V16() ManySortedSet of the carrier of S;
let o be OperSymbol of S;
cluster -> DTree-yielding for Element of Args (o,(FreeMSA V));
coherence
for b1 being Element of Args (o,(FreeMSA V)) holds b1 is DTree-yielding by Th1;
end;
theorem Th2: :: INSTALG1:2
for S being non empty non void ManySortedSign
for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds
for o being OperSymbol of S st Args (o,A1) <> {} holds
Args (o,A2) <> {}
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds
for o being OperSymbol of S st Args (o,A1) <> {} holds
Args (o,A2) <> {}
let A1, A2 be MSAlgebra over S; ::_thesis: ( the Sorts of A1 is_transformable_to the Sorts of A2 implies for o being OperSymbol of S st Args (o,A1) <> {} holds
Args (o,A2) <> {} )
assume A1: for i being set st i in the carrier of S & the Sorts of A2 . i = {} holds
the Sorts of A1 . i = {} ; :: according to PZFMISC1:def_3 ::_thesis: for o being OperSymbol of S st Args (o,A1) <> {} holds
Args (o,A2) <> {}
let o be OperSymbol of S; ::_thesis: ( Args (o,A1) <> {} implies Args (o,A2) <> {} )
assume A2: Args (o,A1) <> {} ; ::_thesis: Args (o,A2) <> {}
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(the_arity_of_o)_holds_
the_Sorts_of_A2_._((the_arity_of_o)_/._i)_<>_{}
let i be Element of NAT ; ::_thesis: ( i in dom (the_arity_of o) implies the Sorts of A2 . ((the_arity_of o) /. i) <> {} )
assume i in dom (the_arity_of o) ; ::_thesis: the Sorts of A2 . ((the_arity_of o) /. i) <> {}
then the Sorts of A1 . ((the_arity_of o) /. i) <> {} by A2, MSUALG_6:3;
hence the Sorts of A2 . ((the_arity_of o) /. i) <> {} by A1; ::_thesis: verum
end;
hence Args (o,A2) <> {} by MSUALG_6:3; ::_thesis: verum
end;
theorem Th3: :: INSTALG1:3
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for V being V16() ManySortedSet of the carrier of S
for x being Element of Args (o,(FreeMSA V)) holds (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x
proof
let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S
for V being V16() ManySortedSet of the carrier of S
for x being Element of Args (o,(FreeMSA V)) holds (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x
let o be OperSymbol of S; ::_thesis: for V being V16() ManySortedSet of the carrier of S
for x being Element of Args (o,(FreeMSA V)) holds (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x
let V be V16() ManySortedSet of the carrier of S; ::_thesis: for x being Element of Args (o,(FreeMSA V)) holds (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x
let x be Element of Args (o,(FreeMSA V)); ::_thesis: (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x
A1: FreeMSA V = MSAlgebra(# (FreeSort V),(FreeOper V) #) by MSAFREE:def_14;
reconsider p = x as ArgumentSeq of Sym (o,V) by Th1;
A2: Sym (o,V) = [o, the carrier of S] by MSAFREE:def_9;
( p is FinSequence of TS (DTConMSA V) & Sym (o,V) ==> roots p ) by MSATERM:21, MSATERM:def_1;
then (DenOp (o,V)) . x = [o, the carrier of S] -tree x by A2, MSAFREE:def_12;
hence (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x by A1, MSAFREE:def_13; ::_thesis: verum
end;
theorem :: INSTALG1:4
for S being non empty non void ManySortedSign
for A, B being MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
for o being OperSymbol of S holds Den (o,A) = Den (o,B) ;
theorem Th5: :: INSTALG1:5
for S being non empty non void ManySortedSign
for A1, A2, B1, B2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) holds
for f being ManySortedFunction of A1,A2
for g being ManySortedFunction of B1,B2 st f = g holds
for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds
for x being Element of Args (o,A1)
for y being Element of Args (o,B1) st x = y holds
f # x = g # y
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A1, A2, B1, B2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) holds
for f being ManySortedFunction of A1,A2
for g being ManySortedFunction of B1,B2 st f = g holds
for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds
for x being Element of Args (o,A1)
for y being Element of Args (o,B1) st x = y holds
f # x = g # y
let A1, A2, B1, B2 be MSAlgebra over S; ::_thesis: ( MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) implies for f being ManySortedFunction of A1,A2
for g being ManySortedFunction of B1,B2 st f = g holds
for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds
for x being Element of Args (o,A1)
for y being Element of Args (o,B1) st x = y holds
f # x = g # y )
assume A1: ( MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) ) ; ::_thesis: for f being ManySortedFunction of A1,A2
for g being ManySortedFunction of B1,B2 st f = g holds
for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds
for x being Element of Args (o,A1)
for y being Element of Args (o,B1) st x = y holds
f # x = g # y
let f be ManySortedFunction of A1,A2; ::_thesis: for g being ManySortedFunction of B1,B2 st f = g holds
for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds
for x being Element of Args (o,A1)
for y being Element of Args (o,B1) st x = y holds
f # x = g # y
let g be ManySortedFunction of B1,B2; ::_thesis: ( f = g implies for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds
for x being Element of Args (o,A1)
for y being Element of Args (o,B1) st x = y holds
f # x = g # y )
assume A2: f = g ; ::_thesis: for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds
for x being Element of Args (o,A1)
for y being Element of Args (o,B1) st x = y holds
f # x = g # y
let o be OperSymbol of S; ::_thesis: ( Args (o,A1) <> {} & Args (o,A2) <> {} implies for x being Element of Args (o,A1)
for y being Element of Args (o,B1) st x = y holds
f # x = g # y )
assume A3: ( Args (o,A1) <> {} & Args (o,A2) <> {} ) ; ::_thesis: for x being Element of Args (o,A1)
for y being Element of Args (o,B1) st x = y holds
f # x = g # y
let x be Element of Args (o,A1); ::_thesis: for y being Element of Args (o,B1) st x = y holds
f # x = g # y
let y be Element of Args (o,B1); ::_thesis: ( x = y implies f # x = g # y )
assume A4: x = y ; ::_thesis: f # x = g # y
f # x = (Frege (f * (the_arity_of o))) . x by A3, MSUALG_3:def_5;
hence f # x = g # y by A1, A2, A3, A4, MSUALG_3:def_5; ::_thesis: verum
end;
theorem :: INSTALG1:6
for S being non empty non void ManySortedSign
for A1, A2, B1, B2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) & the Sorts of A1 is_transformable_to the Sorts of A2 holds
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
ex h9 being ManySortedFunction of B1,B2 st
( h9 = h & h9 is_homomorphism B1,B2 )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A1, A2, B1, B2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) & the Sorts of A1 is_transformable_to the Sorts of A2 holds
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
ex h9 being ManySortedFunction of B1,B2 st
( h9 = h & h9 is_homomorphism B1,B2 )
let A1, A2, B1, B2 be MSAlgebra over S; ::_thesis: ( MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) & the Sorts of A1 is_transformable_to the Sorts of A2 implies for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
ex h9 being ManySortedFunction of B1,B2 st
( h9 = h & h9 is_homomorphism B1,B2 ) )
assume that
A1: MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) and
A2: MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) and
A3: the Sorts of A1 is_transformable_to the Sorts of A2 ; ::_thesis: for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
ex h9 being ManySortedFunction of B1,B2 st
( h9 = h & h9 is_homomorphism B1,B2 )
let h be ManySortedFunction of A1,A2; ::_thesis: ( h is_homomorphism A1,A2 implies ex h9 being ManySortedFunction of B1,B2 st
( h9 = h & h9 is_homomorphism B1,B2 ) )
assume A4: h is_homomorphism A1,A2 ; ::_thesis: ex h9 being ManySortedFunction of B1,B2 st
( h9 = h & h9 is_homomorphism B1,B2 )
reconsider h9 = h as ManySortedFunction of B1,B2 by A1, A2;
take h9 ; ::_thesis: ( h9 = h & h9 is_homomorphism B1,B2 )
thus h9 = h ; ::_thesis: h9 is_homomorphism B1,B2
let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,B1) = {} or for b1 being Element of Args (o,B1) holds (h9 . (the_result_sort_of o)) . ((Den (o,B1)) . b1) = (Den (o,B2)) . (h9 # b1) )
assume A5: Args (o,B1) <> {} ; ::_thesis: for b1 being Element of Args (o,B1) holds (h9 . (the_result_sort_of o)) . ((Den (o,B1)) . b1) = (Den (o,B2)) . (h9 # b1)
then A6: Args (o,B2) <> {} by A1, A2, A3, Th2;
let x be Element of Args (o,B1); ::_thesis: (h9 . (the_result_sort_of o)) . ((Den (o,B1)) . x) = (Den (o,B2)) . (h9 # x)
reconsider y = x as Element of Args (o,A1) by A1;
thus (h9 . (the_result_sort_of o)) . ((Den (o,B1)) . x) = (h . (the_result_sort_of o)) . ((Den (o,A1)) . y) by A1
.= (Den (o,A2)) . (h # y) by A1, A4, A5, MSUALG_3:def_7
.= (Den (o,B2)) . (h9 # x) by A1, A2, A5, A6, Th5 ; ::_thesis: verum
end;
definition
let S be ManySortedSign ;
attrS is feasible means :Def1: :: INSTALG1:def 1
( the carrier of S = {} implies the carrier' of S = {} );
end;
:: deftheorem Def1 defines feasible INSTALG1:def_1_:_
for S being ManySortedSign holds
( S is feasible iff ( the carrier of S = {} implies the carrier' of S = {} ) );
theorem Th7: :: INSTALG1:7
for S being ManySortedSign holds
( S is feasible iff dom the ResultSort of S = the carrier' of S )
proof
let S be ManySortedSign ; ::_thesis: ( S is feasible iff dom the ResultSort of S = the carrier' of S )
hereby ::_thesis: ( dom the ResultSort of S = the carrier' of S implies S is feasible )
assume S is feasible ; ::_thesis: dom the ResultSort of S = the carrier' of S
then ( the carrier of S = {} implies the carrier' of S = {} ) by Def1;
hence dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1; ::_thesis: verum
end;
assume ( dom the ResultSort of S = the carrier' of S & the carrier of S = {} & the carrier' of S <> {} ) ; :: according to INSTALG1:def_1 ::_thesis: contradiction
hence contradiction ; ::_thesis: verum
end;
registration
cluster non empty -> feasible for ManySortedSign ;
coherence
for b1 being ManySortedSign st not b1 is empty holds
b1 is feasible
proof
let S be ManySortedSign ; ::_thesis: ( not S is empty implies S is feasible )
assume ( not the carrier of S is empty & the carrier of S = {} ) ; :: according to STRUCT_0:def_1,INSTALG1:def_1 ::_thesis: the carrier' of S = {}
hence the carrier' of S = {} ; ::_thesis: verum
end;
cluster void -> feasible for ManySortedSign ;
coherence
for b1 being ManySortedSign st b1 is void holds
b1 is feasible
proof
let S be ManySortedSign ; ::_thesis: ( S is void implies S is feasible )
assume that
A1: S is void and
the carrier of S = {} ; :: according to INSTALG1:def_1 ::_thesis: the carrier' of S = {}
thus the carrier' of S = {} by A1; ::_thesis: verum
end;
cluster empty feasible -> void for ManySortedSign ;
coherence
for b1 being ManySortedSign st b1 is empty & b1 is feasible holds
b1 is void
proof
let S be ManySortedSign ; ::_thesis: ( S is empty & S is feasible implies S is void )
assume A2: the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: ( not S is feasible or S is void )
assume ( the carrier of S = {} implies the carrier' of S = {} ) ; :: according to INSTALG1:def_1 ::_thesis: S is void
hence S is void by A2; ::_thesis: verum
end;
cluster non void feasible -> non empty for ManySortedSign ;
coherence
for b1 being ManySortedSign st not b1 is void & b1 is feasible holds
not b1 is empty ;
end;
registration
cluster non empty non void for ManySortedSign ;
existence
ex b1 being ManySortedSign st
( not b1 is void & not b1 is empty )
proof
set S = the non empty non void ManySortedSign ;
take the non empty non void ManySortedSign ; ::_thesis: ( not the non empty non void ManySortedSign is void & not the non empty non void ManySortedSign is empty )
thus ( not the non empty non void ManySortedSign is void & not the non empty non void ManySortedSign is empty ) ; ::_thesis: verum
end;
end;
theorem Th8: :: INSTALG1:8
for S being feasible ManySortedSign holds id the carrier of S, id the carrier' of S form_morphism_between S,S
proof
let S be feasible ManySortedSign ; ::_thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S
percases ( S is void or not S is void ) ;
suppose S is void ; ::_thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S
hence id the carrier of S, id the carrier' of S form_morphism_between S,S by MSALIMIT:6; ::_thesis: verum
end;
suppose not S is void ; ::_thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S
then reconsider S = S as non void feasible ManySortedSign ;
not S is empty ;
hence id the carrier of S, id the carrier' of S form_morphism_between S,S by PUA2MSS1:28; ::_thesis: verum
end;
end;
end;
theorem Th9: :: INSTALG1:9
for S1, S2 being ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
( f is Function of the carrier of S1, the carrier of S2 & g is Function of the carrier' of S1, the carrier' of S2 )
proof
let S1, S2 be ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
( f is Function of the carrier of S1, the carrier of S2 & g is Function of the carrier' of S1, the carrier' of S2 )
let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies ( f is Function of the carrier of S1, the carrier of S2 & g is Function of the carrier' of S1, the carrier' of S2 ) )
assume A1: f,g form_morphism_between S1,S2 ; ::_thesis: ( f is Function of the carrier of S1, the carrier of S2 & g is Function of the carrier' of S1, the carrier' of S2 )
then A2: ( dom f = the carrier of S1 & rng f c= the carrier of S2 ) by PUA2MSS1:def_12;
( dom g = the carrier' of S1 & rng g c= the carrier' of S2 ) by A1, PUA2MSS1:def_12;
hence ( f is Function of the carrier of S1, the carrier of S2 & g is Function of the carrier' of S1, the carrier' of S2 ) by A2, FUNCT_2:2; ::_thesis: verum
end;
begin
definition
let S be feasible ManySortedSign ;
mode Subsignature of S -> ManySortedSign means :Def2: :: INSTALG1:def 2
id the carrier of it, id the carrier' of it form_morphism_between it,S;
existence
ex b1 being ManySortedSign st id the carrier of b1, id the carrier' of b1 form_morphism_between b1,S
proof
take S ; ::_thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S
thus id the carrier of S, id the carrier' of S form_morphism_between S,S by Th8; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines Subsignature INSTALG1:def_2_:_
for S being feasible ManySortedSign
for b2 being ManySortedSign holds
( b2 is Subsignature of S iff id the carrier of b2, id the carrier' of b2 form_morphism_between b2,S );
theorem Th10: :: INSTALG1:10
for S being feasible ManySortedSign
for T being Subsignature of S holds
( the carrier of T c= the carrier of S & the carrier' of T c= the carrier' of S )
proof
let S be feasible ManySortedSign ; ::_thesis: for T being Subsignature of S holds
( the carrier of T c= the carrier of S & the carrier' of T c= the carrier' of S )
let T be Subsignature of S; ::_thesis: ( the carrier of T c= the carrier of S & the carrier' of T c= the carrier' of S )
set g = id the carrier' of T;
id the carrier of T, id the carrier' of T form_morphism_between T,S by Def2;
then ( rng (id the carrier of T) c= the carrier of S & rng (id the carrier' of T) c= the carrier' of S ) by PUA2MSS1:def_12;
hence ( the carrier of T c= the carrier of S & the carrier' of T c= the carrier' of S ) ; ::_thesis: verum
end;
registration
let S be feasible ManySortedSign ;
cluster -> feasible for Subsignature of S;
coherence
for b1 being Subsignature of S holds b1 is feasible
proof
let T be Subsignature of S; ::_thesis: T is feasible
set f = id the carrier of T;
set g = id the carrier' of T;
A1: dom (id the carrier' of T) = the carrier' of T ;
id the carrier of T, id the carrier' of T form_morphism_between T,S by Def2;
then A2: (id the carrier of T) * the ResultSort of T = the ResultSort of S * (id the carrier' of T) by PUA2MSS1:def_12;
assume the carrier of T = {} ; :: according to INSTALG1:def_1 ::_thesis: the carrier' of T = {}
then A3: {} = the ResultSort of S * (id the carrier' of T) by A2;
( the carrier' of S = dom the ResultSort of S & rng (id the carrier' of T) = the carrier' of T ) by Th7;
hence the carrier' of T = {} by A3, A1, Th10, RELAT_1:27, RELAT_1:38; ::_thesis: verum
end;
end;
theorem Th11: :: INSTALG1:11
for S being feasible ManySortedSign
for T being Subsignature of S holds
( the ResultSort of T c= the ResultSort of S & the Arity of T c= the Arity of S )
proof
let S be feasible ManySortedSign ; ::_thesis: for T being Subsignature of S holds
( the ResultSort of T c= the ResultSort of S & the Arity of T c= the Arity of S )
let T be Subsignature of S; ::_thesis: ( the ResultSort of T c= the ResultSort of S & the Arity of T c= the Arity of S )
set f = id the carrier of T;
set g = id the carrier' of T;
A1: dom the Arity of T = the carrier' of T by FUNCT_2:def_1;
A2: id the carrier of T, id the carrier' of T form_morphism_between T,S by Def2;
A3: now__::_thesis:_for_x_being_set_st_x_in_dom_the_Arity_of_T_holds_
the_Arity_of_T_._x_=_the_Arity_of_S_._x
let x be set ; ::_thesis: ( x in dom the Arity of T implies the Arity of T . x = the Arity of S . x )
A4: rng the Arity of T c= the carrier of T * by RELAT_1:def_19;
assume A5: x in dom the Arity of T ; ::_thesis: the Arity of T . x = the Arity of S . x
then the Arity of T . x in rng the Arity of T by FUNCT_1:def_3;
then reconsider p = the Arity of T . x as Element of the carrier of T * by A4;
(id the carrier' of T) . x = x by A1, A5, FUNCT_1:17;
then ( rng p c= the carrier of T & (id the carrier of T) * p = the Arity of S . x ) by A2, A1, A5, FINSEQ_1:def_4, PUA2MSS1:def_12;
hence the Arity of T . x = the Arity of S . x by RELAT_1:53; ::_thesis: verum
end;
the ResultSort of T = (id the carrier of T) * the ResultSort of T by FUNCT_2:17
.= the ResultSort of S * (id the carrier' of T) by A2, PUA2MSS1:def_12 ;
hence the ResultSort of T c= the ResultSort of S by RELAT_1:50; ::_thesis: the Arity of T c= the Arity of S
dom the Arity of S = the carrier' of S by FUNCT_2:def_1;
then dom the Arity of T c= dom the Arity of S by A1, Th10;
hence the Arity of T c= the Arity of S by A3, GRFUNC_1:2; ::_thesis: verum
end;
theorem Th12: :: INSTALG1:12
for S being feasible ManySortedSign
for T being Subsignature of S holds
( the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T )
proof
let S be feasible ManySortedSign ; ::_thesis: for T being Subsignature of S holds
( the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T )
let T be Subsignature of S; ::_thesis: ( the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T )
A1: the Arity of T c= the Arity of S by Th11;
( the carrier of T = {} implies the carrier' of T = {} ) by Def1;
then A2: dom the ResultSort of T = the carrier' of T by FUNCT_2:def_1;
( dom the Arity of T = the carrier' of T & the ResultSort of T c= the ResultSort of S ) by Th11, FUNCT_2:def_1;
hence ( the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T ) by A2, A1, GRFUNC_1:23; ::_thesis: verum
end;
theorem Th13: :: INSTALG1:13
for S, T being feasible ManySortedSign st the carrier of T c= the carrier of S & the Arity of T c= the Arity of S & the ResultSort of T c= the ResultSort of S holds
T is Subsignature of S
proof
let S, T be feasible ManySortedSign ; ::_thesis: ( the carrier of T c= the carrier of S & the Arity of T c= the Arity of S & the ResultSort of T c= the ResultSort of S implies T is Subsignature of S )
assume that
A1: the carrier of T c= the carrier of S and
A2: the Arity of T c= the Arity of S and
A3: the ResultSort of T c= the ResultSort of S ; ::_thesis: T is Subsignature of S
set f = id the carrier of T;
set g = id the carrier' of T;
thus ( dom (id the carrier of T) = the carrier of T & dom (id the carrier' of T) = the carrier' of T ) ; :: according to PUA2MSS1:def_12,INSTALG1:def_2 ::_thesis: ( rng (id the carrier of T) c= the carrier of S & rng (id the carrier' of T) c= the carrier' of S & the ResultSort of T * (id the carrier of T) = (id the carrier' of T) * the ResultSort of S & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of T or not b2 = the Arity of T . b1 or b2 * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . b1) ) ) )
thus rng (id the carrier of T) c= the carrier of S by A1; ::_thesis: ( rng (id the carrier' of T) c= the carrier' of S & the ResultSort of T * (id the carrier of T) = (id the carrier' of T) * the ResultSort of S & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of T or not b2 = the Arity of T . b1 or b2 * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . b1) ) ) )
A4: dom the Arity of T = the carrier' of T by FUNCT_2:def_1;
( dom the Arity of S = the carrier' of S & rng (id the carrier' of T) = the carrier' of T ) by FUNCT_2:def_1;
hence rng (id the carrier' of T) c= the carrier' of S by A2, A4, GRFUNC_1:2; ::_thesis: ( the ResultSort of T * (id the carrier of T) = (id the carrier' of T) * the ResultSort of S & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of T or not b2 = the Arity of T . b1 or b2 * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . b1) ) ) )
A5: dom the ResultSort of T = the carrier' of T by Th7;
rng the ResultSort of T c= the carrier of T by RELAT_1:def_19;
hence (id the carrier of T) * the ResultSort of T = the ResultSort of T by RELAT_1:53
.= the ResultSort of S | the carrier' of T by A3, A5, GRFUNC_1:23
.= the ResultSort of S * (id the carrier' of T) by RELAT_1:65 ;
::_thesis: for b1 being set
for b2 being set holds
( not b1 in the carrier' of T or not b2 = the Arity of T . b1 or b2 * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . b1) )
let o be set ; ::_thesis: for b1 being set holds
( not o in the carrier' of T or not b1 = the Arity of T . o or b1 * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . o) )
let p be Function; ::_thesis: ( not o in the carrier' of T or not p = the Arity of T . o or p * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . o) )
assume that
A6: o in the carrier' of T and
A7: p = the Arity of T . o ; ::_thesis: p * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . o)
reconsider q = p as Element of the carrier of T * by A6, A7, FUNCT_2:5;
rng q c= the carrier of T by FINSEQ_1:def_4;
hence (id the carrier of T) * p = p by RELAT_1:53
.= the Arity of S . o by A2, A4, A6, A7, GRFUNC_1:2
.= the Arity of S . ((id the carrier' of T) . o) by A6, FUNCT_1:17 ;
::_thesis: verum
end;
theorem :: INSTALG1:14
for S, T being feasible ManySortedSign st the carrier of T c= the carrier of S & the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T holds
T is Subsignature of S
proof
let S, T be feasible ManySortedSign ; ::_thesis: ( the carrier of T c= the carrier of S & the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T implies T is Subsignature of S )
assume A1: the carrier of T c= the carrier of S ; ::_thesis: ( not the Arity of T = the Arity of S | the carrier' of T or not the ResultSort of T = the ResultSort of S | the carrier' of T or T is Subsignature of S )
assume that
A2: the Arity of T = the Arity of S | the carrier' of T and
A3: the ResultSort of T = the ResultSort of S | the carrier' of T ; ::_thesis: T is Subsignature of S
the Arity of T c= the Arity of S by A2, RELAT_1:59;
hence T is Subsignature of S by A1, A3, Th13, RELAT_1:59; ::_thesis: verum
end;
theorem Th15: :: INSTALG1:15
for S being feasible ManySortedSign holds S is Subsignature of S
proof
let S be feasible ManySortedSign ; ::_thesis: S is Subsignature of S
thus id the carrier of S, id the carrier' of S form_morphism_between S,S by Th8; :: according to INSTALG1:def_2 ::_thesis: verum
end;
theorem :: INSTALG1:16
for S1 being feasible ManySortedSign
for S2 being Subsignature of S1
for S3 being Subsignature of S2 holds S3 is Subsignature of S1
proof
let S1 be feasible ManySortedSign ; ::_thesis: for S2 being Subsignature of S1
for S3 being Subsignature of S2 holds S3 is Subsignature of S1
let S2 be Subsignature of S1; ::_thesis: for S3 being Subsignature of S2 holds S3 is Subsignature of S1
let S3 be Subsignature of S2; ::_thesis: S3 is Subsignature of S1
rng (id the carrier of S3) = the carrier of S3 ;
then A1: (id the carrier of S2) * (id the carrier of S3) = id the carrier of S3 by Th10, RELAT_1:53;
rng (id the carrier' of S3) = the carrier' of S3 ;
then A2: (id the carrier' of S2) * (id the carrier' of S3) = id the carrier' of S3 by Th10, RELAT_1:53;
( id the carrier of S3, id the carrier' of S3 form_morphism_between S3,S2 & id the carrier of S2, id the carrier' of S2 form_morphism_between S2,S1 ) by Def2;
hence id the carrier of S3, id the carrier' of S3 form_morphism_between S3,S1 by A1, A2, PUA2MSS1:29; :: according to INSTALG1:def_2 ::_thesis: verum
end;
theorem :: INSTALG1:17
for S1 being feasible ManySortedSign
for S2 being Subsignature of S1 st S1 is Subsignature of S2 holds
ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #)
proof
let S1 be feasible ManySortedSign ; ::_thesis: for S2 being Subsignature of S1 st S1 is Subsignature of S2 holds
ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #)
let S2 be Subsignature of S1; ::_thesis: ( S1 is Subsignature of S2 implies ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) )
A1: the carrier of S2 c= the carrier of S1 by Th10;
assume A2: S1 is Subsignature of S2 ; ::_thesis: ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #)
then the carrier of S1 c= the carrier of S2 by Th10;
then A3: the carrier of S1 = the carrier of S2 by A1, XBOOLE_0:def_10;
A4: the carrier' of S2 c= the carrier' of S1 by Th10;
the carrier' of S1 c= the carrier' of S2 by A2, Th10;
then A5: the carrier' of S1 = the carrier' of S2 by A4, XBOOLE_0:def_10;
A6: the Arity of S2 c= the Arity of S1 by Th11;
A7: the ResultSort of S2 c= the ResultSort of S1 by Th11;
the ResultSort of S1 c= the ResultSort of S2 by A2, Th11;
then A8: the ResultSort of S1 = the ResultSort of S2 by A7, XBOOLE_0:def_10;
the Arity of S1 c= the Arity of S2 by A2, Th11;
hence ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) by A6, A3, A5, A8, XBOOLE_0:def_10; ::_thesis: verum
end;
registration
let S be non empty ManySortedSign ;
cluster non empty feasible for Subsignature of S;
existence
not for b1 being Subsignature of S holds b1 is empty
proof
reconsider T = S as Subsignature of S by Th15;
take T ; ::_thesis: not T is empty
thus not T is empty ; ::_thesis: verum
end;
end;
registration
let S be non void feasible ManySortedSign ;
cluster non void feasible for Subsignature of S;
existence
not for b1 being Subsignature of S holds b1 is void
proof
reconsider T = S as Subsignature of S by Th15;
take T ; ::_thesis: not T is void
thus not T is void ; ::_thesis: verum
end;
end;
theorem :: INSTALG1:18
for S being feasible ManySortedSign
for S9 being Subsignature of S
for T being ManySortedSign
for f, g being Function st f,g form_morphism_between S,T holds
f | the carrier of S9,g | the carrier' of S9 form_morphism_between S9,T
proof
let S be feasible ManySortedSign ; ::_thesis: for S9 being Subsignature of S
for T being ManySortedSign
for f, g being Function st f,g form_morphism_between S,T holds
f | the carrier of S9,g | the carrier' of S9 form_morphism_between S9,T
let S9 be Subsignature of S; ::_thesis: for T being ManySortedSign
for f, g being Function st f,g form_morphism_between S,T holds
f | the carrier of S9,g | the carrier' of S9 form_morphism_between S9,T
let T be ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S,T holds
f | the carrier of S9,g | the carrier' of S9 form_morphism_between S9,T
let f, g be Function; ::_thesis: ( f,g form_morphism_between S,T implies f | the carrier of S9,g | the carrier' of S9 form_morphism_between S9,T )
A1: g | the carrier' of S9 = g * (id the carrier' of S9) by RELAT_1:65;
( id the carrier of S9, id the carrier' of S9 form_morphism_between S9,S & f | the carrier of S9 = f * (id the carrier of S9) ) by Def2, RELAT_1:65;
hence ( f,g form_morphism_between S,T implies f | the carrier of S9,g | the carrier' of S9 form_morphism_between S9,T ) by A1, PUA2MSS1:29; ::_thesis: verum
end;
theorem :: INSTALG1:19
for S being ManySortedSign
for T being feasible ManySortedSign
for T9 being Subsignature of T
for f, g being Function st f,g form_morphism_between S,T9 holds
f,g form_morphism_between S,T
proof
let S be ManySortedSign ; ::_thesis: for T being feasible ManySortedSign
for T9 being Subsignature of T
for f, g being Function st f,g form_morphism_between S,T9 holds
f,g form_morphism_between S,T
let T be feasible ManySortedSign ; ::_thesis: for T9 being Subsignature of T
for f, g being Function st f,g form_morphism_between S,T9 holds
f,g form_morphism_between S,T
let T9 be Subsignature of T; ::_thesis: for f, g being Function st f,g form_morphism_between S,T9 holds
f,g form_morphism_between S,T
let f, g be Function; ::_thesis: ( f,g form_morphism_between S,T9 implies f,g form_morphism_between S,T )
assume A1: f,g form_morphism_between S,T9 ; ::_thesis: f,g form_morphism_between S,T
rng f c= the carrier of T9 by A1, PUA2MSS1:def_12;
then A2: (id the carrier of T9) * f = f by RELAT_1:53;
rng g c= the carrier' of T9 by A1, PUA2MSS1:def_12;
then A3: (id the carrier' of T9) * g = g by RELAT_1:53;
id the carrier of T9, id the carrier' of T9 form_morphism_between T9,T by Def2;
hence f,g form_morphism_between S,T by A1, A2, A3, PUA2MSS1:29; ::_thesis: verum
end;
theorem :: INSTALG1:20
for S being ManySortedSign
for T being feasible ManySortedSign
for T9 being Subsignature of T
for f, g being Function st f,g form_morphism_between S,T & rng f c= the carrier of T9 & rng g c= the carrier' of T9 holds
f,g form_morphism_between S,T9
proof
let S be ManySortedSign ; ::_thesis: for T being feasible ManySortedSign
for T9 being Subsignature of T
for f, g being Function st f,g form_morphism_between S,T & rng f c= the carrier of T9 & rng g c= the carrier' of T9 holds
f,g form_morphism_between S,T9
let T be feasible ManySortedSign ; ::_thesis: for T9 being Subsignature of T
for f, g being Function st f,g form_morphism_between S,T & rng f c= the carrier of T9 & rng g c= the carrier' of T9 holds
f,g form_morphism_between S,T9
let T9 be Subsignature of T; ::_thesis: for f, g being Function st f,g form_morphism_between S,T & rng f c= the carrier of T9 & rng g c= the carrier' of T9 holds
f,g form_morphism_between S,T9
let f, g be Function; ::_thesis: ( f,g form_morphism_between S,T & rng f c= the carrier of T9 & rng g c= the carrier' of T9 implies f,g form_morphism_between S,T9 )
assume that
A1: dom f = the carrier of S and
A2: dom g = the carrier' of S and
rng f c= the carrier of T and
rng g c= the carrier' of T and
A3: f * the ResultSort of S = the ResultSort of T * g and
A4: for o being set
for p being Function st o in the carrier' of S & p = the Arity of S . o holds
f * p = the Arity of T . (g . o) and
A5: rng f c= the carrier of T9 and
A6: rng g c= the carrier' of T9 ; :: according to PUA2MSS1:def_12 ::_thesis: f,g form_morphism_between S,T9
thus ( dom f = the carrier of S & dom g = the carrier' of S ) by A1, A2; :: according to PUA2MSS1:def_12 ::_thesis: ( rng f c= the carrier of T9 & rng g c= the carrier' of T9 & the ResultSort of S * f = g * the ResultSort of T9 & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of S or not b2 = the Arity of S . b1 or b2 * f = the Arity of T9 . (g . b1) ) ) )
thus ( rng f c= the carrier of T9 & rng g c= the carrier' of T9 ) by A5, A6; ::_thesis: ( the ResultSort of S * f = g * the ResultSort of T9 & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of S or not b2 = the Arity of S . b1 or b2 * f = the Arity of T9 . (g . b1) ) ) )
thus f * the ResultSort of S = the ResultSort of T * ((id the carrier' of T9) * g) by A3, A6, RELAT_1:53
.= ( the ResultSort of T * (id the carrier' of T9)) * g by RELAT_1:36
.= ( the ResultSort of T | the carrier' of T9) * g by RELAT_1:65
.= the ResultSort of T9 * g by Th12 ; ::_thesis: for b1 being set
for b2 being set holds
( not b1 in the carrier' of S or not b2 = the Arity of S . b1 or b2 * f = the Arity of T9 . (g . b1) )
let o be set ; ::_thesis: for b1 being set holds
( not o in the carrier' of S or not b1 = the Arity of S . o or b1 * f = the Arity of T9 . (g . o) )
let p be Function; ::_thesis: ( not o in the carrier' of S or not p = the Arity of S . o or p * f = the Arity of T9 . (g . o) )
assume that
A7: o in the carrier' of S and
A8: p = the Arity of S . o ; ::_thesis: p * f = the Arity of T9 . (g . o)
A9: ( the Arity of T9 c= the Arity of T & dom the Arity of T9 = the carrier' of T9 ) by Th11, FUNCT_2:def_1;
g . o in rng g by A2, A7, FUNCT_1:def_3;
then the Arity of T9 . (g . o) = the Arity of T . (g . o) by A6, A9, GRFUNC_1:2;
hence p * f = the Arity of T9 . (g . o) by A4, A7, A8; ::_thesis: verum
end;
begin
definition
let S1, S2 be non empty ManySortedSign ;
let A be MSAlgebra over S2;
let f, g be Function;
assume B1: f,g form_morphism_between S1,S2 ;
funcA | (S1,f,g) -> strict MSAlgebra over S1 means :Def3: :: INSTALG1:def 3
( the Sorts of it = the Sorts of A * f & the Charact of it = the Charact of A * g );
existence
ex b1 being strict MSAlgebra over S1 st
( the Sorts of b1 = the Sorts of A * f & the Charact of b1 = the Charact of A * g )
proof
( dom f = the carrier of S1 & rng f c= the carrier of S2 ) by B1, PUA2MSS1:def_12;
then reconsider f9 = f as Function of the carrier of S1, the carrier of S2 by FUNCT_2:def_1, RELSET_1:4;
A1: rng g c= the carrier' of S2 by B1, PUA2MSS1:def_12;
A2: dom g = the carrier' of S1 by B1, PUA2MSS1:def_12;
then reconsider g9 = g as Function of the carrier' of S1, the carrier' of S2 by A1, FUNCT_2:2;
dom the Charact of A = the carrier' of S2 by PARTFUN1:def_2;
then dom ( the Charact of A * g9) = the carrier' of S1 by A2, A1, RELAT_1:27;
then reconsider C = the Charact of A * g9 as ManySortedSet of the carrier' of S1 by PARTFUN1:def_2;
C is ManySortedFunction of (( the Sorts of A * f9) #) * the Arity of S1,( the Sorts of A * f9) * the ResultSort of S1
proof
let o be set ; :: according to PBOOLE:def_15 ::_thesis: ( not o in the carrier' of S1 or C . o is Element of bool [:(((( the Sorts of A * f9) #) * the Arity of S1) . o),((( the Sorts of A * f9) * the ResultSort of S1) . o):] )
assume A3: o in the carrier' of S1 ; ::_thesis: C . o is Element of bool [:(((( the Sorts of A * f9) #) * the Arity of S1) . o),((( the Sorts of A * f9) * the ResultSort of S1) . o):]
then reconsider p1 = the Arity of S1 . o as Element of the carrier of S1 * by FUNCT_2:5;
A4: g . o in rng g by A2, A3, FUNCT_1:def_3;
then reconsider p2 = the Arity of S2 . (g . o) as Element of the carrier of S2 * by A1, FUNCT_2:5;
reconsider o = o as OperSymbol of S1 by A3;
A5: C . o = the Charact of A . (g9 . o) by A1, A3, A4, FUNCT_2:15;
( the Sorts of A * f9) * the ResultSort of S1 = the Sorts of A * (f9 * the ResultSort of S1) by RELAT_1:36
.= the Sorts of A * ( the ResultSort of S2 * g) by B1, PUA2MSS1:def_12
.= ( the Sorts of A * the ResultSort of S2) * g by RELAT_1:36 ;
then A6: (( the Sorts of A * f9) * the ResultSort of S1) . o = ( the Sorts of A * the ResultSort of S2) . (g9 . o) by A1, A3, A4, FUNCT_2:15;
A7: ( the Sorts of A * f9) * p1 = the Sorts of A * (f9 * p1) by RELAT_1:36
.= the Sorts of A * p2 by B1, A3, PUA2MSS1:def_12 ;
((( the Sorts of A * f9) #) * the Arity of S1) . o = (( the Sorts of A * f9) #) . p1 by A3, FUNCT_2:15
.= product (( the Sorts of A * f9) * p1) by FINSEQ_2:def_5
.= ( the Sorts of A #) . p2 by A7, FINSEQ_2:def_5
.= (( the Sorts of A #) * the Arity of S2) . (g9 . o) by A1, A4, FUNCT_2:15 ;
hence C . o is Element of bool [:(((( the Sorts of A * f9) #) * the Arity of S1) . o),((( the Sorts of A * f9) * the ResultSort of S1) . o):] by A1, A4, A6, A5, PBOOLE:def_15; ::_thesis: verum
end;
then reconsider C = C as ManySortedFunction of (( the Sorts of A * f9) #) * the Arity of S1,( the Sorts of A * f9) * the ResultSort of S1 ;
take MSAlgebra(# ( the Sorts of A * f9),C #) ; ::_thesis: ( the Sorts of MSAlgebra(# ( the Sorts of A * f9),C #) = the Sorts of A * f & the Charact of MSAlgebra(# ( the Sorts of A * f9),C #) = the Charact of A * g )
thus ( the Sorts of MSAlgebra(# ( the Sorts of A * f9),C #) = the Sorts of A * f & the Charact of MSAlgebra(# ( the Sorts of A * f9),C #) = the Charact of A * g ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being strict MSAlgebra over S1 st the Sorts of b1 = the Sorts of A * f & the Charact of b1 = the Charact of A * g & the Sorts of b2 = the Sorts of A * f & the Charact of b2 = the Charact of A * g holds
b1 = b2;
;
end;
:: deftheorem Def3 defines | INSTALG1:def_3_:_
for S1, S2 being non empty ManySortedSign
for A being MSAlgebra over S2
for f, g being Function st f,g form_morphism_between S1,S2 holds
for b6 being strict MSAlgebra over S1 holds
( b6 = A | (S1,f,g) iff ( the Sorts of b6 = the Sorts of A * f & the Charact of b6 = the Charact of A * g ) );
definition
let S2, S1 be non empty ManySortedSign ;
let A be MSAlgebra over S2;
funcA | S1 -> strict MSAlgebra over S1 equals :: INSTALG1:def 4
A | (S1,(id the carrier of S1),(id the carrier' of S1));
correctness
coherence
A | (S1,(id the carrier of S1),(id the carrier' of S1)) is strict MSAlgebra over S1;
;
end;
:: deftheorem defines | INSTALG1:def_4_:_
for S2, S1 being non empty ManySortedSign
for A being MSAlgebra over S2 holds A | S1 = A | (S1,(id the carrier of S1),(id the carrier' of S1));
theorem :: INSTALG1:21
for S1, S2 being non empty ManySortedSign
for A, B being MSAlgebra over S2 st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
for f, g being Function st f,g form_morphism_between S1,S2 holds
A | (S1,f,g) = B | (S1,f,g)
proof
let S1, S2 be non empty ManySortedSign ; ::_thesis: for A, B being MSAlgebra over S2 st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
for f, g being Function st f,g form_morphism_between S1,S2 holds
A | (S1,f,g) = B | (S1,f,g)
let A, B be MSAlgebra over S2; ::_thesis: ( MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) implies for f, g being Function st f,g form_morphism_between S1,S2 holds
A | (S1,f,g) = B | (S1,f,g) )
assume A1: MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
A | (S1,f,g) = B | (S1,f,g)
let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies A | (S1,f,g) = B | (S1,f,g) )
assume A2: f,g form_morphism_between S1,S2 ; ::_thesis: A | (S1,f,g) = B | (S1,f,g)
then ( the Sorts of (A | (S1,f,g)) = the Sorts of A * f & the Charact of (A | (S1,f,g)) = the Charact of A * g ) by Def3;
hence A | (S1,f,g) = B | (S1,f,g) by A1, A2, Def3; ::_thesis: verum
end;
theorem Th22: :: INSTALG1:22
for S1, S2 being non empty ManySortedSign
for A being non-empty MSAlgebra over S2
for f, g being Function st f,g form_morphism_between S1,S2 holds
A | (S1,f,g) is non-empty
proof
let S1, S2 be non empty ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S2
for f, g being Function st f,g form_morphism_between S1,S2 holds
A | (S1,f,g) is non-empty
let A be non-empty MSAlgebra over S2; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
A | (S1,f,g) is non-empty
let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies A | (S1,f,g) is non-empty )
assume f,g form_morphism_between S1,S2 ; ::_thesis: A | (S1,f,g) is non-empty
then the Sorts of (A | (S1,f,g)) = the Sorts of A * f by Def3;
hence the Sorts of (A | (S1,f,g)) is V16() ; :: according to MSUALG_1:def_3 ::_thesis: verum
end;
registration
let S2 be non empty ManySortedSign ;
let S1 be non empty Subsignature of S2;
let A be non-empty MSAlgebra over S2;
clusterA | S1 -> strict non-empty ;
coherence
A | S1 is non-empty
proof
id the carrier of S1, id the carrier' of S1 form_morphism_between S1,S2 by Def2;
hence A | S1 is non-empty by Th22; ::_thesis: verum
end;
end;
theorem Th23: :: INSTALG1:23
for S1, S2 being non empty non void ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
for A being MSAlgebra over S2
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
Den (o1,(A | (S1,f,g))) = Den (o2,A)
proof
let S1, S2 be non empty non void ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
for A being MSAlgebra over S2
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
Den (o1,(A | (S1,f,g))) = Den (o2,A)
let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for A being MSAlgebra over S2
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
Den (o1,(A | (S1,f,g))) = Den (o2,A) )
assume A1: f,g form_morphism_between S1,S2 ; ::_thesis: for A being MSAlgebra over S2
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
Den (o1,(A | (S1,f,g))) = Den (o2,A)
then reconsider g9 = g as Function of the carrier' of S1, the carrier' of S2 by Th9;
let A be MSAlgebra over S2; ::_thesis: for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
Den (o1,(A | (S1,f,g))) = Den (o2,A)
let o1 be OperSymbol of S1; ::_thesis: for o2 being OperSymbol of S2 st o2 = g . o1 holds
Den (o1,(A | (S1,f,g))) = Den (o2,A)
let o2 be OperSymbol of S2; ::_thesis: ( o2 = g . o1 implies Den (o1,(A | (S1,f,g))) = Den (o2,A) )
assume o2 = g . o1 ; ::_thesis: Den (o1,(A | (S1,f,g))) = Den (o2,A)
then the Charact of A . o2 = ( the Charact of A * g9) . o1 by FUNCT_2:15
.= the Charact of (A | (S1,f,g)) . o1 by A1, Def3 ;
hence Den (o1,(A | (S1,f,g))) = Den (o2,A) ; ::_thesis: verum
end;
theorem Th24: :: INSTALG1:24
for S1, S2 being non empty non void ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
for A being MSAlgebra over S2
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) )
proof
let S1, S2 be non empty non void ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
for A being MSAlgebra over S2
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) )
let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for A being MSAlgebra over S2
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) ) )
assume A1: f,g form_morphism_between S1,S2 ; ::_thesis: for A being MSAlgebra over S2
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) )
A2: dom f = the carrier of S1 by A1, PUA2MSS1:def_12;
let A be MSAlgebra over S2; ::_thesis: for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) )
let o1 be OperSymbol of S1; ::_thesis: for o2 being OperSymbol of S2 st o2 = g . o1 holds
( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) )
let o2 be OperSymbol of S2; ::_thesis: ( o2 = g . o1 implies ( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) ) )
assume A3: o2 = g . o1 ; ::_thesis: ( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) )
thus Args (o2,A) = product ( the Sorts of A * (the_arity_of o2)) by PRALG_2:3
.= product ( the Sorts of A * (f * (the_arity_of o1))) by A1, A3, PUA2MSS1:def_12
.= product (( the Sorts of A * f) * (the_arity_of o1)) by RELAT_1:36
.= product ( the Sorts of (A | (S1,f,g)) * (the_arity_of o1)) by A1, Def3
.= Args (o1,(A | (S1,f,g))) by PRALG_2:3 ; ::_thesis: Result (o1,(A | (S1,f,g))) = Result (o2,A)
dom g = the carrier' of S1 by A1, PUA2MSS1:def_12;
then the_result_sort_of o2 = ( the ResultSort of S2 * g) . o1 by A3, FUNCT_1:13
.= (f * the ResultSort of S1) . o1 by A1, PUA2MSS1:def_12
.= f . (the_result_sort_of o1) by FUNCT_2:15 ;
hence Result (o2,A) = the Sorts of A . (f . (the_result_sort_of o1)) by PRALG_2:3
.= ( the Sorts of A * f) . (the_result_sort_of o1) by A2, FUNCT_1:13
.= the Sorts of (A | (S1,f,g)) . (the_result_sort_of o1) by A1, Def3
.= Result (o1,(A | (S1,f,g))) by PRALG_2:3 ;
::_thesis: verum
end;
theorem Th25: :: INSTALG1:25
for S being non empty ManySortedSign
for A being MSAlgebra over S holds A | (S,(id the carrier of S),(id the carrier' of S)) = MSAlgebra(# the Sorts of A, the Charact of A #)
proof
let S be non empty ManySortedSign ; ::_thesis: for A being MSAlgebra over S holds A | (S,(id the carrier of S),(id the carrier' of S)) = MSAlgebra(# the Sorts of A, the Charact of A #)
let A be MSAlgebra over S; ::_thesis: A | (S,(id the carrier of S),(id the carrier' of S)) = MSAlgebra(# the Sorts of A, the Charact of A #)
set f = id the carrier of S;
set g = id the carrier' of S;
dom the Charact of A = the carrier' of S by PARTFUN1:def_2;
then A1: the Charact of MSAlgebra(# the Sorts of A, the Charact of A #) = the Charact of A * (id the carrier' of S) by RELAT_1:52;
dom the Sorts of A = the carrier of S by PARTFUN1:def_2;
then A2: the Sorts of MSAlgebra(# the Sorts of A, the Charact of A #) = the Sorts of A * (id the carrier of S) by RELAT_1:52;
id the carrier of S, id the carrier' of S form_morphism_between S,S by Th8;
hence A | (S,(id the carrier of S),(id the carrier' of S)) = MSAlgebra(# the Sorts of A, the Charact of A #) by A2, A1, Def3; ::_thesis: verum
end;
theorem :: INSTALG1:26
for S being non empty ManySortedSign
for A being MSAlgebra over S holds A | S = MSAlgebra(# the Sorts of A, the Charact of A #) by Th25;
theorem Th27: :: INSTALG1:27
for S1, S2, S3 being non empty ManySortedSign
for f1, g1 being Function st f1,g1 form_morphism_between S1,S2 holds
for f2, g2 being Function st f2,g2 form_morphism_between S2,S3 holds
for A being MSAlgebra over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1)
proof
let S1, S2, S3 be non empty ManySortedSign ; ::_thesis: for f1, g1 being Function st f1,g1 form_morphism_between S1,S2 holds
for f2, g2 being Function st f2,g2 form_morphism_between S2,S3 holds
for A being MSAlgebra over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1)
let f1, g1 be Function; ::_thesis: ( f1,g1 form_morphism_between S1,S2 implies for f2, g2 being Function st f2,g2 form_morphism_between S2,S3 holds
for A being MSAlgebra over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1) )
assume A1: f1,g1 form_morphism_between S1,S2 ; ::_thesis: for f2, g2 being Function st f2,g2 form_morphism_between S2,S3 holds
for A being MSAlgebra over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1)
let f2, g2 be Function; ::_thesis: ( f2,g2 form_morphism_between S2,S3 implies for A being MSAlgebra over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1) )
assume A2: f2,g2 form_morphism_between S2,S3 ; ::_thesis: for A being MSAlgebra over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1)
A3: f2 * f1,g2 * g1 form_morphism_between S1,S3 by A1, A2, PUA2MSS1:29;
let A be MSAlgebra over S3; ::_thesis: A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1)
A4: the Charact of ((A | (S2,f2,g2)) | (S1,f1,g1)) = the Charact of (A | (S2,f2,g2)) * g1 by A1, Def3
.= ( the Charact of A * g2) * g1 by A2, Def3
.= the Charact of A * (g2 * g1) by RELAT_1:36 ;
the Sorts of ((A | (S2,f2,g2)) | (S1,f1,g1)) = the Sorts of (A | (S2,f2,g2)) * f1 by A1, Def3
.= ( the Sorts of A * f2) * f1 by A2, Def3
.= the Sorts of A * (f2 * f1) by RELAT_1:36 ;
hence A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1) by A3, A4, Def3; ::_thesis: verum
end;
theorem :: INSTALG1:28
for S1 being non empty feasible ManySortedSign
for S2 being non empty Subsignature of S1
for S3 being non empty Subsignature of S2
for A being MSAlgebra over S1 holds A | S3 = (A | S2) | S3
proof
let S1 be non empty feasible ManySortedSign ; ::_thesis: for S2 being non empty Subsignature of S1
for S3 being non empty Subsignature of S2
for A being MSAlgebra over S1 holds A | S3 = (A | S2) | S3
let S2 be non empty Subsignature of S1; ::_thesis: for S3 being non empty Subsignature of S2
for A being MSAlgebra over S1 holds A | S3 = (A | S2) | S3
let S3 be non empty Subsignature of S2; ::_thesis: for A being MSAlgebra over S1 holds A | S3 = (A | S2) | S3
let A be MSAlgebra over S1; ::_thesis: A | S3 = (A | S2) | S3
set f1 = id the carrier of S2;
set g1 = id the carrier' of S2;
set f2 = id the carrier of S3;
set g2 = id the carrier' of S3;
rng (id the carrier of S3) = the carrier of S3 ;
then A1: (id the carrier of S2) * (id the carrier of S3) = id the carrier of S3 by Th10, RELAT_1:53;
rng (id the carrier' of S3) = the carrier' of S3 ;
then A2: (id the carrier' of S2) * (id the carrier' of S3) = id the carrier' of S3 by Th10, RELAT_1:53;
( id the carrier of S2, id the carrier' of S2 form_morphism_between S2,S1 & id the carrier of S3, id the carrier' of S3 form_morphism_between S3,S2 ) by Def2;
hence A | S3 = (A | S2) | S3 by A1, A2, Th27; ::_thesis: verum
end;
theorem Th29: :: INSTALG1:29
for S1, S2 being non empty ManySortedSign
for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
for A1, A2 being MSAlgebra over S2
for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g))
proof
let S1, S2 be non empty ManySortedSign ; ::_thesis: for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
for A1, A2 being MSAlgebra over S2
for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g))
let f be Function of the carrier of S1, the carrier of S2; ::_thesis: for g being Function st f,g form_morphism_between S1,S2 holds
for A1, A2 being MSAlgebra over S2
for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g))
let g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for A1, A2 being MSAlgebra over S2
for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g)) )
assume A1: f,g form_morphism_between S1,S2 ; ::_thesis: for A1, A2 being MSAlgebra over S2
for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g))
let A1, A2 be MSAlgebra over S2; ::_thesis: for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g))
let h be ManySortedFunction of the Sorts of A1, the Sorts of A2; ::_thesis: h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g))
set B1 = A1 | (S1,f,g);
set B2 = A2 | (S1,f,g);
let x be set ; :: according to PBOOLE:def_15 ::_thesis: ( not x in the carrier of S1 or (h * f) . x is Element of bool [:( the Sorts of (A1 | (S1,f,g)) . x),( the Sorts of (A2 | (S1,f,g)) . x):] )
assume x in the carrier of S1 ; ::_thesis: (h * f) . x is Element of bool [:( the Sorts of (A1 | (S1,f,g)) . x),( the Sorts of (A2 | (S1,f,g)) . x):]
then reconsider s = x as SortSymbol of S1 ;
reconsider fs = f . s as SortSymbol of S2 ;
A2: ( (h * f) . s = h . fs & the Sorts of A1 . fs = ( the Sorts of A1 * f) . s ) by FUNCT_2:15;
A3: the Sorts of A2 . fs = ( the Sorts of A2 * f) . s by FUNCT_2:15;
( the Sorts of A1 * f = the Sorts of (A1 | (S1,f,g)) & the Sorts of A2 * f = the Sorts of (A2 | (S1,f,g)) ) by A1, Def3;
hence (h * f) . x is Element of bool [:( the Sorts of (A1 | (S1,f,g)) . x),( the Sorts of (A2 | (S1,f,g)) . x):] by A2, A3; ::_thesis: verum
end;
theorem :: INSTALG1:30
for S1 being non empty ManySortedSign
for S2 being non empty Subsignature of S1
for A1, A2 being MSAlgebra over S1
for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2)
proof
let S1 be non empty ManySortedSign ; ::_thesis: for S2 being non empty Subsignature of S1
for A1, A2 being MSAlgebra over S1
for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2)
let S2 be non empty Subsignature of S1; ::_thesis: for A1, A2 being MSAlgebra over S1
for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2)
set f = id the carrier of S2;
set g = id the carrier' of S2;
let A1, A2 be MSAlgebra over S1; ::_thesis: for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2)
let h be ManySortedFunction of the Sorts of A1, the Sorts of A2; ::_thesis: h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2)
A1: id the carrier of S2, id the carrier' of S2 form_morphism_between S2,S1 by Def2;
then reconsider f = id the carrier of S2 as Function of the carrier of S2, the carrier of S1 by Th9;
h * f is ManySortedFunction of the Sorts of (A1 | (S2,f,(id the carrier' of S2))), the Sorts of (A2 | (S2,f,(id the carrier' of S2))) by A1, Th29;
hence h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2) by RELAT_1:65; ::_thesis: verum
end;
theorem Th31: :: INSTALG1:31
for S1, S2 being non empty ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
for A being MSAlgebra over S2 holds (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g))
proof
let S1, S2 be non empty ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
for A being MSAlgebra over S2 holds (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g))
let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for A being MSAlgebra over S2 holds (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g)) )
assume A1: f,g form_morphism_between S1,S2 ; ::_thesis: for A being MSAlgebra over S2 holds (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g))
( dom f = the carrier of S1 & rng f c= the carrier of S2 ) by A1, PUA2MSS1:def_12;
then reconsider f = f as Function of the carrier of S1, the carrier of S2 by FUNCT_2:def_1, RELSET_1:4;
let A be MSAlgebra over S2; ::_thesis: (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g))
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S1_holds_
((id_the_Sorts_of_A)_*_f)_._i_=_(id_the_Sorts_of_(A_|_(S1,f,g)))_._i
let i be set ; ::_thesis: ( i in the carrier of S1 implies ((id the Sorts of A) * f) . i = (id the Sorts of (A | (S1,f,g))) . i )
assume i in the carrier of S1 ; ::_thesis: ((id the Sorts of A) * f) . i = (id the Sorts of (A | (S1,f,g))) . i
then reconsider s = i as SortSymbol of S1 ;
thus ((id the Sorts of A) * f) . i = (id the Sorts of A) . (f . s) by FUNCT_2:15
.= id ( the Sorts of A . (f . s)) by MSUALG_3:def_1
.= id (( the Sorts of A * f) . s) by FUNCT_2:15
.= id ( the Sorts of (A | (S1,f,g)) . s) by A1, Def3
.= (id the Sorts of (A | (S1,f,g))) . i by MSUALG_3:def_1 ; ::_thesis: verum
end;
hence (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g)) by PBOOLE:3; ::_thesis: verum
end;
theorem :: INSTALG1:32
for S1 being non empty ManySortedSign
for S2 being non empty Subsignature of S1
for A being MSAlgebra over S1 holds (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2)
proof
let S1 be non empty ManySortedSign ; ::_thesis: for S2 being non empty Subsignature of S1
for A being MSAlgebra over S1 holds (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2)
let S2 be non empty Subsignature of S1; ::_thesis: for A being MSAlgebra over S1 holds (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2)
set f = id the carrier of S2;
set g = id the carrier' of S2;
let A be MSAlgebra over S1; ::_thesis: (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2)
id the carrier of S2, id the carrier' of S2 form_morphism_between S2,S1 by Def2;
then (id the Sorts of A) * (id the carrier of S2) = id the Sorts of (A | S2) by Th31;
hence (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2) by RELAT_1:65; ::_thesis: verum
end;
theorem Th33: :: INSTALG1:33
for S1, S2 being non empty non void ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
for A, B being MSAlgebra over S2
for h2 being ManySortedFunction of A,B
for h1 being ManySortedFunction of (A | (S1,f,g)),(B | (S1,f,g)) st h1 = h2 * f holds
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A) <> {} & Args (o2,B) <> {} holds
for x2 being Element of Args (o2,A)
for x1 being Element of Args (o1,(A | (S1,f,g))) st x2 = x1 holds
h1 # x1 = h2 # x2
proof
let S1, S2 be non empty non void ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
for A, B being MSAlgebra over S2
for h2 being ManySortedFunction of A,B
for h1 being ManySortedFunction of (A | (S1,f,g)),(B | (S1,f,g)) st h1 = h2 * f holds
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A) <> {} & Args (o2,B) <> {} holds
for x2 being Element of Args (o2,A)
for x1 being Element of Args (o1,(A | (S1,f,g))) st x2 = x1 holds
h1 # x1 = h2 # x2
let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for A, B being MSAlgebra over S2
for h2 being ManySortedFunction of A,B
for h1 being ManySortedFunction of (A | (S1,f,g)),(B | (S1,f,g)) st h1 = h2 * f holds
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A) <> {} & Args (o2,B) <> {} holds
for x2 being Element of Args (o2,A)
for x1 being Element of Args (o1,(A | (S1,f,g))) st x2 = x1 holds
h1 # x1 = h2 # x2 )
assume A1: f,g form_morphism_between S1,S2 ; ::_thesis: for A, B being MSAlgebra over S2
for h2 being ManySortedFunction of A,B
for h1 being ManySortedFunction of (A | (S1,f,g)),(B | (S1,f,g)) st h1 = h2 * f holds
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A) <> {} & Args (o2,B) <> {} holds
for x2 being Element of Args (o2,A)
for x1 being Element of Args (o1,(A | (S1,f,g))) st x2 = x1 holds
h1 # x1 = h2 # x2
let A2, B2 be MSAlgebra over S2; ::_thesis: for h2 being ManySortedFunction of A2,B2
for h1 being ManySortedFunction of (A2 | (S1,f,g)),(B2 | (S1,f,g)) st h1 = h2 * f holds
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A2) <> {} & Args (o2,B2) <> {} holds
for x2 being Element of Args (o2,A2)
for x1 being Element of Args (o1,(A2 | (S1,f,g))) st x2 = x1 holds
h1 # x1 = h2 # x2
set A1 = A2 | (S1,f,g);
set B1 = B2 | (S1,f,g);
let h2 be ManySortedFunction of A2,B2; ::_thesis: for h1 being ManySortedFunction of (A2 | (S1,f,g)),(B2 | (S1,f,g)) st h1 = h2 * f holds
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A2) <> {} & Args (o2,B2) <> {} holds
for x2 being Element of Args (o2,A2)
for x1 being Element of Args (o1,(A2 | (S1,f,g))) st x2 = x1 holds
h1 # x1 = h2 # x2
let h1 be ManySortedFunction of (A2 | (S1,f,g)),(B2 | (S1,f,g)); ::_thesis: ( h1 = h2 * f implies for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A2) <> {} & Args (o2,B2) <> {} holds
for x2 being Element of Args (o2,A2)
for x1 being Element of Args (o1,(A2 | (S1,f,g))) st x2 = x1 holds
h1 # x1 = h2 # x2 )
assume A2: h1 = h2 * f ; ::_thesis: for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A2) <> {} & Args (o2,B2) <> {} holds
for x2 being Element of Args (o2,A2)
for x1 being Element of Args (o1,(A2 | (S1,f,g))) st x2 = x1 holds
h1 # x1 = h2 # x2
let o1 be OperSymbol of S1; ::_thesis: for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A2) <> {} & Args (o2,B2) <> {} holds
for x2 being Element of Args (o2,A2)
for x1 being Element of Args (o1,(A2 | (S1,f,g))) st x2 = x1 holds
h1 # x1 = h2 # x2
let o2 be OperSymbol of S2; ::_thesis: ( o2 = g . o1 & Args (o2,A2) <> {} & Args (o2,B2) <> {} implies for x2 being Element of Args (o2,A2)
for x1 being Element of Args (o1,(A2 | (S1,f,g))) st x2 = x1 holds
h1 # x1 = h2 # x2 )
assume A3: o2 = g . o1 ; ::_thesis: ( not Args (o2,A2) <> {} or not Args (o2,B2) <> {} or for x2 being Element of Args (o2,A2)
for x1 being Element of Args (o1,(A2 | (S1,f,g))) st x2 = x1 holds
h1 # x1 = h2 # x2 )
assume that
A4: Args (o2,A2) <> {} and
A5: Args (o2,B2) <> {} ; ::_thesis: for x2 being Element of Args (o2,A2)
for x1 being Element of Args (o1,(A2 | (S1,f,g))) st x2 = x1 holds
h1 # x1 = h2 # x2
let x2 be Element of Args (o2,A2); ::_thesis: for x1 being Element of Args (o1,(A2 | (S1,f,g))) st x2 = x1 holds
h1 # x1 = h2 # x2
let x1 be Element of Args (o1,(A2 | (S1,f,g))); ::_thesis: ( x2 = x1 implies h1 # x1 = h2 # x2 )
assume A6: x2 = x1 ; ::_thesis: h1 # x1 = h2 # x2
then reconsider f1 = x1, f2 = x2, g2 = h2 # x2 as Function by A4, A5, MSUALG_6:1;
A7: Args (o2,A2) = Args (o1,(A2 | (S1,f,g))) by A1, A3, Th24;
then A8: dom f1 = dom (the_arity_of o1) by A4, MSUALG_3:6;
A9: dom f2 = dom (the_arity_of o2) by A4, MSUALG_3:6;
A10: now__::_thesis:_for_i_being_Nat_st_i_in_dom_f1_holds_
g2_._i_=_(h1_._((the_arity_of_o1)_/._i))_._(f1_._i)
let i be Nat; ::_thesis: ( i in dom f1 implies g2 . i = (h1 . ((the_arity_of o1) /. i)) . (f1 . i) )
assume A11: i in dom f1 ; ::_thesis: g2 . i = (h1 . ((the_arity_of o1) /. i)) . (f1 . i)
dom f = the carrier of S1 by A1, PUA2MSS1:def_12;
then h1 . ((the_arity_of o1) /. i) = h2 . (f . ((the_arity_of o1) /. i)) by A2, FUNCT_1:13
.= h2 . (f . ((the_arity_of o1) . i)) by A8, A11, PARTFUN1:def_6
.= h2 . ((f * (the_arity_of o1)) . i) by A8, A11, FUNCT_1:13
.= h2 . ((the_arity_of o2) . i) by A1, A3, PUA2MSS1:def_12
.= h2 . ((the_arity_of o2) /. i) by A6, A9, A11, PARTFUN1:def_6 ;
hence g2 . i = (h1 . ((the_arity_of o1) /. i)) . (f1 . i) by A4, A5, A6, A11, MSUALG_3:24; ::_thesis: verum
end;
Args (o2,B2) = Args (o1,(B2 | (S1,f,g))) by A1, A3, Th24;
hence h1 # x1 = h2 # x2 by A4, A5, A7, A10, MSUALG_3:24; ::_thesis: verum
end;
theorem Th34: :: INSTALG1:34
for S, S9 being non empty non void ManySortedSign
for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st
( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) )
proof
let S, S9 be non empty non void ManySortedSign ; ::_thesis: for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st
( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) )
let A1, A2 be MSAlgebra over S; ::_thesis: ( the Sorts of A1 is_transformable_to the Sorts of A2 implies for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st
( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) ) )
assume A1: the Sorts of A1 is_transformable_to the Sorts of A2 ; ::_thesis: for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st
( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) )
let h be ManySortedFunction of A1,A2; ::_thesis: ( h is_homomorphism A1,A2 implies for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st
( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) ) )
assume A2: h is_homomorphism A1,A2 ; ::_thesis: for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st
( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) )
let f be Function of the carrier of S9, the carrier of S; ::_thesis: for g being Function st f,g form_morphism_between S9,S holds
ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st
( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) )
let g be Function; ::_thesis: ( f,g form_morphism_between S9,S implies ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st
( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) ) )
assume A3: f,g form_morphism_between S9,S ; ::_thesis: ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st
( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) )
A4: ( dom g = the carrier' of S9 & rng g c= the carrier' of S ) by A3, PUA2MSS1:def_12;
set B1 = A1 | (S9,f,g);
set B2 = A2 | (S9,f,g);
reconsider g = g as Function of the carrier' of S9, the carrier' of S by A4, FUNCT_2:def_1, RELSET_1:4;
A5: f * the ResultSort of S9 = the ResultSort of S * g by A3, PUA2MSS1:def_12;
reconsider h9 = h * f as ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) by A3, Th29;
take h9 ; ::_thesis: ( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) )
thus h9 = h * f ; ::_thesis: h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g)
let o be OperSymbol of S9; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,(A1 | (S9,f,g))) = {} or for b1 being Element of Args (o,(A1 | (S9,f,g))) holds (h9 . (the_result_sort_of o)) . ((Den (o,(A1 | (S9,f,g)))) . b1) = (Den (o,(A2 | (S9,f,g)))) . (h9 # b1) )
set go = g . o;
assume A6: Args (o,(A1 | (S9,f,g))) <> {} ; ::_thesis: for b1 being Element of Args (o,(A1 | (S9,f,g))) holds (h9 . (the_result_sort_of o)) . ((Den (o,(A1 | (S9,f,g)))) . b1) = (Den (o,(A2 | (S9,f,g)))) . (h9 # b1)
let x be Element of Args (o,(A1 | (S9,f,g))); ::_thesis: (h9 . (the_result_sort_of o)) . ((Den (o,(A1 | (S9,f,g)))) . x) = (Den (o,(A2 | (S9,f,g)))) . (h9 # x)
reconsider y = x as Element of Args ((g . o),A1) by A3, Th24;
A7: h9 . (the_result_sort_of o) = h . (f . (the_result_sort_of o)) by FUNCT_2:15
.= h . (( the ResultSort of S * g) . o) by A5, FUNCT_2:15
.= h . (the_result_sort_of (g . o)) by FUNCT_2:15 ;
A8: ( Den (o,(A1 | (S9,f,g))) = Den ((g . o),A1) & Den (o,(A2 | (S9,f,g))) = Den ((g . o),A2) ) by A3, Th23;
A9: Args (o,(A1 | (S9,f,g))) = Args ((g . o),A1) by A3, Th24;
A10: Args (o,(A2 | (S9,f,g))) = Args ((g . o),A2) by A3, Th24;
then Args (o,(A2 | (S9,f,g))) <> {} by A1, A6, A9, Th2;
then h9 # x = h # y by A3, A6, A9, A10, Th33;
hence (h9 . (the_result_sort_of o)) . ((Den (o,(A1 | (S9,f,g)))) . x) = (Den (o,(A2 | (S9,f,g)))) . (h9 # x) by A2, A6, A9, A8, A7, MSUALG_3:def_7; ::_thesis: verum
end;
theorem :: INSTALG1:35
for S being non void feasible ManySortedSign
for S9 being non void Subsignature of S
for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st
( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 )
proof
let S be non void feasible ManySortedSign ; ::_thesis: for S9 being non void Subsignature of S
for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st
( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 )
let S9 be non void Subsignature of S; ::_thesis: for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st
( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 )
let A1, A2 be MSAlgebra over S; ::_thesis: ( the Sorts of A1 is_transformable_to the Sorts of A2 implies for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st
( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 ) )
assume A1: the Sorts of A1 is_transformable_to the Sorts of A2 ; ::_thesis: for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st
( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 )
set f = id the carrier of S9;
set g = id the carrier' of S9;
A2: id the carrier of S9, id the carrier' of S9 form_morphism_between S9,S by Def2;
then reconsider f = id the carrier of S9 as Function of the carrier of S9, the carrier of S by Th9;
let h be ManySortedFunction of A1,A2; ::_thesis: ( h is_homomorphism A1,A2 implies ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st
( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 ) )
assume h is_homomorphism A1,A2 ; ::_thesis: ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st
( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 )
then consider h9 being ManySortedFunction of (A1 | (S9,f,(id the carrier' of S9))),(A2 | (S9,f,(id the carrier' of S9))) such that
A3: h9 = h * f and
A4: h9 is_homomorphism A1 | (S9,f,(id the carrier' of S9)),A2 | (S9,f,(id the carrier' of S9)) by A1, A2, Th34;
consider k being ManySortedFunction of (A1 | S9),(A2 | S9) such that
A5: k = h9 and
k is_homomorphism A1 | S9,A2 | S9 by A4;
take k ; ::_thesis: ( k = h | the carrier of S9 & k is_homomorphism A1 | S9,A2 | S9 )
thus ( k = h | the carrier of S9 & k is_homomorphism A1 | S9,A2 | S9 ) by A3, A4, A5, RELAT_1:65; ::_thesis: verum
end;
theorem Th36: :: INSTALG1:36
for S, S9 being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9
for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2
proof
let S, S9 be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9
for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2
let A be non-empty MSAlgebra over S; ::_thesis: for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9
for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2
let f be Function of the carrier of S9, the carrier of S; ::_thesis: for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9
for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2
let g be Function; ::_thesis: ( f,g form_morphism_between S9,S implies for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9
for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2 )
assume A1: f,g form_morphism_between S9,S ; ::_thesis: for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9
for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2
A2: ( dom g = the carrier' of S9 & rng g c= the carrier' of S ) by A1, PUA2MSS1:def_12;
let B be non-empty MSAlgebra over S9; ::_thesis: ( B = A | (S9,f,g) implies for s1, s2 being SortSymbol of S9
for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2 )
assume A3: B = A | (S9,f,g) ; ::_thesis: for s1, s2 being SortSymbol of S9
for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2
reconsider g = g as Function of the carrier' of S9, the carrier' of S by A2, FUNCT_2:def_1, RELSET_1:4;
let s1, s2 be SortSymbol of S9; ::_thesis: for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2
let t be Function; ::_thesis: ( t is_e.translation_of B,s1,s2 implies t is_e.translation_of A,f . s1,f . s2 )
given o being OperSymbol of S9 such that A4: the_result_sort_of o = s2 and
A5: ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st
( a in Args (o,B) & t = transl (o,i,a,B) ) ) ; :: according to MSUALG_6:def_5 ::_thesis: t is_e.translation_of A,f . s1,f . s2
A6: f * (the_arity_of o) = the_arity_of (g . o) by A1, PUA2MSS1:def_12;
take g . o ; :: according to MSUALG_6:def_5 ::_thesis: ( the_result_sort_of (g . o) = f . s2 & ex b1 being Element of NAT st
( b1 in dom (the_arity_of (g . o)) & (the_arity_of (g . o)) /. b1 = f . s1 & ex b2 being set st
( b2 in Args ((g . o),A) & t = transl ((g . o),b1,b2,A) ) ) )
f * the ResultSort of S9 = the ResultSort of S * g by A1, PUA2MSS1:def_12;
hence the_result_sort_of (g . o) = (f * the ResultSort of S9) . o by FUNCT_2:15
.= f . s2 by A4, FUNCT_2:15 ;
::_thesis: ex b1 being Element of NAT st
( b1 in dom (the_arity_of (g . o)) & (the_arity_of (g . o)) /. b1 = f . s1 & ex b2 being set st
( b2 in Args ((g . o),A) & t = transl ((g . o),b1,b2,A) ) )
consider i being Element of NAT , a being Function such that
A7: i in dom (the_arity_of o) and
A8: (the_arity_of o) /. i = s1 and
A9: a in Args (o,B) and
A10: t = transl (o,i,a,B) by A5;
take i ; ::_thesis: ( i in dom (the_arity_of (g . o)) & (the_arity_of (g . o)) /. i = f . s1 & ex b1 being set st
( b1 in Args ((g . o),A) & t = transl ((g . o),i,b1,A) ) )
( rng (the_arity_of o) c= the carrier of S9 & dom f = the carrier of S9 ) by FINSEQ_1:def_4, FUNCT_2:def_1;
hence i in dom (the_arity_of (g . o)) by A7, A6, RELAT_1:27; ::_thesis: ( (the_arity_of (g . o)) /. i = f . s1 & ex b1 being set st
( b1 in Args ((g . o),A) & t = transl ((g . o),i,b1,A) ) )
hence A11: (the_arity_of (g . o)) /. i = (the_arity_of (g . o)) . i by PARTFUN1:def_6
.= f . ((the_arity_of o) . i) by A7, A6, FUNCT_1:13
.= f . s1 by A7, A8, PARTFUN1:def_6 ;
::_thesis: ex b1 being set st
( b1 in Args ((g . o),A) & t = transl ((g . o),i,b1,A) )
then A12: dom (transl ((g . o),i,a,A)) = the Sorts of A . (f . s1) by MSUALG_6:def_4;
A13: the Sorts of B = the Sorts of A * f by A1, A3, Def3;
then A14: the Sorts of B . s1 = the Sorts of A . (f . s1) by FUNCT_2:15;
A15: now__::_thesis:_for_x_being_set_st_x_in_the_Sorts_of_B_._s1_holds_
t_._x_=_(transl_((g_._o),i,a,A))_._x
let x be set ; ::_thesis: ( x in the Sorts of B . s1 implies t . x = (transl ((g . o),i,a,A)) . x )
assume x in the Sorts of B . s1 ; ::_thesis: t . x = (transl ((g . o),i,a,A)) . x
then ( t . x = (Den (o,B)) . (a +* (i,x)) & (transl ((g . o),i,a,A)) . x = (Den ((g . o),A)) . (a +* (i,x)) ) by A8, A10, A11, A14, MSUALG_6:def_4;
hence t . x = (transl ((g . o),i,a,A)) . x by A1, A3, Th23; ::_thesis: verum
end;
take a ; ::_thesis: ( a in Args ((g . o),A) & t = transl ((g . o),i,a,A) )
thus a in Args ((g . o),A) by A1, A3, A9, Th24; ::_thesis: t = transl ((g . o),i,a,A)
dom t = the Sorts of B . s1 by A8, A10, MSUALG_6:def_4;
hence t = transl ((g . o),i,a,A) by A12, A13, A15, FUNCT_1:2, FUNCT_2:15; ::_thesis: verum
end;
Lm1: for S, S9 being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) )
proof
let S, S9 be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) )
let A be non-empty MSAlgebra over S; ::_thesis: for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) )
let f be Function of the carrier of S9, the carrier of S; ::_thesis: for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) )
let g be Function; ::_thesis: ( f,g form_morphism_between S9,S implies for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) )
assume A1: f,g form_morphism_between S9,S ; ::_thesis: for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) )
defpred S1[ set , SortSymbol of S9, SortSymbol of S9] means ( TranslationRel S reduces f . $2,f . $3 & $1 is Translation of A,f . $2,f . $3 );
let B be non-empty MSAlgebra over S9; ::_thesis: ( B = A | (S9,f,g) implies for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) )
assume A2: B = A | (S9,f,g) ; ::_thesis: for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) )
A3: for s1, s2, s3 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
for t being Translation of B,s1,s2 st S1[t,s1,s2] holds
for h being Function st h is_e.translation_of B,s2,s3 holds
S1[h * t,s1,s3]
proof
let s1, s2, s3 be SortSymbol of S9; ::_thesis: ( TranslationRel S9 reduces s1,s2 implies for t being Translation of B,s1,s2 st S1[t,s1,s2] holds
for h being Function st h is_e.translation_of B,s2,s3 holds
S1[h * t,s1,s3] )
assume TranslationRel S9 reduces s1,s2 ; ::_thesis: for t being Translation of B,s1,s2 st S1[t,s1,s2] holds
for h being Function st h is_e.translation_of B,s2,s3 holds
S1[h * t,s1,s3]
let t be Translation of B,s1,s2; ::_thesis: ( S1[t,s1,s2] implies for h being Function st h is_e.translation_of B,s2,s3 holds
S1[h * t,s1,s3] )
assume A4: S1[t,s1,s2] ; ::_thesis: for h being Function st h is_e.translation_of B,s2,s3 holds
S1[h * t,s1,s3]
let h be Function; ::_thesis: ( h is_e.translation_of B,s2,s3 implies S1[h * t,s1,s3] )
assume A5: h is_e.translation_of B,s2,s3 ; ::_thesis: S1[h * t,s1,s3]
then [(f . s2),(f . s3)] in TranslationRel S by A1, A2, Th36, MSUALG_6:12;
then A6: TranslationRel S reduces f . s2,f . s3 by REWRITE1:15;
h is_e.translation_of A,f . s2,f . s3 by A1, A2, A5, Th36;
hence S1[h * t,s1,s3] by A4, A6, MSUALG_6:19, REWRITE1:16; ::_thesis: verum
end;
let s1, s2 be SortSymbol of S9; ::_thesis: ( TranslationRel S9 reduces s1,s2 implies ( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) )
assume A7: TranslationRel S9 reduces s1,s2 ; ::_thesis: ( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) )
A8: for s being SortSymbol of S9 holds S1[ id ( the Sorts of B . s),s,s]
proof
let s be SortSymbol of S9; ::_thesis: S1[ id ( the Sorts of B . s),s,s]
thus TranslationRel S reduces f . s,f . s by REWRITE1:12; ::_thesis: id ( the Sorts of B . s) is Translation of A,f . s,f . s
the Sorts of B = the Sorts of A * f by A1, A2, Def3;
then the Sorts of B . s = the Sorts of A . (f . s) by FUNCT_2:15;
hence id ( the Sorts of B . s) is Translation of A,f . s,f . s by MSUALG_6:16; ::_thesis: verum
end;
for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
for t being Translation of B,s1,s2 holds S1[t,s1,s2] from MSUALG_6:sch_1(A8, A3);
hence ( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) by A7; ::_thesis: verum
end;
theorem :: INSTALG1:37
for S, S9 being non empty non void ManySortedSign
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
TranslationRel S reduces f . s1,f . s2
proof
let S, S9 be non empty non void ManySortedSign ; ::_thesis: for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
TranslationRel S reduces f . s1,f . s2
set A = the non-empty MSAlgebra over S;
let f be Function of the carrier of S9, the carrier of S; ::_thesis: for g being Function st f,g form_morphism_between S9,S holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
TranslationRel S reduces f . s1,f . s2
let g be Function; ::_thesis: ( f,g form_morphism_between S9,S implies for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
TranslationRel S reduces f . s1,f . s2 )
assume A1: f,g form_morphism_between S9,S ; ::_thesis: for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
TranslationRel S reduces f . s1,f . s2
then the non-empty MSAlgebra over S | (S9,f,g) is non-empty MSAlgebra over S9 by Th22;
hence for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
TranslationRel S reduces f . s1,f . s2 by A1, Lm1; ::_thesis: verum
end;
theorem :: INSTALG1:38
for S, S9 being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 by Lm1;
begin
scheme :: INSTALG1:sch 1
GenFuncEx{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), F3() -> V16() ManySortedSet of the carrier of F1(), F4( set , set ) -> set } :
ex h being ManySortedFunction of (FreeMSA F3()),F2() st
( h is_homomorphism FreeMSA F3(),F2() & ( for s being SortSymbol of F1()
for x being Element of F3() . s holds (h . s) . (root-tree [x,s]) = F4(x,s) ) )
provided
A1: for s being SortSymbol of F1()
for x being Element of F3() . s holds F4(x,s) in the Sorts of F2() . s
proof
defpred S1[ set , set ] means ex f being Function of ((FreeGen F3()) . $1),( the Sorts of F2() . $1) st
( $2 = f & ( for x being Element of F3() . $1 holds f . (root-tree [x,$1]) = F4(x,$1) ) );
A2: for a being set st a in the carrier of F1() holds
ex y being set st S1[a,y]
proof
let a be set ; ::_thesis: ( a in the carrier of F1() implies ex y being set st S1[a,y] )
assume a in the carrier of F1() ; ::_thesis: ex y being set st S1[a,y]
then reconsider s = a as SortSymbol of F1() ;
defpred S2[ set , set ] means ex x being Element of F3() . s st
( $1 = root-tree [x,s] & $2 = F4(x,s) );
A3: (FreeGen F3()) . s = FreeGen (s,F3()) by MSAFREE:def_16;
A4: for y being set st y in (FreeGen F3()) . s holds
ex z being set st
( z in the Sorts of F2() . s & S2[y,z] )
proof
let y be set ; ::_thesis: ( y in (FreeGen F3()) . s implies ex z being set st
( z in the Sorts of F2() . s & S2[y,z] ) )
assume y in (FreeGen F3()) . s ; ::_thesis: ex z being set st
( z in the Sorts of F2() . s & S2[y,z] )
then consider a being set such that
A5: a in F3() . s and
A6: y = root-tree [a,s] by A3, MSAFREE:def_15;
reconsider a = a as Element of F3() . s by A5;
take z = F4(a,s); ::_thesis: ( z in the Sorts of F2() . s & S2[y,z] )
thus z in the Sorts of F2() . s by A1; ::_thesis: S2[y,z]
take a ; ::_thesis: ( y = root-tree [a,s] & z = F4(a,s) )
thus ( y = root-tree [a,s] & z = F4(a,s) ) by A6; ::_thesis: verum
end;
consider f being Function such that
A7: ( dom f = (FreeGen F3()) . s & rng f c= the Sorts of F2() . s ) and
A8: for y being set st y in (FreeGen F3()) . s holds
S2[y,f . y] from FUNCT_1:sch_5(A4);
reconsider f = f as Function of ((FreeGen F3()) . a),( the Sorts of F2() . a) by A7, FUNCT_2:2;
take y = f; ::_thesis: S1[a,y]
take f ; ::_thesis: ( y = f & ( for x being Element of F3() . a holds f . (root-tree [x,a]) = F4(x,a) ) )
thus y = f ; ::_thesis: for x being Element of F3() . a holds f . (root-tree [x,a]) = F4(x,a)
let x be Element of F3() . a; ::_thesis: f . (root-tree [x,a]) = F4(x,a)
root-tree [x,s] in (FreeGen F3()) . s by A3, MSAFREE:def_15;
then consider z being Element of F3() . s such that
A9: root-tree [x,s] = root-tree [z,s] and
A10: f . (root-tree [x,s]) = F4(z,s) by A8;
[x,s] = [z,s] by A9, TREES_4:4;
hence f . (root-tree [x,a]) = F4(x,a) by A10, XTUPLE_0:1; ::_thesis: verum
end;
consider h being Function such that
A11: dom h = the carrier of F1() and
A12: for a being set st a in the carrier of F1() holds
S1[a,h . a] from CLASSES1:sch_1(A2);
reconsider h = h as ManySortedSet of the carrier of F1() by A11, PARTFUN1:def_2, RELAT_1:def_18;
h is ManySortedFunction of FreeGen F3(), the Sorts of F2()
proof
let a be set ; :: according to PBOOLE:def_15 ::_thesis: ( not a in the carrier of F1() or h . a is Element of bool [:((FreeGen F3()) . a),( the Sorts of F2() . a):] )
assume a in the carrier of F1() ; ::_thesis: h . a is Element of bool [:((FreeGen F3()) . a),( the Sorts of F2() . a):]
then ex f being Function of ((FreeGen F3()) . a),( the Sorts of F2() . a) st
( h . a = f & ( for x being Element of F3() . a holds f . (root-tree [x,a]) = F4(x,a) ) ) by A12;
hence h . a is Element of bool [:((FreeGen F3()) . a),( the Sorts of F2() . a):] ; ::_thesis: verum
end;
then reconsider h = h as ManySortedFunction of FreeGen F3(), the Sorts of F2() ;
consider H being ManySortedFunction of (FreeMSA F3()),F2() such that
A13: H is_homomorphism FreeMSA F3(),F2() and
A14: H || (FreeGen F3()) = h by MSAFREE:def_5;
take H ; ::_thesis: ( H is_homomorphism FreeMSA F3(),F2() & ( for s being SortSymbol of F1()
for x being Element of F3() . s holds (H . s) . (root-tree [x,s]) = F4(x,s) ) )
thus H is_homomorphism FreeMSA F3(),F2() by A13; ::_thesis: for s being SortSymbol of F1()
for x being Element of F3() . s holds (H . s) . (root-tree [x,s]) = F4(x,s)
let s be SortSymbol of F1(); ::_thesis: for x being Element of F3() . s holds (H . s) . (root-tree [x,s]) = F4(x,s)
let x be Element of F3() . s; ::_thesis: (H . s) . (root-tree [x,s]) = F4(x,s)
A15: ex f being Function of ((FreeGen F3()) . s),( the Sorts of F2() . s) st
( h . s = f & ( for x being Element of F3() . s holds f . (root-tree [x,s]) = F4(x,s) ) ) by A12;
reconsider t = root-tree [x,s] as Term of F1(),F3() by MSATERM:4;
(FreeGen F3()) . s = FreeGen (s,F3()) by MSAFREE:def_16;
then A16: t in (FreeGen F3()) . s by MSAFREE:def_15;
h . s = (H . s) | ((FreeGen F3()) . s) by A14, MSAFREE:def_1;
then (H . s) . (root-tree [x,s]) = (h . s) . (root-tree [x,s]) by A16, FUNCT_1:49;
hence (H . s) . (root-tree [x,s]) = F4(x,s) by A15; ::_thesis: verum
end;
theorem Th39: :: INSTALG1:39
for I being set
for A, B being ManySortedSet of I
for C being ManySortedSubset of A
for F being ManySortedFunction of A,B
for i being set st i in I holds
for f, g being Function st f = F . i & g = (F || C) . i holds
for x being set st x in C . i holds
g . x = f . x
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I
for C being ManySortedSubset of A
for F being ManySortedFunction of A,B
for i being set st i in I holds
for f, g being Function st f = F . i & g = (F || C) . i holds
for x being set st x in C . i holds
g . x = f . x
let A, B be ManySortedSet of I; ::_thesis: for C being ManySortedSubset of A
for F being ManySortedFunction of A,B
for i being set st i in I holds
for f, g being Function st f = F . i & g = (F || C) . i holds
for x being set st x in C . i holds
g . x = f . x
let C be ManySortedSubset of A; ::_thesis: for F being ManySortedFunction of A,B
for i being set st i in I holds
for f, g being Function st f = F . i & g = (F || C) . i holds
for x being set st x in C . i holds
g . x = f . x
let F be ManySortedFunction of A,B; ::_thesis: for i being set st i in I holds
for f, g being Function st f = F . i & g = (F || C) . i holds
for x being set st x in C . i holds
g . x = f . x
let i be set ; ::_thesis: ( i in I implies for f, g being Function st f = F . i & g = (F || C) . i holds
for x being set st x in C . i holds
g . x = f . x )
assume A1: i in I ; ::_thesis: for f, g being Function st f = F . i & g = (F || C) . i holds
for x being set st x in C . i holds
g . x = f . x
then reconsider Fi = F . i as Function of (A . i),(B . i) by PBOOLE:def_15;
let f, g be Function; ::_thesis: ( f = F . i & g = (F || C) . i implies for x being set st x in C . i holds
g . x = f . x )
assume that
A2: f = F . i and
A3: g = (F || C) . i ; ::_thesis: for x being set st x in C . i holds
g . x = f . x
let x be set ; ::_thesis: ( x in C . i implies g . x = f . x )
g = Fi | (C . i) by A1, A3, MSAFREE:def_1;
hence ( x in C . i implies g . x = f . x ) by A2, FUNCT_1:49; ::_thesis: verum
end;
registration
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
cluster FreeGen X -> V16() ;
coherence
FreeGen X is non-empty ;
end;
definition
let S1, S2 be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S2;
let f be Function of the carrier of S1, the carrier of S2;
let g be Function;
assume B1: f,g form_morphism_between S1,S2 ;
func hom (f,g,X,S1,S2) -> ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) means :Def5: :: INSTALG1:def 5
( it is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (it . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) );
existence
ex b1 being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) st
( b1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (b1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) )
proof
set A = (FreeMSA X) | (S1,f,g);
the Sorts of ((FreeMSA X) | (S1,f,g)) = the Sorts of (FreeMSA X) * f by B1, Def3;
then reconsider A = (FreeMSA X) | (S1,f,g) as non-empty MSAlgebra over S1 by MSUALG_1:def_3;
deffunc H1( set , set ) -> set = root-tree [$1,(f . $2)];
A1: now__::_thesis:_for_s_being_SortSymbol_of_S1
for_x_being_Element_of_(X_*_f)_._s_holds_H1(x,s)_in_the_Sorts_of_A_._s
let s be SortSymbol of S1; ::_thesis: for x being Element of (X * f) . s holds H1(x,s) in the Sorts of A . s
let x be Element of (X * f) . s; ::_thesis: H1(x,s) in the Sorts of A . s
reconsider fs = f . s as SortSymbol of S2 ;
reconsider y = x as Element of X . fs by FUNCT_2:15;
reconsider t = root-tree [y,fs] as Term of S2,X by MSATERM:4;
the_sort_of t = fs by MSATERM:14;
then t in FreeSort (X,fs) by MSATERM:def_5;
then A2: t in (FreeSort X) . fs by MSAFREE:def_11;
( FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) & the Sorts of A = the Sorts of (FreeMSA X) * f ) by B1, Def3, MSAFREE:def_14;
hence H1(x,s) in the Sorts of A . s by A2, FUNCT_2:15; ::_thesis: verum
end;
consider H being ManySortedFunction of (FreeMSA (X * f)),A such that
A3: ( H is_homomorphism FreeMSA (X * f),A & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (H . s) . (root-tree [x,s]) = H1(x,s) ) ) from INSTALG1:sch_1(A1);
reconsider G = H as ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) ;
take G ; ::_thesis: ( G is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (G . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) )
thus ( G is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (G . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) ) by A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) st b1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (b1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) & b2 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (b2 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) holds
b1 = b2
proof
reconsider A1 = (FreeMSA X) | (S1,f,g) as non-empty MSAlgebra over S1 by B1, Th22;
let G1, G2 be ManySortedFunction of the Sorts of (FreeMSA (X * f)), the Sorts of ((FreeMSA X) | (S1,f,g)); ::_thesis: ( G1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (G1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) & G2 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (G2 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) implies G1 = G2 )
assume that
A4: G1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) and
A5: for s being SortSymbol of S1
for x being Element of (X * f) . s holds (G1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] and
A6: G2 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) and
A7: for s being SortSymbol of S1
for x being Element of (X * f) . s holds (G2 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ; ::_thesis: G1 = G2
set H1 = G1;
set H2 = G2;
A8: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_S1_holds_
(G1_||_(FreeGen_(X_*_f)))_._x_=_(G2_||_(FreeGen_(X_*_f)))_._x
let x be set ; ::_thesis: ( x in the carrier of S1 implies (G1 || (FreeGen (X * f))) . x = (G2 || (FreeGen (X * f))) . x )
assume x in the carrier of S1 ; ::_thesis: (G1 || (FreeGen (X * f))) . x = (G2 || (FreeGen (X * f))) . x
then reconsider s = x as SortSymbol of S1 ;
reconsider g1 = (G1 || (FreeGen (X * f))) . s, g2 = (G2 || (FreeGen (X * f))) . s as Function of ((FreeGen (X * f)) . s),( the Sorts of A1 . s) ;
now__::_thesis:_for_z_being_Element_of_(FreeGen_(X_*_f))_._s_holds_g1_._z_=_g2_._z
let z be Element of (FreeGen (X * f)) . s; ::_thesis: g1 . z = g2 . z
FreeGen (s,(X * f)) = (FreeGen (X * f)) . s by MSAFREE:def_16;
then consider a being set such that
A9: a in (X * f) . s and
A10: z = root-tree [a,s] by MSAFREE:def_15;
reconsider a = a as Element of (X * f) . s by A9;
thus g1 . z = (G1 . s) . z by Th39
.= root-tree [a,(f . s)] by A5, A10
.= (G2 . s) . z by A7, A10
.= g2 . z by Th39 ; ::_thesis: verum
end;
hence (G1 || (FreeGen (X * f))) . x = (G2 || (FreeGen (X * f))) . x by FUNCT_2:63; ::_thesis: verum
end;
A1 = (FreeMSA X) | (S1,f,g) ;
hence G1 = G2 by A4, A6, A8, EXTENS_1:14, PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines hom INSTALG1:def_5_:_
for S1, S2 being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S2
for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
for b6 being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) holds
( b6 = hom (f,g,X,S1,S2) iff ( b6 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (b6 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) ) );
theorem Th40: :: INSTALG1:40
for S1, S2 being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S2
for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
for o being OperSymbol of S1
for p being Element of Args (o,(FreeMSA (X * f)))
for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds
((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q
proof
let S1, S2 be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S2
for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
for o being OperSymbol of S1
for p being Element of Args (o,(FreeMSA (X * f)))
for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds
((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q
let X be V16() ManySortedSet of the carrier of S2; ::_thesis: for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
for o being OperSymbol of S1
for p being Element of Args (o,(FreeMSA (X * f)))
for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds
((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q
let f be Function of the carrier of S1, the carrier of S2; ::_thesis: for g being Function st f,g form_morphism_between S1,S2 holds
for o being OperSymbol of S1
for p being Element of Args (o,(FreeMSA (X * f)))
for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds
((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q
let g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for o being OperSymbol of S1
for p being Element of Args (o,(FreeMSA (X * f)))
for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds
((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q )
set F = hom (f,g,X,S1,S2);
assume A1: f,g form_morphism_between S1,S2 ; ::_thesis: for o being OperSymbol of S1
for p being Element of Args (o,(FreeMSA (X * f)))
for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds
((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q
then reconsider h = g as Function of the carrier' of S1, the carrier' of S2 by Th9;
let o be OperSymbol of S1; ::_thesis: for p being Element of Args (o,(FreeMSA (X * f)))
for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds
((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q
let p be Element of Args (o,(FreeMSA (X * f))); ::_thesis: for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds
((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q
let q be FinSequence; ::_thesis: ( q = (hom (f,g,X,S1,S2)) # p implies ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q )
assume A2: q = (hom (f,g,X,S1,S2)) # p ; ::_thesis: ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q
then A3: q is Element of Args ((h . o),(FreeMSA X)) by A1, Th24;
hom (f,g,X,S1,S2) is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) by A1, Def5;
then ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ((Den (o,(FreeMSA (X * f)))) . p) = (Den (o,((FreeMSA X) | (S1,f,g)))) . q by A2, MSUALG_3:def_7;
hence ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = (Den (o,((FreeMSA X) | (S1,f,g)))) . q by Th3
.= (Den ((h . o),(FreeMSA X))) . q by A1, Th23
.= [(g . o), the carrier of S2] -tree q by A3, Th3 ;
::_thesis: verum
end;
theorem Th41: :: INSTALG1:41
for S1, S2 being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S2
for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
for t being Term of S1,(X * f) holds
( ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X iff t is CompoundTerm of S1,X * f )
proof
let S1, S2 be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S2
for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
for t being Term of S1,(X * f) holds
( ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X iff t is CompoundTerm of S1,X * f )
let X be V16() ManySortedSet of the carrier of S2; ::_thesis: for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
for t being Term of S1,(X * f) holds
( ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X iff t is CompoundTerm of S1,X * f )
let f be Function of the carrier of S1, the carrier of S2; ::_thesis: for g being Function st f,g form_morphism_between S1,S2 holds
for t being Term of S1,(X * f) holds
( ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X iff t is CompoundTerm of S1,X * f )
let g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for t being Term of S1,(X * f) holds
( ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X iff t is CompoundTerm of S1,X * f ) )
assume A1: f,g form_morphism_between S1,S2 ; ::_thesis: for t being Term of S1,(X * f) holds
( ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X iff t is CompoundTerm of S1,X * f )
then reconsider h = g as Function of the carrier' of S1, the carrier' of S2 by Th9;
let t be Term of S1,(X * f); ::_thesis: ( ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X iff t is CompoundTerm of S1,X * f )
hereby ::_thesis: ( t is CompoundTerm of S1,X * f implies ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X )
assume ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X ; ::_thesis: t is CompoundTerm of S1,X * f
then reconsider w = ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t as CompoundTerm of S2,X ;
assume t is not CompoundTerm of S1,X * f ; ::_thesis: contradiction
then not t . {} in [: the carrier' of S1,{ the carrier of S1}:] by MSATERM:def_6;
then consider s being SortSymbol of S1, v being Element of (X * f) . s such that
A2: t . {} = [v,s] by MSATERM:2;
t = root-tree [v,s] by A2, MSATERM:5;
then ( ((hom (f,g,X,S1,S2)) . s) . t = root-tree [v,(f . s)] & the_sort_of t = s ) by A1, Def5, MSATERM:14;
then ( w . {} in [: the carrier' of S2,{ the carrier of S2}:] & w . {} = [v,(f . s)] ) by MSATERM:def_6, TREES_4:3;
then A3: f . s = the carrier of S2 by ZFMISC_1:106;
f . s in the carrier of S2 ;
hence contradiction by A3; ::_thesis: verum
end;
assume t is CompoundTerm of S1,X * f ; ::_thesis: ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X
then reconsider t = t as CompoundTerm of S1,X * f ;
t . {} in [: the carrier' of S1,{ the carrier of S1}:] by MSATERM:def_6;
then consider o, r being set such that
A4: o in the carrier' of S1 and
A5: r in { the carrier of S1} and
A6: t . {} = [o,r] by ZFMISC_1:def_2;
reconsider o = o as OperSymbol of S1 by A4;
r = the carrier of S1 by A5, TARSKI:def_1;
then consider a being ArgumentSeq of Sym (o,(X * f)) such that
A7: t = [o, the carrier of S1] -tree a by A6, MSATERM:10;
reconsider a = a as Element of Args (o,(FreeMSA (X * f))) by Th1;
reconsider b = (hom (f,g,X,S1,S2)) # a as Element of Args ((h . o),(FreeMSA X)) by A1, Th24;
A8: ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree a) = [(g . o), the carrier of S2] -tree b by A1, Th40;
t . {} = [o, the carrier of S1] by A7, TREES_4:def_4;
then A9: the_sort_of t = the_result_sort_of o by MSATERM:17;
reconsider b = b as ArgumentSeq of Sym ((h . o),X) by Th1;
(Sym ((h . o),X)) -tree b = [(h . o), the carrier of S2] -tree b by MSAFREE:def_9;
then reconsider T = [(h . o), the carrier of S2] -tree b as Term of S2,X ;
( T . {} = [(g . o), the carrier of S2] & [(h . o), the carrier of S2] in [: the carrier' of S2,{ the carrier of S2}:] ) by TREES_4:def_4, ZFMISC_1:106;
hence ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X by A7, A9, A8, MSATERM:def_6; ::_thesis: verum
end;
theorem :: INSTALG1:42
for S1, S2 being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S2
for f being Function of the carrier of S1, the carrier of S2
for g being one-to-one Function st f,g form_morphism_between S1,S2 holds
hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g)
proof
let S1, S2 be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S2
for f being Function of the carrier of S1, the carrier of S2
for g being one-to-one Function st f,g form_morphism_between S1,S2 holds
hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g)
let X be V16() ManySortedSet of the carrier of S2; ::_thesis: for f being Function of the carrier of S1, the carrier of S2
for g being one-to-one Function st f,g form_morphism_between S1,S2 holds
hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g)
let f be Function of the carrier of S1, the carrier of S2; ::_thesis: for g being one-to-one Function st f,g form_morphism_between S1,S2 holds
hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g)
let g be one-to-one Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) )
set A = (FreeMSA X) | (S1,f,g);
set H = hom (f,g,X,S1,S2);
defpred S1[ set ] means ex t1 being Term of S1,(X * f) st
( t1 = $1 & ( for t2 being Term of S1,(X * f) st the_sort_of t1 = the_sort_of t2 & ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 holds
t1 = t2 ) );
A1: FreeMSA (X * f) = MSAlgebra(# (FreeSort (X * f)),(FreeOper (X * f)) #) by MSAFREE:def_14;
assume A2: f,g form_morphism_between S1,S2 ; ::_thesis: hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g)
then reconsider h = g as Function of the carrier' of S1, the carrier' of S2 by Th9;
reconsider B = (FreeMSA X) | (S1,f,g) as non-empty MSAlgebra over S1 by A2, Th22;
reconsider H9 = hom (f,g,X,S1,S2) as ManySortedFunction of (FreeMSA (X * f)),B ;
A3: for o being OperSymbol of S1
for p being ArgumentSeq of Sym (o,(X * f)) st ( for t being Term of S1,(X * f) st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S1] -tree p]
proof
let o be OperSymbol of S1; ::_thesis: for p being ArgumentSeq of Sym (o,(X * f)) st ( for t being Term of S1,(X * f) st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S1] -tree p]
let p be ArgumentSeq of Sym (o,(X * f)); ::_thesis: ( ( for t being Term of S1,(X * f) st t in rng p holds
S1[t] ) implies S1[[o, the carrier of S1] -tree p] )
assume A4: for t being Term of S1,(X * f) st t in rng p holds
S1[t] ; ::_thesis: S1[[o, the carrier of S1] -tree p]
A5: dom p = dom (the_arity_of o) by MSATERM:22;
reconsider a = p as Element of Args (o,(FreeMSA (X * f))) by Th1;
A6: [(h . o), the carrier of S2] in [: the carrier' of S2,{ the carrier of S2}:] by ZFMISC_1:106;
reconsider q = (hom (f,g,X,S1,S2)) # a as Element of Args ((h . o),(FreeMSA X)) by A2, Th24;
take t1 = (Sym (o,(X * f))) -tree p; ::_thesis: ( t1 = [o, the carrier of S1] -tree p & ( for t2 being Term of S1,(X * f) st the_sort_of t1 = the_sort_of t2 & ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 holds
t1 = t2 ) )
thus A7: t1 = [o, the carrier of S1] -tree p by MSAFREE:def_9; ::_thesis: for t2 being Term of S1,(X * f) st the_sort_of t1 = the_sort_of t2 & ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 holds
t1 = t2
reconsider b = q as ArgumentSeq of Sym ((h . o),X) by Th1;
let t2 be Term of S1,(X * f); ::_thesis: ( the_sort_of t1 = the_sort_of t2 & ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 implies t1 = t2 )
assume A8: ( the_sort_of t1 = the_sort_of t2 & ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 ) ; ::_thesis: t1 = t2
the_sort_of t1 = the_result_sort_of o by MSATERM:20;
then A9: ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = [(g . o), the carrier of S2] -tree q by A2, A7, Th40;
( ((Sym ((h . o),X)) -tree b) . {} = Sym ((h . o),X) & Sym ((h . o),X) = [(h . o), the carrier of S2] ) by MSAFREE:def_9, TREES_4:def_4;
then [(h . o), the carrier of S2] -tree b is CompoundTerm of S2,X by A6, MSATERM:def_6;
then t2 is CompoundTerm of S1,X * f by A2, A8, A9, Th41;
then t2 . {} in [: the carrier' of S1,{ the carrier of S1}:] by MSATERM:def_6;
then consider o9, s9 being set such that
A10: o9 in the carrier' of S1 and
A11: ( s9 in { the carrier of S1} & t2 . {} = [o9,s9] ) by ZFMISC_1:def_2;
reconsider o9 = o9 as OperSymbol of S1 by A10;
A12: t2 . {} = [o9, the carrier of S1] by A11, TARSKI:def_1;
then consider r being ArgumentSeq of Sym (o9,(X * f)) such that
A13: t2 = [o9, the carrier of S1] -tree r by MSATERM:10;
reconsider c = r as Element of Args (o9,(FreeMSA (X * f))) by Th1;
reconsider R = (hom (f,g,X,S1,S2)) # c as Element of Args ((h . o9),(FreeMSA X)) by A2, Th24;
the_result_sort_of o9 = the_sort_of t2 by A12, MSATERM:17;
then A14: ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = [(g . o9), the carrier of S2] -tree R by A2, A8, A13, Th40;
then [(g . o9), the carrier of S2] = [(g . o), the carrier of S2] by A9, TREES_4:15;
then h . o = h . o9 by XTUPLE_0:1;
then A15: o = o9 by FUNCT_2:19;
then A16: dom r = dom (the_arity_of o) by MSATERM:22;
A17: q = R by A9, A14, TREES_4:15;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(the_arity_of_o)_holds_
p_._i_=_r_._i
let i be Nat; ::_thesis: ( i in dom (the_arity_of o) implies p . i = r . i )
A18: R = H9 # c ;
assume A19: i in dom (the_arity_of o) ; ::_thesis: p . i = r . i
then reconsider w1 = p . i, w2 = r . i as Term of S1,(X * f) by A5, A16, MSATERM:22;
A20: the_sort_of w1 = (the_arity_of o) /. i by A5, A19, MSATERM:23;
q = H9 # a ;
then q . i = ((hom (f,g,X,S1,S2)) . (the_sort_of w1)) . w1 by A5, A19, A20, MSUALG_3:def_6;
then A21: ((hom (f,g,X,S1,S2)) . (the_sort_of w1)) . w1 = ((hom (f,g,X,S1,S2)) . (the_sort_of w1)) . w2 by A17, A15, A16, A19, A20, A18, MSUALG_3:def_6;
w1 in rng p by A5, A19, FUNCT_1:def_3;
then A22: S1[w1] by A4;
the_sort_of w2 = (the_arity_of o) /. i by A15, A16, A19, MSATERM:23;
hence p . i = r . i by A22, A20, A21; ::_thesis: verum
end;
hence t1 = t2 by A7, A13, A15, A5, A16, FINSEQ_1:13; ::_thesis: verum
end;
thus hom (f,g,X,S1,S2) is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) by A2, Def5; :: according to MSUALG_3:def_9 ::_thesis: hom (f,g,X,S1,S2) is "1-1"
let i be set ; :: according to MSUALG_3:def_2 ::_thesis: for b1 being set holds
( not i in dom (hom (f,g,X,S1,S2)) or not (hom (f,g,X,S1,S2)) . i = b1 or b1 is one-to-one )
let h be Function; ::_thesis: ( not i in dom (hom (f,g,X,S1,S2)) or not (hom (f,g,X,S1,S2)) . i = h or h is one-to-one )
assume i in dom (hom (f,g,X,S1,S2)) ; ::_thesis: ( not (hom (f,g,X,S1,S2)) . i = h or h is one-to-one )
then reconsider s = i as SortSymbol of S1 by PARTFUN1:def_2;
assume A23: (hom (f,g,X,S1,S2)) . i = h ; ::_thesis: h is one-to-one
then A24: dom h = dom (H9 . s)
.= (FreeSort (X * f)) . s by A1, FUNCT_2:def_1
.= FreeSort ((X * f),s) by MSAFREE:def_11 ;
let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in dom h or not y in dom h or not h . x = h . y or x = y )
assume A25: ( x in dom h & y in dom h ) ; ::_thesis: ( not h . x = h . y or x = y )
FreeSort ((X * f),s) c= S1 -Terms (X * f) by MSATERM:12;
then reconsider t1 = x, t2 = y as Term of S1,(X * f) by A24, A25;
A26: for s being SortSymbol of S1
for v being Element of (X * f) . s holds S1[ root-tree [v,s]]
proof
let s be SortSymbol of S1; ::_thesis: for v being Element of (X * f) . s holds S1[ root-tree [v,s]]
let v be Element of (X * f) . s; ::_thesis: S1[ root-tree [v,s]]
reconsider t1 = root-tree [v,s] as Term of S1,(X * f) by MSATERM:4;
take t1 ; ::_thesis: ( t1 = root-tree [v,s] & ( for t2 being Term of S1,(X * f) st the_sort_of t1 = the_sort_of t2 & ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 holds
t1 = t2 ) )
thus t1 = root-tree [v,s] ; ::_thesis: for t2 being Term of S1,(X * f) st the_sort_of t1 = the_sort_of t2 & ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 holds
t1 = t2
let t2 be Term of S1,(X * f); ::_thesis: ( the_sort_of t1 = the_sort_of t2 & ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 implies t1 = t2 )
assume that
A27: the_sort_of t1 = the_sort_of t2 and
A28: ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 ; ::_thesis: t1 = t2
A29: the_sort_of t1 = s by MSATERM:14;
A30: ((hom (f,g,X,S1,S2)) . s) . (root-tree [v,s]) = root-tree [v,(f . s)] by A2, Def5;
now__::_thesis:_not_t2_._{}_in_[:_the_carrier'_of_S1,{_the_carrier_of_S1}:]
assume t2 . {} in [: the carrier' of S1,{ the carrier of S1}:] ; ::_thesis: contradiction
then t2 is CompoundTerm of S1,X * f by MSATERM:def_6;
then ( (root-tree [v,(f . s)]) . {} = [v,(f . s)] & root-tree [v,(f . s)] is CompoundTerm of S2,X ) by A2, A27, A28, A30, A29, Th41, TREES_4:3;
then [v,(f . s)] in [: the carrier' of S2,{ the carrier of S2}:] by MSATERM:def_6;
then A31: f . s = the carrier of S2 by ZFMISC_1:106;
f . s in the carrier of S2 ;
hence contradiction by A31; ::_thesis: verum
end;
then consider s2 being SortSymbol of S1, v2 being Element of (X * f) . s2 such that
A32: t2 . {} = [v2,s2] by MSATERM:2;
A33: t2 = root-tree [v2,s2] by A32, MSATERM:5;
then A34: s = s2 by A27, A29, MSATERM:14;
then ((hom (f,g,X,S1,S2)) . s) . t2 = root-tree [v2,(f . s)] by A2, A33, Def5;
then [v,(f . s)] = [v2,(f . s)] by A28, A30, A29, TREES_4:4;
hence t1 = t2 by A33, A34, XTUPLE_0:1; ::_thesis: verum
end;
for t being Term of S1,(X * f) holds S1[t] from MSATERM:sch_1(A26, A3);
then A35: S1[t1] ;
( the_sort_of t1 = s & the_sort_of t2 = s ) by A24, A25, MSATERM:def_5;
hence ( not h . x = h . y or x = y ) by A23, A35; ::_thesis: verum
end;
theorem :: INSTALG1:43
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds hom ((id the carrier of S),(id the carrier' of S),X,S,S) = id the Sorts of (FreeMSA X)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S holds hom ((id the carrier of S),(id the carrier' of S),X,S,S) = id the Sorts of (FreeMSA X)
let X be V16() ManySortedSet of the carrier of S; ::_thesis: hom ((id the carrier of S),(id the carrier' of S),X,S,S) = id the Sorts of (FreeMSA X)
set f = id the carrier of S;
set h = hom ((id the carrier of S),(id the carrier' of S),X,S,S);
set I = id the Sorts of (FreeMSA X);
set g = id the carrier' of S;
A1: id the carrier of S, id the carrier' of S form_morphism_between S,S by PUA2MSS1:28;
dom X = the carrier of S by PARTFUN1:def_2;
then A2: X * (id the carrier of S) = X by RELAT_1:52;
A3: (FreeMSA X) | (S,(id the carrier of S),(id the carrier' of S)) = FreeMSA X by Th25;
A4: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
((id_the_Sorts_of_(FreeMSA_X))_||_(FreeGen_X))_._i_=_((hom_((id_the_carrier_of_S),(id_the_carrier'_of_S),X,S,S))_||_(FreeGen_(X_*_(id_the_carrier_of_S))))_._i
let i be set ; ::_thesis: ( i in the carrier of S implies ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . i = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . i )
assume i in the carrier of S ; ::_thesis: ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . i = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . i
then reconsider s = i as SortSymbol of S ;
FreeGen X c= the Sorts of (FreeMSA X) by PBOOLE:def_18;
then A5: (FreeGen X) . s c= the Sorts of (FreeMSA X) . s by PBOOLE:def_2;
then ((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s) is Function of ((FreeGen X) . s),( the Sorts of (FreeMSA X) . s) by FUNCT_2:32;
then A6: dom (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) = (FreeGen X) . s by FUNCT_2:def_1;
A7: now__::_thesis:_for_a_being_set_st_a_in_(FreeGen_X)_._s_holds_
(((id_the_Sorts_of_(FreeMSA_X))_._s)_|_((FreeGen_X)_._s))_._a_=_(((hom_((id_the_carrier_of_S),(id_the_carrier'_of_S),X,S,S))_._s)_|_((FreeGen_X)_._s))_._a
let a be set ; ::_thesis: ( a in (FreeGen X) . s implies (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) . a = (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) . a )
assume A8: a in (FreeGen X) . s ; ::_thesis: (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) . a = (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) . a
then reconsider b = a as Element of (FreeMSA X),s by A5;
b in FreeGen (s,X) by A8, MSAFREE:def_16;
then consider x being set such that
A9: x in X . s and
A10: b = root-tree [x,s] by MSAFREE:def_15;
thus (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) . a = ((id the Sorts of (FreeMSA X)) . s) . b by A8, FUNCT_1:49
.= (id ( the Sorts of (FreeMSA X) . s)) . b by MSUALG_3:def_1
.= b by FUNCT_1:18
.= root-tree [x,((id the carrier of S) . s)] by A10, FUNCT_1:18
.= ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) . b by A1, A2, A9, A10, Def5
.= (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) . a by A8, FUNCT_1:49 ; ::_thesis: verum
end;
((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s) is Function of ((FreeGen X) . s),( the Sorts of (FreeMSA X) . s) by A2, A3, A5, FUNCT_2:32;
then A11: dom (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) = (FreeGen X) . s by FUNCT_2:def_1;
( ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . s = ((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s) & ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . s = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen (X * (id the carrier of S))) . s) ) by MSAFREE:def_1;
hence ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . i = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . i by A2, A6, A11, A7, FUNCT_1:2; ::_thesis: verum
end;
( id the Sorts of (FreeMSA X) is_homomorphism FreeMSA X, FreeMSA X & hom ((id the carrier of S),(id the carrier' of S),X,S,S) is_homomorphism FreeMSA (X * (id the carrier of S)),(FreeMSA X) | (S,(id the carrier of S),(id the carrier' of S)) ) by A1, Def5, MSUALG_3:9;
hence hom ((id the carrier of S),(id the carrier' of S),X,S,S) = id the Sorts of (FreeMSA X) by A2, A3, A4, EXTENS_1:19, PBOOLE:3; ::_thesis: verum
end;
theorem :: INSTALG1:44
for S1, S2, S3 being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S3
for f1 being Function of the carrier of S1, the carrier of S2
for g1 being Function st f1,g1 form_morphism_between S1,S2 holds
for f2 being Function of the carrier of S2, the carrier of S3
for g2 being Function st f2,g2 form_morphism_between S2,S3 holds
hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2))
proof
let S1, S2, S3 be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S3
for f1 being Function of the carrier of S1, the carrier of S2
for g1 being Function st f1,g1 form_morphism_between S1,S2 holds
for f2 being Function of the carrier of S2, the carrier of S3
for g2 being Function st f2,g2 form_morphism_between S2,S3 holds
hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2))
let X be V16() ManySortedSet of the carrier of S3; ::_thesis: for f1 being Function of the carrier of S1, the carrier of S2
for g1 being Function st f1,g1 form_morphism_between S1,S2 holds
for f2 being Function of the carrier of S2, the carrier of S3
for g2 being Function st f2,g2 form_morphism_between S2,S3 holds
hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2))
let f1 be Function of the carrier of S1, the carrier of S2; ::_thesis: for g1 being Function st f1,g1 form_morphism_between S1,S2 holds
for f2 being Function of the carrier of S2, the carrier of S3
for g2 being Function st f2,g2 form_morphism_between S2,S3 holds
hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2))
let g1 be Function; ::_thesis: ( f1,g1 form_morphism_between S1,S2 implies for f2 being Function of the carrier of S2, the carrier of S3
for g2 being Function st f2,g2 form_morphism_between S2,S3 holds
hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2)) )
assume A1: f1,g1 form_morphism_between S1,S2 ; ::_thesis: for f2 being Function of the carrier of S2, the carrier of S3
for g2 being Function st f2,g2 form_morphism_between S2,S3 holds
hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2))
let f2 be Function of the carrier of S2, the carrier of S3; ::_thesis: for g2 being Function st f2,g2 form_morphism_between S2,S3 holds
hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2))
let g2 be Function; ::_thesis: ( f2,g2 form_morphism_between S2,S3 implies hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2)) )
set f = f2 * f1;
set g = g2 * g1;
assume A2: f2,g2 form_morphism_between S2,S3 ; ::_thesis: hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2))
then reconsider Af = (FreeMSA X) | (S1,(f2 * f1),(g2 * g1)), Af1 = (FreeMSA (X * f2)) | (S1,f1,g1) as non-empty MSAlgebra over S1 by A1, Th22, PUA2MSS1:29;
A3: hom (f2,g2,X,S2,S3) is_homomorphism FreeMSA (X * f2),(FreeMSA X) | (S2,f2,g2) by A2, Def5;
A4: the Sorts of (FreeMSA (X * f2)) is_transformable_to the Sorts of ((FreeMSA X) | (S2,f2,g2))
proof
let i be set ; :: according to PZFMISC1:def_3 ::_thesis: ( not i in the carrier of S2 or not the Sorts of ((FreeMSA X) | (S2,f2,g2)) . i = {} or the Sorts of (FreeMSA (X * f2)) . i = {} )
assume i in the carrier of S2 ; ::_thesis: ( not the Sorts of ((FreeMSA X) | (S2,f2,g2)) . i = {} or the Sorts of (FreeMSA (X * f2)) . i = {} )
then reconsider s = i as SortSymbol of S2 ;
the Sorts of ((FreeMSA X) | (S2,f2,g2)) . s = ( the Sorts of (FreeMSA X) * f2) . s by A2, Def3;
hence ( not the Sorts of ((FreeMSA X) | (S2,f2,g2)) . i = {} or the Sorts of (FreeMSA (X * f2)) . i = {} ) ; ::_thesis: verum
end;
(FreeMSA X) | (S1,(f2 * f1),(g2 * g1)) = ((FreeMSA X) | (S2,f2,g2)) | (S1,f1,g1) by A1, A2, Th27;
then consider hf1 being ManySortedFunction of Af1,Af such that
A5: hf1 = (hom (f2,g2,X,S2,S3)) * f1 and
A6: hf1 is_homomorphism Af1,Af by A1, A3, A4, Th34;
reconsider hh = hom (f1,g1,(X * f2),S1,S2) as ManySortedFunction of (FreeMSA (X * (f2 * f1))),Af1 by RELAT_1:36;
reconsider hf1h = hf1 ** hh as ManySortedFunction of (FreeMSA (X * (f2 * f1))),((FreeMSA X) | (S1,(f2 * f1),(g2 * g1))) ;
A7: X * (f2 * f1) = (X * f2) * f1 by RELAT_1:36;
A8: now__::_thesis:_for_s_being_SortSymbol_of_S1
for_x_being_Element_of_(X_*_(f2_*_f1))_._s_holds_(hf1h_._s)_._(root-tree_[x,s])_=_root-tree_[x,((f2_*_f1)_._s)]
let s be SortSymbol of S1; ::_thesis: for x being Element of (X * (f2 * f1)) . s holds (hf1h . s) . (root-tree [x,s]) = root-tree [x,((f2 * f1) . s)]
let x be Element of (X * (f2 * f1)) . s; ::_thesis: (hf1h . s) . (root-tree [x,s]) = root-tree [x,((f2 * f1) . s)]
reconsider t = root-tree [x,s] as Term of S1,(X * (f2 * f1)) by MSATERM:4;
A9: FreeMSA (X * (f2 * f1)) = MSAlgebra(# (FreeSort (X * (f2 * f1))),(FreeOper (X * (f2 * f1))) #) by MSAFREE:def_14;
( the_sort_of t = s & (FreeSort (X * (f2 * f1))) . s = FreeSort ((X * (f2 * f1)),s) ) by MSAFREE:def_11, MSATERM:14;
then A10: root-tree [x,s] in the Sorts of (FreeMSA (X * (f2 * f1))) . s by A9, MSATERM:def_5;
A11: (X * (f2 * f1)) . s = (X * f2) . (f1 . s) by A7, FUNCT_2:15;
(hf1h . s) . (root-tree [x,s]) = ((hf1 . s) * ((hom (f1,g1,(X * f2),S1,S2)) . s)) . (root-tree [x,s]) by MSUALG_3:2
.= (hf1 . s) . (((hom (f1,g1,(X * f2),S1,S2)) . s) . (root-tree [x,s])) by A7, A10, FUNCT_2:15
.= (hf1 . s) . (root-tree [x,(f1 . s)]) by A1, A7, Def5 ;
hence (hf1h . s) . (root-tree [x,s]) = ((hom (f2,g2,X,S2,S3)) . (f1 . s)) . (root-tree [x,(f1 . s)]) by A5, FUNCT_2:15
.= root-tree [x,(f2 . (f1 . s))] by A2, A11, Def5
.= root-tree [x,((f2 * f1) . s)] by FUNCT_2:15 ;
::_thesis: verum
end;
A12: f2 * f1,g2 * g1 form_morphism_between S1,S3 by A1, A2, PUA2MSS1:29;
hom (f1,g1,(X * f2),S1,S2) is_homomorphism FreeMSA ((X * f2) * f1),(FreeMSA (X * f2)) | (S1,f1,g1) by A1, Def5;
then hf1 ** hh is_homomorphism FreeMSA (X * (f2 * f1)),Af by A6, A7, MSUALG_3:10;
hence hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2)) by A12, A5, A8, Def5; ::_thesis: verum
end;