:: Free Term Algebras
:: by Grzegorz Bancerek
::
:: Received May 15, 2012
:: Copyright (c) 2012-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 TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
FINSEQ_1, FUNCOP_1, ZF_LANG, ZF_MODEL, REALSET1, PBOOLE, TREES_1,
ORDINAL4, FUNCT_4, FINSET_1, PROB_2, GROUP_6, CARD_3, TREES_2, CARD_1,
ARYTM_3, XXREAL_0, MCART_1, MEMBER_1, PRELAMB, TREES_4, DTCONSTR,
TDGROUP, TREES_3, FUNCT_6, TREES_A, TREES_9, MSUALG_6, MATROID0,
ZF_LANG1, MARGREL1, PZFMISC1, NUMBERS, NAT_1, STRUCT_0, UNIALG_2,
MSUALG_1, MSUALG_2, MSUALG_3, MSAFREE, ALGSPEC1, MSATERM, EQUATION,
AOFA_000, AOFA_I00, MSAFREE4, FOMODEL2, SETLIM_2, PENCIL_1, MSUALG_4,
REWRITE1, CIRCUIT2, MOD_4, RLTOPSP1, RFINSEQ, ARYTM_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, ORDINAL1, FINSET_1, CARD_1, XXREAL_0,
XCMPLX_0, AOFA_I00, FINSEQ_1, FINSEQ_2, LANG1, FUNCT_6, NUMBERS,
FUNCOP_1, TREES_1, CARD_3, PBOOLE, PROB_2, FUNCT_4, TREES_2, TREES_3,
TREES_4, TREES_9, RFINSEQ, REWRITE1, PENCIL_1, FUNCT_7, DTCONSTR,
PZFMISC1, COMPUT_1, STRUCT_0, MSUALG_1, MSUALG_2, MSUALG_3, MSUALG_4,
MSAFREE, MSAFREE1, MSATERM, MSUALG_6, ALGSPEC1, CATALG_1, MSAFREE3,
EQUATION, AOFA_000;
constructors RELSET_1, DOMAIN_1, PZFMISC1, FUNCT_4, TREES_9, COMPUT_1,
MSUALG_3, MSAFREE1, MSUALG_6, EQUATION, CATALG_1, ALGSPEC1, MSAFREE3,
REAL_1, PRALG_2, PENCIL_1, REWRITE1, RFINSEQ;
registrations XBOOLE_0, RELSET_1, PBOOLE, MSUALG_1, INSTALG1, MSAFREE1,
FUNCT_1, FUNCOP_1, FINSET_1, FINSEQ_1, STRUCT_0, MSAFREE3, EQUATION,
COMPUT_1, CARD_3, MSAFREE, NAT_1, ORDINAL1, CARD_1, RELAT_1, SUBSET_1,
CATALG_1, TREES_2, MSUALG_2, MSATERM, TREES_1, TREES_3, MSUALG_3,
ALTCAT_2, MSSUBFAM, TREES_9, MSUALG_4, MSUALG_6, REWRITE1, MSUALG_9,
XREAL_0, XTUPLE_0;
requirements BOOLE, SUBSET, ARITHM, NUMERALS;
definitions TARSKI, XBOOLE_0, FUNCT_1, PARTFUN1, FUNCOP_1, FINSEQ_1, PROB_2,
COMPUT_1, MSUALG_1, MSUALG_2, MSUALG_3, CATALG_1, MSUALG_6, MSAFREE,
MSAFREE1, EQUATION, PBOOLE;
equalities TARSKI, FINSEQ_1, TREES_9, MSUALG_1, MSAFREE, EQUATION;
expansions TARSKI, XBOOLE_0, FUNCT_1, FINSET_1, FINSEQ_1, REWRITE1, MSUALG_2,
MSUALG_3, MSUALG_6, MSAFREE, EQUATION, PBOOLE;
theorems XBOOLE_0, XBOOLE_1, ZFMISC_1, PARTFUN1, FUNCT_1, FUNCT_2, PBOOLE,
CARD_5, PROB_2, MSUALG_2, MSUALG_3, MSAFREE3, SUBSET_1, RELAT_1,
FUNCOP_1, FUNCT_6, EQUATION, MSAFREE, MSAFREE2, MSATERM, DTCONSTR,
INSTALG1, FINSEQ_1, FINSEQ_2, CARD_3, ALGSPEC1, PZFMISC1, EXTENS_1,
TREES_4, PRALG_2, ORDINAL1, TREES_9, TREES_1, TREES_2, FINSEQ_3, NAT_1,
TREES_3, TARSKI, FUNCT_4, AOFA_I00, MSSUBFAM, COMPUT_1, FINSET_1,
XXREAL_0, FOMODEL0, MSUALG_6, MSUALG_9, XTUPLE_0, PENCIL_1, MSUALG_4,
REWRITE1, FINSEQ_5, RELSET_1, FUNCT_7, RFINSEQ, MSUALG_1, XREAL_1;
schemes TARSKI, NAT_1, FUNCT_1, FINSEQ_1, PBOOLE, CLASSES1, MSATERM, MSSUBFAM,
CIRCTRM1, YELLOW18;
begin :: Preliminaries
reserve S for non empty non void ManySortedSign;
reserve X for non-empty ManySortedSet of S;
theorem Th1:
for I being set, f1,f2 being ManySortedSet of I st f1 c= f2
holds Union f1 c= Union f2
proof
let I be set;
let f1,f2 be ManySortedSet of I;
assume A1: f1 c= f2;
let x be object;
assume x in Union f1; then
consider y being object such that
A2: y in dom f1 & x in f1.y by CARD_5:2;
A3: dom f1 = I & dom f2 = I by PARTFUN1:def 2;
f1.y c= f2.y by A1,A2;
hence x in Union f2 by A2,A3,CARD_5:2;
end;
reserve x,y,z for set, i,j for Nat;
deffunc cc(Function,set) = $1.$2;
definition
let I be set;
let X be non-empty ManySortedSet of I;
let A be Component of X;
redefine mode Element of A -> Element of Union X; :: redefines Element (SUBSET_1, definition)
coherence
proof let a be Element of A;
per cases;
suppose I = {}; then
A1: rng X = {} & X = {} & Union({}-->I) = {} by FUNCT_6:26;
thus thesis by A1,SUBSET_1:def 1;
end;
suppose I <> {}; then
consider x being object such that
A2: x in dom X & A = X.x by FUNCT_1:def 3;
thus thesis by A2,CARD_5:2;
end;
end;
end;
definition
let I be set;
let X be ManySortedSet of I;
let i be Element of I;
redefine func X.i -> Component of X; :: redefines . (FUNCT_1, definition)
coherence
proof
A1: dom X = I by PARTFUN1:def 2;
per cases;
suppose I = {};
hence thesis by SUBSET_1:def 1;
end;
suppose I <> {};
hence thesis by A1,FUNCT_1:def 3;
end;
end;
end;
Lm1:
now
let I be set;
let X,Y be ManySortedSet of I;
let f be ManySortedFunction of X,Y;
let x be object;
per cases;
suppose
x in I;
hence f.x is Function of X.x,Y.x by PBOOLE:def 15;
end;
suppose
A1: x nin I;
dom f = I & dom X = I & dom Y = I by PARTFUN1:def 2; then
f.x = {} & X.x = {} & Y.x = {} & dom {} = {} & rng {} = {}
by A1,FUNCT_1:def 2;
hence f.x is Function of X.x,Y.x by FUNCT_2:2;
end;
end;
definition
let I be set;
let X,Y be ManySortedSet of I;
let f be ManySortedFunction of X,Y;
let x be object;
redefine func f.x -> Function of X.x,Y.x; :: redefines . (FUNCT_1, definition)
coherence by Lm1;
end;
scheme Sch1{I()-> set, A()->non-empty ManySortedSet of I(),
F(object,object)->set}:
ex f being ManySortedFunction of I() st
for x st x in I() holds dom(f.x) = A().x &
for y being Element of A().x holds f.x .y = F(x,y)
proof
defpred P[object,object] means
ex f being Function st $2 = f & dom f = A().$1 &
for y being Element of A().$1 holds f.y = F($1,y);
A1: for x being object st x in I() ex y being object st P[x,y]
proof
let x be object; assume
A2: x in I();
then reconsider s = x as Element of I();
deffunc G(object) = F(x,$1);
consider f being Function such that
A3: dom f = A().x & for y being object st y in A().x holds f.y = G(y)
from FUNCT_1:sch 3;
take f,f;
thus thesis by A2,A3;
end;
consider g being Function such that
A4: dom g = I() &
for x being object st x in I() holds P[x,g.x] from CLASSES1:sch 1(A1);
g is Function-yielding
proof
let x be object; assume x in dom g;
then P[x,g.x] by A4;
hence thesis;
end;
then reconsider g as ManySortedFunction of I()
by A4,RELAT_1:def 18,PARTFUN1:def 2;
take g; let x; assume
x in I();
then P[x,g.x] & A().x <> {} by A4;
hence thesis;
end;
scheme Sch2{I()->non empty set, A,B()->non-empty ManySortedSet of I(),
F(object,object) -> set}:
ex f being ManySortedFunction of A(),B() st
for i being Element of I() for a being Element of A().i holds f.i.a = F(i,a)
provided
A1: for i being Element of I() for a being Element of A().i
holds F(i,a) in B().i
proof
defpred P[object,object,object] means $1 = F($3,$2);
A2: for i be object st i in I() for x be object st x in A().i
ex y be object st y in B().i & P[y,x,i] by A1;
consider F be ManySortedFunction of A(), B() such that
A3: for i be object st i in I() ex f be Function of A().i, B().i
st f = F.i & for x be object st x in A().i holds P[f.x,x,i]
from MSSUBFAM:sch 1(A2);
take F;
let i be Element of I();
let a be Element of A().i;
consider f being Function of A().i, B().i such that
A4: f = F.i & for x be object st x in A().i holds P[f.x,x,i] by A3;
thus F.i.a = F(i,a) by A4;
end;
definition
let X be non empty set;
let O be set;
let f be Function of O,X;
let g be ManySortedSet of X;
redefine func g*f -> ManySortedSet of O; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence;
end;
registration
let S, X;
let F be ManySortedSet of S -Terms X;
let o be OperSymbol of S;
let p be ArgumentSeq of Sym(o,X);
cluster F*p -> FinSequence-like;
coherence
proof
dom (F*p) = dom p by PARTFUN1:def 2;
hence ex n being Nat st dom(F*p) = Seg n by FINSEQ_1:def 2;
end;
end;
theorem Th2:
Subtrees root-tree x = {root-tree x}
proof
A1: dom root-tree x = {{}} by TREES_4:3,TREES_1:29;
thus Subtrees root-tree x c= {root-tree x}
proof
let y be object; assume y in Subtrees root-tree x; then
consider p being Element of dom root-tree x such that
A2: y = (root-tree x)|p;
p = {} by A1,TARSKI:def 1;
then y = root-tree x by A2,TREES_9:1;
hence thesis by TARSKI:def 1;
end;
reconsider p = {} as Element of dom root-tree x by A1,TARSKI:def 1;
let y be object; assume y in {root-tree x};
then y = root-tree x by TARSKI:def 1;
then y = (root-tree x)|p by TREES_9:1;
hence thesis;
end;
registration
let f be DTree-yielding Function;
cluster rng f -> constituted-DTrees;
coherence by TREES_3:def 11;
end;
theorem Th3:
for p being non empty DTree-yielding FinSequence holds
Subtrees(x-tree p) = {x-tree p} \/ Subtrees rng p
proof
let p be non empty DTree-yielding FinSequence;
thus Subtrees(x-tree p) c= {x-tree p} \/ Subtrees rng p
proof
let y be object; assume y in Subtrees(x-tree p);
then consider q being Element of dom(x-tree p) such that
A1: y = (x-tree p)|q;
A2: dom(x-tree p) = tree doms p by TREES_4:10;
per cases by A2,TREES_3:def 15;
suppose q = {};
then y = x-tree p by A1,TREES_9:1;
then y in {x-tree p} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose ex n being Nat,r being FinSequence st
n < len doms p & r in (doms p).(n+1) & q = <*n*>^r;
then consider n being Nat,r being FinSequence such that
A3: n < len doms p & r in (doms p).(n+1) & q = <*n*>^r;
A4: len doms p = len p by TREES_3:38;
n+1 >= 1 & n+1 <= len p by A3,A4,NAT_1:11,13;
then
A5: n+1 in dom p by FINSEQ_3:25;
then
A6: p.(n+1) in rng p by FUNCT_1:def 3;
then reconsider t = p.(n+1) as DecoratedTree;
reconsider r as Element of dom t by A3,A5,FUNCT_6:22;
reconsider n as Element of NAT by ORDINAL1:def 12;
p.(n+1) = (x-tree p)|<*n*> by A3,A4,TREES_4:def 4;
then y = t|r by A1,A3,TREES_9:3;
then y in Subtrees rng p by A6;
hence thesis by XBOOLE_0:def 3;
end;
end;
let z be object; assume z in {x-tree p} \/ Subtrees rng p;
then
A7: z in {x-tree p} or z in Subtrees rng p by XBOOLE_0:def 3;
reconsider q = {} as Element of dom (x-tree p) by TREES_1:22;
per cases by A7,TARSKI:def 1;
suppose z = x-tree p;
then z = (x-tree p)|q by TREES_9:1;
hence z in Subtrees (x-tree p);
end;
suppose
z in Subtrees rng p;
then consider t being (Element of rng p),
q being Element of dom t such that
A8: z = t|q;
consider y being object such that
A9: y in dom p & t = p.y by FUNCT_1:def 3;
reconsider y as Nat by A9;
consider n being Nat such that
A10: y = 1+n by A9,FINSEQ_3:25,NAT_1:10;
reconsider n as Element of NAT by ORDINAL1:def 12;
y <= len p by A9,FINSEQ_3:25;
then
A11: n < len p by A10,NAT_1:13;
then
A12: t = (x-tree p)|<*n*> by A9,A10,TREES_4:def 4;
A13: tree doms p = dom(x-tree p) by TREES_4:10;
dom t = (doms p).y & len doms p = len p by A9,FUNCT_6:22,TREES_3:38;
then
A14: <*n*>^q in dom(x-tree p) by A10,A11,A13,TREES_3:def 15;
then z = (x-tree p)|(<*n*>^q) by A8,A12,TREES_9:3;
hence thesis by A14;
end;
end;
theorem Th4:
Subtrees(x-tree{}) = {x-tree {}}
proof
dom(x-tree {}) = elementary_tree 0 by TREES_4:10,FUNCT_6:23,TREES_3:52;
then x-tree {} = root-tree ((x-tree {}).{}) by TREES_4:5
.= root-tree x by TREES_4:def 4;
hence thesis by Th2;
end;
theorem
x-tree {} = root-tree x
proof
dom(x-tree {}) = elementary_tree 0 by TREES_4:10,FUNCT_6:23,TREES_3:52;
hence x-tree {} = root-tree ((x-tree {}).{}) by TREES_4:5
.= root-tree x by TREES_4:def 4;
end;
registration
cluster finite-yielding DTree-yielding non empty for FinSequence;
existence
proof
set t = the finite DecoratedTree;
take <*t*>;
thus <*t*> is finite-yielding
proof
now
let x; assume x in rng <*t*>;
then x in {t} by FINSEQ_1:39;
hence x is finite;
end;
hence thesis;
end;
thus thesis;
end;
cluster finite-yielding Tree-yielding non empty for FinSequence;
existence
proof
set t = the finite Tree;
take <*t*>;
thus <*t*> is finite-yielding
proof
now
let x; assume x in rng <*t*>;
then x in {t} by FINSEQ_1:39;
hence x is finite;
end;
hence thesis;
end;
thus thesis;
end;
end;
registration
let f be finite-yielding Function-yielding Function;
cluster doms f -> finite-yielding;
coherence
proof
now
let y; assume y in rng doms f;
then consider x being object such that
A1: x in dom doms f & y = (doms f).x by FUNCT_1:def 3;
x in dom f by A1,FUNCT_6:def 2;
then
A2: x in dom f & f.x is Function & y = proj1(f.x) by A1,FUNCT_6:def 2;
thus y is finite by A2;
end;
hence thesis;
end;
end;
registration
let p be finite-yielding Tree-yielding FinSequence;
cluster tree p -> finite;
coherence
proof
set X = {{<*i*>^q where q is Element of NAT*: q in p.(i+1)}
where i is Nat: i < len p};
A1: tree p c= {{}}\/union X
proof
let x be object; assume
A2: x in tree p;
reconsider xx=x as set by TARSKI:1;
per cases by A2,TREES_3:def 15;
suppose x = {};
then x in {{}} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose ex n being Nat,q being FinSequence st
n < len p & q in p.(n+1) & x = <*n*>^q;
then consider n being Nat,q being FinSequence such that
A3: n < len p & q in p.(n+1) & x = <*n*>^q;
1 <= n+1 & n+1 <= len p by A3,NAT_1:11,13;
then n+1 in dom p by FINSEQ_3:25;
then p.(n+1) in rng p & rng p is constituted-Trees
by FUNCT_1:def 3,TREES_3:def 9;
then reconsider t = p.(n+1) as Tree;
q is Element of t by A3;
then q in NAT* by FINSEQ_1:def 11;
then
A4: x in {<*n*>^w where w is Element of NAT*: w in p.(n+1)} by A3;
{<*n*>^w where w is Element of NAT*: w in p.(n+1)} in X by A3;
then x in union X by A4,TARSKI:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
deffunc F(object) = {<*i*>^q where q is (Element of NAT*), i is Nat:
$1 = i+1 & q in p.(i+1)};
consider f being Function such that
A5: dom f = dom p & for x being object st x in dom p holds f.x = F(x)
from FUNCT_1:sch 3;
A6: rng f = X
proof
thus rng f c= X
proof let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in rng f;
then consider y being object such that
A7: y in dom f & x = f.y by FUNCT_1:def 3;
A8: x = F(y) by A5,A7;
reconsider y as Element of NAT by A5,A7;
consider i being Nat such that
A9: y = 1+i by A5,A7,FINSEQ_3:25,NAT_1:10;
y <= len p by A5,A7,FINSEQ_3:25;
then
A10: i < len p by A9,NAT_1:13;
xx = {<*i*>^q where q is Element of NAT*: q in p.(i+1)}
proof
thus xx c= {<*i*>^q where q is Element of NAT*: q in p.(i+1)}
proof
let z be object; assume z in xx;
then consider q being (Element of NAT*), j being Nat such that
A11: z = <*j*>^q & i+1 = j+1 & q in p.(j+1) by A8,A9;
thus thesis by A11;
end;
let z be object;
assume z in {<*i*>^q where q is Element of NAT*: q in p.(i+1)};
then consider q being Element of NAT* such that
A12: z = <*i*>^q & q in p.(i+1);
thus thesis by A8,A9,A12;
end;
hence x in X by A10;
end;
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in X;
then consider i being Nat such that
A13: x = {<*i*>^q where q is Element of NAT*: q in p.(i+1)} & i < len p;
A14: xx = F(i+1)
proof
thus xx c= F(i+1)
proof
let z be object; assume z in xx;
then consider q being Element of NAT* such that
A15: z = <*i*>^q & q in p.(i+1) by A13;
thus z in F(i+1) by A15;
end;
let z be object; assume z in F(i+1);
then consider q being (Element of NAT*), j being Nat such that
A16: z = <*j*>^q & i+1 = j+1 & q in p.(j+1);
thus z in xx by A13,A16;
end;
A17: i+1 >= 1 & i+1 <= len p by A13,NAT_1:11,13;
then
A18: i+1 in dom f by A5,FINSEQ_3:25;
f.(i+1) = x by A5,A14,A17,FINSEQ_3:25;
hence x in rng f by A18,FUNCT_1:def 3;
end;
now let x; assume x in X;
then consider i being Nat such that
A19: x = {<*i*>^q where q is Element of NAT*: q in p.(i+1)} & i < len p;
i+1 >= 1 & i+1 <= len p by A19,NAT_1:11,13;
then i+1 in dom p by FINSEQ_3:25;
then p.(i+1) in rng p & rng p is constituted-Trees
by FUNCT_1:def 3,TREES_3:def 9;
then reconsider t = p.(i+1) as finite Tree;
deffunc G(Element of t) = <*i*>^$1;
consider g being Function such that
A20
: dom g = t & for x being Element of t holds g.x = G(x) from FUNCT_1:sch 4;
A21: x c= rng g
proof
let z be object; assume z in x;
then consider q being Element of NAT* such that
A22: z = <*i*>^q & q in p.(i+1) by A19;
z = g.q by A20,A22;
hence thesis by A20,A22,FUNCT_1:def 3;
end;
rng g is finite by A20,FINSET_1:8;
hence x is finite by A21;
end;
then union X is finite by A6,A5,FINSET_1:7,8;
hence tree p is finite by A1;
end;
end;
registration
let t be finite DecoratedTree;
cluster Subtrees t -> finite-membered;
coherence;
end;
registration
let p be finite-yielding DTree-yielding FinSequence;
let x;
cluster x-tree p -> finite;
coherence
proof
dom (x-tree p) = tree doms p by TREES_4:10;
hence thesis by FINSET_1:10;
end;
end;
theorem Th6:
for t1,t2 being finite DecoratedTree st t1 in Subtrees t2
holds height dom t1 <= height dom t2
proof
let t1,t2 be finite DecoratedTree; assume
t1 in Subtrees t2;
then consider p being Element of dom t2 such that
A1: t1 = t2|p;
consider r being FinSequence of NAT such that
A2: r in dom t1 & len r = height dom t1 by TREES_1:def 12;
dom t1 = (dom t2)|p by A1,TREES_2:def 10;
then p^r in dom t2 by A2,TREES_1:def 6;
then len (p^r) <= height dom t2 by TREES_1:def 12;
then len p + len r <= height dom t2 & len r <= len p+len r
by NAT_1:11,FINSEQ_1:22;
hence height dom t1 <= height dom t2 by A2,XXREAL_0:2;
end;
theorem Th7:
for p being DTree-yielding FinSequence st p is finite-yielding
for t being DecoratedTree st x in Subtrees t & t in rng p
holds x <> y-tree p
proof
let p be DTree-yielding FinSequence such that
A1: p is finite-yielding;
let t be DecoratedTree; assume
A2: x in Subtrees t & t in rng p;
reconsider t as finite DecoratedTree
by A1,A2;
x is Element of Subtrees t by A2;
then reconsider x as finite DecoratedTree;
reconsider p as finite-yielding DTree-yielding FinSequence by A1;
consider z being object such that
A3: z in dom p & t = p.z by A2,FUNCT_1:def 3;
reconsider z as Nat by A3;
consider i such that
A4: z = 1+i by A3,FINSEQ_3:25,NAT_1:10;
reconsider i as Element of NAT by ORDINAL1:def 12;
z <= len p by A3,FINSEQ_3:25;
then
A5: i < len p by A4,NAT_1:13;
A6: dom (y-tree p) = tree doms p by TREES_4:10;
A7: len doms p = len p by TREES_3:38;
A8: dom t = (doms p).z by A3,FUNCT_6:22;
consider h being FinSequence of NAT such that
A9: h in dom t & len h = height dom t by TREES_1:def 12;
<*i*>^h in dom (y-tree p) by A4,A5,A6,A7,A8,A9,TREES_3:48;
then len (<*i*>^h) <= height dom (y-tree p) by TREES_1:def 12;
then len <*i*> + len h <= height dom (y-tree p) & len <*i*> = 1
by FINSEQ_1:22,40;
hence thesis by A2,Th6,A9,NAT_1:13;
end;
registration
let S;
let X be ManySortedSet of S;
cluster -> finite-yielding for S-Terms X-valued Function;
coherence
proof
let f be S-Terms X-valued Function;
for x st x in rng f holds x is finite;
hence thesis;
end;
end;
theorem Th8:
for X being non empty constituted-DTrees set
for t being DecoratedTree st t in X
holds Subtrees t c= Subtrees X
proof
let X be non empty constituted-DTrees set;
let t be DecoratedTree such that
A1: t in X;
let x be object; assume x in Subtrees t;
then consider p being Element of dom t such that
A2: x = t|p;
thus thesis by A1,A2;
end;
theorem Th9:
for X being non empty constituted-DTrees set holds X c= Subtrees X
proof
let X be non empty constituted-DTrees set;
let x be object; assume x in X;
then reconsider x as Element of X;
reconsider p = {} as Element of dom x by TREES_1:22;
x = x|p by TREES_9:1;
hence thesis;
end;
theorem Th10:
for t being Term of S,X
for x st x in Subtrees t holds x is Term of S,X
proof
let t be Term of S,X;
let x; assume x in Subtrees t;
then consider p being Element of dom t such that
A1: x = t|p;
thus x is Term of S,X by A1;
end;
theorem Th11:
for p being DTree-yielding FinSequence holds
rng p c= Subtrees (x-tree p)
proof
let p be DTree-yielding FinSequence;
let z be object; assume z in rng p;
then consider y being object such that
A1: y in dom p & z = p.y by FUNCT_1:def 3;
reconsider y as Nat by A1;
consider i being Nat such that
A2: y = 1+i by A1,FINSEQ_3:25,NAT_1:10;
reconsider i as Element of NAT by ORDINAL1:def 12;
y <= len p by A1,FINSEQ_3:25;
then
A3: i < len p by A2,NAT_1:13;
then
A4: z = (x-tree p)|<*i*> by A1,A2,TREES_4:def 4;
then reconsider z as DecoratedTree;
reconsider q = {} as Element of dom z by TREES_1:22;
dom(x-tree p) = tree doms p & dom z = (doms p).y & len doms p = len p
by A1,FUNCT_6:22,TREES_4:10,TREES_3:38;
then <*i*>^q in dom(x-tree p) by A2,A3,TREES_3:def 15;
then <*i*> in dom(x-tree p) by FINSEQ_1:34;
hence thesis by A4;
end;
theorem Th12:
for t1,t2 being DecoratedTree st t1 in Subtrees t2
holds Subtrees t1 c= Subtrees t2
proof
let t1,t2 be DecoratedTree; assume t1 in Subtrees t2;
then consider p being Element of dom t2 such that
A1: t1 = t2|p;
thus Subtrees t1 c= Subtrees t2 by A1,TREES_9:13;
end;
theorem Th13:
for X being ManySortedSet of S
for o being OperSymbol of S
for p being FinSequence st p in Args(o,Free(S,X)) holds
Den(o,Free(S,X)).p = [o,the carrier of S]-tree p
proof
let X be ManySortedSet of S;
let o be OperSymbol of S;
let p be FinSequence such that
A1: p in Args(o,Free(S,X));
set Y = X (\/) ((the carrier of S) --> {0});
consider A being MSSubset of FreeMSA Y such that
A2: Free(S,X) = GenMSAlg A & A = (Reverse (Y))""X by MSAFREE3:def 1;
A3: Free(S,Y) = FreeMSA Y by MSAFREE3:31;
then Args(o,Free(S,X)) c= Args(o,Free(S,Y)) by A2,MSAFREE3:37;
then Den(o,Free(S,Y)).p = [o,the carrier of S]-tree p by A1,A3,INSTALG1:3;
hence Den(o,Free(S,X)).p = [o,the carrier of S]-tree p
by A1,A2,A3,EQUATION:19;
end;
registration
let I be set;
let A,B be non-empty ManySortedSet of I;
let f be ManySortedFunction of A,B;
cluster rngs f -> non-empty;
coherence
proof
let x be object; assume
A1: x in I;
(rngs f).x = rng(f.x) & dom(f.x) = A.x by A1,FUNCT_2:def 1,MSSUBFAM:13;
hence thesis by A1,RELAT_1:42;
end;
end;
registration
let S;
cluster -> Relation-like Function-like for Element of TermAlg S;
coherence
proof
Union the Sorts of TermAlg S = S-Terms ((the carrier of S)--> NAT)
by MSATERM:13;
hence thesis;
end;
end;
registration
let I be set;
let A be ManySortedSet of I;
let f be FinSequence of I;
cluster A*f -> dom f-defined;
coherence
proof
rng f c= I & dom A = I by PARTFUN1:def 2;
then dom (A*f) = dom f by RELAT_1:27;
hence thesis by RELAT_1:def 18;
end;
end;
registration
let I be set;
let A be ManySortedSet of I;
let f be FinSequence of I;
cluster A*f -> total for dom f-defined Relation;
coherence
proof
rng f c= I & dom A = I by PARTFUN1:def 2;
then dom (A*f) = dom f by RELAT_1:27;
hence thesis by PARTFUN1:def 2;
end;
end;
theorem
for I being non empty set, J being set
for A,B being ManySortedSet of I st A c= B
for f being Function of J,I holds A*f c= B*f qua ManySortedSet of J
proof
let I be non empty set, J be set;
let A,B be ManySortedSet of I;
assume A1: A c= B;
let f be Function of J,I;
let j be object;
assume A2: j in J;
then (A*f).j = A.(f.j) & (B*f).j = B.(f.j) by FUNCT_2:15;
hence (A*f).j c= (B*f).j by A1,A2,FUNCT_2:5;
end;
theorem Th15:
for I being set
for A,B being ManySortedSet of I st A c= B
for f being FinSequence of I holds A*f c= B*f qua ManySortedSet of dom f
proof
let I be set;
let A,B be ManySortedSet of I;
assume A1: A c= B;
let f be FinSequence of I;
let j be object;
assume A2: j in dom f;
then (A*f).j = A.(f.j) & (B*f).j = B.(f.j) by FUNCT_1:13;
hence (A*f).j c= (B*f).j by A1,A2,FUNCT_1:102;
end;
theorem Th16:
for I being set
for A,B being ManySortedSet of I st A c= B
holds product A c= product B
proof
let I be set;
let A,B be ManySortedSet of I;
assume A1: A c= B;
let x be object; assume x in product A; then
consider g being Function such that
A2: x = g & dom g = dom A & for y being object st y in dom A holds g.y in A.y
by CARD_3:def 5;
A3: dom A = I & dom B = I by PARTFUN1:def 2;
now let y be object; assume y in I; then
g.y in A.y & A.y c= B.y by A1,A2,A3;
hence g.y in B.y;
end;
hence x in product B by A2,A3,CARD_3:9;
end;
theorem Th17:
for R being weakly-normalizing with_UN_property Relation
st x is_a_normal_form_wrt R holds nf(x,R) = x
proof
let R be weakly-normalizing with_UN_property Relation;
assume A1: x is_a_normal_form_wrt R;
A2: x is_a_normal_form_of x,R by A1,REWRITE1:12;
then
A3: x has_a_normal_form_wrt R;
for b,c being object st b is_a_normal_form_of x,R & c
is_a_normal_form_of x,R holds b = c by REWRITE1:53;
hence nf(x,R) = x by A2,A3,REWRITE1:def 12;
end;
theorem Th18:
for R being weakly-normalizing with_UN_property Relation
holds nf(nf(x,R),R) = nf(x,R)
proof
let R be weakly-normalizing with_UN_property Relation;
nf(x,R) is_a_normal_form_of x,R by REWRITE1:54;
then
A1: nf(x,R) is_a_normal_form_wrt R & R reduces nf(x,R),nf(x,R)
by REWRITE1:12;
then
A2: nf(x,R) is_a_normal_form_of nf(x,R),R;
nf(x,R) has_a_normal_form_wrt R &
for b,c being object st b is_a_normal_form_of nf(x,R),R & c
is_a_normal_form_of nf(x,R),R holds b = c
by A1,REWRITE1:def 6,53;
hence nf(nf(x,R),R) = nf(x,R) by A2,REWRITE1:def 12;
end;
registration
let S, X;
let A be MSSubset of FreeMSA X;
let x be object;
cluster -> Relation-like Function-like for Element of A.x;
coherence
proof
let t be Element of A.x;
per cases;
suppose x nin dom A or A.x = {};
then A.x = {} by FUNCT_1:def 2;
hence thesis;
end;
suppose
A1: x in the carrier of S & A.x <> {};
then reconsider s = x as SortSymbol of S;
A.s c= (the Sorts of FreeMSA X).s & t in A.s by A1,PBOOLE:def 2,def 18;
then t is Element of (the Sorts of FreeMSA X).s;
then t is Term of S,X by MSATERM:13;
hence thesis;
end;
end;
end;
definition
let I be set;
let A be ManySortedSet of I;
attr A is countable means: Def1:
for x st x in I holds A.x is countable;
end;
registration
let I be set;
let X be countable set;
cluster I --> X -> countable for ManySortedSet of I;
coherence
by FUNCOP_1:7;
end;
registration
let I be set;
cluster non-empty countable for ManySortedSet of I;
existence
proof
take I-->NAT;
thus thesis;
end;
end;
registration
let I be set;
let X be countable ManySortedSet of I;
let x be object;
cluster X.x -> countable;
coherence
proof
x in I or x nin dom X;
hence thesis by Def1,FUNCT_1:def 2;
end;
end;
registration
let A be countable set;
cluster one-to-one for Function of A,NAT;
existence
proof
set f = the Enumeration of A;
dom f = A & rng f c= NAT by AOFA_I00:6,11;
then f is Function of A,NAT by FUNCT_2:2;
hence thesis;
end;
end;
registration
let I be set;
let X0 be countable ManySortedSet of I;
cluster "1-1" for ManySortedFunction of X0, I-->NAT;
existence
proof
deffunc F(object) = the one-to-one Function of X0.$1, NAT;
consider f being ManySortedSet of I such that
A1: for x being object st x in I holds f.x = F(x) from PBOOLE:sch 4;
f is ManySortedFunction of X0, I-->NAT
proof
let x be object; assume x in I;
then f.x = F(x) & (I-->NAT).x = NAT by A1,FUNCOP_1:7;
hence thesis;
end;
then reconsider f as ManySortedFunction of X0, I-->NAT;
take f; let x; let g be Function;
assume x in dom f;
then f.x = F(x) by A1;
hence thesis;
end;
end;
theorem Th19:
for S being set
for X being ManySortedSet of S
for Y being non-empty ManySortedSet of S
for w being ManySortedFunction of X, Y
holds rngs w is ManySortedSubset of Y
proof
let S be set;
let X be ManySortedSet of S;
let Y be non-empty ManySortedSet of S;
let w be ManySortedFunction of X, Y;
let x be object; assume x in S; then
(rngs w).x = rng(w.x) by MSSUBFAM:13;
hence (rngs w).x c= Y.x;
end;
theorem
for S being set
for X being countable ManySortedSet of S
ex Y being ManySortedSubset of S-->NAT,
w being ManySortedFunction of X, S-->NAT st
w is "1-1" & Y = rngs w &
for x st x in S holds w.x is Enumeration of X.x & Y.x = card(X.x)
proof let S be set;
let X be countable ManySortedSet of S;
set Y = S-->NAT;
deffunc F(object) = the Enumeration of X.$1;
consider w being ManySortedSet of S such that
A1: for s being object st s in S holds w.s = F(s) from PBOOLE:sch 4;
w is Function-yielding
proof
let x be object; assume x in dom w;
then w.x = F(x) by A1;
hence thesis;
end;
then reconsider w as ManySortedFunction of S;
w is ManySortedFunction of X,Y
proof
let x be object; assume
A2: x in S;
A3: card (X.x) c= NAT by CARD_3:def 14;
A4: w.x = F(x) by A1,A2;
then
A5: dom (w.x) = X.x by AOFA_I00:6;
A6: Y.x = NAT by A2,FUNCOP_1:7;
rng (w.x) c= Y.x by A4,A3,A6,AOFA_I00:6;
hence thesis by A5,FUNCT_2:2;
end;
then reconsider w as ManySortedFunction of X,Y;
reconsider Z = rngs w as ManySortedSubset of Y by Th19;
take Z,w;
thus w is "1-1"
proof
let x; let f be Function;
assume x in dom w;
then w.x = F(x) by A1;
hence thesis;
end;
thus Z = rngs w;
let x; assume x in S;
then w.x = F(x) & Z.x = rng(w.x) by A1,MSSUBFAM:13;
hence w.x is Enumeration of X.x & Z.x = card(X.x) by AOFA_I00:6;
end;
theorem Th21:
for I being set
for A being ManySortedSet of I
for B being non-empty ManySortedSet of I holds
A is_transformable_to B
proof
let I be set;
let A be ManySortedSet of I;
let B be non-empty ManySortedSet of I;
for i being set st i in I holds B.i = {} implies A.i = {};
hence A is_transformable_to B by PZFMISC1:def 3;
end;
theorem Th22:
for I being set
for A,B,C being non-empty ManySortedSet of I
for f being ManySortedFunction of A,B st B is ManySortedSubset of C
holds f is ManySortedFunction of A,C
proof
let I be set;
let A,B,C be non-empty ManySortedSet of I;
let f be ManySortedFunction of A,B;
assume A1: B c= C;
let x be object; assume
A2: x in I; then
A3: f.x is Function of A.x,B.x & B.x <> {} & B.x c= C.x
by A1;
dom(f.x) = A.x & rng(f.x) c= B.x
by A2,FUNCT_2:def 1;
hence f.x is Function of A.x,C.x by A3,XBOOLE_1:1,FUNCT_2:2;
end;
theorem Th23:
for I being set, A,B being ManySortedSet of I st A is_transformable_to B
for f being ManySortedFunction of A,B st f is "onto"
ex g being ManySortedFunction of B,A st f**g = id B
proof
let I be set;
let A,B be ManySortedSet of I;
assume A1: A is_transformable_to B;
let f be ManySortedFunction of A,B;
assume A2: f is "onto";
deffunc F(object) = the rng-retract of f.$1;
consider g being ManySortedSet of I such that
A3: for i being object st i in I holds g.i = F(i) from PBOOLE:sch 4;
g is Function-yielding
proof
let x be object; assume x in dom g; then
g.x = F(x) by A3;
hence thesis;
end; then
reconsider g as ManySortedFunction of I;
g is ManySortedFunction of B,A
proof
let x be object; assume
A4: x in I; then
A5: g.x = F(x) by A3; then
A6: dom (g.x) = rng (f.x) & rng (f.x) = B.x
by A2,A4,ALGSPEC1:def 2;
A.x <> {} implies B.x <> {} by A4,A1,PZFMISC1:def 3; then
A7: dom (f.x) = A.x by FUNCT_2:def 1;
A8: (f.x)*(g.x) = id (B.x) & dom id (B.x) = B.x
by A5,A6,ALGSPEC1:def 2;
rng (g.x) c= dom (f.x)
proof let y be object;
assume y in rng (g.x); then
consider z being object such that
A9: z in dom (g.x) & y = (g.x).z by FUNCT_1:def 3;
thus y in dom (f.x) by A6,A8,A9,FUNCT_1:11;
end;
hence thesis by A6,A7,FUNCT_2:2;
end; then
reconsider g as ManySortedFunction of B,A;
take g;
now let x be object;
assume
A10: x in I; then
g.x = F(x) by A3; then
(f.x)*(g.x) = id rng (f.x) & dom (g.x) = rng (f.x) & rng (f.x) = B.x
by A2,A10,ALGSPEC1:def 2;
hence (f**g).x = id (B.x) by A10,MSUALG_3:2
.= (id B).x by A10,MSUALG_3:def 1;
end;
hence f**g = id B;
end;
Lm2:
now
let p be FinSequence;
let i;
assume i < len p; then
i+1 <= len p & 1 <= i+1 by NAT_1:13,11;
hence i+1 in dom p by FINSEQ_3:25;
end;
theorem Th24:
for A1,A2 being MSAlgebra over S
st the MSAlgebra of A1 = the MSAlgebra of A2
for B1 being MSSubset of A1, B2 being MSSubset of A2 st B1 = B2
for o being OperSymbol of S st B1 is_closed_on o holds B2 is_closed_on o;
theorem Th25:
for A1,A2 being MSAlgebra over S
st the MSAlgebra of A1 = the MSAlgebra of A2
for B1 being MSSubset of A1, B2 being MSSubset of A2 st B1 = B2
for o being OperSymbol of S st B1 is_closed_on o holds o/.B2 = o/.B1
proof
let A1,A2 be MSAlgebra over S;
assume A1: the MSAlgebra of A1 = the MSAlgebra of A2;
let B1 be MSSubset of A1;
let B2 be MSSubset of A2;
assume A2: B1 = B2;
let o be OperSymbol of S;
assume A3: B1 is_closed_on o;
hence o/.B2 = (Den(o,A2)) | ((B2# * the Arity of S).o)
by A1,A2,Th24,MSUALG_2:def 7
.= (Den(o,A1)) | ((B1# * the Arity of S).o) by A1,A2
.= o/.B1 by A3,MSUALG_2:def 7;
end;
theorem Th26:
for A1,A2 being MSAlgebra over S
st the MSAlgebra of A1 = the MSAlgebra of A2
for B1 being MSSubset of A1, B2 being MSSubset of A2
st B1 = B2 & B1 is opers_closed holds Opers(A2,B2) = Opers(A1,B1)
proof
let A1,A2 be MSAlgebra over S;
assume A1: the MSAlgebra of A1 = the MSAlgebra of A2;
let B1 be MSSubset of A1;
let B2 be MSSubset of A2;
assume A2: B1 = B2 & B1 is opers_closed;
now
let x be object; assume x in the carrier' of S; then
reconsider o = x as OperSymbol of S;
thus Opers(A2,B2).x = o/.B2 by MSUALG_2:def 8
.= o/.B1 by A1,A2,Th25
.= Opers(A1,B1).x by MSUALG_2:def 8;
end;
hence Opers(A2,B2) = Opers(A1,B1);
end;
theorem Th27:
for A1,A2 being MSAlgebra over S
st the MSAlgebra of A1 = the MSAlgebra of A2
for B1 being MSSubset of A1, B2 being MSSubset of A2
st B1 = B2 & B1 is opers_closed holds B2 is opers_closed
by Th24;
theorem
for A1,A2,B being MSAlgebra over S
st the MSAlgebra of A1 = the MSAlgebra of A2
for B1 being MSSubAlgebra of A1 st the MSAlgebra of B = the MSAlgebra of B1
holds B is MSSubAlgebra of A2
proof
let A1,A2,B be MSAlgebra over S;
assume A1: the MSAlgebra of A1 = the MSAlgebra of A2;
let B1 be MSSubAlgebra of A1;
assume A2: the MSAlgebra of B = the MSAlgebra of B1;
thus the Sorts of B is MSSubset of A2 by A1,A2,MSUALG_2:def 9;
let C be MSSubset of A2;
reconsider C1 = C as MSSubset of A1 by A1;
assume
A3: C = the Sorts of B;
hence C is opers_closed by A1,Th27,A2,MSUALG_2:def 9;
the Charact of B1 = Opers(A1,C1) by A2,A3,MSUALG_2:def 9;
hence the Charact of B = Opers(A2,C) by A1,A2,A3,MSUALG_2:def 9,Th26;
end;
theorem
for A1,A2 being MSAlgebra over S st A2 is empty
for h being ManySortedFunction of A1,A2
holds h is_homomorphism A1,A2
proof
let A1,A2 be MSAlgebra over S such that
A1: the Sorts of A2 is empty-yielding;
let h be ManySortedFunction of A1,A2;
let o be OperSymbol of S;
assume Args(o,A1) <> {};
let x be Element of Args(o,A1);
(the Sorts of A2).the_result_sort_of o = {} by A1; then
A2: Result(o,A2) = {} by PRALG_2:3;
thus (h.(the_result_sort_of o)).(Den(o,A1).x) = {} by A1
.= Den(o,A2).(h#x) by A2;
end;
theorem Th30:
for A1,A2,B1 being MSAlgebra over S, B2 being non-empty MSAlgebra over S
st the MSAlgebra of A1 = the MSAlgebra of A2 &
the MSAlgebra of B1 = the MSAlgebra of B2
for h1 being ManySortedFunction of A1,B1
for h2 being ManySortedFunction of A2,B2 st h1 = h2 &
h1 is_homomorphism A1,B1 holds h2 is_homomorphism A2,B2
proof
let A1,A2,B1 be MSAlgebra over S,B2 be non-empty MSAlgebra over S such that
A1: the MSAlgebra of A1 = the MSAlgebra of A2 &
the MSAlgebra of B1 = the MSAlgebra of B2;
let h1 be ManySortedFunction of A1,B1;
let h2 be ManySortedFunction of A2,B2 such that
A2: h1 = h2 & h1 is_homomorphism A1,B1;
let o be OperSymbol of S such that
A3: Args(o,A2) <> {};
let x be Element of Args(o,A2);
reconsider x1 = x as Element of Args(o,A1) by A1;
thus (h2.(the_result_sort_of o)).(Den(o,A2).x)
= (h1.(the_result_sort_of o)).(Den(o,A1).x1) by A1,A2
.= Den(o,B1).(h1#x1) by A2,A1,A3
.= Den(o,B2).(h2#x) by A1,A2,A3,INSTALG1:5;
end;
begin :: Trivial algebras
definition
let I be set;
let X be ManySortedSet of I;
redefine attr X is trivial-yielding means: Def2: :: redefines trivial-yielding (PENCIL_1, definition)
for x st x in I holds X.x is trivial;
compatibility
proof
hereby assume
A1: X is trivial-yielding;
let x; assume x in I;
then x in dom X by PARTFUN1:def 2;
then X.x in rng X by FUNCT_1:def 3;
hence X.x is trivial by A1,PENCIL_1:def 16;
end;
assume
A2: for x st x in I holds X.x is trivial;
now
let y; assume y in rng X;
then consider x being object such that
A3: x in dom X & y = X.x by FUNCT_1:def 3;
thus y is trivial by A2,A3;
end;
hence thesis by PENCIL_1:def 16;
end;
end;
registration
let I be set;
cluster non-empty trivial-yielding for ManySortedSet of I;
existence
proof
deffunc F(object) = {$1};
consider S being ManySortedSet of I such that
A1: for x being object st x in I holds S.x = F(x) from PBOOLE:sch 4;
take S;
hereby
let x be object; assume x in I; then
S.x = F(x) by A1;
hence S.x is non empty;
end;
let x be set; assume x in I; then
S.x = F(x) by A1;
hence thesis;
end;
end;
registration
let I be set;
let S be trivial-yielding ManySortedSet of I;
let x be object;
cluster S.x -> trivial;
coherence
proof
(x in I or x nin I) & dom S = I by PARTFUN1:def 2;
hence thesis by Def2,FUNCT_1:def 2;
end;
end;
definition
let S;
let A be MSAlgebra over S;
attr A is trivial means: Def3:
the Sorts of A is trivial-yielding;
end;
registration
let S;
cluster trivial disjoint_valued non-empty for strict MSAlgebra over S;
existence
proof
deffunc F(object) = {$1};
consider X being ManySortedSet of S such that
A1: for x being object st x in the carrier of S holds X.x = F(x)
from PBOOLE:sch 4;
set o = the ManySortedFunction of X#*the Arity of S, X*the ResultSort of S;
take A = MSAlgebra(#X,o#);
thus the Sorts of A is trivial-yielding
proof
let x; assume x in the carrier of S; then
X.x = F(x) by A1;
hence thesis;
end;
thus the Sorts of A is disjoint_valued
proof
let x,y be object; assume
A2: x <> y;
(x in the carrier of S or x nin the carrier of S) &
(y in the carrier of S or y nin the carrier of S) &
dom the Sorts of A = the carrier of S by PARTFUN1:def 2; then
(F(x) = X.x or X.x = {}) & (F(y) = X.y or X.y = {}) by A1,FUNCT_1:def 2;
hence thesis by A2,ZFMISC_1:11;
end;
thus the Sorts of A is non-empty
proof
let x be object; assume x in the carrier of S; then
X.x = F(x) by A1;
hence thesis;
end;
thus thesis;
end;
end;
registration
let S;
let A be trivial MSAlgebra over S;
cluster the Sorts of A -> trivial-yielding;
coherence by Def3;
end;
theorem Th31:
for A being trivial non-empty MSAlgebra over S
for s being SortSymbol of S
for e being Element of (Equations S).s
holds A |= e
proof
let A be trivial non-empty MSAlgebra over S;
let s be SortSymbol of S;
let e be Element of (Equations S).s;
let h be ManySortedFunction of TermAlg S, A;
assume h is_homomorphism TermAlg S, A;
h.s.(e`1) in (the Sorts of A).s &
h.s.(e`2) in (the Sorts of A).s by FUNCT_2:5,EQUATION:30,29;
hence h.s.(e`1) = h.s.(e`2) by ZFMISC_1:def 10;
end;
theorem Th32:
for A being trivial non-empty MSAlgebra over S
for T being EqualSet of S
holds A |= T
by Th31;
theorem Th33:
for A being non-empty MSAlgebra over S
for T being non-empty trivial MSAlgebra over S
for f being ManySortedFunction of A,T holds
f is_homomorphism A,T
proof
let A be non-empty MSAlgebra over S;
let T be non-empty trivial MSAlgebra over S;
let f be ManySortedFunction of A,T;
let o be OperSymbol of S; assume
Args(o,A) <> {};
let x be Element of Args(o,A);
A1: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1; then
reconsider a = Den(o,A).x as Element of
(the Sorts of A).the_result_sort_of o by FUNCT_1:13;
Den(o,T).(f#x) in Result(o,T); then
(the Sorts of T).the_result_sort_of o is trivial &
Den(o,T).(f#x) in (the Sorts of T).the_result_sort_of o &
(f.(the_result_sort_of o)).a in (the Sorts of T).the_result_sort_of o
by A1,FUNCT_1:13;
hence (f.(the_result_sort_of o)).(Den(o,A).x) = Den(o,T).(f#x)
by ZFMISC_1:def 10;
end;
theorem Th34:
for T being non-empty trivial MSAlgebra over S
for A being non-empty MSSubAlgebra of T holds
the MSAlgebra of A = the MSAlgebra of T
proof
let T be non-empty trivial MSAlgebra over S;
let A be non-empty MSSubAlgebra of T;
A1: the Sorts of A is ManySortedSubset of the Sorts of T
by MSUALG_2:def 9;
A2: now
let x be object;
assume
A3: x in the carrier of S; then
A4: (the Sorts of A).x c= (the Sorts of T).x & (the Sorts of A).x <> {} &
(the Sorts of T).x <> {} by A1,PBOOLE:def 2,def 18;
(the Sorts of A).x is non empty trivial by A4;
then consider a being object such that
A5: (the Sorts of A).x = {a} by ZFMISC_1:131;
consider b being object such that
A6: (the Sorts of T).x = {b} by A3,ZFMISC_1:131;
thus (the Sorts of A).x = (the Sorts of T).x
by A4,A5,A6,ZFMISC_1:3;
end;
the MSAlgebra of T = the MSAlgebra of T;
then T is MSSubAlgebra of T & A is MSSubAlgebra of T by MSUALG_2:5;
hence the MSAlgebra of A = the MSAlgebra of T by A2,PBOOLE:3,MSUALG_2:9;
end;
begin :: Image
definition
let S;
let A be non-empty MSAlgebra over S;
let C be MSAlgebra over S;
attr C is A-Image means
ex B being non-empty MSAlgebra over S, h being ManySortedFunction of A,B st
h is_homomorphism A,B & the MSAlgebra of C = Image h;
end;
registration
let S;
let A be non-empty MSAlgebra over S;
cluster A-Image -> non-empty for MSAlgebra over S;
coherence
proof let C be MSAlgebra over S; assume
C is A-Image; then
consider B being non-empty MSAlgebra over S,
h being ManySortedFunction of A,B such that
A1: h is_homomorphism A,B & the MSAlgebra of C = Image h;
thus the Sorts of C is non-empty by A1;
end;
cluster A-Image for non-empty strict MSAlgebra over S;
existence
proof
take C = Image id the Sorts of A, A, h = id the Sorts of A;
thus h is_homomorphism A,A by MSUALG_3:9;
thus thesis;
end;
end;
definition
let S;
let A be non-empty MSAlgebra over S;
let C be non-empty MSAlgebra over S;
redefine attr C is A-Image means: Def5: :: redefines -Image (MSAFREE4, definition)
ex h being ManySortedFunction of A,C st h is_epimorphism A,C;
compatibility
proof
thus C is A-Image implies
ex h being ManySortedFunction of A,C st h is_epimorphism A,C
proof
given B being non-empty MSAlgebra over S,
h being ManySortedFunction of A,B such that
A1: h is_homomorphism A,B & the MSAlgebra of C = Image h;
consider g0 being ManySortedFunction of A, Image h such that
A2: h = g0 & g0 is_epimorphism A, Image h by A1,MSUALG_3:21;
reconsider g = g0 as ManySortedFunction of A,C by A1;
take g; thus g is_homomorphism A,C
proof
let o be OperSymbol of S; assume Args(o,A) <> {};
let x be Element of Args(o,A);
A3: Args(o,Image h) = Args(o,C) & Den(o,Image h) = Den(o,C) by A1;
g0#x = (Frege(g0*the_arity_of o)).x by MSUALG_3:def 5
.= g#x by MSUALG_3:def 5;
hence (g.(the_result_sort_of o)).(Den(o,A).x) = Den(o,C).(g#x)
by A2,A3,MSUALG_3:def 7;
end;
thus g is "onto" by A1,A2;
end;
given h being ManySortedFunction of A,C such that
A4: h is_epimorphism A,C;
take C,h;
thus h is_homomorphism A,C by A4;
thus thesis by A4,MSUALG_3:19;
end;
end;
definition
let S;
let A be non-empty MSAlgebra over S;
mode image of A is A-Image non-empty MSAlgebra over S;
end;
registration
let S;
let A be non-empty MSAlgebra over S;
cluster disjoint_valued trivial for image of A;
existence
proof
set T = the trivial disjoint_valued non-empty MSAlgebra over S;
set h = the ManySortedFunction of A,T;
reconsider T0 = T as MSAlgebra over S;
T0 is A-Image
proof
take T,h;
thus h is_homomorphism A,T by Th33;
thus the MSAlgebra of T0 = Image h by Th34;
end;
hence thesis;
end;
end;
theorem Th35:
for A being non-empty MSAlgebra over S
for B being A-Image MSAlgebra over S
for s being SortSymbol of S
for e being Element of (Equations S).s
st A |= e holds B |= e
proof
let A be non-empty MSAlgebra over S;
let B be A-Image MSAlgebra over S;
consider f being ManySortedFunction of A,B such that
A1: f is_epimorphism A,B by Def5;
let s be SortSymbol of S;
let e be Element of (Equations S).s;
assume A2: A |= e;
let h be ManySortedFunction of TermAlg S, B;
assume
A3: h is_homomorphism TermAlg S, B;
consider g being ManySortedFunction of TermAlg S,A such that
A4: g is_homomorphism TermAlg S, A & h = f**g by A1,A3,EQUATION:24;
h.s = (f.s)*(g.s) & e`1 in (the Sorts of TermAlg S).s &
e`2 in (the Sorts of TermAlg S).s
by A4,MSUALG_3:2,EQUATION:29,30; then
h.s.e`1 = f.s.(g.s.e`1) & h.s.e`2 = f.s.(g.s.e`2) by FUNCT_2:15;
hence h.s.e`1 = h.s.e`2 by A2,A4;
end;
theorem Th36:
for A being non-empty MSAlgebra over S
for B being A-Image MSAlgebra over S
for T being EqualSet of S
st A |= T holds B |= T
by Th35;
begin :: Term Algebras
definition
let S, X;
let A be MSAlgebra over S;
attr A is (X,S)-terms means: Def6:
the Sorts of A is ManySortedSubset of the Sorts of Free(S,X);
end;
registration
let S,X;
cluster Free(S,X) -> X,S-terms;
coherence
proof
thus the Sorts of Free(S,X) is ManySortedSubset of the Sorts of Free(S,X)
proof
thus the Sorts of Free(S,X) c= the Sorts of Free(S,X);
end;
end;
end;
registration
let S, X;
cluster Free(S,X) -> non-empty disjoint_valued;
coherence
proof
A1: Free(S,X) = FreeMSA X by MSAFREE3:31;
hence Free(S,X) is non-empty;
let x,y be object; assume
A2: x <> y;
assume
(the Sorts of Free(S,X)).x meets (the Sorts of Free(S,X)).y; then
consider z being object such that
A3: z in (the Sorts of Free(S,X)).x & z in (the Sorts of Free(S,X)).y
by XBOOLE_0:3;
A4: dom the Sorts of Free(S,X) = the carrier of S by PARTFUN1:def 2; then
reconsider x,y as SortSymbol of S by A3,FUNCT_1:def 2;
z in (the Sorts of Free(S,X)).x by A3; then
reconsider z as Element of Union the Sorts of Free(S,X) by A4,CARD_5:2;
reconsider z as Term of S,X by A1,MSAFREE3:6;
the_sort_of z = x & the_sort_of z = y by A1,A3,MSAFREE3:7;
hence contradiction by A2;
end;
end;
registration
let S,X;
cluster X,S-terms non-empty for strict MSAlgebra over S;
existence
proof
take Free(S,X);
thus thesis;
end;
end;
definition
let S,X;
let A be X,S-terms MSAlgebra over S;
attr A is all_vars_including means: Def7:
FreeGen X is ManySortedSubset of the Sorts of A;
attr A is inheriting_operations means: Def8:
for o being OperSymbol of S, p being FinSequence holds
(p in Args(o, Free(S,X)) &
Den(o,Free(S,X)).p in (the Sorts of A).the_result_sort_of o implies
p in Args(o,A) & Den(o,A).p = Den(o,Free(S,X)).p);
attr A is free_in_itself means: Def9:
for f being ManySortedFunction of FreeGen X, the Sorts of A
for G being ManySortedSubset of the Sorts of A st G = FreeGen X
ex h being ManySortedFunction of A,A st h is_homomorphism A,A & f = h || G;
end;
theorem
for A,B being non-empty MSAlgebra over S
st the MSAlgebra of A = the MSAlgebra of B
holds A is (X,S)-terms implies B is (X,S)-terms;
theorem
for A,B being X,S-terms non-empty MSAlgebra over S
st the MSAlgebra of A = the MSAlgebra of B
holds (A is all_vars_including implies B is all_vars_including) &
(A is inheriting_operations implies B is inheriting_operations) &
(A is free_in_itself implies B is free_in_itself)
proof
let A,B be X,S-terms non-empty MSAlgebra over S such that
A1: the MSAlgebra of A = the MSAlgebra of B;
thus A is all_vars_including implies B is all_vars_including by A1;
thus A is inheriting_operations implies B is inheriting_operations
proof assume
A3: for o being OperSymbol of S, p being FinSequence holds
(p in Args(o, Free(S,X)) &
Den(o,Free(S,X)).p in (the Sorts of A).the_result_sort_of o implies
p in Args(o,A) & Den(o,A).p = Den(o,Free(S,X)).p);
let o be OperSymbol of S, p be FinSequence;
Args(o,A) = Args(o,B) & Den(o,A) = Den(o,B) by A1;
hence p in Args(o, Free(S,X)) &
Den(o,Free(S,X)).p in (the Sorts of B).the_result_sort_of o implies
p in Args(o,B) & Den(o,B).p = Den(o,Free(S,X)).p by A1,A3;
end;
assume
A4: for f being ManySortedFunction of FreeGen X, the Sorts of A
for G being ManySortedSubset of the Sorts of A st G = FreeGen X
ex h being ManySortedFunction of A,A st h is_homomorphism A,A & f = h || G;
let f be ManySortedFunction of FreeGen X, the Sorts of B;
let G be ManySortedSubset of the Sorts of B such that
A5: G = FreeGen X;
reconsider G1 = G as ManySortedSubset of the Sorts of A by A1;
consider h being ManySortedFunction of A,A such that
A6: h is_homomorphism A,A & f = h||G1 by A1,A4,A5;
reconsider h2 = h as ManySortedFunction of B,B by A1;
take h2;
thus h2 is_homomorphism B,B by A6,A1,Th30;
thus f = h2 || G by A1,A6;
end;
registration
let J be non empty non void ManySortedSign;
let T be non-empty MSAlgebra over J;
cluster non-empty for GeneratorSet of T;
existence
proof
the Sorts of T is GeneratorSet of T by MSAFREE2:6;
hence thesis;
end;
end;
registration
let S, X;
cluster Free(S,X) -> all_vars_including inheriting_operations free_in_itself;
coherence
proof
set A = Free(S,X);
A1: A = FreeMSA X by MSAFREE3:31;
thus FreeGen X is ManySortedSubset of the Sorts of A &
for o being OperSymbol of S, p being FinSequence holds
(p in Args(o, Free(S,X)) &
Den(o,Free(S,X)).p in (the Sorts of A).the_result_sort_of o implies
p in Args(o,A) & Den(o,A).p = Den(o,Free(S,X)).p) by MSAFREE3:31;
let f be ManySortedFunction of FreeGen X, the Sorts of A;
let G be MSSubset of A; assume
A2: G = FreeGen X; then
reconsider H = G as non-empty GeneratorSet of A by MSAFREE3:31;
thus thesis by A2,A1,MSAFREE:def 5;
end;
end;
registration
let S, X;
cluster all_vars_including -> non-empty for (X,S)-terms MSAlgebra over S;
coherence
proof
let A be (X,S)-terms MSAlgebra over S;
assume
A1: FreeGen X is ManySortedSubset of the Sorts of A;
let x be object; assume x in the carrier of S; then
reconsider x as SortSymbol of S;
(FreeGen X).x c= (the Sorts of A).x by A1,PBOOLE:def 2,def 18;
hence thesis;
end;
cluster all_vars_including inheriting_operations free_in_itself
for (X,S)-terms strict MSAlgebra over S;
existence
proof
take Free(S,X);
thus thesis;
end;
end;
reserve
A0 for (X,S)-terms non-empty MSAlgebra over S,
A1 for all_vars_including (X,S)-terms MSAlgebra over S,
A2 for all_vars_including inheriting_operations (X,S)-terms MSAlgebra over S,
A for all_vars_including inheriting_operations free_in_itself
(X,S)-terms MSAlgebra over S;
theorem Th39:
(for t being Element of A0 holds t is Element of Free(S,X)) &
for s being SortSymbol of S
for t being Element of A0,s holds t is Element of Free(S,X),s
proof
A1: the Sorts of A0 is MSSubset of Free(S,X) by Def6;
then Union the Sorts of A0 c= Union the Sorts of Free(S,X)
by Th1,PBOOLE:def 18;
hence for t being Element of A0 holds t is Element of Free(S,X);
let s be SortSymbol of S;
let t be Element of A0,s;
t in (the Sorts of A0).s &
(the Sorts of A0).s c= (the Sorts of Free(S,X)).s
by A1,PBOOLE:def 2,def 18;
hence thesis;
end;
theorem Th40:
for s being SortSymbol of S
for x being Element of X.s holds root-tree [x,s] is Element of A1,s
proof
let s be SortSymbol of S;
let x be Element of X.s;
FreeGen X is ManySortedSubset of the Sorts of A1 by Def7; then
A1: (FreeGen X).s c= (the Sorts of A1).s by PBOOLE:def 2,def 18;
root-tree [x,s] in FreeGen(s,X) by MSAFREE:def 15; then
root-tree [x,s] in (FreeGen X).s by MSAFREE:def 16;
hence root-tree [x,s] is Element of A1,s by A1;
end;
theorem Th41:
for o being OperSymbol of S holds Args(o,A1) c= Args(o, Free(S,X))
proof
let o be OperSymbol of S;
let x be object; assume x in Args(o,A1); then
A1: x in product((the Sorts of A1)*the_arity_of o) by PRALG_2:3;
A2: dom((the Sorts of A1)*the_arity_of o) = dom the_arity_of o by PRALG_2:3;
A3: dom((the Sorts of Free(S,X))*the_arity_of o) = dom the_arity_of o
by PRALG_2:3;
now
let a be object; assume
A4: a in dom the_arity_of o; then
A5: (the_arity_of o).a in the carrier of S by FUNCT_1:102;
A6: ((the Sorts of A1)*the_arity_of o).a =
(the Sorts of A1).((the_arity_of o).a) by A4,FUNCT_1:13;
A7: ((the Sorts of Free(S,X))*the_arity_of o).a =
(the Sorts of Free(S,X)).((the_arity_of o).a) by A4,FUNCT_1:13;
the Sorts of A1 is MSSubset of Free(S,X) by Def6;
hence ((the Sorts of A1)*the_arity_of o).a c=
((the Sorts of Free(S,X))*the_arity_of o).a
by A5,A6,A7,PBOOLE:def 2,def 18;
end; then
product((the Sorts of A1)*the_arity_of o) c=
product((the Sorts of Free(S,X))*the_arity_of o) by A2,A3,CARD_3:27; then
x in product((the Sorts of Free(S,X))*the_arity_of o) by A1;
hence x in Args(o, Free(S,X)) by PRALG_2:3;
end;
registration
let S be set;
cluster disjoint_valued non-empty for ManySortedSet of S;
existence
proof
deffunc I(object) = {$1};
consider f being Function such that
A1: dom f = S & for x being object st x in S holds f.x = I(x)
from FUNCT_1:sch 3;
reconsider f as ManySortedSet of S by A1,RELAT_1:def 18,PARTFUN1:def 2;
take f;
thus f is disjoint_valued
proof
let x,y be object;
assume
A2: x <> y;
(x in S or x nin S) & (y in S or y nin S); then
(f.x = {x} or f.x = {}) & (f.y = {y} or f.y = {}) by A1,FUNCT_1:def 2;
hence f.x misses f.y by A2,ZFMISC_1:11;
end;
let x be object; assume x in S; then
f.x = {x} by A1;
hence thesis;
end;
end;
registration
let S be set;
let T be disjoint_valued non-empty ManySortedSet of S;
cluster -> disjoint_valued for ManySortedSubset of T;
coherence
proof
let X be ManySortedSubset of T;
let x,y be object; assume
A1: x <> y;
(x in S or x nin S) & (y in S or y nin S) & X c= T & dom X = S
by PBOOLE:def 18,PARTFUN1:def 2; then
(X.x c= T.x or X.x = {}) & (X.y c= T.y or X.y = {})
by FUNCT_1:def 2;
hence thesis by A1,PROB_2:def 2,XBOOLE_1:64;
end;
end;
registration
let S, X;
cluster (X,S)-terms strict for MSAlgebra over S;
existence
proof
take Free(S,X);
thus thesis;
end;
end;
definition
let S, X, A1;
func canonical_homomorphism A1 -> ManySortedFunction of Free(S,X),A1 means:
Def10:
it is_homomorphism Free(S,X),A1 & for G being GeneratorSet of Free(S,X)
st G = FreeGen X holds id G = it || G;
existence
proof
A1: FreeMSA X = Free(S,X) by MSAFREE3:31;
reconsider H = FreeGen X as non-empty GeneratorSet of Free(S,X)
by MSAFREE3:31;
H is MSSubset of A1 by Def7; then
reconsider f = id H as ManySortedFunction of H, the Sorts of A1 by Th22;
consider g being ManySortedFunction of Free(S,X),A1 such that
A2: g is_homomorphism Free(S,X),A1 & g||H = f by A1,MSAFREE:def 5;
take g; thus thesis by A2;
end;
uniqueness
proof
let h1,h2 be ManySortedFunction of Free(S,X),A1 such that
A3: h1 is_homomorphism Free(S,X),A1 & for G being GeneratorSet of Free(S,X)
st G = FreeGen X holds id G = h1 || G and
A4: h2 is_homomorphism Free(S,X),A1 & for G being GeneratorSet of Free(S,X)
st G = FreeGen X holds id G = h2 || G;
reconsider H = FreeGen X as non-empty GeneratorSet of Free(S,X)
by MSAFREE3:31;
h1 || H = id H by A3 .= h2 || H by A4;
hence h1 = h2 by A3,A4,EXTENS_1:19;
end;
end;
registration
let S, X, A0;
cluster -> Function-like Relation-like for Element of A0;
coherence
proof
let a be Element of A0;
consider x being object such that
A1: x in dom the Sorts of A0 & a in (the Sorts of A0).x by CARD_5:2;
reconsider x as SortSymbol of S by A1;
the Sorts of A0 is ManySortedSubset of the Sorts of Free(S,X) by Def6; then
(the Sorts of A0).x c= (the Sorts of Free(S,X)).x by PBOOLE:def 2,def 18;
then a is Element of (the Sorts of Free(S,X)).x by A1;
hence thesis;
end;
let s be SortSymbol of S;
cluster -> Function-like Relation-like for Element of A0,s;
coherence
proof
let a be Element of A0,s;
a is Element of (the Sorts of A0).s;
hence thesis;
end;
end;
registration
let S, X, A0;
cluster -> DecoratedTree-like for Element of A0;
coherence
proof
let a be Element of A0;
consider x being object such that
A1: x in dom the Sorts of A0 & a in (the Sorts of A0).x by CARD_5:2;
reconsider x as SortSymbol of S by A1;
the Sorts of A0 is ManySortedSubset of the Sorts of Free(S,X) by Def6; then
(the Sorts of A0).x c= (the Sorts of Free(S,X)).x by PBOOLE:def 2,def 18;
then a is Element of (the Sorts of Free(S,X)).x by A1;
hence thesis;
end;
let s be SortSymbol of S;
cluster -> DecoratedTree-like for Element of A0,s;
coherence
proof
let a be Element of A0,s;
a is Element of (the Sorts of A0).s;
hence thesis;
end;
end;
registration
let S, X;
cluster (X,S)-terms -> disjoint_valued for MSAlgebra over S;
coherence
proof let A be MSAlgebra over S;
assume A is (X,S)-terms; then
the Sorts of A is ManySortedSubset of the Sorts of Free(S,X);
hence the Sorts of A is disjoint_valued;
end;
end;
theorem Th42:
for t being Element of A0 holds t is Term of S,X
proof
let t be Element of A0;
consider s being object such that
A1: s in dom the Sorts of A0 & t in (the Sorts of A0).s by CARD_5:2;
reconsider s as SortSymbol of S by A1;
the Sorts of A0 is ManySortedSubset of the Sorts of Free(S,X)
by Def6; then
(the Sorts of A0).s c= (the Sorts of Free(S,X)).s by PBOOLE:def 2,def 18;
then t is Element of (the Sorts of Free(S,X)).s by A1; then
t is Element of FreeMSA X by MSAFREE3:31;
hence t is Term of S,X by MSAFREE3:6;
end;
theorem Th43:
for t being Element of A0
for s being SortSymbol of S st t in (the Sorts of Free(S,X)).s holds
t in (the Sorts of A0).s
proof
let t be Element of A0;
consider x being object such that
A1: x in dom the Sorts of A0 & t in (the Sorts of A0).x by CARD_5:2;
reconsider x as SortSymbol of S by A1;
the Sorts of A0 is ManySortedSubset of the Sorts of Free(S,X)
by Def6; then
A2: (the Sorts of A0).x c= (the Sorts of Free(S,X)).x by PBOOLE:def 2,def 18;
let s be SortSymbol of S;
assume
t in (the Sorts of Free(S,X)).s;
hence t in (the Sorts of A0).s by A1,A2,XBOOLE_0:3,PROB_2:def 2;
end;
theorem
for t being Element of A2
for p being Element of dom t holds t|p is Element of A2
proof set A = A2;
let t be Element of A;
defpred P[Nat] means for p being Element of dom t st len p = $1 holds
t|p is Element of A;
A1: P[0]
proof
let p be Element of dom t; assume len p = 0; then
p = {};
hence thesis by TREES_9:1;
end;
A2: P[i] implies P[i+1]
proof assume
A3: P[i];
let p be Element of dom t; assume
A4: len p = i+1; then
consider q being FinSequence, a being object such that
A5: p = q^<*a*> by FINSEQ_2:18;
<*a*> is FinSequence of NAT by A5,FINSEQ_1:36; then
rng <*a*> c= NAT by FINSEQ_1:def 4; then
{a} c= NAT by FINSEQ_1:39; then
reconsider a as Element of NAT by ZFMISC_1:31;
len <*a*> = 1 by FINSEQ_1:40; then
A6: len p = len q+1 by A5,FINSEQ_1:22;
reconsider q as FinSequence of NAT by A5,FINSEQ_1:36;
reconsider q as Element of dom t by A5,TREES_1:21;
t is Term of S,X by Th42; then
reconsider tq = t|q, tp = t|p as Term of S,X by MSATERM:29;
A7: dom tq = (dom t)|q by TREES_2:def 10; then
<*a*> in dom tq & {} in dom tq by A5,TREES_1:22,def 6; then
tq is not trivial by ZFMISC_1:def 10; then
tq is CompoundTerm of S,X by MSATERM:28; then
tq.{} in [:the carrier' of S,{the carrier of S}:] by MSATERM:def 6; then
consider o,s being object such that
A8: o in the carrier' of S & s in {the carrier of S} & tq.{} = [o,s]
by ZFMISC_1:def 2;
reconsider o as OperSymbol of S by A8;
A9: s = the carrier of S by A8,TARSKI:def 1; then
consider arg being ArgumentSeq of Sym(o,X) such that
A10: tq = [o,the carrier of S]-tree arg by A8,MSATERM:10;
<*a*> in dom tq & dom tq = tree doms arg & <*a*> <> {}
by A7,A5,A10,TREES_1:def 6,TREES_4:10; then
consider n being Nat, e being FinSequence such that
A11: n < len doms arg & e in (doms arg).(n+1) & <*a*> = <*n*>^e
by TREES_3:def 15;
A12: a = <*a*>.1 .= n by A11,FINSEQ_1:41;
A13: Free(S,X) = FreeMSA X by MSAFREE3:31;
A14: tq is Element of A by A3,A6,A4;
Sym(o,X) ==> roots arg & arg is FinSequence of TS DTConMSA X
by MSATERM:21,def 1; then
DenOp(o,X).arg = Sym(o,X)-tree arg by MSAFREE:def 12; then
A15: Den(o, Free(S,X)).arg = tq by A10,A13,MSAFREE:def 13;
the_sort_of tq = the_result_sort_of o by A8,A9,MSATERM:17; then
Den(o,Free(S,X)).arg in FreeSort(X, the_result_sort_of o)
by A15,MSATERM:def 5; then
Den(o,Free(S,X)).arg in (the Sorts of Free(S, X)).the_result_sort_of o
by A13,MSAFREE:def 11; then
A16: Den(o,Free(S,X)).arg in (the Sorts of A).the_result_sort_of o
by A14,A15,Th43;
reconsider r = {} as Element of dom tq by TREES_1:22;
A17: tp = tq|<*a*> & a < len arg by A5,A11,A12,TREES_3:38,TREES_9:3; then
A18: tp = arg.(a+1) & a+1 in dom arg by Lm2,A10,TREES_4:def 4;
reconsider ar = arg as Element of Args(o,Free(S,X)) by A13,INSTALG1:1;
ar in Args(o,A) & dom the Arity of S = the carrier' of S
by A16,Def8,FUNCT_2:def 1; then
arg in cc((the Sorts of A)#,the_arity_of o) by FUNCT_1:13; then
A19: arg in product ((the Sorts of A)*the_arity_of o) by FINSEQ_2:def 5; then
A20: dom arg = dom ((the Sorts of A)*the_arity_of o) by CARD_3:9;
dom ((the Sorts of A)*the_arity_of o) = dom the_arity_of o
by PARTFUN1:def 2;
then (the_arity_of o).(a+1) in rng the_arity_of o by A18,A20
,FUNCT_1:def 3;
then reconsider s = (the_arity_of o).(a+1) as SortSymbol of S;
tp in ((the Sorts of A)*the_arity_of o).(a+1) by A18,A19,A20,CARD_3:9;
then tp is Element of (the Sorts of A).s
by A17,Lm2,A20,FUNCT_1:12;
hence thesis;
end;
A21: P[i] from NAT_1:sch 2(A1,A2);
let p be Element of dom t;
len p = len p;
hence t|p is Element of A by A21;
end;
theorem Th45:
FreeGen X is GeneratorSet of A2
proof set A = A2;
reconsider G = FreeGen X as ManySortedSubset of the Sorts of A by Def7;
defpred P[set] means
for s being SortSymbol of S st $1 in (the Sorts of A).s
holds $1 in (the Sorts of GenMSAlg G).s;
A1: FreeMSA X = Free(S,X) by MSAFREE3:31;
A2: for s being SortSymbol of S, v being Element of X.s holds
P[root-tree [v,s]]
proof
let s be SortSymbol of S;
let v be Element of X.s;
reconsider t = root-tree [v,s] as Term of S,X by MSATERM:4;
let r be SortSymbol of S; assume
A3: root-tree [v,s] in (the Sorts of A).r;
the Sorts of A is ManySortedSubset of the Sorts of Free(S,X) by Def6;then
(the Sorts of A).r c= (the Sorts of Free(S,X)).r by PBOOLE:def 2,def 18;
then t in (the Sorts of Free(S,X)).r by A3; then
t in FreeSort(X,r) by A1,MSAFREE:def 11; then
r = the_sort_of t by MSATERM:def 5 .= s by MSATERM:14; then
root-tree [v,s] in FreeGen(r,X) by MSAFREE:def 15; then
A4: root-tree [v,s] in (FreeGen X).r by MSAFREE:def 16;
FreeGen X is ManySortedSubset of the Sorts of GenMSAlg G
by MSUALG_2:def 17; then
(FreeGen X).r c= (the Sorts of GenMSAlg G).r by PBOOLE:def 2,def 18;
hence thesis by A4;
end;
A5: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) st
for t being Term of S,X st t in rng p holds P[t]
holds P[[o,the carrier of S]-tree p]
proof
let o be OperSymbol of S;
let p be ArgumentSeq of Sym(o,X);
assume A6: for t being Term of S,X st t in rng p holds P[t];
let r be SortSymbol of S;
assume [o,the carrier of S]-tree p in (the Sorts of A).r; then
reconsider t1 = [o,the carrier of S]-tree p as
Element of (the Sorts of A).r;
p is SubtreeSeq of Sym(o,X) by MSATERM:def 2; then
Sym(o,X) ==> roots p & p is FinSequence of TS DTConMSA X
by DTCONSTR:def 6; then
A7: t1 = DenOp(o,X).p by MSAFREE:def 12;
p is Element of Args(o, FreeMSA X) qua non empty set by INSTALG1:1; then
p in Args(o, FreeMSA X); then
A8: p in Args(o, Free(S,X)) by MSAFREE3:31; then
Den(o,Free(S,X)).p in ((the Sorts of Free(S,X))*the ResultSort of S).o &
dom the ResultSort of S = the carrier' of S
by FUNCT_2:5,def 1; then
A9: Den(o,Free(S,X)).p in (the Sorts of Free(S,X)).the_result_sort_of o
by FUNCT_1:13;
Den(o,Free(S,X)).p = t1 by A1,A7,MSAFREE:def 13; then
Den(o,Free(S,X)).p in (the Sorts of A).the_result_sort_of o
by A9,Th43; then
A10: p in Args(o,A) & Den(o,A).p = Den(o,Free(S,X)).p by A8,Def8;
A11: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
A12: Args(o, GenMSAlg G) =
cc((the Sorts of GenMSAlg G)#,(the_arity_of o qua set)) by A11,FUNCT_1:13
.= product ((the Sorts of GenMSAlg G)*the_arity_of o)
by FINSEQ_2:def 5;
A13: Args(o,A) = cc((the Sorts of A)#,the_arity_of o) by A11,FUNCT_1:13
.= product ((the Sorts of A)*the_arity_of o) by FINSEQ_2:def 5;
A14: dom ((the Sorts of GenMSAlg G)*the_arity_of o) = dom the_arity_of o
by PARTFUN1:def 2;
A15: dom ((the Sorts of A)*the_arity_of o) = dom the_arity_of o
by PARTFUN1:def 2; then
A16: dom p = dom the_arity_of o by A10,A13,CARD_3:9;
now let x be object; assume
A17: x in dom the_arity_of o; then
A18: p.x in rng p & p.x in ((the Sorts of A)*the_arity_of o).x
by A16,FUNCT_1:def 3,CARD_3:9,A10,A15,A13;
(the_arity_of o).x in rng the_arity_of o & rng the_arity_of o c=
the carrier of S by A17,FUNCT_1:def 3; then
reconsider s = (the_arity_of o).x as SortSymbol of S;
reconsider px = p.x as Element of (the Sorts of A).s
by A18,A17,FUNCT_1:13;
px is Term of S,X by Th42; then
px in (the Sorts of GenMSAlg G).s by A18,A6;
hence p.x in ((the Sorts of GenMSAlg G)*the_arity_of o).x
by A17,FUNCT_1:13;
end; then
reconsider q = p as Element of Args(o, GenMSAlg G) by A12,A16,A14
,CARD_3:9;
reconsider B = the Sorts of GenMSAlg G as
ManySortedSubset of the Sorts of A by MSUALG_2:def 9;
A19: B is opers_closed & the Charact of GenMSAlg G = Opers(A,B)
by MSUALG_2:def 9;
A20: B is_closed_on o by MSUALG_2:def 6,def 9;
Den(o, GenMSAlg G) = o/.B by A19,MSUALG_2:def 8
.= (Den(o,A))|((B# * the Arity of S).o) by A20,MSUALG_2:def 7; then
A21: Den(o, GenMSAlg G).p = Den(o,A).q by FUNCT_1:49;
A22: Den(o, GenMSAlg G).q = [o,the carrier of S]-tree p
by A1,A21,A7,A10,MSAFREE:def 13; then
A23: [o,the carrier of S]-tree p in Result(o, GenMSAlg G) by FUNCT_2:5;
dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1; then
A24: Result(o, GenMSAlg G) = (the Sorts of GenMSAlg G).the_result_sort_of o &
Result(o, A) = (the Sorts of A).the_result_sort_of o by FUNCT_1:13;
t1 in Result(o, A) & t1 in (the Sorts of A).r by A10,A21,A22,FUNCT_2:5;
hence [o,the carrier of S]-tree p in (the Sorts of GenMSAlg G).r
by A23,A24,PROB_2:def 2,XBOOLE_0:3;
end;
A25: for t being Term of S,X holds P[t] from MSATERM:sch 1(A2,A5);
G is GeneratorSet of A
proof
now
the Sorts of GenMSAlg G is ManySortedSubset of the Sorts of A
by MSUALG_2:def 9;
hence the Sorts of GenMSAlg G c= the Sorts of A by PBOOLE:def 18;
thus the Sorts of A c= the Sorts of GenMSAlg G
proof
let x be object; assume x in the carrier of S; then
reconsider s = x as SortSymbol of S;
let y be object; assume
y in (the Sorts of A).x; then
reconsider y as Element of (the Sorts of A).s;
the Sorts of A is ManySortedSubset of the Sorts of Free(S,X)
by Def6; then
(the Sorts of A).s c= (the Sorts of Free(S,X)).s
by PBOOLE:def 2,def 18; then
y is Element of (the Sorts of Free(S,X)).s; then
y is Element of FreeMSA X by MSAFREE3:31; then
y is Term of S,X by MSAFREE3:6;
hence thesis by A25;
end;
end;
hence the Sorts of GenMSAlg G = the Sorts of A by PBOOLE:146;
end;
hence thesis;
end;
theorem
for T being free_in_itself non-empty (X,S)-terms MSAlgebra over S
for A being image of T
for G being GeneratorSet of T st G = FreeGen X
for f being ManySortedFunction of G, the Sorts of A
ex h being ManySortedFunction of T,A st
h is_homomorphism T,A & f = h||G
proof
let T be free_in_itself non-empty (X,S)-terms MSAlgebra over S;
let A be image of T;
let G be GeneratorSet of T such that
A1: G = FreeGen X;
let f be ManySortedFunction of G, the Sorts of A;
reconsider H = FreeGen X as non-empty GeneratorSet of Free(S,X)
by MSAFREE3:31;
consider j being ManySortedFunction of T,A such that
A2: j is_epimorphism T,A by Def5;
A3: j is_homomorphism T,A & j is "onto" by A2;
consider jj being ManySortedFunction of A,T such that
A4: j**jj = id the Sorts of A by A3,Th23,Th21;
consider h being ManySortedFunction of T,T such that
A5: h is_homomorphism T,T & jj**f = h || G by A1,Def9;
take k = j**h;
thus k is_homomorphism T,A by A3,A5,MSUALG_3:10;
thus f = (id the Sorts of A)**f by MSUALG_3:4
.= j**(jj**f) by A4,PBOOLE:140
.= k || G by A5,EXTENS_1:4;
end;
theorem Th47:
canonical_homomorphism A2 is_epimorphism Free(S,X),A2 &
for s being SortSymbol of S, t being Element of A2,s holds
(canonical_homomorphism A2).s.t = t
proof set A = A2;
A1: FreeMSA X = Free(S,X) by MSAFREE3:31;
reconsider G = FreeGen X as GeneratorSet of Free(S,X) by MSAFREE3:31;
set f = canonical_homomorphism A;
A2: f is_homomorphism Free(S,X),A & f||G = id G by Def10;
defpred P[set] means for s being SortSymbol of S
st $1 in (the Sorts of A).s
holds f.s.$1 = $1;
A3: for s being SortSymbol of S, v being Element of X.s
holds P[root-tree [v,s]]
proof
let s be SortSymbol of S;
let v be Element of X.s;
reconsider t = root-tree [v,s] as Term of S,X by MSATERM:4;
let r be SortSymbol of S; assume
A4: root-tree [v,s] in (the Sorts of A).r;
the Sorts of A is MSSubset of Free(S,X) by Def6; then
(the Sorts of A).r c= (the Sorts of Free(S,X)).r by PBOOLE:def 2,def 18;
then root-tree [v,s] in (FreeSort X).r by A4,A1; then
root-tree [v,s] in FreeSort(X, r) by MSAFREE:def 11; then
A5: the_sort_of t = r & s = the_sort_of t by MSATERM:def 5,14;
root-tree [v,s] in FreeGen(s, X) by MSAFREE:def 15; then
A6: root-tree [v,s] in (FreeGen X).s by MSAFREE:def 16;
A7: (id FreeGen X).s = id ((FreeGen X).s) by MSUALG_3:def 1;
(f.s)|((FreeGen X).s).root-tree [v,s] = (f.s).root-tree [v,s]
by A6,FUNCT_1:49; then
A8: (f.s).root-tree [v,s] = (id((FreeGen X).s)).root-tree [v,s]
by A2,A7,MSAFREE:def 1 .= root-tree [v,s] by A6,FUNCT_1:18;
thus thesis by A5,A8;
end;
A9: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) st
for t being Term of S,X st t in rng p holds P[t]
holds P[[o,the carrier of S]-tree p]
proof
let o be OperSymbol of S;
let p be ArgumentSeq of Sym(o,X);
assume
A10: for t being Term of S,X st t in rng p holds P[t];
let s be SortSymbol of S;
assume
A11: [o,the carrier of S]-tree p in (the Sorts of A).s;
Sym(o,X) ==> roots p & p is FinSequence of TS DTConMSA X
by MSATERM:def 1,21; then
A12: DenOp(o, X).p = Sym(o,X)-tree p & (FreeOper X).o = DenOp(o, X)
by MSAFREE:def 12,def 13;
A13: p is Element of Args(o, Free(S,X)) by A1,INSTALG1:1;
reconsider t = Sym(o,X)-tree p as Term of S,X;
the Sorts of A is MSSubset of Free(S,X) by Def6; then
A14: (the Sorts of A).s c= (the Sorts of Free(S,X)).s by PBOOLE:def 2,def 18;
A15: the_sort_of t = the_result_sort_of o &
FreeSort(X,s) = (the Sorts of Free(S,X)).s
by A1,MSATERM:20,MSAFREE:def 11; then
A16: s = the_result_sort_of o by A11,A14,MSATERM:def 5;
A17: Den(o,Free(S,X)).p in (the Sorts of A).the_result_sort_of o
by A11,A12,A1,A15,A14,MSATERM:def 5; then
A18: p in Args(o,A) & Den(o,A).p = Den(o,Free(S,X)).p
by A13,Def8;
reconsider q = p as Element of Args(o, A) by A17,A13,Def8;
reconsider p0 = p as Element of Args(o, Free(S,X)) by A1,INSTALG1:1;
A19: dom q = dom the_arity_of o & dom(f#p0) = dom the_arity_of o &
Args(o,A) = product ((the Sorts of A)*the_arity_of o) &
dom ((the Sorts of A)*the_arity_of o) = dom the_arity_of o
by MSUALG_3:6,PRALG_2:3;
now
let i be Nat; assume
A20: i in dom the_arity_of o; then
A21: (the_arity_of o)/.i = (the_arity_of o).i & p0.i in rng p
by A19,FUNCT_1:def 3,PARTFUN1:def 6;
A22: p0.i in ((the Sorts of A)*the_arity_of o).i by A19,A20,CARD_3:9; then
A23: p0.i in (the Sorts of A).((the_arity_of o).i) by A20,FUNCT_1:13;
p0.i is Element of (the Sorts of A).((the_arity_of o)/.i)
by A21,A22,A20,FUNCT_1:13;
then p0.i is Term of S,X by Th42;
hence q.i = (f.((the_arity_of o)/.i)).(p0.i) by A10,A21,A23;
end; then
f#p0 = q by A19,MSUALG_3:24;
hence thesis by A16,A12,A1,A18,Def10,MSUALG_3:def 7;
end;
A24: for t being Term of S,X holds P[t] from MSATERM:sch 1(A3,A9);
thus f is_epimorphism Free(S,X),A
proof
thus f is_homomorphism Free(S,X), A by Def10;
let x; assume x in the carrier of S; then
reconsider s = x as SortSymbol of S;
thus rng(f.x) c= (the Sorts of A).x;
let y be object; assume
y in (the Sorts of A).x; then
reconsider t = y as Element of (the Sorts of A).s;
t is Term of S,X by Th42; then
A25: f.s.t = t by A24;
the Sorts of A is MSSubset of Free(S,X) by Def6; then
(the Sorts of A).s c= (the Sorts of Free(S,X)).s
by PBOOLE:def 2,def 18; then
t in (the Sorts of Free(S,X)).s & dom(f.s) = (the Sorts of Free(S,X)).s
by FUNCT_2:def 1;
hence thesis by A25,FUNCT_1:def 3;
end;
let s be SortSymbol of S;
let t be Element of (the Sorts of A).s;
t is Term of S,X by Th42;
hence f.s.t = t by A24;
end;
theorem Th48:
(canonical_homomorphism A2)**(canonical_homomorphism A2)
= canonical_homomorphism A2
proof set A = A2;
set f = canonical_homomorphism A;
now
let x be object; assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
the Sorts of A is MSSubset of Free(S,X) by Def6;
then
the Sorts of A c= the Sorts of Free(S,X) &
dom (f**f) = the carrier of S by PARTFUN1:def 2,PBOOLE:def 18;
then
A1: (f**f).s = (f.s)*(f.s) & dom (f.s) = (the Sorts of Free(S,X)).s &
rng (f.s) c= (the Sorts of A).s &
(the Sorts of A).s c= (the Sorts of Free(S,X)).s
by PBOOLE:def 19,FUNCT_2:def 1;
then
A2: dom ((f**f).s) = (the Sorts of Free(S,X)).s by XBOOLE_1:1,RELAT_1:27;
now let y be object; assume
A3: y in (the Sorts of Free(S,X)).s;
then
A4: f.s.y in (the Sorts of A).s by FUNCT_2:5;
thus (f**f).s.y = f.s.(f.s.y) by A1,A3,FUNCT_1:13 .= f.s.y by A4,Th47;
end;
hence (f**f).x = f.x by A1,A2;
end;
hence thesis;
end;
theorem
A is Free(S,X)-Image
proof
now
take B = A;
FreeGen X is ManySortedSubset of the Sorts of A by Def7; then
FreeGen X is free & id FreeGen X is ManySortedFunction of FreeGen X,
the Sorts of A by Th22; then
consider f being ManySortedFunction of FreeMSA(X), A such that
A1: f is_homomorphism FreeMSA(X), A & f||FreeGen X = id FreeGen X;
A2: Free(S,X) = FreeMSA X by MSAFREE3:31;
reconsider f0 = f as ManySortedFunction of Free(S,X), B by MSAFREE3:31;
take f0;
thus
A3: f0 is_homomorphism Free(S,X),B by A1,MSAFREE3:31;
reconsider C = the MSAlgebra of B as strict non-empty MSSubAlgebra of A
by MSUALG_2:5;
the Sorts of C = f0.:.:the Sorts of Free(S,X)
proof
defpred P[set] means
for s being SortSymbol of S st $1 in (the Sorts of C).s
holds $1 in (f0.:.:the Sorts of Free(S,X)).s & f0.s.$1 = $1;
A4: for s being SortSymbol of S, v being Element of X.s
holds P[root-tree [v,s]]
proof
let s be SortSymbol of S;
let v be Element of X.s;
reconsider t = root-tree [v,s] as Term of S,X by MSATERM:4;
let r be SortSymbol of S; assume
A5: root-tree [v,s] in (the Sorts of C).r;
the Sorts of C is MSSubset of Free(S,X) by Def6; then
(the Sorts of C).r c= (the Sorts of Free(S,X)).r
by PBOOLE:def 2,def 18; then
root-tree [v,s] in (FreeSort X).r by A5,A2; then
root-tree [v,s] in FreeSort(X, r) by MSAFREE:def 11; then
A6: the_sort_of t = r & s = the_sort_of t by MSATERM:def 5,14;
root-tree [v,s] in FreeGen(s, X) by MSAFREE:def 15; then
A7: root-tree [v,s] in (FreeGen X).s by MSAFREE:def 16;
A8: (f0.:.:the Sorts of Free(S,X)).s
= (f0.s).:((the Sorts of Free(S,X)).s) by PBOOLE:def 20;
A9: (id FreeGen X).s = id ((FreeGen X).s) by MSUALG_3:def 1;
(f.s)|((FreeGen X).s).root-tree [v,s] = (f.s).root-tree [v,s]
by A7,FUNCT_1:49; then
A10: (f.s).root-tree [v,s] = (id((FreeGen X).s)).root-tree [v,s]
by A1,A9,MSAFREE:def 1 .= root-tree [v,s] by A7,FUNCT_1:18;
FreeGen X is MSSubset of Free(S,X) by MSAFREE3:31; then
(FreeGen X).s c= (the Sorts of Free(S,X)).s &
dom (f0.s) = (the Sorts of Free(S,X)).s
by FUNCT_2:def 1,PBOOLE:def 2,def 18;
hence thesis by A6,A8,A7,A10,FUNCT_1:def 6;
end;
A11: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) st
for t being Term of S,X st t in rng p holds P[t]
holds P[[o,the carrier of S]-tree p]
proof
let o be OperSymbol of S;
let p be ArgumentSeq of Sym(o,X);
assume
A12: for t being Term of S,X st t in rng p holds P[t];
let s be SortSymbol of S;
assume
A13: [o,the carrier of S]-tree p in (the Sorts of C).s;
Sym(o,X) ==> roots p & p is FinSequence of TS DTConMSA X
by MSATERM:def 1,21; then
A14: DenOp(o, X).p = Sym(o,X)-tree p & (FreeOper X).o = DenOp(o, X)
by MSAFREE:def 12,def 13;
A15: p is Element of Args(o, Free(S,X)) by A2,INSTALG1:1;
reconsider t = Sym(o,X)-tree p as Term of S,X;
the Sorts of C is MSSubset of Free(S,X) by Def6; then
A16: (the Sorts of C).s c= (the Sorts of Free(S,X)).s
by PBOOLE:def 2,def 18;
A17: the_sort_of t = the_result_sort_of o &
FreeSort(X,s) = (the Sorts of Free(S,X)).s
by A2,MSATERM:20,MSAFREE:def 11; then
A18: s = the_result_sort_of o by A13,A16,MSATERM:def 5;
A19: Den(o,Free(S,X)).p in (the Sorts of A).the_result_sort_of o
by A13,A14,A2,A17,A16,MSATERM:def 5; then
A20: p in Args(o,A) & Den(o,A).p = Den(o,Free(S,X)).p by A15,Def8;
reconsider q = p as Element of Args(o, A) by A19,A15,Def8;
reconsider p0 = p as Element of Args(o, Free(S,X)) by A2,INSTALG1:1;
A21: dom q = dom the_arity_of o & dom(f0#p0) = dom the_arity_of o &
Args(o,A) = product ((the Sorts of A)*the_arity_of o) &
dom ((the Sorts of A)*the_arity_of o) = dom the_arity_of o
by MSUALG_3:6,PRALG_2:3;
now
let i; assume
A22: i in dom the_arity_of o; then
A23: (the_arity_of o)/.i = (the_arity_of o).i & p0.i in rng p
by A21,FUNCT_1:def 3,PARTFUN1:def 6;
A24: p0.i in ((the Sorts of A)*the_arity_of o).i by A21,A22
,CARD_3:9; then
A25: p0.i in (the Sorts of A).((the_arity_of o).i) by A22,FUNCT_1:13;
p0.i is Element of (the Sorts of A).((the_arity_of o)/.i)
by A23,A24,A22,FUNCT_1:13;
then p0.i is Term of S,X by Th42;
hence q.i = (f0.((the_arity_of o)/.i)).(p0.i) by A12,A23,A25;
end; then
A26: f0#p0 = q by A21,MSUALG_3:24; then
A27: f0.(the_result_sort_of o).(Den(o,Free(S,X)).p) = Den(o,A).p
by A3;
A28: (f0.:.:the Sorts of Free(S,X)).s
= (f0.s).:((the Sorts of Free(S,X)).s) by PBOOLE:def 20;
dom(f0.s) = (the Sorts of Free(S,X)).s &
[o,the carrier of S]-tree p in (the Sorts of Free(S,X)).s &
f0.s.([o,the carrier of S]-tree p) = [o,the carrier of S]-tree p
by A14,A2,A16,A27,A18,A13,A15,Def8,FUNCT_2:def 1;
hence [o,the carrier of S]-tree p in (f0.:.:the Sorts of Free(S,X)).s
by A28,FUNCT_1:def 6;
thus thesis by A18,A14,A2,A20,A26,A1;
end;
A29: for t being Term of S,X holds P[t] from MSATERM:sch 1(A4,A11);
now
thus the Sorts of C c= f0.:.:the Sorts of Free(S,X)
proof
let x be object; assume x in the carrier of S; then
reconsider s = x as SortSymbol of S;
let y be object; assume y in (the Sorts of C).x; then
reconsider t = y as Element of (the Sorts of C).s;
t is Term of S,X by Th42;
hence thesis by A29;
end;
f0.:.:the Sorts of Free(S,X) is ManySortedSubset of the Sorts of C
by EQUATION:7;
hence f0.:.:the Sorts of Free(S,X) c= the Sorts of C
by PBOOLE:def 18;
end;
hence the Sorts of C = f0.:.:the Sorts of Free(S,X) by PBOOLE:146;
end;
hence the MSAlgebra of A = Image f0 by A3,MSUALG_3:def 12;
end;
hence thesis;
end;
begin :: Satisfiability
theorem
for A being non-empty MSAlgebra over S
for s being SortSymbol of S
for t being Element of TermAlg S,s
holds A |= t '=' t;
theorem
for A being non-empty MSAlgebra over S
for s being SortSymbol of S
for t1,t2 being Element of TermAlg S,s
holds A |= t1 '=' t2 implies A |= t2 '=' t1;
theorem
for A being non-empty MSAlgebra over S
for s being SortSymbol of S
for t1,t2,t3 being Element of TermAlg S,s
holds A |= t1 '=' t2 & A |= t2 '=' t3 implies A |= t1 '=' t3
proof
let A be non-empty MSAlgebra over S;
let s be SortSymbol of S;
let t1,t2,t3 be Element of TermAlg S,s;
assume
A1: A |= t1 '=' t2 & A |= t2 '=' t3;
let h be ManySortedFunction of TermAlg S, A such that
A2: h is_homomorphism TermAlg S, A;
h.s.t1 = h.s.t2 & h.s.t2 = h.s.t3 by A1,A2;
hence thesis;
end;
theorem
for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for a1,a2 being FinSequence
st a1 in Args(o,TermAlg S) & a2 in Args(o,TermAlg S) &
for i being Nat st i in dom the_arity_of o
for s being SortSymbol of S st s = (the_arity_of o).i
for t1,t2 being Element of TermAlg S, s st t1 = a1.i & t2 = a2.i
holds A |= t1 '=' t2
for t1,t2 being Element of TermAlg S, the_result_sort_of o
st t1 = [o,the carrier of S]-tree a1 & t2 = [o,the carrier of S]-tree a2
holds A |= t1 '=' t2
proof
let A be non-empty MSAlgebra over S;
let o be OperSymbol of S;
let a1,a2 be FinSequence;
assume A1: a1 in Args(o,TermAlg S);
assume A2: a2 in Args(o,TermAlg S); then
reconsider b1 = a1, b2 = a2 as Element of Args(o,TermAlg S) by A1;
assume A3: for i being Nat st i in dom the_arity_of o
for s being SortSymbol of S st s = (the_arity_of o).i
for t1,t2 being Element of TermAlg S, s st t1 = a1.i & t2 = a2.i
holds A |= t1 '=' t2;
set s = the_result_sort_of o;
let t1,t2 be Element of TermAlg S, s;
assume A4: t1 = [o,the carrier of S]-tree a1;
assume A5: t2 = [o,the carrier of S]-tree a2;
let h be ManySortedFunction of TermAlg S, A;
assume
A6: h is_homomorphism TermAlg S, A;
A7: now
let n be Nat; assume
A8: n in dom b1;
A9: dom b1 = dom the_arity_of o & dom b2 = dom the_arity_of o by MSUALG_3:6;
reconsider s = (the_arity_of o).n as SortSymbol of S
by A8,A9,FUNCT_1:102;
dom ((the Sorts of TermAlg S) * (the_arity_of o)) =dom the_arity_of o &
((the Sorts of TermAlg S) * (the_arity_of o)).n
= (the Sorts of TermAlg S).s by A8,A9,FUNCT_1:13,PRALG_2:3; then
reconsider t1 = a1.n, t2 = a2.n as Element of TermAlg S, s
by A8,A9,MSUALG_3:6;
h.s.(t1 '=' t2)`1 = h.s.(t1 '=' t2)`2 by A3,A8,A9,A6,EQUATION:def 5; then
A10: h.s.t1 = h.s.(t1 '=' t2)`2 .= h.s.t2;
A11: s = (the_arity_of o)/.n by A8,A9,PARTFUN1:def 6;
thus (h#b2).n
= (h.((the_arity_of o)/.n)).(b1.n) by A10,A11,A8,A9,MSUALG_3:def 6;
end;
thus h.s.(t1 '=' t2)`1
= h.s.(Den(o,TermAlg S).a1) by A1,A4,INSTALG1:3
.= Den(o, A).(h#b1) by A6
.= Den(o, A).(h#b2) by A7,MSUALG_3:def 6
.= h.s.(Den(o,TermAlg S).a2) by A6
.= h.s.(t1 '=' t2)`2 by A2,A5,INSTALG1:3;
end;
definition
let S;
let T be EqualSet of S;
let A be MSAlgebra over S;
attr A is T-satisfying means: Def11: A |= T;
end;
registration
let S;
let T be EqualSet of S;
cluster T-satisfying non-empty trivial for MSAlgebra over S;
existence
proof
set A = the non-empty trivial MSAlgebra over S;
take A;
thus A |= T by Th32;
thus thesis;
end;
end;
registration
let S;
let T be EqualSet of S;
let A be T-satisfying non-empty MSAlgebra over S;
cluster A-Image -> T-satisfying for non-empty MSAlgebra over S;
coherence
by Def11,Th36;
end;
definition
let S;
let A be MSAlgebra over S;
let T be EqualSet of S;
let G be GeneratorSet of A;
attr G is T-free means
for B be T-satisfying non-empty MSAlgebra over S
for f be ManySortedFunction of G, the Sorts of B
ex h be ManySortedFunction of A, B st
h is_homomorphism A,B & h || G = f;
end;
definition
let S;
let T be EqualSet of S;
let A be MSAlgebra over S;
attr A is T-free means
ex G being GeneratorSet of A st G is T-free;
end;
definition
let S;
let A be MSAlgebra over S;
func Equations(S,A) -> EqualSet of S means: Def14:
for s being SortSymbol of S holds
it.s = {e where e is Element of (Equations S).s: A |= e};
existence
proof
deffunc X(SortSymbol of S)
= {e where e is Element of (Equations S).$1: A |= e};
consider f being ManySortedSet of S such that
A1: for s being SortSymbol of S holds f.s = X(s) from PBOOLE:sch 5;
f is EqualSet of S
proof
let x be object; assume x in the carrier of S; then
reconsider s = x as SortSymbol of S;
A2: f.s = X(s) by A1;
let y be object; assume y in f.x; then
ex e being Element of (Equations S).s st y = e & A |= e by A2;
hence thesis;
end;
hence thesis by A1;
end;
uniqueness
proof
let f1,f2 be EqualSet of S such that
A3: for s being SortSymbol of S holds
f1.s = {e where e is Element of (Equations S).s: A |= e} and
A4: for s being SortSymbol of S holds
f2.s = {e where e is Element of (Equations S).s: A |= e};
now
let x be object; assume x in the carrier of S; then
reconsider s = x as SortSymbol of S;
thus f1.x = {e where e is Element of (Equations S).s: A |= e} by A3
.= f2.x by A4;
end;
hence thesis;
end;
end;
theorem Th54:
for A being MSAlgebra over S
holds A |= Equations(S,A)
proof
let A be MSAlgebra over S;
let s be SortSymbol of S;
let r be Element of (Equations S).s;
assume r in Equations(S,A).s; then
r in {e where e is Element of (Equations S).s: A |= e} by Def14; then
consider e being Element of (Equations S).s such that
A1: r = e & A |= e;
thus thesis by A1;
end;
registration
let S;
let A be non-empty MSAlgebra over S;
cluster -> Equations(S,A)-satisfying for A-Image MSAlgebra over S;
coherence
proof
let B be A-Image MSAlgebra over S;
A is Equations(S,A)-satisfying
by Th54;
hence thesis;
end;
end;
begin :: Term correspondence
scheme TermDefEx{ S()-> non empty non void ManySortedSign,
X()-> non-empty ManySortedSet of S(),
R(set,set)->set, F(set,set)->set}:
ex F being ManySortedSet of S()-Terms X() st
(for s being SortSymbol of S(), x being Element of X().s holds
F.root-tree [x,s] = R(x,s)) &
for o being OperSymbol of S(), p being ArgumentSeq of Sym(o,X()) holds
F.(Sym(o,X())-tree p) = F(o,F*p)
proof
defpred Q[DecoratedTree,Function] means dom $2 = Subtrees $1 &
(for s being SortSymbol of S(), x being Element of X().s
st root-tree [x,s] in Subtrees $1 holds $2.root-tree [x,s] = R(x,s)) &
for o being OperSymbol of S(), p being ArgumentSeq of Sym(o,X())
st Sym(o,X())-tree p in Subtrees $1
holds $2.(Sym(o,X())-tree p) = F(o,$2*p);
defpred P[DecoratedTree] means ex f being Function st Q[$1,f];
A1: for t1,t2 being Term of S(),X()
for f1,f2 being Function st Q[t1,f1] & Q[t2,f2] holds f1 tolerates f2
proof
let t1,t2 be Term of S(),X();
let f1,f2 be Function; assume
A2: Q[t1,f1] & Q[t2,f2];
let x be object; assume x in dom f1 /\ dom f2;
then
A3: x in Subtrees t1 & x in Subtrees t2 by A2,XBOOLE_0:def 4;
then
A4: ex r being Element of dom t1 st x = t1|r;
defpred R[DecoratedTree] means $1 in Subtrees t1 & $1 in Subtrees t2
implies f1.$1 = f2.$1;
A5: for s being SortSymbol of S(), v being Element of X().s
holds R[root-tree [v,s]]
proof
let s be SortSymbol of S(), x be Element of X().s;
assume
A6: root-tree [x,s] in Subtrees t1 & root-tree [x,s] in Subtrees t2;
then f1.root-tree [x,s] = R(x,s) by A2;
hence thesis by A6,A2;
end;
A7: for o being OperSymbol of S(), p being ArgumentSeq of Sym(o,X()) st
for t being Term of S(),X() st t in rng p holds R[t]
holds R[[o,the carrier of S()]-tree p]
proof
let o be OperSymbol of S(), p be ArgumentSeq of Sym(o,X()) such that
A8: for t being Term of S(),X() st t in rng p holds R[t];
set t = [o,the carrier of S()]-tree p;
assume
A9: t in Subtrees t1 & t in Subtrees t2;
rng p c= Subtrees t1
proof
let x be object; assume
A10: x in rng p;
then consider y being object such that
A11: y in dom p & x = p.y by FUNCT_1:def 3;
reconsider y as Nat by A11;
consider n being Nat such that
A12: y = 1+n by A11,FINSEQ_3:25,NAT_1:10;
reconsider n as Element of NAT by ORDINAL1:def 12;
rng p c= S()-Terms X() by FINSEQ_1:def 4;
then reconsider tn = p.y as Term of S(),X() by A11,A10;
reconsider q = {} as Element of dom tn by TREES_1:22;
consider r being Element of dom t1 such that
A13: t = t1|r by A9;
n+1 <= len p by A11,A12,FINSEQ_3:25;
then n < len p & <*n*>^q = <*n*> by NAT_1:13,FINSEQ_1:34;
then t|<*n*> = x & <*n*> in dom t by A11,A12,TREES_4:def 4,11;
then x in Subtrees t & Subtrees t c= Subtrees t1 by A13,TREES_9:13;
hence x in Subtrees t1;
end;
then
A14: dom(f1*p) = dom p by A2,RELAT_1:27;
rng p c= Subtrees t2
proof
let x be object; assume
A15: x in rng p;
then consider y being object such that
A16: y in dom p & x = p.y by FUNCT_1:def 3;
reconsider y as Nat by A16;
consider n being Nat such that
A17: y = 1+n by A16,FINSEQ_3:25,NAT_1:10;
reconsider n as Element of NAT by ORDINAL1:def 12;
rng p c= S()-Terms X() by FINSEQ_1:def 4;
then reconsider tn = p.y as Term of S(),X() by A16,A15;
reconsider q = {} as Element of dom tn by TREES_1:22;
consider r being Element of dom t2 such that
A18: t = t2|r by A9;
n+1 <= len p by A16,A17,FINSEQ_3:25;
then n < len p & <*n*>^q = <*n*> by NAT_1:13,FINSEQ_1:34;
then t|<*n*> = x & <*n*> in dom t by A16,A17,TREES_4:def 4,11;
then x in Subtrees t & Subtrees t c= Subtrees t2 by A18,TREES_9:13;
hence x in Subtrees t2;
end;
then
A19: dom(f2*p) = dom p by A2,RELAT_1:27;
now let x be object; assume
A20: x in dom p;
then
A21: p.x in rng p by FUNCT_1:def 3;
rng p c= S()-Terms X() by FINSEQ_1:def 4;
then reconsider w = p.x as Term of S(),X() by A21;
A22: R[w] by A8,A21;
reconsider y = x as Nat by A20;
consider n being Nat such that
A23: y = 1+n by A20,FINSEQ_3:25,NAT_1:10;
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider q = {} as Element of dom w by TREES_1:22;
consider r1 being Element of dom t1 such that
A24: t = t1|r1 by A9;
consider r2 being Element of dom t2 such that
A25: t = t2|r2 by A9;
n+1 <= len p by A20,A23,FINSEQ_3:25;
then n < len p & <*n*>^q = <*n*> by NAT_1:13,FINSEQ_1:34;
then t|<*n*> = w & <*n*> in dom t by A23,TREES_4:def 4,11;
then w in Subtrees t & Subtrees t c= Subtrees t2 &
Subtrees t c= Subtrees t1 by A24,A25,TREES_9:13;
hence (f1*p).x = f2.w by A20,A22,FUNCT_1:13 .= (f2*p).x
by A20,FUNCT_1:13;
end;
then f1*p = f2*p by A14,A19;
hence f1.t = F(o,f2*p) by A2,A9 .= f2.t by A2,A9;
end;
for t being Term of S(),X() holds R[t] from MSATERM:sch 1(A5,A7);
hence thesis by A3,A4;
end;
A26: for s being SortSymbol of S(), v being Element of X().s
holds P[root-tree [v,s]]
proof
let s be SortSymbol of S(), x be Element of X().s;
A27: Subtrees root-tree [x,s] = {root-tree [x,s]} by Th2;
take f = {root-tree [x,s]}-->R(x,s);
thus dom f = Subtrees root-tree [x,s] by A27;
hereby let s1 be SortSymbol of S(), x1 be Element of X().s1;
assume
A28: root-tree [x1,s1] in Subtrees root-tree [x,s];
then root-tree [x1,s1] = root-tree [x,s] by A27,TARSKI:def 1;
then [x1,s1] = [x,s] by TREES_4:4;
then x1 = x & s1 = s by XTUPLE_0:1;
hence f.root-tree [x1,s1] = R(x1,s1) by A27,A28,FUNCOP_1:7;
end;
let o be OperSymbol of S(), p be ArgumentSeq of Sym(o,X());
assume Sym(o,X())-tree p in Subtrees root-tree [x,s];
then Sym(o,X())-tree p = root-tree [x,s] by A27,TARSKI:def 1;
then Sym(o,X()) = [x,s] by TREES_4:17;
then s = the carrier of S() & s in the carrier of S() by XTUPLE_0:1;
hence thesis;
end;
A29: for o being OperSymbol of S(), p being ArgumentSeq of Sym(o,X()) st
for t being Term of S(),X() 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,X())such that
A30: for t be Term of S(),X() st t in rng p holds P[t];
defpred W[object,object] means
ex f being Function, t being Term of S(),X()
st t = p.$1 & $2 = f & Q[t,f];
A31: for x being object st x in dom p ex y being object st W[x,y]
proof
let x be object; assume x in dom p;
then
A32: p.x in rng p & rng p c= S()-Terms X() by FUNCT_1:def 3,FINSEQ_1:def 4;
then reconsider t = p.x as Term of S(),X();
consider f being Function such that
A33: Q[t,f] by A30,A32;
take f,f,t;
thus thesis by A33;
end;
consider g being Function such that
A34: dom g = dom p & for x being object st x in dom p holds W[x,g.x]
from CLASSES1:sch 1(A31);
A35: now
thus rng g is functional
proof
let y be object; assume y in rng g;
then consider x being object such that
A36: x in dom g & y = g.x by FUNCT_1:def 3;
W[x,y] by A34,A36;
hence thesis;
end;
let x,y be Function; assume
A37: x in rng g & y in rng g;
then consider x0 being object such that
A38: x0 in dom g & x = g.x0 by FUNCT_1:def 3;
consider y0 being object such that
A39: y0 in dom g & y = g.y0 by A37,FUNCT_1:def 3;
W[x0,x] & W[y0,y] by A34,A38,A39;
hence x tolerates y by A1;
end;
then reconsider f1 = union rng g as Function by PARTFUN1:78;
set t = [o,the carrier of S()]-tree p;
set f = f1+*({t}-->F(o,f1*p));
take f;
defpred S[object,object] means ex I be set st I = $1 & $2 = proj1 I;
A40: for x,y,z being object st S[x,y] & S[x,z] holds y = z;
consider Y being set such that
A41: for x being object holds
x in Y iff ex y be object st y in rng g & S[y,x] from TARSKI:sch 1(A40);
A42: dom f1 = union Y
proof
thus dom f1 c= union Y
proof
let x be object; assume x in dom f1;
then [x,f1.x] in f1 by FUNCT_1:1;
then consider Z being set such that
A43: [x,f1.x] in Z & Z in rng g by TARSKI:def 4;
x in proj1 Z & proj1 Z in Y by A43,A41,XTUPLE_0:def 12;
hence thesis by TARSKI:def 4;
end;
let z be object; assume z in union Y;
then consider Z being set such that
A44: z in Z & Z in Y by TARSKI:def 4;
consider y be object such that
A45: y in rng g & ex I being set st I = y & Z = proj1 I by A44,A41;
reconsider y as Function by A45,A35;
[z,y.z] in y by A44,A45,FUNCT_1:1;
then [z,y.z] in f1 by A45,TARSKI:def 4;
hence thesis by FUNCT_1:1;
end;
A46: dom f = dom f1 \/ dom({Sym(o,X())-tree p}-->F(o,f1*p)) by FUNCT_4:def 1
.= dom f1 \/ {Sym(o,X())-tree p};
dom f1 misses dom ({t}-->F(o,f1*p))
proof
set x = the Element of dom f1 /\ dom ({t}-->F(o,f1*p));
assume dom f1 /\ dom ({t}-->F(o,f1*p)) <> {};
then
A47: x in dom f1 & x in dom ({t}-->F(o,f1*p)) by XBOOLE_0:def 4;
then [x,f1.x] in f1 by FUNCT_1:1;
then consider Y being set such that
A48: [x,f1.x] in Y & Y in rng g by TARSKI:def 4;
consider y being object such that
A49: y in dom g & Y = g.y by A48,FUNCT_1:def 3;
A50: W[y,Y] by A34,A49;
then reconsider t1 = p.y as Term of S(),X();
x in Subtrees t1 & t1 in rng p
by A34,A49,A48,A50,XTUPLE_0:def 12,FUNCT_1:def 3;
then x <> t by Th7;
hence thesis by A47,TARSKI:def 1;
end;
then
A51: f1 c= f by FUNCT_4:28,PARTFUN1:56;
per cases;
suppose
A52: p = {};
then
A53: Subtrees (Sym(o,X())-tree p) = {Sym(o,X())-tree p} by Th4;
dom p = {} by A52;
then rng g = {} by A34,RELAT_1:42;
hence dom f = {} \/ Subtrees t by A53,A46,ZFMISC_1:2 .= Subtrees t;
hereby let s be SortSymbol of S(), x be Element of X().s;
assume root-tree [x,s] in Subtrees t;
then root-tree [x,s] = t by A53,TARSKI:def 1;
then [x,s] = Sym(o,X()) by TREES_4:17;
then s = the carrier of S() & s in the carrier of S() by XTUPLE_0:1;
hence f.root-tree [x,s] = R(x,s);
end;
let o0 be OperSymbol of S(), p0 be ArgumentSeq of Sym(o0,X());
assume Sym(o0,X())-tree p0 in Subtrees t;
then
A54: Sym(o0,X())-tree p0 = t by A53,TARSKI:def 1;
rng p /\ dom f c= dom f1
proof
let z be object; assume z in rng p /\ dom f; then
A55
: z in rng p & rng p c= S()-Terms X() by XBOOLE_0:def 4,FINSEQ_1:def 4;
then reconsider z as Term of S(),X();
consider y being object such that
A56: y in dom p & z = p.y by A55,FUNCT_1:def 3;
W[y,g.y] by A34,A56;
then
A57: z in proj1 (g.y) & g.y in rng g by A34,A56,TREES_9:11,FUNCT_1:def 3;
then proj1 (g.y) in Y by A41;
hence thesis by A42,A57,TARSKI:def 4;
end;
then
A58: f1*p = f*p by A51,ALGSPEC1:2;
Sym(o0,X()) = Sym(o,X()) & p = p0 by A54,TREES_4:15;
then
A59: p0 = p & o0 = o by XTUPLE_0:1;
A60: t in {t} by TARSKI:def 1;
t in dom ({t}-->F(o,f1*p)) by TARSKI:def 1;
hence f.(Sym(o0,X())-tree p0) = ({t}-->F(o,f1*p)).t by A54,FUNCT_4:13
.= F(o0,f*p0) by A58,A59,A60,FUNCOP_1:7;
end;
suppose p <> {};
then reconsider p as non empty DTree-yielding FinSequence;
A61: union Y = Subtrees rng p
proof
thus union Y c= Subtrees rng p
proof
let z be object; assume z in union Y;
then consider W being set such that
A62: z in W & W in Y by TARSKI:def 4;
consider y be object such that
A63: y in rng g & S[y,W] by A62,A41;
consider a being object such that
A64: a in dom g & y = g.a by A63,FUNCT_1:def 3;
reconsider a as Nat by A34,A64;
consider f being Function, t being Term of S(),X() such that
A65: t = p.a & y = f & Q[t,f] by A34,A64;
W = Subtrees t & t in rng p by A34,A63,A64,A65,FUNCT_1:def 3;
then W c= Subtrees rng p by Th8;
hence thesis by A62;
end;
let z be object; assume z in Subtrees rng p;
then consider t being (Element of rng p), q being Element of dom t
such that
A66: z = t|q;
A67: z in Subtrees t by A66;
consider a being object such that
A68: a in dom p & t = p.a by FUNCT_1:def 3;
reconsider a as Nat by A68;
consider f3 being Function, t1 being Term of S(),X() such that
A69: t1 = p.a & g.a = f3 & Q[t1,f3] by A68,A34;
f3 in rng g by A34,A68,A69,FUNCT_1:def 3;
then Subtrees t in Y by A68,A69,A41;
hence thesis by A67,TARSKI:def 4;
end;
dom ({t}-->F(o,f1*p)) = {t};
then dom f = union Y \/ {t} by A42,FUNCT_4:def 1;
hence dom f = Subtrees t by A61,Th3;
hereby let s be SortSymbol of S(), x be Element of X().s;
assume
A70: root-tree [x,s] in Subtrees t;
s in the carrier of S(); then s <> the carrier of S();
then [x,s] <> Sym(o,X()) by XTUPLE_0:1;
then
A71: root-tree [x,s] <> t by TREES_4:17;
then
root-tree [x,s] nin {t} & Subtrees t = {t}\/Subtrees rng p
by Th3,TARSKI:def 1;
then root-tree [x,s] in Subtrees rng p by A70,XBOOLE_0:def 3;
then consider h being (Element of rng p), r being Element of dom h
such that
A72: root-tree [x,s] = h|r;
h in rng p & rng p c= S()-Terms X() by FINSEQ_1:def 4;
then reconsider h as Term of S(),X();
consider f2 being Function such that
A73: Q[h,f2] by A30;
consider a being object such that
A74: a in dom p & h = p.a by FUNCT_1:def 3;
reconsider a as Nat by A74;
consider f3 being Function, t1 being Term of S(),X() such that
A75: t1 = p.a & g.a = f3 & Q[t1,f3] by A74,A34;
A76: f3 = f2 by A73,A74,A75,A1,PARTFUN1:55;
A77: root-tree [x,s] in Subtrees h by A72;
then f2.root-tree [x,s] = R(x,s) by A73;
then [root-tree [x,s], R(x,s)] in f2 & f2 in rng g
by A77,A74,A75,A76,A34,FUNCT_1:1,def 3;
then [root-tree [x,s], R(x,s)] in f1 by TARSKI:def 4;
then f1.root-tree [x,s] = R(x,s) &
root-tree [x,s] nin dom ({t}-->F(o,f1*p))
by A71,TARSKI:def 1,FUNCT_1:1;
hence f.root-tree [x,s] = R(x,s) by FUNCT_4:11;
end;
let o1 be OperSymbol of S(), p1 be ArgumentSeq of Sym(o1,X());
set t1 = Sym(o1,X())-tree p1;
assume Sym(o1,X())-tree p1 in Subtrees t;
then
A78: Sym(o1,X())-tree p1 in {t} \/ Subtrees rng p by Th3;
rng p c= Subtrees rng p & (rng p)/\dom f c= rng p by Th9,XBOOLE_1:17;
then (rng p)/\dom f c= dom f1 by A42,A61;
then
A79: f1*p = f*p by A51,ALGSPEC1:2;
per cases by A78,A61,XBOOLE_0:def 3;
suppose
A80: t1 in {t};
then
t1 = t by TARSKI:def 1;
then
A81: Sym(o,X()) = Sym(o1,X()) & p = p1 by TREES_4:15;
dom({t}-->F(o,f1*p)) = {t};
then
f.t1 = ({t}-->F(o,f1*p)).t1 by A80,FUNCT_4:13
.= F(o,f1*p) by A80,FUNCOP_1:7;
hence f.(Sym(o1,X())-tree p1) = F(o1,f*p1)
by A81,A79,XTUPLE_0:1;
end;
suppose t1 in union Y;
then consider W being set such that
A82: t1 in W & W in Y by TARSKI:def 4;
consider y be object such that
A83: y in rng g & S[y,W] by A41,A82;
consider z being object such that
A84: z in dom g & y = g.z by A83,FUNCT_1:def 3;
reconsider z as Nat by A34,A84;
consider f2 being Function, t2 be Term of S(),X() such that
A85: t2 = p.z & y = f2 & Q[t2,f2] by A34,A84;
A86: f2.t1 = F(o1,f2*p1) by A85,A82,A83;
A87: rng p1 c= Subtrees t1 & (rng p1)/\dom f c= rng p1
by XBOOLE_1:17,Th11;
Subtrees t1 c= Subtrees t2 by A82,A83,A85,Th12;
then
A88: rng p1 c= dom f2 by A87,A85;
f2 c= f1 by A83,A85,ZFMISC_1:74;
then
A89: (rng p1)/\dom f c= dom f2 & f2 c= f by A51,A87,A88;
thus f.(Sym(o1,X())-tree p1) = f2.t1 by A82,A83,A89,A85,FOMODEL0:51
.= F(o1,f*p1) by A86,A89,ALGSPEC1:2;
end;
end;
end;
A90: for t being Term of S(),X() holds P[t] from MSATERM:sch 1(A26,A29);
defpred G[object,object] means
ex t being Term of S(),X(),f being Function st
t = $1 & f = $2 & Q[t,f];
A91: for x being object st x in S()-Terms X() ex y being object st G[x,y]
proof
let x be object; assume x in S()-Terms X();
then reconsider t = x as Term of S(),X();
P[t] by A90;
hence thesis;
end;
consider F being Function such that
A92: dom F = S()-Terms X() &
for x being object st x in S()-Terms X() holds G[x,F.x]
from CLASSES1:sch 1(A91);
rng F is functional compatible
proof
thus rng F is functional
proof
let x be object; assume x in rng F;
then consider x0 being object such that
A93: x0 in dom F & x = F.x0 by FUNCT_1:def 3;
G[x0,x] by A92,A93;
hence thesis;
end;
let h1,h2 be Function; assume
A94: h1 in rng F & h2 in rng F;
then consider x0 being object such that
A95: x0 in dom F & h1 = F.x0 by FUNCT_1:def 3;
consider y0 being object such that
A96: y0 in dom F & h2 = F.y0 by A94,FUNCT_1:def 3;
G[x0,h1] & G[y0,h2] by A92,A95,A96;
hence h1 tolerates h2 by A1;
end;
then reconsider rF = rng F as non empty functional compatible set
by A92,RELAT_1:42;
reconsider f = union rF as Function;
dom f = S()-Terms X()
proof
A97: dom f = union the set of all dom h where h is Element of rF
by COMPUT_1:12;
thus dom f c= S()-Terms X()
proof
let x be object; assume x in dom f;
then consider W being set such that
A98: x in W & W in the set of all dom h where h is Element of rF
by A97,TARSKI:def 4;
consider h being Element of rF such that
A99: W = dom h by A98;
consider x0 being object such that
A100: x0 in dom F & h = F.x0 by FUNCT_1:def 3;
reconsider x0 as Term of S(),X() by A92,A100;
G[x0,h] by A92,A100;
then x is Term of S(),X() by A98,A99,Th10;
hence thesis;
end;
let x be object; assume x in S()-Terms X();
then reconsider x as Term of S(),X();
consider t being Term of S(),X(), h be Function such that
A101: t = x & h = F.x & Q[t,h] by A92;
reconsider h as Element of rF by A92,A101,FUNCT_1:def 3;
x in dom h & dom h in the set of all dom g where g is Element of rF
by A101,TREES_9:11;
hence thesis by A97,TARSKI:def 4;
end;
then reconsider f as ManySortedSet of S()-Terms X()
by PARTFUN1:def 2,RELAT_1:def 18;
take f;
hereby let s be SortSymbol of S(), x be Element of X().s;
reconsider t = root-tree [x,s] as Term of S(),X() by MSATERM:4;
G[t,F.t] by A92;
then consider g being Function such that
A102: g = F.t & Q[t,g];
g in rF by A92,A102,FUNCT_1:def 3;
then
A103: g c= f by ZFMISC_1:74;
t in dom g by A102,TREES_9:11;
hence f.root-tree [x,s] = g.t by A103,FOMODEL0:51
.= R(x,s) by A102,TREES_9:11;
end;
let o be OperSymbol of S(), p be ArgumentSeq of Sym(o,X());
reconsider t = Sym(o,X())-tree p as Term of S(),X();
G[t,F.t] by A92;
then consider g being Function such that
A104: g = F.t & Q[t,g];
A105: g in rF by A92,A104,FUNCT_1:def 3;
then
A106: g c= f by ZFMISC_1:74;
A107: t in dom g by A104,TREES_9:11;
rng p c= Subtrees t & (rng p)/\ dom f c= rng p by Th11,XBOOLE_1:17;
then (rng p)/\ dom f c= dom g by A104;
then
A108: g*p = f*p by A105,ZFMISC_1:74,ALGSPEC1:2;
thus f.(Sym(o,X())-tree p) = g.t by A106,A107,FOMODEL0:51
.= F(o,f*p) by A104,TREES_9:11,A108;
end;
scheme TermDefUniq{ S()-> non empty non void ManySortedSign,
X()-> non-empty ManySortedSet of S(),
R(set,set)->set, F(set,FinSequence)->set,
F1,F2()->ManySortedSet of S()-Terms X()}:
F1() = F2()
provided
A1: (for s being SortSymbol of S(), x being Element of X().s holds
F1().root-tree [x,s] = R(x,s)) and
A2: for o being OperSymbol of S(), p being ArgumentSeq of Sym(o,X()) holds
F1().(Sym(o,X())-tree p) = F(o,F1()*p) and
A3: (for s being SortSymbol of S(), x being Element of X().s holds
F2().root-tree [x,s] = R(x,s)) and
A4: for o being OperSymbol of S(), p being ArgumentSeq of Sym(o,X()) holds
F2().(Sym(o,X())-tree p) = F(o,F2()*p)
proof
defpred P[object] means F1().$1 = F2().$1;
A5: for s being SortSymbol of S(), x being Element of X().s holds
P[root-tree[x,s]]
proof
let s be SortSymbol of S();
let x be Element of X().s;
thus F1().root-tree[x,s] = R(x,s) by A1
.= F2().root-tree[x,s] by A3;
end;
A6: for o being OperSymbol of S(), p being ArgumentSeq of Sym(o,X())
st for t being Term of S(),X() st t in rng p holds P[t]
holds P[[o,the carrier of S()]-tree p]
proof
let o be OperSymbol of S();
let p be ArgumentSeq of Sym(o,X()); assume
A7: for t being Term of S(),X() st t in rng p holds P[t];
A8: dom (F1()*p) = dom p & dom (F2()*p) = dom p
by PARTFUN1:def 2;
now
let x be object; assume
A9: x in dom p; then reconsider i = x as Element of NAT;
reconsider t = p.i as Term of S(),X() by A9,MSATERM:22;
t in rng p by A9,FUNCT_1:def 3; then
P[t] by A7;
hence (F1()*p).x = F2().t by A9,FUNCT_1:13
.= (F2()*p).x by A9,FUNCT_1:13;
end; then
F1()*p = F2()*p by A8;
hence F1().([o, the carrier of S()]-tree p) = F(o,F2()*p) by A2
.= F2().([o, the carrier of S()]-tree p) by A4;
end;
A10: for t being Term of S(),X() holds P[t] from MSATERM:sch 1(A5,A6);
for x being object st x in S()-Terms X() holds P[x] by A10;
hence thesis;
end;
definition
let S, X;
let w be ManySortedFunction of X, (the carrier of S) --> NAT;
let t be Function such that
A1: t is Element of Free(S,X);
deffunc R(set,set) = root-tree [w.$2.$1,$2];
deffunc F(OperSymbol of S,FinSequence) =
Sym($1,(the carrier of S)-->NAT)-tree($2);
func #(t,w) -> Element of TermAlg S means: Def15:
ex F being ManySortedSet of S-Terms X st it = F.t &
(for s being SortSymbol of S, x being Element of X.s holds
F.root-tree [x,s] = root-tree [w.s.x,s]) &
for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds
F.(Sym(o,X)-tree p) = Sym(o,(the carrier of S)-->NAT)-tree(F*p);
existence
proof
consider F being ManySortedSet of S-Terms X such that
A2: for s being SortSymbol of S, x being Element of X.s holds
F.root-tree [x,s] = R(x,s) and
A3: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds
F.(Sym(o,X)-tree p) = F(o,F*p) from TermDefEx;
set Y = (the carrier of S)-->NAT;
defpred P[set] means
ex t being Term of S,Y, q being Term of S,X st t = F.$1 & q = $1 &
the_sort_of t = the_sort_of q;
A4: now let s be SortSymbol of S;
let x be Element of X.s;
A5: w.s.x in NAT & F.root-tree [x,s] = R(x,s) by A2; then
reconsider t = F.root-tree [x,s] as Term of S,Y by MSATERM:4;
reconsider q = root-tree [x,s] as Term of S,X by MSATERM:4;
thus P[root-tree [x,s]]
proof
take t, q;
the_sort_of t = s by A5,MSATERM:14;
hence thesis by MSATERM:14;
end;
end;
A6: now let o be OperSymbol of S;
let p be ArgumentSeq of Sym(o,X); assume
A7: for t being Term of S,X st t in rng p holds P[t];
A8: dom (F*p) = dom p & dom p = dom the_arity_of o
by MSATERM:22,PARTFUN1:def 2;
now let i be Nat;
assume
A9: i in dom p; then
reconsider q = p.i as Term of S,X by PARTFUN1:4;
A10: (F*p).i = F.(p.i) & p.i in rng p & p.i in S-Terms X
by A9,FUNCT_1:def 3,13,PARTFUN1:4; then
A11: P[p.i] by A7; then
reconsider t = (F*p).i as Term of S,Y
by A9,FUNCT_1:13;
reconsider q = p.i as Term of S,X by A9,PARTFUN1:4;
take t;
thus t = (F*p).i;
thus the_sort_of t = (the_arity_of o).i by A9,A10,A11,MSATERM:23;
end; then
reconsider Fp = F*p as ArgumentSeq of Sym(o,Y) by A8,MSATERM:24;
reconsider q = Sym(o,X)-tree p as Term of S,X;
reconsider t = Sym(o,Y)-tree Fp as Term of S,Y;
thus P[[o, the carrier of S]-tree p]
proof
take t,q;
thus t = F.([o, the carrier of S]-tree (p)) &
q = [o, the carrier of S]-tree p by A3;
A12: q.{} = Sym(o,X) by TREES_4:def 4;
t.{} = Sym(o,Y) by TREES_4:def 4;
hence the_sort_of t = the_result_sort_of o by MSATERM:17
.= the_sort_of q by A12,MSATERM:17;
end;
end;
A13: for t being Term of S,X holds P[t] from MSATERM:sch 1(A4,A6);
t is Term of S,X by A1,Th42;
then consider tt being Term of S,Y, q being Term of S,X such that
A14: tt = F.t & q = t & the_sort_of tt = the_sort_of q by A13;
reconsider Ft = F.t as Element of TermAlg S by A14,MSATERM:13;
take Ft, F;
thus thesis by A2,A3;
end;
uniqueness
proof
let t1,t2 being Element of TermAlg S;
given F1 being ManySortedSet of S-Terms X such that
A15: t1 = F1.t and
A16: (for s being SortSymbol of S, x being Element of X.s holds
F1.root-tree [x,s] = R(x,s)) and
A17: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds
F1.(Sym(o,X)-tree p) = F(o,F1*p);
given F2 being ManySortedSet of S-Terms X such that
A18: t2 = F2.t and
A19: (for s being SortSymbol of S, x being Element of X.s holds
F2.root-tree [x,s] = R(x,s)) and
A20: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds
F2.(Sym(o,X)-tree p) = F(o,F2*p);
F1 = F2 from TermDefUniq(A16,A17,A19,A20);
hence thesis by A15,A18;
end;
end;
theorem Th55:
for w being ManySortedFunction of X, (the carrier of S) --> NAT
for F being ManySortedSet of S-Terms X st
(for s being SortSymbol of S, x being Element of X.s holds
F.root-tree [x,s] = root-tree [w.s.x,s]) &
for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds
F.(Sym(o,X)-tree p) = Sym(o,(the carrier of S)-->NAT)-tree(F*p)
holds
for t being Element of Free(S,X) holds F.t = #(t,w)
proof
let w be ManySortedFunction of X, (the carrier of S) --> NAT;
deffunc R(set,set) = root-tree [w.$2.$1,$2];
deffunc F(OperSymbol of S,FinSequence)
= Sym($1,(the carrier of S)-->NAT)-tree($2);
let F be ManySortedSet of S-Terms X such that
A1: (for s being SortSymbol of S, x being Element of X.s holds
F.root-tree [x,s] = R(x,s)) and
A2: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds
F.(Sym(o,X)-tree p) = F(o,F*p);
let t be Element of Free(S,X);
consider G being ManySortedSet of S-Terms X such that
A3: #(t,w) = G.t and
A4: (for s being SortSymbol of S, x being Element of X.s holds
G.root-tree [x,s] = R(x,s)) and
A5: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds
G.(Sym(o,X)-tree p) = F(o,G*p) by Def15;
F = G from TermDefUniq(A1,A2,A4,A5);
hence F.t = #(t,w) by A3;
end;
registration
let S, X;
let G be non-empty MSSubset of Free(S,X);
let s be SortSymbol of S;
cluster -> Relation-like Function-like for Element of G.s;
coherence
proof
let x be Element of G.s;
G.s c= (the Sorts of Free(S,X)).s & x in G.s by PBOOLE:def 2,def 18;
hence thesis;
end;
end;
theorem Th56:
for w being ManySortedFunction of X, (the carrier of S) --> NAT
ex h being ManySortedFunction of Free(S,X), TermAlg S st
h is_homomorphism Free(S,X), TermAlg S &
for s being SortSymbol of S, t being Element of Free(S,X),s
holds #(t,w) = h.s.t
proof
let w be ManySortedFunction of X, (the carrier of S) --> NAT;
A1: TermAlg S = Free(S, (the carrier of S)-->NAT) by MSAFREE3:31;
reconsider G = FreeGen X as non-empty GeneratorSet of Free(S,X)
by MSAFREE3:31;
deffunc F(SortSymbol of S,Element of G.$1)
= root-tree [w.$1.($2.{})`1, $1];
A2: for s being SortSymbol of S, x being Element of G.s holds
F(s,x) in (the Sorts of TermAlg S).s
proof
let s be SortSymbol of S, x be Element of G.s;
G.s = FreeGen(s,X) by MSAFREE:def 16;
then consider y such that
A3: y in X.s & x = root-tree [y,s] by MSAFREE:def 15;
x .{} = [y,s] by A3,TREES_4:3;
then reconsider x1 = (x .{})`1 as Element of X.s by A3;
A4: w.s.x1 in ((the carrier of S)-->NAT).s;
then reconsider t = F(s,x) as Term of S, (the carrier of S)-->NAT
by MSATERM:4;
t in FreeSort((the carrier of S)-->NAT, the_sort_of t) by MSATERM:def 5;
then t in FreeSort((the carrier of S)-->NAT,s) by A4;
hence thesis by MSAFREE:def 11;
end;
consider f being ManySortedFunction of G, the Sorts of TermAlg S such that
A5: for s being SortSymbol of S for x being Element of G.s holds f.s.x = F(s,x)
from Sch2(A2);
FreeGen X is free & FreeMSA X = Free(S, X) by MSAFREE3:31;
then consider h being ManySortedFunction of Free(S,X), TermAlg S such that
A6: h is_homomorphism Free(S,X), TermAlg S & h||G = f;
set t = the Element of Free(S, X);
consider F being ManySortedSet of S-Terms X such that
A7: #(t,w) = F.t &
(for s being SortSymbol of S, x being Element of X.s holds
F.root-tree [x,s] = root-tree [w.s.x,s]) &
for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds
F.(Sym(o,X)-tree p) = Sym(o,(the carrier of S)-->NAT)-tree(F*p) by Def15;
take h; thus h is_homomorphism Free(S,X), TermAlg S by A6;
let s be SortSymbol of S, t be Element of Free(S,X),s;
defpred P[DecoratedTree] means
for s being SortSymbol of S
st $1 in (the Sorts of Free(S,X)).s holds #($1,w) = h.s.$1;
A8: for s being SortSymbol of S, x being Element of X.s
holds P[root-tree [x,s]]
proof
let s be SortSymbol of S, x be Element of X.s;
reconsider t = root-tree [x,s] as Term of S,X by MSATERM:4;
let s1 be SortSymbol of S;
assume root-tree [x,s] in (the Sorts of Free(S,X)).s1;
then t in (the Sorts of FreeMSA X).s1 by MSAFREE3:31;
then s = the_sort_of t & t in FreeSort(X, s1)
by MSAFREE:def 11,MSATERM:14;
then
A9: s = s1 by MSATERM:def 5;
t in FreeGen(s,X) by MSAFREE:def 15;
then reconsider q = t as Element of G.s by MSAFREE:def 16;
t is Element of FreeMSA X by MSATERM:13;
then t is Element of Free(S,X) by MSAFREE3:31;
hence #(root-tree [x,s],w) = F.t by A7,Th55
.= root-tree [w.s.x,s] by A7
.= root-tree [w.s.[x,s]`1,s]
.= F(s,q) by TREES_4:3
.= f.s.t by A5
.= ((h.s)|(G.s)).q by A6,MSAFREE:def 1
.= h.s1.(root-tree [x,s]) by A9,FUNCT_1:49;
end;
A10: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) st
for t being Term of S,X st t in rng p holds P[t]
holds P[[o,the carrier of S]-tree p]
proof
let o be OperSymbol of S;
let p be ArgumentSeq of Sym(o,X) such that
A11: for t being Term of S,X st t in rng p holds P[t];
let s be SortSymbol of S;
reconsider t = Sym(o,X)-tree p as Term of S,X;
assume [o, the carrier of S]-tree p in (the Sorts of Free(S,X)).s;
then t in (the Sorts of FreeMSA X).s by MSAFREE3:31;
then t in FreeSort(X,s) by MSAFREE:def 11;
then the_sort_of t = s & t.{} = Sym(o,X) by TREES_4:def 4,MSATERM:def 5;
then
A12: s = the_result_sort_of o by MSATERM:17;
FreeMSA X = Free(S,X) by MSAFREE3:31;
then reconsider q = p as Element of Args(o,Free(S,X)) by INSTALG1:1;
rng p c= dom F
proof
let y be object; assume y in rng p;
then consider x being object such that
A13: x in dom p & y = p.x by FUNCT_1:def 3;
reconsider x as Nat by A13;
p.x is Term of S,X & dom F = S-Terms X
by A13,MSATERM:22,PARTFUN1:def 2;
hence thesis by A13;
end; then
A14: dom(F*p) = dom p & dom(h#q) = dom the_arity_of o &
dom q = dom the_arity_of o by RELAT_1:27,MSUALG_3:6;
now
let x be object; assume
A15: x in dom p;
then reconsider i = x as Nat;
reconsider t = p.i as Term of S,X by A15,MSATERM:22;
t is Element of FreeMSA X by MSATERM:13;
then reconsider u = t as Element of Free(S,X) by MSAFREE3:31;
reconsider s = (the_arity_of o)/.i as SortSymbol of S;
A16: t in rng p by A15,FUNCT_1:def 3;
the_sort_of t = s by A15,MSATERM:23;
then t in FreeSort(X,s) by MSATERM:def 5;
then t in (the Sorts of FreeMSA X).s by MSAFREE:def 11;
then
A17: t in (the Sorts of Free(S,X)).s by MSAFREE3:31;
thus (F*p).x = F.t by A15,FUNCT_1:13
.= #(u,w) by A7,Th55
.= h.s.u by A11,A16,A17
.= (h#q).x by A15,MSUALG_3:def 6;
end; then
A18: F*p = h#q by A14;
t is Element of FreeMSA X by MSATERM:13;
then t is Element of Free(S,X) by MSAFREE3:31;
hence #([o, the carrier of S]-tree p, w) = F.t by Th55,A7
.= Sym(o,(the carrier of S)-->NAT)-tree (F*p) by A7
.= Den(o,Free(S,(the carrier of S)-->NAT)).(h#q) by A18,A1,Th13
.= h.s.(Den(o,Free(S,X)).q) by A1,A6,A12
.= h.s.([o, the carrier of S]-tree p) by Th13;
end;
A19: for t being Term of S,X holds P[t] from MSATERM:sch 1(A8,A10);
t is Element of (the Sorts of Free(S,X)).s;
then t is Element of FreeMSA X by MSAFREE3:31;
then t is Term of S,X by MSATERM:13;
hence #(t,w) = h.s.t by A19;
end;
theorem Th57:
for w being ManySortedFunction of X, (the carrier of S) --> NAT
for s being SortSymbol of S, x being Element of X.s
holds #(root-tree [x,s], w) = root-tree [w.s.x, s]
proof
let w be ManySortedFunction of X, (the carrier of S) --> NAT;
let s be SortSymbol of S, x be Element of X.s;
reconsider t = root-tree [x,s] as Term of S,X by MSATERM:4;
deffunc R(set,set) = root-tree [w.$2.$1,$2];
deffunc F(OperSymbol of S,FinSequence)
= Sym($1,(the carrier of S)-->NAT)-tree($2);
S-Terms X = Union the Sorts of FreeMSA X by MSATERM:13;
then t is Element of Free(S,X) by MSAFREE3:31;
then consider G being ManySortedSet of S-Terms X such that
A1: #(t,w) = G.t and
A2: (for s being SortSymbol of S, x being Element of X.s holds
G.root-tree [x,s] = R(x,s)) and
for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds
G.(Sym(o,X)-tree p) = F(o,G*p) by Def15;
thus #(root-tree [x,s], w) = root-tree [w.s.x, s] by A1,A2;
end;
theorem Th58:
for w being ManySortedFunction of X, (the carrier of S) --> NAT
for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X)
for q being FinSequence st dom q = dom p &
for i being Nat, t being Element of Free(S,X) st i in dom p & t = p.i
holds q.i = #(t,w)
holds #(Sym(o,X)-tree p, w) = Sym(o,(the carrier of S)-->NAT)-tree q
proof
let w be ManySortedFunction of X, (the carrier of S) --> NAT;
let o be OperSymbol of S, p be ArgumentSeq of Sym(o,X);
let q be FinSequence such that
A1: dom q = dom p and
A2: for i being Nat, t being Element of Free(S,X) st i in dom p & t = p.i
holds q.i = #(t,w);
reconsider t = Sym(o,X)-tree p as Term of S,X;
deffunc R(set,set) = root-tree [w.$2.$1,$2];
deffunc F(OperSymbol of S,FinSequence)
= Sym($1,(the carrier of S)-->NAT)-tree($2);
A3: S-Terms X = Union the Sorts of FreeMSA X by MSATERM:13;
then t is Element of Free(S,X) by MSAFREE3:31;
then consider G being ManySortedSet of S-Terms X such that
A4: #(t,w) = G.t and
A5: (for s being SortSymbol of S, x being Element of X.s holds
G.root-tree [x,s] = R(x,s)) and
A6: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds
G.(Sym(o,X)-tree p) = F(o,G*p) by Def15;
rng p c= dom G
proof
let y be object; assume y in rng p;
then consider x being object such that
A7: x in dom p & y = p.x by FUNCT_1:def 3;
reconsider x as Nat by A7;
y is Term of S, X by A7,MSATERM:22;
then y in S-Terms X;
hence thesis by PARTFUN1:def 2;
end;
then
A8: dom (G*p) = dom p by RELAT_1:27;
now
let x be object; assume
A9: x in dom p;
then reconsider i = x as Nat;
reconsider t = p.i as Term of S,X by A9,MSATERM:22;
reconsider t as Element of Free(S,X) by A3,MSAFREE3:31;
thus q.x = #(t,w) by A2,A9 .= G.t by A5,A6,Th55
.= (G*p).x by A9,FUNCT_1:13;
end;
then q = G*p by A1,A8;
hence #(Sym(o,X)-tree p, w) = Sym(o,(the carrier of S)-->NAT)-tree q
by A4,A6;
end;
theorem Th59:
for Y being ManySortedSubset of X
holds Free(S,Y) is MSSubAlgebra of Free(S,X)
proof
let Y be ManySortedSubset of X;
thus
A1: the Sorts of Free(S,Y) c= the Sorts of Free(S,X)
proof
let x be object; assume
x in the carrier of S;
then reconsider s = x as SortSymbol of S;
let z be object; assume
A2: z in (the Sorts of Free(S,Y)).x;
then reconsider t = z as Element of (the Sorts of Free(S,Y)).x;
A3: t in S-Terms(Y,Y(\/)((the carrier of S)-->{0})).s by A2,MSAFREE3:24;
then reconsider t1 = t as Term of S,Y(\/)((the carrier of S)-->{0})
by MSAFREE3:16;
A4: t = t1 & the_sort_of t1 = x & variables_in t1 c= Y by A3,MSAFREE3:17;
A5: Y c= X by PBOOLE:def 18;
Y(\/)((the carrier of S)-->{0}) c= X(\/)((the carrier of S)-->{0})
by PBOOLE:18,def 18;
then reconsider t2 = t1 as Term of S, X(\/)((the carrier of S)-->{0})
by MSATERM:26;
variables_in t2 = S variables_in t2 by MSAFREE3:def 4
.= variables_in t1 by MSAFREE3:def 4;
then variables_in t2 c= X & the_sort_of t2 = the_sort_of t1
by A4,A5,PBOOLE:13,MSAFREE3:29;
then t2 in {t3 where t3 is Term of S,X(\/)((the carrier of S)-->{0}):
the_sort_of t3 = s & variables_in t3 c= X} by A4;
then t2 in S-Terms(X,X(\/)((the carrier of S)-->{0})).s
by MSAFREE3:def 5;
hence z in (the Sorts of Free(S,X)).x by MSAFREE3:24;
end;
let B be MSSubset of Free(S,X); assume
A6: B = the Sorts of Free(S,Y);
consider A1 being MSSubset of FreeMSA(Y (\/) ((the carrier of S) --> {0}))
such that
A7: Free(S,Y) = GenMSAlg A1 &
A1 = (Reverse (Y (\/)((the carrier of S) --> {0})))""Y by MSAFREE3:def 1;
thus
A8: B is opers_closed
proof
let o be OperSymbol of S;
let z be object;
assume z in rng ((Den(o,Free(S,X)))|((B# * the Arity of S).o ));
then consider a being object such that
A9: a in dom ((Den(o,Free(S,X)))|((B# * the Arity of S).o )) &
z = ((Den(o,Free(S,X)))|((B# * the Arity of S).o )).a by FUNCT_1:def 3;
A10: a in dom (Den(o,Free(S,X))) /\ ((B# * the Arity of S).o )
by A9,RELAT_1:61;
then
A11: a in dom (Den(o,Free(S,X))) & a in (B# * the Arity of S).o
by XBOOLE_0:def 4;
reconsider a as Element of Args(o,Free(S,X)) by A10;
A12: (B# * the Arity of S).o = (B# ).the_arity_of o by FUNCT_2:15;
A13: (B# ).the_arity_of o = product (B*the_arity_of o) by FINSEQ_2:def 5;
A14
: Args(o,Free(S,X)) = product ((the Sorts of Free(S,X))*(the_arity_of o)) &
dom ((the Sorts of Free(S,X))*(the_arity_of o)) = dom (the_arity_of o) &
Args(o,Free(S,Y)) = product ((the Sorts of Free(S,Y))*(the_arity_of o)) &
dom ((the Sorts of Free(S,Y))*(the_arity_of o)) = dom (the_arity_of o)
by PRALG_2:3;
then
A15: dom a = dom the_arity_of o by PARTFUN1:def 2;
z = Den(o,Free(S,X)).a by A9,A11,FUNCT_1:49;
then
A16: z = Sym(o,X)-tree a by Th13;
A17: for x being object
st x in dom ((the Sorts of Free(S,Y))*(the_arity_of o))
holds a.x in ((the Sorts of Free(S,Y))*(the_arity_of o)).x
by A11,A12,A13,A6,CARD_3:9;
then
A18: a in Args(o,Free(S,Y)) by A14,A15,CARD_3:9;
A19: Den(o,Free(S,Y)).a = [o,the carrier of S]-tree a
by A17,A14,A15,CARD_3:9,Th13;
thus z in (B * the ResultSort of S).o
by A6,A16,A18,A19,FUNCT_2:5,MSUALG_6:def 1;
end;
now
let o be OperSymbol of S;
set Z = Y (\/) ((the carrier of S) --> {0});
reconsider A2 = the Sorts of Free(S,Y) as MSSubset of FreeMSA Z
by A7,MSUALG_2:def 9;
A20: A2 is_closed_on o by A7,MSUALG_2:def 6,def 9;
Free(S,Z) = FreeMSA Z by MSAFREE3:31;
then
A21: Args(o,Free(S,Y)) c= Args(o,Free(S,Z)) &
dom(Den(o,Free(S,Z))) = Args(o,Free(S,Z))
by A7,FUNCT_2:def 1,MSAFREE3:37;
then
A22: dom (Den(o,Free(S,Z))| Args(o,Free(S,Y))) = Args(o,Free(S,Y))
by RELAT_1:62;
A23: Args(o,Free(S,Y)) c= Args(o,Free(S,X))
proof
let x be object; assume x in Args(o,Free(S,Y)); then
A24: x in product ((the Sorts of Free(S,Y))*the_arity_of o) &
dom ((the Sorts of Free(S,Y))*the_arity_of o) = dom the_arity_of o &
dom ((the Sorts of Free(S,X))*the_arity_of o) = dom the_arity_of o
by PRALG_2:3;
then consider f being Function such that
A25: x = f & dom f = dom the_arity_of o &
for y being object st y in dom the_arity_of o
holds f.y in ((the Sorts of Free(S,Y))*the_arity_of o).y
by CARD_3:def 5;
now
let y be object; assume
A26: y in dom the_arity_of o;
f.y in ((the Sorts of Free(S,Y))*the_arity_of o).y &
(the_arity_of o).y in the carrier of S by A25,A26,FUNCT_1:102;
then f.y in (the Sorts of Free(S,Y)).((the_arity_of o).y) &
(the Sorts of Free(S,Y)).((the_arity_of o).y) c=
(the Sorts of Free(S,X)).((the_arity_of o).y)
by A1,A26,FUNCT_1:13;
then f.y in (the Sorts of Free(S,X)).((the_arity_of o).y);
hence f.y in ((the Sorts of Free(S,X))*the_arity_of o).y
by A26,FUNCT_1:13;
end;
then x in product ((the Sorts of Free(S,X))*the_arity_of o)
by A25,A24,CARD_3:def 5;
hence x in Args(o,Free(S,X)) by PRALG_2:3;
end;
dom(Den(o,Free(S,X))) = Args(o,Free(S,X))
by FUNCT_2:def 1;
then
A27: dom (Den(o,Free(S,X))| Args(o,Free(S,Y))) = Args(o,Free(S,Y))
by A23,RELAT_1:62;
A28: now let x be object; assume
A29: x in Args(o,Free(S,Y));
then
A30: x in product ((the Sorts of Free(S,Y))*the_arity_of o) by PRALG_2:3;
reconsider p = x as Element of
product ((the Sorts of Free(S,Y))*the_arity_of o) by A29,PRALG_2:3;
dom p = dom ((the Sorts of Free(S,Y))*the_arity_of o) &
rng the_arity_of o c= the carrier of S &
dom the Sorts of Free(S,Y) = the carrier of S
by A30,CARD_3:9,PARTFUN1:def 2;
then dom p = dom the_arity_of o by RELAT_1:27;
then dom p = Seg len the_arity_of o by FINSEQ_1:def 3;
then reconsider p = x as FinSequence by FINSEQ_1:def 2;
A31: (Den(o,Free(S,X))| Args(o,Free(S,Y))).x = Den(o,Free(S,X)).x
by A29,FUNCT_1:49
.= [o, the carrier of S]-tree p by A23,A29,Th13;
thus (Den(o,Free(S,Z))| Args(o,Free(S,Y))).x
= Den(o,Free(S,Z)).x by A29,FUNCT_1:49
.= (Den(o,Free(S,X))| Args(o,Free(S,Y))).x by A21,A29,A31,Th13;
end;
thus (the Charact of Free(S,Y)).o
= Opers(FreeMSA Z,A2).o by A7,MSUALG_2:def 9
.= o/.A2 by MSUALG_2:def 8
.= Den(o,FreeMSA Z)| ((A2# * the Arity of S).o) by A20,MSUALG_2:def 7
.= Den(o,Free(S,Z))| ((A2# * the Arity of S).o) by MSAFREE3:31
.= (Den(o,Free(S,X))) | ((B# * the Arity of S).o)
by A6,A28,A27,A22
.= o/.B by A8,MSUALG_2:def 7;
end;
hence the Charact of Free(S,Y) = Opers(Free(S,X),B) by A6,MSUALG_2:def 8;
end;
theorem Th60:
for w being ManySortedFunction of X, (the carrier of S)-->NAT
for t being Term of S,X
holds #(t,w) is Element of Free(S, rngs w), the_sort_of t &
#(t,w) is Element of TermAlg S, the_sort_of t
proof
let w be ManySortedFunction of X, (the carrier of S)-->NAT;
let t be Term of S,X;
defpred P[DecoratedTree] means ex t being Term of S,X st
$1 = t & #(t,w) is Element of Free(S, rngs w), the_sort_of t;
A1: for s being SortSymbol of S, x being Element of X.s
holds P[root-tree [x,s]]
proof
let s be SortSymbol of S, x be Element of X.s;
reconsider t = root-tree [x,s] as Term of S,X by MSATERM:4;
take t; thus root-tree [x,s] = t;
S-Terms X = Union the Sorts of FreeMSA X by MSATERM:13;
then t is Element of Free(S,X) by MSAFREE3:31;
then consider F being ManySortedSet of S-Terms X such that
A2: #(t,w) = F.t &
(for s being SortSymbol of S, x being Element of X.s holds
F.root-tree [x,s] = root-tree [w.s.x,s]) &
for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds
F.(Sym(o,X)-tree p) = Sym(o,(the carrier of S)-->NAT)-tree(F*p) by Def15;
A3: #(t,w) = root-tree [w.s.x,s] by A2;
dom w = the carrier of S by PARTFUN1:def 2;
then rng (w.s) = (rngs w).s by FUNCT_6:22;
then
A4: w.s.x in (rngs w).s by FUNCT_2:4;
then reconsider tw = #(t,w) as Term of S, rngs w by A3,MSATERM:4;
the_sort_of tw = s & the_sort_of t = s by A3,A4,MSATERM:14;
then tw in FreeSort (rngs w, the_sort_of t) by MSATERM:def 5;
then tw in (the Sorts of FreeMSA rngs w).the_sort_of t by MSAFREE:def 11;
hence thesis by MSAFREE3:31;
thus thesis;
end;
A5: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) st
for t being Term of S,X 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,X) such that
A6: for t being Term of S,X st t in rng p holds P[t];
take tt = Sym(o,X)-tree p;
thus tt = [o,the carrier of S]-tree p;
S-Terms X = Union the Sorts of FreeMSA X by MSATERM:13;
then tt is Element of Free(S,X) by MSAFREE3:31;
then consider F being ManySortedSet of S-Terms X such that
A7: #(tt,w) = F.tt &
(for s being SortSymbol of S, x being Element of X.s holds
F.root-tree [x,s] = root-tree [w.s.x,s]) &
for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds
F.(Sym(o,X)-tree p) = Sym(o,(the carrier of S)-->NAT)-tree(F*p) by Def15;
A8: #(tt,w) = Sym(o,(the carrier of S)-->NAT)-tree(F*p) by A7;
A9: Args(o,Free(S,rngs w))
= product ((the Sorts of Free(S,rngs w))*the_arity_of o) &
dom((the Sorts of Free(S,rngs w))*the_arity_of o) = dom the_arity_of o
by PRALG_2:3;
p is Element of Args(o,FreeMSA X) by INSTALG1:1;
then p is Element of Args(o,Free(S,X)) &
Args(o,Free(S,X)) = product ((the Sorts of Free(S,X))*the_arity_of o)
by PRALG_2:3,MSAFREE3:31;
then
A10: p in product ((the Sorts of Free(S,X))*the_arity_of o) &
dom((the Sorts of Free(S,X))*the_arity_of o) = dom the_arity_of o
by PRALG_2:3;
then
A11: dom p = dom the_arity_of o by CARD_3:9;
A12: dom F = S-Terms X by PARTFUN1:def 2
.= Union the Sorts of FreeMSA X by MSATERM:13
.= Union the Sorts of Free(S,X) by MSAFREE3:31;
A13: rng p c= Union the Sorts of Free(S,X)
proof let y be object; assume y in rng p;
then consider x being object such that
A14: x in dom p & y = p.x by FUNCT_1:def 3;
y in ((the Sorts of Free(S,X))*the_arity_of o).x by A10,A14,A11
,CARD_3:9;
then y in (the Sorts of Free(S,X)).((the_arity_of o).x) &
(the_arity_of o).x in the carrier of S &
dom the Sorts of Free(S,X) = the carrier of S
by A14,A11,FUNCT_1:13,102,PARTFUN1:def 2;
hence thesis by CARD_5:2;
end;
then
A15: dom (F*p) = dom p by A12,RELAT_1:27
.= dom the_arity_of o by A10,CARD_3:9;
A16: now
let y be object; assume
A17: y in dom the_arity_of o;
then
A18: p.y in rng p by A11,FUNCT_1:def 3;
p.y is Element of FreeMSA X by A18,A13,MSAFREE3:31;
then reconsider t = p.y as Term of S,X by MSAFREE3:6;
A19: P[t] & F.t = #(t,w) by A7,A6,A18,A13,Th55;
reconsider i = y as Nat by A17;
(the_arity_of o).i = the_sort_of t by A11,A17,MSATERM:23;
then F.t in (the Sorts of Free(S,rngs w)).((the_arity_of o).i) by A19;
then F.t in ((the Sorts of Free(S,rngs w))*the_arity_of o).i
by A17,FUNCT_1:13;
hence (F*p).y in ((the Sorts of Free(S,rngs w))*the_arity_of o).y
by A11,A17,FUNCT_1:13;
end;
Den(o,Free(S,rngs w)).(F*p) = [o,the carrier of S]-tree (F*p)
by A16,A9,A15,CARD_3:9,Th13;
then [o,the carrier of S]-tree (F*p) in Result(o,Free(S,rngs w)) &
dom the ResultSort of S = the carrier' of S
by A16,A9,A15,CARD_3:9,FUNCT_2:5,def 1;
then #(tt,w) in ((the Sorts of Free(S,rngs w)).the_result_sort_of o) &
tt.{} = Sym(o,X) by A8,FUNCT_1:13,TREES_4:def 4;
hence thesis by MSATERM:17;
end;
for t being Term of S,X holds P[t] from MSATERM:sch 1(A1,A5);
then P[t];
hence #(t,w) is Element of Free(S, rngs w), the_sort_of t;
then
A20: #(t,w) in (the Sorts of Free(S, rngs w)).the_sort_of t;
X is_transformable_to (the carrier of S)-->NAT by Th21;
then rngs w is ManySortedSubset of (the carrier of S)-->NAT
by PBOOLE:def 18,MSSUBFAM:17;
then Free(S, rngs w) is MSSubAlgebra of Free(S, (the carrier of S)-->NAT)
by Th59;
then the Sorts of Free(S, rngs w) is MSSubset of
Free(S, (the carrier of S)-->NAT) by MSUALG_2:def 9;
then the Sorts of Free(S, rngs w) is MSSubset of TermAlg S by MSAFREE3:31;
then (the Sorts of Free(S, rngs w)).the_sort_of t c=
(the Sorts of TermAlg S).the_sort_of t by PBOOLE:def 2,def 18;
hence thesis by A20;
end;
theorem
for w being ManySortedFunction of X, (the carrier of S) --> NAT
for F being ManySortedSet of S-Terms X st
(for s being SortSymbol of S, x being Element of X.s holds
F.root-tree [x,s] = root-tree [w.s.x,s]) &
for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds
F.(Sym(o,X)-tree p) = Sym(o,(the carrier of S)-->NAT)-tree(F*p)
for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds
F*p in Args(o, Free(S, rngs w)) &
F*p in Args(o, Free(S, (the carrier of S)-->NAT))
proof
let w be ManySortedFunction of X, (the carrier of S) --> NAT;
deffunc R(set,set) = root-tree [w.$2.$1,$2];
deffunc F(OperSymbol of S,FinSequence)
= Sym($1,(the carrier of S)-->NAT)-tree($2);
let F be ManySortedSet of S-Terms X such that
A1: (for s being SortSymbol of S, x being Element of X.s holds
F.root-tree [x,s] = R(x,s)) and
A2: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) holds
F.(Sym(o,X)-tree p) = F(o,F*p);
let o be OperSymbol of S, p be ArgumentSeq of Sym(o,X);
rng p c= dom F
proof
let y be object; assume y in rng p;
then consider x being object such that
A3: x in dom p & y = p.x by FUNCT_1:def 3;
reconsider x as Nat by A3;
y is Term of S, X by A3,MSATERM:22;
then y in S-Terms X;
hence thesis by PARTFUN1:def 2;
end;
then
A4: dom (F*p) = dom p by RELAT_1:27;
A5: dom p = dom the_arity_of o by MSATERM:22;
A6: S-Terms X = Union the Sorts of FreeMSA X by MSATERM:13
.= Union the Sorts of Free(S,X) by MSAFREE3:31;
X is_transformable_to (the carrier of S)-->NAT by Th21;
then rngs w is ManySortedSubset of (the carrier of S)-->NAT
by PBOOLE:def 18,MSSUBFAM:17;
then
A7: Free(S, rngs w) is MSSubAlgebra of Free(S, (the carrier of S)-->NAT)
by Th59;
now
let i be Nat;
assume
A8: i in dom p;
then reconsider t = p.i as Term of S,X by MSATERM:22;
F.t = #(t,w) by A1,A2,A6,Th55;
then reconsider tt = F.t as Element of (the Sorts of Free(S, rngs w)).
the_sort_of t by Th60;
A9: the Sorts of Free(S, rngs w) is MSSubset of
Free(S, (the carrier of S)-->NAT) by A7,MSUALG_2:def 9;
reconsider tt as Term of S, rngs w by Th42;
take tt; thus tt = (F*p).i by A8,FUNCT_1:13;
(the Sorts of Free(S, rngs w)).the_sort_of t c= (the Sorts of
Free(S, (the carrier of S)-->NAT)).the_sort_of t &
tt in (the Sorts of Free(S,rngs w)).the_sort_of t
by A9,PBOOLE:def 2,def 18;
then tt in (the Sorts of FreeMSA(rngs w)).the_sort_of t
by MSAFREE3:31;
then tt in FreeSort(rngs w,the_sort_of t)
by MSAFREE:def 11;
hence the_sort_of tt = the_sort_of t by MSATERM:def 5
.= (the_arity_of o).i by A8,MSATERM:23;
end;
then F*p is ArgumentSeq of Sym(o, rngs w)
by A4,A5,MSATERM:24;
then F*p is Element of Args(o, FreeMSA(rngs w))
by INSTALG1:1;
then F*p is Element of Args(o, Free(S, rngs w))
by MSAFREE3:31;
then F*p in Args(o, Free(S,rngs w)) & Args(o, Free(S,rngs w)) c=
Args(o, Free(S, (the carrier of S)-->NAT)) by A7,MSAFREE3:37;
hence thesis;
end;
theorem Th62:
for w being ManySortedFunction of (the carrier of S)-->NAT, X
ex h being ManySortedFunction of TermAlg S, A st
h is_homomorphism TermAlg S, A &
for s being SortSymbol of S, i being Nat holds
h.s.root-tree [i,s] = root-tree [w.s.i, s]
proof
set Y = (the carrier of S)-->NAT;
let w be ManySortedFunction of Y, X;
deffunc F(set,Function) = root-tree [w.$1.($2.{})`1, $1];
consider ww being ManySortedFunction of the carrier of S such that
A1: for x st x in the carrier of S holds dom(ww.x) = (FreeGen Y).x &
for y being Element of (FreeGen Y).x holds ww.x .y = F(x,y) from Sch1;
A2: ww is ManySortedFunction of FreeGen Y, FreeGen X
proof
let x be object; assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
A3: dom(ww.s) = (FreeGen Y).s by A1;
A4: (FreeGen X).s = FreeGen(s,X) & (FreeGen Y).s = FreeGen(s,Y)
by MSAFREE:def 16;
rng(ww.s) c= (FreeGen X).s
proof
let y be object; assume y in rng(ww.s);
then consider z being object such that
A5: z in dom(ww.s) & y = ww.s.z by FUNCT_1:def 3;
reconsider z as Element of (FreeGen Y).s by A1,A5;
consider v being set such that
A6: v in Y.s & z = root-tree [v,s] by A4,MSAFREE:def 15;
A7: y = F(s,z) by A1,A5;
z.{} = [v,s] by A6,TREES_4:3;
then (z.{})`1 = v;
then w.s.(z.{})`1 in X.s by A6,FUNCT_2:5;
hence thesis by A4,A7,MSAFREE:def 15;
end;
hence thesis by A3,FUNCT_2:2;
end;
reconsider G = FreeGen Y as GeneratorSet of TermAlg S;
FreeGen X is MSSubset of A by Def7;
then reconsider ww as ManySortedFunction of G, the Sorts of A by A2,Th22;
consider h being ManySortedFunction of TermAlg S, A such that
A8: h is_homomorphism TermAlg S, A & ww = h||G by MSAFREE:def 5;
take h; thus h is_homomorphism TermAlg S, A by A8;
let s be SortSymbol of S, i be Nat;
A9: ww.s = (h.s)|(G.s) by A8,MSAFREE:def 1;
i in NAT & NAT = Y.s by ORDINAL1:def 12;
then root-tree [i,s] in FreeGen(s,Y) & FreeGen(s,Y) = G.s
by MSAFREE:def 15,def 16;
then reconsider z = root-tree [i,s] as Element of (FreeGen Y).s;
thus h.s.root-tree [i,s] = ww.s.z by A9,FUNCT_1:49
.= F(s,z) by A1 .= root-tree [w.s.[i,s]`1, s] by TREES_4:3
.= root-tree [w.s.i, s];
end;
theorem Th63:
for w being ManySortedFunction of X, (the carrier of S)-->NAT
ex h being ManySortedFunction of FreeGen X, the Sorts of TermAlg S st
for s being SortSymbol of S, i being Element of X.s holds
h.s.root-tree [i,s] = root-tree [w.s.i, s]
proof
set Y = (the carrier of S)-->NAT;
let w be ManySortedFunction of X, Y;
deffunc F(set,Function) = root-tree [w.$1.($2.{})`1, $1];
consider ww being ManySortedFunction of the carrier of S such that
A1: for x st x in the carrier of S holds dom(ww.x) = (FreeGen X).x &
for y being Element of (FreeGen X).x holds ww.x .y = F(x,y) from Sch1;
A2: ww is ManySortedFunction of FreeGen X, FreeGen Y
proof
let x be object; assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
A3: dom(ww.s) = (FreeGen X).s by A1;
A4: (FreeGen X).s = FreeGen(s,X) & (FreeGen Y).s = FreeGen(s,Y)
by MSAFREE:def 16;
rng(ww.s) c= (FreeGen Y).s
proof
let y be object; assume y in rng(ww.s);
then consider z being object such that
A5: z in dom(ww.s) & y = ww.s.z by FUNCT_1:def 3;
reconsider z as Element of (FreeGen X).s by A1,A5;
consider v being set such that
A6: v in X.s & z = root-tree [v,s] by A4,MSAFREE:def 15;
A7: y = F(s,z) by A1,A5;
z.{} = [v,s] by A6,TREES_4:3;
then (z.{})`1 = v;
then w.s.(z.{})`1 in Y.s by A6,FUNCT_2:5;
hence thesis by A4,A7,MSAFREE:def 15;
end;
hence thesis by A3,FUNCT_2:2;
end;
set A = the all_vars_including inheriting_operations free_in_itself
(X,S)-terms MSAlgebra over S;
reconsider G = FreeGen X as GeneratorSet of A by Th45;
reconsider ww as ManySortedFunction of FreeGen X,
the Sorts of TermAlg S by A2,Th22;
take ww;
let s be SortSymbol of S, i be Element of X.s;
root-tree [i,s] in FreeGen(s,X) & FreeGen(s,X) = G.s
by MSAFREE:def 15,def 16;
then reconsider z = root-tree [i,s] as Element of (FreeGen X).s;
thus ww.s.root-tree [i,s]
= F(s,z) by A1 .= root-tree [w.s.[i,s]`1, s] by TREES_4:3
.= root-tree [w.s.i, s];
end;
begin :: Free algebras
reserve X0 for non-empty countable ManySortedSet of S;
reserve A0 for all_vars_including inheriting_operations free_in_itself
(X0,S)-terms MSAlgebra over S;
theorem
for h being ManySortedFunction of TermAlg S, A0 st
h is_homomorphism TermAlg S, A0
for w being ManySortedFunction of X0, (the carrier of S)-->NAT st w is "1-1"
ex Y being non-empty ManySortedSubset of (the carrier of S)-->NAT,
B being MSSubset of TermAlg S,
ww being ManySortedFunction of Free(S,Y), A0,
g being ManySortedFunction of A0,A0 st
Y = rngs w & B = the Sorts of Free(S,Y) & FreeGen rngs w c= B &
ww is_homomorphism Free(S,Y), A0 & g is_homomorphism A0,A0 & h||B = g**ww &
for s being SortSymbol of S, i being Nat st i in Y.s
ex x being Element of X0.s st w.s.x = i &
ww.s.root-tree [i,s] = root-tree [x, s]
proof set A = A0;
let h be ManySortedFunction of TermAlg S, A such that
A1: h is_homomorphism TermAlg S, A;
let v be ManySortedFunction of X0, (the carrier of S)-->NAT such that
A2: v is "1-1";
set Z = (the carrier of S)-->NAT;
deffunc F(object) = (NAT-->the Element of X0.$1)+*(v.$1)";
consider w being ManySortedSet of S such that
A3: for s being SortSymbol of S holds w.s = F(s) from PBOOLE:sch 5;
w is Function-yielding
proof
let x be object; assume x in dom w;
then w.x = F(x) by A3;
hence thesis;
end;
then reconsider w as ManySortedFunction of the carrier of S;
w is ManySortedFunction of Z,X0
proof
let x be object; assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
dom v = the carrier of S by PARTFUN1:def 2; then
A4: w.x = F(s) & v.s is one-to-one & Z.s = NAT & rng(v.s) c= Z.s
by A2,A3;
then
A5: dom (w.s) = dom(NAT-->the Element of X0.s)\/ dom((v.s)") by FUNCT_4:def 1
.= NAT \/ dom((v.s)")
.= NAT\/rng(v.s) by A4,FUNCT_1:33 .= NAT by XBOOLE_1:12;
rng (w.s) c= X0.s
proof
let x be object; assume x in rng (w.s);
then consider y being object such that
A7: y in dom (w.s) & x = w.s.y by FUNCT_1:def 3;
y in dom ((v.s)") or
y nin dom((v.s)");
then x = ((v.s)").y & y in dom ((v.s)") & dom v = the carrier of S or
x = (NAT-->the Element of X0.s).y
by A4,A7,FUNCT_4:11,13,PARTFUN1:def 2;
then x = (v.s)".y & y in dom ((v.s)") & v.s is one-to-one or
x = the Element of X0.s
by A2,A5,A7,FUNCOP_1:7;
then x in rng ((v.s)") & rng ((v.s)") = dom (v.s) & dom (v.s) c= X0.s
or x in X0.s by FUNCT_1:33,FUNCT_1:def 3;
hence thesis;
end;
hence thesis by A5,FUNCT_2:2;
end;
then reconsider w as ManySortedFunction of Z,X0;
consider ww being ManySortedFunction of TermAlg S, A such that
A8: ww is_homomorphism TermAlg S, A &
for s being SortSymbol of S, i being Nat holds
ww.s.root-tree [i,s] = root-tree [w.s.i, s] by Th62;
A9: dom v = the carrier of S by PARTFUN1:def 2;
rngs v c= Z
proof
let s be object; assume
s in the carrier of S;
then (rngs v).s = rng (v.s) by A9,FUNCT_6:22;
hence (rngs v).s c= Z.s;
end;
then reconsider Y = rngs v as non-empty ManySortedSubset of Z
by PBOOLE:def 18;
take Y;
A10: Free(S,Z) = TermAlg S by MSAFREE3:31;
A11: Free(S,Y) is MSSubAlgebra of Free(S,Z) by Th59;
then reconsider B = the Sorts of Free(S,Y) as MSSubset of TermAlg S
by A10,MSUALG_2:def 9;
take B;
reconsider wB = ww||B as ManySortedFunction of Free(S,Y),A;
take wB;
reconsider G = FreeGen X0 as GeneratorSet of A by Th45;
consider vv being ManySortedFunction of G, the Sorts of TermAlg S such that
A12: for s being SortSymbol of S, i being Element of X0.s holds
vv.s.root-tree [i,s] = root-tree [v.s.i, s] by Th63;
consider g being ManySortedFunction of A,A such that
A13: g is_homomorphism A,A & g||G = h**vv by Def9;
take g;
thus Y = rngs v & B = the Sorts of Free(S,Y);
Free(S,Y) = FreeMSA rngs v by MSAFREE3:31;
hence FreeGen rngs v c= B by PBOOLE:def 18;
thus wB is_homomorphism Free(S,Y), A & g is_homomorphism A,A
by A13,A8,A10,A11,EQUATION:22; then
A14: g**wB is_homomorphism Free(S,Y),A by MSUALG_3:10;
reconsider H = FreeGen Y as GeneratorSet of Free(S,Y) by MSAFREE3:31;
reconsider hB = h||B as ManySortedFunction of Free(S,Y),A;
A15: now
let x be object; assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
A16: dom ((hB||H).s) = H.s & dom (((g**wB)||H).s) = H.s by FUNCT_2:def 1;
now let y be object; assume
A17: y in H.s; then y in FreeGen(s,Y) by MSAFREE:def 16;
then consider z such that
A18: z in Y.s & y = root-tree [z,s] by MSAFREE:def 15;
A19: H.s c= B.s & Y.s c= Z.s by PBOOLE:def 2,def 18;
then
A20: w.s.z in X0.s by A18,FUNCT_2:5;
wB.s = (ww.s)|(B.s) & z in Z.s by A18,A19,MSAFREE:def 1;
then
A21: wB.s.y = ww.s.y & z in NAT by A17,A19,FUNCT_1:49;
then wB.s.y = root-tree[w.s.z,s] by A8,A18;
then wB.s.y in FreeGen(s,X0) by A20,MSAFREE:def 15;
then
A22: wB.s.y in G.s by MSAFREE:def 16;
z in Z.s by A18,A19; then
z in NAT; then
A23: vv.s.(ww.s.y) = vv.s.root-tree [w.s.z, s] by A8,A18
.= root-tree [v.s.(w.s.z), s] by A12,A20
.= root-tree [v.s.(((NAT-->the Element of X0.s)+*((v.s)")).z), s]
by A3;
dom v = the carrier of S by PARTFUN1:def 2;
then
A24: v.s is one-to-one & rng(v.s) = Y.s
by A2,FUNCT_6:22;
A25: z in dom ((v.s)") by A18,A24,FUNCT_1:33;
A26: vv.s.(ww.s.y) = root-tree [v.s.((((v.s)")).z), s]
by A23,A25,FUNCT_4:13
.= y by A18,A24,FUNCT_1:35;
A27: rngs vv c= B
proof
let x be object; assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
let y be object; assume
A28: y in (rngs vv).x;
dom vv = the carrier of S by PARTFUN1:def 2;
then y in rng (vv.s) by A28,FUNCT_6:22;
then consider z being object such that
A29: z in dom(vv.s) & y = vv.s.z by FUNCT_1:def 3;
dom(vv.s) = G.s by FUNCT_2:def 1 .= FreeGen(s,X0) by MSAFREE:def 16;
then consider a being set such that
A30: a in X0.s & z = root-tree[a,s] by A29,MSAFREE:def 15;
v.s.a in rng (v.s) & dom v = the carrier of S
by A30,FUNCT_2:4,PARTFUN1:def 2;
then v.s.a in Y.s & y = root-tree[v.s.a, s] by A29,A30,A12
,FUNCT_6:22;
then y in FreeGen(s,Y) by MSAFREE:def 15;
then y in H.s & H.s c= B.s by MSAFREE:def 16,PBOOLE:def 2,def 18;
hence thesis;
end;
A31: dom (hB**vv) = (the carrier of S)/\the carrier of S
by PARTFUN1:def 2;
A32: dom (g**wB) = (the carrier of S)/\the carrier of S
by PARTFUN1:def 2;
thus (hB||H).x .y = ((hB.s)|(H.s)).y by MSAFREE:def 1
.= hB.s.y by A17,FUNCT_1:49
.= ((hB.s)*(vv.s)).(wB.s.y) by A26,A21,A22,FUNCT_2:15
.= ((hB**vv).s).(wB.s.y) by A31,PBOOLE:def 19
.= (g||G).s.(wB.s.y) by A13,A27,EXTENS_1:11
.= ((g.s)|(G.s)).(wB.s.y) by MSAFREE:def 1
.= g.s.(wB.s.y) by A22,FUNCT_1:49
.= ((g.s)*(wB.s)).y by A19,A17,FUNCT_2:15
.= ((g**wB).s).y by A32,PBOOLE:def 19
.= (((g**wB).s)|(H.s)).y by A17,FUNCT_1:49
.= ((g**wB)||H).x .y by MSAFREE:def 1;
end;
hence (hB||H).x = ((g**wB)||H).x by A16;
end;
hB is_homomorphism Free(S,Y), A by A1,A11,A10,EQUATION:22;
hence h||B = g**wB by A15,A14,EXTENS_1:19,PBOOLE:3;
let s be SortSymbol of S, i be Nat; assume
A33: i in Y.s;
A34: dom v = the carrier of S by PARTFUN1:def 2;
then
A35: v.s is one-to-one by A2;
then
A36: rng ((v.s)") = dom (v.s) & dom (v.s) = X0.s & rng (v.s) = Y.s &
dom((v.s)") = rng (v.s) by A34,FUNCT_1:33,FUNCT_2:def 1,FUNCT_6:22;
then reconsider x = (v.s)".i as Element of X0.s by A33,FUNCT_1:def 3;
take x; thus v.s.x = i by A33,A35,A36,FUNCT_1:35;
root-tree [i,s] in FreeGen(s,Y) & H c= B
by A33,PBOOLE:def 18,MSAFREE:def 15;
then
A37: root-tree [i,s] in H.s & H.s c= B.s by MSAFREE:def 16;
w.s = F(s) by A3;
then x = w.s.i by A33,A36,FUNCT_4:13;
then root-tree [x, s] = ww.s.root-tree [i,s] by A8
.= ((ww.s)|(B.s)).root-tree [i,s] by A37,FUNCT_1:49;
hence wB.s.root-tree [i,s] = root-tree [x, s] by MSAFREE:def 1;
end;
theorem Th65:
for h being ManySortedFunction of Free(S,X), A st
h is_homomorphism Free(S,X), A
ex g being ManySortedFunction of A,A st
g is_homomorphism A,A & h = g**canonical_homomorphism A
proof set X0 = X;
let h be ManySortedFunction of Free(S,X0), A such that
A1: h is_homomorphism Free(S,X0), A;
set ww = canonical_homomorphism A;
reconsider H = FreeGen X0 as GeneratorSet of Free(S,X0) by Th45;
reconsider G = FreeGen X0 as GeneratorSet of A by Th45;
A2: now
let s be SortSymbol of S, i be Element of X0.s;
root-tree [i,s] in FreeGen(s,X0) by MSAFREE:def 15;
then A3: root-tree [i,s] in H.s by MSAFREE:def 16;
G c= the Sorts of A by PBOOLE:def 18;
then H.s c= (the Sorts of A).s;
hence ww.s.root-tree [i,s] = root-tree [i, s] by A3,Th47;
end; then
A4: ww is_homomorphism Free(S,X0), A &
for s being SortSymbol of S, i being Element of X0.s holds
ww.s.root-tree [i,s] = root-tree [i, s] by Def10;
reconsider hG = h||H as ManySortedFunction of
G qua ManySortedSet of S, the Sorts of A;
consider g being ManySortedFunction of A,A such that
A5: g is_homomorphism A,A & g||G = hG by Def9;
take g;
thus g is_homomorphism A,A by A5;
A6: g**ww is_homomorphism Free(S,X0),A by A4,A5,MSUALG_3:10;
now
let x be object; assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
A7: dom ((h||H).s) = H.s & dom (((g**ww)||H).s) = H.s by FUNCT_2:def 1;
now let y be object; assume
A8: y in H.s; then y in FreeGen(s,X0) by MSAFREE:def 16;
then consider z such that
A9: z in X0.s & y = root-tree [z,s] by MSAFREE:def 15;
A10: ww.s.y = root-tree[z,s] by A2,A9;
then ww.s.y in FreeGen(s,X0) by A9,MSAFREE:def 15;
then
A11: ww.s.y in G.s by MSAFREE:def 16;
A12: H.s c= (the Sorts of Free(S,X0)).s by PBOOLE:def 2,def 18;
A13: dom (g**ww) = (the carrier of S)/\the carrier of S
by PARTFUN1:def 2;
thus (h||H).x .y
= ((g.s)|(G.s)).(ww.s.y) by A9,A10,A5,MSAFREE:def 1
.= g.s.(ww.s.y) by A11,FUNCT_1:49
.= ((g.s)*(ww.s)).y by A8,A12,FUNCT_2:15
.= ((g**ww).s).y by A13,PBOOLE:def 19
.= (((g**ww).s)|(H.s)).y by A8,FUNCT_1:49
.= ((g**ww)||H).x .y by MSAFREE:def 1;
end;
hence (h||H).x = ((g**ww)||H).x by A7;
end;
hence h = g**ww by A1,A6,EXTENS_1:19,PBOOLE:3;
end;
theorem Th66:
for o being OperSymbol of S
for x being Element of Args(o,A) holds
for x0 being Element of Args(o,Free(S,X)) st x0 = x holds
(canonical_homomorphism A)#x0 = x
proof:: set A = A0;
let o be OperSymbol of S;
let x be Element of Args(o,A);
let x0 be Element of Args(o,Free(S,X));
assume A1: x0 = x;
set k = canonical_homomorphism A;
now
let n being Nat;
assume
A2: n in dom x0;
A3: dom x = dom the_arity_of o by MSUALG_3:6; then
A4: (the_arity_of o)/.n = (the_arity_of o).n by A1,A2,PARTFUN1:def 6;
dom ((the Sorts of A)*the_arity_of o) = dom x by A3,PRALG_2:3; then
x .n in ((the Sorts of A)*the_arity_of o).n by A1,A2,MSUALG_3:6; then
x .n is Element of A, (the_arity_of o)/.n by A4,A2,A1,A3,FUNCT_1:13;
hence x .n = k.((the_arity_of o)/.n).(x0.n) by A1,Th47;
end;
hence (canonical_homomorphism A)#x0 = x by MSUALG_3:def 6;
end;
theorem Th67:
for o being OperSymbol of S
for x being Element of Args(o,A) holds
Den(o,A).x =
(canonical_homomorphism A).(the_result_sort_of o).(Den(o,Free(S,X)).x)
proof ::set A = A0;
let o be OperSymbol of S;
let x be Element of Args(o,A);
set k = canonical_homomorphism A;
set s = the_result_sort_of o;
x in Args(o,A) & Args(o,A) c= Args(o, Free(S,X)) by Th41; then
reconsider x0 = x as Element of Args(o,Free(S,X));
k#x0 = x by Th66;
hence Den(o,A).x
= k.(the_result_sort_of o).(Den(o,Free(S,X)).x) by Def10,MSUALG_3:def 7;
end;
theorem Th68:
for h being ManySortedFunction of Free(S,X), A
st h is_homomorphism Free(S,X), A
for o being OperSymbol of S
for x being Element of Args(o,A) holds
h.(the_result_sort_of o).(Den(o,A).x)
= h.(the_result_sort_of o).(Den(o,Free(S,X)).x)
proof set X0 = X;
let h be ManySortedFunction of Free(S,X0), A;
assume h is_homomorphism Free(S,X0), A; then
consider g being ManySortedFunction of A,A such that
A1: g is_homomorphism A,A & h = g**canonical_homomorphism A by Th65;
let o be OperSymbol of S;
let x be Element of Args(o,A);
A2: dom h = the carrier of S & dom canonical_homomorphism A = the carrier of S
by PARTFUN1:def 2;
A3: dom (h**canonical_homomorphism A) = (dom h)/\dom canonical_homomorphism A
by PBOOLE:def 19;
A4: x in Args(o,A) & Args(o,A) c= Args(o,Free(S,X0)) by Th41;
thus h.(the_result_sort_of o).(Den(o,A).x)
= h.(the_result_sort_of o).((canonical_homomorphism A).
(the_result_sort_of o).(Den(o,Free(S,X0)).x)) by Th67
.= ((h.the_result_sort_of o)*((canonical_homomorphism A).
(the_result_sort_of o))).(Den(o,Free(S,X0)).x) by A4,MSUALG_9:18,FUNCT_2:15
.= (h**canonical_homomorphism A).
(the_result_sort_of o).(Den(o,Free(S,X0)).x) by A2,A3,PBOOLE:def 19
.= (g**((canonical_homomorphism A)**(canonical_homomorphism A))).
(the_result_sort_of o).(Den(o,Free(S,X0)).x) by A1,PBOOLE:140
.= h.(the_result_sort_of o).(Den(o,Free(S,X0)).x) by A1,Th48;
end;
theorem Th69:
for h being ManySortedFunction of Free(S,X), A
st h is_homomorphism Free(S,X), A
for o being OperSymbol of S
for x being Element of Args(o,Free(S,X)) holds
h.(the_result_sort_of o).(Den(o,Free(S,X)).x)
= h.(the_result_sort_of o).(Den(o,Free(S,X)).
((canonical_homomorphism A)#x))
proof set X0 = X;
let h be ManySortedFunction of Free(S,X0), A;
assume h is_homomorphism Free(S,X0), A; then
consider g being ManySortedFunction of A,A such that
A1: g is_homomorphism A,A & h = g**canonical_homomorphism A by Th65;
let o be OperSymbol of S;
let x be Element of Args(o,Free(S,X0));
set k = canonical_homomorphism A;
A2: k#x in Args(o,A) & Args(o,A) c= Args(o,Free(S,X0)) by Th41;
thus h.(the_result_sort_of o).(Den(o,Free(S,X0)).x)
= ((g.the_result_sort_of o)*((canonical_homomorphism A).
the_result_sort_of o)).(Den(o,Free(S,X0)).x) by A1,MSUALG_3:2
.= g.(the_result_sort_of o).((canonical_homomorphism A).
(the_result_sort_of o).(Den(o,Free(S,X0)).x)) by MSUALG_9:18,FUNCT_2:15
.= g.(the_result_sort_of o).
(Den(o,A).(((canonical_homomorphism A))#x)) by Def10,MSUALG_3:def 7
.= g.(the_result_sort_of o).((canonical_homomorphism A).
(the_result_sort_of o).
(Den(o,Free(S,X0)).(((canonical_homomorphism A))#x))) by Th67
.= ((g.the_result_sort_of o)*((canonical_homomorphism A).
the_result_sort_of o)).(Den(o,Free(S,X0)).(((canonical_homomorphism A))#x))
by A2,MSUALG_9:18,FUNCT_2:15
.= h.(the_result_sort_of o).(Den(o,Free(S,X0)).
((canonical_homomorphism A)#x)) by A1,MSUALG_3:2;
end;
theorem
for X0,Y0 being non-empty countable ManySortedSet of S
for A being all_vars_including inheriting_operations
(X0,S)-terms MSAlgebra over S
for h being ManySortedFunction of Free(S,Y0), A st
h is_homomorphism Free(S,Y0), A
ex g being ManySortedFunction of Free(S,Y0),Free(S,X0) st
g is_homomorphism Free(S,Y0),Free(S,X0) & h = (canonical_homomorphism A)**g &
for G being GeneratorSet of Free(S,Y0) st G = FreeGen Y0
holds g||G = h||G
proof
let X0,Y be non-empty countable ManySortedSet of S;
let A be all_vars_including inheriting_operations
(X0,S)-terms MSAlgebra over S;
let h be ManySortedFunction of Free(S,Y), A such that
A1: h is_homomorphism Free(S,Y), A;
set ww = canonical_homomorphism A;
reconsider F = FreeGen Y as GeneratorSet of Free(S,Y) by Th45;
reconsider H = FreeGen X0 as GeneratorSet of Free(S,X0) by Th45;
reconsider G = FreeGen X0 as GeneratorSet of A by Th45;
now
let s be SortSymbol of S, i be Element of X0.s;
root-tree [i,s] in FreeGen(s,X0) by MSAFREE:def 15;
then A2: root-tree [i,s] in H.s by MSAFREE:def 16;
G c= the Sorts of A by PBOOLE:def 18;
then H.s c= (the Sorts of A).s;
hence ww.s.root-tree [i,s] = root-tree [i, s] by A2,Th47;
end; then
A3: ww is_homomorphism Free(S,X0), A &
for s being SortSymbol of S, i being Element of X0.s holds
ww.s.root-tree [i,s] = root-tree [i, s] by Def10;
the Sorts of A is MSSubset of Free(S,X0) by Def6;
then reconsider hG = h||F as ManySortedFunction of
F qua ManySortedSet of S, the Sorts of Free(S,X0) by Th22;
FreeGen Y is free & FreeMSA Y = Free(S,Y) by MSAFREE3:31;
then consider g being ManySortedFunction of Free(S,Y),Free(S,X0) such that
A4: g is_homomorphism Free(S,Y),Free(S,X0) & g||F = hG;
take g;
thus g is_homomorphism Free(S,Y),Free(S,X0) by A4;
A5: ww**g is_homomorphism Free(S,Y),A by A3,A4,MSUALG_3:10;
now
let x be object; assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
A6: dom ((h||F).s) = F.s & dom (((ww**g)||F).s) = F.s by FUNCT_2:def 1;
now let y be object; assume
A7: y in F.s;
A8: g.s.y = ((g.s)|(F.s)).y by A7,FUNCT_1:49
.= (h||F).s.y by A4,MSAFREE:def 1;
then
A9: g.s.y in (the Sorts of A).s by A7,FUNCT_2:5;
A10: F.s c= (the Sorts of Free(S,Y)).s by PBOOLE:def 2,def 18;
A11: dom (ww**g) = (the carrier of S)/\the carrier of S
by PARTFUN1:def 2;
thus (h||F).x .y = ww.s.(g.s.y) by A8,A9,Th47
.= ((ww.s)*(g.s)).y by A7,A10,FUNCT_2:15
.= ((ww**g).s).y by A11,PBOOLE:def 19
.= (((ww**g).s)|(F.s)).y by A7,FUNCT_1:49
.= ((ww**g)||F).x .y by MSAFREE:def 1;
end;
hence (h||F).x = ((ww**g)||F).x by A6;
end;
hence h = ww**g by A1,A5,EXTENS_1:19,PBOOLE:3;
thus thesis by A4;
end;
theorem Th71:
for w being ManySortedFunction of X0, (the carrier of S)-->NAT
for s being SortSymbol of S
for t being Element of Free(S,X0),s
for t1,t2 being Element of TermAlg S, s st
t1 = #(t,w) & t2 = #((canonical_homomorphism A0).s.t,w)
holds A0 |= t1 '=' t2
proof set A = A0;
let w be ManySortedFunction of X0, (the carrier of S)-->NAT;
let s be SortSymbol of S;
set k = canonical_homomorphism A;
set Y = (the carrier of S)-->NAT;
defpred P[DecoratedTree-like Function] means
for s being SortSymbol of S
for t1,t2 being Element of TermAlg S, s
for t3 being Term of S,X0
st t3 = k.s.$1 & t1 = #($1,w) & t2 = #(t3,w) holds A |= t1 '=' t2;
A1: for s1 being SortSymbol of S, v being Element of X0.s1
holds P[root-tree [v,s1]]
proof
let s1 be SortSymbol of S;
let v be Element of X0.s1;
set t = root-tree [v,s1];
let s be SortSymbol of S;
let t1,t2 be Element of TermAlg S, s;
let t3 be Term of S,X0;
assume A2: t3 = k.s.t;
assume A3: t1 = #(t,w);
assume A4: t2 = #(t3,w);
t1 = root-tree [w.s1.v, s1] & FreeMSA Y = Free(S,Y)
by A3,Th57,MSAFREE3:31; then
t1 in (the Sorts of Free(S,Y)).s1 & t1 in (the Sorts of Free(S,Y)).s
by MSAFREE3:4; then
(the Sorts of Free(S,Y)).s1 meets (the Sorts of Free(S,Y)).s &
(s <> s1 implies
(the Sorts of Free(S,Y)).s1 misses (the Sorts of Free(S,Y)).s)
by XBOOLE_0:3,PROB_2:def 2; then
t is Element of A,s by Th40; then
t3 = t by A2,Th47;
hence A |= t1 '=' t2 by A3,A4;
end;
A5: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X0) st
for t being Term of S,X0 st t in rng p holds P[t]
holds P[[o,the carrier of S]-tree p]
proof
let o be OperSymbol of S;
let p be ArgumentSeq of Sym(o,X0);
assume
for t being Term of S,X0 st t in rng p holds P[t];
set t = [o,the carrier of S]-tree p;
let s be SortSymbol of S;
let t1,t2 be Element of TermAlg S, s;
let t3 be Term of S,X0;
assume A6: t3 = k.s.t;
assume A7: t1 = #(t,w);
assume A8: t2 = #(t3,w);
A9: FreeMSA X0 = Free(S,X0) by MSAFREE3:31; then
reconsider a = p as Element of Args(o,Free(S,X0)) by INSTALG1:1;
A10: t = Den(o,Free(S,X0)).a by A9,INSTALG1:3;
t1 is Element of (the Sorts of Free(S,Y)).s by MSAFREE3:31; then
reconsider tq = t1 as Term of S,Y by Th42;
defpred Q[Nat,object] means
for t being Element of Free(S,X0) st t = p.$1 holds $2 = #(t,w);
A11: dom p = Seg len p by FINSEQ_1:def 3;
A12: for i being Nat st i in Seg len p ex x being object st Q[i,x]
proof
let i be Nat;
assume i in Seg len p; then
p.i is Term of S,X0 by A11,MSATERM:22; then
p.i is Element of FreeMSA X0 by MSATERM:13; then
reconsider t = p.i as Element of Free(S,X0) by MSAFREE3:31;
take x = #(t,w);
thus Q[i,x];
end;
consider q being FinSequence such that
A13: dom q = Seg len p &
for i being Nat st i in Seg len p holds Q[i,q.i] from FINSEQ_1:sch 1(A12
);
dom q = dom p & for i being Nat, t being Element of Free(S,X0)
st i in dom p & t = p.i
holds q.i = #(t,w) by A11,A13;
then
A14: t1 = Sym(o,Y)-tree q by A7,Th58;
now
let i be object; assume
A15: i in dom q; then
p.i is Term of S,X0 by A11,A13,MSATERM:22; then
p.i is Element of FreeMSA X0 by MSATERM:13; then
reconsider t = p.i as Element of Free(S,X0) by MSAFREE3:31;
q.i = #(t,w) by A13,A15; then
q.i is Element of Free(S, Y) by MSAFREE3:31;
hence q.i is DecoratedTree;
end; then
q is DTree-yielding by TREES_3:24; then
tq.{} = Sym(o,Y) by A14,TREES_4:def 4; then
the_sort_of tq = the_result_sort_of o by MSATERM:17; then
tq in FreeSort(Y,the_result_sort_of o) by MSATERM:def 5; then
t1 in (the Sorts of TermAlg S).s &
t1 in (the Sorts of TermAlg S).the_result_sort_of o by MSAFREE:def 11;
then
A16: s = the_result_sort_of o by PROB_2:def 2,XBOOLE_0:3;
reconsider tt = t as Element of Free(S,X0), s by A16,A10,MSUALG_9:18;
A17: the Sorts of A is MSSubset of Free(S,X0) by Def6;
k.s.tt in (the Sorts of A).s &
(the Sorts of A).s c= (the Sorts of Free(S,X0)).s
by A17,PBOOLE:def 2,def 18; then
reconsider kt = k.s.tt as Element of Free(S,X0), s;
let h be ManySortedFunction of TermAlg S, A such that
A18: h is_homomorphism TermAlg S, A;
consider hh being ManySortedFunction of Free(S,X0), TermAlg S such that
A19: hh is_homomorphism Free(S,X0), TermAlg S &
for s being SortSymbol of S, t being Element of Free(S,X0),s
holds #(t,w) = hh.s.t by Th56;
A20: k.s.(Den(o,Free(S,X0)).a) in (the Sorts of A).s &
(the Sorts of A).s c= (the Sorts of Free(S,X0)).s
by A17,PBOOLE:def 2,def 18,FUNCT_2:5,A16,MSUALG_9:18;
thus h.s.(t1 '=' t2)`1 = h.s.(hh.s.tt) by A7,A19
.= h.s.(hh.s.(Den(o,Free(S,X0)).a)) by A9,INSTALG1:3
.= ((h.s)*(hh.s)).(Den(o,Free(S,X0)).a) by A16,MSUALG_9:18,FUNCT_2:15
.= ((h**hh).s).(Den(o,Free(S,X0)).a) by MSUALG_3:2
.= ((h**hh).s).(Den(o,Free(S,X0)).(k#a)) by A16,Th69,A18,A19,MSUALG_3:10
.= ((h**hh).s).(Den(o,A).(k#a)) by Th68,A18,A19,MSUALG_3:10,A16
.= ((h**hh).s).(k.s.(Den(o,Free(S,X0)).a)) by A16,Def10,MSUALG_3:def 7
.= ((h.s)*(hh.s)).(k.s.(Den(o,Free(S,X0)).a)) by MSUALG_3:2
.= h.s.(hh.s.(k.s.(Den(o,Free(S,X0)).a))) by A20,FUNCT_2:15
.= h.s.(hh.s.kt) by A9,INSTALG1:3
.= h.s.t2 by A6,A8,A19
.= h.s.(t1 '=' t2)`2;
end;
A21: for t being Term of S,X0 holds P[t] from MSATERM:sch 1(A1,A5);
let t be Element of (the Sorts of Free(S,X0)).s;
A22: t is Term of S,X0 by Th42;
let t1,t2 be Element of TermAlg S, s;
assume A23: t1 = #(t,w);
assume A24: t2 = #(k.s.t,w);
k.s.t is Element of (the Sorts of A).s; then
k.s.t is Term of S,X0 by Th42;
hence A |= t1 '=' t2 by A22,A21,A23,A24;
end;
theorem
for w being ManySortedFunction of X0, (the carrier of S)-->NAT
for o being OperSymbol of S
for p being Element of Args(o,Free(S,X0))
for q being Element of Args(o,A0) st (canonical_homomorphism A0)#p = q
for t1,t2 being Term of S,X0 st t1 = Den(o,Free(S,X0)).p & t2 = Den(o,A0).q
for t3,t4 being Element of TermAlg S, the_result_sort_of o
st t3 = #(t1,w) & t4 = #(t2,w) holds
A0 |= t3 '=' t4
proof set A = A0;
let w be ManySortedFunction of X0, (the carrier of S)-->NAT;
set Y = (the carrier of S)-->NAT;
let o be OperSymbol of S;
let p be Element of Args(o,Free(S,X0));
let q be Element of Args(o,A) such that
A1: (canonical_homomorphism A)#p = q;
Free(S,X0) = FreeMSA X0 by MSAFREE3:31;
then reconsider p0 = p as ArgumentSeq of Sym(o,X0) by INSTALG1:1;
let t1,t2 be Term of S,X0 such that
A2: t1 = Den(o,Free(S,X0)).p & t2 = Den(o,A).q;
let t3,t4 be Element of TermAlg S, the_result_sort_of o;
assume
A3: t3 = #(t1,w) & t4 = #(t2,w);
reconsider t1 as Element of Free(S,X0),the_result_sort_of o
by A2,MSUALG_9:18;
t2 = (canonical_homomorphism A).(the_result_sort_of o).t1
by A1,A2,Def10,MSUALG_3:def 7;
hence A |= t3 '=' t4 by A3,Th71;
end;
theorem Th73:
for w being ManySortedFunction of X0, (the carrier of S)-->NAT st w is "1-1"
ex g being ManySortedFunction of TermAlg S, Free(S,X0) st
g is_homomorphism TermAlg S, Free(S,X0) &
for s being SortSymbol of S
for t being Element of Free(S,X0),s holds g.s. #(t,w) = t
proof
let w be ManySortedFunction of X0, (the carrier of S)-->NAT;
assume A1: w is "1-1";
A2: Free(S,X0) = FreeMSA X0 by MSAFREE3:31;
reconsider G = FreeGen((the carrier of S)-->NAT) as
non-empty GeneratorSet of TermAlg S;
set Y = (the carrier of S)-->NAT;
defpred P[set,set,set] means
for x being Element of Y.$1 st $2 = root-tree [x,$1] holds
(x in rng (w.$1) implies $3 = root-tree [(w.$1)".x,$1]) &
(x nin rng (w.$1) implies
$3 = the Element of (the Sorts of Free(S,X0)).$1);
A3: for s being SortSymbol of S, t being Element of G.s
ex T being Element of (the Sorts of Free(S,X0)).s st P[s,t,T]
proof
let s be SortSymbol of S;
let t be Element of G.s;
t in G.s; then
t in FreeGen(s,Y) by MSAFREE:def 16; then
consider x being set such that
A4: x in Y.s & t = root-tree [x,s] by MSAFREE:def 15;
reconsider x as Element of Y.s by A4;
per cases;
suppose
A5: x in rng(w.s); then
consider a being object such that
A6: a in dom(w.s) & x = (w.s).a by FUNCT_1:def 3;
reconsider T = root-tree [a,s] as Element of
(the Sorts of Free(S,X0)).s by A6,MSAFREE3:4;
take T;
let x0 be Element of Y.s; assume t = root-tree [x0,s]; then
A7: [x0,s] = [x,s] by A4,TREES_4:4; then
A8: x = x0 by XTUPLE_0:1;
w.s is one-to-one by A1,MSUALG_3:1;
hence x0 in rng(w.s) implies T = root-tree [(w.s)".x0,s]
by A6,A8,FUNCT_1:34;
thus thesis by A5,A7,XTUPLE_0:1;
end;
suppose
A9: x nin rng(w.s);
set T = the Element of (the Sorts of Free(S,X0)).s;
take T;
let x0 be Element of Y.s; assume t = root-tree [x0,s]; then
[x0,s] = [x,s] by A4,TREES_4:4;
hence thesis by A9,XTUPLE_0:1;
end;
end;
consider gg being ManySortedFunction of G, the Sorts of Free(S,X0)
such that
A10: for s being SortSymbol of S for t being Element of G.s
holds P[s,t,gg.s.t] from CIRCTRM1:sch 1(A3);
consider g being ManySortedFunction of TermAlg S, Free(S,X0) such that
A11: g is_homomorphism TermAlg S, Free(S,X0) & g||G = gg by MSAFREE:def 5;
take g;
thus g is_homomorphism TermAlg S, Free(S,X0) by A11;
defpred P[DecoratedTree] means
for s being SortSymbol of S st $1 in (the Sorts of Free(S,X0)).s
holds g.s. #($1,w) = $1;
A12: for s being SortSymbol of S, v being Element of X0.s
holds P[root-tree [v,s]]
proof
let s be SortSymbol of S;
let v be Element of X0.s;
set t = root-tree [v,s];
let s0 be SortSymbol of S; assume
A13: t in (the Sorts of Free(S,X0)).s0;
t in (the Sorts of Free(S,X0)).s by MSAFREE3:4; then
A14: s = s0 by A13,XBOOLE_0:3,PROB_2:def 2; then
A15: w.s0.v in rng (w.s0) & w.s0.v in Y.s0 by FUNCT_2:4,5; then
root-tree [w.s0.v,s0] in FreeGen(s0,Y) by MSAFREE:def 15; then
A16: root-tree [w.s0.v,s0] in G.s0 by MSAFREE:def 16; then
A17: gg.s0.root-tree [w.s0.v,s0] = root-tree [(w.s0)".(w.s0.v),s0] by A15,A10
;
A18: #(t,w) = root-tree [w.s0.v,s0] by A14,Th57;
gg.s0 = (g.s0)|(G.s0) by A11,MSAFREE:def 1; then
A19: g.s0.root-tree [w.s0.v,s0] = root-tree [(w.s0)".(w.s0.v),s0]
by A16,A17,FUNCT_1:49;
w.s0 is one-to-one by A1,MSUALG_3:1;
hence thesis by A14,A18,A19,FUNCT_2:26;
end;
A20: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X0) st
for t being Term of S,X0 st t in rng p holds P[t]
holds P[[o,the carrier of S]-tree p]
proof
let o be OperSymbol of S;
let p be ArgumentSeq of Sym(o,X0);
assume
A21: for t being Term of S,X0 st t in rng p holds P[t];
set t = [o,the carrier of S]-tree p;
let s be SortSymbol of S; assume
A22: t in (the Sorts of Free(S,X0)).s;
t.{} = [o,the carrier of S] by TREES_4:def 4; then
the_sort_of (Sym(o,X0)-tree p) = the_result_sort_of o by MSATERM:17; then
t in FreeSort(X0,the_result_sort_of o) by MSATERM:def 5; then
t in (the Sorts of Free(S,X0)).the_result_sort_of o by A2,MSAFREE:def 11;
then
A23: s = the_result_sort_of o by A22,XBOOLE_0:3,PROB_2:def 2;
defpred Q[Nat,object] means
for t being Element of Free(S,X0) st t = p.$1 holds $2 = #(t,w);
A24: dom p = Seg len p by FINSEQ_1:def 3;
A25: for i being Nat st i in Seg len p ex x being object st Q[i,x]
proof
let i be Nat;
assume i in Seg len p; then
p.i is Term of S,X0 by A24,MSATERM:22; then
p.i is Element of FreeMSA X0 by MSATERM:13; then
reconsider t = p.i as Element of Free(S,X0) by MSAFREE3:31;
take x = #(t,w);
thus Q[i,x];
end;
consider q being FinSequence such that
A26: dom q = Seg len p &
for i being Nat st i in Seg len p holds Q[i,q.i] from FINSEQ_1:sch 1(A25
);
dom q = dom p & for i being Nat, t being Element of Free(S,X0)
st i in dom p & t = p.i
holds q.i = #(t,w) by A24,A26;
then
A27: #(t,w) = Sym(o,Y)-tree q by Th58;
now
let i be object; assume
A28: i in dom q; then
p.i is Term of S,X0 by A24,A26,MSATERM:22; then
p.i is Element of FreeMSA X0 by MSATERM:13; then
reconsider t = p.i as Element of Free(S,X0) by MSAFREE3:31;
q.i = #(t,w) by A26,A28; then
q.i is Element of Free(S, Y) by MSAFREE3:31;
hence q.i is DecoratedTree;
end; then
A29: q is DTree-yielding by TREES_3:24;
TermAlg S = Free(S,Y) by MSAFREE3:31; then
#(t,w).{} = Sym(o,Y) & #(t,w) is Term of S,Y
by Th42,A29,A27,TREES_4:def 4; then
consider r being ArgumentSeq of Sym(o,Y) such that
A30: #(t,w) = [o,the carrier of S]-tree r by MSATERM:10;
r = q by A29,A27,A30,TREES_4:15; then
reconsider q as Element of Args(o,TermAlg S) by INSTALG1:1;
reconsider a = p as Element of Args(o,Free(S,X0)) by A2,INSTALG1:1;
for n being Nat st n in dom q holds a.n = (g.((the_arity_of o)/.n)).(q.n)
proof
let n be Nat;
assume A31: n in dom q;
A32: dom q = dom the_arity_of o & dom a = dom the_arity_of o by MSUALG_3:6;
then reconsider tn = a.n as Term of S,X0 by A31,MSATERM:22;
A33: tn in rng p by A31,A32,FUNCT_1:def 3;
the_sort_of tn = (the_arity_of o)/.n by A31,A32,MSATERM:23; then
tn in FreeSort(X0,(the_arity_of o)/.n) by MSATERM:def 5; then
tn in (the Sorts of Free(S,X0)).((the_arity_of o)/.n)
by A2,MSAFREE:def 11; then
A34: g.((the_arity_of o)/.n). #(tn,w) = tn by A21,A33;
Q[n,q.n] & tn is Element of Free(S,X0)
by A2,A26,A31,MSATERM:13;
hence a.n = (g.((the_arity_of o)/.n)).(q.n) by A34;
end; then
A35: g#q = a by MSUALG_3:def 6;
thus g.s. #(t,w) = g.s.(Den(o,TermAlg S).q) by A27,INSTALG1:3
.= Den(o,Free(S,X0)).(g#q) by A11,A23
.= t by A2,A35,INSTALG1:3;
end;
A36: for t being Term of S,X0 holds P[t] from MSATERM:sch 1(A12,A20);
let s be SortSymbol of S;
let t be Element of (the Sorts of Free(S,X0)).s;
t is Term of S,X0 by Th42;
hence g.s. #(t,w) = t by A36;
end;
theorem Th74:
for B being non-empty MSAlgebra over S
for h being ManySortedFunction of Free(S,X0),B
st h is_homomorphism Free(S,X0),B
for w being ManySortedFunction of X0, (the carrier of S)-->NAT st w is "1-1"
for s being SortSymbol of S
for t1,t2 being Element of Free(S,X0),s
for t3,t4 being Element of TermAlg S, s st t3 = #(t1,w) & t4 = #(t2,w) holds
B |= t3 '=' t4 implies h.s.t1 = h.s.t2
proof
let A be non-empty MSAlgebra over S;
let h be ManySortedFunction of Free(S,X0),A;
assume A1: h is_homomorphism Free(S,X0),A;
let w be ManySortedFunction of X0, (the carrier of S)-->NAT;
assume w is "1-1"; then
consider g being ManySortedFunction of TermAlg S, Free(S,X0) such that
A2: g is_homomorphism TermAlg S, Free(S,X0) &
for s being SortSymbol of S
for t being Element of Free(S,X0),s holds g.s. #(t,w) = t by Th73;
let s be SortSymbol of S;
let t1,t2 be Element of Free(S,X0),s;
let t3,t4 be Element of TermAlg S, s;
assume A3: t3 = #(t1,w);
assume A4: t4 = #(t2,w);
assume A |= t3 '=' t4; then
A6: (h**g).s.(t3 '=' t4)`1 = (h**g).s.(t3 '=' t4)`2
by A2,A1,MSUALG_3:10;
(h**g).s = (h.s)*(g.s) by MSUALG_3:2; then
(h**g).s.t3 = h.s.(g.s.t3) & (h**g).s.t4 = h.s.(g.s.t4) by FUNCT_2:15;
hence h.s.t1 = h.s.(g.s.t4) by A2,A6,A3 .= h.s.t2 by A2,A4;
end;
theorem Th75:
for G being GeneratorSet of A0 st G = FreeGen X0
holds G is Equations(S,A0)-free
proof set A = A0;
A1: FreeMSA X0 = Free(S,X0) by MSAFREE3:31;
let G be GeneratorSet of A; assume
A2: G = FreeGen X0;
set T = Equations(S,A);
let B be T-satisfying non-empty MSAlgebra over S;
let f be ManySortedFunction of G, the Sorts of B;
reconsider f0 = f as ManySortedFunction of FreeGen X0, the Sorts of B
by A2;
reconsider H = FreeGen X0 as free GeneratorSet of Free(S,X0)
by A1;
consider g being ManySortedFunction of Free(S,X0), B such that
A3: g is_homomorphism Free(S,X0),B & g || H = f0 by MSAFREE:def 5;
the Sorts of A is MSSubset of Free(S,X0) by Def6; then
reconsider i = id the Sorts of A as ManySortedFunction of A, Free(S,X0)
by Th22;
take h = g**i;
thus h is_homomorphism A,B
proof
let o be OperSymbol of S such that Args(o,A) <> {};
let x be Element of Args(o,A);
set s = the_result_sort_of o;
Den(o,A).x in Result(o,A); then
A4: Den(o,A).x in (the Sorts of A).s by FUNCT_2:15;
A5: i.s = id ((the Sorts of A).s) by MSUALG_3:def 1;
x in Args(o,A) & Args(o,A) c= Args(o, Free(S,X0)) by Th41; then
reconsider x0 = x as Element of Args(o,Free(S,X0));
set w = the "1-1" ManySortedFunction of X0, (the carrier of S)-->NAT;
Den(o,A).x is Element of Result(o,A) &
Den(o,Free(S,X0)).x0 is Element of Result(o,Free(S,X0)); then
reconsider f1 = Den(o,A).x, f2 = Den(o,Free(S,X0)).x0 as Term of S,X0
by Th42;
reconsider f = Den(o,Free(S,X0)).x0 as Element of Free(S,X0),s
by MSUALG_9:18;
reconsider fa = (canonical_homomorphism A).s.f as
Element of Free(S,X0),s by Th39;
f1 in (the Sorts of A).s by MSUALG_9:18; then
f1 is Element of Free(S,X0),s by Th39; then
f1 in (the Sorts of Free(S,X0)).s & f2 in (the Sorts of Free(S,X0)).s
by MSUALG_9:18; then
f1 in FreeSort(X0,s) & f2 in FreeSort(X0,s) by A1,MSAFREE:def 11; then
the_sort_of f1 = s & the_sort_of f2 = s by MSATERM:def 5; then
reconsider t2 = #(f1,w), t1 = #(f2,w) as Element of TermAlg S, s by Th60;
A6: f1 = (canonical_homomorphism A).s.f by Th67;
A |= t1 '=' t2 by A6,Th71; then
t1 '=' t2 in {e where e is Element of (Equations S).s: A |= e}; then
t1 '=' t2 in T.s & B |= T by Def14,Def11; then
A7: g.s.f = g.s.fa by A6,A3,Th74;
A8: now
let n be Nat;
set an = (the_arity_of o)/.n;
assume
A9: n in dom x;
A10: dom ((the Sorts of A)*the_arity_of o) = dom the_arity_of o &
dom x = dom the_arity_of o by MSUALG_3:6,PRALG_2:3; then
x .n in ((the Sorts of A)*the_arity_of o).n by A9,MSUALG_3:6; then
x .n in (the Sorts of A).((the_arity_of o).n) by A9,A10
,FUNCT_1:13; then
A11: x .n in (the Sorts of A).an by A9,A10,PARTFUN1:def 6;
thus (h#x).n = (h.(an)).(x .n) by A9,MSUALG_3:def 6
.= ((g.an)*(i.an)).(x .n) by MSUALG_3:2
.= (g.an).((i.an).(x .n)) by A11,FUNCT_2:15
.= (g.an).((id ((the Sorts of A).an)).(x .n)) by MSUALG_3:def 1
.= (g.((the_arity_of o)/.n)).(x .n) by A11,FUNCT_1:17;
end;
thus (h.(s)).(Den(o,A).x)
= ((g.s)*(i.s)).(Den(o,A).x) by MSUALG_3:2
.= (g.s).((i.s).(Den(o,A).x)) by A4,FUNCT_2:15
.= (g.s).(Den(o,A).x) by A5,A4,FUNCT_1:18
.= (g.s).(Den(o,Free(S,X0)).x0) by A7,Th67
.= Den(o,B).(g#x0) by A3
.= Den(o,B).(h#x) by A8,MSUALG_3:def 6;
end;
now let x be object; assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
A12: G.s c= (the Sorts of A).s by PBOOLE:def 2,def 18;
dom (g.s) = (the Sorts of Free(S,X0)).s &
rng (i.s) c= (the Sorts of Free(S,X0)).s
by FUNCT_2:def 1; then
dom((g.s)*(i.s qua Function)) = dom (i.s) by RELAT_1:27
.= (the Sorts of A).s by FUNCT_2:def 1; then
A13: dom (((g.s)*(i.s))|(G.s)) = G.s by A12,RELAT_1:62;
the Sorts of A is MSSubset of Free(S,X0) by Def6; then
(the Sorts of A).s c= (the Sorts of Free(S,X0)).s
by PBOOLE:def 2,def 18; then
G.s c= (the Sorts of Free(S,X0)).s &
dom (g.s) = (the Sorts of Free(S,X0)).s by A12,FUNCT_2:def 1;
then
A14: dom ((g.s)|(H.s)) = G.s by A2,RELAT_1:62;
A15: now
let x be object; assume
A16: x in G.s;
hence (((g.s)*(i.s))|(G.s)).x = ((g.s)*(i.s)).x by FUNCT_1:49
.= (g.s).((i.s).x) by A12,A16,FUNCT_2:15
.= (g.s).((id ((the Sorts of A).s)).x) by MSUALG_3:def 1
.= g.s.x by A12,A16,FUNCT_1:17
.= ((g.s)|(H.s)).x by A2,A16,FUNCT_1:49;
end;
thus (h||G).x = (h.s)|(G.s) by MSAFREE:def 1
.= ((g.s)*(i.s))|(G.s) by MSUALG_3:2
.= (g.s)|(H.s) by A13,A14,A15
.= f.x by A3,MSAFREE:def 1;
end;
hence h || G = f;
end;
theorem
A0 is Equations(S,A0)-free
proof
reconsider G = FreeGen X0 as GeneratorSet of A0 by Th45;
take G; thus thesis by Th75;
end;
begin :: Algebra of normal forms
definition
let I be set;
let X,Y be ManySortedSet of I;
let R be ManySortedRelation of X,Y;
let x be object;
redefine func R.x -> Relation of X.x,Y.x; :: redefines . (FUNCT_1, definition)
coherence
proof
per cases;
suppose x in I;
hence thesis by MSUALG_4:def 1;
end;
suppose x nin dom R;
then R.x = {} by FUNCT_1:def 2;
hence thesis by XBOOLE_1:2;
end;
end;
end;
definition
let I be set;
let X be ManySortedSet of I;
let R be ManySortedRelation of X;
attr R is terminating means: Def16:
for x being set st x in I holds R.x is strongly-normalizing;
attr R is with_UN_property means: Def17:
for x being set st x in I holds R.x is with_UN_property;
end;
registration
cluster -> strongly-normalizing with_UN_property for empty set;
coherence;
end;
theorem Th77:
for I being set
for A being ManySortedSet of I
ex R being ManySortedRelation of A
st R = I-->{} & R is terminating
proof
let I be set;
let A be ManySortedSet of I;
set R = I-->{};
for i being set st i in I holds R.i is Relation of A.i by XBOOLE_1:2;
then reconsider R as ManySortedRelation of A by MSUALG_4:def 1;
take R;
thus R = I-->{};
let i be set;
thus thesis;
end;
registration
let I be set;
let X be ManySortedSet of I;
cluster empty-yielding -> with_UN_property terminating
for ManySortedRelation of X;
coherence;
cluster empty-yielding for ManySortedRelation of X;
existence
proof
consider R being ManySortedRelation of X such that
A1: R = I-->{} & R is terminating by Th77;
take R;
rng R c= {{}} by A1,FUNCOP_1:13;
hence thesis by RELAT_1:def 15;
end;
end;
registration
let I be set;
let X be ManySortedSet of I;
let R be terminating ManySortedRelation of X;
let i be object;
cluster R.i -> strongly-normalizing for Relation;
coherence
proof
per cases;
suppose i in I;
hence thesis by Def16;
end;
suppose i nin dom R;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let I be set;
let X be ManySortedSet of I;
let R be with_UN_property ManySortedRelation of X;
let i be object;
cluster R.i -> with_UN_property for Relation;
coherence
proof
per cases;
suppose i in I;
hence thesis by Def17;
end;
suppose i nin dom R;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
definition
let S,X;
let R be ManySortedRelation of Free(S,X);
attr R is NF-var means: Def18:
for s being SortSymbol of S for x being Element of (FreeGen X).s
holds x is_a_normal_form_wrt R.s;
end;
theorem
x is_a_normal_form_wrt {};
registration
let S,X;
cluster empty-yielding -> NF-var invariant stable
for ManySortedRelation of Free(S,X);
coherence
proof
let R be ManySortedRelation of Free(S,X); assume
A1: R is empty-yielding;
thus R is NF-var
proof
let s be SortSymbol of S;
R.s is empty by A1;
hence thesis;
end;
thus R is invariant
by A1;
let h be Endomorphism of Free(S,X);
let s be SortSymbol of S;
thus thesis by A1;
end;
end;
registration
let S,X;
cluster NF-var terminating with_UN_property
for invariant stable ManySortedRelation of Free(S,X);
existence
proof
take R = the empty-yielding ManySortedRelation of Free(S,X);
thus thesis;
end;
end;
scheme A {x1,x2()->set, R()->Relation, P[set] }:
P[x2()]
provided
A1: P[x1()] and
A2: R() reduces x1(),x2() and
A3: for y,z being set st R() reduces x1(),y & [y,z] in R() &
P[y] holds P[z]
proof
consider t being RedSequence of R() such that
A4: t.1 = x1() & t.len t = x2() by A2;
defpred Q[Nat] means $1 in dom t implies P[t.$1];
A5: Q[0] by FINSEQ_3:24;
A6: now let i; assume
A7: Q[i];
thus Q[i+1]
proof assume
A8: i+1 in dom t & not P[t.(i+1)];
per cases by NAT_1:3;
suppose i = 0;
hence thesis by A1,A4,A8;
end;
suppose i > 0;
then consider j being Nat such that
A9: i = j+1 by NAT_1:6;
i <= i+1 & i+1 <= len t by A8,FINSEQ_3:25,NAT_1:11; then
A10: 1 <= i & i <= len t & rng t <> {} by A9,NAT_1:11,XXREAL_0:2; then
A11: i in dom t & 1 in dom t by FINSEQ_3:25,32;
[t.i,t.(i+1)] in R() by A8,A11,REWRITE1:def 2;
hence thesis by A3,A7,A8,A11,A4,A10,REWRITE1:17;
end;
end;
end;
Q[i] from NAT_1:sch 2(A5,A6);
hence thesis by A4,FINSEQ_5:6;
end;
scheme B {x1,x2()->set, R()->Relation, P[set] }:
P[x1()]
provided
A1: P[x2()] and
A2: R() reduces x1(),x2() and
A3: for y,z being set st [y,z] in R() & P[z] holds P[y]
proof
A4: R()~ reduces x2(),x1() by A2,REWRITE1:24;
A5: for y,z being set st R()~ reduces x2(),y & [y,z] in R()~ & P[y] holds P[z]
proof
let y,z be set;
assume R()~ reduces x2(),y;
assume [y,z] in R()~;
then [z,y] in R() by RELAT_1:def 7;
hence thesis by A3;
end;
thus P[x1()] from A(A1,A4,A5);
end;
definition
let X be non empty set;
let R be with_UN_property strongly-normalizing Relation of X;
let x be Element of X;
redefine func nf(x,R) -> Element of X; :: redefines nf (REWRITE1, definition)
coherence
proof
defpred P[set] means $1 in X;
A1: P[x];
nf(x,R) is_a_normal_form_of x,R by REWRITE1:54;
then
A2: R reduces x,nf(x,R);
A3: for y,z being set st R reduces x,y & [y,z] in R &
P[y] holds P[z]
proof
let y,z be set;
assume R reduces x,y;
assume A4: [y,z] in R;
z in field R & field R c= X \/ X by A4,RELAT_1:15,RELSET_1:8;
hence thesis;
end;
P[nf(x,R)] from A(A1,A2,A3);
hence thesis;
end;
end;
definition
let I be non empty set;
let X be non-empty ManySortedSet of I;
let R be with_UN_property terminating ManySortedRelation of X;
func NForms R -> non-empty ManySortedSubset of X means: Def19:
for i being Element of I holds
it.i = the set of all nf(x,R.i) where x is Element of X.i;
existence
proof
deffunc F(Element of I) =
the set of all nf(x,R.$1) where x is Element of X.$1;
consider A being ManySortedSet of I such that
A1: for i being Element of I holds A.i = F(i) from PBOOLE:sch 5;
A2: A is ManySortedSubset of X
proof
let i be object;
assume i in I;
then reconsider j = i as Element of I;
A3: A.j = the set of all nf(x,R.j) where x is Element of X.j by A1;
let x be object; assume x in A.i;
then ex y being Element of X.j st x = nf(y,R.j) by A3;
hence thesis;
end;
A is non-empty
proof
let i be object;
assume i in I;
then reconsider j = i as Element of I;
A4: A.j = the set of all nf(x,R.j) where x is Element of X.j by A1;
set x = the Element of X.j;
nf(x,R.j) in A.i by A4;
hence thesis;
end;
hence thesis by A1,A2;
end;
uniqueness
proof
let A1,A2 be non-empty ManySortedSubset of X such that
A5: for i being Element of I holds
A1.i = the set of all nf(x,R.i) where x is Element of X.i and
A6: for i being Element of I holds
A2.i = the set of all nf(x,R.i) where x is Element of X.i;
let i be Element of I;
thus A1.i = the set of all nf(x,R.i) where x is Element of X.i by A5
.= A2.i by A6;
end;
end;
scheme MSFLambda {B()->non empty set,D(object)->non empty set,
F(object,object)->set}:
ex f being ManySortedFunction of B() st
for o being Element of B() holds dom (f.o) = D(o) &
for x being Element of D(o) holds f.o.x = F(o,x)
proof
defpred P[object,object] means
ex g being Function st $2 = g & dom g = D($1) &
for x being Element of D($1) holds g.x = F($1,x);
A1: for o being object st o in B() ex g being object st P[o,g]
proof
let o be object; assume o in B();
deffunc G(object) = F(o,$1);
consider g being Function such that
A2: dom g = D(o) & for x being object st x in D(o) holds g.x = G(x)
from FUNCT_1:sch 3;
take g,g; thus g = g & dom g = D(o) by A2;
thus for x being Element of D(o) holds g.x = F(o,x) by A2;
end;
consider f being ManySortedSet of B() such that
A3: for o being object st o in B() holds P[o,f.o] from PBOOLE:sch 3(A1);
f is Function-yielding
proof
let o be object; assume o in dom f;
then P[o,f.o] by A3;
hence f.o is Function;
end;
then reconsider f as ManySortedFunction of B();
take f;
let o be Element of B();
A4: P[o,f.o] by A3;
hence dom (f.o) = D(o);
let x be Element of D(o);
thus f.o.x = F(o,x) by A4;
end;
definition
let S,X;
let R be terminating with_UN_property invariant stable
ManySortedRelation of Free(S,X);
func NFAlgebra R -> non-empty strict MSAlgebra over S means: Def20:
the Sorts of it = NForms R &
for o being OperSymbol of S, a being Element of Args(o,it) holds
Den(o,it).a = nf (Den(o,Free(S,X)).a, R.the_result_sort_of o);
existence
proof
deffunc D(OperSymbol of S) = product ((NForms R)*the_arity_of $1);
deffunc F(OperSymbol of S,Element of D($1)) =
nf(Den($1,Free(S,X)).$2, R.the_result_sort_of $1);
consider f being ManySortedFunction of the carrier' of S such that
A1: for o being OperSymbol of S holds dom(f.o) = D(o) &
for x being Element of D(o) holds f.o.x = F(o,x) from MSFLambda;
f is ManySortedFunction of (NForms R)#*the Arity of S,
(NForms R)*the ResultSort of S
proof
let i be object; assume
i in the carrier' of S;
then reconsider o = i as OperSymbol of S;
dom(f.o) = D(o) by A1;
then
A2: dom(f.o) = (NForms R)# qua Function.the_arity_of o by FINSEQ_2:def 5
.= ((NForms R)#*the Arity of S).o by FUNCT_2:15;
rng(f.o) c= ((NForms R)*the ResultSort of S).o
proof
let x be object; assume x in rng(f.o);
then consider y being object such that
A3: y in dom(f.o) & x = f.o.y by FUNCT_1:def 3;
reconsider y as Element of D(o) by A1,A3;
A4: x = F(o,y) by A1,A3;
(NForms R)*the_arity_of o qua ManySortedSet of dom the_arity_of o
c= (the Sorts of Free(S,X))*the_arity_of o
qua ManySortedSet of dom the_arity_of o
by Th15,PBOOLE:def 18;
then product ((NForms R)*the_arity_of o) c=
product((the Sorts of Free(S,X))*the_arity_of o) by Th16;
then product ((NForms R)*the_arity_of o) c= Args(o,Free(S,X))
by PRALG_2:3;
then Den(o,Free(S,X)).y in Result(o,Free(S,X)) by FUNCT_2:5;
then reconsider a = Den(o,Free(S,X)).y as
Element of Free(S,X),the_result_sort_of o by FUNCT_2:15;
nf(a, R.the_result_sort_of o) in the set of all
nf(z, R.the_result_sort_of o)
where z is Element of Free(S,X), the_result_sort_of o;
then nf(a, R.the_result_sort_of o) in (NForms R).the_result_sort_of o
by Def19;
hence thesis by A4,FUNCT_2:15;
end;
hence f.i is Function of ((NForms R)#*the Arity of S).i,
((NForms R)*the ResultSort of S).i by A2,FUNCT_2:2;
end;
then reconsider f as ManySortedFunction of (NForms R)#*the Arity of S,
(NForms R)*the ResultSort of S;
reconsider A = MSAlgebra(#NForms R, f#) as
non-empty strict MSAlgebra over S by MSUALG_1:def 3;
take A;
thus the Sorts of A = NForms R;
let o be OperSymbol of S, a be Element of Args(o,A);
Args(o,A) = product ((the Sorts of A)*the_arity_of o) by PRALG_2:3;
hence Den(o,A).a = nf (Den(o,Free(S,X)).a, R.the_result_sort_of o) by A1;
end;
uniqueness
proof
let A1,A2 be non-empty strict MSAlgebra over S such that
A5: the Sorts of A1 = NForms R &
for o being OperSymbol of S, a being Element of Args(o,A1) holds
Den(o,A1).a = nf (Den(o,Free(S,X)).a, R.the_result_sort_of o) and
A6: the Sorts of A2 = NForms R &
for o being OperSymbol of S, a being Element of Args(o,A2) holds
Den(o,A2).a = nf (Den(o,Free(S,X)).a, R.the_result_sort_of o);
the Charact of A1 = the Charact of A2
proof
let o be OperSymbol of S;
A7: dom Den(o,A1) = Args(o,A1) & dom Den(o,A2) = Args(o,A2) by FUNCT_2:def 1;
now
let a be object;
assume a in Args(o,A1);
then Den(o,A1).a = nf(Den(o,Free(S,X)).a, R.the_result_sort_of o) &
Den(o,A2).a = nf(Den(o,Free(S,X)).a, R.the_result_sort_of o) by A5,A6;
hence Den(o,A1).a = Den(o,A2).a;
end;
hence thesis by A5,A6,A7,FUNCT_1:2;
end;
hence thesis by A5,A6;
end;
end;
theorem Th79:
for R being terminating with_UN_property invariant stable
ManySortedRelation of Free(S,X)
for a being SortSymbol of S
st x in (NForms R).a holds nf(x,R.a) = x
proof
let R be terminating with_UN_property invariant stable
ManySortedRelation of Free(S,X);
let a be SortSymbol of S;
assume x in (NForms R).a;
then x in the set of all nf(z,R.a) where z is Element of Free(S,X),a
by Def19;
then ex z being Element of Free(S,X),a st x = nf(z,R.a);
hence nf(x,R.a) = x by Th18;
end;
Lm3: now
let S,X;
let R be terminating with_UN_property invariant stable
ManySortedRelation of Free(S,X);
let o be OperSymbol of S;
set A = NFAlgebra R;
A1: the Sorts of A = NForms R by Def20;
(NForms R)*the_arity_of o qua ManySortedSet of dom the_arity_of o
c= (the Sorts of Free(S,X))*the_arity_of o
qua ManySortedSet of dom the_arity_of o
by Th15,PBOOLE:def 18;
then product ((NForms R)*the_arity_of o) c=
product((the Sorts of Free(S,X))*the_arity_of o) by Th16;
then product ((NForms R)*the_arity_of o) c= Args(o,Free(S,X))
by PRALG_2:3;
hence Args(o,A) c= Args(o,Free(S,X)) by A1,PRALG_2:3;
end;
theorem Th80:
for R being terminating with_UN_property invariant stable
ManySortedRelation of Free(S,X)
for g being ManySortedFunction of Free(S,X),Free(S,X)
st g is_homomorphism Free(S,X),Free(S,X)
for s being SortSymbol of S
for a being Element of Free(S,X),s holds
nf(g.s.nf(a,R.s), R.s) = nf(g.s.a, R.s)
proof
let R be terminating with_UN_property invariant stable
ManySortedRelation of Free(S,X);
let g be ManySortedFunction of Free(S,X),Free(S,X);
assume g is_homomorphism Free(S,X),Free(S,X);
then
A1: g is Endomorphism of Free(S,X) by MSUALG_6:def 2;
let s be SortSymbol of S;
let a be Element of Free(S,X),s;
nf(a,R.s) is_a_normal_form_of a,R.s by REWRITE1:54;
then
A2: R.s reduces a, nf(a,R.s);
defpred P[set] means nf(g.s.nf(a,R.s), R.s) = nf(g.s.$1, R.s);
A3: P[nf(a,R.s)];
A4: for b,c being set st [b,c] in R.s & P[c] holds P[b]
proof
let b,c be set;
assume A5: [b,c] in R.s;
then reconsider x = b, y = c as Element of Free(S,X),s by ZFMISC_1:87;
A6: [g.s.x,g.s.y] in R.s by A1,A5,MSUALG_6:def 9;
assume P[c];
hence P[b] by A6,REWRITE1:29,55;
end;
P[a] from B(A3,A2,A4);
hence nf(g.s.nf(a,R.s), R.s) = nf(g.s.a, R.s);
end;
theorem Th81:
for p being FinSequence holds p/^0 = p &
for i being Nat st i >= len p holds p/^i = {}
proof
let p be FinSequence;
A1: 0 <= len p by NAT_1:2;
A2: now
let i be Nat;
assume 1 <= i & i <= len(p/^0);
then i in dom(p/^0) by FINSEQ_3:25;
hence (p/^0).i = p.(i+0) by A1,RFINSEQ:def 1 .= p.i;
end;
len(p/^0) = len p - 0 by A1,RFINSEQ:def 1 .= len p;
hence p/^0 = p by A2;
let i be Nat;
assume i >= len p;
then i = len p & len (p /^ len p) = len p - len p or i > len p
by XXREAL_0:1,RFINSEQ:def 1;
hence p/^i = {} by RFINSEQ:def 1;
end;
theorem Th82:
for p,q being FinSequence holds (p^<*x*>^q)+*(len p+1,y) = p^<*y*>^q
proof
let p,q be FinSequence;
A1: dom (p^<*x*>^q) = Seg len(p^<*x*>^q) by FINSEQ_1:def 3
.= Seg(len(p^<*x*>)+len q) by FINSEQ_1:22
.= Seg(len p + len <*x*>+len q) by FINSEQ_1:22
.= Seg(len p+1+len q) by FINSEQ_1:40;
A2: dom (p^<*y*>^q) = Seg len(p^<*y*>^q) by FINSEQ_1:def 3
.= Seg(len(p^<*y*>)+len q) by FINSEQ_1:22
.= Seg(len p + len <*y*>+len q) by FINSEQ_1:22
.= Seg(len p+1+len q) by FINSEQ_1:40;
A3: dom((p^<*x*>^q)+*(len p+1,y)) = dom (p^<*x*>^q) by FUNCT_7:30;
now let a be object;
assume
A4: a in dom(p^<*x*>^q);
then reconsider i = a as Nat;
A5: i >= 1 & i <= len(p^<*x*>^q) by A4,FINSEQ_3:25;
per cases by XXREAL_0:1;
suppose
A6: i < len p+1;
then i <= len p by NAT_1:13;
then i in dom p & dom p c= dom(p^<*x*>) & dom p c= dom(p^<*y*>)
by A5,FINSEQ_1:26,FINSEQ_3:25;
then (p^<*x*>).i = p.i & (p^<*x*>^q).i = (p^<*x*>).i &
len p+1 <> i & (p^<*y*>).i = p.i & (p^<*y*>^q).i = (p^<*y*>).i
by A6,FINSEQ_1:def 7;
hence (p^<*x*>^q)+*(len p+1,y).a = (p^<*y*>^q).a by FUNCT_7:32;
end;
suppose
A7: i = len p+1;
len <*x*> = 1 & len <*y*> = 1 by FINSEQ_1:40;
then i >= 1 & len(p^<*x*>) = len p+1 & len(p^<*y*>) = len p+1
by A7,FINSEQ_1:22,NAT_1:11;
then i in dom (p^<*x*>) & i in dom(p^<*y*>) by A7,FINSEQ_3:25;
then (p^<*x*>^q).i = (p^<*x*>).i & (p^<*x*>).i = x &
(p^<*y*>^q).i = (p^<*y*>).i & (p^<*y*>).i = y by A7,FINSEQ_1:def 7,42;
hence (p^<*x*>^q)+*(len p+1,y).a = (p^<*y*>^q).a by A4,A7,FUNCT_7:31;
end;
suppose
A8: i > len p+1;
then i >= len p+1+1 by NAT_1:13;
then consider j being Nat such that
A9: i = len p+1+1+j by NAT_1:10;
A10: i = len p+1+(1+j) by A9;
len <*x*> = 1 & len <*y*> = 1 by FINSEQ_1:40;
then
A11: len(p^<*x*>) = len p+1 & len(p^<*y*>) = len p+1 by FINSEQ_1:22;
then len(p^<*x*>^q) = len p+1+len q by FINSEQ_1:22;
then 1 <= 1+j & 1+j <= len q by A10,A4,FINSEQ_3:25,XREAL_1:6,NAT_1:11;
then 1+j in dom q by FINSEQ_3:25;
then (p^<*x*>^q).i = q.(1+j) & (p^<*y*>^q).i = q.(1+j)
by A10,A11,FINSEQ_1:def 7;
hence (p^<*x*>^q)+*(len p+1,y).a = (p^<*y*>^q).a by A8,FUNCT_7:32;
end;
end;
hence (p^<*x*>^q)+*(len p+1,y) = p^<*y*>^q by A1,A2,A3;
end;
theorem Th83:
for p being FinSequence, i being Nat st i+1 <= len p
holds p|(i+1) = (p|i)^<*p.(i+1)*>
proof
let p be FinSequence;
let i be Nat;
assume A1: i+1 <= len p;
then
A2: len(p|(i+1)) = i+1 by FINSEQ_1:59;
i < len p by A1,NAT_1:13;
then
A3: len(p|i) = i & len <*p.(i+1)*> = 1 by FINSEQ_1:40,59;
then
A4: len((p|i)^<*p.(i+1)*>) = i+1 by FINSEQ_1:22;
thus len (p|(i+1)) = len ((p|i)^<*p.(i+1)*>) by A1,A4,FINSEQ_1:59;
let j be Nat;
assume
A5: 1 <= j & j <= len(p|(i+1));
per cases by A5,A2,NAT_1:8;
suppose
A6: j <= i;
A7: j in dom (p|i) by A3,A5,A6,FINSEQ_3:25;
thus (p|(i+1)).j = p.j by A2,A5,FINSEQ_1:1,FUNCT_1:49
.= (p|i).j by A6,A5,FINSEQ_1:1,FUNCT_1:49
.= ((p|i)^<*p.(i+1)*>).j by A7,FINSEQ_1:def 7;
end;
suppose
A8: j = i+1; then j >= 1 by NAT_1:11;
hence (p|(i+1)).j = p.(i+1) by A8,FINSEQ_1:1,FUNCT_1:49
.= ((p|i)^<*p.(i+1)*>).j by A3,A8,FINSEQ_1:42;
end;
end;
theorem Th84:
for p being FinSequence, i being Nat st i+1 <= len p
holds p/^i = <*p.(i+1)*>^(p/^(i+1))
proof
let p be FinSequence;
let i be Nat;
assume A1: i+1 <= len p;
then
A2: i < len p by NAT_1:13;
then
A3: len(p/^i) = len p-i by RFINSEQ:def 1;
len(<*p.(i+1)*>^(p/^(i+1))) = len <*p.(i+1)*>+len(p/^(i+1)) by FINSEQ_1:22
.= 1+len(p/^(i+1)) by FINSEQ_1:40 .= 1+(len p-(i+1)) by A1,RFINSEQ:def 1
.= len p-i;
hence len(p/^i) = len(<*p.(i+1)*>^(p/^(i+1))) by A2,RFINSEQ:def 1;
let j be Nat;
assume
A4: 1 <= j & j <= len(p/^i);
then
A5: j in dom(p/^i) by FINSEQ_3:25;
per cases by A4,XXREAL_0:1;
suppose
A6: j = 1;
hence (p/^i).j = p.(i+1) by A2,A5,RFINSEQ:def 1
.= (<*p.(i+1)*>^(p/^(i+1))).j by A6,FINSEQ_1:41;
end;
suppose
j > 1;
then j >= 1+1 by NAT_1:13;
then consider k being Nat such that
A7: j = 1+1+k by NAT_1:10;
A8: len <*p.(i+1)*> = 1 by FINSEQ_1:40;
A9: len(p/^(i+1)) = len p-(i+1) & len p-(i+1)+1 = len p-i & j = 1+k+1
by A1,A7,RFINSEQ:def 1;
then
1 <= 1+k & 1+k <= len(p/^(i+1)) by A3,A4,XREAL_1:6,NAT_1:11;
then
A10: 1+k in dom(p/^(i+1)) by FINSEQ_3:25;
thus (p/^i).j = p.(i+j) by A2,A5,RFINSEQ:def 1 .= p.(i+1+(1+k)) by A7
.= (p/^(i+1)).(1+k) by A1,A10,RFINSEQ:def 1
.= (<*p.(i+1)*>^(p/^(i+1))).j by A8,A10,A9,FINSEQ_1:def 7;
end;
end;
theorem Th85:
for R being terminating with_UN_property invariant stable
ManySortedRelation of Free(S,X)
for g being ManySortedFunction of Free(S,X),Free(S,X)
st g is_homomorphism Free(S,X),Free(S,X)
for h being ManySortedFunction of NFAlgebra R, NFAlgebra R
st for s being SortSymbol of S, x being Element of NFAlgebra R,s holds
h.s.x = nf(g.s.x,R.s)
for s being SortSymbol of S
for o being OperSymbol of S st s = the_result_sort_of o
for x being Element of Args(o,NFAlgebra R)
for y being Element of Args(o,Free(S,X)) st x = y holds
nf(Den(o,NFAlgebra R).(h#x),R.s) = nf(Den(o,Free(S,X)).(g#y),R.s)
proof
let R be terminating with_UN_property invariant stable
ManySortedRelation of Free(S,X);
let g be ManySortedFunction of Free(S,X),Free(S,X);
assume g is_homomorphism Free(S,X),Free(S,X);
let h be ManySortedFunction of NFAlgebra R, NFAlgebra R;
assume
A1: for s being SortSymbol of S, x being Element of NFAlgebra R,s holds
h.s.x = nf(g.s.x,R.s);
let s be SortSymbol of S;
let o be OperSymbol of S such that
A2: s = the_result_sort_of o;
let x be Element of Args(o,NFAlgebra R);
let y be Element of Args(o,Free(S,X)) such that
A3: x = y;
defpred P[Nat] means $1 <= len the_arity_of o implies
nf(Den(o,Free(S,X)).(((g#y)|$1)^((h#x)/^$1)),R.s)
= nf(Den(o,NFAlgebra R).(h#x),R.s);
dom(h#x) = dom the_arity_of o & dom(g#y) = dom the_arity_of o
by MSUALG_3:6;
then
A4: len(h#x) = len the_arity_of o & len(g#y) = len the_arity_of o
by FINSEQ_3:29;
(g#y)|0 = {} & (h#x)/^0 = h#x by Th81;
then
A5: ((g#y)|0)^((h#x)/^0) = h#x by FINSEQ_1:34;
A6: Args(o,NFAlgebra R) c= Args(o, Free(S,X)) & h#x in Args(o,NFAlgebra R)
by Lm3;
then reconsider hx = h#x as Element of Args(o,Free(S,X));
NForms R c= the Sorts of Free(S,X) & the Sorts of NFAlgebra R = NForms R
by Def20,PBOOLE:def 18;
then Result(o,Free(S,X)) = (the Sorts of Free(S,X)).s &
Result(o,NFAlgebra R) = (the Sorts of NFAlgebra R).s &
(the Sorts of NFAlgebra R).s c= (the Sorts of Free(S,X)).s &
Den(o,NFAlgebra R).(h#x) in Result(o,NFAlgebra R)
by A2,FUNCT_2:15;
then
reconsider Dx = Den(o,Free(S,X)).hx, Dnx = Den(o,NFAlgebra R).(h#x) as
Element of Free(S,X),s;
nf(nf(Dx,R.s),R.s) = nf(Dnx,R.s) by A2,Def20;
then
A7: P[0] by A5,Th18;
A8: now let i be Nat;
assume
A9: P[i];
thus P[i+1]
proof assume
A10: i+1 <= len the_arity_of o;
then
A11: i < len the_arity_of o by NAT_1:13;
A12: len ((h#x)|i) = i & len ((g#y)|i) = i by A4,A11,FINSEQ_1:59;
A13: (g#y)|(i+1) = ((g#y)|i)^<*(g#y).(i+1)*> by A4,A10,Th83;
A14: (h#x)/^i = <*(h#x).(i+1)*>^((h#x)/^(i+1)) by A4,A10,Th84;
A15: i+1 in dom the_arity_of o & dom ((the Sorts of NFAlgebra R)
*the_arity_of o) = dom the_arity_of o
by A10,NAT_1:11,FINSEQ_3:25,PRALG_2:3;
A16: x .(i+1) in ((the Sorts of NFAlgebra R)*the_arity_of o).(i+1) &
(the_arity_of o)/.(i+1) = (the_arity_of o).(i+1)
by A15,PARTFUN1:def 6,MSUALG_3:6;
then
reconsider xi1 = x .(i+1) as Element of
NFAlgebra R,(the_arity_of o)/.(i+1) by A15,FUNCT_1:13;
dom x = dom the_arity_of o by MSUALG_3:6;
then (h#x).(i+1) = h.((the_arity_of o)/.(i+1)).xi1 by A15
,MSUALG_3:def 6
.= nf(g.((the_arity_of o)/.(i+1)).xi1,R.((the_arity_of o)/.(i+1)))
by A1;
then hx.(i+1) is_a_normal_form_of g.((the_arity_of o)/.(i+1)).xi1,
R.((the_arity_of o)/.(i+1)) by REWRITE1:54;
then
A17: R.((the_arity_of o)/.(i+1)) reduces g.((the_arity_of o)/.(i+1)).xi1,
hx.(i+1);
A18: dom(h#x) = dom the_arity_of o by MSUALG_3:6;
then
A19: len (h#x) = len the_arity_of o by FINSEQ_3:29;
defpred Q[set] means
nf((Den(o,Free(S,X)).(((g#y)|i)^<*$1*>^((h#x)/^(i+1)))),R.s)
= nf((Den(o,NFAlgebra R).(h#x)),R.s);
A20: Q[hx.(i+1)] by A9,A10,NAT_1:13,A14,FINSEQ_1:32;
A21: for a,b being set st [a,b] in R.((the_arity_of o)/.(i+1)) & Q[b]
holds Q[a]
proof
let a,b be set;
assume A22: [a,b] in R.((the_arity_of o)/.(i+1));
then reconsider c = a, d = b as Element of (the Sorts of Free(S,X))
.((the_arity_of o)/.(i+1)) by ZFMISC_1:87;
reconsider j = i+1 as Element of NAT by ORDINAL1:def 12;
set f = transl(o,j,((g#y)|i)^<*d*>^((h#x)/^(i+1)),Free(S,X));
now
A23: len(((g#y)|i)^<*d*>) = i+len<*d*> by A12,FINSEQ_1:22
.= i+1 by FINSEQ_1:40;
thus
A24: dom (((the Sorts of Free(S,X))*the_arity_of o))
= dom the_arity_of o by PRALG_2:3;
len (((g#y)|i)^<*d*>^((h#x)/^(i+1))) = len(((g#y)|i)^<*d*>)+
len((h#x)/^(i+1)) by FINSEQ_1:22
.= i+1+(len (h#x) - (i+1)) by A10,A19,A23,RFINSEQ:def 1
.= len the_arity_of o by A18,FINSEQ_3:29;
hence dom (((the Sorts of Free(S,X))*the_arity_of o))
= dom (((g#y)|i)^<*d*>^((h#x)/^(i+1))) by A24,FINSEQ_3:29;
let a be object;
assume
A25: a in dom the_arity_of o;
then reconsider b = a as Nat;
A26: b <= len the_arity_of o & b >= 1 by A25,FINSEQ_3:25;
per cases by NAT_1:8;
suppose
A27: b <= i;
then
A28: b in dom((g#y)|i) & dom((g#y)|i) c= dom(((g#y)|i)^<*d*>) &
b in Seg i by A26,A12,FINSEQ_3:25,FINSEQ_1:26;
then (((g#y)|i)^<*d*>^((h#x)/^(i+1))).a = (((g#y)|i)^<*d*>).a
by FINSEQ_1:def 7 .= ((g#y)|i).a by A28,FINSEQ_1:def 7
.= (g#y).a by A27,A26,FINSEQ_1:1,FUNCT_1:49;
hence (((g#y)|i)^<*d*>^((h#x)/^(i+1))).a
in ((the Sorts of Free(S,X))*the_arity_of o).a
by A24,A25,MSUALG_3:6;
end;
suppose
A29: b = i+1;
then b in dom(((g#y)|i)^<*d*>) by A26,A23,FINSEQ_3:25;
then (((g#y)|i)^<*d*>^((h#x)/^(i+1))).a = (((g#y)|i)^<*d*>).a
by FINSEQ_1:def 7 .= d by A12,A29,FINSEQ_1:42;
then (((g#y)|i)^<*d*>^((h#x)/^(i+1))).a
in (the Sorts of Free(S,X)).((the_arity_of o)/.(i+1));
hence (((g#y)|i)^<*d*>^((h#x)/^(i+1))).a
in ((the Sorts of Free(S,X))*the_arity_of o).a
by A16,A25,A29,FUNCT_1:13;
end;
suppose
A30: b > i+1;
then consider k being Nat such that
A31: b = i+1+k by NAT_1:10;
i+1+k > i+1+0 by A30,A31;
then k > 0 & b-(i+1) <= (len the_arity_of o)-(i+1)
by A26,XREAL_1:9,6;
then k >= 0+1 & k <= len((h#x)/^(i+1))
by A10,A19,RFINSEQ:def 1,A31,NAT_1:13;
then
A32: k in dom((h#x)/^(i+1)) by FINSEQ_3:25;
then (((g#y)|i)^<*d*>^((h#x)/^(i+1))).a = ((h#x)/^(i+1)).k
by A23,A31,FINSEQ_1:def 7 .= (h#x).a by A31,A19,A32,A10
,RFINSEQ:def 1;
hence (((g#y)|i)^<*d*>^((h#x)/^(i+1))).a
in ((the Sorts of Free(S,X))*the_arity_of o).a
by A24,A25,A6,MSUALG_3:6;
end;
end;
then
A33: ((g#y)|i)^<*d*>^((h#x)/^(i+1))
in product ((the Sorts of Free(S,X))*the_arity_of o) by CARD_3:9;
then
((g#y)|i)^<*d*>^((h#x)/^(i+1)) in Args(o,Free(S,X)) by PRALG_2:3;
then
A34: [f.c,f.d] in R.s by A2,A15,A22,MSUALG_6:def 5,def 8;
reconsider ad = ((g#y)|i)^<*d*>^((h#x)/^(i+1)) as Element of
Args(o,Free(S,X)) by A33,PRALG_2:3;
reconsider Dd = Den(o,Free(S,X)).ad as Element of Free(S,X),s
by A2,FUNCT_2:15;
A35: f.c = Den(o,Free(S,X)).((((g#y)|i)^<*d*>^((h#x)/^(i+1)))+*(j,c))
by MSUALG_6:def 4
.= Den(o,Free(S,X)).(((g#y)|i)^<*c*>^((h#x)/^(i+1))) by A12,Th82;
f.d = Den(o,Free(S,X)).((((g#y)|i)^<*d*>^((h#x)/^(i+1)))+*(j,d))
by MSUALG_6:def 4
.= Den(o,Free(S,X)).(((g#y)|i)^<*d*>^((h#x)/^(i+1))) by A12,Th82;
then
A36: (Den(o,Free(S,X)).(((g#y)|i)^<*c*>^((h#x)/^(i+1)))),
(Den(o,Free(S,X)).(((g#y)|i)^<*d*>^((h#x)/^(i+1))))
are_convertible_wrt R.s by A34,A35,REWRITE1:29;
assume Q[b];
hence Q[a] by A36,REWRITE1:55;
end;
A37: Q[g.((the_arity_of o)/.(i+1)).xi1] from B(A20,A17,A21);
dom y = dom the_arity_of o by MSUALG_3:6;
hence
nf((Den(o,Free(S,X)).(((g#y)|(i+1))^((h#x)/^(i+1)))),R.s)
= nf((Den(o,NFAlgebra R).(h#x)),R.s) by A13,A3,A15,A37,MSUALG_3:def 6;
end;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A7,A8);
then
A38: nf(Den(o,Free(S,X)).(((g#y)|len the_arity_of o)^
((h#x)/^len the_arity_of o)),R.s)
= nf(Den(o,NFAlgebra R).(h#x),R.s);
(g#y)|len the_arity_of o = g#y & (h#x)/^len the_arity_of o = {}
by A4,FINSEQ_1:58,Th81;
hence thesis by A38,FINSEQ_1:34;
end;
registration
let S,X;
let R be terminating with_UN_property invariant stable
ManySortedRelation of Free(S,X);
cluster NFAlgebra R -> (X,S)-terms;
coherence
proof set A = NFAlgebra R;
the Sorts of A = NForms R by Def20;
hence the Sorts of A is ManySortedSubset of the Sorts of Free(S,X);
end;
end;
registration
let S,X;
let R be NF-var terminating with_UN_property invariant stable
ManySortedRelation of Free(S,X);
cluster NFAlgebra R -> all_vars_including inheriting_operations
free_in_itself;
coherence
proof set A = NFAlgebra R;
A1: the Sorts of A = NForms R by Def20;
thus FreeGen X is ManySortedSubset of the Sorts of A
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
let x be object; assume
A2: x in (FreeGen X).i;
Free(S,X) = FreeMSA X by MSAFREE3:31;
then (FreeGen X).s c= (the Sorts of Free(S,X)).s by PBOOLE:def 2,def 18;
then reconsider x as Element of Free(S,X),s by A2;
x is_a_normal_form_wrt R.s & R.s reduces x,x by A2,Def18,REWRITE1:12;
then x is_a_normal_form_of x,R.s & nf(x,R.s) is_a_normal_form_of x,R.s
by REWRITE1:54;
then x = nf(x,R.s) &
(NForms R).s = the set of all nf(y,R.s) where y is Element of Free(S,X),s
by Def19,REWRITE1:53;
hence thesis by A1;
end;
hereby
let o be OperSymbol of S, p be FinSequence;
assume
A3: p in Args(o, Free(S,X)) &
Den(o,Free(S,X)).p in (the Sorts of A).the_result_sort_of o;
then
A4: dom p = dom the_arity_of o &
dom ((the Sorts of Free(S,X))*the_arity_of o)
= dom the_arity_of o by MSUALG_3:6,PRALG_2:3;
reconsider q = p as FinSequence;
Den(o,Free(S,X)).p in the set of all
nf(z,R.the_result_sort_of o) where z is Element of
(the Sorts of Free(S,X)).the_result_sort_of o
by A1,A3,Def19;
then consider z being Element of (the Sorts of Free(S,X))
.the_result_sort_of o such that
A5: Den(o,Free(S,X)).p = nf(z,R.the_result_sort_of o);
A6: Den(o,Free(S,X)).p is_a_normal_form_of z, R.the_result_sort_of o
by A5,REWRITE1:54;
A7: now
let i be object; assume
A8: i in dom p;
then
A9: (the Sorts of Free(S,X)).((the_arity_of o).i) =
((the Sorts of Free(S,X))*the_arity_of o).i by A4,FUNCT_1:13;
reconsider j = i as Element of NAT by A8;
reconsider ai = (the_arity_of o).i as SortSymbol of S
by A4,A8,FUNCT_1:102;
A10: ai = (the_arity_of o)/.j by A8,A4,PARTFUN1:def 6;
Args(o,Free(S,X)) = product ((the Sorts of Free(S,X))*the_arity_of o)
by PRALG_2:3;
then reconsider pj = p.i as Element of
(the Sorts of Free(S,X)).((the_arity_of o).i) by A3,A9,A8,A4,CARD_3:9;
assume p.i nin ((NForms R)*the_arity_of o).i;
then p.i nin (NForms R).((the_arity_of o).i) by A4,A8,FUNCT_1:13;
then pj nin the set of all
nf(b,R.((the_arity_of o)/.i)) where b is Element of
(the Sorts of Free(S,X)).((the_arity_of o)/.i)
by A10,Def19;
then nf(pj,R.((the_arity_of o).i)) is_a_normal_form_of pj,
R.((the_arity_of o).i) &
for a being Element of (the Sorts of Free(S,X)).
((the_arity_of o).i) holds pj <> nf(a,R.((the_arity_of o).i))
by A10,REWRITE1:54;
then R.((the_arity_of o).i) reduces pj,nf(pj,R.((the_arity_of o).i))
& nf(pj,R.((the_arity_of o).i)) <> pj;
then consider x being object such that
A11: [pj,x] in R.((the_arity_of o).i) by REWRITE1:33,def 5;
reconsider x as Element of
(the Sorts of Free(S,X)).((the_arity_of o).i) by A11,ZFMISC_1:87;
set f = transl(o,j,q,Free(S,X));
A12: f.pj = Den(o,Free(S,X)).(q+*(j,pj)) by A10,MSUALG_6:def 4
.= Den(o,Free(S,X)).p by FUNCT_7:35;
[f.pj,f.x] in R.the_result_sort_of o
by A11,A3,A8,A4,A10,MSUALG_6:def 5,def 8;
hence contradiction by A6,A12,REWRITE1:def 5;
end;
dom ((NForms R)*the_arity_of o) = dom the_arity_of o by A1,PRALG_2:3;
then p in product ((NForms R)*the_arity_of o) by A4,A7,CARD_3:9;
hence p in Args(o,A) by A1,PRALG_2:3;
hence Den(o,A).p
= nf(Den(o,Free(S,X)).p,R.the_result_sort_of o) by Def20
.= Den(o,Free(S,X)).p by A6,Th17;
end;
let f be ManySortedFunction of FreeGen X, the Sorts of A;
let G be ManySortedSubset of the Sorts of A; assume
A13: G = FreeGen X;
reconsider H = FreeGen X as GeneratorSet of Free(S,X) by MSAFREE3:31;
the Sorts of NFAlgebra R = NForms R & H is_transformable_to NForms R &
H is_transformable_to the Sorts of Free(S,X) by Def20,Th21;
then
A14: the Sorts of A c= the Sorts of Free(S,X) & rngs f c= the Sorts of A &
doms f = H by MSSUBFAM:17,PBOOLE:def 18;
then rngs f c= the Sorts of Free(S,X) & FreeMSA X = Free(S,X)
by PBOOLE:13,MSAFREE3:31;
then f is ManySortedFunction of H, the Sorts of Free(S,X) &
H is free by A14,Th21,EQUATION:4;
then consider g being ManySortedFunction of Free(S,X),Free(S,X) such that
A15: g is_homomorphism Free(S,X),Free(S,X) & g||H = f;
deffunc F(SortSymbol of S, Element of A,$1) = nf(g.$1.$2, R.$1);
defpred P[object,object,object] means $3 = nf(g.$1.$2, R.$1);
A16: for s,x being object
st s in the carrier of S & x in (the Sorts of A).s
ex y being object st y in (the Sorts of A).s & P[s,x,y]
proof
let s,x be object;
assume A17: s in the carrier of S;
assume A18: x in (the Sorts of A).s;
reconsider t = s as SortSymbol of S by A17;
reconsider z = x as Element of A,t by A18;
take y = F(t,z);
(NForms R).t c= (the Sorts of Free(S,X)).t by PBOOLE:def 2,def 18;
then reconsider a = g.t.z as Element of Free(S,X),t by A1,FUNCT_2:5;
y = nf(a, R.t);
then y in the set of all nf(u,R.t) where u is Element of Free(S,X),t;
hence y in (the Sorts of A).s by A1,Def19;
thus P[s,x,y];
end;
consider h being ManySortedFunction of A,A such that
A19: for s, x being object
st s in the carrier of S & x in (the Sorts of A).s
holds
h.s.x in (the Sorts of A).s & P[s,x,h.s.x] from YELLOW18:sch 23(A16);
take h;
thus h is_homomorphism A,A
proof
let o be OperSymbol of S; assume
Args(o,A) <> {};
let x be Element of Args(o,A);
(NForms R)*the_arity_of o qua ManySortedSet of dom the_arity_of o
c= (the Sorts of Free(S,X))*the_arity_of o
qua ManySortedSet of dom the_arity_of o
by Th15,PBOOLE:def 18;
then product ((NForms R)*the_arity_of o) c=
product((the Sorts of Free(S,X))*the_arity_of o) by Th16;
then product ((NForms R)*the_arity_of o) c= Args(o,Free(S,X))
by PRALG_2:3;
then Args(o,A) c= Args(o,Free(S,X)) & x in Args(o,A) by A1,PRALG_2:3;
then reconsider y = x as Element of Args(o,Free(S,X));
A20: for s being SortSymbol of S, x being Element of NFAlgebra R,s holds
h.s.x = nf(g.s.x,R.s) by A19;
reconsider Dy = Den(o,Free(S,X)).y as
Element of Free(S,X),the_result_sort_of o by FUNCT_2:15;
Den(o,A).x in Result(o,A);
then Den(o,A).x in (the Sorts of A).the_result_sort_of o
by FUNCT_2:15;
hence h.(the_result_sort_of o).(Den(o,A).x)
= nf(g.(the_result_sort_of o).(Den(o,A).x), R.(the_result_sort_of o))
by A19
.= nf(g.(the_result_sort_of o).nf(Den(o,Free(S,X)).x,
R.(the_result_sort_of o)), R.(the_result_sort_of o)) by Def20
.= nf(g.(the_result_sort_of o).(Dy),
R.(the_result_sort_of o)) by A15,Th80
.= nf(Den(o,Free(S,X)).(g#y), R.(the_result_sort_of o))
by A15
.= nf(Den(o,A).(h#x), R.(the_result_sort_of o)) by A15,A20,Th85
.= nf(nf(Den(o,Free(S,X)).(h#x), R.(the_result_sort_of o)),
R.the_result_sort_of o) by Def20
.= nf(Den(o,Free(S,X)).(h#x), R.(the_result_sort_of o)) by Th18
.= Den(o,A).(h#x) by Def20;
end;
let a be Element of S;
A21: dom(f.a) = H.a & dom((h||G).a) = G.a by FUNCT_2:def 1;
hence dom(f.a) = dom((h||G).a) by A13;
let x be object;
assume
A22: x in dom(f.a);
A23: G.a c= (the Sorts of A).a by PBOOLE:def 2,def 18;
reconsider fax = f.a.x as Element of A,a by A22,FUNCT_2:5;
the Sorts of A = NForms R by Def20;
hence f.a.x = nf(fax,R.a) by Th79
.= nf(((g.a)|(H.a)).x,R.a) by A15,MSAFREE:def 1
.= nf(g.a.x,R.a) by A22,FUNCT_1:49
.= h.a.x by A23,A13,A21,A22,A19
.= ((h.a)|(G.a)).x by A13,A22,FUNCT_1:49
.= (h||G).a.x by MSAFREE:def 1;
end;
end;