:: Terms over many sorted universal algebra :: by Grzegorz Bancerek :: :: Received November 25, 1994 :: Copyright (c) 1994-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies FINSEQ_1, RELAT_1, SUBSET_1, NUMBERS, ARYTM_3, XXREAL_0, NAT_1, CARD_1, FUNCT_1, TARSKI, STRUCT_0, XBOOLE_0, MSUALG_1, PBOOLE, TREES_3, MSAFREE, DTCONSTR, LANG1, ZFMISC_1, TREES_4, TDGROUP, CARD_3, TREES_2, FINSET_1, MARGREL1, PARTFUN1, TREES_9, ORDINAL4, ORDINAL1, TREES_1, MCART_1, FUNCT_6, TREES_A, QC_LANG1, MSATERM, SETLIM_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, XTUPLE_0, MCART_1, RELAT_1, STRUCT_0, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, FUNCT_2, FINSET_1, TREES_1, TREES_2, CARD_3, FUNCT_6, LANG1, TREES_3, TREES_4, TREES_9, PBOOLE, MSUALG_1, DTCONSTR, MSUALG_3, MSAFREE, XXREAL_0; constructors NAT_1, NAT_D, TREES_9, MSUALG_3, MSAFREE, RELSET_1, XTUPLE_0; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, FINSEQ_1, PBOOLE, TREES_2, TREES_3, TREES_9, STRUCT_0, DTCONSTR, MSUALG_1, MSUALG_2, MSAFREE, FINSET_1, TREES_1, RELSET_1, XTUPLE_0; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve S for non void non empty ManySortedSign, V for non-empty ManySortedSet of the carrier of S; definition let S; let V be ManySortedSet of the carrier of S; func S-Terms V -> Subset of FinTrees the carrier of DTConMSA V equals :: MSATERM:def 1 TS DTConMSA V; end; registration let S, V; cluster S-Terms V -> non empty; end; definition let S, V; mode Term of S,V is Element of S-Terms V; end; reserve A for MSAlgebra over S, t for Term of S,V; definition let S, V; let o be OperSymbol of S; redefine func Sym(o, V) -> NonTerminal of DTConMSA V; end; definition let S, V; let sy be NonTerminal of DTConMSA V; mode ArgumentSeq of sy -> FinSequence of S-Terms V means :: MSATERM:def 2 it is SubtreeSeq of sy; end; theorem :: MSATERM:1 for o being OperSymbol of S, 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); scheme :: MSATERM:sch 1 TermInd { S() -> non void non empty ManySortedSign, V() -> non-empty ManySortedSet of the carrier of S(), P[set] }: for t being Term of S(),V() holds P[t] provided for s being SortSymbol of S(), v being Element of V().s holds P[ root-tree [v,s]] and for o being OperSymbol of S(), p being ArgumentSeq of Sym(o,V()) st for t being Term of S(),V() st t in rng p holds P[t] holds P[[o,the carrier of S()]-tree p]; definition let S, A, V; mode c-Term of A,V is Term of S, (the Sorts of A) (\/) V; end; definition let S, A, V; 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 { S() -> non void non empty ManySortedSign, A() -> non-empty MSAlgebra over S(), V() -> non-empty ManySortedSet of the carrier of S(), P[set ] }: for t being c-Term of A(),V() holds P[t] provided for s being SortSymbol of S(), x being Element of (the Sorts of A()) .s holds P[root-tree [x,s]] and for s being SortSymbol of S(), v being Element of V().s holds P[ root-tree [v,s]] and for o being OperSymbol of S(), p being ArgumentSeq of o,A(),V() st for t being c-Term of A(),V() st t in rng p holds P[t] holds P[Sym(o,(the Sorts of A()) (\/) V())-tree p]; definition let S, V, t; let p be Node of t; redefine func t.p -> Symbol of DTConMSA V; end; registration let S, V; cluster -> finite for Term of S,V; end; theorem :: MSATERM:2 (ex s being SortSymbol of S, v being Element of V.s st t.{} = [v, s]) or t.{} in [:the carrier' of S,{the carrier of S}:]; theorem :: MSATERM:3 for t being c-Term of A,V holds (ex s being SortSymbol of S, x being set st x in (the Sorts of A).s & t.{} = [x,s]) or (ex s being SortSymbol of S, v being Element of V.s st t.{} = [v,s]) or t.{} in [:the carrier' of S,{the carrier of S}:]; theorem :: MSATERM:4 for s being SortSymbol of S, v being Element of V.s holds root-tree [v,s] is Term of S, V; theorem :: MSATERM:5 for s being SortSymbol of S, v being Element of V.s st t.{} = [v, s] holds t = root-tree [v,s]; theorem :: MSATERM:6 for s being SortSymbol of S, x being set st x in (the Sorts of A) .s holds root-tree [x,s] is c-Term of A, V; theorem :: MSATERM:7 for t being c-Term of A,V for s being SortSymbol of S, x being set st x in (the Sorts of A).s & t.{} = [x,s] holds t = root-tree [x,s]; theorem :: MSATERM:8 for s being SortSymbol of S, v being Element of V.s holds root-tree [v,s] is c-Term of A, V; theorem :: MSATERM:9 for t being c-Term of A,V for s being SortSymbol of S, v being Element of V.s st t.{} = [v,s] holds t = root-tree [v,s]; theorem :: MSATERM:10 for o being OperSymbol of S st t.{} = [o,the carrier of S] ex a being ArgumentSeq of Sym(o,V) st t = [o,the carrier of S]-tree a; definition let S; let A be non-empty MSAlgebra over S; let V; let s be SortSymbol of S; let x be Element of (the Sorts of A).s; func x-term(A,V) -> c-Term of A,V equals :: MSATERM:def 3 root-tree [x,s]; end; definition let S, A, V; let s be SortSymbol of S; let v be Element of V.s; func v-term A -> c-Term of A,V equals :: MSATERM:def 4 root-tree [v,s]; end; definition let S, V; let sy be NonTerminal of DTConMSA V; let p be ArgumentSeq of sy; redefine func sy-tree p -> Term of S,V; end; scheme :: MSATERM:sch 3 TermInd2 { S() -> non void non empty ManySortedSign, A() -> non-empty MSAlgebra over S(), V() -> non-empty ManySortedSet of the carrier of S(), P[set ] }: for t being c-Term of A(),V() holds P[t] provided for s being SortSymbol of S(), x being Element of (the Sorts of A()) .s holds P[x-term (A(), V())] and for s being SortSymbol of S(), v being Element of V().s holds P[v -term A()] and for o being OperSymbol of S(), p being ArgumentSeq of Sym(o,(the Sorts of A()) (\/) V()) st for t being c-Term of A(),V() st t in rng p holds P[t] holds P[Sym(o,(the Sorts of A()) (\/) V())-tree p]; begin :: Sort of a term theorem :: MSATERM:11 for t being Term of S,V ex s being SortSymbol of S st t in FreeSort (V, s); theorem :: MSATERM:12 for s being SortSymbol of S holds FreeSort (V, s) c= S-Terms V; theorem :: MSATERM:13 S-Terms V = Union FreeSort V; definition let S, V, t; func the_sort_of t -> SortSymbol of S means :: MSATERM:def 5 t in FreeSort (V, it); end; theorem :: MSATERM:14 for s being SortSymbol of S, v be Element of V.s st t = root-tree [v,s] holds the_sort_of t = s; theorem :: MSATERM:15 for t being c-Term of A,V for s being SortSymbol of S, x be set st x in (the Sorts of A).s & t = root-tree [x,s] holds the_sort_of t = s; theorem :: MSATERM:16 for t being c-Term of A,V for s being SortSymbol of S, v being Element of V.s st t = root-tree [v,s] holds the_sort_of t = s; theorem :: MSATERM:17 for o being OperSymbol of S st t.{} = [o,the carrier of S] holds the_sort_of t = the_result_sort_of o; theorem :: MSATERM:18 for A being non-empty MSAlgebra over S for s being SortSymbol of S, x being Element of (the Sorts of A).s holds the_sort_of (x-term (A,V)) = s; theorem :: MSATERM:19 for s being SortSymbol of S, v being Element of V.s holds the_sort_of (v-term A) = s; theorem :: MSATERM:20 for o being OperSymbol of S, p being ArgumentSeq of Sym(o,V) holds the_sort_of (Sym(o,V)-tree p qua Term of S,V) = the_result_sort_of o; begin :: Argument Sequence theorem :: MSATERM:21 for o being OperSymbol of S, a being FinSequence of S-Terms V holds a is ArgumentSeq of Sym(o,V) iff Sym(o, V) ==> roots a; theorem :: MSATERM:22 for o being OperSymbol of S, 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; theorem :: MSATERM:23 for o being OperSymbol of S, a being ArgumentSeq of Sym(o,V) for i being Nat st i in dom a for t being Term of S,V st t = a.i holds t = (a qua FinSequence of S-Terms V qua non empty set)/.i & the_sort_of t = (the_arity_of o).i & the_sort_of t = (the_arity_of o)/.i; theorem :: MSATERM:24 for o being OperSymbol of S, 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 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 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); theorem :: MSATERM:25 for o being OperSymbol of S, 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 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 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); theorem :: MSATERM:26 for S being non void non empty ManySortedSign, V1,V2 being non-empty ManySortedSet of the carrier of S st V1 c= V2 for t being Term of S, V1 holds t is Term of S, V2; theorem :: MSATERM:27 for S being non void non empty ManySortedSign, A being MSAlgebra over S, V being non-empty ManySortedSet of the carrier of S, t being Term of S, V holds t is c-Term of A, V; begin :: Compound terms definition let S be non void non empty ManySortedSign; let V be non-empty 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}:]; end; definition let S be non void non empty ManySortedSign; let V be non-empty 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; end; theorem :: MSATERM:28 t is not root implies t is CompoundTerm of S,V; theorem :: MSATERM:29 for p being Node of t holds t|p is Term of S,V; definition let S be non void non empty ManySortedSign; let V be non-empty ManySortedSet of the carrier of S; let t be Term of S,V; let p be Node of t; redefine func t|p -> Term of S,V; end; begin :: Evaluation of terms definition let S be non void non empty ManySortedSign; let A be MSAlgebra over S; mode Variables of A -> non-empty ManySortedSet of the carrier of S means :: MSATERM:def 8 it misses the Sorts of A; end; theorem :: MSATERM:30 for V being Variables of A for s being SortSymbol of S, x being set st x in (the Sorts of A).s for v being Element of V.s holds x <> v; definition let S be non void non empty ManySortedSign; let A be non-empty MSAlgebra over S; let V be non-empty 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; pred vt is_an_evaluation_of t,f means :: MSATERM:def 9 dom vt = dom t & for p being Node of vt holds (for s being SortSymbol of S, v being Element of V.s st t.p = [v,s] holds vt.p = f.s.v) & (for s being SortSymbol of S, 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; reserve S for non void non empty ManySortedSign, A for non-empty MSAlgebra over S, V for Variables of A, t for c-Term of A,V, f for ManySortedFunction of V, the Sorts of A; theorem :: MSATERM:31 for s being SortSymbol of S, 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; theorem :: MSATERM:32 for s being SortSymbol of S, v being Element of V.s st t = root-tree [v,s] holds root-tree (f.s.v) is_an_evaluation_of t,f; theorem :: MSATERM:33 for o being OperSymbol of S, p being ArgumentSeq of o,A,V for q being DTree-yielding FinSequence st len q = len p & for i being Nat, t being c-Term of A,V st i in dom p & t = p.i ex vt being finite DecoratedTree st vt = q.i & vt is_an_evaluation_of t,f 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 qua c-Term of A,V), f; theorem :: MSATERM:34 for t being c-Term of A,V, e being finite DecoratedTree st e is_an_evaluation_of t,f for p being Node of t, n being Node of e st n = p holds e|n is_an_evaluation_of t|p, f; theorem :: MSATERM:35 for o being OperSymbol of S, 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 qua c-Term of A,V), f ex q being DTree-yielding FinSequence st len q = len p & vt = (Den(o,A).roots q)-tree q & for i being Nat, t being c-Term of A ,V st i in dom p & t = p.i ex vt being finite DecoratedTree st vt = q.i & vt is_an_evaluation_of t,f; theorem :: MSATERM:36 ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f; theorem :: MSATERM:37 for e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds e1 = e2; theorem :: MSATERM:38 for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds vt.{} in (the Sorts of A).the_sort_of t; definition let S be non void non empty 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; func t@f -> Element of (the Sorts of A).the_sort_of t means :: MSATERM:def 10 ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f & it = vt.{}; end; reserve t for c-Term of A,V; theorem :: MSATERM:39 for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds t@f = vt.{}; theorem :: MSATERM:40 for vt being finite DecoratedTree st vt is_an_evaluation_of t,f for p being Node of t holds vt.p = (t|p)@f; theorem :: MSATERM:41 for s being SortSymbol of S, x being Element of (the Sorts of A).s holds (x-term(A,V))@f = x; theorem :: MSATERM:42 for s being SortSymbol of S, v being Element of V.s holds (v-term A)@f = f.s.v; theorem :: MSATERM:43 for o being OperSymbol of S, 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 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 qua c-Term of A,V)@f = Den(o,A).q;