:: Terms over many sorted universal algebra
:: by Grzegorz Bancerek
::
:: Received November 25, 1994
:: Copyright (c) 1994-2026 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;
definitions TARSKI, PBOOLE, XBOOLE_0;
equalities TARSKI;
expansions TARSKI, PBOOLE;
theorems TARSKI, NAT_1, ZFMISC_1, CARD_3, FUNCT_1, FINSEQ_1, FUNCT_2,
FINSEQ_3, FINSEQ_4, CARD_5, FUNCT_6, TREES_1, TREES_2, TREES_3, TREES_4,
LANG1, DTCONSTR, TREES_9, PBOOLE, MSUALG_1, MSAFREE, DOMAIN_1, RELAT_1,
XBOOLE_0, FINSET_1, XREAL_1, ORDINAL1, PARTFUN1, FINSEQ_2, XTUPLE_0;
schemes TREES_2, CLASSES1, DTCONSTR, PBOOLE;
begin
Lm1: for n being set, p being FinSequence st n in dom p ex k being Element of
NAT st n = k+1 & k < len p
proof
let n be set, p be FinSequence;
assume
A1: n in dom p;
then reconsider 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 as Element of NAT by ORDINAL1:def 12;
take k;
n <= len p by A1,FINSEQ_3:25;
hence thesis by A2,NAT_1:13;
end;
Lm2: now
let n be Element of NAT, x be set;
let p be FinSequence of x;
n >= 0 by NAT_1:2;
then
A1: n+1 >= 0+1 by XREAL_1:7;
assume n < len p;
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;
end;
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
:Def1:
TS DTConMSA V;
correctness;
end;
registration
let S, V;
cluster S-Terms V -> non empty;
correctness;
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; :: redefines Sym (MSAFREE, definition)
coherence
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 thesis by A2,A1,ZFMISC_1:87;
end;
end;
definition
let S, V;
let sy be NonTerminal of DTConMSA V;
mode ArgumentSeq of sy -> FinSequence of S-Terms V means
:Def2:
it is SubtreeSeq of sy;
existence
proof
set q = the SubtreeSeq of sy;
q is FinSequence of S-Terms V;
hence thesis;
end;
end;
theorem Th1:
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)
proof
let o be OperSymbol of S, a be FinSequence;
A1: [o,the carrier of S] = Sym(o, V) by MSAFREE:def 9;
A2: S-Terms V = TS DTConMSA V;
hereby
assume [o,the carrier of S]-tree a in S-Terms V;
then reconsider
t = [o,the carrier of S]-tree a as Element of TS DTConMSA V;
assume
A3: a is DTree-yielding;
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;
end;
assume a is ArgumentSeq of Sym(o,V);
then reconsider 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 thesis by A1,DTCONSTR:def 1;
end;
Lm3: now
let S, V;
let x be set;
set X = V, G = DTConMSA X;
A1: Terminals G = Union coprod X by MSAFREE:6;
hereby
assume x in Terminals G;
then consider s being object such that
A2: s in dom coprod X and
A3: x in (coprod X).s by A1,CARD_5:2;
reconsider s as SortSymbol of S by A2,PARTFUN1:def 2;
(coprod X).s = coprod(s, X) by MSAFREE:def 3;
then ex a being set st a in X.s & x = [a,s] by A3,MSAFREE:def 2;
hence ex s being SortSymbol of S, v being Element of V.s st x = [v,s];
end;
let s be SortSymbol of S;
let a be Element of V.s;
assume x = [a,s];
then x in coprod (s, X) by MSAFREE:def 2;
then
A4: x in (coprod X).s by MSAFREE:def 3;
dom coprod X = the carrier of S by PARTFUN1:def 2;
hence x in Terminals G by A1,A4,CARD_5:2;
end;
Lm4: now
let S, A, V;
let x be set;
set X = (the Sorts of A) (\/) V, G = DTConMSA X;
A1: dom coprod X = the carrier of S by PARTFUN1:def 2;
A2: Terminals G = Union coprod X by MSAFREE:6;
hereby
assume x in Terminals G;
then consider s being object such that
A3: s in dom coprod X and
A4: x in (coprod X).s by A2,CARD_5:2;
reconsider s as SortSymbol of S by A3,PARTFUN1:def 2;
(coprod X).s = coprod(s, X) by MSAFREE:def 3;
then consider a being set such that
A5: a in X.s and
A6: x = [a,s] by A4,MSAFREE:def 2;
X.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, a being set st a in (the Sorts of A).s &
x = [a,s]) or ex s being SortSymbol of S, v being Element of V.s st x = [v,s]
by A6;
end;
let s be SortSymbol of S;
A7: X.s = (the Sorts of A).s \/ V.s by PBOOLE:def 4;
hereby
let a be set;
assume a in (the Sorts of A).s;
then
A8: a in X.s by A7,XBOOLE_0:def 3;
assume x = [a,s];
then x in coprod (s, X) by A8,MSAFREE:def 2;
then x in (coprod X).s by MSAFREE:def 3;
hence x in Terminals G by A2,A1,CARD_5:2;
end;
let a be Element of V.s;
assume
A9: x = [a,s];
a in X.s by A7,XBOOLE_0:def 3;
then x in coprod (s, X) by A9,MSAFREE:def 2;
then x in (coprod X).s by MSAFREE:def 3;
hence x in Terminals G by A2,A1,CARD_5:2;
end;
Lm5: now
let S, V;
set G = DTConMSA V;
let x be set;
NonTerminals G = [:the carrier' of S,{the carrier of S}:] by MSAFREE:6;
hence
x is NonTerminal of G iff x in [:the carrier' of S,{the carrier of S}:];
end;
scheme
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
A1: for s being SortSymbol of S(), v being Element of V().s holds P[
root-tree [v,s]] and
A2: 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]
proof
set X = V(), G = DTConMSA X;
A3: for nt being Symbol of G, ts being FinSequence of TS G st nt ==> roots
ts & for t being DecoratedTree of the carrier of G st t in rng ts holds P[t]
holds P[nt-tree ts]
proof
let nt be Symbol of G, ts be FinSequence of TS G such that
A4: nt ==> roots ts and
A5: for t being DecoratedTree of the carrier of G st t in rng ts holds P[t];
nt in {s where s is Symbol of G: ex n being FinSequence st s ==> n} by A4;
then reconsider sy = nt as NonTerminal of G by LANG1:def 3;
reconsider p = ts as FinSequence of S()-Terms X;
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
A6: sy = [o,x2] by DOMAIN_1:1;
A7: x2 = the carrier of S() by TARSKI:def 1;
[o,the carrier of S()] = Sym(o,X) by MSAFREE:def 9;
then ts is SubtreeSeq of Sym(o,X) by A4,A6,A7,DTCONSTR:def 6;
then reconsider p as ArgumentSeq of Sym(o,V()) by Def2;
for t be Term of S(),V() st t in rng p holds P[t] by A5;
hence thesis by A2,A6,A7;
end;
A8: for s being Symbol of G st s in Terminals G holds P[root-tree s]
proof
let x be Symbol of G;
assume x in Terminals G;
then ex s being SortSymbol of S(), v being Element of V().s st x = [v,s ]
by Lm3;
hence thesis by A1;
end;
for t being DecoratedTree of the carrier of G st t in TS G holds P[t]
from DTCONSTR:sch 7(A8,A3);
hence thesis;
end;
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
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
A1: for s being SortSymbol of S(), x being Element of (the Sorts of A())
.s holds P[root-tree [x,s]] and
A2: for s being SortSymbol of S(), v being Element of V().s holds P[
root-tree [v,s]] and
A3: 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]
proof
set X = (the Sorts of A()) (\/) V(), G = DTConMSA X;
A4: for nt being Symbol of G, ts being FinSequence of TS G st nt ==> roots
ts & for t being DecoratedTree of the carrier of G st t in rng ts holds P[t]
holds P[nt-tree ts]
proof
let nt be Symbol of G, ts be FinSequence of TS G such that
A5: nt ==> roots ts and
A6: for t being DecoratedTree of the carrier of G st t in rng ts holds P[t];
nt in {s where s is Symbol of G: ex n being FinSequence st s ==> n} by A5;
then reconsider sy = nt as NonTerminal of G by LANG1:def 3;
reconsider p = ts as FinSequence of S()-Terms X;
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
A7: sy = [o,x2] by DOMAIN_1:1;
A8: [o,the carrier of S()] = Sym(o,X) by MSAFREE:def 9;
A9: x2 = the carrier of S() by TARSKI:def 1;
then ts is SubtreeSeq of Sym(o,X) by A5,A7,A8,DTCONSTR:def 6;
then reconsider p as ArgumentSeq of Sym(o,(the Sorts of A()) (\/) V())
by Def2;
for t be c-Term of A(),V() st t in rng p holds P[t] by A6;
hence thesis by A3,A7,A9,A8;
end;
A10: for s being Symbol of G st s in Terminals G holds P[root-tree s]
proof
let x be Symbol of G;
assume x in Terminals G;
then
(ex s being SortSymbol of S(), a being set st a in (the Sorts of A()).
s & x = [a,s]) or ex s being SortSymbol of S(), v being Element of V().s st x =
[v,s] by Lm4;
hence thesis by A1,A2;
end;
for t being DecoratedTree of the carrier of G st t in TS G holds P[t]
from DTCONSTR:sch 7(A10,A4);
hence thesis;
end;
definition
let S, V, t;
let p be Node of t;
redefine func t.p -> Symbol of DTConMSA V; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider t as Element of TS DTConMSA V;
reconsider t as DecoratedTree of the carrier of DTConMSA V;
reconsider p as Node of t;
t.p = t.p;
hence thesis;
end;
end;
registration
let S, V;
cluster -> finite for Term of S,V;
coherence;
end;
Lm6: now
let G be with_terminals with_nonterminals non empty DTConstrStr;
let s be Symbol 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;
(Terminals G) misses (NonTerminals G) by DTCONSTR:8;
hence not (s is Terminal of G & s is NonTerminal of G) by XBOOLE_0:3;
end;
theorem Th2:
(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}:]
proof
set G = DTConMSA V;
A1: the carrier of G = (Terminals G) \/ (NonTerminals G) by LANG1:1;
reconsider e = {} as Node of t by TREES_1:22;
NonTerminals G = [:the carrier' of S,{the carrier of S}:] by MSAFREE:6;
then t.e in Terminals G or t.e in [:the carrier' of S,{the carrier of S} :]
by A1,XBOOLE_0:def 3;
hence thesis by Lm3;
end;
theorem
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}:]
proof
let t be c-Term of A,V;
set G = DTConMSA ((the Sorts of A) (\/) V);
A1: the carrier of G = (Terminals G) \/ (NonTerminals G) by LANG1:1;
reconsider e = {} as Node of t by TREES_1:22;
NonTerminals G = [:the carrier' of S,{the carrier of S}:] by MSAFREE:6;
then
t.e in Terminals G or t.e in [:the carrier' of S,{the carrier of S}:] by A1,
XBOOLE_0:def 3;
hence thesis by Lm4;
end;
theorem Th4:
for s being SortSymbol of S, v being Element of V.s holds
root-tree [v,s] is Term of S, V
proof
let s be SortSymbol of S, v be Element of V.s;
reconsider vs = [v,s] as Terminal of DTConMSA V by MSAFREE:7;
root-tree vs in TS DTConMSA V;
hence thesis;
end;
theorem Th5:
for s being SortSymbol of S, v being Element of V.s st t.{} = [v,
s] holds t = root-tree [v,s]
proof
let s be SortSymbol of S, x be Element of V.s;
set G = DTConMSA V;
reconsider a = [x,s] as Terminal of G by Lm3;
reconsider t as Element of TS G;
t.{} = a implies t = root-tree a by DTCONSTR:9;
hence thesis;
end;
theorem Th6:
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
proof
let s be SortSymbol of S, x be set;
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;
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 thesis;
end;
theorem
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]
proof
let t be c-Term of A,V;
let s be SortSymbol of S, x be set;
set G = DTConMSA ((the Sorts of A) (\/) V);
reconsider t as Element of TS G;
assume x in (the Sorts of A).s;
then reconsider a = [x,s] as Terminal of G by Lm4;
t.{} = a implies t = root-tree a by DTCONSTR:9;
hence thesis;
end;
theorem Th8:
for s being SortSymbol of S, v being Element of V.s holds
root-tree [v,s] is c-Term of A, V
proof
let s be SortSymbol of S, v be Element of V.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;
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 thesis;
end;
theorem
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]
proof
let t be c-Term of A,V;
let s be SortSymbol of S, x be Element of V.s;
set G = DTConMSA ((the Sorts of A) (\/) V);
reconsider a = [x,s] as Terminal of G by Lm4;
reconsider t as Element of TS G;
t.{} = a implies t = root-tree a by DTCONSTR:9;
hence thesis;
end;
theorem Th10:
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
proof
let o be OperSymbol of S such that
A1: t.{} = [o,the carrier of S];
set X = V, G = DTConMSA X;
reconsider t as Element of TS G;
[o,the carrier of S] = Sym(o, X) by MSAFREE:def 9;
then consider p being FinSequence of TS G such that
A2: t = Sym(o,X)-tree p and
A3: Sym(o,X) ==> roots p by A1,DTCONSTR:10;
reconsider a = p as FinSequence of S-Terms V;
a is SubtreeSeq of Sym(o,X) by A3,DTCONSTR:def 6;
then reconsider a as ArgumentSeq of Sym(o,V) by Def2;
take a;
thus thesis by A2,MSAFREE:def 9;
end;
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
root-tree [x,s];
correctness by Th6;
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
root-tree [v,s];
correctness by Th8;
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; :: redefines -tree (TREES_4, definition)
coherence
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 thesis by A1,A2,Th1;
end;
end;
scheme
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
A1: for s being SortSymbol of S(), x being Element of (the Sorts of A())
.s holds P[x-term (A(), V())] and
A2: for s being SortSymbol of S(), v being Element of V().s holds P[v
-term A()] and
A3: 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]
proof
A4: now
let s be SortSymbol of S(), x be Element of (the Sorts of A()).s;
P[x-term (A(), V())] by A1;
hence P[root-tree [x,s]];
end;
A5: now
let s be SortSymbol of S(), v be Element of V().s;
P[v-term A()] by A2;
hence P[root-tree [v,s]];
end;
A6: 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] by A3;
for t being c-Term of A(),V() holds P[t] from CTermInd(A4,A5,A6);
hence thesis;
end;
begin :: Sort of a term
theorem Th11:
for t being Term of S,V ex s being SortSymbol of S st t in FreeSort (V, s)
proof
let t be Term of S,V;
set X = V;
set G = DTConMSA X;
reconsider e = {} as Node of t by TREES_1:22;
per cases;
suppose
t.{} is Terminal of G;
then reconsider ts = t.{} as Terminal of G;
consider s being SortSymbol of S, x being set such that
A1: x in X.s and
A2: ts = [x,s] by MSAFREE:7;
take s;
t = root-tree [x,s] by A2,DTCONSTR:9;
then t in {a where a is Element of TS G: (ex x be set st x in X.s & a =
root-tree [x,s]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} &
the_result_sort_of o = s} by A1;
hence thesis by MSAFREE:def 10;
end;
suppose
t.{} is not Terminal of G;
then reconsider nt = t.e as NonTerminal of G 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;
x2 = the carrier of S by TARSKI:def 1;
then t in {a where a is Element of TS G: (ex x be set st x in X.s & a =
root-tree [x,s]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} &
the_result_sort_of o = s} by A3;
hence thesis by MSAFREE:def 10;
end;
end;
theorem
for s being SortSymbol of S holds FreeSort (V, s) c= S-Terms V;
theorem
S-Terms V = Union FreeSort V
proof
set T = S-Terms V, X = V;
A1: dom FreeSort X = the carrier of S by PARTFUN1:def 2;
hereby
let x be object;
assume x in T;
then reconsider t = x as Term of S,V;
consider s being SortSymbol of S such that
A2: t in FreeSort (X, s) by Th11;
FreeSort (X,s) = (FreeSort X).s by MSAFREE:def 11;
hence x in Union FreeSort X by A1,A2,CARD_5:2;
end;
let x be object;
assume x in Union FreeSort X;
then consider y being object such that
A3: y in dom FreeSort X and
A4: x in (FreeSort X).y by CARD_5:2;
reconsider y as SortSymbol of S by A3,PARTFUN1:def 2;
x in FreeSort(X,y) by A4,MSAFREE:def 11;
hence thesis;
end;
Lm7: for x being set holds not x in x;
definition
let S, V, t;
func the_sort_of t -> SortSymbol of S means
:Def5:
t in FreeSort (V, it);
existence by Th11;
uniqueness
proof
set X = V;
let s1,s2 be SortSymbol of S such that
A1: t in FreeSort (X, s1) and
A2: t in FreeSort (X, s2);
FreeSort (X, s1) = {a where a is Element of TS(DTConMSA(X)): (ex x be
set st x in X.s1 & a = root-tree [x,s1]) or ex o be 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(X)) such that
A3: t = a1 and
A4: (ex x be set st x in X.s1 & a1 = root-tree [x,s1]) or ex o be
OperSymbol of S st [o,the carrier of S] = a1.{} & the_result_sort_of o = s1 by
A1;
FreeSort (X, s2) = {a where a is Element of TS(DTConMSA(X)): (ex x be
set st x in X.s2 & a = root-tree [x,s2]) or ex o be 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(X)) such that
A5: t = a2 and
A6: (ex x be set st x in X.s2 & a2 = root-tree [x,s2]) or ex o be
OperSymbol of S st [o,the carrier of S] = a2.{} & the_result_sort_of o = s2 by
A2;
per cases by A4;
suppose
ex x be set st x in X.s1 & a1 = root-tree [x,s1];
then consider x1 being set such that
x1 in X.s1 and
A7: a1 = root-tree [x1,s1];
now
let o be OperSymbol of S;
assume [o,the carrier of S] = [x1,s1];
then the carrier of S = s1 by XTUPLE_0:1;
hence contradiction by Lm7;
end;
then consider x2 being set such that
x2 in X.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 thesis by XTUPLE_0:1;
end;
suppose
ex o be OperSymbol of S st [o,the carrier of S] = a1.{} &
the_result_sort_of o = s1;
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
given x2 being set such that
x2 in X.s2 and
A11: a2 = root-tree [x2,s2];
[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;
end;
hence thesis by A3,A5,A6,A9,A10,XTUPLE_0:1;
end;
end;
end;
theorem Th14:
for s being SortSymbol of S, v be Element of V.s st t =
root-tree [v,s] holds the_sort_of t = s
proof
let s be SortSymbol of S, x be Element of V.s;
set X = V, G = DTConMSA X;
set tst = the_sort_of t;
A1: FreeSort (X, tst) = {a where a is Element of TS G: (ex x be set st x in
X.tst & a = root-tree [x,tst]) or ex o be OperSymbol of S st [o,the carrier of
S] = a.{} & the_result_sort_of o = tst} by MSAFREE:def 10;
t in FreeSort (V, the_sort_of t) by Def5;
then consider a being Element of TS G such that
A2: t = a and
A3: (ex x be set st x in X.tst & a = root-tree [x,tst]) or ex o be
OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o = tst by
A1;
A4: [x,s] in Terminals G by Lm3;
assume
A5: t = root-tree [x,s];
then t.{} = [x,s] by TREES_4:3;
then t.{} is not NonTerminal of G 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 X.tst and
A7: a = root-tree [y,tst] by A2,A3,A6,ZFMISC_1:87;
[y,tst] = [x,s] by A2,A5,A7,TREES_4:4;
hence thesis by XTUPLE_0:1;
end;
theorem Th15:
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
proof
let t be c-Term of A,V;
let s be SortSymbol of S, x be set;
assume x in (the Sorts of A).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 thesis by Th14;
end;
theorem
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
proof
let t be c-Term of A,V;
let s be SortSymbol of S, x be Element of V.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 thesis by Th14;
end;
theorem Th17:
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 o be OperSymbol of S;
set X = V, G = DTConMSA X;
set tst = the_sort_of t;
A1: FreeSort (X, tst) = {a where a is Element of TS G: (ex x be set st x in
X.tst & a = root-tree [x,tst]) or ex o be OperSymbol of S st [o,the carrier of
S] = a.{} & the_result_sort_of o = tst} by MSAFREE:def 10;
t in FreeSort (V, the_sort_of t) by Def5;
then consider a being Element of TS G such that
A2: t = a and
A3: (ex x be set st x in X.tst & a = root-tree [x,tst]) or ex o be
OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o = tst by
A1;
assume
A4: t.{} = [o,the carrier of S];
per cases by A3;
suppose
ex x be set st x in X.tst & a = root-tree [x,tst];
then consider x being set such that
x in X.tst and
A5: a = root-tree [x,tst];
[o,the carrier of S] = [x,tst] by A2,A4,A5,TREES_4:3;
then the carrier of S = tst by XTUPLE_0:1;
hence thesis by Lm7;
end;
suppose
ex o be OperSymbol of S st [o,the carrier of S] = a.{} &
the_result_sort_of o = tst;
hence thesis by A2,A4,XTUPLE_0:1;
end;
end;
theorem
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 by
Th15;
theorem Th19:
for s being SortSymbol of S, v being Element of V.s holds
the_sort_of (v-term A) = s
proof
let s be SortSymbol of S, v be Element of V.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 thesis by Th14;
end;
theorem Th20:
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
proof
let o be OperSymbol of S, p be ArgumentSeq of Sym(o,V);
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 thesis by A1,Th17;
end;
begin :: Argument Sequence
theorem Th21:
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
proof
let o be OperSymbol of S, a be FinSequence of S-Terms V;
a is SubtreeSeq of Sym(o, V) iff Sym(o, V) ==> roots a by DTCONSTR:def 6;
hence thesis by Def2;
end;
Lm8: 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 ex t being Term of S,V st t = a.i & 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
proof
let o be OperSymbol of S, a be ArgumentSeq of Sym(o,V);
set X = V;
reconsider p = a as FinSequence of TS DTConMSA X by Def1;
Sym(o, X) ==> roots a by Th21;
then
A1: p in ((FreeSort X)# * (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;
let i be Nat;
reconsider t = (a qua FinSequence of S-Terms V qua non empty set)/.i as Term
of S,V;
assume
A3: i in dom a;
then
A4: i <= len a by FINSEQ_3:25;
take t;
1 <= i by A3,FINSEQ_3:25;
hence t = a.i by A4,FINSEQ_4:15;
then t in FreeSort(X, (the_arity_of o)/.i) by A1,A3,MSAFREE:9;
then the_sort_of t = (the_arity_of o)/.i by Def5;
hence thesis by A2,A3,PARTFUN1:def 6;
end;
theorem Th22:
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
proof
let o be OperSymbol of S, a be ArgumentSeq of Sym(o,V);
thus len a = len the_arity_of o & dom a = dom the_arity_of o by Lm8;
let i be Nat;
assume i in dom a;
then
ex t being Term of S,V st t = a.i & 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 by Lm8;
hence thesis;
end;
theorem
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
proof
let o be OperSymbol of S, a be ArgumentSeq of Sym(o,V);
let i be Nat;
assume i in dom a;
then
ex t being Term of S,V st t = a.i & 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 by Lm8;
hence thesis;
end;
theorem Th24:
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)
proof
set X = V;
let o be OperSymbol of S, a be FinSequence such 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 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;
rng a c= TS DTConMSA X
proof
let x be object;
assume x in rng a;
then consider i being object such that
A3: i in dom a and
A4: x = a.i by FUNCT_1:def 3;
reconsider 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 thesis by A4;
end;
then reconsider p = a as FinSequence of TS DTConMSA X by FINSEQ_1:def 4;
A5: dom a = dom the_arity_of o by A1,FINSEQ_3:29;
now
let n be Nat;
assume
A6: n in dom p;
thus p.n in FreeSort(X,(the_arity_of o)/.n)
proof
per cases by A2,A6;
suppose
ex t being Term of S,V st t = a.n & the_sort_of t = (
the_arity_of o).n;
then consider t be 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 thesis by A7,Def5;
end;
suppose
ex t being Term of S,V st t = a.n & the_sort_of t = (
the_arity_of o)/.n;
hence thesis by Def5;
end;
end;
end;
then p in ((FreeSort X)# * (the Arity of S)).o by A5,MSAFREE:9;
then
A9: Sym(o, X) ==> roots p by MSAFREE:10;
S-Terms V = TS DTConMSA X;
hence thesis by A9,Th21;
end;
theorem
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)
proof
let o be OperSymbol of S, a be FinSequence of S-Terms V such 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 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;
A3: now
let i be Nat;
assume i in dom a;
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;
end;
now
per cases by A2;
case
A5: 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;
let i be Nat;
assume
A6: i in dom a;
then reconsider t = a.i as Term of S,V by A3;
take t;
thus t = a.i & the_sort_of t = (the_arity_of o).i by A5,A6;
end;
case
A7: 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;
let i be Nat;
assume
A8: i in dom a;
then reconsider t = a.i as Term of S,V by A3;
take t;
thus t = a.i & the_sort_of t = (the_arity_of o)/.i by A7,A8;
end;
end;
hence thesis by A1,Th24;
end;
theorem Th26:
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
proof
let S be non void non empty ManySortedSign;
let V1,V2 be non-empty ManySortedSet of the carrier of S such that
A1: for s being object st s in the carrier of S holds V1.s c= V2.s;
defpred P[set] means $1 is Term of S,V2;
A2: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,V1) st for t
being Term of S,V1 st t in rng p holds P[t] holds P[[o,the carrier of S]-tree p
]
proof
let o be OperSymbol of S, p be ArgumentSeq of Sym(o,V1);
assume
A3: for t being Term of S,V1 st t in rng p holds t is Term of S,V2;
rng p c= S-Terms V2
proof
let x be object;
assume
A4: x in rng p;
rng p c= S-Terms V1 by FINSEQ_1:def 4;
then reconsider x as Term of S,V1 by A4;
x is Term of S,V2 by A3,A4;
hence thesis;
end;
then reconsider q = p as FinSequence of S-Terms V2 by FINSEQ_1:def 4;
A5: now
let i be Nat;
assume
A6: i in dom q;
then consider t being Term of S,V1 such that
A7: t = q.i and
t = (p qua FinSequence of S-Terms V1 qua non empty set)/.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;
thus T = q.i by A7;
thus the_sort_of T = (the_arity_of o).i
proof
per cases by Th2;
suppose
ex s being SortSymbol of S, v being Element of V1.s st t.{} = [v,s];
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;
hence the_sort_of T = s by A10,Th14
.= (the_arity_of o).i by A8,A10,Th14;
end;
suppose
t.{} in [:the carrier' of S,{the carrier of S}:];
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;
end;
end;
end;
len p = len the_arity_of o by Lm8;
then q is ArgumentSeq of Sym(o,V2) by A5,Th24;
hence thesis by Th1;
end;
A13: for s being SortSymbol of S, v being Element of V1.s holds P[root-tree [
v,s]]
proof
let s be SortSymbol of S, v be Element of V1.s;
V1.s c= V2.s by A1;
then v in V2.s;
hence thesis by Th4;
end;
for t being Term of S,V1 holds P[t] from TermInd(A13,A2);
hence thesis;
end;
theorem
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 by Th26,PBOOLE:14;
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
it.{} in [:the carrier' of S, {the carrier of S}:];
existence
proof
set s = the OperSymbol of S;
reconsider nt = Sym(s, V) as NonTerminal of DTConMSA V;
set p = the SubtreeSeq of nt;
reconsider t = nt-tree p as Term of S,V;
take t;
nt = [s,the carrier of S] by MSAFREE:def 9;
then
A1: [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 thesis by A1,ZFMISC_1:87;
end;
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
ex t being CompoundTerm of S,V st t in it;
existence
proof
set t = the CompoundTerm of S,V;
reconsider X = {t} as non empty Subset of S-Terms V by ZFMISC_1:31;
take X, t;
thus thesis by TARSKI:def 1;
end;
end;
theorem
t is not root implies t is CompoundTerm of S,V
proof
assume
A1: t is not root;
per cases by Th2;
suppose
ex s being SortSymbol of S, v being Element of V.s st t.{} = [v,s];
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 thesis by A1;
end;
suppose
t.{} in [:the carrier' of S,{the carrier of S}:];
hence t.{} in [:the carrier' of S,{the carrier of S}:];
end;
end;
Lm9: for n being Element of NAT, p being FinSequence holds n < len p implies n
+1 in dom p & p.(n+1) in rng p
proof
let n be Element of NAT, p be FinSequence;
n >= 0 by NAT_1:2;
then
A1: n+1 >= 0+1 by XREAL_1:7;
assume n < len p;
then n+1 <= len p by NAT_1:13;
then n+1 in dom p by A1,FINSEQ_3:25;
hence thesis by FUNCT_1:def 3;
end;
theorem Th29:
for p being Node of t holds t|p is Term of S,V
proof
defpred P[set] means for q being Node of t st q = $1 holds t|q is Term of S,
V;
A1: for p be Node of t,n be Nat st P[p] & p^<*n*> in dom t holds
P[p^<*n*>]
proof
let p be Node of t, n be Nat;
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;
reconsider u = t|p as Term of S,V by A2;
A4: dom u = (dom t)|p by TREES_2:def 10;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
A5: <*nn*> in (dom t)|p by A3,TREES_1:def 6;
A6: now
given s being SortSymbol of S, x being Element of V.s such that
A7: u.{} = [x,s];
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;
end;
(ex s being SortSymbol of S, 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 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
.= i by A11,FINSEQ_1:41;
then
A13: u|<*nn*> = a.(nn+1) by A9,A10,TREES_4:def 4;
let q be Node of t;
nn+1 in dom a by A10,A12,Lm9;
then ex t being Term of S,V
st t = u|<*nn*> & t = (a qua FinSequence of S
-Terms V qua non empty set)/.(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 thesis by TREES_9:3;
end;
A14: P[{}] by TREES_9:1;
for p being Node of t holds P[p] from TREES_2:sch 1(A14,A1);
hence thesis;
end;
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; :: redefines | (TREES_2, definition)
coherence by Th29;
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
:
Def8: it misses the Sorts of A;
existence
proof
deffunc F(object)= {(the Sorts of A).$1};
consider V being ManySortedSet of the carrier of S such that
A1: for s be object st s in the carrier of S holds V.s = F(s) from PBOOLE
:sch 4;
V is non-empty
proof
let s be object;
assume s in the carrier of S;
then V.s = {(the Sorts of A).s} by A1;
hence thesis;
end;
then reconsider V as non-empty ManySortedSet of the carrier of S;
take V;
let s be object;
assume s in the carrier of S;
then
A2: V.s = {(the Sorts of A).s} by A1;
now
let x be object;
assume x in V.s;
then A: x = (the Sorts of A).s by A2,TARSKI:def 1;
then reconsider xx = x as set;
not xx in xx;
hence not x in (the Sorts of A).s by A;
end;
hence thesis by XBOOLE_0:3;
end;
end;
theorem Th30:
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
proof
let V be Variables of A;
let s be SortSymbol of S, x be set such that
A1: x in (the Sorts of A).s;
let v be Element of V.s;
V misses the Sorts of A by Def8;
then V.s misses (the Sorts of A).s;
hence thesis by A1,XBOOLE_0:3;
end;
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
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 Th31:
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
proof
let s be SortSymbol of S, x be Element of (the Sorts of A).s such that
A1: t = root-tree [x,s];
A2: t.{} = [x,s] by A1,TREES_4:3;
set vt = root-tree x;
A3: dom vt = elementary_tree 0 by TREES_4:3;
hence dom vt = dom t by A1,TREES_4:3;
let p be Node of vt;
reconsider e = p as empty FinSequence of NAT by A3,TARSKI:def 1,TREES_1:29;
hereby
let s1 be SortSymbol of S, v be Element of V.s1;
assume t.p = [v,s1];
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 vt.p = f.s1.v by A5,Th30;
end;
A6: vt.{} = x by TREES_4:3;
hereby
let s1 be SortSymbol of S, x1 be Element of (the Sorts of A).s1;
assume t.p = [x1,s1];
then [x1,s1] = t.e;
hence vt.p = x1 by A2,A6,XTUPLE_0:1;
end;
let o be OperSymbol of S;
assume t.p = [o,the carrier of S];
then the carrier of S = (t.e)`2
.= s by A2;
hence vt.p = Den(o, A).succ(vt,p) by Lm7;
end;
theorem Th32:
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
proof
let s be SortSymbol of S, x be Element of V.s such that
A1: t = root-tree [x,s];
set vt = root-tree (f.s.x);
A2: dom vt = elementary_tree 0 by TREES_4:3;
hence dom vt = dom t by A1,TREES_4:3;
let p be Node of vt;
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
let s1 be SortSymbol of S, x1 be Element of V.s1;
A4: e = p;
assume t.p = [x1,s1];
then
A5: [x1,s1] = t.e;
then
A6: s = s1 by A3,XTUPLE_0:1;
x = x1 by A3,A5,XTUPLE_0:1;
hence vt.p = f.s1.x1 by A6,A4,TREES_4:3;
end;
hereby
let s1 be SortSymbol of S, v be Element of (the Sorts of A).s1;
assume t.p = [v,s1];
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 vt.p = v by A8,Th30;
end;
let o be OperSymbol of S;
assume t.p = [o,the carrier of S];
then the carrier of S = (t.e)`2
.= s by A3;
hence vt.p = Den(o, A).succ(vt,p) by Lm7;
end;
theorem Th33:
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
proof
let o be OperSymbol of S, p be ArgumentSeq of o,A,V;
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 such that
A5: len q = len p and
A6: 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;
A7: dom q = Seg len q by FINSEQ_1:def 3;
now
let x be object;
A8: rng p c= S-Terms ((the Sorts of A) (\/) V) by FINSEQ_1:def 4;
assume
A9: x in dom doms q;
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;
end;
then reconsider r = doms q as FinTree-yielding FinSequence by TREES_3:23;
A12: now
let i be Nat;
A13: rng p c= S-Terms ((the Sorts of A) (\/) V) by FINSEQ_1:def 4;
assume
A14: i in dom p;
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
.= (doms p).i by A14,FUNCT_6:22;
end;
set vt = (Den(o,A).roots q)-tree q;
A17: len doms q = len q by TREES_3:38;
A18: dom vt = tree r by TREES_4:10;
then reconsider vt as finite DecoratedTree by FINSET_1:10;
take vt;
thus vt = (Den(o,A).roots q)-tree q;
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;
let n be Node of vt;
A19: ([o,the carrier of S]-tree p).{} = [o,the carrier of S] by TREES_4:def 4;
hereby
let s be SortSymbol of S, v be Element of V.s;
assume
A20: (Sym(o,(the Sorts of A) (\/) V)-tree p).n = [v,s];
now
assume n = {};
then s = the carrier of S by A1,A19,A20,XTUPLE_0:1;
hence contradiction by Lm7;
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 as Node of e by A5,A4,A7,A22,A24,FUNCT_6:22;
dom e = dom t by A25;
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;
end;
hereby
let s be SortSymbol of S, x be Element of (the Sorts of A).s;
assume
A27: (Sym(o,(the Sorts of A) (\/) V)-tree p).n = [x,s];
now
assume n = {};
then s = the carrier of S by A1,A19,A27,XTUPLE_0:1;
hence contradiction by Lm7;
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 as Node of e by A5,A4,A7,A29,A31,FUNCT_6:22;
dom e = dom t by A32;
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;
end;
let o1 be OperSymbol of S;
assume
A34: (Sym(o,(the Sorts of A) (\/) V)-tree p).n = [o1,the carrier of S];
per cases;
suppose
A35: 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 thesis by A35,A36,TREES_4:def 4;
end;
suppose
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 as Node of e by A5,A4,A7,A38,A40,FUNCT_6:22;
dom e = dom t by A41;
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
.= Den(o1, A).succ(vt,n) by A37,A42,TREES_9:31;
hence thesis by A5,A37,A39,A40,TREES_4:12;
end;
end;
theorem Th34:
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
proof
let t be c-Term of A,V, e be finite DecoratedTree such that
A1: dom e = dom t and
A2: for p being Node of e holds (for s being SortSymbol of S, v being
Element of V.s st t.p = [v,s] holds e.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 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);
let p be Node of t, n be Node of e;
set vt = e|n, tp = t|p;
A3: dom vt = (dom e)|n by TREES_2:def 10;
assume
A4: n = p;
hence dom vt = dom tp by A1,A3,TREES_2:def 10;
let q be Node of vt;
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
let s be SortSymbol of S, v be Element of V.s;
assume tp.q = [v,s];
then t.pq = [v,s] by A1,A4,A3,TREES_2:def 10;
then e.nq = f.s.v by A2,A4;
hence vt.q = f.s.v by A3,TREES_2:def 10;
end;
hereby
let s be SortSymbol of S, x be Element of (the Sorts of A).s;
assume tp.q = [x,s];
then t.pq = [x,s] by A1,A4,A3,TREES_2:def 10;
then e.nq = x by A2,A4;
hence vt.q = x by A3,TREES_2:def 10;
end;
let o be OperSymbol of S;
assume tp.q = [o,the carrier of S];
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 vt.q = Den(o, A).succ(e,n^q) by A3,TREES_2:def 10;
hence thesis by TREES_9:31;
end;
theorem Th35:
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
proof
let o be OperSymbol of S, p be ArgumentSeq of o,A,V;
let vt be finite DecoratedTree;
assume
A1: vt is_an_evaluation_of (Sym(o,(the Sorts of A) (\/) V)-tree p qua
c-Term of A,V), 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;
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;
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;
([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
.= 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;
let i be Nat, t be c-Term of A,V;
assume that
A8: i in dom p and
A9: t = p.i;
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;
len doms p = len p by TREES_3:38;
hence e = q.i by A2,A7,A4,A10,A11,TREES_4:def 4;
reconsider r1 = r as Node of [o,the carrier of S]-tree p by A5,A1;
t = ([o,the carrier of S]-tree p)|r1 by A9,A10,A11,TREES_4:def 4;
hence thesis by A5,A1,Th34;
end;
theorem Th36:
ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f
proof
defpred P[set] means ex t being c-Term of A,V, vt being finite DecoratedTree
st t = $1 & vt is_an_evaluation_of t,f;
A1: 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]
proof
let o be OperSymbol of S, p be ArgumentSeq of o,A,V such that
A2: for t being c-Term of A,V st t in rng p ex u being c-Term of A,V,
vt being finite DecoratedTree st u = t & vt is_an_evaluation_of u,f;
defpred Q[object,object] means
ex t being c-Term of A,V, vt being finite
DecoratedTree st $2 = vt & t = p.$1 & vt is_an_evaluation_of t,f;
A3: for e be object st e in dom p ex u be object st Q[e,u]
proof
let x be object;
assume x in dom p;
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, vt being finite DecoratedTree st u = t &
vt is_an_evaluation_of u,f by A2,A4;
hence thesis;
end;
consider q being Function such that
A5: dom q = dom p & for x being object st x in dom p holds Q[x,q.x] from
CLASSES1:sch 1(A3);
dom p = Seg len p by FINSEQ_1:def 3;
then reconsider q as FinSequence by A5,FINSEQ_1:def 2;
A6: len p = len q by A5,FINSEQ_3:29;
now
let x be object;
assume x in dom q;
then
ex t being c-Term of A,V, 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;
end;
then reconsider q as DTree-yielding FinSequence by TREES_3:24;
now
let i be Nat, t be c-Term of A,V;
assume i in dom p;
then
ex t being c-Term of A,V, 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;
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 qua c-Term of A,V),
f by A6,Th33;
hence thesis;
end;
A7: for s being SortSymbol of S, v being Element of V.s holds P[root-tree [v
,s]]
proof
let s be SortSymbol of S, x be Element of V.s;
reconsider t = root-tree [x,s] as c-Term of A,V by Th8;
take t, root-tree (f.s.x);
thus t = root-tree [x,s];
thus thesis by Th32;
end;
A8: for s being SortSymbol of S, x being Element of (the Sorts of A).s holds
P[root-tree [x,s]]
proof
let s be SortSymbol of S, x be Element of (the Sorts of A).s;
reconsider t = root-tree [x,s] as c-Term of A,V by Th6;
take t, root-tree x;
thus t = root-tree [x,s];
thus thesis by Th31;
end;
for t being c-Term of A,V holds P[t] from CTermInd(A8,A7,A1);
then ex u being c-Term of A,V, vt being finite DecoratedTree st u = t & vt
is_an_evaluation_of u,f;
hence thesis;
end;
theorem Th37:
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
defpred P[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
let s be SortSymbol of S, v be Element of V.s;
thus P[v-term A]
proof
let e1,e2 be finite DecoratedTree;
set t = v-term A;
assume that
A2: e1 is_an_evaluation_of t,f and
A3: e2 is_an_evaluation_of t,f;
A4: dom e1 = dom t by A2;
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;
then
A7: e1 = root-tree (f.s.v) by A4,TREES_4:3,5;
A8: dom e2 = dom t by A3;
e2.{} = f.s.v by A3,A4,A6,A5;
hence thesis by A8,A7,TREES_4:3,5;
end;
end;
A9: now
let o be OperSymbol of S, p be ArgumentSeq of o,A,V;
assume
A10: for t being c-Term of A,V st t in rng p holds P[t];
thus P[Sym(o,(the Sorts of A) (\/) V)-tree p]
proof
set t = Sym(o,(the Sorts of A) (\/) V)-tree p;
let e1, e2 be finite DecoratedTree;
assume that
A11: e1 is_an_evaluation_of t qua c-Term of A,V,f and
A12: e2 is_an_evaluation_of t qua c-Term of A,V,f;
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, t being c-Term of A,V st i in dom p & t = p.i
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, t being c-Term of A,V st i in dom p & t = p.i
ex vt being finite DecoratedTree st vt = q2.i & vt is_an_evaluation_of t,f by
A12,Th35;
A19: now
let i be Element of NAT;
assume
A20: i < len p;
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;
end;
A22: now
let i be Nat;
assume i in dom q1;
then ex k being Element of NAT st i = k+1 & k < len q1 by Lm1;
hence q1.i = q2.i by A13,A19;
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 thesis by A14,A17;
end;
end;
A24: now
let s be SortSymbol of S, x be Element of (the Sorts of A).s;
thus P[x-term (A, V)]
proof
let e1,e2 be finite DecoratedTree;
set t = x-term (A, V);
assume that
A25: e1 is_an_evaluation_of t,f and
A26: e2 is_an_evaluation_of t,f;
A27: dom e1 = dom t by A25;
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;
then
A30: e1 = root-tree x by A27,TREES_4:3,5;
A31: dom e2 = dom t by A26;
e2.{} = x by A26,A27,A29,A28;
hence thesis by A31,A30,TREES_4:3,5;
end;
end;
for t being c-Term of A,V holds P[t] from TermInd2(A24,A1,A9);
hence thesis;
end;
theorem Th38:
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
defpred P[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
let s be SortSymbol of S, v be Element of V.s;
thus P[v-term A]
proof
let vt be finite DecoratedTree;
set t = v-term A;
assume
A2: vt is_an_evaluation_of t,f;
root-tree (f.s.v) is_an_evaluation_of t,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 t by Th19;
hence thesis by A3;
end;
end;
A4: now
let o be OperSymbol of S, p be ArgumentSeq of o,A,V;
assume
A5: for t being c-Term of A,V st t in rng p holds P[t];
thus P[Sym(o,(the Sorts of A) (\/) V)-tree p]
proof
let vt be finite DecoratedTree;
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 t qua c-Term of A,V,f;
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, 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 by
Th35;
A10: vt.{} = Den(o,A).roots q by A8,TREES_4:def 4;
now
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;
let x be object;
assume
A15: x in dom ((the Sorts of A)*the_arity_of o);
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 qua FinSequence
of S-Terms ((the Sorts of A) (\/) V) qua non empty set)/.(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;
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 (t qua c-Term of A,V) by Th20;
hence thesis by A10,A23,FUNCT_2:5;
end;
end;
A24: now
let s be SortSymbol of S, x be Element of (the Sorts of A).s;
thus P[x-term (A, V)]
proof
let vt be finite DecoratedTree;
set t = x-term (A, V);
assume
A25: vt is_an_evaluation_of t,f;
root-tree x is_an_evaluation_of t,f by Th31;
then vt = root-tree x by A25,Th37;
then
A26: vt.{} = x by TREES_4:3;
s = the_sort_of t by Th15;
hence thesis by A26;
end;
end;
for t being c-Term of A,V holds P[t] from TermInd2(A24,A1,A4);
hence thesis;
end;
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
: Def10:
ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f & it = vt.{};
existence
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, vt;
thus thesis by A1;
end;
uniqueness by Th37;
end;
reserve t for c-Term of A,V;
theorem Th39:
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f
holds t@f = vt.{}
proof
A1: ex e being finite DecoratedTree st e is_an_evaluation_of t,f & t@f = e
.{} by Def10;
let vt be finite DecoratedTree;
assume vt is_an_evaluation_of t,f;
hence thesis by A1,Th37;
end;
theorem
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
proof
let vt be finite DecoratedTree such that
A1: vt is_an_evaluation_of t,f;
let p be Node of t;
reconsider n = p as Node of vt by A1;
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 thesis by A2,A3,TREES_2:def 10;
end;
theorem
for s being SortSymbol of S, x being Element of (the Sorts of A).s
holds (x-term(A,V))@f = x
proof
let s be SortSymbol of S, x be Element of (the Sorts of A).s;
x = (root-tree x).{} by TREES_4:3;
hence thesis by Th31,Th39;
end;
theorem
for s being SortSymbol of S, v being Element of V.s holds (v-term A)@f
= f.s.v
proof
let s be SortSymbol of S, v be Element of V.s;
f.s.v = (root-tree f.s.v).{} by TREES_4:3;
hence thesis by Th32,Th39;
end;
theorem
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
proof
let o be OperSymbol of S, p be ArgumentSeq of o,A,V;
let q be FinSequence;
assume that
A1: len q = len p and
A2: 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;
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, t being c-Term of A,V st i in dom p & t = p.i ex vt
being finite DecoratedTree st vt = r.i & vt is_an_evaluation_of t,f by A3,Th35;
now
thus
A7: dom p = dom p & dom q = dom p & dom r = dom p by A1,A4,FINSEQ_3:29;
let i be Element of NAT;
assume
A8: i in dom r;
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;
thus T = r.i by A9;
thus q.i = t@f by A2,A7,A8
.= T.{} by A10,Th39;
end;
then q = roots r by TREES_3:def 18;
hence
(Sym(o,(the Sorts of A) (\/) V)-tree p qua c-Term of A,V)@f = (((Den(o,A)
).q)-tree r).{} by A3,A5,Th39
.= Den(o,A).q by TREES_4:def 4;
end;