:: Terms over many sorted universal algebra :: by Grzegorz Bancerek :: :: Received November 25, 1994 :: Copyright (c) 1994-2012 Association of Mizar Users begin Lm1: for n being set for p being FinSequence st n in dom p holds ex k being Element of NAT st ( n = k + 1 & k < len p ) proofend; Lm2: now__::_thesis:_for_n_being_Element_of_NAT_ for_x_being_set_ for_p_being_FinSequence_of_x_st_n_<_len_p_holds_ p_._(n_+_1)_in_x let n be Element of NAT ; ::_thesis: for x being set for p being FinSequence of x st n < len p holds p . (n + 1) in x let x be set ; ::_thesis: for p being FinSequence of x st n < len p holds p . (n + 1) in x let p be FinSequence of x; ::_thesis: ( n < len p implies p . (n + 1) in x ) n >= 0 by NAT_1:2; then A1: n + 1 >= 0 + 1 by XREAL_1:7; assume n < len p ; ::_thesis: p . (n + 1) in x then n + 1 <= len p by NAT_1:13; then n + 1 in dom p by A1, FINSEQ_3:25; then A2: p . (n + 1) in rng p by FUNCT_1:def_3; rng p c= x by FINSEQ_1:def_4; hence p . (n + 1) in x by A2; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let V be ManySortedSet of the carrier of S; funcS -Terms V -> Subset of (FinTrees the carrier of (DTConMSA V)) equals :Def1: :: MSATERM:def 1 TS (DTConMSA V); correctness coherence TS (DTConMSA V) is Subset of (FinTrees the carrier of (DTConMSA V)); ; end; :: deftheorem Def1 defines -Terms MSATERM:def_1_:_ for S being non empty non void ManySortedSign for V being ManySortedSet of the carrier of S holds S -Terms V = TS (DTConMSA V); registration let S be non empty non void ManySortedSign ; let V be V16() ManySortedSet of the carrier of S; clusterS -Terms V -> non empty ; correctness coherence not S -Terms V is empty ; ; end; definition let S be non empty non void ManySortedSign ; let V be V16() ManySortedSet of the carrier of S; mode Term of S,V is Element of S -Terms V; end; definition let S be non empty non void ManySortedSign ; let V be V16() ManySortedSet of the carrier of S; let o be OperSymbol of S; :: original:Sym redefine func Sym (o,V) -> NonTerminal of (DTConMSA V); coherence Sym (o,V) is NonTerminal of (DTConMSA V) proofend; end; definition let S be non empty non void ManySortedSign ; let V be V16() ManySortedSet of the carrier of S; let sy be NonTerminal of (DTConMSA V); mode ArgumentSeq of sy -> FinSequence of S -Terms V means :Def2: :: MSATERM:def 2 it is SubtreeSeq of sy; existence ex b1 being FinSequence of S -Terms V st b1 is SubtreeSeq of sy proofend; end; :: deftheorem Def2 defines ArgumentSeq MSATERM:def_2_:_ for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for sy being NonTerminal of (DTConMSA V) for b4 being FinSequence of S -Terms V holds ( b4 is ArgumentSeq of sy iff b4 is SubtreeSeq of sy ); theorem Th1: :: MSATERM:1 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for o being OperSymbol of S for a being FinSequence holds ( ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym (o,V) ) proofend; Lm3: now__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_ for_V_being_V16()_ManySortedSet_of_the_carrier_of_S for_x_being_set_holds_ (_(_x_in_Terminals_(DTConMSA_V)_implies_ex_s_being_SortSymbol_of_S_ex_v_being_Element_of_V_._s_st_x_=_[v,s]_)_&_(_for_s_being_SortSymbol_of_S for_a_being_Element_of_V_._s_st_x_=_[a,s]_holds_ x_in_Terminals_(DTConMSA_V)_)_) let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S for x being set holds ( ( x in Terminals (DTConMSA V) implies ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S for a being Element of V . s st x = [a,s] holds x in Terminals (DTConMSA V) ) ) let V be V16() ManySortedSet of the carrier of S; ::_thesis: for x being set holds ( ( x in Terminals (DTConMSA V) implies ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S for a being Element of V . s st x = [a,s] holds x in Terminals (DTConMSA V) ) ) let x be set ; ::_thesis: ( ( x in Terminals (DTConMSA V) implies ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S for a being Element of V . s st x = [a,s] holds x in Terminals (DTConMSA V) ) ) set X = V; set G = DTConMSA V; A1: Terminals (DTConMSA V) = Union (coprod V) by MSAFREE:6; hereby ::_thesis: for s being SortSymbol of S for a being Element of V . s st x = [a,s] holds x in Terminals (DTConMSA V) assume x in Terminals (DTConMSA V) ; ::_thesis: ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] then consider s being set such that A2: s in dom (coprod V) and A3: x in (coprod V) . s by A1, CARD_5:2; reconsider s = s as SortSymbol of S by A2, PARTFUN1:def_2; (coprod V) . s = coprod (s,V) by MSAFREE:def_3; then ex a being set st ( a in V . s & x = [a,s] ) by A3, MSAFREE:def_2; hence ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ; ::_thesis: verum end; let s be SortSymbol of S; ::_thesis: for a being Element of V . s st x = [a,s] holds x in Terminals (DTConMSA V) let a be Element of V . s; ::_thesis: ( x = [a,s] implies x in Terminals (DTConMSA V) ) assume x = [a,s] ; ::_thesis: x in Terminals (DTConMSA V) then x in coprod (s,V) by MSAFREE:def_2; then A4: x in (coprod V) . s by MSAFREE:def_3; dom (coprod V) = the carrier of S by PARTFUN1:def_2; hence x in Terminals (DTConMSA V) by A1, A4, CARD_5:2; ::_thesis: verum end; Lm4: now__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_ for_A_being_MSAlgebra_over_S for_V_being_V16()_ManySortedSet_of_the_carrier_of_S for_x_being_set_holds_ (_(_not_x_in_Terminals_(DTConMSA_(_the_Sorts_of_A_\/_V))_or_ex_s_being_SortSymbol_of_S_ex_a_being_set_st_ (_a_in_the_Sorts_of_A_._s_&_x_=_[a,s]_)_or_ex_s_being_SortSymbol_of_S_ex_v_being_Element_of_V_._s_st_x_=_[v,s]_)_&_(_for_s_being_SortSymbol_of_S_holds_ (_(_for_a_being_set_st_a_in_the_Sorts_of_A_._s_&_x_=_[a,s]_holds_ x_in_Terminals_(DTConMSA_(_the_Sorts_of_A_\/_V))_)_&_(_for_a_being_Element_of_V_._s_st_x_=_[a,s]_holds_ x_in_Terminals_(DTConMSA_(_the_Sorts_of_A_\/_V))_)_)_)_) let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S for V being V16() ManySortedSet of the carrier of S for x being set holds ( ( not x in Terminals (DTConMSA ( the Sorts of A \/ V)) or ex s being SortSymbol of S ex a being set st ( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S holds ( ( for a being set st a in the Sorts of A . s & x = [a,s] holds x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) & ( for a being Element of V . s st x = [a,s] holds x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) ) ) ) let A be MSAlgebra over S; ::_thesis: for V being V16() ManySortedSet of the carrier of S for x being set holds ( ( not x in Terminals (DTConMSA ( the Sorts of A \/ V)) or ex s being SortSymbol of S ex a being set st ( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S holds ( ( for a being set st a in the Sorts of A . s & x = [a,s] holds x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) & ( for a being Element of V . s st x = [a,s] holds x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) ) ) ) let V be V16() ManySortedSet of the carrier of S; ::_thesis: for x being set holds ( ( not x in Terminals (DTConMSA ( the Sorts of A \/ V)) or ex s being SortSymbol of S ex a being set st ( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S holds ( ( for a being set st a in the Sorts of A . s & x = [a,s] holds x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) & ( for a being Element of V . s st x = [a,s] holds x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) ) ) ) let x be set ; ::_thesis: ( ( not x in Terminals (DTConMSA ( the Sorts of A \/ V)) or ex s being SortSymbol of S ex a being set st ( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S holds ( ( for a being set st a in the Sorts of A . s & x = [a,s] holds x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) & ( for a being Element of V . s st x = [a,s] holds x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) ) ) ) set X = the Sorts of A \/ V; set G = DTConMSA ( the Sorts of A \/ V); A1: dom (coprod ( the Sorts of A \/ V)) = the carrier of S by PARTFUN1:def_2; A2: Terminals (DTConMSA ( the Sorts of A \/ V)) = Union (coprod ( the Sorts of A \/ V)) by MSAFREE:6; hereby ::_thesis: for s being SortSymbol of S holds ( ( for a being set st a in the Sorts of A . s & x = [a,s] holds x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) & ( for a being Element of V . s st x = [a,s] holds x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) ) assume x in Terminals (DTConMSA ( the Sorts of A \/ V)) ; ::_thesis: ( ex s being SortSymbol of S ex a being set st ( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) then consider s being set such that A3: s in dom (coprod ( the Sorts of A \/ V)) and A4: x in (coprod ( the Sorts of A \/ V)) . s by A2, CARD_5:2; reconsider s = s as SortSymbol of S by A3, PARTFUN1:def_2; (coprod ( the Sorts of A \/ V)) . s = coprod (s,( the Sorts of A \/ V)) by MSAFREE:def_3; then consider a being set such that A5: a in ( the Sorts of A \/ V) . s and A6: x = [a,s] by A4, MSAFREE:def_2; ( the Sorts of A \/ V) . s = ( the Sorts of A . s) \/ (V . s) by PBOOLE:def_4; then ( a in the Sorts of A . s or a in V . s ) by A5, XBOOLE_0:def_3; hence ( ex s being SortSymbol of S ex a being set st ( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) by A6; ::_thesis: verum end; let s be SortSymbol of S; ::_thesis: ( ( for a being set st a in the Sorts of A . s & x = [a,s] holds x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) & ( for a being Element of V . s st x = [a,s] holds x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) ) A7: ( the Sorts of A \/ V) . s = ( the Sorts of A . s) \/ (V . s) by PBOOLE:def_4; hereby ::_thesis: for a being Element of V . s st x = [a,s] holds x in Terminals (DTConMSA ( the Sorts of A \/ V)) let a be set ; ::_thesis: ( a in the Sorts of A . s & x = [a,s] implies x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) assume a in the Sorts of A . s ; ::_thesis: ( x = [a,s] implies x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) then A8: a in ( the Sorts of A \/ V) . s by A7, XBOOLE_0:def_3; assume x = [a,s] ; ::_thesis: x in Terminals (DTConMSA ( the Sorts of A \/ V)) then x in coprod (s,( the Sorts of A \/ V)) by A8, MSAFREE:def_2; then x in (coprod ( the Sorts of A \/ V)) . s by MSAFREE:def_3; hence x in Terminals (DTConMSA ( the Sorts of A \/ V)) by A2, A1, CARD_5:2; ::_thesis: verum end; let a be Element of V . s; ::_thesis: ( x = [a,s] implies x in Terminals (DTConMSA ( the Sorts of A \/ V)) ) assume A9: x = [a,s] ; ::_thesis: x in Terminals (DTConMSA ( the Sorts of A \/ V)) a in ( the Sorts of A \/ V) . s by A7, XBOOLE_0:def_3; then x in coprod (s,( the Sorts of A \/ V)) by A9, MSAFREE:def_2; then x in (coprod ( the Sorts of A \/ V)) . s by MSAFREE:def_3; hence x in Terminals (DTConMSA ( the Sorts of A \/ V)) by A2, A1, CARD_5:2; ::_thesis: verum end; Lm5: now__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_ for_V_being_V16()_ManySortedSet_of_the_carrier_of_S for_x_being_set_holds_ (_x_is_NonTerminal_of_(DTConMSA_V)_iff_x_in_[:_the_carrier'_of_S,{_the_carrier_of_S}:]_) let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S for x being set holds ( x is NonTerminal of (DTConMSA V) iff x in [: the carrier' of S,{ the carrier of S}:] ) let V be V16() ManySortedSet of the carrier of S; ::_thesis: for x being set holds ( x is NonTerminal of (DTConMSA V) iff x in [: the carrier' of S,{ the carrier of S}:] ) set G = DTConMSA V; let x be set ; ::_thesis: ( x is NonTerminal of (DTConMSA V) iff x in [: the carrier' of S,{ the carrier of S}:] ) NonTerminals (DTConMSA V) = [: the carrier' of S,{ the carrier of S}:] by MSAFREE:6; hence ( x is NonTerminal of (DTConMSA V) iff x in [: the carrier' of S,{ the carrier of S}:] ) ; ::_thesis: verum end; scheme :: MSATERM:sch 1 TermInd{ F1() -> non empty non void ManySortedSign , F2() -> V16() ManySortedSet of the carrier of F1(), P1[ set ] } : for t being Term of F1(),F2() holds P1[t] provided A1: for s being SortSymbol of F1() for v being Element of F2() . s holds P1[ root-tree [v,s]] and A2: for o being OperSymbol of F1() for p being ArgumentSeq of Sym (o,F2()) st ( for t being Term of F1(),F2() st t in rng p holds P1[t] ) holds P1[[o, the carrier of F1()] -tree p] proofend; definition let S be non empty non void ManySortedSign ; let A be MSAlgebra over S; let V be V16() ManySortedSet of the carrier of S; mode c-Term of A,V is Term of S,( the Sorts of A \/ V); end; definition let S be non empty non void ManySortedSign ; let A be MSAlgebra over S; let V be V16() ManySortedSet of the carrier of S; let o be OperSymbol of S; mode ArgumentSeq of o,A,V is ArgumentSeq of Sym (o,( the Sorts of A \/ V)); end; scheme :: MSATERM:sch 2 CTermInd{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), F3() -> V16() ManySortedSet of the carrier of F1(), P1[ set ] } : for t being c-Term of F2(),F3() holds P1[t] provided A1: for s being SortSymbol of F1() for x being Element of the Sorts of F2() . s holds P1[ root-tree [x,s]] and A2: for s being SortSymbol of F1() for v being Element of F3() . s holds P1[ root-tree [v,s]] and A3: for o being OperSymbol of F1() for p being ArgumentSeq of o,F2(),F3() st ( for t being c-Term of F2(),F3() st t in rng p holds P1[t] ) holds P1[(Sym (o,( the Sorts of F2() \/ F3()))) -tree p] proofend; definition let S be non empty non void ManySortedSign ; let V be V16() ManySortedSet of the carrier of S; let t be Term of S,V; let p be Node of t; :: original:. redefine funct . p -> Symbol of (DTConMSA V); coherence t . p is Symbol of (DTConMSA V) proofend; end; registration let S be non empty non void ManySortedSign ; let V be V16() ManySortedSet of the carrier of S; cluster -> finite for Element of S -Terms V; coherence for b1 being Term of S,V holds b1 is finite ; end; Lm6: now__::_thesis:_for_G_being_non_empty_with_terminals_with_nonterminals_DTConstrStr_ for_s_being_Symbol_of_G_holds_ (_(_s_is_Terminal_of_G_or_s_is_NonTerminal_of_G_)_&_(_not_s_is_Terminal_of_G_or_not_s_is_NonTerminal_of_G_)_) let G be non empty with_terminals with_nonterminals DTConstrStr ; ::_thesis: for s being Symbol of G holds ( ( s is Terminal of G or s is NonTerminal of G ) & ( not s is Terminal of G or not s is NonTerminal of G ) ) let s be Symbol of G; ::_thesis: ( ( s is Terminal of G or s is NonTerminal of G ) & ( not s is Terminal of G or not s is NonTerminal of G ) ) the carrier of G = (Terminals G) \/ (NonTerminals G) by LANG1:1; hence ( s is Terminal of G or s is NonTerminal of G ) by XBOOLE_0:def_3; ::_thesis: ( not s is Terminal of G or not s is NonTerminal of G ) Terminals G misses NonTerminals G by DTCONSTR:8; hence ( not s is Terminal of G or not s is NonTerminal of G ) by XBOOLE_0:3; ::_thesis: verum end; theorem Th2: :: MSATERM:2 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for t being Term of S,V holds ( ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] ) proofend; theorem :: MSATERM:3 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for A being MSAlgebra over S for t being c-Term of A,V holds ( ex s being SortSymbol of S ex x being set st ( x in the Sorts of A . s & t . {} = [x,s] ) or ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] ) proofend; theorem Th4: :: MSATERM:4 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for s being SortSymbol of S for v being Element of V . s holds root-tree [v,s] is Term of S,V proofend; theorem Th5: :: MSATERM:5 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for t being Term of S,V for s being SortSymbol of S for v being Element of V . s st t . {} = [v,s] holds t = root-tree [v,s] proofend; theorem Th6: :: MSATERM:6 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for A being MSAlgebra over S for s being SortSymbol of S for x being set st x in the Sorts of A . s holds root-tree [x,s] is c-Term of A,V proofend; theorem :: MSATERM:7 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for A being MSAlgebra over S for t being c-Term of A,V for s being SortSymbol of S for x being set st x in the Sorts of A . s & t . {} = [x,s] holds t = root-tree [x,s] proofend; theorem Th8: :: MSATERM:8 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for A being MSAlgebra over S for s being SortSymbol of S for v being Element of V . s holds root-tree [v,s] is c-Term of A,V proofend; theorem :: MSATERM:9 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for A being MSAlgebra over S for t being c-Term of A,V for s being SortSymbol of S for v being Element of V . s st t . {} = [v,s] holds t = root-tree [v,s] proofend; theorem Th10: :: MSATERM:10 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for t being Term of S,V for o being OperSymbol of S st t . {} = [o, the carrier of S] holds ex a being ArgumentSeq of Sym (o,V) st t = [o, the carrier of S] -tree a proofend; definition let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; let V be V16() ManySortedSet of the carrier of S; let s be SortSymbol of S; let x be Element of the Sorts of A . s; funcx -term (A,V) -> c-Term of A,V equals :: MSATERM:def 3 root-tree [x,s]; correctness coherence root-tree [x,s] is c-Term of A,V; by Th6; end; :: deftheorem defines -term MSATERM:def_3_:_ for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being V16() ManySortedSet of the carrier of S for s being SortSymbol of S for x being Element of the Sorts of A . s holds x -term (A,V) = root-tree [x,s]; definition let S be non empty non void ManySortedSign ; let A be MSAlgebra over S; let V be V16() ManySortedSet of the carrier of S; let s be SortSymbol of S; let v be Element of V . s; funcv -term A -> c-Term of A,V equals :: MSATERM:def 4 root-tree [v,s]; correctness coherence root-tree [v,s] is c-Term of A,V; by Th8; end; :: deftheorem defines -term MSATERM:def_4_:_ for S being non empty non void ManySortedSign for A being MSAlgebra over S for V being V16() ManySortedSet of the carrier of S for s being SortSymbol of S for v being Element of V . s holds v -term A = root-tree [v,s]; definition let S be non empty non void ManySortedSign ; let V be V16() ManySortedSet of the carrier of S; let sy be NonTerminal of (DTConMSA V); let p be ArgumentSeq of sy; :: original:-tree redefine funcsy -tree p -> Term of S,V; coherence sy -tree p is Term of S,V proofend; end; scheme :: MSATERM:sch 3 TermInd2{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), F3() -> V16() ManySortedSet of the carrier of F1(), P1[ set ] } : for t being c-Term of F2(),F3() holds P1[t] provided A1: for s being SortSymbol of F1() for x being Element of the Sorts of F2() . s holds P1[x -term (F2(),F3())] and A2: for s being SortSymbol of F1() for v being Element of F3() . s holds P1[v -term F2()] and A3: for o being OperSymbol of F1() for p being ArgumentSeq of Sym (o,( the Sorts of F2() \/ F3())) st ( for t being c-Term of F2(),F3() st t in rng p holds P1[t] ) holds P1[(Sym (o,( the Sorts of F2() \/ F3()))) -tree p] proofend; begin theorem Th11: :: MSATERM:11 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for t being Term of S,V ex s being SortSymbol of S st t in FreeSort (V,s) proofend; theorem :: MSATERM:12 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for s being SortSymbol of S holds FreeSort (V,s) c= S -Terms V ; theorem :: MSATERM:13 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S holds S -Terms V = Union (FreeSort V) proofend; Lm7: for x being set holds not x in x ; definition let S be non empty non void ManySortedSign ; let V be V16() ManySortedSet of the carrier of S; let t be Term of S,V; func the_sort_of t -> SortSymbol of S means :Def5: :: MSATERM:def 5 t in FreeSort (V,it); existence ex b1 being SortSymbol of S st t in FreeSort (V,b1) by Th11; uniqueness for b1, b2 being SortSymbol of S st t in FreeSort (V,b1) & t in FreeSort (V,b2) holds b1 = b2 proofend; end; :: deftheorem Def5 defines the_sort_of MSATERM:def_5_:_ for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for t being Term of S,V for b4 being SortSymbol of S holds ( b4 = the_sort_of t iff t in FreeSort (V,b4) ); theorem Th14: :: MSATERM:14 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for t being Term of S,V for s being SortSymbol of S for v being Element of V . s st t = root-tree [v,s] holds the_sort_of t = s proofend; theorem Th15: :: MSATERM:15 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for A being MSAlgebra over S for t being c-Term of A,V for s being SortSymbol of S for x being set st x in the Sorts of A . s & t = root-tree [x,s] holds the_sort_of t = s proofend; theorem :: MSATERM:16 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for A being MSAlgebra over S for t being c-Term of A,V for s being SortSymbol of S for v being Element of V . s st t = root-tree [v,s] holds the_sort_of t = s proofend; theorem Th17: :: MSATERM:17 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for t being Term of S,V for o being OperSymbol of S st t . {} = [o, the carrier of S] holds the_sort_of t = the_result_sort_of o proofend; theorem :: MSATERM:18 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for A being non-empty MSAlgebra over S for s being SortSymbol of S for x being Element of the Sorts of A . s holds the_sort_of (x -term (A,V)) = s by Th15; theorem Th19: :: MSATERM:19 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for A being MSAlgebra over S for s being SortSymbol of S for v being Element of V . s holds the_sort_of (v -term A) = s proofend; theorem Th20: :: MSATERM:20 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for o being OperSymbol of S for p being ArgumentSeq of Sym (o,V) holds the_sort_of ((Sym (o,V)) -tree p) = the_result_sort_of o proofend; begin theorem Th21: :: MSATERM:21 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for o being OperSymbol of S for a being FinSequence of S -Terms V holds ( a is ArgumentSeq of Sym (o,V) iff Sym (o,V) ==> roots a ) proofend; Lm8: for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for o being OperSymbol of S for a being ArgumentSeq of Sym (o,V) holds ( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) & ( for i being Nat st i in dom a holds ex t being Term of S,V st ( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) ) ) proofend; theorem Th22: :: MSATERM:22 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for o being OperSymbol of S for a being ArgumentSeq of Sym (o,V) holds ( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) & ( for i being Nat st i in dom a holds a . i is Term of S,V ) ) proofend; theorem :: MSATERM:23 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for o being OperSymbol of S for a being ArgumentSeq of Sym (o,V) for i being Nat st i in dom a holds for t being Term of S,V st t = a . i holds ( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) proofend; theorem Th24: :: MSATERM:24 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for o being OperSymbol of S for a being FinSequence st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds ex t being Term of S,V st ( t = a . i & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds ex t being Term of S,V st ( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) holds a is ArgumentSeq of Sym (o,V) proofend; theorem :: MSATERM:25 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for o being OperSymbol of S for a being FinSequence of S -Terms V st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds for t being Term of S,V st t = a . i holds the_sort_of t = (the_arity_of o) . i or for i being Nat st i in dom a holds for t being Term of S,V st t = a . i holds the_sort_of t = (the_arity_of o) /. i ) holds a is ArgumentSeq of Sym (o,V) proofend; theorem Th26: :: MSATERM:26 for S being non empty non void ManySortedSign for V1, V2 being V16() ManySortedSet of the carrier of S st V1 c= V2 holds for t being Term of S,V1 holds t is Term of S,V2 proofend; theorem :: MSATERM:27 for S being non empty non void ManySortedSign for A being MSAlgebra over S for V being V16() ManySortedSet of the carrier of S for t being Term of S,V holds t is c-Term of A,V by Th26, PBOOLE:14; begin definition let S be non empty non void ManySortedSign ; let V be V16() ManySortedSet of the carrier of S; mode CompoundTerm of S,V -> Term of S,V means :: MSATERM:def 6 it . {} in [: the carrier' of S,{ the carrier of S}:]; existence ex b1 being Term of S,V st b1 . {} in [: the carrier' of S,{ the carrier of S}:] proofend; end; :: deftheorem defines CompoundTerm MSATERM:def_6_:_ for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for b3 being Term of S,V holds ( b3 is CompoundTerm of S,V iff b3 . {} in [: the carrier' of S,{ the carrier of S}:] ); definition let S be non empty non void ManySortedSign ; let V be V16() ManySortedSet of the carrier of S; mode SetWithCompoundTerm of S,V -> non empty Subset of (S -Terms V) means :: MSATERM:def 7 ex t being CompoundTerm of S,V st t in it; existence ex b1 being non empty Subset of (S -Terms V) ex t being CompoundTerm of S,V st t in b1 proofend; end; :: deftheorem defines SetWithCompoundTerm MSATERM:def_7_:_ for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for b3 being non empty Subset of (S -Terms V) holds ( b3 is SetWithCompoundTerm of S,V iff ex t being CompoundTerm of S,V st t in b3 ); theorem :: MSATERM:28 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for t being Term of S,V st not t is root holds t is CompoundTerm of S,V proofend; Lm9: for n being Element of NAT for p being FinSequence st n < len p holds ( n + 1 in dom p & p . (n + 1) in rng p ) proofend; theorem Th29: :: MSATERM:29 for S being non empty non void ManySortedSign for V being V16() ManySortedSet of the carrier of S for t being Term of S,V for p being Node of t holds t | p is Term of S,V proofend; definition let S be non empty non void ManySortedSign ; let V be V16() ManySortedSet of the carrier of S; let t be Term of S,V; let p be Node of t; :: original:| redefine funct | p -> Term of S,V; coherence t | p is Term of S,V by Th29; end; begin definition let S be non empty non void ManySortedSign ; let A be MSAlgebra over S; mode Variables of A -> V16() ManySortedSet of the carrier of S means :Def8: :: MSATERM:def 8 it misses the Sorts of A; existence ex b1 being V16() ManySortedSet of the carrier of S st b1 misses the Sorts of A proofend; end; :: deftheorem Def8 defines Variables MSATERM:def_8_:_ for S being non empty non void ManySortedSign for A being MSAlgebra over S for b3 being V16() ManySortedSet of the carrier of S holds ( b3 is Variables of A iff b3 misses the Sorts of A ); theorem Th30: :: MSATERM:30 for S being non empty non void ManySortedSign for A being MSAlgebra over S for V being Variables of A for s being SortSymbol of S for x being set st x in the Sorts of A . s holds for v being Element of V . s holds x <> v proofend; definition let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; let V be V16() ManySortedSet of the carrier of S; let t be c-Term of A,V; let f be ManySortedFunction of V, the Sorts of A; let vt be finite DecoratedTree; predvt is_an_evaluation_of t,f means :Def9: :: MSATERM:def 9 ( dom vt = dom t & ( for p being Node of vt holds ( ( for s being SortSymbol of S for v being Element of V . s st t . p = [v,s] holds vt . p = (f . s) . v ) & ( for s being SortSymbol of S for x being Element of the Sorts of A . s st t . p = [x,s] holds vt . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds vt . p = (Den (o,A)) . (succ (vt,p)) ) ) ) ); end; :: deftheorem Def9 defines is_an_evaluation_of MSATERM:def_9_:_ for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being V16() ManySortedSet of the carrier of S for t being c-Term of A,V for f being ManySortedFunction of V, the Sorts of A for vt being finite DecoratedTree holds ( vt is_an_evaluation_of t,f iff ( dom vt = dom t & ( for p being Node of vt holds ( ( for s being SortSymbol of S for v being Element of V . s st t . p = [v,s] holds vt . p = (f . s) . v ) & ( for s being SortSymbol of S for x being Element of the Sorts of A . s st t . p = [x,s] holds vt . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds vt . p = (Den (o,A)) . (succ (vt,p)) ) ) ) ) ); theorem Th31: :: MSATERM:31 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being Variables of A for t being c-Term of A,V for f being ManySortedFunction of V, the Sorts of A for s being SortSymbol of S for x being Element of the Sorts of A . s st t = root-tree [x,s] holds root-tree x is_an_evaluation_of t,f proofend; theorem Th32: :: MSATERM:32 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being Variables of A for t being c-Term of A,V for f being ManySortedFunction of V, the Sorts of A for s being SortSymbol of S for v being Element of V . s st t = root-tree [v,s] holds root-tree ((f . s) . v) is_an_evaluation_of t,f proofend; theorem Th33: :: MSATERM:33 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being Variables of A for f being ManySortedFunction of V, the Sorts of A for o being OperSymbol of S for p being ArgumentSeq of o,A,V for q being DTree-yielding FinSequence st len q = len p & ( for i being Nat for t being c-Term of A,V st i in dom p & t = p . i holds ex vt being finite DecoratedTree st ( vt = q . i & vt is_an_evaluation_of t,f ) ) holds ex vt being finite DecoratedTree st ( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f ) proofend; theorem Th34: :: MSATERM:34 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being Variables of A for f being ManySortedFunction of V, the Sorts of A for t being c-Term of A,V for e being finite DecoratedTree st e is_an_evaluation_of t,f holds for p being Node of t for n being Node of e st n = p holds e | n is_an_evaluation_of t | p,f proofend; theorem Th35: :: MSATERM:35 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being Variables of A for f being ManySortedFunction of V, the Sorts of A for o being OperSymbol of S for p being ArgumentSeq of o,A,V for vt being finite DecoratedTree st vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f holds ex q being DTree-yielding FinSequence st ( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat for t being c-Term of A,V st i in dom p & t = p . i holds ex vt being finite DecoratedTree st ( vt = q . i & vt is_an_evaluation_of t,f ) ) ) proofend; theorem Th36: :: MSATERM:36 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being Variables of A for t being c-Term of A,V for f being ManySortedFunction of V, the Sorts of A ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f proofend; theorem Th37: :: MSATERM:37 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being Variables of A for t being c-Term of A,V for f being ManySortedFunction of V, the Sorts of A for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds e1 = e2 proofend; theorem Th38: :: MSATERM:38 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being Variables of A for t being c-Term of A,V for f being ManySortedFunction of V, the Sorts of A for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds vt . {} in the Sorts of A . (the_sort_of t) proofend; definition let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; let V be Variables of A; let t be c-Term of A,V; let f be ManySortedFunction of V, the Sorts of A; funct @ f -> Element of the Sorts of A . (the_sort_of t) means :Def10: :: MSATERM:def 10 ex vt being finite DecoratedTree st ( vt is_an_evaluation_of t,f & it = vt . {} ); existence ex b1 being Element of the Sorts of A . (the_sort_of t) ex vt being finite DecoratedTree st ( vt is_an_evaluation_of t,f & b1 = vt . {} ) proofend; uniqueness for b1, b2 being Element of the Sorts of A . (the_sort_of t) st ex vt being finite DecoratedTree st ( vt is_an_evaluation_of t,f & b1 = vt . {} ) & ex vt being finite DecoratedTree st ( vt is_an_evaluation_of t,f & b2 = vt . {} ) holds b1 = b2 by Th37; end; :: deftheorem Def10 defines @ MSATERM:def_10_:_ for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being Variables of A for t being c-Term of A,V for f being ManySortedFunction of V, the Sorts of A for b6 being Element of the Sorts of A . (the_sort_of t) holds ( b6 = t @ f iff ex vt being finite DecoratedTree st ( vt is_an_evaluation_of t,f & b6 = vt . {} ) ); theorem Th39: :: MSATERM:39 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being Variables of A for f being ManySortedFunction of V, the Sorts of A for t being c-Term of A,V for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds t @ f = vt . {} proofend; theorem :: MSATERM:40 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being Variables of A for f being ManySortedFunction of V, the Sorts of A for t being c-Term of A,V for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds for p being Node of t holds vt . p = (t | p) @ f proofend; theorem :: MSATERM:41 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being Variables of A for f being ManySortedFunction of V, the Sorts of A for s being SortSymbol of S for x being Element of the Sorts of A . s holds (x -term (A,V)) @ f = x proofend; theorem :: MSATERM:42 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being Variables of A for f being ManySortedFunction of V, the Sorts of A for s being SortSymbol of S for v being Element of V . s holds (v -term A) @ f = (f . s) . v proofend; theorem :: MSATERM:43 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being Variables of A for f being ManySortedFunction of V, the Sorts of A for o being OperSymbol of S for p being ArgumentSeq of o,A,V for q being FinSequence st len q = len p & ( for i being Nat st i in dom p holds for t being c-Term of A,V st t = p . i holds q . i = t @ f ) holds ((Sym (o,( the Sorts of A \/ V))) -tree p) @ f = (Den (o,A)) . q proofend;