:: MSATERM semantic presentation 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 ) proof let n be set ; ::_thesis: for p being FinSequence st n in dom p holds ex k being Element of NAT st ( n = k + 1 & k < len p ) let p be FinSequence; ::_thesis: ( n in dom p implies ex k being Element of NAT st ( n = k + 1 & k < len p ) ) assume A1: n in dom p ; ::_thesis: ex k being Element of NAT st ( n = k + 1 & k < len p ) then reconsider n = n as Element of NAT ; n >= 1 by A1, FINSEQ_3:25; then consider k being Nat such that A2: n = 1 + k by NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; take k ; ::_thesis: ( n = k + 1 & k < len p ) n <= len p by A1, FINSEQ_3:25; hence ( n = k + 1 & k < len p ) by A2, NAT_1:13; ::_thesis: verum end; 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) proof A1: the carrier of S in { the carrier of S} by TARSKI:def_1; A2: NonTerminals (DTConMSA V) = [: the carrier' of S,{ the carrier of S}:] by MSAFREE:6; Sym (o,V) = [o, the carrier of S] by MSAFREE:def_9; hence Sym (o,V) is NonTerminal of (DTConMSA V) by A2, A1, ZFMISC_1:87; ::_thesis: verum end; 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 proof set q = the SubtreeSeq of sy; the SubtreeSeq of sy is FinSequence of S -Terms V ; hence ex b1 being FinSequence of S -Terms V st b1 is SubtreeSeq of sy ; ::_thesis: verum end; 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) ) proof let S be non empty non void ManySortedSign ; ::_thesis: 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) ) let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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) ) let o be OperSymbol of S; ::_thesis: 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) ) let a be FinSequence; ::_thesis: ( ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym (o,V) ) A1: [o, the carrier of S] = Sym (o,V) by MSAFREE:def_9; A2: S -Terms V = TS (DTConMSA V) ; hereby ::_thesis: ( a is ArgumentSeq of Sym (o,V) implies ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) ) assume [o, the carrier of S] -tree a in S -Terms V ; ::_thesis: ( a is DTree-yielding implies a is ArgumentSeq of Sym (o,V) ) then reconsider t = [o, the carrier of S] -tree a as Element of TS (DTConMSA V) ; assume A3: a is DTree-yielding ; ::_thesis: a is ArgumentSeq of Sym (o,V) then t . {} = [o, the carrier of S] by TREES_4:def_4; then consider p being FinSequence of TS (DTConMSA V) such that A4: t = (Sym (o,V)) -tree p and A5: Sym (o,V) ==> roots p by A1, DTCONSTR:10; a = p by A3, A4, TREES_4:15; then a is SubtreeSeq of Sym (o,V) by A5, DTCONSTR:def_6; hence a is ArgumentSeq of Sym (o,V) by A2, Def2; ::_thesis: verum end; assume a is ArgumentSeq of Sym (o,V) ; ::_thesis: ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) then reconsider a = a as ArgumentSeq of Sym (o,V) ; reconsider p = a as FinSequence of TS (DTConMSA V) by Def1; p is SubtreeSeq of Sym (o,V) by Def2; then Sym (o,V) ==> roots p by DTCONSTR:def_6; hence ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) by A1, DTCONSTR:def_1; ::_thesis: verum end; 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] proof set X = F2(); set G = DTConMSA F2(); A3: for nt being Symbol of (DTConMSA F2()) for ts being FinSequence of TS (DTConMSA F2()) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA F2()) st t in rng ts holds P1[t] ) holds P1[nt -tree ts] proof let nt be Symbol of (DTConMSA F2()); ::_thesis: for ts being FinSequence of TS (DTConMSA F2()) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA F2()) st t in rng ts holds P1[t] ) holds P1[nt -tree ts] let ts be FinSequence of TS (DTConMSA F2()); ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA F2()) st t in rng ts holds P1[t] ) implies P1[nt -tree ts] ) assume that A4: nt ==> roots ts and A5: for t being DecoratedTree of the carrier of (DTConMSA F2()) st t in rng ts holds P1[t] ; ::_thesis: P1[nt -tree ts] nt in { s where s is Symbol of (DTConMSA F2()) : ex n being FinSequence st s ==> n } by A4; then reconsider sy = nt as NonTerminal of (DTConMSA F2()) by LANG1:def_3; reconsider p = ts as FinSequence of F1() -Terms F2() ; sy in [: the carrier' of F1(),{ the carrier of F1()}:] by Lm5; then consider o being OperSymbol of F1(), x2 being Element of { the carrier of F1()} such that A6: sy = [o,x2] by DOMAIN_1:1; A7: x2 = the carrier of F1() by TARSKI:def_1; [o, the carrier of F1()] = Sym (o,F2()) by MSAFREE:def_9; then ts is SubtreeSeq of Sym (o,F2()) by A4, A6, A7, DTCONSTR:def_6; then reconsider p = p as ArgumentSeq of Sym (o,F2()) by Def2; for t being Term of F1(),F2() st t in rng p holds P1[t] by A5; hence P1[nt -tree ts] by A2, A6, A7; ::_thesis: verum end; A8: for s being Symbol of (DTConMSA F2()) st s in Terminals (DTConMSA F2()) holds P1[ root-tree s] proof let x be Symbol of (DTConMSA F2()); ::_thesis: ( x in Terminals (DTConMSA F2()) implies P1[ root-tree x] ) assume x in Terminals (DTConMSA F2()) ; ::_thesis: P1[ root-tree x] then ex s being SortSymbol of F1() ex v being Element of F2() . s st x = [v,s] by Lm3; hence P1[ root-tree x] by A1; ::_thesis: verum end; for t being DecoratedTree of the carrier of (DTConMSA F2()) st t in TS (DTConMSA F2()) holds P1[t] from DTCONSTR:sch_7(A8, A3); hence for t being Term of F1(),F2() holds P1[t] ; ::_thesis: verum 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; 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] proof set X = the Sorts of F2() \/ F3(); set G = DTConMSA ( the Sorts of F2() \/ F3()); A4: for nt being Symbol of (DTConMSA ( the Sorts of F2() \/ F3())) for ts being FinSequence of TS (DTConMSA ( the Sorts of F2() \/ F3())) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) st t in rng ts holds P1[t] ) holds P1[nt -tree ts] proof let nt be Symbol of (DTConMSA ( the Sorts of F2() \/ F3())); ::_thesis: for ts being FinSequence of TS (DTConMSA ( the Sorts of F2() \/ F3())) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) st t in rng ts holds P1[t] ) holds P1[nt -tree ts] let ts be FinSequence of TS (DTConMSA ( the Sorts of F2() \/ F3())); ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) st t in rng ts holds P1[t] ) implies P1[nt -tree ts] ) assume that A5: nt ==> roots ts and A6: for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) st t in rng ts holds P1[t] ; ::_thesis: P1[nt -tree ts] nt in { s where s is Symbol of (DTConMSA ( the Sorts of F2() \/ F3())) : ex n being FinSequence st s ==> n } by A5; then reconsider sy = nt as NonTerminal of (DTConMSA ( the Sorts of F2() \/ F3())) by LANG1:def_3; reconsider p = ts as FinSequence of F1() -Terms ( the Sorts of F2() \/ F3()) ; sy in [: the carrier' of F1(),{ the carrier of F1()}:] by Lm5; then consider o being OperSymbol of F1(), x2 being Element of { the carrier of F1()} such that A7: sy = [o,x2] by DOMAIN_1:1; A8: [o, the carrier of F1()] = Sym (o,( the Sorts of F2() \/ F3())) by MSAFREE:def_9; A9: x2 = the carrier of F1() by TARSKI:def_1; then ts is SubtreeSeq of Sym (o,( the Sorts of F2() \/ F3())) by A5, A7, A8, DTCONSTR:def_6; then reconsider p = p as ArgumentSeq of Sym (o,( the Sorts of F2() \/ F3())) by Def2; for t being c-Term of F2(),F3() st t in rng p holds P1[t] by A6; hence P1[nt -tree ts] by A3, A7, A9, A8; ::_thesis: verum end; A10: for s being Symbol of (DTConMSA ( the Sorts of F2() \/ F3())) st s in Terminals (DTConMSA ( the Sorts of F2() \/ F3())) holds P1[ root-tree s] proof let x be Symbol of (DTConMSA ( the Sorts of F2() \/ F3())); ::_thesis: ( x in Terminals (DTConMSA ( the Sorts of F2() \/ F3())) implies P1[ root-tree x] ) assume x in Terminals (DTConMSA ( the Sorts of F2() \/ F3())) ; ::_thesis: P1[ root-tree x] then ( ex s being SortSymbol of F1() ex a being set st ( a in the Sorts of F2() . s & x = [a,s] ) or ex s being SortSymbol of F1() ex v being Element of F3() . s st x = [v,s] ) by Lm4; hence P1[ root-tree x] by A1, A2; ::_thesis: verum end; for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) st t in TS (DTConMSA ( the Sorts of F2() \/ F3())) holds P1[t] from DTCONSTR:sch_7(A10, A4); hence for t being c-Term of F2(),F3() holds P1[t] ; ::_thesis: verum end; 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) proof reconsider t = t as Element of TS (DTConMSA V) ; reconsider t = t as DecoratedTree of the carrier of (DTConMSA V) ; reconsider p = p as Node of t ; t . p = t . p ; hence t . p is Symbol of (DTConMSA V) ; ::_thesis: verum end; 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}:] ) proof let S be non empty non void ManySortedSign ; ::_thesis: 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}:] ) let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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}:] ) let t be Term of S,V; ::_thesis: ( 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}:] ) set G = DTConMSA V; A1: the carrier of (DTConMSA V) = (Terminals (DTConMSA V)) \/ (NonTerminals (DTConMSA V)) by LANG1:1; reconsider e = {} as Node of t by TREES_1:22; NonTerminals (DTConMSA V) = [: the carrier' of S,{ the carrier of S}:] by MSAFREE:6; then ( t . e in Terminals (DTConMSA V) or t . e in [: the carrier' of S,{ the carrier of S}:] ) by A1, XBOOLE_0:def_3; hence ( 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}:] ) by Lm3; ::_thesis: verum end; 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}:] ) proof let S be non empty non void ManySortedSign ; ::_thesis: 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}:] ) let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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}:] ) let A be MSAlgebra over S; ::_thesis: 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}:] ) let t be c-Term of A,V; ::_thesis: ( 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}:] ) set G = DTConMSA ( the Sorts of A \/ V); A1: the carrier of (DTConMSA ( the Sorts of A \/ V)) = (Terminals (DTConMSA ( the Sorts of A \/ V))) \/ (NonTerminals (DTConMSA ( the Sorts of A \/ V))) by LANG1:1; reconsider e = {} as Node of t by TREES_1:22; NonTerminals (DTConMSA ( the Sorts of A \/ V)) = [: the carrier' of S,{ the carrier of S}:] by MSAFREE:6; then ( t . e in Terminals (DTConMSA ( the Sorts of A \/ V)) or t . e in [: the carrier' of S,{ the carrier of S}:] ) by A1, XBOOLE_0:def_3; hence ( 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}:] ) by Lm4; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let V be V16() ManySortedSet of the carrier of S; ::_thesis: for s being SortSymbol of S for v being Element of V . s holds root-tree [v,s] is Term of S,V let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds root-tree [v,s] is Term of S,V let v be Element of V . s; ::_thesis: root-tree [v,s] is Term of S,V reconsider vs = [v,s] as Terminal of (DTConMSA V) by MSAFREE:7; root-tree vs in TS (DTConMSA V) ; hence root-tree [v,s] is Term of S,V ; ::_thesis: verum end; 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] proof let S be non empty non void ManySortedSign ; ::_thesis: 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] let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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] let t be Term of S,V; ::_thesis: for s being SortSymbol of S for v being Element of V . s st t . {} = [v,s] holds t = root-tree [v,s] let s be SortSymbol of S; ::_thesis: for v being Element of V . s st t . {} = [v,s] holds t = root-tree [v,s] let x be Element of V . s; ::_thesis: ( t . {} = [x,s] implies t = root-tree [x,s] ) set G = DTConMSA V; reconsider a = [x,s] as Terminal of (DTConMSA V) by Lm3; reconsider t = t as Element of TS (DTConMSA V) ; ( t . {} = a implies t = root-tree a ) by DTCONSTR:9; hence ( t . {} = [x,s] implies t = root-tree [x,s] ) ; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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 let A be MSAlgebra over S; ::_thesis: 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 let s be SortSymbol of S; ::_thesis: for x being set st x in the Sorts of A . s holds root-tree [x,s] is c-Term of A,V let x be set ; ::_thesis: ( x in the Sorts of A . s implies root-tree [x,s] is c-Term of A,V ) A1: ( the Sorts of A \/ V) . s = ( the Sorts of A . s) \/ (V . s) by PBOOLE:def_4; assume x in the Sorts of A . s ; ::_thesis: root-tree [x,s] is c-Term of A,V then x in ( the Sorts of A \/ V) . s by A1, XBOOLE_0:def_3; then reconsider xs = [x,s] as Terminal of (DTConMSA ( the Sorts of A \/ V)) by MSAFREE:7; root-tree xs in TS (DTConMSA ( the Sorts of A \/ V)) ; hence root-tree [x,s] is c-Term of A,V ; ::_thesis: verum end; 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] proof let S be non empty non void ManySortedSign ; ::_thesis: 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] let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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] let A be MSAlgebra over S; ::_thesis: 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] let t be c-Term of A,V; ::_thesis: 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] let s be SortSymbol of S; ::_thesis: for x being set st x in the Sorts of A . s & t . {} = [x,s] holds t = root-tree [x,s] let x be set ; ::_thesis: ( x in the Sorts of A . s & t . {} = [x,s] implies t = root-tree [x,s] ) set G = DTConMSA ( the Sorts of A \/ V); reconsider t = t as Element of TS (DTConMSA ( the Sorts of A \/ V)) ; assume x in the Sorts of A . s ; ::_thesis: ( not t . {} = [x,s] or t = root-tree [x,s] ) then reconsider a = [x,s] as Terminal of (DTConMSA ( the Sorts of A \/ V)) by Lm4; ( t . {} = a implies t = root-tree a ) by DTCONSTR:9; hence ( not t . {} = [x,s] or t = root-tree [x,s] ) ; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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 let A be MSAlgebra over S; ::_thesis: for s being SortSymbol of S for v being Element of V . s holds root-tree [v,s] is c-Term of A,V let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds root-tree [v,s] is c-Term of A,V let v be Element of V . s; ::_thesis: root-tree [v,s] is c-Term of A,V ( the Sorts of A \/ V) . s = ( the Sorts of A . s) \/ (V . s) by PBOOLE:def_4; then v in ( the Sorts of A \/ V) . s by XBOOLE_0:def_3; then reconsider vs = [v,s] as Terminal of (DTConMSA ( the Sorts of A \/ V)) by MSAFREE:7; root-tree vs in TS (DTConMSA ( the Sorts of A \/ V)) ; hence root-tree [v,s] is c-Term of A,V ; ::_thesis: verum end; 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] proof let S be non empty non void ManySortedSign ; ::_thesis: 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] let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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] let A be MSAlgebra over S; ::_thesis: 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] let t be c-Term of A,V; ::_thesis: for s being SortSymbol of S for v being Element of V . s st t . {} = [v,s] holds t = root-tree [v,s] let s be SortSymbol of S; ::_thesis: for v being Element of V . s st t . {} = [v,s] holds t = root-tree [v,s] let x be Element of V . s; ::_thesis: ( t . {} = [x,s] implies t = root-tree [x,s] ) set G = DTConMSA ( the Sorts of A \/ V); reconsider a = [x,s] as Terminal of (DTConMSA ( the Sorts of A \/ V)) by Lm4; reconsider t = t as Element of TS (DTConMSA ( the Sorts of A \/ V)) ; ( t . {} = a implies t = root-tree a ) by DTCONSTR:9; hence ( t . {} = [x,s] implies t = root-tree [x,s] ) ; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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 let t be Term of S,V; ::_thesis: 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 let o be OperSymbol of S; ::_thesis: ( t . {} = [o, the carrier of S] implies ex a being ArgumentSeq of Sym (o,V) st t = [o, the carrier of S] -tree a ) assume A1: t . {} = [o, the carrier of S] ; ::_thesis: ex a being ArgumentSeq of Sym (o,V) st t = [o, the carrier of S] -tree a set X = V; set G = DTConMSA V; reconsider t = t as Element of TS (DTConMSA V) ; [o, the carrier of S] = Sym (o,V) by MSAFREE:def_9; then consider p being FinSequence of TS (DTConMSA V) such that A2: t = (Sym (o,V)) -tree p and A3: Sym (o,V) ==> roots p by A1, DTCONSTR:10; reconsider a = p as FinSequence of S -Terms V ; a is SubtreeSeq of Sym (o,V) by A3, DTCONSTR:def_6; then reconsider a = a as ArgumentSeq of Sym (o,V) by Def2; take a ; ::_thesis: t = [o, the carrier of S] -tree a thus t = [o, the carrier of S] -tree a by A2, MSAFREE:def_9; ::_thesis: verum end; 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 proof sy in [: the carrier' of S,{ the carrier of S}:] by Lm5; then consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that A1: sy = [o,x2] by DOMAIN_1:1; A2: x2 = the carrier of S by TARSKI:def_1; then sy = Sym (o,V) by A1, MSAFREE:def_9; hence sy -tree p is Term of S,V by A1, A2, Th1; ::_thesis: verum end; 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] proof A4: now__::_thesis:_for_s_being_SortSymbol_of_F1() for_x_being_Element_of_the_Sorts_of_F2()_._s_holds_P1[_root-tree_[x,s]] let s be SortSymbol of F1(); ::_thesis: for x being Element of the Sorts of F2() . s holds P1[ root-tree [x,s]] let x be Element of the Sorts of F2() . s; ::_thesis: P1[ root-tree [x,s]] P1[x -term (F2(),F3())] by A1; hence P1[ root-tree [x,s]] ; ::_thesis: verum end; A5: now__::_thesis:_for_s_being_SortSymbol_of_F1() for_v_being_Element_of_F3()_._s_holds_P1[_root-tree_[v,s]] let s be SortSymbol of F1(); ::_thesis: for v being Element of F3() . s holds P1[ root-tree [v,s]] let v be Element of F3() . s; ::_thesis: P1[ root-tree [v,s]] P1[v -term F2()] by A2; hence P1[ root-tree [v,s]] ; ::_thesis: verum end; A6: 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] by A3; for t being c-Term of F2(),F3() holds P1[t] from MSATERM:sch_2(A4, A5, A6); hence for t being c-Term of F2(),F3() holds P1[t] ; ::_thesis: verum end; 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) proof let S be non empty non void ManySortedSign ; ::_thesis: 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) let V be V16() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,V ex s being SortSymbol of S st t in FreeSort (V,s) let t be Term of S,V; ::_thesis: ex s being SortSymbol of S st t in FreeSort (V,s) set X = V; set G = DTConMSA V; reconsider e = {} as Node of t by TREES_1:22; percases ( t . {} is Terminal of (DTConMSA V) or not t . {} is Terminal of (DTConMSA V) ) ; suppose t . {} is Terminal of (DTConMSA V) ; ::_thesis: ex s being SortSymbol of S st t in FreeSort (V,s) then reconsider ts = t . {} as Terminal of (DTConMSA V) ; consider s being SortSymbol of S, x being set such that A1: x in V . s and A2: ts = [x,s] by MSAFREE:7; take s ; ::_thesis: t in FreeSort (V,s) t = root-tree [x,s] by A2, DTCONSTR:9; then t in { a where a is Element of TS (DTConMSA V) : ( ex x being set st ( x in V . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } by A1; hence t in FreeSort (V,s) by MSAFREE:def_10; ::_thesis: verum end; suppose t . {} is not Terminal of (DTConMSA V) ; ::_thesis: ex s being SortSymbol of S st t in FreeSort (V,s) then reconsider nt = t . e as NonTerminal of (DTConMSA V) by Lm6; nt in [: the carrier' of S,{ the carrier of S}:] by Lm5; then consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that A3: nt = [o,x2] by DOMAIN_1:1; take s = the_result_sort_of o; ::_thesis: t in FreeSort (V,s) x2 = the carrier of S by TARSKI:def_1; then t in { a where a is Element of TS (DTConMSA V) : ( ex x being set st ( x in V . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } by A3; hence t in FreeSort (V,s) by MSAFREE:def_10; ::_thesis: verum end; end; end; 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) proof let S be non empty non void ManySortedSign ; ::_thesis: for V being V16() ManySortedSet of the carrier of S holds S -Terms V = Union (FreeSort V) let V be V16() ManySortedSet of the carrier of S; ::_thesis: S -Terms V = Union (FreeSort V) set T = S -Terms V; set X = V; A1: dom (FreeSort V) = the carrier of S by PARTFUN1:def_2; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: Union (FreeSort V) c= S -Terms V let x be set ; ::_thesis: ( x in S -Terms V implies x in Union (FreeSort V) ) assume x in S -Terms V ; ::_thesis: x in Union (FreeSort V) then reconsider t = x as Term of S,V ; consider s being SortSymbol of S such that A2: t in FreeSort (V,s) by Th11; FreeSort (V,s) = (FreeSort V) . s by MSAFREE:def_11; hence x in Union (FreeSort V) by A1, A2, CARD_5:2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (FreeSort V) or x in S -Terms V ) assume x in Union (FreeSort V) ; ::_thesis: x in S -Terms V then consider y being set such that A3: y in dom (FreeSort V) and A4: x in (FreeSort V) . y by CARD_5:2; reconsider y = y as SortSymbol of S by A3, PARTFUN1:def_2; x in FreeSort (V,y) by A4, MSAFREE:def_11; hence x in S -Terms V ; ::_thesis: verum end; 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 proof set X = V; let s1, s2 be SortSymbol of S; ::_thesis: ( t in FreeSort (V,s1) & t in FreeSort (V,s2) implies s1 = s2 ) assume that A1: t in FreeSort (V,s1) and A2: t in FreeSort (V,s2) ; ::_thesis: s1 = s2 FreeSort (V,s1) = { a where a is Element of TS (DTConMSA V) : ( ex x being set st ( x in V . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = s1 ) ) } by MSAFREE:def_10; then consider a1 being Element of TS (DTConMSA V) such that A3: t = a1 and A4: ( ex x being set st ( x in V . s1 & a1 = root-tree [x,s1] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a1 . {} & the_result_sort_of o = s1 ) ) by A1; FreeSort (V,s2) = { a where a is Element of TS (DTConMSA V) : ( ex x being set st ( x in V . s2 & a = root-tree [x,s2] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = s2 ) ) } by MSAFREE:def_10; then consider a2 being Element of TS (DTConMSA V) such that A5: t = a2 and A6: ( ex x being set st ( x in V . s2 & a2 = root-tree [x,s2] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a2 . {} & the_result_sort_of o = s2 ) ) by A2; percases ( ex x being set st ( x in V . s1 & a1 = root-tree [x,s1] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a1 . {} & the_result_sort_of o = s1 ) ) by A4; suppose ex x being set st ( x in V . s1 & a1 = root-tree [x,s1] ) ; ::_thesis: s1 = s2 then consider x1 being set such that x1 in V . s1 and A7: a1 = root-tree [x1,s1] ; now__::_thesis:_for_o_being_OperSymbol_of_S_holds_not_[o,_the_carrier_of_S]_=_[x1,s1] let o be OperSymbol of S; ::_thesis: not [o, the carrier of S] = [x1,s1] assume [o, the carrier of S] = [x1,s1] ; ::_thesis: contradiction then the carrier of S = s1 by XTUPLE_0:1; hence contradiction by Lm7; ::_thesis: verum end; then consider x2 being set such that x2 in V . s2 and A8: a2 = root-tree [x2,s2] by A3, A5, A6, A7, TREES_4:3; [x1,s1] = [x2,s2] by A3, A5, A7, A8, TREES_4:4; hence s1 = s2 by XTUPLE_0:1; ::_thesis: verum end; suppose ex o being OperSymbol of S st ( [o, the carrier of S] = a1 . {} & the_result_sort_of o = s1 ) ; ::_thesis: s1 = s2 then consider o1 being OperSymbol of S such that A9: [o1, the carrier of S] = a1 . {} and A10: the_result_sort_of o1 = s1 ; now__::_thesis:_for_x2_being_set_holds_ (_not_x2_in_V_._s2_or_not_a2_=_root-tree_[x2,s2]_) given x2 being set such that x2 in V . s2 and A11: a2 = root-tree [x2,s2] ; ::_thesis: contradiction [o1, the carrier of S] = [x2,s2] by A3, A5, A9, A11, TREES_4:3; then the carrier of S = s2 by XTUPLE_0:1; hence contradiction by Lm7; ::_thesis: verum end; hence s1 = s2 by A3, A5, A6, A9, A10, XTUPLE_0:1; ::_thesis: verum end; end; end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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 let t be Term of S,V; ::_thesis: 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 let s be SortSymbol of S; ::_thesis: for v being Element of V . s st t = root-tree [v,s] holds the_sort_of t = s let x be Element of V . s; ::_thesis: ( t = root-tree [x,s] implies the_sort_of t = s ) set X = V; set G = DTConMSA V; set tst = the_sort_of t; A1: FreeSort (V,(the_sort_of t)) = { a where a is Element of TS (DTConMSA V) : ( ex x being set st ( x in V . (the_sort_of t) & a = root-tree [x,(the_sort_of t)] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = the_sort_of t ) ) } by MSAFREE:def_10; t in FreeSort (V,(the_sort_of t)) by Def5; then consider a being Element of TS (DTConMSA V) such that A2: t = a and A3: ( ex x being set st ( x in V . (the_sort_of t) & a = root-tree [x,(the_sort_of t)] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = the_sort_of t ) ) by A1; A4: [x,s] in Terminals (DTConMSA V) by Lm3; assume A5: t = root-tree [x,s] ; ::_thesis: the_sort_of t = s then t . {} = [x,s] by TREES_4:3; then t . {} is not NonTerminal of (DTConMSA V) by A4, Lm6; then A6: not t . {} in [: the carrier' of S,{ the carrier of S}:] by Lm5; the carrier of S in { the carrier of S} by TARSKI:def_1; then consider y being set such that y in V . (the_sort_of t) and A7: a = root-tree [y,(the_sort_of t)] by A2, A3, A6, ZFMISC_1:87; [y,(the_sort_of t)] = [x,s] by A2, A5, A7, TREES_4:4; hence the_sort_of t = s by XTUPLE_0:1; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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 let A be MSAlgebra over S; ::_thesis: 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 let t be c-Term of A,V; ::_thesis: 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 let s be SortSymbol of S; ::_thesis: for x being set st x in the Sorts of A . s & t = root-tree [x,s] holds the_sort_of t = s let x be set ; ::_thesis: ( x in the Sorts of A . s & t = root-tree [x,s] implies the_sort_of t = s ) assume x in the Sorts of A . s ; ::_thesis: ( not t = root-tree [x,s] or the_sort_of t = s ) then x in ( the Sorts of A . s) \/ (V . s) by XBOOLE_0:def_3; then x in ( the Sorts of A \/ V) . s by PBOOLE:def_4; hence ( not t = root-tree [x,s] or the_sort_of t = s ) by Th14; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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 let A be MSAlgebra over S; ::_thesis: 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 let t be c-Term of A,V; ::_thesis: 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 let s be SortSymbol of S; ::_thesis: for v being Element of V . s st t = root-tree [v,s] holds the_sort_of t = s let x be Element of V . s; ::_thesis: ( t = root-tree [x,s] implies the_sort_of t = s ) x in ( the Sorts of A . s) \/ (V . s) by XBOOLE_0:def_3; then x in ( the Sorts of A \/ V) . s by PBOOLE:def_4; hence ( t = root-tree [x,s] implies the_sort_of t = s ) by Th14; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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 let t be Term of S,V; ::_thesis: for o being OperSymbol of S st t . {} = [o, the carrier of S] holds the_sort_of t = the_result_sort_of o let o be OperSymbol of S; ::_thesis: ( t . {} = [o, the carrier of S] implies the_sort_of t = the_result_sort_of o ) set X = V; set G = DTConMSA V; set tst = the_sort_of t; A1: FreeSort (V,(the_sort_of t)) = { a where a is Element of TS (DTConMSA V) : ( ex x being set st ( x in V . (the_sort_of t) & a = root-tree [x,(the_sort_of t)] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = the_sort_of t ) ) } by MSAFREE:def_10; t in FreeSort (V,(the_sort_of t)) by Def5; then consider a being Element of TS (DTConMSA V) such that A2: t = a and A3: ( ex x being set st ( x in V . (the_sort_of t) & a = root-tree [x,(the_sort_of t)] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = the_sort_of t ) ) by A1; assume A4: t . {} = [o, the carrier of S] ; ::_thesis: the_sort_of t = the_result_sort_of o percases ( ex x being set st ( x in V . (the_sort_of t) & a = root-tree [x,(the_sort_of t)] ) or ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = the_sort_of t ) ) by A3; suppose ex x being set st ( x in V . (the_sort_of t) & a = root-tree [x,(the_sort_of t)] ) ; ::_thesis: the_sort_of t = the_result_sort_of o then consider x being set such that x in V . (the_sort_of t) and A5: a = root-tree [x,(the_sort_of t)] ; [o, the carrier of S] = [x,(the_sort_of t)] by A2, A4, A5, TREES_4:3; then the carrier of S = the_sort_of t by XTUPLE_0:1; hence the_sort_of t = the_result_sort_of o by Lm7; ::_thesis: verum end; suppose ex o being OperSymbol of S st ( [o, the carrier of S] = a . {} & the_result_sort_of o = the_sort_of t ) ; ::_thesis: the_sort_of t = the_result_sort_of o hence the_sort_of t = the_result_sort_of o by A2, A4, XTUPLE_0:1; ::_thesis: verum end; end; end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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 let A be MSAlgebra over S; ::_thesis: for s being SortSymbol of S for v being Element of V . s holds the_sort_of (v -term A) = s let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds the_sort_of (v -term A) = s let v be Element of V . s; ::_thesis: the_sort_of (v -term A) = s ( the Sorts of A \/ V) . s = ( the Sorts of A . s) \/ (V . s) by PBOOLE:def_4; then v in ( the Sorts of A \/ V) . s by XBOOLE_0:def_3; hence the_sort_of (v -term A) = s by Th14; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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 let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,V) holds the_sort_of ((Sym (o,V)) -tree p) = the_result_sort_of o let p be ArgumentSeq of Sym (o,V); ::_thesis: the_sort_of ((Sym (o,V)) -tree p) = the_result_sort_of o A1: ([o, the carrier of S] -tree p) . {} = [o, the carrier of S] by TREES_4:def_4; [o, the carrier of S] = Sym (o,V) by MSAFREE:def_9; hence the_sort_of ((Sym (o,V)) -tree p) = the_result_sort_of o by A1, Th17; ::_thesis: verum end; 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 ) proof let S be non empty non void ManySortedSign ; ::_thesis: 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 ) let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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 ) let o be OperSymbol of S; ::_thesis: for a being FinSequence of S -Terms V holds ( a is ArgumentSeq of Sym (o,V) iff Sym (o,V) ==> roots a ) let a be FinSequence of S -Terms V; ::_thesis: ( a is ArgumentSeq of Sym (o,V) iff Sym (o,V) ==> roots a ) ( a is SubtreeSeq of Sym (o,V) iff Sym (o,V) ==> roots a ) by DTCONSTR:def_6; hence ( a is ArgumentSeq of Sym (o,V) iff Sym (o,V) ==> roots a ) by Def2; ::_thesis: verum end; 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 ) ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: 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 ) ) ) let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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 ) ) ) let o be OperSymbol of S; ::_thesis: 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 ) ) ) let a be ArgumentSeq of Sym (o,V); ::_thesis: ( 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 ) ) ) set X = V; reconsider p = a as FinSequence of TS (DTConMSA V) by Def1; Sym (o,V) ==> roots a by Th21; then A1: p in (((FreeSort V) #) * the Arity of S) . o by MSAFREE:10; then A2: dom p = dom (the_arity_of o) by MSAFREE:9; hence ( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) ) by FINSEQ_3:29; ::_thesis: 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 ) let i be Nat; ::_thesis: ( i in dom a implies 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 ) ) reconsider t = a /. i as Term of S,V ; assume A3: i in dom a ; ::_thesis: 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 ) then A4: i <= len a by FINSEQ_3:25; take t ; ::_thesis: ( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) 1 <= i by A3, FINSEQ_3:25; hence t = a . i by A4, FINSEQ_4:15; ::_thesis: ( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) then t in FreeSort (V,((the_arity_of o) /. i)) by A1, A3, MSAFREE:9; then the_sort_of t = (the_arity_of o) /. i by Def5; hence ( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) by A2, A3, PARTFUN1:def_6; ::_thesis: verum end; 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 ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: 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 ) ) let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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 ) ) let o be OperSymbol of S; ::_thesis: 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 ) ) let a be ArgumentSeq of Sym (o,V); ::_thesis: ( 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 ) ) thus ( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) ) by Lm8; ::_thesis: for i being Nat st i in dom a holds a . i is Term of S,V let i be Nat; ::_thesis: ( i in dom a implies a . i is Term of S,V ) assume i in dom a ; ::_thesis: a . i is Term of S,V then 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 ) by Lm8; hence a . i is Term of S,V ; ::_thesis: verum end; 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 ) proof let S be non empty non void ManySortedSign ; ::_thesis: 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 ) let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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 ) let o be OperSymbol of S; ::_thesis: 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 ) let a be ArgumentSeq of Sym (o,V); ::_thesis: 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 ) let i be Nat; ::_thesis: ( i in dom a implies 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 ) ) assume i in dom a ; ::_thesis: 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 ) then 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 ) by Lm8; hence 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 ) ; ::_thesis: verum end; 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) proof let S be non empty non void ManySortedSign ; ::_thesis: 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) let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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) set X = V; let o be OperSymbol of S; ::_thesis: 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) let a be FinSequence; ::_thesis: ( ( 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 ) ) implies a is ArgumentSeq of Sym (o,V) ) assume that A1: ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) and A2: ( 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 ) ) ; ::_thesis: a is ArgumentSeq of Sym (o,V) rng a c= TS (DTConMSA V) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng a or x in TS (DTConMSA V) ) assume x in rng a ; ::_thesis: x in TS (DTConMSA V) then consider i being set such that A3: i in dom a and A4: x = a . i by FUNCT_1:def_3; reconsider i = i as Nat by A3; ( ex t being Term of S,V st ( t = a . i & the_sort_of t = (the_arity_of o) . i ) or ex t being Term of S,V st ( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) by A2, A3; hence x in TS (DTConMSA V) by A4; ::_thesis: verum end; then reconsider p = a as FinSequence of TS (DTConMSA V) by FINSEQ_1:def_4; A5: dom a = dom (the_arity_of o) by A1, FINSEQ_3:29; now__::_thesis:_for_n_being_Nat_st_n_in_dom_p_holds_ p_._n_in_FreeSort_(V,((the_arity_of_o)_/._n)) let n be Nat; ::_thesis: ( n in dom p implies p . n in FreeSort (V,((the_arity_of o) /. n)) ) assume A6: n in dom p ; ::_thesis: p . n in FreeSort (V,((the_arity_of o) /. n)) thus p . n in FreeSort (V,((the_arity_of o) /. n)) ::_thesis: verum proof percases ( ex t being Term of S,V st ( t = a . n & the_sort_of t = (the_arity_of o) . n ) or ex t being Term of S,V st ( t = a . n & the_sort_of t = (the_arity_of o) /. n ) ) by A2, A6; suppose ex t being Term of S,V st ( t = a . n & the_sort_of t = (the_arity_of o) . n ) ; ::_thesis: p . n in FreeSort (V,((the_arity_of o) /. n)) then consider t being Term of S,V such that A7: t = a . n and A8: the_sort_of t = (the_arity_of o) . n ; the_sort_of t = (the_arity_of o) /. n by A5, A6, A8, PARTFUN1:def_6; hence p . n in FreeSort (V,((the_arity_of o) /. n)) by A7, Def5; ::_thesis: verum end; suppose ex t being Term of S,V st ( t = a . n & the_sort_of t = (the_arity_of o) /. n ) ; ::_thesis: p . n in FreeSort (V,((the_arity_of o) /. n)) hence p . n in FreeSort (V,((the_arity_of o) /. n)) by Def5; ::_thesis: verum end; end; end; end; then p in (((FreeSort V) #) * the Arity of S) . o by A5, MSAFREE:9; then A9: Sym (o,V) ==> roots p by MSAFREE:10; S -Terms V = TS (DTConMSA V) ; hence a is ArgumentSeq of Sym (o,V) by A9, Th21; ::_thesis: verum end; 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) proof let S be non empty non void ManySortedSign ; ::_thesis: 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) let V be V16() ManySortedSet of the carrier of S; ::_thesis: 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) let o be OperSymbol of S; ::_thesis: 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) let a be FinSequence of S -Terms V; ::_thesis: ( ( 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 ) implies a is ArgumentSeq of Sym (o,V) ) assume that A1: ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) and A2: ( 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 ) ; ::_thesis: a is ArgumentSeq of Sym (o,V) A3: now__::_thesis:_for_i_being_Nat_st_i_in_dom_a_holds_ a_._i_in_S_-Terms_V let i be Nat; ::_thesis: ( i in dom a implies a . i in S -Terms V ) assume i in dom a ; ::_thesis: a . i in S -Terms V then A4: a . i in rng a by FUNCT_1:def_3; rng a c= S -Terms V by FINSEQ_1:def_4; hence a . i in S -Terms V by A4; ::_thesis: verum end; now__::_thesis:_(_(_(_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_)_&_(_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_ for_t_being_Term_of_S,V_st_t_=_a_._i_holds_ the_sort_of_t_=_(the_arity_of_o)_/._i_)_&_(_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_)_)_)_) percases ( 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 ) by A2; caseA5: 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 ; ::_thesis: 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 ) let i be Nat; ::_thesis: ( i in dom a implies ex t being Term of S,V st ( t = a . i & the_sort_of t = (the_arity_of o) . i ) ) assume A6: i in dom a ; ::_thesis: ex t being Term of S,V st ( t = a . i & the_sort_of t = (the_arity_of o) . i ) then reconsider t = a . i as Term of S,V by A3; take t = t; ::_thesis: ( t = a . i & the_sort_of t = (the_arity_of o) . i ) thus ( t = a . i & the_sort_of t = (the_arity_of o) . i ) by A5, A6; ::_thesis: verum end; caseA7: 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 ; ::_thesis: 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 ) let i be Nat; ::_thesis: ( i in dom a implies ex t being Term of S,V st ( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) assume A8: i in dom a ; ::_thesis: ex t being Term of S,V st ( t = a . i & the_sort_of t = (the_arity_of o) /. i ) then reconsider t = a . i as Term of S,V by A3; take t = t; ::_thesis: ( t = a . i & the_sort_of t = (the_arity_of o) /. i ) thus ( t = a . i & the_sort_of t = (the_arity_of o) /. i ) by A7, A8; ::_thesis: verum end; end; end; hence a is ArgumentSeq of Sym (o,V) by A1, Th24; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let V1, V2 be V16() ManySortedSet of the carrier of S; ::_thesis: ( V1 c= V2 implies for t being Term of S,V1 holds t is Term of S,V2 ) assume A1: for s being set st s in the carrier of S holds V1 . s c= V2 . s ; :: according to PBOOLE:def_2 ::_thesis: for t being Term of S,V1 holds t is Term of S,V2 defpred S1[ set ] means \$1 is Term of S,V2; A2: for o being OperSymbol of S for p being ArgumentSeq of Sym (o,V1) st ( for t being Term of S,V1 st t in rng p holds S1[t] ) holds S1[[o, the carrier of S] -tree p] proof let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,V1) st ( for t being Term of S,V1 st t in rng p holds S1[t] ) holds S1[[o, the carrier of S] -tree p] let p be ArgumentSeq of Sym (o,V1); ::_thesis: ( ( for t being Term of S,V1 st t in rng p holds S1[t] ) implies S1[[o, the carrier of S] -tree p] ) assume A3: for t being Term of S,V1 st t in rng p holds t is Term of S,V2 ; ::_thesis: S1[[o, the carrier of S] -tree p] rng p c= S -Terms V2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in S -Terms V2 ) assume A4: x in rng p ; ::_thesis: x in S -Terms V2 rng p c= S -Terms V1 by FINSEQ_1:def_4; then reconsider x = x as Term of S,V1 by A4; x is Term of S,V2 by A3, A4; hence x in S -Terms V2 ; ::_thesis: verum end; then reconsider q = p as FinSequence of S -Terms V2 by FINSEQ_1:def_4; A5: now__::_thesis:_for_i_being_Nat_st_i_in_dom_q_holds_ ex_T_being_Term_of_S,V2_st_ (_T_=_q_._i_&_the_sort_of_T_=_(the_arity_of_o)_._i_) let i be Nat; ::_thesis: ( i in dom q implies ex T being Term of S,V2 st ( T = q . i & the_sort_of T = (the_arity_of o) . i ) ) assume A6: i in dom q ; ::_thesis: ex T being Term of S,V2 st ( T = q . i & the_sort_of T = (the_arity_of o) . i ) then consider t being Term of S,V1 such that A7: t = q . i and t = p /. i and A8: the_sort_of t = (the_arity_of o) . i and the_sort_of t = (the_arity_of o) /. i by Lm8; t in rng p by A6, A7, FUNCT_1:def_3; then reconsider T = t as Term of S,V2 by A3; take T = T; ::_thesis: ( T = q . i & the_sort_of T = (the_arity_of o) . i ) thus T = q . i by A7; ::_thesis: the_sort_of T = (the_arity_of o) . i thus the_sort_of T = (the_arity_of o) . i ::_thesis: verum proof percases ( ex s being SortSymbol of S ex v being Element of V1 . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] ) by Th2; suppose ex s being SortSymbol of S ex v being Element of V1 . s st t . {} = [v,s] ; ::_thesis: the_sort_of T = (the_arity_of o) . i then consider s being SortSymbol of S, v being Element of V1 . s such that A9: t . {} = [v,s] ; A10: t = root-tree [v,s] by A9, Th5; V1 . s c= V2 . s by A1; then v in V2 . s by TARSKI:def_3; hence the_sort_of T = s by A10, Th14 .= (the_arity_of o) . i by A8, A10, Th14 ; ::_thesis: verum end; suppose t . {} in [: the carrier' of S,{ the carrier of S}:] ; ::_thesis: the_sort_of T = (the_arity_of o) . i then consider o9 being OperSymbol of S, x2 being Element of { the carrier of S} such that A11: t . {} = [o9,x2] by DOMAIN_1:1; A12: x2 = the carrier of S by TARSKI:def_1; hence the_sort_of T = the_result_sort_of o9 by A11, Th17 .= (the_arity_of o) . i by A8, A11, A12, Th17 ; ::_thesis: verum end; end; end; end; len p = len (the_arity_of o) by Lm8; then q is ArgumentSeq of Sym (o,V2) by A5, Th24; hence S1[[o, the carrier of S] -tree p] by Th1; ::_thesis: verum end; A13: for s being SortSymbol of S for v being Element of V1 . s holds S1[ root-tree [v,s]] proof let s be SortSymbol of S; ::_thesis: for v being Element of V1 . s holds S1[ root-tree [v,s]] let v be Element of V1 . s; ::_thesis: S1[ root-tree [v,s]] V1 . s c= V2 . s by A1; then v in V2 . s by TARSKI:def_3; hence S1[ root-tree [v,s]] by Th4; ::_thesis: verum end; for t being Term of S,V1 holds S1[t] from MSATERM:sch_1(A13, A2); hence for t being Term of S,V1 holds t is Term of S,V2 ; ::_thesis: verum end; 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}:] proof set s = the OperSymbol of S; reconsider nt = Sym ( the OperSymbol of S,V) as NonTerminal of (DTConMSA V) ; set p = the SubtreeSeq of nt; reconsider t = nt -tree the SubtreeSeq of nt as Term of S,V ; take t ; ::_thesis: t . {} in [: the carrier' of S,{ the carrier of S}:] nt = [ the OperSymbol of S, the carrier of S] by MSAFREE:def_9; then A1: [ the OperSymbol of S, the carrier of S] = t . {} by TREES_4:def_4; the carrier of S in { the carrier of S} by TARSKI:def_1; hence t . {} in [: the carrier' of S,{ the carrier of S}:] by A1, ZFMISC_1:87; ::_thesis: verum end; 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 proof set t = the CompoundTerm of S,V; reconsider X = { the CompoundTerm of S,V} as non empty Subset of (S -Terms V) by ZFMISC_1:31; take X ; ::_thesis: ex t being CompoundTerm of S,V st t in X take the CompoundTerm of S,V ; ::_thesis: the CompoundTerm of S,V in X thus the CompoundTerm of S,V in X by TARSKI:def_1; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let V be V16() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,V st not t is root holds t is CompoundTerm of S,V let t be Term of S,V; ::_thesis: ( not t is root implies t is CompoundTerm of S,V ) assume A1: not t is root ; ::_thesis: t is CompoundTerm of S,V percases ( 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}:] ) by Th2; suppose ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] ; ::_thesis: t is CompoundTerm of S,V then consider s being SortSymbol of S, x being Element of V . s such that A2: t . {} = [x,s] ; t = root-tree [x,s] by A2, Th5; hence t is CompoundTerm of S,V by A1; ::_thesis: verum end; suppose t . {} in [: the carrier' of S,{ the carrier of S}:] ; ::_thesis: t is CompoundTerm of S,V hence t . {} in [: the carrier' of S,{ the carrier of S}:] ; :: according to MSATERM:def_6 ::_thesis: verum end; end; end; 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 ) proof let n be Element of NAT ; ::_thesis: for p being FinSequence st n < len p holds ( n + 1 in dom p & p . (n + 1) in rng p ) let p be FinSequence; ::_thesis: ( n < len p implies ( n + 1 in dom p & p . (n + 1) in rng p ) ) n >= 0 by NAT_1:2; then A1: n + 1 >= 0 + 1 by XREAL_1:7; assume n < len p ; ::_thesis: ( n + 1 in dom p & p . (n + 1) in rng p ) then n + 1 <= len p by NAT_1:13; then n + 1 in dom p by A1, FINSEQ_3:25; hence ( n + 1 in dom p & p . (n + 1) in rng p ) by FUNCT_1:def_3; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let V be V16() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,V for p being Node of t holds t | p is Term of S,V let t be Term of S,V; ::_thesis: for p being Node of t holds t | p is Term of S,V defpred S1[ set ] means for q being Node of t st q = \$1 holds t | q is Term of S,V; A1: for p being Node of t for n being Element of NAT st S1[p] & p ^ <*n*> in dom t holds S1[p ^ <*n*>] proof let p be Node of t; ::_thesis: for n being Element of NAT st S1[p] & p ^ <*n*> in dom t holds S1[p ^ <*n*>] let n be Element of NAT ; ::_thesis: ( S1[p] & p ^ <*n*> in dom t implies S1[p ^ <*n*>] ) assume that A2: for q being Node of t st q = p holds t | q is Term of S,V and A3: p ^ <*n*> in dom t ; ::_thesis: S1[p ^ <*n*>] reconsider u = t | p as Term of S,V by A2; A4: dom u = (dom t) | p by TREES_2:def_10; A5: <*n*> in (dom t) | p by A3, TREES_1:def_6; A6: now__::_thesis:_for_s_being_SortSymbol_of_S for_x_being_Element_of_V_._s_holds_not_u_._{}_=_[x,s] given s being SortSymbol of S, x being Element of V . s such that A7: u . {} = [x,s] ; ::_thesis: contradiction u = root-tree [x,s] by A7, Th5; then <*n*> in {{}} by A5, A4, TREES_1:29, TREES_4:3; hence contradiction by TARSKI:def_1; ::_thesis: verum end; ( ex s being SortSymbol of S ex v being Element of V . s st u . {} = [v,s] or u . {} in [: the carrier' of S,{ the carrier of S}:] ) by Th2; then consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that A8: u . {} = [o,x2] by A6, DOMAIN_1:1; x2 = the carrier of S by TARSKI:def_1; then consider a being ArgumentSeq of Sym (o,V) such that A9: u = [o, the carrier of S] -tree a by A8, Th10; consider i being Element of NAT , T being DecoratedTree, r being Node of T such that A10: i < len a and T = a . (i + 1) and A11: <*n*> = <*i*> ^ r by A5, A4, A9, TREES_4:11; A12: n = <*n*> . 1 by FINSEQ_1:40 .= i by A11, FINSEQ_1:41 ; then A13: u | <*n*> = a . (n + 1) by A9, A10, TREES_4:def_4; let q be Node of t; ::_thesis: ( q = p ^ <*n*> implies t | q is Term of S,V ) assume A14: q = p ^ <*n*> ; ::_thesis: t | q is Term of S,V n + 1 in dom a by A10, A12, Lm9; then ex t being Term of S,V st ( t = u | <*n*> & t = a /. (n + 1) & the_sort_of t = (the_arity_of o) . (n + 1) & the_sort_of t = (the_arity_of o) /. (n + 1) ) by A13, Lm8; hence t | q is Term of S,V by A14, TREES_9:3; ::_thesis: verum end; A15: S1[ {} ] by TREES_9:1; for p being Node of t holds S1[p] from TREES_2:sch_1(A15, A1); hence for p being Node of t holds t | p is Term of S,V ; ::_thesis: verum end; 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 proof deffunc H1( set ) -> set = {( the Sorts of A . \$1)}; consider V being ManySortedSet of the carrier of S such that A1: for s being set st s in the carrier of S holds V . s = H1(s) from PBOOLE:sch_4(); V is V16() proof let s be set ; :: according to PBOOLE:def_13 ::_thesis: ( not s in the carrier of S or not V . s is empty ) assume s in the carrier of S ; ::_thesis: not V . s is empty then V . s = {( the Sorts of A . s)} by A1; hence not V . s is empty ; ::_thesis: verum end; then reconsider V = V as V16() ManySortedSet of the carrier of S ; take V ; ::_thesis: V misses the Sorts of A let s be set ; :: according to PBOOLE:def_8 ::_thesis: ( not s in the carrier of S or V . s misses the Sorts of A . s ) assume s in the carrier of S ; ::_thesis: V . s misses the Sorts of A . s then A2: V . s = {( the Sorts of A . s)} by A1; now__::_thesis:_for_x_being_set_st_x_in_V_._s_holds_ not_x_in_the_Sorts_of_A_._s let x be set ; ::_thesis: ( x in V . s implies not x in the Sorts of A . s ) assume x in V . s ; ::_thesis: not x in the Sorts of A . s then x = the Sorts of A . s by A2, TARSKI:def_1; hence not x in the Sorts of A . s ; ::_thesis: verum end; hence V . s misses the Sorts of A . s by XBOOLE_0:3; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let A be MSAlgebra over S; ::_thesis: 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 let V be Variables of A; ::_thesis: 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 let s be SortSymbol of S; ::_thesis: for x being set st x in the Sorts of A . s holds for v being Element of V . s holds x <> v let x be set ; ::_thesis: ( x in the Sorts of A . s implies for v being Element of V . s holds x <> v ) assume A1: x in the Sorts of A . s ; ::_thesis: for v being Element of V . s holds x <> v let v be Element of V . s; ::_thesis: x <> v V misses the Sorts of A by Def8; then V . s misses the Sorts of A . s by PBOOLE:def_8; hence x <> v by A1, XBOOLE_0:3; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let A be non-empty MSAlgebra over S; ::_thesis: 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 let V be Variables of A; ::_thesis: 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 let t be c-Term of A,V; ::_thesis: 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 let f be ManySortedFunction of V, the Sorts of A; ::_thesis: 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 let s be SortSymbol of S; ::_thesis: 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 let x be Element of the Sorts of A . s; ::_thesis: ( t = root-tree [x,s] implies root-tree x is_an_evaluation_of t,f ) assume A1: t = root-tree [x,s] ; ::_thesis: root-tree x is_an_evaluation_of t,f A2: t . {} = [x,s] by A1, TREES_4:3; set vt = root-tree x; A3: dom (root-tree x) = elementary_tree 0 by TREES_4:3; hence dom (root-tree x) = dom t by A1, TREES_4:3; :: according to MSATERM:def_9 ::_thesis: for p being Node of (root-tree x) holds ( ( for s being SortSymbol of S for v being Element of V . s st t . p = [v,s] holds (root-tree x) . 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 (root-tree x) . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds (root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p)) ) ) let p be Node of (root-tree x); ::_thesis: ( ( for s being SortSymbol of S for v being Element of V . s st t . p = [v,s] holds (root-tree x) . 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 (root-tree x) . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds (root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p)) ) ) reconsider e = p as empty FinSequence of NAT by A3, TARSKI:def_1, TREES_1:29; hereby ::_thesis: ( ( for s being SortSymbol of S for x being Element of the Sorts of A . s st t . p = [x,s] holds (root-tree x) . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds (root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p)) ) ) let s1 be SortSymbol of S; ::_thesis: for v being Element of V . s1 st t . p = [v,s1] holds (root-tree x) . p = (f . s1) . v let v be Element of V . s1; ::_thesis: ( t . p = [v,s1] implies (root-tree x) . p = (f . s1) . v ) assume t . p = [v,s1] ; ::_thesis: (root-tree x) . p = (f . s1) . v then A4: [v,s1] = t . e .= [x,s] by A1, TREES_4:3 ; then A5: x = v by XTUPLE_0:1; s = s1 by A4, XTUPLE_0:1; hence (root-tree x) . p = (f . s1) . v by A5, Th30; ::_thesis: verum end; A6: (root-tree x) . {} = x by TREES_4:3; hereby ::_thesis: for o being OperSymbol of S st t . p = [o, the carrier of S] holds (root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p)) let s1 be SortSymbol of S; ::_thesis: for x1 being Element of the Sorts of A . s1 st t . p = [x1,s1] holds (root-tree x) . p = x1 let x1 be Element of the Sorts of A . s1; ::_thesis: ( t . p = [x1,s1] implies (root-tree x) . p = x1 ) assume t . p = [x1,s1] ; ::_thesis: (root-tree x) . p = x1 then [x1,s1] = t . e ; hence (root-tree x) . p = x1 by A2, A6, XTUPLE_0:1; ::_thesis: verum end; let o be OperSymbol of S; ::_thesis: ( t . p = [o, the carrier of S] implies (root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p)) ) assume t . p = [o, the carrier of S] ; ::_thesis: (root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p)) then the carrier of S = (t . e) `2 by MCART_1:7 .= s by A2, MCART_1:7 ; hence (root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p)) by Lm7; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let A be non-empty MSAlgebra over S; ::_thesis: 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 let V be Variables of A; ::_thesis: 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 let t be c-Term of A,V; ::_thesis: 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 let f be ManySortedFunction of V, the Sorts of A; ::_thesis: 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 let s be SortSymbol of S; ::_thesis: 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 let x be Element of V . s; ::_thesis: ( t = root-tree [x,s] implies root-tree ((f . s) . x) is_an_evaluation_of t,f ) assume A1: t = root-tree [x,s] ; ::_thesis: root-tree ((f . s) . x) is_an_evaluation_of t,f set vt = root-tree ((f . s) . x); A2: dom (root-tree ((f . s) . x)) = elementary_tree 0 by TREES_4:3; hence dom (root-tree ((f . s) . x)) = dom t by A1, TREES_4:3; :: according to MSATERM:def_9 ::_thesis: for p being Node of (root-tree ((f . s) . x)) holds ( ( for s being SortSymbol of S for v being Element of V . s st t . p = [v,s] holds (root-tree ((f . s) . x)) . 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 (root-tree ((f . s) . x)) . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds (root-tree ((f . s) . x)) . p = (Den (o,A)) . (succ ((root-tree ((f . s) . x)),p)) ) ) let p be Node of (root-tree ((f . s) . x)); ::_thesis: ( ( for s being SortSymbol of S for v being Element of V . s st t . p = [v,s] holds (root-tree ((f . s) . x)) . 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 (root-tree ((f . s) . x)) . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds (root-tree ((f . s) . x)) . p = (Den (o,A)) . (succ ((root-tree ((f . s) . x)),p)) ) ) reconsider e = p as empty FinSequence of NAT by A2, TARSKI:def_1, TREES_1:29; A3: t . {} = [x,s] by A1, TREES_4:3; hereby ::_thesis: ( ( for s being SortSymbol of S for x being Element of the Sorts of A . s st t . p = [x,s] holds (root-tree ((f . s) . x)) . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds (root-tree ((f . s) . x)) . p = (Den (o,A)) . (succ ((root-tree ((f . s) . x)),p)) ) ) let s1 be SortSymbol of S; ::_thesis: for x1 being Element of V . s1 st t . p = [x1,s1] holds (root-tree ((f . s) . x)) . p = (f . s1) . x1 let x1 be Element of V . s1; ::_thesis: ( t . p = [x1,s1] implies (root-tree ((f . s) . x)) . p = (f . s1) . x1 ) A4: e = p ; assume t . p = [x1,s1] ; ::_thesis: (root-tree ((f . s) . x)) . p = (f . s1) . x1 then A5: [x1,s1] = t . e ; then A6: s = s1 by A3, XTUPLE_0:1; x = x1 by A3, A5, XTUPLE_0:1; hence (root-tree ((f . s) . x)) . p = (f . s1) . x1 by A6, A4, TREES_4:3; ::_thesis: verum end; hereby ::_thesis: for o being OperSymbol of S st t . p = [o, the carrier of S] holds (root-tree ((f . s) . x)) . p = (Den (o,A)) . (succ ((root-tree ((f . s) . x)),p)) let s1 be SortSymbol of S; ::_thesis: for v being Element of the Sorts of A . s1 st t . p = [v,s1] holds (root-tree ((f . s) . x)) . p = v let v be Element of the Sorts of A . s1; ::_thesis: ( t . p = [v,s1] implies (root-tree ((f . s) . x)) . p = v ) assume t . p = [v,s1] ; ::_thesis: (root-tree ((f . s) . x)) . p = v then A7: [v,s1] = t . e .= [x,s] by A1, TREES_4:3 ; then A8: x = v by XTUPLE_0:1; s = s1 by A7, XTUPLE_0:1; hence (root-tree ((f . s) . x)) . p = v by A8, Th30; ::_thesis: verum end; let o be OperSymbol of S; ::_thesis: ( t . p = [o, the carrier of S] implies (root-tree ((f . s) . x)) . p = (Den (o,A)) . (succ ((root-tree ((f . s) . x)),p)) ) assume t . p = [o, the carrier of S] ; ::_thesis: (root-tree ((f . s) . x)) . p = (Den (o,A)) . (succ ((root-tree ((f . s) . x)),p)) then the carrier of S = (t . e) `2 by MCART_1:7 .= s by A3, MCART_1:7 ; hence (root-tree ((f . s) . x)) . p = (Den (o,A)) . (succ ((root-tree ((f . s) . x)),p)) by Lm7; ::_thesis: verum end; 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 ) proof let S be non empty non void ManySortedSign ; ::_thesis: 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 ) let A be non-empty MSAlgebra over S; ::_thesis: 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 ) let V be Variables of A; ::_thesis: 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 ) let f be ManySortedFunction of V, the Sorts of A; ::_thesis: 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 ) let o be OperSymbol of S; ::_thesis: 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 ) let p be ArgumentSeq of o,A,V; ::_thesis: 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 ) A1: Sym (o,( the Sorts of A \/ V)) = [o, the carrier of S] by MSAFREE:def_9; A2: dom (doms p) = dom p by TREES_3:37; A3: tree (doms p) = dom ([o, the carrier of S] -tree p) by TREES_4:10; A4: dom p = Seg (len p) by FINSEQ_1:def_3; let q be DTree-yielding FinSequence; ::_thesis: ( 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 ) ) implies 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 ) ) assume that A5: len q = len p and A6: 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 ) ; ::_thesis: 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 ) A7: dom q = Seg (len q) by FINSEQ_1:def_3; now__::_thesis:_for_x_being_set_st_x_in_dom_(doms_q)_holds_ (doms_q)_._x_is_finite_Tree let x be set ; ::_thesis: ( x in dom (doms q) implies (doms q) . x is finite Tree ) A8: rng p c= S -Terms ( the Sorts of A \/ V) by FINSEQ_1:def_4; assume A9: x in dom (doms q) ; ::_thesis: (doms q) . x is finite Tree then A10: x in dom q by TREES_3:37; then p . x in rng p by A5, A4, A7, FUNCT_1:def_3; then reconsider t = p . x as c-Term of A,V by A8; reconsider i = x as Nat by A9; consider vt being finite DecoratedTree such that A11: vt = q . i and vt is_an_evaluation_of t,f by A5, A6, A4, A7, A10; (doms q) . x = dom vt by A10, A11, FUNCT_6:22; hence (doms q) . x is finite Tree ; ::_thesis: verum end; then reconsider r = doms q as FinTree-yielding FinSequence by TREES_3:23; A12: now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_ r_._i_=_(doms_p)_._i let i be Nat; ::_thesis: ( i in dom p implies r . i = (doms p) . i ) A13: rng p c= S -Terms ( the Sorts of A \/ V) by FINSEQ_1:def_4; assume A14: i in dom p ; ::_thesis: r . i = (doms p) . i then p . i in rng p by FUNCT_1:def_3; then reconsider t = p . i as c-Term of A,V by A13; consider vt being finite DecoratedTree such that A15: vt = q . i and A16: vt is_an_evaluation_of t,f by A6, A14; thus r . i = dom vt by A5, A4, A7, A14, A15, FUNCT_6:22 .= dom t by A16, Def9 .= (doms p) . i by A14, FUNCT_6:22 ; ::_thesis: verum end; set vt = ((Den (o,A)) . (roots q)) -tree q; A17: len (doms q) = len q by TREES_3:38; A18: dom (((Den (o,A)) . (roots q)) -tree q) = tree r by TREES_4:10; then reconsider vt = ((Den (o,A)) . (roots q)) -tree q as finite DecoratedTree by FINSET_1:10; take vt ; ::_thesis: ( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f ) thus vt = ((Den (o,A)) . (roots q)) -tree q ; ::_thesis: vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f dom (doms q) = dom q by TREES_3:37; hence dom vt = dom ((Sym (o,( the Sorts of A \/ V))) -tree p) by A1, A5, A4, A7, A18, A3, A2, A12, FINSEQ_1:13; :: according to MSATERM:def_9 ::_thesis: for p being Node of vt holds ( ( for s being SortSymbol of S for v being Element of V . s st ((Sym (o,( the Sorts of A \/ V))) -tree p) . 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 ((Sym (o,( the Sorts of A \/ V))) -tree p) . p = [x,s] holds vt . p = x ) & ( for o being OperSymbol of S st ((Sym (o,( the Sorts of A \/ V))) -tree p) . p = [o, the carrier of S] holds vt . p = (Den (o,A)) . (succ (vt,p)) ) ) let n be Node of vt; ::_thesis: ( ( for s being SortSymbol of S for v being Element of V . s st ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [v,s] holds vt . n = (f . s) . v ) & ( for s being SortSymbol of S for x being Element of the Sorts of A . s st ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [x,s] holds vt . n = x ) & ( for o being OperSymbol of S st ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [o, the carrier of S] holds vt . n = (Den (o,A)) . (succ (vt,n)) ) ) A19: ([o, the carrier of S] -tree p) . {} = [o, the carrier of S] by TREES_4:def_4; hereby ::_thesis: ( ( for s being SortSymbol of S for x being Element of the Sorts of A . s st ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [x,s] holds vt . n = x ) & ( for o being OperSymbol of S st ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [o, the carrier of S] holds vt . n = (Den (o,A)) . (succ (vt,n)) ) ) let s be SortSymbol of S; ::_thesis: for v being Element of V . s st ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [v,s] holds vt . n = (f . s) . v let v be Element of V . s; ::_thesis: ( ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [v,s] implies vt . n = (f . s) . v ) assume A20: ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [v,s] ; ::_thesis: vt . n = (f . s) . v now__::_thesis:_not_n_=_{} assume n = {} ; ::_thesis: contradiction then s = the carrier of S by A1, A19, A20, XTUPLE_0:1; hence contradiction by Lm7; ::_thesis: verum end; then consider w being FinSequence of NAT , i being Element of NAT such that A21: n = <*i*> ^ w by FINSEQ_2:130; A22: w in (doms q) . (i + 1) by A18, A21, TREES_3:48; A23: i < len p by A5, A18, A17, A21, TREES_3:48; then reconsider t = p . (i + 1) as c-Term of A,V by Lm2; consider e being finite DecoratedTree such that A24: e = q . (i + 1) and A25: e is_an_evaluation_of t,f by A6, A23, Lm9; i + 1 in dom p by A23, Lm9; then reconsider w = w as Node of e by A5, A4, A7, A22, A24, FUNCT_6:22; dom e = dom t by A25, Def9; then A26: t . w = [v,s] by A20, A21, A23, TREES_4:12; thus vt . n = e . w by A5, A21, A23, A24, TREES_4:12 .= (f . s) . v by A25, A26, Def9 ; ::_thesis: verum end; hereby ::_thesis: for o being OperSymbol of S st ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [o, the carrier of S] holds vt . n = (Den (o,A)) . (succ (vt,n)) let s be SortSymbol of S; ::_thesis: for x being Element of the Sorts of A . s st ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [x,s] holds vt . n = x let x be Element of the Sorts of A . s; ::_thesis: ( ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [x,s] implies vt . n = x ) assume A27: ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [x,s] ; ::_thesis: vt . n = x now__::_thesis:_not_n_=_{} assume n = {} ; ::_thesis: contradiction then s = the carrier of S by A1, A19, A27, XTUPLE_0:1; hence contradiction by Lm7; ::_thesis: verum end; then consider w being FinSequence of NAT , i being Element of NAT such that A28: n = <*i*> ^ w by FINSEQ_2:130; A29: w in (doms q) . (i + 1) by A18, A28, TREES_3:48; A30: i < len p by A5, A18, A17, A28, TREES_3:48; then reconsider t = p . (i + 1) as c-Term of A,V by Lm2; consider e being finite DecoratedTree such that A31: e = q . (i + 1) and A32: e is_an_evaluation_of t,f by A6, A30, Lm9; i + 1 in dom p by A30, Lm9; then reconsider w = w as Node of e by A5, A4, A7, A29, A31, FUNCT_6:22; dom e = dom t by A32, Def9; then A33: t . w = [x,s] by A27, A28, A30, TREES_4:12; thus vt . n = e . w by A5, A28, A30, A31, TREES_4:12 .= x by A32, A33, Def9 ; ::_thesis: verum end; let o1 be OperSymbol of S; ::_thesis: ( ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [o1, the carrier of S] implies vt . n = (Den (o1,A)) . (succ (vt,n)) ) assume A34: ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = [o1, the carrier of S] ; ::_thesis: vt . n = (Den (o1,A)) . (succ (vt,n)) percases ( n = {} or n <> {} ) ; supposeA35: n = {} ; ::_thesis: vt . n = (Den (o1,A)) . (succ (vt,n)) then ((Sym (o,( the Sorts of A \/ V))) -tree p) . n = Sym (o,( the Sorts of A \/ V)) by TREES_4:def_4 .= [o, the carrier of S] by MSAFREE:def_9 ; then A36: o = o1 by A34, XTUPLE_0:1; succ (vt,n) = roots q by A35, TREES_9:30; hence vt . n = (Den (o1,A)) . (succ (vt,n)) by A35, A36, TREES_4:def_4; ::_thesis: verum end; suppose n <> {} ; ::_thesis: vt . n = (Den (o1,A)) . (succ (vt,n)) then consider w being FinSequence of NAT , i being Element of NAT such that A37: n = <*i*> ^ w by FINSEQ_2:130; reconsider ii = <*i*> as Node of vt by A37, TREES_1:21; A38: w in (doms q) . (i + 1) by A18, A37, TREES_3:48; A39: i < len p by A5, A18, A17, A37, TREES_3:48; then reconsider t = p . (i + 1) as c-Term of A,V by Lm2; consider e being finite DecoratedTree such that A40: e = q . (i + 1) and A41: e is_an_evaluation_of t,f by A6, A39, Lm9; A42: e = vt | ii by A5, A39, A40, TREES_4:def_4; i + 1 in dom p by A39, Lm9; then reconsider w = w as Node of e by A5, A4, A7, A38, A40, FUNCT_6:22; dom e = dom t by A41, Def9; then t . w = [o1, the carrier of S] by A34, A37, A39, TREES_4:12; then e . w = (Den (o1,A)) . (succ (e,w)) by A41, Def9 .= (Den (o1,A)) . (succ (vt,n)) by A37, A42, TREES_9:31 ; hence vt . n = (Den (o1,A)) . (succ (vt,n)) by A5, A37, A39, A40, TREES_4:12; ::_thesis: verum end; end; end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let A be non-empty MSAlgebra over S; ::_thesis: 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 let V be Variables of A; ::_thesis: 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 let f be ManySortedFunction of V, the Sorts of A; ::_thesis: 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 let t be c-Term of A,V; ::_thesis: 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 let e be finite DecoratedTree; ::_thesis: ( e is_an_evaluation_of t,f implies 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 ) assume that A1: dom e = dom t and A2: for p being Node of e holds ( ( for s being SortSymbol of S for v being Element of V . s st t . p = [v,s] holds e . 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 e . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds e . p = (Den (o,A)) . (succ (e,p)) ) ) ; :: according to MSATERM:def_9 ::_thesis: 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 let p be Node of t; ::_thesis: for n being Node of e st n = p holds e | n is_an_evaluation_of t | p,f let n be Node of e; ::_thesis: ( n = p implies e | n is_an_evaluation_of t | p,f ) set vt = e | n; set tp = t | p; A3: dom (e | n) = (dom e) | n by TREES_2:def_10; assume A4: n = p ; ::_thesis: e | n is_an_evaluation_of t | p,f hence dom (e | n) = dom (t | p) by A1, A3, TREES_2:def_10; :: according to MSATERM:def_9 ::_thesis: for p being Node of (e | n) holds ( ( for s being SortSymbol of S for v being Element of V . s st (t | p) . p = [v,s] holds (e | n) . p = (f . s) . v ) & ( for s being SortSymbol of S for x being Element of the Sorts of A . s st (t | p) . p = [x,s] holds (e | n) . p = x ) & ( for o being OperSymbol of S st (t | p) . p = [o, the carrier of S] holds (e | n) . p = (Den (o,A)) . (succ ((e | n),p)) ) ) let q be Node of (e | n); ::_thesis: ( ( for s being SortSymbol of S for v being Element of V . s st (t | p) . q = [v,s] holds (e | n) . q = (f . s) . v ) & ( for s being SortSymbol of S for x being Element of the Sorts of A . s st (t | p) . q = [x,s] holds (e | n) . q = x ) & ( for o being OperSymbol of S st (t | p) . q = [o, the carrier of S] holds (e | n) . q = (Den (o,A)) . (succ ((e | n),q)) ) ) reconsider nq = n ^ q as Node of e by A3, TREES_1:def_6; reconsider pq = p ^ q as Node of t by A1, A4, A3, TREES_1:def_6; hereby ::_thesis: ( ( for s being SortSymbol of S for x being Element of the Sorts of A . s st (t | p) . q = [x,s] holds (e | n) . q = x ) & ( for o being OperSymbol of S st (t | p) . q = [o, the carrier of S] holds (e | n) . q = (Den (o,A)) . (succ ((e | n),q)) ) ) let s be SortSymbol of S; ::_thesis: for v being Element of V . s st (t | p) . q = [v,s] holds (e | n) . q = (f . s) . v let v be Element of V . s; ::_thesis: ( (t | p) . q = [v,s] implies (e | n) . q = (f . s) . v ) assume (t | p) . q = [v,s] ; ::_thesis: (e | n) . q = (f . s) . v then t . pq = [v,s] by A1, A4, A3, TREES_2:def_10; then e . nq = (f . s) . v by A2, A4; hence (e | n) . q = (f . s) . v by A3, TREES_2:def_10; ::_thesis: verum end; hereby ::_thesis: for o being OperSymbol of S st (t | p) . q = [o, the carrier of S] holds (e | n) . q = (Den (o,A)) . (succ ((e | n),q)) let s be SortSymbol of S; ::_thesis: for x being Element of the Sorts of A . s st (t | p) . q = [x,s] holds (e | n) . q = x let x be Element of the Sorts of A . s; ::_thesis: ( (t | p) . q = [x,s] implies (e | n) . q = x ) assume (t | p) . q = [x,s] ; ::_thesis: (e | n) . q = x then t . pq = [x,s] by A1, A4, A3, TREES_2:def_10; then e . nq = x by A2, A4; hence (e | n) . q = x by A3, TREES_2:def_10; ::_thesis: verum end; let o be OperSymbol of S; ::_thesis: ( (t | p) . q = [o, the carrier of S] implies (e | n) . q = (Den (o,A)) . (succ ((e | n),q)) ) assume (t | p) . q = [o, the carrier of S] ; ::_thesis: (e | n) . q = (Den (o,A)) . (succ ((e | n),q)) then t . pq = [o, the carrier of S] by A1, A4, A3, TREES_2:def_10; then e . nq = (Den (o,A)) . (succ (e,nq)) by A2, A4; then (e | n) . q = (Den (o,A)) . (succ (e,(n ^ q))) by A3, TREES_2:def_10; hence (e | n) . q = (Den (o,A)) . (succ ((e | n),q)) by TREES_9:31; ::_thesis: verum end; 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 ) ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: 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 ) ) ) let A be non-empty MSAlgebra over S; ::_thesis: 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 ) ) ) let V be Variables of A; ::_thesis: 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 ) ) ) let f be ManySortedFunction of V, the Sorts of A; ::_thesis: 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 ) ) ) let o be OperSymbol of S; ::_thesis: 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 ) ) ) let p be ArgumentSeq of o,A,V; ::_thesis: 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 ) ) ) let vt be finite DecoratedTree; ::_thesis: ( vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f implies 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 ) ) ) ) assume A1: vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f ; ::_thesis: 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 ) ) ) reconsider r = {} as empty Element of dom vt by TREES_1:22; consider x being set , q being DTree-yielding FinSequence such that A2: vt = x -tree q by TREES_9:8; A3: dom vt = tree (doms q) by A2, TREES_4:10; take q ; ::_thesis: ( 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 ) ) ) A4: len (doms q) = len q by TREES_3:38; A5: Sym (o,( the Sorts of A \/ V)) = [o, the carrier of S] by MSAFREE:def_9; then A6: dom vt = dom ([o, the carrier of S] -tree p) by A1, Def9; then dom vt = tree (doms p) by TREES_4:10; then A7: doms q = doms p by A3, TREES_3:50; hence len q = len p by A4, TREES_3:38; ::_thesis: ( 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 ) ) ) ([o, the carrier of S] -tree p) . r = [o, the carrier of S] by TREES_4:def_4; then vt . r = (Den (o,A)) . (succ (vt,r)) by A5, A1, Def9 .= (Den (o,A)) . (roots q) by A2, TREES_9:30 ; hence vt = ((Den (o,A)) . (roots q)) -tree q by A2, TREES_4:def_4; ::_thesis: 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 ) let i be Nat; ::_thesis: 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 ) let t be c-Term of A,V; ::_thesis: ( i in dom p & t = p . i implies ex vt being finite DecoratedTree st ( vt = q . i & vt is_an_evaluation_of t,f ) ) assume that A8: i in dom p and A9: t = p . i ; ::_thesis: ex vt being finite DecoratedTree st ( vt = q . i & vt is_an_evaluation_of t,f ) reconsider u = {} as Node of t by TREES_1:22; consider k being Element of NAT such that A10: i = k + 1 and A11: k < len p by A8, Lm1; <*k*> ^ u = <*k*> by FINSEQ_1:34; then reconsider r = <*k*> as Node of vt by A6, A9, A10, A11, TREES_4:11; take e = vt | r; ::_thesis: ( e = q . i & e is_an_evaluation_of t,f ) len (doms p) = len p by TREES_3:38; hence e = q . i by A2, A7, A4, A10, A11, TREES_4:def_4; ::_thesis: e is_an_evaluation_of t,f reconsider r1 = r as Node of ([o, the carrier of S] -tree p) by A5, A1, Def9; t = ([o, the carrier of S] -tree p) | r1 by A9, A10, A11, TREES_4:def_4; hence e is_an_evaluation_of t,f by A5, A1, Th34; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let A be non-empty MSAlgebra over S; ::_thesis: 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 let V be Variables of A; ::_thesis: 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 let t be c-Term of A,V; ::_thesis: for f being ManySortedFunction of V, the Sorts of A ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f let f be ManySortedFunction of V, the Sorts of A; ::_thesis: ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f defpred S1[ set ] means ex t being c-Term of A,V ex vt being finite DecoratedTree st ( t = \$1 & vt is_an_evaluation_of t,f ); A1: for o being OperSymbol of S for p being ArgumentSeq of o,A,V st ( for t being c-Term of A,V st t in rng p holds S1[t] ) holds S1[(Sym (o,( the Sorts of A \/ V))) -tree p] proof let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of o,A,V st ( for t being c-Term of A,V st t in rng p holds S1[t] ) holds S1[(Sym (o,( the Sorts of A \/ V))) -tree p] let p be ArgumentSeq of o,A,V; ::_thesis: ( ( for t being c-Term of A,V st t in rng p holds S1[t] ) implies S1[(Sym (o,( the Sorts of A \/ V))) -tree p] ) assume A2: for t being c-Term of A,V st t in rng p holds ex u being c-Term of A,V ex vt being finite DecoratedTree st ( u = t & vt is_an_evaluation_of u,f ) ; ::_thesis: S1[(Sym (o,( the Sorts of A \/ V))) -tree p] defpred S2[ set , set ] means ex t being c-Term of A,V ex vt being finite DecoratedTree st ( \$2 = vt & t = p . \$1 & vt is_an_evaluation_of t,f ); A3: for e being set st e in dom p holds ex u being set st S2[e,u] proof let x be set ; ::_thesis: ( x in dom p implies ex u being set st S2[x,u] ) assume x in dom p ; ::_thesis: ex u being set st S2[x,u] then A4: p . x in rng p by FUNCT_1:def_3; rng p c= S -Terms ( the Sorts of A \/ V) by FINSEQ_1:def_4; then reconsider t = p . x as c-Term of A,V by A4; ex u being c-Term of A,V ex vt being finite DecoratedTree st ( u = t & vt is_an_evaluation_of u,f ) by A2, A4; hence ex u being set st S2[x,u] ; ::_thesis: verum end; consider q being Function such that A5: ( dom q = dom p & ( for x being set st x in dom p holds S2[x,q . x] ) ) from CLASSES1:sch_1(A3); dom p = Seg (len p) by FINSEQ_1:def_3; then reconsider q = q as FinSequence by A5, FINSEQ_1:def_2; A6: len p = len q by A5, FINSEQ_3:29; now__::_thesis:_for_x_being_set_st_x_in_dom_q_holds_ q_._x_is_DecoratedTree let x be set ; ::_thesis: ( x in dom q implies q . x is DecoratedTree ) assume x in dom q ; ::_thesis: q . x is DecoratedTree then ex t being c-Term of A,V ex vt being finite DecoratedTree st ( q . x = vt & t = p . x & vt is_an_evaluation_of t,f ) by A5; hence q . x is DecoratedTree ; ::_thesis: verum end; then reconsider q = q as DTree-yielding FinSequence by TREES_3:24; now__::_thesis:_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_) let i be Nat; ::_thesis: 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 ) let t be c-Term of A,V; ::_thesis: ( i in dom p & t = p . i implies ex vt being finite DecoratedTree st ( vt = q . i & vt is_an_evaluation_of t,f ) ) assume i in dom p ; ::_thesis: ( t = p . i implies ex vt being finite DecoratedTree st ( vt = q . i & vt is_an_evaluation_of t,f ) ) then ex t being c-Term of A,V ex vt being finite DecoratedTree st ( q . i = vt & t = p . i & vt is_an_evaluation_of t,f ) by A5; hence ( t = p . i implies ex vt being finite DecoratedTree st ( vt = q . i & vt is_an_evaluation_of t,f ) ) ; ::_thesis: verum end; then 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 ) by A6, Th33; hence S1[(Sym (o,( the Sorts of A \/ V))) -tree p] ; ::_thesis: verum end; A7: for s being SortSymbol of S for v being Element of V . s holds S1[ root-tree [v,s]] proof let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds S1[ root-tree [v,s]] let x be Element of V . s; ::_thesis: S1[ root-tree [x,s]] reconsider t = root-tree [x,s] as c-Term of A,V by Th8; take t ; ::_thesis: ex vt being finite DecoratedTree st ( t = root-tree [x,s] & vt is_an_evaluation_of t,f ) take root-tree ((f . s) . x) ; ::_thesis: ( t = root-tree [x,s] & root-tree ((f . s) . x) is_an_evaluation_of t,f ) thus t = root-tree [x,s] ; ::_thesis: root-tree ((f . s) . x) is_an_evaluation_of t,f thus root-tree ((f . s) . x) is_an_evaluation_of t,f by Th32; ::_thesis: verum end; A8: for s being SortSymbol of S for x being Element of the Sorts of A . s holds S1[ root-tree [x,s]] proof let s be SortSymbol of S; ::_thesis: for x being Element of the Sorts of A . s holds S1[ root-tree [x,s]] let x be Element of the Sorts of A . s; ::_thesis: S1[ root-tree [x,s]] reconsider t = root-tree [x,s] as c-Term of A,V by Th6; take t ; ::_thesis: ex vt being finite DecoratedTree st ( t = root-tree [x,s] & vt is_an_evaluation_of t,f ) take root-tree x ; ::_thesis: ( t = root-tree [x,s] & root-tree x is_an_evaluation_of t,f ) thus t = root-tree [x,s] ; ::_thesis: root-tree x is_an_evaluation_of t,f thus root-tree x is_an_evaluation_of t,f by Th31; ::_thesis: verum end; for t being c-Term of A,V holds S1[t] from MSATERM:sch_2(A8, A7, A1); then ex u being c-Term of A,V ex vt being finite DecoratedTree st ( u = t & vt is_an_evaluation_of u,f ) ; hence ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f ; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let A be non-empty MSAlgebra over S; ::_thesis: 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 let V be Variables of A; ::_thesis: 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 let t be c-Term of A,V; ::_thesis: 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 let f be ManySortedFunction of V, the Sorts of A; ::_thesis: for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds e1 = e2 defpred S1[ c-Term of A,V] means for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of \$1,f & e2 is_an_evaluation_of \$1,f holds e1 = e2; A1: now__::_thesis:_for_s_being_SortSymbol_of_S for_v_being_Element_of_V_._s_holds_S1[v_-term_A] let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds S1[v -term A] let v be Element of V . s; ::_thesis: S1[v -term A] thus S1[v -term A] ::_thesis: verum proof let e1, e2 be finite DecoratedTree; ::_thesis: ( e1 is_an_evaluation_of v -term A,f & e2 is_an_evaluation_of v -term A,f implies e1 = e2 ) set t = v -term A; assume that A2: e1 is_an_evaluation_of v -term A,f and A3: e2 is_an_evaluation_of v -term A,f ; ::_thesis: e1 = e2 A4: dom e1 = dom (v -term A) by A2, Def9; A5: {} is Node of e1 by TREES_1:22; A6: (root-tree [v,s]) . {} = [v,s] by TREES_4:3; then e1 . {} = (f . s) . v by A2, A5, Def9; then A7: e1 = root-tree ((f . s) . v) by A4, TREES_4:3, TREES_4:5; A8: dom e2 = dom (v -term A) by A3, Def9; then e2 . {} = (f . s) . v by A3, A4, A6, A5, Def9; hence e1 = e2 by A8, A7, TREES_4:3, TREES_4:5; ::_thesis: verum end; end; A9: now__::_thesis:_for_o_being_OperSymbol_of_S for_p_being_ArgumentSeq_of_o,A,V_st_(_for_t_being_c-Term_of_A,V_st_t_in_rng_p_holds_ S1[t]_)_holds_ S1[(Sym_(o,(_the_Sorts_of_A_\/_V)))_-tree_p] let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of o,A,V st ( for t being c-Term of A,V st t in rng p holds S1[t] ) holds S1[(Sym (o,( the Sorts of A \/ V))) -tree p] let p be ArgumentSeq of o,A,V; ::_thesis: ( ( for t being c-Term of A,V st t in rng p holds S1[t] ) implies S1[(Sym (o,( the Sorts of A \/ V))) -tree p] ) assume A10: for t being c-Term of A,V st t in rng p holds S1[t] ; ::_thesis: S1[(Sym (o,( the Sorts of A \/ V))) -tree p] thus S1[(Sym (o,( the Sorts of A \/ V))) -tree p] ::_thesis: verum proof set t = (Sym (o,( the Sorts of A \/ V))) -tree p; let e1, e2 be finite DecoratedTree; ::_thesis: ( e1 is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f & e2 is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f implies e1 = e2 ) assume that A11: e1 is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f and A12: e2 is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f ; ::_thesis: e1 = e2 consider q1 being DTree-yielding FinSequence such that A13: len q1 = len p and A14: e1 = ((Den (o,A)) . (roots q1)) -tree q1 and A15: 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 = q1 . i & vt is_an_evaluation_of t,f ) by A11, Th35; consider q2 being DTree-yielding FinSequence such that A16: len q2 = len p and A17: e2 = ((Den (o,A)) . (roots q2)) -tree q2 and A18: 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 = q2 . i & vt is_an_evaluation_of t,f ) by A12, Th35; A19: now__::_thesis:_for_i_being_Element_of_NAT_st_i_<_len_p_holds_ q1_._(i_+_1)_=_q2_._(i_+_1) let i be Element of NAT ; ::_thesis: ( i < len p implies q1 . (i + 1) = q2 . (i + 1) ) assume A20: i < len p ; ::_thesis: q1 . (i + 1) = q2 . (i + 1) then reconsider t = p . (i + 1) as c-Term of A,V by Lm2; A21: ex vt2 being finite DecoratedTree st ( vt2 = q2 . (i + 1) & vt2 is_an_evaluation_of t,f ) by A18, A20, Lm9; ex vt1 being finite DecoratedTree st ( vt1 = q1 . (i + 1) & vt1 is_an_evaluation_of t,f ) by A15, A20, Lm9; hence q1 . (i + 1) = q2 . (i + 1) by A10, A20, A21, Lm9; ::_thesis: verum end; A22: now__::_thesis:_for_i_being_Nat_st_i_in_dom_q1_holds_ q1_._i_=_q2_._i let i be Nat; ::_thesis: ( i in dom q1 implies q1 . i = q2 . i ) assume i in dom q1 ; ::_thesis: q1 . i = q2 . i then ex k being Element of NAT st ( i = k + 1 & k < len q1 ) by Lm1; hence q1 . i = q2 . i by A13, A19; ::_thesis: verum end; A23: dom q2 = Seg (len q2) by FINSEQ_1:def_3; dom q1 = Seg (len q1) by FINSEQ_1:def_3; then q1 = q2 by A13, A16, A23, A22, FINSEQ_1:13; hence e1 = e2 by A14, A17; ::_thesis: verum end; end; A24: now__::_thesis:_for_s_being_SortSymbol_of_S for_x_being_Element_of_the_Sorts_of_A_._s_holds_S1[x_-term_(A,V)] let s be SortSymbol of S; ::_thesis: for x being Element of the Sorts of A . s holds S1[x -term (A,V)] let x be Element of the Sorts of A . s; ::_thesis: S1[x -term (A,V)] thus S1[x -term (A,V)] ::_thesis: verum proof let e1, e2 be finite DecoratedTree; ::_thesis: ( e1 is_an_evaluation_of x -term (A,V),f & e2 is_an_evaluation_of x -term (A,V),f implies e1 = e2 ) set t = x -term (A,V); assume that A25: e1 is_an_evaluation_of x -term (A,V),f and A26: e2 is_an_evaluation_of x -term (A,V),f ; ::_thesis: e1 = e2 A27: dom e1 = dom (x -term (A,V)) by A25, Def9; A28: {} is Node of e1 by TREES_1:22; A29: (root-tree [x,s]) . {} = [x,s] by TREES_4:3; then e1 . {} = x by A25, A28, Def9; then A30: e1 = root-tree x by A27, TREES_4:3, TREES_4:5; A31: dom e2 = dom (x -term (A,V)) by A26, Def9; then e2 . {} = x by A26, A27, A29, A28, Def9; hence e1 = e2 by A31, A30, TREES_4:3, TREES_4:5; ::_thesis: verum end; end; for t being c-Term of A,V holds S1[t] from MSATERM:sch_3(A24, A1, A9); hence for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds e1 = e2 ; ::_thesis: verum end; 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) proof let S be non empty non void ManySortedSign ; ::_thesis: 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) let A be non-empty MSAlgebra over S; ::_thesis: 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) let V be Variables of A; ::_thesis: 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) let t be c-Term of A,V; ::_thesis: 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) let f be ManySortedFunction of V, the Sorts of A; ::_thesis: for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds vt . {} in the Sorts of A . (the_sort_of t) defpred S1[ c-Term of A,V] means for vt being finite DecoratedTree st vt is_an_evaluation_of \$1,f holds vt . {} in the Sorts of A . (the_sort_of \$1); A1: now__::_thesis:_for_s_being_SortSymbol_of_S for_v_being_Element_of_V_._s_holds_S1[v_-term_A] let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds S1[v -term A] let v be Element of V . s; ::_thesis: S1[v -term A] thus S1[v -term A] ::_thesis: verum proof let vt be finite DecoratedTree; ::_thesis: ( vt is_an_evaluation_of v -term A,f implies vt . {} in the Sorts of A . (the_sort_of (v -term A)) ) set t = v -term A; assume A2: vt is_an_evaluation_of v -term A,f ; ::_thesis: vt . {} in the Sorts of A . (the_sort_of (v -term A)) root-tree ((f . s) . v) is_an_evaluation_of v -term A,f by Th32; then vt = root-tree ((f . s) . v) by A2, Th37; then A3: vt . {} = (f . s) . v by TREES_4:3; s = the_sort_of (v -term A) by Th19; hence vt . {} in the Sorts of A . (the_sort_of (v -term A)) by A3; ::_thesis: verum end; end; A4: now__::_thesis:_for_o_being_OperSymbol_of_S for_p_being_ArgumentSeq_of_o,A,V_st_(_for_t_being_c-Term_of_A,V_st_t_in_rng_p_holds_ S1[t]_)_holds_ S1[(Sym_(o,(_the_Sorts_of_A_\/_V)))_-tree_p] let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of o,A,V st ( for t being c-Term of A,V st t in rng p holds S1[t] ) holds S1[(Sym (o,( the Sorts of A \/ V))) -tree p] let p be ArgumentSeq of o,A,V; ::_thesis: ( ( for t being c-Term of A,V st t in rng p holds S1[t] ) implies S1[(Sym (o,( the Sorts of A \/ V))) -tree p] ) assume A5: for t being c-Term of A,V st t in rng p holds S1[t] ; ::_thesis: S1[(Sym (o,( the Sorts of A \/ V))) -tree p] thus S1[(Sym (o,( the Sorts of A \/ V))) -tree p] ::_thesis: verum proof let vt be finite DecoratedTree; ::_thesis: ( vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f implies vt . {} in the Sorts of A . (the_sort_of ((Sym (o,( the Sorts of A \/ V))) -tree p)) ) set t = (Sym (o,( the Sorts of A \/ V))) -tree p; A6: dom ( the Sorts of A * the ResultSort of S) = the carrier' of S by PARTFUN1:def_2; assume vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f ; ::_thesis: vt . {} in the Sorts of A . (the_sort_of ((Sym (o,( the Sorts of A \/ V))) -tree p)) then consider q being DTree-yielding FinSequence such that A7: len q = len p and A8: vt = ((Den (o,A)) . (roots q)) -tree q and A9: 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 ) by Th35; A10: vt . {} = (Den (o,A)) . (roots q) by A8, TREES_4:def_4; now__::_thesis:_(_dom_(roots_q)_=_dom_(_the_Sorts_of_A_*_(the_arity_of_o))_&_(_for_x_being_set_st_x_in_dom_(_the_Sorts_of_A_*_(the_arity_of_o))_holds_ (roots_q)_._x_in_(_the_Sorts_of_A_*_(the_arity_of_o))_._x_)_) A11: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4; A12: dom the Sorts of A = the carrier of S by PARTFUN1:def_2; A13: dom (roots q) = dom q by TREES_3:def_18; hence A14: dom (roots q) = Seg (len q) by FINSEQ_1:def_3 .= Seg (len (the_arity_of o)) by A7, Lm8 .= dom (the_arity_of o) by FINSEQ_1:def_3 .= dom ( the Sorts of A * (the_arity_of o)) by A12, A11, RELAT_1:27 ; ::_thesis: for x being set st x in dom ( the Sorts of A * (the_arity_of o)) holds (roots q) . x in ( the Sorts of A * (the_arity_of o)) . x let x be set ; ::_thesis: ( x in dom ( the Sorts of A * (the_arity_of o)) implies (roots q) . x in ( the Sorts of A * (the_arity_of o)) . x ) assume A15: x in dom ( the Sorts of A * (the_arity_of o)) ; ::_thesis: (roots q) . x in ( the Sorts of A * (the_arity_of o)) . x then consider i being Element of NAT such that A16: x = i + 1 and A17: i < len q by A13, A14, Lm1; A18: ex T being DecoratedTree st ( T = q . (i + 1) & (roots q) . (i + 1) = T . {} ) by A13, A14, A15, A16, TREES_3:def_18; i + 1 in dom p by A7, A17, Lm9; then A19: ex t being c-Term of A,V st ( t = p . (i + 1) & t = p /. (i + 1) & the_sort_of t = (the_arity_of o) . (i + 1) & the_sort_of t = (the_arity_of o) /. (i + 1) ) by Lm8; reconsider t = p . (i + 1) as c-Term of A,V by A7, A17, Lm2; consider vt being finite DecoratedTree such that A20: vt = q . (i + 1) and A21: vt is_an_evaluation_of t,f by A7, A9, A17, Lm9; vt . {} in the Sorts of A . (the_sort_of t) by A5, A7, A17, A21, Lm9; hence (roots q) . x in ( the Sorts of A * (the_arity_of o)) . x by A15, A16, A18, A20, A19, FUNCT_1:12; ::_thesis: verum end; then roots q in product ( the Sorts of A * (the_arity_of o)) by CARD_3:9; then roots q in ( the Sorts of A #) . (the_arity_of o) by FINSEQ_2:def_5; then A22: roots q in ( the Sorts of A #) . ( the Arity of S . o) by MSUALG_1:def_1; dom (( the Sorts of A #) * the Arity of S) = the carrier' of S by PARTFUN1:def_2; then roots q in (( the Sorts of A #) * the Arity of S) . o by A22, FUNCT_1:12; then A23: roots q in Args (o,A) by MSUALG_1:def_4; Result (o,A) = ( the Sorts of A * the ResultSort of S) . o by MSUALG_1:def_5 .= the Sorts of A . ( the ResultSort of S . o) by A6, FUNCT_1:12 .= the Sorts of A . (the_result_sort_of o) by MSUALG_1:def_2 .= the Sorts of A . (the_sort_of ((Sym (o,( the Sorts of A \/ V))) -tree p)) by Th20 ; hence vt . {} in the Sorts of A . (the_sort_of ((Sym (o,( the Sorts of A \/ V))) -tree p)) by A10, A23, FUNCT_2:5; ::_thesis: verum end; end; A24: now__::_thesis:_for_s_being_SortSymbol_of_S for_x_being_Element_of_the_Sorts_of_A_._s_holds_S1[x_-term_(A,V)] let s be SortSymbol of S; ::_thesis: for x being Element of the Sorts of A . s holds S1[x -term (A,V)] let x be Element of the Sorts of A . s; ::_thesis: S1[x -term (A,V)] thus S1[x -term (A,V)] ::_thesis: verum proof let vt be finite DecoratedTree; ::_thesis: ( vt is_an_evaluation_of x -term (A,V),f implies vt . {} in the Sorts of A . (the_sort_of (x -term (A,V))) ) set t = x -term (A,V); assume A25: vt is_an_evaluation_of x -term (A,V),f ; ::_thesis: vt . {} in the Sorts of A . (the_sort_of (x -term (A,V))) root-tree x is_an_evaluation_of x -term (A,V),f by Th31; then vt = root-tree x by A25, Th37; then A26: vt . {} = x by TREES_4:3; s = the_sort_of (x -term (A,V)) by Th15; hence vt . {} in the Sorts of A . (the_sort_of (x -term (A,V))) by A26; ::_thesis: verum end; end; for t being c-Term of A,V holds S1[t] from MSATERM:sch_3(A24, A1, A4); hence for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds vt . {} in the Sorts of A . (the_sort_of t) ; ::_thesis: verum end; 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 . {} ) proof consider vt being finite DecoratedTree such that A1: vt is_an_evaluation_of t,f by Th36; reconsider tf = vt . {} as Element of the Sorts of A . (the_sort_of t) by A1, Th38; take tf ; ::_thesis: ex vt being finite DecoratedTree st ( vt is_an_evaluation_of t,f & tf = vt . {} ) take vt ; ::_thesis: ( vt is_an_evaluation_of t,f & tf = vt . {} ) thus ( vt is_an_evaluation_of t,f & tf = vt . {} ) by A1; ::_thesis: verum end; 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 . {} proof let S be non empty non void ManySortedSign ; ::_thesis: 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 . {} let A be non-empty MSAlgebra over S; ::_thesis: 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 . {} let V be Variables of A; ::_thesis: 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 . {} let f be ManySortedFunction of V, the Sorts of A; ::_thesis: 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 . {} let t be c-Term of A,V; ::_thesis: for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds t @ f = vt . {} A1: ex e being finite DecoratedTree st ( e is_an_evaluation_of t,f & t @ f = e . {} ) by Def10; let vt be finite DecoratedTree; ::_thesis: ( vt is_an_evaluation_of t,f implies t @ f = vt . {} ) assume vt is_an_evaluation_of t,f ; ::_thesis: t @ f = vt . {} hence t @ f = vt . {} by A1, Th37; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let A be non-empty MSAlgebra over S; ::_thesis: 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 let V be Variables of A; ::_thesis: 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 let f be ManySortedFunction of V, the Sorts of A; ::_thesis: 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 let t be c-Term of A,V; ::_thesis: 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 let vt be finite DecoratedTree; ::_thesis: ( vt is_an_evaluation_of t,f implies for p being Node of t holds vt . p = (t | p) @ f ) assume A1: vt is_an_evaluation_of t,f ; ::_thesis: for p being Node of t holds vt . p = (t | p) @ f let p be Node of t; ::_thesis: vt . p = (t | p) @ f reconsider n = p as Node of vt by A1, Def9; A2: n ^ {} = n by FINSEQ_1:34; A3: {} in (dom vt) | p by TREES_1:22; (t | p) @ f = (vt | n) . (<*> NAT) by A1, Th34, Th39; hence vt . p = (t | p) @ f by A2, A3, TREES_2:def_10; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let A be non-empty MSAlgebra over S; ::_thesis: 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 let V be Variables of A; ::_thesis: 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 let f be ManySortedFunction of V, the Sorts of A; ::_thesis: for s being SortSymbol of S for x being Element of the Sorts of A . s holds (x -term (A,V)) @ f = x let s be SortSymbol of S; ::_thesis: for x being Element of the Sorts of A . s holds (x -term (A,V)) @ f = x let x be Element of the Sorts of A . s; ::_thesis: (x -term (A,V)) @ f = x x = (root-tree x) . {} by TREES_4:3; hence (x -term (A,V)) @ f = x by Th31, Th39; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let A be non-empty MSAlgebra over S; ::_thesis: 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 let V be Variables of A; ::_thesis: 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 let f be ManySortedFunction of V, the Sorts of A; ::_thesis: for s being SortSymbol of S for v being Element of V . s holds (v -term A) @ f = (f . s) . v let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds (v -term A) @ f = (f . s) . v let v be Element of V . s; ::_thesis: (v -term A) @ f = (f . s) . v (f . s) . v = (root-tree ((f . s) . v)) . {} by TREES_4:3; hence (v -term A) @ f = (f . s) . v by Th32, Th39; ::_thesis: verum end; 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 proof let S be non empty non void ManySortedSign ; ::_thesis: 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 let A be non-empty MSAlgebra over S; ::_thesis: 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 let V be Variables of A; ::_thesis: 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 let f be ManySortedFunction of V, the Sorts of A; ::_thesis: 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 let o be OperSymbol of S; ::_thesis: 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 let p be ArgumentSeq of o,A,V; ::_thesis: 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 let q be FinSequence; ::_thesis: ( 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 ) implies ((Sym (o,( the Sorts of A \/ V))) -tree p) @ f = (Den (o,A)) . q ) assume that A1: len q = len p and A2: 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 ; ::_thesis: ((Sym (o,( the Sorts of A \/ V))) -tree p) @ f = (Den (o,A)) . q consider vt being finite DecoratedTree such that A3: vt is_an_evaluation_of (Sym (o,( the Sorts of A \/ V))) -tree p,f by Th36; consider r being DTree-yielding FinSequence such that A4: len r = len p and A5: vt = ((Den (o,A)) . (roots r)) -tree r and A6: 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 = r . i & vt is_an_evaluation_of t,f ) by A3, Th35; now__::_thesis:_(_dom_p_=_dom_p_&_dom_q_=_dom_p_&_dom_r_=_dom_p_&_(_for_i_being_Element_of_NAT_st_i_in_dom_r_holds_ ex_T_being_DecoratedTree_st_ (_T_=_r_._i_&_q_._i_=_T_._{}_)_)_) thus A7: ( dom p = dom p & dom q = dom p & dom r = dom p ) by A1, A4, FINSEQ_3:29; ::_thesis: for i being Element of NAT st i in dom r holds ex T being DecoratedTree st ( T = r . i & q . i = T . {} ) let i be Element of NAT ; ::_thesis: ( i in dom r implies ex T being DecoratedTree st ( T = r . i & q . i = T . {} ) ) assume A8: i in dom r ; ::_thesis: ex T being DecoratedTree st ( T = r . i & q . i = T . {} ) then reconsider t = p . i as c-Term of A,V by A7, Th22; consider vt being finite DecoratedTree such that A9: vt = r . i and A10: vt is_an_evaluation_of t,f by A6, A7, A8; reconsider T = vt as DecoratedTree ; take T = T; ::_thesis: ( T = r . i & q . i = T . {} ) thus T = r . i by A9; ::_thesis: q . i = T . {} thus q . i = t @ f by A2, A7, A8 .= T . {} by A10, Th39 ; ::_thesis: verum end; then q = roots r by TREES_3:def_18; hence ((Sym (o,( the Sorts of A \/ V))) -tree p) @ f = (((Den (o,A)) . q) -tree r) . {} by A3, A5, Th39 .= (Den (o,A)) . q by TREES_4:def_4 ; ::_thesis: verum end;