:: Free Term Algebras
:: by Grzegorz Bancerek
::
:: Received May 15, 2012
:: Copyright (c) 2012 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, REAL_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, ZFMISC_1, 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;
requirements BOOLE, SUBSET, ARITHM, NUMERALS;
definitions TARSKI, XBOOLE_0, FUNCT_1, PARTFUN1, FUNCOP_1, FINSET_1, FINSEQ_1,
PROB_2, TREES_9, REWRITE1, 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, MCART_1, 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 Lemma1:
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 Z0: f1 c= f2;
let x be element;
assume x in Union f1; then
consider y being set such that
A1: y in dom f1 & x in f1.y by CARD_5:2;
A2: dom f1 = I & dom f2 = I by PARTFUN1:def 2;
f1.y c= f2.y by Z0,A1,PBOOLE:def 2;
hence x in Union f2 by A1,A2,CARD_5:2;
end;
reserve x,y,z for element, 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;
coherence
proof let a be Element of A;
per cases;
suppose I = {}; then
A2: rng X = {} & X = {} & Union({}-->I) = {} by FUNCT_6:26;
thus thesis by A2,SUBSET_1:def 1;
end;
suppose I <> {}; then
consider x being element such that
A3: x in dom X & A = X.x by FUNCT_1:def 3;
thus thesis by A3,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;
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;
Lem1:
now
let I be set;
let X,Y be ManySortedSet of I;
let f be ManySortedFunction of X,Y;
let x be set;
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 set;
redefine func f.x -> Function of X.x,Y.x;
coherence by Lem1;
end;
scheme Sch1{I()-> set, A()->non-empty ManySortedSet of I(),
F(element,element)->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[element,element] 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 st x in I() ex y st P[x,y]
proof
let x; assume
A2: x in I();
then reconsider s = x as Element of I();
deffunc G(element) = F(x,$1);
consider f being Function such that
A3: dom f = A().x & for y 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 st x in I() holds P[x,g.x] from CLASSES1:sch 1(A1);
g is Function-yielding
proof
let x; 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(element,element) -> 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
A: for i being Element of I() for a being Element of A().i
holds F(i,a) in B().i
proof
defpred P[element,element,element] means $1 = F($3,$2);
A1: for i be element st i in I() holds for x st x in A().i
ex y st y in B().i & P[y,x,i] by A;
consider F be ManySortedFunction of A(), B() such that
A2: for i be element st i in I() ex f be Function of A().i, B().i
st f = F.i & for x st x in A().i holds P[f.x,x,i]
from MSSUBFAM:sch 1(A1);
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
A3: f = F.i & for x st x in A().i holds P[f.x,x,i] by A2;
thus F.i.a = F(i,a) by A3;
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;
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 RELAT_1:27,PARTFUN1:def 2,FINSEQ_1:def 4;
hence ex n being Nat st dom(F*p) = Seg n by FINSEQ_1:def 2;
end;
end;
theorem Lem3:
Subtrees root-tree x = {root-tree x}
proof
A2: dom root-tree x = {{}} by TREES_4:3,TREES_1:29;
thus Subtrees root-tree x c= {root-tree x}
proof
let y be element; assume y in Subtrees root-tree x; then
consider p being Element of dom root-tree x such that
A1: y = (root-tree x)|p;
p = {} by A2,TARSKI:def 1;
then y = root-tree x by A1,TREES_9:1;
hence thesis by TARSKI:def 1;
end;
reconsider p = {} as Element of dom root-tree x by A2,TARSKI:def 1;
let y be element; 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 Lem4:
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 element; 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
A6: n+1 in dom p by FINSEQ_3:25;
then
A5: 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,A6,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 A5;
hence thesis by XBOOLE_0:def 3;
end;
end;
let z be element; assume z in {x-tree p} \/ Subtrees rng p;
then
A6: 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 A6,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
A7: z = t|q;
consider y such that
A8: y in dom p & t = p.y by FUNCT_1:def 3;
reconsider y as Nat by A8;
consider n being Nat such that
A9: y = 1+n by A8,FINSEQ_3:25,NAT_1:10;
reconsider n as Element of NAT by ORDINAL1:def 12;
y <= len p by A8,FINSEQ_3:25;
then
AC: n < len p by A9,NAT_1:13;
then
AA: t = (x-tree p)|<*n*> by A8,A9,TREES_4:def 4;
AB: tree doms p = dom(x-tree p) by TREES_4:10;
dom t = (doms p).y & len doms p = len p by A8,FUNCT_6:22,TREES_3:38;
then
AD: <*n*>^q in dom(x-tree p) by A9,AC,AB,TREES_3:def 15;
then z = (x-tree p)|(<*n*>^q) by A7,AA,TREES_9:3;
hence thesis by AD;
end;
end;
theorem Lem5:
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 Lem3;
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 being set; assume x in rng <*t*>;
then x in {t} by FINSEQ_1:39;
hence x is finite;
end;
hence thesis by FINSET_1:def 2;
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 being set; assume x in rng <*t*>;
then x in {t} by FINSEQ_1:39;
hence x is finite;
end;
hence thesis by FINSET_1:def 2;
end;
thus thesis;
end;
end;
registration
let f be finite-yielding Function-yielding Function;
cluster doms f -> finite-yielding;
coherence
proof
now
let y being set; assume y in rng doms f;
then consider x such that
A0: x in dom doms f & y = (doms f).x by FUNCT_1:def 3;
x in dom f by A0,FUNCT_6:def 2;
then
A1: x in dom f & f.x is Function & y = proj1(f.x) by A0,FUNCT_6:def 2;
thus y is finite by A1;
end;
hence thesis by FINSET_1:def 2;
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};
A0: tree p c= {{}}\/union X
proof
let x be element; assume
B1: x in tree p;
reconsider xx=x as set by TARSKI:1;
per cases by B1,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
B2: n < len p & q in p.(n+1) & x = <*n*>^q;
1 <= n+1 & n+1 <= len p by B2,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 B2;
then q in NAT* by FINSEQ_1:def 11;
then
B3: x in {<*n*>^w where w is Element of NAT*: w in p.(n+1)} by B2;
{<*n*>^w where w is Element of NAT*: w in p.(n+1)} in X by B2;
then x in union X by B3,TARSKI:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
deffunc F(element) = {<*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
B4: dom f = dom p & for x st x in dom p holds f.x = F(x)
from FUNCT_1:sch 3;
AA: rng f = X
proof
thus rng f c= X
proof let x;
reconsider xx=x as set by TARSKI:1;
assume x in rng f;
then consider y such that
B5: y in dom f & x = f.y by FUNCT_1:def 3;
B6: x = F(y) by B4,B5;
reconsider y as Element of NAT by B4,B5;
consider i being Nat such that
B7: y = 1+i by B4,B5,FINSEQ_3:25,NAT_1:10;
y <= len p by B4,B5,FINSEQ_3:25;
then
B8: i < len p by B7,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 element; assume z in xx;
then consider q being (Element of NAT*), j being Nat such that
B9: z = <*j*>^q & i+1 = j+1 & q in p.(j+1) by B6,B7;
thus thesis by B9;
end;
let z be element;
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
C1: z = <*i*>^q & q in p.(i+1);
thus thesis by B6,B7,C1;
end;
hence x in X by B8;
end;
let x;
reconsider xx=x as set by TARSKI:1;
assume x in X;
then consider i being Nat such that
C2: x = {<*i*>^q where q is Element of NAT*: q in p.(i+1)} & i < len p;
C3: xx = F(i+1)
proof
thus xx c= F(i+1)
proof
let z be element; assume z in xx;
then consider q being Element of NAT* such that
C4: z = <*i*>^q & q in p.(i+1) by C2;
thus z in F(i+1) by C4;
end;
let z be element; assume z in F(i+1);
then consider q being (Element of NAT*), j being Nat such that
C5: z = <*j*>^q & i+1 = j+1 & q in p.(j+1);
thus z in xx by C2,C5;
end;
C5: i+1 >= 1 & i+1 <= len p by C2,NAT_1:11,13;
then
C4: i+1 in dom f by B4,FINSEQ_3:25;
f.(i+1) = x by B4,C3,C5,FINSEQ_3:25;
hence x in rng f by C4,FUNCT_1:def 3;
end;
now let x be set; assume x in X;
then consider i being Nat such that
C2: 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 C2,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
C6: dom g = t & for x being Element of t holds g.x = G(x) from FUNCT_1:sch 4;
C8: x c= rng g
proof
let z be element; assume z in x;
then consider q being Element of NAT* such that
C7: z = <*i*>^q & q in p.(i+1) by C2;
z = g.q by C6,C7;
hence thesis by C6,C7,FUNCT_1:def 3;
end;
rng g is finite by C6,FINSET_1:8;
hence x is finite by C8;
end;
then union X is finite by AA,B4,FINSET_1:7,8;
hence tree p is finite by A0;
end;
end;
registration
let t be finite DecoratedTree;
cluster Subtrees t -> finite-membered;
coherence
proof
let x be set; assume x in Subtrees t;
hence thesis;
end;
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 Lem7a:
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
A3: 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 A3,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 A3,XXREAL_0:2;
end;
theorem Lem7:
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 such that
A7: z in dom p & t = p.z by A2,FUNCT_1:def 3;
reconsider z as Nat by A7;
consider i such that
A8: z = 1+i by A7,FINSEQ_3:25,NAT_1:10;
reconsider i as Element of NAT by ORDINAL1:def 12;
z <= len p by A7,FINSEQ_3:25;
then
A9: i < len p by A8,NAT_1:13;
B1: dom (y-tree p) = tree doms p by TREES_4:10;
B2: len doms p = len p by TREES_3:38;
B3: dom t = (doms p).z by A7,FUNCT_6:22;
consider h being FinSequence of NAT such that
B4: h in dom t & len h = height dom t by TREES_1:def 12;
<*i*>^h in dom (y-tree p) by A8,A9,B1,B2,B3,B4,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,Lem7a,B4,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;
now
let x be set; assume
A1: x in rng f;
x in S-Terms X by A1;
then reconsider y = x as DecoratedTree of the carrier of DTConMSA X;
thus x is finite by A1;
end;
hence thesis by FINSET_1:def 2;
end;
end;
theorem Lem8:
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 element; 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 Lem9:
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 element; 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 Lem10:
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 Lem11:
for p being DTree-yielding FinSequence holds
rng p c= Subtrees (x-tree p)
proof
let p be DTree-yielding FinSequence;
let z be element; assume z in rng p;
then consider y 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 Lem12:
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 Th33:
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; assume
A1: x in I; reconsider x as set by TARSKI:1;
(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 Z0: A c= B;
let f be Function of J,I;
let j be element;
assume A1: 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 Z0,A1,PBOOLE:def 2,FUNCT_2:5;
end;
theorem Lem15:
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 Z0: A c= B;
let f be FinSequence of I;
let j be element;
assume A1: 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 Z0,A1,PBOOLE:def 2,FUNCT_1:102;
end;
theorem Lem14:
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 Z0: A c= B;
let x be element; assume x in product A; then
consider g being Function such that
A1: x = g & dom g = dom A & for y st y in dom A holds g.y in A.y
by CARD_3:def 5;
A2: dom A = I & dom B = I by PARTFUN1:def 2;
now let y; assume y in I; then
g.y in A.y & A.y c= B.y by Z0,A1,A2,PBOOLE:def 2;
hence g.y in B.y;
end;
hence x in product B by A1,A2,CARD_3:9;
end;
theorem Lem16:
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 Z0: x is_a_normal_form_wrt R;
A0: x is set by TARSKI:1;
A1: x is_a_normal_form_of x,R by Z0,REWRITE1:12,def 6;
then
A2: x has_a_normal_form_wrt R by REWRITE1:def 11;
for b,c being element 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 A0,A1,A2,REWRITE1:def 12;
end;
theorem Lem16a:
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
A2: nf(x,R) is_a_normal_form_wrt R & R reduces nf(x,R),nf(x,R)
by REWRITE1:def 6,12;
then
A1: nf(x,R) is_a_normal_form_of nf(x,R),R by REWRITE1:def 6;
nf(x,R) has_a_normal_form_wrt R &
for b,c being element 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 A2,REWRITE1:def 6,def 11,53;
hence nf(nf(x,R),R) = nf(x,R) by A1,REWRITE1:def 12;
end;
registration
let S, X;
let A be MSSubset of FreeMSA X;
let x;
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: COUNT:
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
proof
let f be ManySortedSet of I;
assume
A1: f = I-->X;
let x; assume x in I;
hence thesis by A1,FUNCOP_1:7;
end;
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 element;
cluster X.x -> countable;
coherence
proof
x in I or x nin dom X;
hence thesis by COUNT,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(element) = the one-to-one Function of X0.$1, NAT;
consider f being ManySortedSet of I such that
A1: for x being element st x in I holds f.x = F(x) from PBOOLE:sch 4;
f is ManySortedFunction of X0, I-->NAT
proof
let x be set; 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 be set; let g be Function;
assume x in dom f;
then f.x = F(x) by A1;
hence thesis;
end;
end;
theorem Th44:
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 element; reconsider a = x as set by TARSKI:1;
assume x in S;
then (rngs w).x = rng(w.a) 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(element) = the Enumeration of X.$1;
consider w being ManySortedSet of S such that
A2: for s being element st s in S holds w.s = F(s) from PBOOLE:sch 4;
w is Function-yielding
proof
let x; assume x in dom w;
then w.x = F(x) by A2;
hence thesis;
end;
then reconsider w as ManySortedFunction of S;
w is ManySortedFunction of X,Y
proof
let x be set; assume
A3: x in S;
BB: card (X.x) c= NAT by CARD_3:def 14;
B0: w.x = F(x) by A2,A3;
then
B1: dom (w.x) = X.x by AOFA_I00:6;
B3: Y.x = NAT by A3,FUNCOP_1:7;
rng (w.x) c= Y.x by B0,BB,B3,AOFA_I00:6;
hence thesis by B1,FUNCT_2:2;
end;
then reconsider w as ManySortedFunction of X,Y;
reconsider Z = rngs w as ManySortedSubset of Y by Th44;
take Z,w;
thus w is "1-1"
proof
let x be set; let f be Function;
assume x in dom w;
then w.x = F(x) by A2;
hence thesis;
end;
thus Z = rngs w;
let x; assume x in S;
then w.x = F(x) & Z.x = rng(w.x) by A2,MSSUBFAM:13;
hence w.x is Enumeration of X.x & Z.x = card(X.x) by AOFA_I00:6;
end;
theorem Th96:
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;
now let i be set; assume i in I;
hence B.i = {} implies A.i = {};
end;
hence A is_transformable_to B by PZFMISC1:def 3;
end;
theorem Th108:
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 Z0: B c= C;
let x be set; assume
A0: x in I; then
A1: f.x is Function of A.x,B.x & B.x <> {} & B.x c= C.x
by Z0,PBOOLE:def 2;
dom(f.x) = A.x & rng(f.x) c= B.x
by A0,FUNCT_2:def 1;
hence f.x is Function of A.x,C.x by A1,XBOOLE_1:1,FUNCT_2:2;
end;
theorem Th39:
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 Z1: A is_transformable_to B;
let f be ManySortedFunction of A,B;
assume Z0: f is "onto";
deffunc F(element) = the rng-retract of f.$1;
consider g being ManySortedSet of I such that
A1: for i being element st i in I holds g.i = F(i) from PBOOLE:sch 4;
g is Function-yielding
proof
let x; assume x in dom g; then
g.x = F(x) by A1;
hence thesis;
end; then
reconsider g as ManySortedFunction of I;
g is ManySortedFunction of B,A
proof
let x be set; assume
A2: x in I; then
A3: g.x = F(x) by A1; then
A4: dom (g.x) = rng (f.x) & rng (f.x) = B.x
by Z0,A2,MSUALG_3:def 3,ALGSPEC1:def 2;
A.x <> {} implies B.x <> {} by A2,Z1,PZFMISC1:def 3; then
A5: dom (f.x) = A.x by FUNCT_2:def 1;
A6: (f.x)*(g.x) = id (B.x) & dom id (B.x) = B.x
by A3,A4,ALGSPEC1:def 2;
rng (g.x) c= dom (f.x)
proof let y be element;
assume y in rng (g.x); then
consider z such that
A7: z in dom (g.x) & y = (g.x).z by FUNCT_1:def 3;
thus y in dom (f.x) by A4,A6,A7,FUNCT_1:11;
end;
hence thesis by A4,A5,FUNCT_2:2;
end; then
reconsider g as ManySortedFunction of B,A;
take g;
now let x;
assume
A8: x in I; then
g.x = F(x) by A1; then
(f.x)*(g.x) = id rng (f.x) & dom (g.x) = rng (f.x) & rng (f.x) = B.x
by Z0,A8,MSUALG_3:def 3,ALGSPEC1:def 2;
hence (f**g).x = id (B.x) by A8,MSUALG_3:2
.= (id B).x by A8,MSUALG_3:def 1;
end;
hence f**g = id B by PBOOLE:3;
end;
Lem2:
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 Th77:
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
proof
let A1,A2 be MSAlgebra over S;
assume Z0: the MSAlgebra of A1 = the MSAlgebra of A2;
let B1 be MSSubset of A1;
let B2 be MSSubset of A2;
assume Z1: B1 = B2;
let o be OperSymbol of S;
assume
rng((Den(o,A1))|((B1#*the Arity of S).o)) c= (B1*the ResultSort of S).o;
hence
rng((Den(o,A2))|((B2#*the Arity of S).o)) c= (B2*the ResultSort of S).o
by Z0,Z1;
end;
theorem Th76:
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 Z0: the MSAlgebra of A1 = the MSAlgebra of A2;
let B1 be MSSubset of A1;
let B2 be MSSubset of A2;
assume Z1: B1 = B2;
let o be OperSymbol of S;
assume Z2: B1 is_closed_on o;
hence o/.B2 = (Den(o,A2)) | ((B2# * the Arity of S).o)
by Z0,Z1,Th77,MSUALG_2:def 7
.= (Den(o,A1)) | ((B1# * the Arity of S).o) by Z0,Z1
.= o/.B1 by Z2,MSUALG_2:def 7;
end;
theorem Th78:
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 Z0: the MSAlgebra of A1 = the MSAlgebra of A2;
let B1 be MSSubset of A1;
let B2 be MSSubset of A2;
assume Z1: B1 = B2 & B1 is opers_closed;
now
let x; 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 Z0,Z1,MSUALG_2:def 6,Th76
.= Opers(A1,B1).x by MSUALG_2:def 8;
end;
hence Opers(A2,B2) = Opers(A1,B1) by PBOOLE:3;
end;
theorem Th79:
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
proof
let A1,A2 be MSAlgebra over S;
assume Z0: the MSAlgebra of A1 = the MSAlgebra of A2;
let B1 be MSSubset of A1;
let B2 be MSSubset of A2;
assume Z1: B1 = B2;
assume Z2: B1 is opers_closed;
let o be OperSymbol of S;
thus B2 is_closed_on o by Z0,Z1,Th77,Z2,MSUALG_2:def 6;
end;
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 Z0: the MSAlgebra of A1 = the MSAlgebra of A2;
let B1 be MSSubAlgebra of A1;
assume Z1: the MSAlgebra of B = the MSAlgebra of B1;
thus the Sorts of B is MSSubset of A2 by Z0,Z1,MSUALG_2:def 9;
let C be MSSubset of A2;
reconsider C1 = C as MSSubset of A1 by Z0;
assume
A2: C = the Sorts of B;
hence C is opers_closed by Z0,Th79,Z1,MSUALG_2:def 9;
the Charact of B1 = Opers(A1,C1) by Z1,A2,MSUALG_2:def 9;
hence the Charact of B = Opers(A2,C) by Z0,Z1,A2,MSUALG_2:def 9,Th78;
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
A4: 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 A4;
end;
theorem Th11:
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,MSUALG_3:def 7
.= 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: TRIV:
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 be set; assume y in rng X;
then consider x 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(element) = {$1};
consider S being ManySortedSet of I such that
A1: for x st x in I holds S.x = F(x) from PBOOLE:sch 4;
take S;
hereby
let x; assume x in I; then
S.x = F(x) by A1;
hence S.x is non empty;
end;
let x; 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;
cluster S.x -> trivial;
coherence
proof
(x in I or x nin I) & dom S = I by PARTFUN1:def 2;
hence thesis by TRIV,FUNCT_1:def 2;
end;
end;
definition
let S;
let A be MSAlgebra over S;
attr A is trivial means: TRIV2:
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(element) = {$1};
consider X being ManySortedSet of S such that
A1: for x 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; 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,XBOOLE_1:65;
end;
thus the Sorts of A is non-empty
proof
let x; 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 TRIV2;
end;
theorem Th121:
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 Th122:
for A being trivial non-empty MSAlgebra over S
for T being EqualSet of S
holds A |= T
proof
let A be trivial non-empty MSAlgebra over S;
let T be EqualSet of S;
let s be SortSymbol of S;
let e be Element of (Equations S).s; assume e in T.s;
thus A |= e by Th121;
end;
theorem Th81:
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);
A2: 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 A2,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 Th82:
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;
A0: the Sorts of A is ManySortedSubset of the Sorts of T
by MSUALG_2:def 9;
A7: now
let x;
assume
A7: x in the carrier of S; then
A3: (the Sorts of A).x c= (the Sorts of T).x & (the Sorts of A).x <> {} &
(the Sorts of T).x <> {} by A0,PBOOLE:def 2,def 18;
consider a being element such that
A4: (the Sorts of A).x = {a} by A3,ZFMISC_1:131;
consider b being element such that
A5: (the Sorts of T).x = {b}
by A7,ZFMISC_1:131;
thus (the Sorts of A).x = (the Sorts of T).x
by A3,A4,A5,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 A7,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: IMAGE:
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 by IMAGE;
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: IMAGE2:
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);
A4: 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,MSUALG_3:def 8,A4,MSUALG_3:def 7;
end;
thus g is "onto" by A1,A2,MSUALG_3:def 8;
end;
given h being ManySortedFunction of A,C such that
A5: h is_epimorphism A,C;
take C,h;
thus h is_homomorphism A,C by A5,MSUALG_3:def 8;
hence thesis by A5,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 Th81;
thus the MSAlgebra of T0 = Image h by Th82;
end;
hence thesis;
end;
end;
theorem Th123:
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 IMAGE2;
let s be SortSymbol of S;
let e be Element of (Equations S).s;
assume Z0: A |= e;
let h be ManySortedFunction of TermAlg S, B;
assume
A2: h is_homomorphism TermAlg S, B;
consider g being ManySortedFunction of TermAlg S,A such that
A3: g is_homomorphism TermAlg S, A & h = f**g by A1,A2,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 A3,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 Z0,A3,EQUATION:def 5;
end;
theorem Th124:
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
proof
let A be non-empty MSAlgebra over S;
let B be A-Image MSAlgebra over S;
let T be EqualSet of S;
assume Z0: A |= T;
let s be SortSymbol of S;
let e be Element of (Equations S).s;
assume e in T.s;
hence B |= e by Th123,Z0,EQUATION:def 6;
end;
begin :: Term Algebras
definition
let S, X;
let A be MSAlgebra over S;
attr A is (X,S)-terms means: TERM:
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
A0: Free(S,X) = FreeMSA X by MSAFREE3:31;
hence Free(S,X) is non-empty;
let x,y; assume
A1: x <> y;
assume
(the Sorts of Free(S,X)).x meets (the Sorts of Free(S,X)).y; then
consider z such that
A2: z in (the Sorts of Free(S,X)).x & z in (the Sorts of Free(S,X)).y
by XBOOLE_0:3;
A3: dom the Sorts of Free(S,X) = the carrier of S by PARTFUN1:def 2; then
reconsider x,y as SortSymbol of S by A2,FUNCT_1:def 2;
z in (the Sorts of Free(S,X)).x by A2; then
reconsider z as Element of Union the Sorts of Free(S,X) by A3,CARD_5:2;
reconsider z as Term of S,X by A0,MSAFREE3:6;
the_sort_of z = x & the_sort_of z = y by A0,A2,MSAFREE3:7;
hence contradiction by A1;
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: AVAR:
FreeGen X is ManySortedSubset of the Sorts of A;
attr A is inheriting_operations means: INHOP:
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: FREEITSELF:
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
proof
let A,B be non-empty MSAlgebra over S such that
A1: the MSAlgebra of A = the MSAlgebra of B;
assume
A2: the Sorts of A is ManySortedSubset of the Sorts of Free(S,X);
hence
the Sorts of B is ManySortedSubset of the Sorts of Free(S,X) by A1;
end;
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
proof
assume
A2: FreeGen X is ManySortedSubset of the Sorts of A;
hence FreeGen X is ManySortedSubset of the Sorts of B by A1;
end;
thus A is inheriting_operations implies B is inheriting_operations
proof assume
A2: 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,A2;
end;
assume
A2: 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
A3: G = FreeGen X;
reconsider G1 = G as ManySortedSubset of the Sorts of A by A1;
consider h being ManySortedFunction of A,A such that
A4: h is_homomorphism A,A & f = h||G1 by A1,A2,A3;
reconsider h2 = h as ManySortedFunction of B,B by A1;
take h2;
thus h2 is_homomorphism B,B by A4,A1,Th11;
thus f = h2 || G by A1,A4;
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);
A0: 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
A1: G = FreeGen X; then
reconsider H = G as non-empty GeneratorSet of A by MSAFREE3:31;
thus thesis by A1,A0,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; 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 Th13:
(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 TERM;
then
A2: Union the Sorts of A0 c= Union the Sorts of Free(S,X)
by Lemma1,PBOOLE:def 18;
hereby let t be Element of A0;
t in Union the Sorts of A0;
hence t is Element of Free(S,X) by A2;
end;
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 ThE:
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 AVAR; 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 ThA:
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 element; 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 element; 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 TERM;
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(element) = {$1};
consider f being Function such that
A1: dom f = S & for x 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;
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,XBOOLE_1:65,ZFMISC_1:11;
end;
let x; 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; 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,PBOOLE:def 2;
hence thesis by A1,PROB_2:def 2,XBOOLE_1:65,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:
CH:
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
A0: 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 AVAR; then
reconsider f = id H as ManySortedFunction of H, the Sorts of A1 by Th108;
consider g being ManySortedFunction of Free(S,X),A1 such that
A1: g is_homomorphism Free(S,X),A1 & g||H = f by A0,MSAFREE:def 5;
take g; thus thesis by A1;
end;
uniqueness
proof
let h1,h2 be ManySortedFunction of Free(S,X),A1 such that
A1: 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
A2: 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 A1 .= h2 || H by A2;
hence h1 = h2 by A1,A2,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 set 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 TERM; 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 set 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 TERM; 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) by TERM;
hence the Sorts of A is disjoint_valued;
end;
end;
theorem Th27:
for t being Element of A0 holds t is Term of S,X
proof
let t be Element of A0;
consider s being set 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 TERM; 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 Th29:
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 set 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 TERM; 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
B1: P[i];
let p be Element of dom t; assume
B3: len p = i+1; then
consider q being FinSequence, a being element such that
B2: p = q^<*a*> by FINSEQ_2:18;
<*a*> is FinSequence of NAT by B2,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
B4: len p = len q+1 by B2,FINSEQ_1:22;
reconsider q as FinSequence of NAT by B2,FINSEQ_1:36;
reconsider q as Element of dom t by B2,TREES_1:21;
t is Term of S,X by Th27; then
reconsider tq = t|q, tp = t|p as Term of S,X by MSATERM:29;
C2: dom tq = (dom t)|q by TREES_2:def 10; then
<*a*> in dom tq & {} in dom tq by B2,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 element such that
B5: 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 B5;
B6: s = the carrier of S by B5,TARSKI:def 1; then
consider arg being ArgumentSeq of Sym(o,X) such that
B7: tq = [o,the carrier of S]-tree arg by B5,MSATERM:10;
<*a*> in dom tq & dom tq = tree doms arg & <*a*> <> {}
by C2,B2,B7,TREES_1:def 6,TREES_4:10; then
consider n being Nat, e being FinSequence such that
C4: n < len doms arg & e in (doms arg).(n+1) & <*a*> = <*n*>^e
by TREES_3:def 15;
C5: a = <*a*>.1 by FINSEQ_1:40 .= n by C4,FINSEQ_1:41;
B8: Free(S,X) = FreeMSA X by MSAFREE3:31;
C7: tq is Element of A by B1,B4,B3;
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
B9: Den(o, Free(S,X)).arg = tq by B7,B8,MSAFREE:def 13;
the_sort_of tq = the_result_sort_of o by B5,B6,MSATERM:17; then
Den(o,Free(S,X)).arg in FreeSort(X, the_result_sort_of o)
by B9,MSATERM:def 5; then
Den(o,Free(S,X)).arg in (the Sorts of Free(S, X)).the_result_sort_of o
by B8,MSAFREE:def 11; then
C1: Den(o,Free(S,X)).arg in (the Sorts of A).the_result_sort_of o
by C7,B9,Th29;
reconsider r = {} as Element of dom tq by TREES_1:22;
D9: tp = tq|<*a*> & a < len arg by B2,C4,C5,TREES_3:38,TREES_9:3; then
C9: tp = arg.(a+1) & a+1 in dom arg by Lem2,B7,TREES_4:def 4;
reconsider ar = arg as Element of Args(o,Free(S,X)) by B8,INSTALG1:1;
ar in Args(o,A) & dom the Arity of S = the carrier' of S
by C1,INHOP,FUNCT_2:def 1; then
arg in cc((the Sorts of A)#,the_arity_of o) by FUNCT_1:13; then
D1: arg in product ((the Sorts of A)*the_arity_of o) by FINSEQ_2:def 5; then
D2: 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 RELAT_1:27,PARTFUN1:def 2;
then (the_arity_of o).(a+1) in rng the_arity_of o by C9,D2,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 C9,D1,D2,CARD_3:9;
then tp is Element of (the Sorts of A).s
by D9,Lem2,D2,FUNCT_1:12;
hence thesis;
end;
A3: 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 A3;
end;
theorem Th111:
FreeGen X is GeneratorSet of A2
proof set A = A2;
reconsider G = FreeGen X as ManySortedSubset of the Sorts of A by AVAR;
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;
A5: FreeMSA X = Free(S,X) by MSAFREE3:31;
P0: 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 ManySortedSubset of the Sorts of Free(S,X) by TERM;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 A4; then
t in FreeSort(X,r) by A5,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
A3: 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 A3;
end;
P1: 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 Z0: 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
A6: 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
A7: 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
A8: 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 A5,A6,MSAFREE:def 13; then
Den(o,Free(S,X)).p in (the Sorts of A).the_result_sort_of o
by A8,Th29; then
E0: p in Args(o,A) & Den(o,A).p = Den(o,Free(S,X)).p by A7,INHOP;
E1: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
E2: Args(o, GenMSAlg G) =
cc((the Sorts of GenMSAlg G)#,(the_arity_of o qua set)) by E1,FUNCT_1:13
.= product ((the Sorts of GenMSAlg G)*the_arity_of o)
by FINSEQ_2:def 5;
E2a: Args(o,A) = cc((the Sorts of A)#,the_arity_of o) by E1,FUNCT_1:13
.= product ((the Sorts of A)*the_arity_of o) by FINSEQ_2:def 5;
E4: dom ((the Sorts of GenMSAlg G)*the_arity_of o) = dom the_arity_of o
by RELAT_1:27,PARTFUN1:def 2;
E4a: dom ((the Sorts of A)*the_arity_of o) = dom the_arity_of o
by RELAT_1:27,PARTFUN1:def 2; then
E3: dom p = dom the_arity_of o by E0,E2a,CARD_3:9;
now let x; assume
E6: x in dom the_arity_of o; then
E5: p.x in rng p & p.x in ((the Sorts of A)*the_arity_of o).x
by E3,FUNCT_1:def 3,CARD_3:9,E0,E4a,E2a;
(the_arity_of o).x in rng the_arity_of o & rng the_arity_of o c=
the carrier of S by E6,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 E5,E6,FUNCT_1:13;
px is Term of S,X by Th27; then
px in (the Sorts of GenMSAlg G).s by E5,Z0;
hence p.x in ((the Sorts of GenMSAlg G)*the_arity_of o).x
by E6,FUNCT_1:13;
end; then
reconsider q = p as Element of Args(o, GenMSAlg G) by E2,E3,E4,CARD_3:9;
reconsider B = the Sorts of GenMSAlg G as
ManySortedSubset of the Sorts of A by MSUALG_2:def 9;
A1: B is opers_closed & the Charact of GenMSAlg G = Opers(A,B)
by MSUALG_2:def 9;
A2: B is_closed_on o by MSUALG_2:def 6,def 9;
Den(o, GenMSAlg G) = o/.B by A1,MSUALG_2:def 8
.= (Den(o,A))|((B# * the Arity of S).o) by A2,MSUALG_2:def 7; then
A3: Den(o, GenMSAlg G).p = Den(o,A).q by FUNCT_1:49;
J1: Den(o, GenMSAlg G).q = [o,the carrier of S]-tree p
by A5,A3,A6,E0,MSAFREE:def 13; then
J2: [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
J3: 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 E0,A3,J1,FUNCT_2:5;
hence [o,the carrier of S]-tree p in (the Sorts of GenMSAlg G).r
by J2,J3,PROB_2:def 2,XBOOLE_0:3;
end;
PP: for t being Term of S,X holds P[t] from MSATERM:sch 1(P0,P1);
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; assume x in the carrier of S; then
reconsider s = x as SortSymbol of S;
let y be element; assume
A1: 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 TERM; 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 by A1; then
y is Element of FreeMSA X by MSAFREE3:31; then
y is Term of S,X by MSAFREE3:6;
hence thesis by PP;
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
Z0: 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
H1: j is_epimorphism T,A by IMAGE2;
H2: j is_homomorphism T,A & j is "onto" by H1,MSUALG_3:def 8;
consider jj being ManySortedFunction of A,T such that
H3: j**jj = id the Sorts of A by H2,Th39,Th96;
consider h being ManySortedFunction of T,T such that
H4: h is_homomorphism T,T & jj**f = h || G by Z0,FREEITSELF;
take k = j**h;
thus k is_homomorphism T,A by H2,H4,MSUALG_3:10;
thus f = (id the Sorts of A)**f by MSUALG_3:4
.= j**(jj**f) by H3,PBOOLE:140
.= k || G by H4,EXTENS_1:4;
end;
theorem Th107:
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;
A0: 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;
A1: f is_homomorphism Free(S,X),A & f||G = id G by CH;
defpred P[set] means for s being SortSymbol of S
st $1 in (the Sorts of A).s
holds f.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
Z1: root-tree [v,s] in (the Sorts of A).r;
the Sorts of A is MSSubset of Free(S,X) by TERM; 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 Z1,A0; then
root-tree [v,s] in FreeSort(X, r) by MSAFREE:def 11; then
B0: 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
B1: root-tree [v,s] in (FreeGen X).s by MSAFREE:def 16;
B3: (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 B1,FUNCT_1:49; then
B4: (f.s).root-tree [v,s] = (id((FreeGen X).s)).root-tree [v,s]
by A1,B3,MSAFREE:def 1 .= root-tree [v,s] by B1,FUNCT_1:18;
thus thesis by B0,B4;
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
Z0: for t being Term of S,X st t in rng p holds P[t];
let s be SortSymbol of S;
assume
B5: [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
D7: DenOp(o, X).p = Sym(o,X)-tree p & (FreeOper X).o = DenOp(o, X)
by MSAFREE:def 12,def 13;
B6: p is Element of Args(o, Free(S,X)) by A0,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 TERM; then
B8: (the Sorts of A).s c= (the Sorts of Free(S,X)).s by PBOOLE:def 2,def 18;
D1: the_sort_of t = the_result_sort_of o &
FreeSort(X,s) = (the Sorts of Free(S,X)).s
by A0,MSATERM:20,MSAFREE:def 11; then
C7: s = the_result_sort_of o by B5,B8,MSATERM:def 5;
D2: Den(o,Free(S,X)).p in (the Sorts of A).the_result_sort_of o
by B5,D7,A0,D1,B8,MSATERM:def 5; then
B9: p in Args(o,A) & Den(o,A).p = Den(o,Free(S,X)).p
by B6,INHOP;
reconsider q = p as Element of Args(o, A) by D2,B6,INHOP;
reconsider p0 = p as Element of Args(o, Free(S,X)) by A0,INSTALG1:1;
C2: 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
C3: i in dom the_arity_of o; then
C4: (the_arity_of o)/.i = (the_arity_of o).i & p0.i in rng p
by C2,FUNCT_1:def 3,PARTFUN1:def 6;
C6: p0.i in ((the Sorts of A)*the_arity_of o).i by C2,C3,CARD_3:9; then
C5: p0.i in (the Sorts of A).((the_arity_of o).i) by C3,FUNCT_1:13;
p0.i is Element of (the Sorts of A).((the_arity_of o)/.i)
by C4,C6,C3,FUNCT_1:13;
then p0.i is Term of S,X by Th27;
hence q.i = (f.((the_arity_of o)/.i)).(p0.i) by Z0,C4,C5;
end; then
f#p0 = q by C2,MSUALG_3:24;
hence thesis by C7,D7,A0,B9,CH,MSUALG_3:def 7;
end;
A6: for t being Term of S,X holds P[t] from MSATERM:sch 1(A4,A5);
thus f is_epimorphism Free(S,X),A
proof
thus f is_homomorphism Free(S,X), A by CH;
let x be set; 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 element; assume
B1: 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 Th27; then
A7: f.s.t = t by A6;
the Sorts of A is MSSubset of Free(S,X) by TERM; 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 B1,FUNCT_2:def 1;
hence thesis by A7,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 Th27;
hence f.s.t = t by A6;
end;
theorem Th67:
(canonical_homomorphism A2)**(canonical_homomorphism A2)
= canonical_homomorphism A2
proof set A = A2;
set f = canonical_homomorphism A;
now
let x; 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 TERM;
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
A0: (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,PBOOLE:def 2;
then
A1: dom ((f**f).s) = (the Sorts of Free(S,X)).s by XBOOLE_1:1,RELAT_1:27;
now let y; assume
A3: y in (the Sorts of Free(S,X)).s;
then
A2: f.s.y in (the Sorts of A).s by FUNCT_2:5;
thus (f**f).s.y = f.s.(f.s.y) by A0,A3,FUNCT_1:13 .= f.s.y by A2,Th107;
end;
hence (f**f).x = f.x by A0,A1,FUNCT_1:2;
end;
hence thesis by PBOOLE:3;
end;
theorem
A is Free(S,X)-Image
proof
now
take B = A;
FreeGen X is ManySortedSubset of the Sorts of A by AVAR; then
FreeGen X is free & id FreeGen X is ManySortedFunction of FreeGen X,
the Sorts of A by Th108; then
consider f being ManySortedFunction of FreeMSA(X), A such that
A1: f is_homomorphism FreeMSA(X), A & f||FreeGen X = id FreeGen X
by MSAFREE:def 5;
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
Z1: root-tree [v,s] in (the Sorts of C).r;
the Sorts of C is MSSubset of Free(S,X) by TERM; 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 Z1,A2; then
root-tree [v,s] in FreeSort(X, r) by MSAFREE:def 11; then
B0: 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
B1: root-tree [v,s] in (FreeGen X).s by MSAFREE:def 16;
B2: (f0.:.:the Sorts of Free(S,X)).s
= (f0.s).:((the Sorts of Free(S,X)).s) by PBOOLE:def 20;
B3: (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 B1,FUNCT_1:49; then
B4: (f.s).root-tree [v,s] = (id((FreeGen X).s)).root-tree [v,s]
by A1,B3,MSAFREE:def 1 .= root-tree [v,s] by B1,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 B0,B2,B1,B4,FUNCT_1:def 6;
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
Z0: for t being Term of S,X st t in rng p holds P[t];
let s be SortSymbol of S;
assume
B5: [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
D2: DenOp(o, X).p = Sym(o,X)-tree p & (FreeOper X).o = DenOp(o, X)
by MSAFREE:def 12,def 13;
B6: 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 TERM; then
B8: (the Sorts of C).s c= (the Sorts of Free(S,X)).s
by PBOOLE:def 2,def 18;
D1: 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
C7: s = the_result_sort_of o by B5,B8,MSATERM:def 5;
C8: Den(o,Free(S,X)).p in (the Sorts of A).the_result_sort_of o
by B5,D2,A2,D1,B8,MSATERM:def 5; then
B9: p in Args(o,A) & Den(o,A).p = Den(o,Free(S,X)).p by B6,INHOP;
reconsider q = p as Element of Args(o, A) by C8,B6,INHOP;
reconsider p0 = p as Element of Args(o, Free(S,X)) by A2,INSTALG1:1;
C2: 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
C3: i in dom the_arity_of o; then
C4: (the_arity_of o)/.i = (the_arity_of o).i & p0.i in rng p
by C2,FUNCT_1:def 3,PARTFUN1:def 6;
D7: p0.i in ((the Sorts of A)*the_arity_of o).i by C2,C3,CARD_3:9; then
C5: p0.i in (the Sorts of A).((the_arity_of o).i) by C3,FUNCT_1:13;
p0.i is Element of (the Sorts of A).((the_arity_of o)/.i)
by C4,D7,C3,FUNCT_1:13;
then p0.i is Term of S,X by Th27;
hence q.i = (f0.((the_arity_of o)/.i)).(p0.i) by Z0,C4,C5;
end; then
D8: f0#p0 = q by C2,MSUALG_3:24; then
C1: f0.(the_result_sort_of o).(Den(o,Free(S,X)).p) = Den(o,A).p
by A3,MSUALG_3:def 7;
C6: (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 D2,A2,B8,C1,C7,B5,D2,A2,D1,
B8,MSATERM:def 5,B6,INHOP,FUNCT_2:def 1;
hence [o,the carrier of S]-tree p in (f0.:.:the Sorts of Free(S,X)).s
by C6,FUNCT_1:def 6;
thus thesis by C7,D2,A2,B9,D8,A1,MSUALG_3:def 7;
end;
A6: for t being Term of S,X holds P[t] from MSATERM:sch 1(A4,A5);
now
thus the Sorts of C c= f0.:.:the Sorts of Free(S,X)
proof
let x; assume x in the carrier of S; then
reconsider s = x as SortSymbol of S;
let y be element; 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 Th27;
hence thesis by A6;
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 by IMAGE;
end;
begin :: Satisfiability
theorem ThE0:
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
proof
let A be non-empty MSAlgebra over S;
let s be SortSymbol of S;
let t be Element of TermAlg S,s;
let h be ManySortedFunction of TermAlg S, A;
(t '=' t)`1 = t & (t '=' t)`2 = t by MCART_1:7;
hence thesis;
end;
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
proof
let A be non-empty MSAlgebra over S;
let s be SortSymbol of S;
let t1,t2 be Element of TermAlg S,s;
assume
A1: A |= t1 '=' t2;
let h be ManySortedFunction of TermAlg S, A;
(t1 '=' t2)`1 = t1 & (t1 '=' t2)`2 = t2 &
(t2 '=' t1)`1 = t2 & (t2 '=' t1)`2 = t1 by MCART_1:7;
hence thesis by A1,EQUATION:def 5;
end;
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
A3: h is_homomorphism TermAlg S, A;
A2: (t1 '=' t2)`1 = t1 & (t1 '=' t2)`2 = t2 &
(t2 '=' t3)`1 = t2 & (t2 '=' t3)`2 = t3 &
(t1 '=' t3)`1 = t1 & (t1 '=' t3)`2 = t3 by MCART_1:7; then
h.s.t1 = h.s.t2 & h.s.t2 = h.s.t3 by A1,A3,EQUATION:def 5;
hence thesis by A2;
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 Z4: a1 in Args(o,TermAlg S);
assume Z5: a2 in Args(o,TermAlg S); then
reconsider b1 = a1, b2 = a2 as Element of Args(o,TermAlg S) by Z4;
assume Z6: 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 Z7: t1 = [o,the carrier of S]-tree a1;
assume Z8: t2 = [o,the carrier of S]-tree a2;
let h be ManySortedFunction of TermAlg S, A;
assume
A1: h is_homomorphism TermAlg S, A;
AA: now
let n be Nat; assume
A4: n in dom b1;
A5: 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 A4,A5,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 A4,A5,FUNCT_1:13,PRALG_2:3; then
reconsider t1 = a1.n, t2 = a2.n as Element of TermAlg S, s
by A4,A5,MSUALG_3:6;
h.s.(t1 '=' t2)`1 = h.s.(t1 '=' t2)`2 by Z6,A4,A5,A1,EQUATION:def 5; then
A6: h.s.t1 = h.s.(t1 '=' t2)`2 by MCART_1:7 .= h.s.t2 by MCART_1:7;
A7: s = (the_arity_of o)/.n by A4,A5,PARTFUN1:def 6;
thus (h#b2).n
= (h.((the_arity_of o)/.n)).(b1.n) by A6,A7,A4,A5,MSUALG_3:def 6;
end;
A2: (t1 '=' t2)`1 = t1 & (t1 '=' t2)`2 = t2 by MCART_1:7;
hence h.s.(t1 '=' t2)`1
= h.s.(Den(o,TermAlg S).a1) by Z4,Z7,INSTALG1:3
.= Den(o, A).(h#b1) by A1,MSUALG_3:def 7
.= Den(o, A).(h#b2) by AA,MSUALG_3:def 6
.= h.s.(Den(o,TermAlg S).a2) by A1,MSUALG_3:def 7
.= h.s.(t1 '=' t2)`2 by A2,Z5,Z8,INSTALG1:3;
end;
definition
let S;
let T be EqualSet of S;
let A be MSAlgebra over S;
attr A is T-satisfying means: SAT: 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 Th122;
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
proof
let B be non-empty MSAlgebra over S;
assume B is A-Image;
hence B |= T by SAT,Th124;
end;
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: EQUAL:
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; 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 element; 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
A1: for s being SortSymbol of S holds
f1.s = {e where e is Element of (Equations S).s: A |= e} and
A2: for s being SortSymbol of S holds
f2.s = {e where e is Element of (Equations S).s: A |= e};
now
let x; 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 A1
.= f2.x by A2;
end;
hence thesis by PBOOLE:3;
end;
end;
theorem Th125:
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 EQUAL; 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
proof
thus A |= Equations(S,A) by Th125;
end;
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];
A0: 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
B1: Q[t1,f1] & Q[t2,f2];
let x; assume x in dom f1 /\ dom f2;
then
B2: x in Subtrees t1 & x in Subtrees t2 by B1,XBOOLE_0:def 4;
then
E1: 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;
B3: 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
C1: root-tree [x,s] in Subtrees t1 & root-tree [x,s] in Subtrees t2;
then f1.root-tree [x,s] = R(x,s) by B1;
hence thesis by C1,B1;
end;
B4: 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
C2: 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
C3: t in Subtrees t1 & t in Subtrees t2;
rng p c= Subtrees t1
proof
let x be element; assume
C6: x in rng p;
then consider y such that
C4: y in dom p & x = p.y by FUNCT_1:def 3;
reconsider y as Nat by C4;
consider n being Nat such that
C5: y = 1+n by C4,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 C4,C6;
reconsider q = {} as Element of dom tn by TREES_1:22;
consider r being Element of dom t1 such that
C7: t = t1|r by C3;
n+1 <= len p by C4,C5,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 C4,C5,TREES_4:def 4,11;
then x in Subtrees t & Subtrees t c= Subtrees t1 by C7,TREES_9:13;
hence x in Subtrees t1;
end;
then
C8: dom(f1*p) = dom p by B1,RELAT_1:27;
rng p c= Subtrees t2
proof
let x be element; assume
C6: x in rng p;
then consider y such that
C4: y in dom p & x = p.y by FUNCT_1:def 3;
reconsider y as Nat by C4;
consider n being Nat such that
C5: y = 1+n by C4,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 C4,C6;
reconsider q = {} as Element of dom tn by TREES_1:22;
consider r being Element of dom t2 such that
C7: t = t2|r by C3;
n+1 <= len p by C4,C5,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 C4,C5,TREES_4:def 4,11;
then x in Subtrees t & Subtrees t c= Subtrees t2 by C7,TREES_9:13;
hence x in Subtrees t2;
end;
then
C9: dom(f2*p) = dom p by B1,RELAT_1:27;
now let x; assume
D0: x in dom p;
then
D1: 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 D1;
D2: R[w] by C2,D1;
reconsider y = x as Nat by D0;
consider n being Nat such that
C5: y = 1+n by D0,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
C7: t = t1|r1 by C3;
consider r2 being Element of dom t2 such that
C8: t = t2|r2 by C3;
n+1 <= len p by D0,C5,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 C5,TREES_4:def 4,11;
then w in Subtrees t & Subtrees t c= Subtrees t2 &
Subtrees t c= Subtrees t1 by C7,C8,TREES_9:13;
hence (f1*p).x = f2.w by D0,D2,FUNCT_1:13 .= (f2*p).x
by D0,FUNCT_1:13;
end;
then f1*p = f2*p by C8,C9,FUNCT_1:2;
hence f1.t = F(o,f2*p) by B1,C3 .= f2.t by B1,C3;
end;
for t being Term of S(),X() holds R[t] from MSATERM:sch 1(B3,B4);
hence thesis by B2,E1;
end;
A1: 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;
E1: Subtrees root-tree [x,s] = {root-tree [x,s]} by Lem3;
take f = {root-tree [x,s]}-->R(x,s);
thus dom f = Subtrees root-tree [x,s] by E1,FUNCOP_1:13;
hereby let s1 be SortSymbol of S(), x1 be Element of X().s1;
assume
E2: root-tree [x1,s1] in Subtrees root-tree [x,s];
then root-tree [x1,s1] = root-tree [x,s] by E1,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 E1,E2,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 E1,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;
A2: 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
E3: for t be Term of S(),X() st t in rng p holds P[t];
defpred W[element,element] means
ex f being Function, t being Term of S(),X()
st t = p.$1 & $2 = f & Q[t,f];
E5: for x st x in dom p ex y st W[x,y]
proof
let x; assume x in dom p;
then
F1: 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
F2: Q[t,f] by E3,F1;
take f,f,t;
thus thesis by F2;
end;
consider g being Function such that
E4: dom g = dom p & for x st x in dom p holds W[x,g.x]
from CLASSES1:sch 1(E5);
EE: now
thus rng g is functional
proof
let y be set; assume y in rng g;
then consider x such that
E6: x in dom g & y = g.x by FUNCT_1:def 3;
W[x,y] by E4,E6;
hence thesis;
end;
let x,y be Function; assume
E7: x in rng g & y in rng g;
then consider x0 being element such that
E8: x0 in dom g & x = g.x0 by FUNCT_1:def 3;
consider y0 being element such that
E9: y0 in dom g & y = g.y0 by E7,FUNCT_1:def 3;
W[x0,x] & W[y0,y] by E4,E8,E9;
hence x tolerates y by A0;
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[element,element] means ex I be set st I = $1 & $2 = proj1 I;
FF: for x,y,z being element st S[x,y] & S[x,z] holds y = z;
consider Y being set such that
F0: for x being element holds
x in Y iff ex y be element st y in rng g & S[y,x] from TARSKI:sch 1(FF);
H9: dom f1 = union Y
proof
thus dom f1 c= union Y
proof
let x be element; assume x in dom f1;
then [x,f1.x] in f1 by FUNCT_1:1;
then consider Z being set such that
H1: [x,f1.x] in Z & Z in rng g by TARSKI:def 4;
x in proj1 Z & proj1 Z in Y by H1,F0,XTUPLE_0:def 12;
hence thesis by TARSKI:def 4;
end;
let z be element; assume z in union Y;
then consider Z being set such that
H2: z in Z & Z in Y by TARSKI:def 4;
consider y be element such that
H3: y in rng g & ex I being set st I = y & Z = proj1 I by H2,F0;
reconsider y as Function by H3,EE;
[z,y.z] in y by H2,H3,FUNCT_1:1;
then [z,y.z] in f1 by H3,TARSKI:def 4;
hence thesis by FUNCT_1:1;
end;
F1: 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} by FUNCOP_1:13;
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
F4: 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
F5: [x,f1.x] in Y & Y in rng g by TARSKI:def 4;
consider y such that
F6: y in dom g & Y = g.y by F5,FUNCT_1:def 3;
F7: W[y,Y] by E4,F6;
then reconsider t1 = p.y as Term of S(),X();
x in Subtrees t1 & t1 in rng p
by E4,F6,F5,F7,XTUPLE_0:def 12,FUNCT_1:def 3;
then x <> t by Lem7;
hence thesis by F4,TARSKI:def 1;
end;
then
F3: f1 c= f by FUNCT_4:28,PARTFUN1:56;
per cases;
suppose
T1: p = {};
then
T2: Subtrees (Sym(o,X())-tree p) = {Sym(o,X())-tree p} by Lem5;
dom p = {} by T1;
then rng g = {} by E4,RELAT_1:42;
hence dom f = {} \/ Subtrees t by T2,F1,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 T2,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
F2: Sym(o0,X())-tree p0 = t by T2,TARSKI:def 1;
rng p /\ dom f c= dom f1
proof
let z be element; assume z in rng p /\ dom f; then
G0: 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 such that
G1: y in dom p & z = p.y by G0,FUNCT_1:def 3;
W[y,g.y] by E4,G1;
then
G2: z in proj1 (g.y) & g.y in rng g by E4,G1,TREES_9:11,FUNCT_1:def 3;
then proj1 (g.y) in Y by F0;
hence thesis by H9,G2,TARSKI:def 4;
end;
then
G3: f1*p = f*p by F3,ALGSPEC1:2;
Sym(o0,X()) = Sym(o,X()) & p = p0 by F2,TREES_4:15;
then
G4: p0 = p & o0 = o by XTUPLE_0:1;
G5: t in {t} by TARSKI:def 1;
dom({t}-->F(o,f1*p)) = {t} by FUNCOP_1:13;
then 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 F2,FUNCT_4:13
.= F(o0,f*p0) by G3,G4,G5,FUNCOP_1:7;
end;
suppose p <> {};
then reconsider p as non empty DTree-yielding FinSequence;
G6: union Y = Subtrees rng p
proof
thus union Y c= Subtrees rng p
proof
let z be element; assume z in union Y;
then consider W being set such that
G7: z in W & W in Y by TARSKI:def 4;
consider y be element such that
G8: y in rng g & S[y,W] by G7,F0;
consider a being element such that
G9: a in dom g & y = g.a by G8,FUNCT_1:def 3;
reconsider a as Nat by E4,G9;
consider f being Function, t being Term of S(),X() such that
I1: t = p.a & y = f & Q[t,f] by E4,G9;
W = Subtrees t & t in rng p by E4,G8,G9,I1,FUNCT_1:def 3;
then W c= Subtrees rng p by Lem8;
hence thesis by G7;
end;
let z be element; assume z in Subtrees rng p;
then consider t being (Element of rng p), q being Element of dom t
such that
I2: z = t|q;
I3: z in Subtrees t by I2;
consider a being element such that
I4: a in dom p & t = p.a by FUNCT_1:def 3;
reconsider a as Nat by I4;
consider f3 being Function, t1 being Term of S(),X() such that
I5: t1 = p.a & g.a = f3 & Q[t1,f3] by I4,E4;
f3 in rng g by E4,I4,I5,FUNCT_1:def 3;
then Subtrees t in Y by I4,I5,F0;
hence thesis by I3,TARSKI:def 4;
end;
dom ({t}-->F(o,f1*p)) = {t} by FUNCOP_1:13;
then dom f = union Y \/ {t} by H9,FUNCT_4:def 1;
hence dom f = Subtrees t by G6,Lem4;
hereby let s be SortSymbol of S(), x be Element of X().s;
assume
G8: 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
J7a: root-tree [x,s] <> t by TREES_4:17;
then
root-tree [x,s] nin {t} & Subtrees t = {t}\/Subtrees rng p
by Lem4,TARSKI:def 1;
then root-tree [x,s] in Subtrees rng p by G8,XBOOLE_0:def 3;
then consider h being (Element of rng p), r being Element of dom h
such that
G9: 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
J1: Q[h,f2] by E3;
consider a being element such that
J4: a in dom p & h = p.a by FUNCT_1:def 3;
reconsider a as Nat by J4;
consider f3 being Function, t1 being Term of S(),X() such that
J5: t1 = p.a & g.a = f3 & Q[t1,f3] by J4,E4;
J6: f3 = f2 by J1,J4,J5,A0,PARTFUN1:55;
J2: root-tree [x,s] in Subtrees h by G9;
then f2.root-tree [x,s] = R(x,s) by J1;
then [root-tree [x,s], R(x,s)] in f2 & f2 in rng g
by J2,J4,J5,J6,E4,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 J7a,Lem4,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
K1: Sym(o1,X())-tree p1 in {t} \/ Subtrees rng p by Lem4;
rng p c= Subtrees rng p & (rng p)/\dom f c= rng p by Lem9,XBOOLE_1:17;
then (rng p)/\dom f c= dom f1 by H9,G6,XBOOLE_1:1;
then
KK: f1*p = f*p by F3,ALGSPEC1:2;
per cases by K1,G6,XBOOLE_0:def 3;
suppose
K2: t1 in {t};
then
t1 = t by TARSKI:def 1;
then
K3: Sym(o,X()) = Sym(o1,X()) & p = p1 by TREES_4:15;
dom({t}-->F(o,f1*p)) = {t} by FUNCOP_1:13;
then
f.t1 = ({t}-->F(o,f1*p)).t1 by K2,FUNCT_4:13
.= F(o,f1*p) by K2,FUNCOP_1:7;
hence f.(Sym(o1,X())-tree p1) = F(o1,f*p1)
by K3,KK,XTUPLE_0:1;
end;
suppose t1 in union Y;
then consider W being set such that
K6: t1 in W & W in Y by TARSKI:def 4;
consider y be element such that
K7: y in rng g & S[y,W] by F0,K6;
consider z such that
K8: z in dom g & y = g.z by K7,FUNCT_1:def 3;
reconsider z as Nat by E4,K8;
consider f2 being Function, t2 be Term of S(),X() such that
K9: t2 = p.z & y = f2 & Q[t2,f2] by E4,K8;
KB: f2.t1 = F(o1,f2*p1) by K9,K6,K7;
KA: rng p1 c= Subtrees t1 & (rng p1)/\dom f c= rng p1
by XBOOLE_1:17,Lem11;
Subtrees t1 c= Subtrees t2 by K6,K7,K9,Lem12;
then
KE: rng p1 c= dom f2 by KA,K9,XBOOLE_1:1;
f2 c= f1 by K7,K9,ZFMISC_1:74;
then
KC: (rng p1)/\dom f c= dom f2 & f2 c= f by F3,KA,KE,XBOOLE_1:1;
thus f.(Sym(o1,X())-tree p1) = f2.t1 by K6,K7,KC,K9,FOMODEL0:51
.= F(o1,f*p1) by KB,KC,ALGSPEC1:2;
end;
end;
end;
AA: for t being Term of S(),X() holds P[t] from MSATERM:sch 1(A1,A2);
defpred G[element,element] means
ex t being Term of S(),X(),f being Function st
t = $1 & f = $2 & Q[t,f];
L1: for x st x in S()-Terms X() ex y st G[x,y]
proof
let x; assume x in S()-Terms X();
then reconsider t = x as Term of S(),X();
P[t] by AA;
hence thesis;
end;
consider F being Function such that
L2: dom F = S()-Terms X() & for x st x in S()-Terms X() holds G[x,F.x]
from CLASSES1:sch 1(L1);
rng F is functional compatible
proof
thus rng F is functional
proof
let x be set; assume x in rng F;
then consider x0 being element such that
E8: x0 in dom F & x = F.x0 by FUNCT_1:def 3;
G[x0,x] by L2,E8;
hence thesis;
end;
let h1,h2 be Function; assume
E7: h1 in rng F & h2 in rng F;
then consider x0 being element such that
E8: x0 in dom F & h1 = F.x0 by FUNCT_1:def 3;
consider y0 being element such that
E9: y0 in dom F & h2 = F.y0 by E7,FUNCT_1:def 3;
G[x0,h1] & G[y0,h2] by L2,E8,E9;
hence h1 tolerates h2 by A0;
end;
then reconsider rF = rng F as non empty functional compatible set
by L2,RELAT_1:42;
reconsider f = union rF as Function;
dom f = S()-Terms X()
proof
L3: dom f = union {dom h where h is Element of rF: not contradiction}
by COMPUT_1:12;
thus dom f c= S()-Terms X()
proof
let x be element; assume x in dom f;
then consider W being set such that
L4: x in W & W in {dom h where h is Element of rF: not contradiction}
by L3,TARSKI:def 4;
consider h being Element of rF such that
L5: W = dom h by L4;
consider x0 being element such that
L6: x0 in dom F & h = F.x0 by FUNCT_1:def 3;
reconsider x0 as Term of S(),X() by L2,L6;
G[x0,h] by L2,L6;
then x is Term of S(),X() by L4,L5,Lem10;
hence thesis;
end;
let x be element; 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
L7: t = x & h = F.x & Q[t,h] by L2;
reconsider h as Element of rF by L2,L7,FUNCT_1:def 3;
x in dom h & dom h in {dom g where g is Element of rF: not contradiction}
by L7,TREES_9:11;
hence thesis by L3,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 L2;
then consider g being Function such that
L8: g = F.t & Q[t,g];
g in rF by L2,L8,FUNCT_1:def 3;
then
L9: g c= f by ZFMISC_1:74;
t in dom g by L8,TREES_9:11;
hence f.root-tree [x,s] = g.t by L9,FOMODEL0:51
.= R(x,s) by L8,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 L2;
then consider g being Function such that
L8: g = F.t & Q[t,g];
LA: g in rF by L2,L8,FUNCT_1:def 3;
then
L9: g c= f by ZFMISC_1:74;
LL: t in dom g by L8,TREES_9:11;
rng p c= Subtrees t & (rng p)/\ dom f c= rng p by Lem11,XBOOLE_1:17;
then (rng p)/\ dom f c= dom g by L8,XBOOLE_1:1;
then
LK: g*p = f*p by LA,ZFMISC_1:74,ALGSPEC1:2;
thus f.(Sym(o,X())-tree p) = g.t by L9,LL,FOMODEL0:51
.= F(o,f*p) by L8,TREES_9:11,LK;
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[element] means F1().$1 = F2().$1;
B1: 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;
B2: 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
B3: for t being Term of S(),X() st t in rng p holds P[t];
B4: dom (F1()*p) = dom p & dom (F2()*p) = dom p
by RELAT_1:27,PARTFUN1:def 2,FINSEQ_1:def 4;
now
let x; assume
B5: x in dom p; then reconsider i = x as Element of NAT;
reconsider t = p.i as Term of S(),X() by B5,MSATERM:22;
t in rng p by B5,FUNCT_1:def 3; then
P[t] by B3;
hence (F1()*p).x = F2().t by B5,FUNCT_1:13
.= (F2()*p).x by B5,FUNCT_1:13;
end; then
F1()*p = F2()*p by B4,FUNCT_1:2;
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;
B6: for t being Term of S(),X() holds P[t] from MSATERM:sch 1(B1,B2);
now let x; assume
x in S()-Terms X();
hence P[x] by B6;
end;
hence thesis by PBOOLE:3;
end;
definition
let S, X;
let w be ManySortedFunction of X, (the carrier of S) --> NAT;
let t be Function such that
AA: 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: HASH:
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
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) 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;
A3: now let s be SortSymbol of S;
let x be Element of X.s;
w.s is Function of X.s,Y.s & Y.s = NAT by FUNCOP_1:7; then
C2: w.s.x in NAT & F.root-tree [x,s] = R(x,s) by A1; 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 C2,MSATERM:14;
hence thesis by MSATERM:14;
end;
end;
A4: now let o be OperSymbol of S;
let p be ArgumentSeq of Sym(o,X); assume
A5: for t being Term of S,X st t in rng p holds P[t];
A6: dom (F*p) = dom p & dom p = dom the_arity_of o
by RELAT_1:27,MSATERM:22,PARTFUN1:def 2,FINSEQ_1:def 4;
now let i be Nat;
assume
A7: i in dom p; then
reconsider q = p.i as Term of S,X by PARTFUN1:4;
A8: (F*p).i = F.(p.i) & p.i in rng p & p.i in S-Terms X
by A7,FUNCT_1:def 3,13,PARTFUN1:4; then
A9: P[p.i] by A5; then
reconsider t = (F*p).i as Term of S,Y
by A7,FUNCT_1:13;
reconsider q = p.i as Term of S,X by A7,PARTFUN1:4;
take t;
thus t = (F*p).i;
thus the_sort_of t = (the_arity_of o).i by A7,A8,A9,MSATERM:23;
end; then
reconsider Fp = F*p as ArgumentSeq of Sym(o,Y) by A6,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 A2;
C1: 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 C1,MSATERM:17;
end;
end;
C3: for t being Term of S,X holds P[t] from MSATERM:sch 1(A3,A4);
t is Term of S,X by AA,Th27;
then consider tt being Term of S,Y, q being Term of S,X such that
C4: tt = F.t & q = t & the_sort_of tt = the_sort_of q by C3;
reconsider Ft = F.t as Element of TermAlg S by C4,MSATERM:13;
take Ft, F;
thus thesis by A1,A2;
end;
uniqueness
proof
let t1,t2 being Element of TermAlg S;
given F1 being ManySortedSet of S-Terms X such that
A0: t1 = F1.t and
A1: (for s being SortSymbol of S, x being Element of X.s holds
F1.root-tree [x,s] = R(x,s)) and
B1: 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
B0: t2 = F2.t and
A2: (for s being SortSymbol of S, x being Element of X.s holds
F2.root-tree [x,s] = R(x,s)) and
B2: 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(A1,B1,A2,B2);
hence thesis by A0,B0;
end;
end;
theorem HASH1:
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 HASH;
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 HASHA:
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];
A3: 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 being set such that
B0: y in X.s & x = root-tree [y,s] by MSAFREE:def 15;
x .{} = [y,s] by B0,TREES_4:3;
then reconsider x1 = (x .{})`1 as Element of X.s by B0,MCART_1:7;
B1: 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 B1;
hence thesis by MSAFREE:def 11;
end;
consider f being ManySortedFunction of G, the Sorts of TermAlg S such that
A4: for s being SortSymbol of S for x being Element of G.s holds f.s.x = F(s,x)
from Sch2(A3);
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
A2: h is_homomorphism Free(S,X), TermAlg S & h||G = f by MSAFREE:def 5;
set t = the Element of Free(S, X);
consider F being ManySortedSet of S-Terms X such that
A5: #(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 HASH;
take h; thus h is_homomorphism Free(S,X), TermAlg S by A2;
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;
A6: 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
B2: 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 A5,HASH1
.= root-tree [w.s.x,s] by A5
.= root-tree [w.s.[x,s]`1,s] by MCART_1:7
.= F(s,q) by TREES_4:3
.= f.s.t by A4
.= ((h.s)|(G.s)).q by A2,MSAFREE:def 1
.= h.s1.(root-tree [x,s]) by B2,FUNCT_1:49;
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 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
B3: 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
B4: 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 element; assume y in rng p;
then consider x such that
C1: x in dom p & y = p.x by FUNCT_1:def 3;
reconsider x as Nat by C1;
p.x is Term of S,X & dom F = S-Terms X
by C1,MSATERM:22,PARTFUN1:def 2;
hence thesis by C1;
end; then
B5: 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; assume
C2: x in dom p;
then reconsider i = x as Nat;
reconsider t = p.i as Term of S,X by C2,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;
C3: t in rng p by C2,FUNCT_1:def 3;
the_sort_of t = s by C2,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
C4: t in (the Sorts of Free(S,X)).s by MSAFREE3:31;
thus (F*p).x = F.t by C2,FUNCT_1:13
.= #(u,w) by A5,HASH1
.= h.s.u by B3,C3,C4
.= (h#q).x by C2,MSUALG_3:def 6;
end; then
B7: F*p = h#q by B5,FUNCT_1:2;
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 HASH1,A5
.= Sym(o,(the carrier of S)-->NAT)-tree (F*p) by A5
.= Den(o,Free(S,(the carrier of S)-->NAT)).(h#q) by B7,A1,Th33
.= h.s.(Den(o,Free(S,X)).q) by A1,A2,B4,MSUALG_3:def 7
.= h.s.([o, the carrier of S]-tree p) by Th33;
end;
A8: for t being Term of S,X holds P[t] from MSATERM:sch 1(A6,A7);
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 A8;
end;
theorem HASH2:
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
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
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 HASH;
thus #(root-tree [x,s], w) = root-tree [w.s.x, s] by A3,A4;
end;
theorem HASH3:
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);
A7: 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
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 HASH;
rng p c= dom G
proof
let y be element; assume y in rng p;
then consider x such that
B1: x in dom p & y = p.x by FUNCT_1:def 3;
reconsider x as Nat by B1;
y is Term of S, X by B1,MSATERM:22;
then y in S-Terms X;
hence thesis by PARTFUN1:def 2;
end;
then
A6: dom (G*p) = dom p by RELAT_1:27;
now
let x; assume
B2: x in dom p;
then reconsider i = x as Nat;
reconsider t = p.i as Term of S,X by B2,MSATERM:22;
reconsider t as Element of Free(S,X) by A7,MSAFREE3:31;
thus q.x = #(t,w) by A2,B2 .= G.t by A4,A5,HASH1
.= (G*p).x by B2,FUNCT_1:13;
end;
then q = G*p by A1,A6,FUNCT_1:2;
hence #(Sym(o,X)-tree p, w) = Sym(o,(the carrier of S)-->NAT)-tree q
by A3,A5;
end;
theorem Th34:
for Y being ManySortedSubset of X
holds Free(S,Y) is MSSubAlgebra of Free(S,X)
proof
let Y be ManySortedSubset of X;
thus
A0: the Sorts of Free(S,Y) c= the Sorts of Free(S,X)
proof
let x; assume
x in the carrier of S;
then reconsider s = x as SortSymbol of S;
let z be element; 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
AA: B = the Sorts of Free(S,Y);
consider A1 being MSSubset of FreeMSA(Y (\/) ((the carrier of S) --> {0}))
such that
AB: Free(S,Y) = GenMSAlg A1 &
A1 = (Reverse (Y (\/)((the carrier of S) --> {0})))""Y by MSAFREE3:def 1;
thus
BB: B is opers_closed
proof
let o be OperSymbol of S;
let z be element;
assume z in rng ((Den(o,Free(S,X)))|((B# * the Arity of S).o ));
then consider a being element such that
A6: 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;
AG: a in dom (Den(o,Free(S,X))) /\ ((B# * the Arity of S).o )
by A6,RELAT_1:61;
then
A8: 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 AG,XBOOLE_0:def 4;
B4: (B# * the Arity of S).o = (B# ).the_arity_of o by FUNCT_2:15;
B5: (B# ).the_arity_of o = product (B*the_arity_of o) by FINSEQ_2:def 5;
B2: 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
B3: dom a = dom the_arity_of o by PARTFUN1:def 2,CARD_3:9;
z = Den(o,Free(S,X)).a by A6,A8,FUNCT_1:49;
then
B6: z = Sym(o,X)-tree a by Th33;
B9: now
let x; assume x in dom ((the Sorts of Free(S,Y))*(the_arity_of o));
hence a.x in ((the Sorts of Free(S,Y))*(the_arity_of o)).x
by A8,B4,B5,AA,CARD_3:9;
end;
then
B7: a in Args(o,Free(S,Y)) by B2,B3,CARD_3:9;
B8: Den(o,Free(S,Y)).a = [o,the carrier of S]-tree a
by B9,B2,B3,CARD_3:9,Th33;
thus z in (B * the ResultSort of S).o
by AA,B6,B7,B8,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 AB,MSUALG_2:def 9;
C2: A2 is_closed_on o by AB,MSUALG_2:def 6,def 9;
Free(S,Z) = FreeMSA Z by MSAFREE3:31;
then
CC: Args(o,Free(S,Y)) c= Args(o,Free(S,Z)) &
dom(Den(o,Free(S,Z))) = Args(o,Free(S,Z))
by AB,FUNCT_2:def 1,MSAFREE3:37;
then
C4: dom (Den(o,Free(S,Z))| Args(o,Free(S,Y))) = Args(o,Free(S,Y))
by RELAT_1:62;
C9: Args(o,Free(S,Y)) c= Args(o,Free(S,X))
proof
let x be element; assume x in Args(o,Free(S,Y)); then
C8: 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
C7: x = f & dom f = dom the_arity_of o & for y 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; assume
D1: 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 C7,D1,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 A0,D1,FUNCT_1:13,PBOOLE:def 2;
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 D1,FUNCT_1:13;
end;
then x in product ((the Sorts of Free(S,X))*the_arity_of o)
by C7,C8,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
C6: dom (Den(o,Free(S,X))| Args(o,Free(S,Y))) = Args(o,Free(S,Y))
by C9,RELAT_1:62;
CD: now let x; assume
D2: x in Args(o,Free(S,Y));
then
D2a: 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 D2,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 D2a,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;
D4: (Den(o,Free(S,X))| Args(o,Free(S,Y))).x = Den(o,Free(S,X)).x
by D2,FUNCT_1:49
.= [o, the carrier of S]-tree p by C9,D2,Th33;
thus (Den(o,Free(S,Z))| Args(o,Free(S,Y))).x
= Den(o,Free(S,Z)).x by D2,FUNCT_1:49
.= (Den(o,Free(S,X))| Args(o,Free(S,Y))).x by CC,D2,D4,Th33;
end;
thus (the Charact of Free(S,Y)).o
= Opers(FreeMSA Z,A2).o by AB,MSUALG_2:def 9
.= o/.A2 by MSUALG_2:def 8
.= Den(o,FreeMSA Z)| ((A2# * the Arity of S).o) by C2,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 AA,CD,C6,C4,FUNCT_1:2
.= o/.B by BB,MSUALG_2:def 6,MSUALG_2:def 7;
end;
hence the Charact of Free(S,Y) = Opers(Free(S,X),B) by AA,MSUALG_2:def 8;
end;
theorem Th48:
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
B1: #(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 HASH;
B2: #(t,w) = root-tree [w.s.x,s] by B1;
dom w = the carrier of S by PARTFUN1:def 2;
then rng (w.s) = (rngs w).s by FUNCT_6:22;
then
B3: w.s.x in (rngs w).s by FUNCT_2:4;
then reconsider tw = #(t,w) as Term of S, rngs w by B2,MSATERM:4;
the_sort_of tw = s & the_sort_of t = s by B2,B3,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;
A2: 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
B3: 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
B1: #(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 HASH;
B2: #(tt,w) = Sym(o,(the carrier of S)-->NAT)-tree(F*p) by B1;
B4: 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
B7: 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
C2: dom p = dom the_arity_of o by CARD_3:9;
B6: 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;
C5: rng p c= Union the Sorts of Free(S,X)
proof let y be element; assume y in rng p;
then consider x such that
C1: 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 B7,C1,C2,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 C1,C2,FUNCT_1:13,102,PARTFUN1:def 2;
hence thesis by CARD_5:2;
end;
then
B5: dom (F*p) = dom p by B6,RELAT_1:27
.= dom the_arity_of o by B7,CARD_3:9;
CA: now
let y; assume
C3: y in dom the_arity_of o;
then
C4: p.y in rng p by C2,FUNCT_1:def 3;
p.y is Element of FreeMSA X by C4,C5,MSAFREE3:31;
then reconsider t = p.y as Term of S,X by MSAFREE3:6;
C7: P[t] & F.t = #(t,w) by B1,B3,C4,C5,HASH1;
reconsider i = y as Nat by C3;
(the_arity_of o).i = the_sort_of t by C2,C3,MSATERM:23;
then F.t in (the Sorts of Free(S,rngs w)).((the_arity_of o).i) by C7;
then F.t in ((the Sorts of Free(S,rngs w))*the_arity_of o).i
by C3,FUNCT_1:13;
hence (F*p).y in ((the Sorts of Free(S,rngs w))*the_arity_of o).y
by C2,C3,FUNCT_1:13;
end;
Den(o,Free(S,rngs w)).(F*p) = [o,the carrier of S]-tree (F*p)
by CA,B4,B5,CARD_3:9,Th33;
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 CA,B4,B5,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 B2,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,A2);
then P[t];
hence #(t,w) is Element of Free(S, rngs w), the_sort_of t;
then
TT: #(t,w) in (the Sorts of Free(S, rngs w)).the_sort_of t;
X is_transformable_to (the carrier of S)-->NAT by Th96;
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 Th34;
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 TT;
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 element; assume y in rng p;
then consider x such that
B1: x in dom p & y = p.x by FUNCT_1:def 3;
reconsider x as Nat by B1;
y is Term of S, X by B1,MSATERM:22;
then y in S-Terms X;
hence thesis by PARTFUN1:def 2;
end;
then
A3: dom (F*p) = dom p by RELAT_1:27;
A4: dom p = dom the_arity_of o by MSATERM:22;
A9: 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 Th96;
then rngs w is ManySortedSubset of (the carrier of S)-->NAT
by PBOOLE:def 18,MSSUBFAM:17;
then
AA: Free(S, rngs w) is MSSubAlgebra of Free(S, (the carrier of S)-->NAT)
by Th34;
now
let i be Nat;
assume
F1: i in dom p;
then reconsider t = p.i as Term of S,X by MSATERM:22;
F.t = #(t,w) by A1,A2,A9,HASH1;
then reconsider tt = F.t as Element of (the Sorts of Free(S, rngs w)).
the_sort_of t by Th48;
F3: the Sorts of Free(S, rngs w) is MSSubset of
Free(S, (the carrier of S)-->NAT) by AA,MSUALG_2:def 9;
reconsider tt as Term of S, rngs w by Th27;
take tt; thus tt = (F*p).i by F1,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 F3,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 F1,MSATERM:23;
end;
then F*p is ArgumentSeq of Sym(o, rngs w)
by A3,A4,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 AA,MSAFREE3:37;
hence thesis;
end;
theorem Th18:
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(element,Function) = root-tree [w.$1.($2.{})`1, $1];
consider ww being ManySortedFunction of the carrier of S such that
A0: 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;
B0: ww is ManySortedFunction of FreeGen Y, FreeGen X
proof
let x be set; assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
B1: dom(ww.s) = (FreeGen Y).s by A0;
B2: (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 element; assume y in rng(ww.s);
then consider z such that
B3: z in dom(ww.s) & y = ww.s.z by FUNCT_1:def 3;
reconsider z as Element of (FreeGen Y).s by A0,B3;
consider v being set such that
B4: v in Y.s & z = root-tree [v,s] by B2,MSAFREE:def 15;
B5: y = F(s,z) by A0,B3;
z.{} = [v,s] by B4,TREES_4:3;
then (z.{})`1 = v by MCART_1:7;
then w.s.(z.{})`1 in X.s by B4,FUNCT_2:5;
hence thesis by B2,B5,MSAFREE:def 15;
end;
hence thesis by B1,FUNCT_2:2;
end;
reconsider G = FreeGen Y as GeneratorSet of TermAlg S;
FreeGen X is MSSubset of A by AVAR;
then reconsider ww as ManySortedFunction of G, the Sorts of A by B0,Th108;
consider h being ManySortedFunction of TermAlg S, A such that
A1: h is_homomorphism TermAlg S, A & ww = h||G by MSAFREE:def 5;
take h; thus h is_homomorphism TermAlg S, A by A1;
let s be SortSymbol of S, i be Nat;
A2: ww.s = (h.s)|(G.s) by A1,MSAFREE:def 1;
i in NAT & NAT = Y.s by ORDINAL1:def 12,FUNCOP_1:7;
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 A2,FUNCT_1:49
.= F(s,z) by A0 .= root-tree [w.s.[i,s]`1, s] by TREES_4:3
.= root-tree [w.s.i, s] by MCART_1:7;
end;
theorem Th19:
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(element,Function) = root-tree [w.$1.($2.{})`1, $1];
consider ww being ManySortedFunction of the carrier of S such that
A0: 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;
B0: ww is ManySortedFunction of FreeGen X, FreeGen Y
proof
let x be set; assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
B1: dom(ww.s) = (FreeGen X).s by A0;
B2: (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 element; assume y in rng(ww.s);
then consider z such that
B3: z in dom(ww.s) & y = ww.s.z by FUNCT_1:def 3;
reconsider z as Element of (FreeGen X).s by A0,B3;
consider v being set such that
B4: v in X.s & z = root-tree [v,s] by B2,MSAFREE:def 15;
B5: y = F(s,z) by A0,B3;
z.{} = [v,s] by B4,TREES_4:3;
then (z.{})`1 = v by MCART_1:7;
then w.s.(z.{})`1 in Y.s by B4,FUNCT_2:5;
hence thesis by B2,B5,MSAFREE:def 15;
end;
hence thesis by B1,FUNCT_2:2;
end;
set A = the inheriting_operations all_vars_including (X,S)-terms
MSAlgebra over S;
reconsider G = FreeGen X as GeneratorSet of A by Th111;
reconsider ww as ManySortedFunction of FreeGen X,
the Sorts of TermAlg S by B0,Th108;
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 A0 .= root-tree [w.s.[i,s]`1, s] by TREES_4:3
.= root-tree [w.s.i, s] by MCART_1:7;
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
A0: v is "1-1";
set Z = (the carrier of S)-->NAT;
deffunc F(element) = (NAT-->the Element of X0.$1)+*(v.$1)";
consider w being ManySortedSet of S such that
A2: for s being SortSymbol of S holds w.s = F(s) from PBOOLE:sch 5;
w is Function-yielding
proof
let x; assume x in dom w;
then w.x = F(x) by A2;
hence thesis;
end;
then reconsider w as ManySortedFunction of the carrier of S;
w is ManySortedFunction of Z,X0
proof
let x be set; 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
B0: w.x = F(s) & v.s is one-to-one & Z.s = NAT & rng(v.s) c= Z.s
by A0,A2,MSUALG_3:def 2,FUNCOP_1:7;
then
B1: dom (w.s) = dom(NAT-->the Element of X0.s)\/ dom((v.s)") by FUNCT_4:def 1
.= NAT \/ dom((v.s)") by FUNCOP_1:13
.= NAT\/rng(v.s) by B0,FUNCT_1:33 .= NAT by B0,XBOOLE_1:12;
B3: Z.s = NAT by FUNCOP_1:7;
rng (w.s) c= X0.s
proof
let x be element; assume x in rng (w.s);
then consider y such that
B2: 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 B0,B2,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 A0,B1,B2,FUNCOP_1:7,MSUALG_3:def 2;
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 B1,B3,FUNCT_2:2;
end;
then reconsider w as ManySortedFunction of Z,X0;
consider ww being ManySortedFunction of TermAlg S, A such that
A3: 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 Th18;
B1: dom v = the carrier of S by PARTFUN1:def 2;
rngs v c= Z
proof
let s being element; reconsider x = s as set by TARSKI:1;
assume s in the carrier of S;
then (rngs v).s = rng (v.x) by B1,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;
AC: Free(S,Z) = TermAlg S by MSAFREE3:31;
A8: Free(S,Y) is MSSubAlgebra of Free(S,Z) by Th34;
then reconsider B = the Sorts of Free(S,Y) as MSSubset of TermAlg S
by AC,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 Th111;
consider vv being ManySortedFunction of G, the Sorts of TermAlg S such that
A5: 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 Th19;
consider g being ManySortedFunction of A,A such that
A4: g is_homomorphism A,A & g||G = h**vv by FREEITSELF;
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 A4,A3,AC,A8,EQUATION:22; then
A7: 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;
HH: now
let x; assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
C2: dom ((hB||H).s) = H.s & dom (((g**wB)||H).s) = H.s by FUNCT_2:def 1;
now let y; assume
C4: y in H.s; then y in FreeGen(s,Y) by MSAFREE:def 16;
then consider z being set such that
C3: z in Y.s & y = root-tree [z,s] by MSAFREE:def 15;
C7: H.s c= B.s & Y.s c= Z.s by PBOOLE:def 2,def 18;
then
C5: w.s.z in X0.s by C3,FUNCT_2:5;
wB.s = (ww.s)|(B.s) & z in Z.s by C3,C7,MSAFREE:def 1;
then
C9: wB.s.y = ww.s.y & z in NAT by C4,C7,FUNCT_1:49,FUNCOP_1:7;
then wB.s.y = root-tree[w.s.z,s] by A3,C3;
then wB.s.y in FreeGen(s,X0) by C5,MSAFREE:def 15;
then
C6: wB.s.y in G.s by MSAFREE:def 16;
z in Z.s by C3,C7; then
z in NAT by FUNCOP_1:7; then
C0: vv.s.(ww.s.y) = vv.s.root-tree [w.s.z, s] by A3,C3
.= root-tree [v.s.(w.s.z), s] by A5,C5
.= root-tree [v.s.(((NAT-->the Element of X0.s)+*((v.s)")).z), s]
by A2;
dom v = the carrier of S by PARTFUN1:def 2;
then
E3: v.s is one-to-one & rng(v.s) = Y.s
by A0,FUNCT_6:22,MSUALG_3:def 2;
E1: z in dom ((v.s)") by C3,E3,FUNCT_1:33;
E5: vv.s.(ww.s.y) = root-tree [v.s.((((v.s)")).z), s]
by C0,E1,FUNCT_4:13
.= y by C3,E3,FUNCT_1:35;
EE: rngs vv c= B
proof
let x; assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
let y be element; assume
D0: y in (rngs vv).x;
dom vv = the carrier of S by PARTFUN1:def 2;
then y in rng (vv.s) by D0,FUNCT_6:22;
then consider z such that
D1: 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
D2: a in X0.s & z = root-tree[a,s] by D1,MSAFREE:def 15;
v.s.a in rng (v.s) & dom v = the carrier of S
by D2,FUNCT_2:4,PARTFUN1:def 2;
then v.s.a in Y.s & y = root-tree[v.s.a, s] by D1,D2,A5,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;
E7: dom (hB**vv) = (the carrier of S)/\the carrier of S
by PARTFUN1:def 2;
E8: 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 C4,FUNCT_1:49
.= ((hB.s)*(vv.s)).(wB.s.y) by E5,C9,C6,FUNCT_2:15
.= ((hB**vv).s).(wB.s.y) by E7,PBOOLE:def 19
.= (g||G).s.(wB.s.y) by A4,EE,EXTENS_1:11
.= ((g.s)|(G.s)).(wB.s.y) by MSAFREE:def 1
.= g.s.(wB.s.y) by C6,FUNCT_1:49
.= ((g.s)*(wB.s)).y by C7,C4,FUNCT_2:15
.= ((g**wB).s).y by E8,PBOOLE:def 19
.= (((g**wB).s)|(H.s)).y by C4,FUNCT_1:49
.= ((g**wB)||H).x .y by MSAFREE:def 1;
end;
hence (hB||H).x = ((g**wB)||H).x by C2,FUNCT_1:2;
end;
hB is_homomorphism Free(S,Y), A by A1,A8,AC,EQUATION:22;
hence h||B = g**wB by HH,A7,EXTENS_1:19,PBOOLE:3;
let s be SortSymbol of S, i be Nat; assume
H1: i in Y.s;
H2: dom v = the carrier of S by PARTFUN1:def 2;
then
H3: v.s is one-to-one by A0,MSUALG_3:def 2;
then
H4: rng ((v.s)") = dom (v.s) & dom (v.s) = X0.s & rng (v.s) = Y.s &
dom((v.s)") = rng (v.s) by H2,FUNCT_1:33,FUNCT_2:def 1,FUNCT_6:22;
then reconsider x = (v.s)".i as Element of X0.s by H1,FUNCT_1:def 3;
take x; thus v.s.x = i by H1,H3,H4,FUNCT_1:35;
root-tree [i,s] in FreeGen(s,Y) & H c= B
by H1,PBOOLE:def 18,MSAFREE:def 15;
then
H5: root-tree [i,s] in H.s & H.s c= B.s by PBOOLE:def 2,MSAFREE:def 16;
w.s = F(s) by A2;
then x = w.s.i by H1,H4,FUNCT_4:13;
then root-tree [x, s] = ww.s.root-tree [i,s] by A3
.= ((ww.s)|(B.s)).root-tree [i,s] by H5,FUNCT_1:49;
hence wB.s.root-tree [i,s] = root-tree [x, s] by MSAFREE:def 1;
end;
theorem Th50:
for h being ManySortedFunction of Free(S,X0), A0 st
h is_homomorphism Free(S,X0), A0
ex g being ManySortedFunction of A0,A0 st
g is_homomorphism A0,A0 & h = g**canonical_homomorphism A0
proof set A = A0;
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 Th111;
reconsider G = FreeGen X0 as GeneratorSet of A by Th111;
AB: 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 a: 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 by PBOOLE:def 2;
hence ww.s.root-tree [i,s] = root-tree [i, s] by a,Th107;
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 CH;
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
A4: g is_homomorphism A,A & g||G = hG by FREEITSELF;
take g;
thus g is_homomorphism A,A by A4;
A7: g**ww is_homomorphism Free(S,X0),A by A3,A4,MSUALG_3:10;
now
let x; assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
C2: dom ((h||H).s) = H.s & dom (((g**ww)||H).s) = H.s by FUNCT_2:def 1;
now let y; assume
C4: y in H.s; then y in FreeGen(s,X0) by MSAFREE:def 16;
then consider z being set such that
C3: z in X0.s & y = root-tree [z,s] by MSAFREE:def 15;
C8: ww.s.y = root-tree[z,s] by AB,C3;
then ww.s.y in FreeGen(s,X0) by C3,MSAFREE:def 15;
then
C6: ww.s.y in G.s by MSAFREE:def 16;
C7: H.s c= (the Sorts of Free(S,X0)).s by PBOOLE:def 2,def 18;
E8: 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 C3,C8,A4,MSAFREE:def 1
.= g.s.(ww.s.y) by C6,FUNCT_1:49
.= ((g.s)*(ww.s)).y by C4,C7,FUNCT_2:15
.= ((g**ww).s).y by E8,PBOOLE:def 19
.= (((g**ww).s)|(H.s)).y by C4,FUNCT_1:49
.= ((g**ww)||H).x .y by MSAFREE:def 1;
end;
hence (h||H).x = ((g**ww)||H).x by C2,FUNCT_1:2;
end;
hence h = g**ww by A1,A7,EXTENS_1:19,PBOOLE:3;
end;
theorem Th69:
for o being OperSymbol of S
for x being Element of Args(o,A0) holds
for x0 being Element of Args(o,Free(S,X0)) st x0 = x holds
(canonical_homomorphism A0)#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,X0));
assume Z0: x0 = x;
set k = canonical_homomorphism A;
now
let n being Nat;
assume
A0: n in dom x0;
A2: dom x = dom the_arity_of o by MSUALG_3:6; then
A1: (the_arity_of o)/.n = (the_arity_of o).n by Z0,A0,PARTFUN1:def 6;
dom ((the Sorts of A)*the_arity_of o) = dom x by A2,PRALG_2:3; then
x .n in ((the Sorts of A)*the_arity_of o).n by Z0,A0,MSUALG_3:6; then
x .n is Element of A, (the_arity_of o)/.n by A1,A0,Z0,A2,FUNCT_1:13;
hence x .n = k.((the_arity_of o)/.n).(x0.n) by Z0,Th107;
end;
hence (canonical_homomorphism A)#x0 = x by MSUALG_3:def 6;
end;
theorem Th68:
for o being OperSymbol of S
for x being Element of Args(o,A0) holds
Den(o,A0).x =
(canonical_homomorphism A0).(the_result_sort_of o).(Den(o,Free(S,X0)).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,X0)) by ThA; then
reconsider x0 = x as Element of Args(o,Free(S,X0));
k#x0 = x by Th69;
hence Den(o,A).x
= k.(the_result_sort_of o).(Den(o,Free(S,X0)).x) by CH,MSUALG_3:def 7;
end;
theorem Th68A:
for h being ManySortedFunction of Free(S,X0), A0
st h is_homomorphism Free(S,X0), A0
for o being OperSymbol of S
for x being Element of Args(o,A0) holds
h.(the_result_sort_of o).(Den(o,A0).x)
= h.(the_result_sort_of o).(Den(o,Free(S,X0)).x)
proof set A = A0;
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
A0: g is_homomorphism A,A & h = g**canonical_homomorphism A by Th50;
let o be OperSymbol of S;
let x be Element of Args(o,A);
A3: dom h = the carrier of S & dom canonical_homomorphism A = the carrier of S
by PARTFUN1:def 2;
A6: dom (h**canonical_homomorphism A) = (dom h)/\dom canonical_homomorphism A
by PBOOLE:def 19;
AC: x in Args(o,A) & Args(o,A) c= Args(o,Free(S,X0)) by ThA;
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 Th68
.= ((h.the_result_sort_of o)*((canonical_homomorphism A).
(the_result_sort_of o))).(Den(o,Free(S,X0)).x) by AC,MSUALG_9:18,FUNCT_2:15
.= (h**canonical_homomorphism A).
(the_result_sort_of o).(Den(o,Free(S,X0)).x) by A3,A6,PBOOLE:def 19
.= (g**((canonical_homomorphism A)**(canonical_homomorphism A))).
(the_result_sort_of o).(Den(o,Free(S,X0)).x) by A0,PBOOLE:140
.= h.(the_result_sort_of o).(Den(o,Free(S,X0)).x) by A0,Th67;
end;
theorem Th68B:
for h being ManySortedFunction of Free(S,X0), A0
st h is_homomorphism Free(S,X0), A0
for o being OperSymbol of S
for x being Element of Args(o,Free(S,X0)) holds
h.(the_result_sort_of o).(Den(o,Free(S,X0)).x)
= h.(the_result_sort_of o).(Den(o,Free(S,X0)).
((canonical_homomorphism A0)#x))
proof set A = A0;
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
A0: g is_homomorphism A,A & h = g**canonical_homomorphism A by Th50;
let o be OperSymbol of S;
let x be Element of Args(o,Free(S,X0));
set k = canonical_homomorphism A;
A8: k#x in Args(o,A) & Args(o,A) c= Args(o,Free(S,X0)) by ThA;
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 A0,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 CH,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 Th68
.= ((g.the_result_sort_of o)*((canonical_homomorphism A).
the_result_sort_of o)).(Den(o,Free(S,X0)).(((canonical_homomorphism A))#x))
by A8,MSUALG_9:18,FUNCT_2:15
.= h.(the_result_sort_of o).(Den(o,Free(S,X0)).
((canonical_homomorphism A)#x)) by A0,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 Th111;
reconsider H = FreeGen X0 as GeneratorSet of Free(S,X0) by Th111;
reconsider G = FreeGen X0 as GeneratorSet of A by Th111;
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 a: 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 by PBOOLE:def 2;
hence ww.s.root-tree [i,s] = root-tree [i, s] by a,Th107;
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 CH;
the Sorts of A is MSSubset of Free(S,X0) by TERM;
then reconsider hG = h||F as ManySortedFunction of
F qua ManySortedSet of S, the Sorts of Free(S,X0) by Th108;
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 by MSAFREE:def 5;
take g;
thus g is_homomorphism Free(S,Y),Free(S,X0) by A4;
A7: ww**g is_homomorphism Free(S,Y),A by A3,A4,MSUALG_3:10;
now
let x; assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
C2: dom ((h||F).s) = F.s & dom (((ww**g)||F).s) = F.s by FUNCT_2:def 1;
now let y; assume
C4: y in F.s;
C9: g.s.y = ((g.s)|(F.s)).y by C4,FUNCT_1:49
.= (h||F).s.y by A4,MSAFREE:def 1;
then
Ca: g.s.y in (the Sorts of A).s by C4,FUNCT_2:5;
C7: F.s c= (the Sorts of Free(S,Y)).s by PBOOLE:def 2,def 18;
E8: 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 C9,Ca,Th107
.= ((ww.s)*(g.s)).y by C4,C7,FUNCT_2:15
.= ((ww**g).s).y by E8,PBOOLE:def 19
.= (((ww**g).s)|(F.s)).y by C4,FUNCT_1:49
.= ((ww**g)||F).x .y by MSAFREE:def 1;
end;
hence (h||F).x = ((ww**g)||F).x by C2,FUNCT_1:2;
end;
hence h = ww**g by A1,A7,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;
W1: 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 Z0: t3 = k.s.t;
assume Z1: t1 = #(t,w);
assume Z2: t2 = #(t3,w);
t1 = root-tree [w.s1.v, s1] & FreeMSA Y = Free(S,Y)
by Z1,HASH2,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 ThE; then
t3 = t by Z0,Th107;
hence A |= t1 '=' t2 by ThE0,Z1,Z2;
end;
W2: 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 Z1: t3 = k.s.t;
assume Z2: t1 = #(t,w);
assume Z3: t2 = #(t3,w);
A0: FreeMSA X0 = Free(S,X0) by MSAFREE3:31; then
reconsider a = p as Element of Args(o,Free(S,X0)) by INSTALG1:1;
BB: t = Den(o,Free(S,X0)).a by A0,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 Th27;
defpred Q[Nat,element] means
for t being Element of Free(S,X0) st t = p.$1 holds $2 = #(t,w);
B0: dom p = Seg len p by FINSEQ_1:def 3;
B1: for i being Nat st i in Seg len p ex x st Q[i,x]
proof
let i be Nat;
assume i in Seg len p; then
p.i is Term of S,X0 by B0,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
B2: 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(B1);
now
thus dom q = dom p by FINSEQ_1:def 3,B2;
thus 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 B0,B2;
end; then
AA: t1 = Sym(o,Y)-tree q by Z2,HASH3;
now
let i be set; assume
B3: i in dom q; then
p.i is Term of S,X0 by B0,B2,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 B2,B3; 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 AA,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
A1: 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 A1,BB,MSUALG_9:18;
V4: the Sorts of A is MSSubset of Free(S,X0) by TERM;
k.s.tt in (the Sorts of A).s &
(the Sorts of A).s c= (the Sorts of Free(S,X0)).s
by V4,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
ZZ: h is_homomorphism TermAlg S, A;
consider hh being ManySortedFunction of Free(S,X0), TermAlg S such that
YY: 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 HASHA;
VV: 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 V4,PBOOLE:def 2,def 18,FUNCT_2:5,A1,MSUALG_9:18;
(t1 '=' t2)`1 = t1 & (t1 '=' t2)`2 = t2 by MCART_1:7;
hence h.s.(t1 '=' t2)`1 = h.s.(hh.s.tt) by Z2,YY
.= h.s.(hh.s.(Den(o,Free(S,X0)).a)) by A0,INSTALG1:3
.= ((h.s)*(hh.s)).(Den(o,Free(S,X0)).a) by A1,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 A1,Th68B,ZZ,YY,MSUALG_3:10
.= ((h**hh).s).(Den(o,A).(k#a)) by Th68A,ZZ,YY,MSUALG_3:10,A1
.= ((h**hh).s).(k.s.(Den(o,Free(S,X0)).a)) by A1,CH,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 VV,FUNCT_2:15
.= h.s.(hh.s.kt) by A0,INSTALG1:3
.= h.s.t2 by Z1,Z3,YY
.= h.s.(t1 '=' t2)`2 by MCART_1:7;
end;
GG: for t being Term of S,X0 holds P[t] from MSATERM:sch 1(W1,W2);
let t be Element of (the Sorts of Free(S,X0)).s;
II: t is Term of S,X0 by Th27;
let t1,t2 be Element of TermAlg S, s;
assume Z0: t1 = #(t,w);
assume Z1: 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 Th27;
hence A |= t1 '=' t2 by II,GG,Z0,Z1;
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,CH,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 Z0: w is "1-1";
A0: 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);
A2: 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
B1: x in Y.s & t = root-tree [x,s] by MSAFREE:def 15;
reconsider x as Element of Y.s by B1;
per cases;
suppose
B2: x in rng(w.s); then
consider a being element such that
B3: 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 B3,MSAFREE3:4;
take T;
let x0 be Element of Y.s; assume t = root-tree [x0,s]; then
B6: [x0,s] = [x,s] by B1,TREES_4:4; then
B5: x = x0 by XTUPLE_0:1;
w.s is one-to-one by Z0,MSUALG_3:1;
hence x0 in rng(w.s) implies T = root-tree [(w.s)".x0,s]
by B3,B5,FUNCT_1:34;
thus thesis by B2,B6,XTUPLE_0:1;
end;
suppose
B2: 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 B1,TREES_4:4;
hence thesis by B2,XTUPLE_0:1;
end;
end;
consider gg being ManySortedFunction of G, the Sorts of Free(S,X0)
such that
A3: for s being SortSymbol of S for t being Element of G.s
holds P[s,t,gg.s.t] from CIRCTRM1:sch 1(A2);
consider g being ManySortedFunction of TermAlg S, Free(S,X0) such that
A4: 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 A4;
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;
W1: 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
C0: t in (the Sorts of Free(S,X0)).s0;
t in (the Sorts of Free(S,X0)).s by MSAFREE3:4; then
C1: s = s0 by C0,XBOOLE_0:3,PROB_2:def 2; then
C2: 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
C3: root-tree [w.s0.v,s0] in G.s0 by MSAFREE:def 16; then
C4: gg.s0.root-tree [w.s0.v,s0] = root-tree [(w.s0)".(w.s0.v),s0] by C2,A3;
C5: #(t,w) = root-tree [w.s0.v,s0] by C1,HASH2;
gg.s0 = (g.s0)|(G.s0) by A4,MSAFREE:def 1; then
C6: g.s0.root-tree [w.s0.v,s0] = root-tree [(w.s0)".(w.s0.v),s0]
by C3,C4,FUNCT_1:49;
w.s0 is one-to-one by Z0,MSUALG_3:1;
hence thesis by C1,C5,C6,FUNCT_2:26;
end;
W2: 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
Z1: 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
C0: 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 A0,MSAFREE:def 11;
then
C1: s = the_result_sort_of o by C0,XBOOLE_0:3,PROB_2:def 2;
defpred Q[Nat,element] means
for t being Element of Free(S,X0) st t = p.$1 holds $2 = #(t,w);
B0: dom p = Seg len p by FINSEQ_1:def 3;
B1: for i being Nat st i in Seg len p ex x st Q[i,x]
proof
let i be Nat;
assume i in Seg len p; then
p.i is Term of S,X0 by B0,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
B2: 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(B1);
now
thus dom q = dom p by FINSEQ_1:def 3,B2;
thus 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 B0,B2;
end; then
AA: #(t,w) = Sym(o,Y)-tree q by HASH3;
now
let i be set; assume
B3: i in dom q; then
p.i is Term of S,X0 by B0,B2,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 B2,B3; then
q.i is Element of Free(S, Y) by MSAFREE3:31;
hence q.i is DecoratedTree;
end; then
D1: 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 Th27,D1,AA,TREES_4:def 4; then
consider r being ArgumentSeq of Sym(o,Y) such that
A5: #(t,w) = [o,the carrier of S]-tree r by MSATERM:10;
r = q by D1,AA,A5,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 A0,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 Z2: n in dom q;
D2: 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 Z2,MSATERM:22;
D3: tn in rng p by Z2,D2,FUNCT_1:def 3;
the_sort_of tn = (the_arity_of o)/.n by Z2,D2,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 A0,MSAFREE:def 11; then
D4: g.((the_arity_of o)/.n). #(tn,w) = tn by Z1,D3;
Q[n,q.n] & tn is Element of Free(S,X0)
by A0,B2,Z2,MSATERM:13;
hence a.n = (g.((the_arity_of o)/.n)).(q.n) by D4;
end; then
A6: g#q = a by MSUALG_3:def 6;
thus g.s. #(t,w) = g.s.(Den(o,TermAlg S).q) by AA,INSTALG1:3
.= Den(o,Free(S,X0)).(g#q) by A4,C1,MSUALG_3:def 7
.= t by A0,A6,INSTALG1:3;
end;
WW: for t being Term of S,X0 holds P[t] from MSATERM:sch 1(W1,W2);
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 Th27;
hence g.s. #(t,w) = t by WW;
end;
theorem Th77:
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 Z0: 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
A1: 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 Z2: t3 = #(t1,w);
assume Z3: t4 = #(t2,w);
A4: (t3 '=' t4)`1 = t3 & (t3 '=' t4)`2 = t4 by MCART_1:7;
assume A |= t3 '=' t4; then
A5: (h**g).s.(t3 '=' t4)`1 = (h**g).s.(t3 '=' t4)`2
by A1,Z0,MSUALG_3:10,EQUATION:def 5;
(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 A1,A4,A5,Z2 .= h.s.t2 by A1,Z3;
end;
theorem ThFree:
for G being GeneratorSet of A0 st G = FreeGen X0
holds G is Equations(S,A0)-free
proof set A = A0;
A0: FreeMSA X0 = Free(S,X0) by MSAFREE3:31;
let G be GeneratorSet of A; assume
A1: 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 A1;
reconsider H = FreeGen X0 as free GeneratorSet of Free(S,X0)
by A0;
consider g being ManySortedFunction of Free(S,X0), B such that
A2: 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 TERM; then
reconsider i = id the Sorts of A as ManySortedFunction of A, Free(S,X0)
by Th108;
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
C1: Den(o,A).x in (the Sorts of A).s by FUNCT_2:15;
C2: 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 ThA; 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 Th27;
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 Th13;
f1 in (the Sorts of A).s by MSUALG_9:18; then
f1 is Element of Free(S,X0),s by Th13; 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 A0,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 Th48;
AC: f1 = (canonical_homomorphism A).s.f by Th68;
A |= t1 '=' t2 by AC,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 EQUAL,SAT; then
AB: g.s.f = g.s.fa by AC,A2,Th77,EQUATION:def 6;
Ae: now
let n be Nat;
set an = (the_arity_of o)/.n;
assume
S1: n in dom x;
S3: 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 S1,MSUALG_3:6; then
x .n in (the Sorts of A).((the_arity_of o).n) by S1,S3,FUNCT_1:13; then
S2: x .n in (the Sorts of A).an by S1,S3,PARTFUN1:def 6;
thus (h#x).n = (h.(an)).(x .n) by S1,MSUALG_3:def 6
.= ((g.an)*(i.an)).(x .n) by MSUALG_3:2
.= (g.an).((i.an).(x .n)) by S2,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 S2,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 C1,FUNCT_2:15
.= (g.s).(Den(o,A).x) by C2,C1,FUNCT_1:18
.= (g.s).(Den(o,Free(S,X0)).x0) by AB,Th68
.= Den(o,B).(g#x0) by A2,MSUALG_3:def 7
.= Den(o,B).(h#x) by Ae,MSUALG_3:def 6;
end;
F1: dom(h||G) = the carrier of S by PARTFUN1:def 2;
F2: dom f = the carrier of S by PARTFUN1:def 2;
now let x; assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
F6: 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
F3: dom (((g.s)*(i.s))|(G.s)) = G.s by F6,RELAT_1:62;
the Sorts of A is MSSubset of Free(S,X0) by TERM; 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 F6,XBOOLE_1:1,FUNCT_2:def 1;
then
F4: dom ((g.s)|(H.s)) = G.s by A1,RELAT_1:62;
F5: now
let x; assume
F7: 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 F6,F7,FUNCT_2:15
.= (g.s).((id ((the Sorts of A).s)).x) by MSUALG_3:def 1
.= g.s.x by F6,F7,FUNCT_1:17
.= ((g.s)|(H.s)).x by A1,F7,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 F3,F4,F5,FUNCT_1:2
.= f.x by A2,MSAFREE:def 1;
end;
hence h || G = f by F1,F2,FUNCT_1:2;
end;
theorem
A0 is Equations(S,A0)-free
proof
reconsider G = FreeGen X0 as GeneratorSet of A0 by Th111;
take G; thus thesis by ThFree;
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 element;
redefine func R.x -> Relation of X.x,Y.x;
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: TERMIN:
for x being set st x in I holds R.x is strongly-normalizing;
attr R is with_UN_property means: UNP:
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
proof
let E be empty set;
thus E is strongly-normalizing
proof
let f be ManySortedSet of NAT;
thus thesis;
end;
let a,b be element;
thus thesis by REWRITE1:27;
end;
end;
theorem Th201:
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-->{};
now let i be set;
assume i in I;
then R.i = {} by FUNCOP_1:7;
hence R.i is Relation of A.i by XBOOLE_1:2;
end;
then reconsider R as ManySortedRelation of A by MSUALG_4:def 1;
take R;
thus R = I-->{};
let i be set;
assume i in I;
hence R.i is strongly-normalizing by FUNCOP_1:7;
end;
registration
let I be set;
let X be ManySortedSet of I;
cluster empty-yielding -> with_UN_property terminating
for ManySortedRelation of X;
coherence
proof
let R be ManySortedRelation of X;
assume
A1: R is empty-yielding;
thus R is with_UN_property
proof
let i be set;
assume i in I;
thus thesis by A1;
end;
let i be set;
assume i in I;
thus thesis by A1;
end;
cluster empty-yielding for ManySortedRelation of X;
existence
proof
consider R being ManySortedRelation of X such that
A1: R = I-->{} & R is terminating by Th201;
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 element;
cluster R.i -> strongly-normalizing for Relation;
coherence
proof
per cases;
suppose i in I;
hence thesis by TERMIN;
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 element;
cluster R.i -> with_UN_property for Relation;
coherence
proof
per cases;
suppose i in I;
hence thesis by UNP;
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: NFV:
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 Th202:
x is_a_normal_form_wrt {}
proof
assume ex y st [x,y] in {};
hence thesis;
end;
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 by Th202;
end;
thus R is invariant
proof let s be SortSymbol of S;
thus thesis by A1;
end;
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,REWRITE1:def 3;
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;
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) by REWRITE1:def 6;
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 Z1: [y,z] in R;
z in field R & field R c= X \/ X by Z1,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: NFORM:
for i being Element of I holds
it.i = {nf(x,R.i) where x is Element of X.i: not contradiction};
existence
proof
deffunc F(Element of I) =
{nf(x,R.$1) where x is Element of X.$1: not contradiction};
consider A being ManySortedSet of I such that
A1: for i being Element of I holds A.i = F(i) from PBOOLE:sch 5;
A3: A is ManySortedSubset of X
proof
let i be element;
assume i in I;
then reconsider j = i as Element of I;
A2: A.j = {nf(x,R.j) where x is Element of X.j: not contradiction} by A1;
let x be element; assume x in A.i;
then ex y being Element of X.j st x = nf(y,R.j) by A2;
hence thesis;
end;
A is non-empty
proof
let i be element;
assume i in I;
then reconsider j = i as Element of I;
A2: A.j = {nf(x,R.j) where x is Element of X.j: not contradiction} by A1;
set x = the Element of X.j;
nf(x,R.j) in A.i by A2;
hence thesis;
end;
hence thesis by A1,A3;
end;
uniqueness
proof
let A1,A2 be non-empty ManySortedSubset of X such that
A1: for i being Element of I holds
A1.i = {nf(x,R.i) where x is Element of X.i: not contradiction} and
A2: for i being Element of I holds
A2.i = {nf(x,R.i) where x is Element of X.i: not contradiction};
let i be Element of I;
thus A1.i = {nf(x,R.i) where x is Element of X.i: not contradiction} by A1
.= A2.i by A2;
end;
end;
scheme MSFLambda {B()->non empty set,D(element)->non empty set,
F(element,element)->element}:
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[element,element] 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 element st o in B() ex g being element st P[o,g]
proof
let o be element; assume o in B();
deffunc G(element) = F(o,$1);
consider g being Function such that
A2: dom g = D(o) & for x 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
A2: for o being element st o in B() holds P[o,f.o] from PBOOLE:sch 3(A1);
f is Function-yielding
proof
let o be element; assume o in dom f;
then P[o,f.o] by A2;
hence f.o is Function;
end;
then reconsider f as ManySortedFunction of B();
take f;
let o be Element of B();
A3: P[o,f.o] by A2;
hence dom (f.o) = D(o);
let x be Element of D(o);
thus f.o.x = F(o,x) by A3;
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: NFALG:
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 set; assume
i in the carrier' of S;
then reconsider o = i as OperSymbol of S;
A5: 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 element; assume x in rng(f.o);
then consider y 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 Lem15,PBOOLE:def 18;
then product ((NForms R)*the_arity_of o) c=
product((the Sorts of Free(S,X))*the_arity_of o) by Lem14;
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 A5,A3,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 {nf(z, R.the_result_sort_of o)
where z is Element of Free(S,X), the_result_sort_of o:
not contradiction};
then nf(a, R.the_result_sort_of o) in (NForms R).the_result_sort_of o
by NFORM;
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
A1: 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
A2: 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;
A3: dom Den(o,A1) = Args(o,A1) & dom Den(o,A2) = Args(o,A2) by FUNCT_2:def 1;
now
let a be element;
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 A1,A2;
hence Den(o,A1).a = Den(o,A2).a;
end;
hence thesis by A1,A2,A3,FUNCT_1:2;
end;
hence thesis by A1,A2;
end;
end;
theorem Th98:
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 {nf(z,R.a) where z is Element of Free(S,X),a:not contradiction}
by NFORM;
then ex z being Element of Free(S,X),a st x = nf(z,R.a);
hence nf(x,R.a) = x by Lem16a;
end;
Lm7: 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 NFALG;
(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 Lem15,PBOOLE:def 18;
then product ((NForms R)*the_arity_of o) c=
product((the Sorts of Free(S,X))*the_arity_of o) by Lem14;
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 Lem17:
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) by REWRITE1:def 6;
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 Z1: [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,Z1,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 Lem20:
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,FINSEQ_1:14;
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 Lem22:
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 element;
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;
AB: i = len p+1+(1+j) by A9;
len <*x*> = 1 & len <*y*> = 1 by FINSEQ_1:40;
then
AA: 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 AB,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 AB,AA,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,FUNCT_1:2;
end;
theorem Lem23:
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 Z0: i+1 <= len p;
then
A1: len(p|(i+1)) = i+1 by FINSEQ_1:59;
i < len p by Z0,NAT_1:13;
then
A7: len(p|i) = i & len <*p.(i+1)*> = 1 by FINSEQ_1:40,59;
then
A2: len((p|i)^<*p.(i+1)*>) = i+1 by FINSEQ_1:22;
thus len (p|(i+1)) = len ((p|i)^<*p.(i+1)*>) by Z0,A2,FINSEQ_1:59;
let j be Nat;
assume
A3: 1 <= j & j <= len(p|(i+1));
per cases by A3,A1,NAT_1:8;
suppose
A4: j <= i;
A6: j in dom (p|i) by A7,A3,A4,FINSEQ_3:25;
thus (p|(i+1)).j = p.j by A1,A3,FINSEQ_1:1,FUNCT_1:49
.= (p|i).j by A4,A3,FINSEQ_1:1,FUNCT_1:49
.= ((p|i)^<*p.(i+1)*>).j by A6,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 A7,A8,FINSEQ_1:42;
end;
end;
theorem Lem24:
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 Z1: i+1 <= len p;
then
A0: i < len p by NAT_1:13;
then
A1: 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 Z1,RFINSEQ:def 1
.= len p-i;
hence len(p/^i) = len(<*p.(i+1)*>^(p/^(i+1))) by A0,RFINSEQ:def 1;
let j be Nat;
assume
A3: 1 <= j & j <= len(p/^i);
then
A4: j in dom(p/^i) by FINSEQ_3:25;
per cases by A3,XXREAL_0:1;
suppose
A5: j = 1;
hence (p/^i).j = p.(i+1) by A0,A4,RFINSEQ:def 1
.= (<*p.(i+1)*>^(p/^(i+1))).j by A5,FINSEQ_1:41;
end;
suppose
j > 1;
then j >= 1+1 by NAT_1:13;
then consider k being Nat such that
A6: j = 1+1+k by NAT_1:10;
A7: 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 Z1,A6,RFINSEQ:def 1;
then
1 <= 1+k & 1+k <= len(p/^(i+1)) by A1,A3,XREAL_1:6,NAT_1:11;
then
A8: 1+k in dom(p/^(i+1)) by FINSEQ_3:25;
thus (p/^i).j = p.(i+j) by A0,A4,RFINSEQ:def 1 .= p.(i+1+(1+k)) by A6
.= (p/^(i+1)).(1+k) by Z1,A8,RFINSEQ:def 1
.= (<*p.(i+1)*>^(p/^(i+1))).j by A7,A8,A9,FINSEQ_1:def 7;
end;
end;
theorem Lem18:
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
Z1: 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
Z2: 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
Z3: 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
B1: 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 Lem20;
then
B2: ((g#y)|0)^((h#x)/^0) = h#x by FINSEQ_1:34;
B3: Args(o,NFAlgebra R) c= Args(o, Free(S,X)) & h#x in Args(o,NFAlgebra R)
by Lm7;
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 NFALG,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 Z2,FUNCT_2:15,PBOOLE:def 2;
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 Z2,NFALG;
then
A1: P[0] by B2,Lem16a;
A2: now let i be Nat;
assume
A3: P[i];
thus P[i+1]
proof assume
A4: i+1 <= len the_arity_of o;
then
D3: i < len the_arity_of o by NAT_1:13;
F6: len ((h#x)|i) = i & len ((g#y)|i) = i by B1,D3,FINSEQ_1:59;
D1: (g#y)|(i+1) = ((g#y)|i)^<*(g#y).(i+1)*> by B1,A4,Lem23;
D2: (h#x)/^i = <*(h#x).(i+1)*>^((h#x)/^(i+1)) by B1,A4,Lem24;
F1: i+1 in dom the_arity_of o & dom ((the Sorts of NFAlgebra R)
*the_arity_of o) = dom the_arity_of o
by A4,NAT_1:11,FINSEQ_3:25,PRALG_2:3;
F9: 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 F1,PARTFUN1:def 6,MSUALG_3:6;
then
reconsider xi1 = x .(i+1) as Element of
NFAlgebra R,(the_arity_of o)/.(i+1) by F1,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 F1,MSUALG_3:def 6
.= nf(g.((the_arity_of o)/.(i+1)).xi1,R.((the_arity_of o)/.(i+1)))
by Z1;
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
F3: R.((the_arity_of o)/.(i+1)) reduces g.((the_arity_of o)/.(i+1)).xi1,
hx.(i+1) by REWRITE1:def 6;
D5: dom(h#x) = dom the_arity_of o by MSUALG_3:6;
then
D4: 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);
F2: Q[hx.(i+1)] by A3,A4,NAT_1:13,D2,FINSEQ_1:32;
F4: 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 Z4: [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
H6: len(((g#y)|i)^<*d*>) = i+len<*d*> by F6,FINSEQ_1:22
.= i+1 by FINSEQ_1:40;
thus
H1: 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 A4,D4,H6,RFINSEQ:def 1
.= len the_arity_of o by D5,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 H1,FINSEQ_3:29;
let a be element;
assume
H2: a in dom the_arity_of o;
then reconsider b = a as Nat;
H3: b <= len the_arity_of o & b >= 1 by H2,FINSEQ_3:25;
per cases by NAT_1:8;
suppose
H5: b <= i;
then
H4: b in dom((g#y)|i) & dom((g#y)|i) c= dom(((g#y)|i)^<*d*>) &
b in Seg i by H3,F6,FINSEQ_3:25,FINSEQ_1: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 H4,FINSEQ_1:def 7
.= (g#y).a by H5,H3,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 H1,H2,MSUALG_3:6;
end;
suppose
H7: b = i+1;
then b in dom(((g#y)|i)^<*d*>) by H3,H6,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 F6,H7,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 F9,H2,H7,FUNCT_1:13;
end;
suppose
H8: b > i+1;
then consider k being Nat such that
H9: b = i+1+k by NAT_1:10;
i+1+k > i+1+0 by H8,H9;
then k > 0 & b-(i+1) <= (len the_arity_of o)-(i+1)
by H3,XREAL_1:9,6;
then k >= 0+1 & k <= len((h#x)/^(i+1))
by A4,D4,RFINSEQ:def 1,H9,NAT_1:13;
then
D8: 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 H6,H9,FINSEQ_1:def 7 .= (h#x).a by H9,D4,D8,A4,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 H1,H2,B3,MSUALG_3:6;
end;
end;
then
J2: ((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
F5: [f.c,f.d] in R.s by Z2,F1,Z4,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 J2,PRALG_2:3;
reconsider Dd = Den(o,Free(S,X)).ad as Element of Free(S,X),s
by Z2,FUNCT_2:15;
F7: 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 F6,Lem22;
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 F6,Lem22;
then
FF: (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 F5,F7,REWRITE1:29;
assume Q[b];
hence Q[a] by FF,REWRITE1:55;
end;
F5: Q[g.((the_arity_of o)/.(i+1)).xi1] from B(F2,F3,F4);
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 D1,Z3,F1,F5,MSUALG_3:def 6;
end;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A2);
then
AA: 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 B1,FINSEQ_1:58,Lem20;
hence thesis by AA,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 NFALG;
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 NFALG;
thus FreeGen X is ManySortedSubset of the Sorts of A
proof
let i be element;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
let x be element; assume
B1: 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 B1;
x is_a_normal_form_wrt R.s & R.s reduces x,x by B1,NFV,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:def 6,54;
then x = nf(x,R.s) &
(NForms R).s = {nf(y,R.s) where y is Element of Free(S,X),s:
not contradiction}
by NFORM,REWRITE1:53;
hence thesis by A1;
end;
hereby
let o be OperSymbol of S, p be FinSequence;
assume
B1: p in Args(o, Free(S,X)) &
Den(o,Free(S,X)).p in (the Sorts of A).the_result_sort_of o;
then
B2: 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 {nf(z,R.the_result_sort_of o) where z is Element of
(the Sorts of Free(S,X)).the_result_sort_of o: not contradiction}
by A1,B1,NFORM;
then consider z being Element of (the Sorts of Free(S,X))
.the_result_sort_of o such that
BB: Den(o,Free(S,X)).p = nf(z,R.the_result_sort_of o);
BD: Den(o,Free(S,X)).p is_a_normal_form_of z, R.the_result_sort_of o
by BB,REWRITE1:54;
BA: now
let i be element; assume
B4: i in dom p;
then
B3: (the Sorts of Free(S,X)).((the_arity_of o).i) =
((the Sorts of Free(S,X))*the_arity_of o).i by B2,FUNCT_1:13;
reconsider j = i as Element of NAT by B4;
reconsider ai = (the_arity_of o).i as SortSymbol of S
by B2,B4,FUNCT_1:102;
B6: ai = (the_arity_of o)/.j by B4,B2,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 B1,B3,B4,B2,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 B2,B4,FUNCT_1:13;
then pj nin {nf(b,R.((the_arity_of o)/.i)) where b is Element of
(the Sorts of Free(S,X)).((the_arity_of o)/.i): not contradiction}
by B6,NFORM;
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 B6,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 by REWRITE1:def 6;
then consider x such that
B5: [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 B5,ZFMISC_1:87;
set f = transl(o,j,q,Free(S,X));
B7: f.pj = Den(o,Free(S,X)).(q+*(j,pj)) by B6,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 B5,B1,B4,B2,B6,MSUALG_6:def 5,def 8;
hence contradiction by BD,B7,REWRITE1:def 5,def 6;
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 B2,BA,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 NFALG
.= Den(o,Free(S,X)).p by BD,Lem16,REWRITE1:def 6;
end;
let f be ManySortedFunction of FreeGen X, the Sorts of A;
let G be ManySortedSubset of the Sorts of A; assume
AA: 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 NFALG,Th96;
then
A2: 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 A2,Th96,EQUATION:4;
then consider g being ManySortedFunction of Free(S,X),Free(S,X) such that
A6: g is_homomorphism Free(S,X),Free(S,X) & g||H = f by MSAFREE:def 5;
deffunc F(SortSymbol of S, Element of A,$1) = nf(g.$1.$2, R.$1);
defpred P[element,element,element] means $3 = nf(g.$1.$2, R.$1);
A5: for s,x being element st s in the carrier of S & x in (the Sorts of A).s
ex y st y in (the Sorts of A).s & P[s,x,y]
proof
let s,x be element;
assume Z3: s in the carrier of S;
assume Z4: x in (the Sorts of A).s;
reconsider t = s as SortSymbol of S by Z3;
reconsider z = x as Element of A,t by Z4;
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,Z4,FUNCT_2:5;
y = nf(a, R.t);
then y in {nf(u,R.t) where u is Element of Free(S,X),t:
not contradiction};
hence y in (the Sorts of A).s by A1,NFORM;
thus P[s,x,y];
end;
consider h being ManySortedFunction of A,A such that
A3: for s,x being element 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(A5);
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 Lem15,PBOOLE:def 18;
then product ((NForms R)*the_arity_of o) c=
product((the Sorts of Free(S,X))*the_arity_of o) by Lem14;
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));
D1: for s being SortSymbol of S, x being Element of NFAlgebra R,s holds
h.s.x = nf(g.s.x,R.s) by A3;
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 A3
.= 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 NFALG
.= nf(g.(the_result_sort_of o).(Dy),
R.(the_result_sort_of o)) by A6,Lem17
.= nf(Den(o,Free(S,X)).(g#y), R.(the_result_sort_of o))
by A6,MSUALG_3:def 7
.= nf(Den(o,A).(h#x), R.(the_result_sort_of o)) by A6,D1,Lem18
.= nf(nf(Den(o,Free(S,X)).(h#x), R.(the_result_sort_of o)),
R.the_result_sort_of o) by NFALG
.= nf(Den(o,Free(S,X)).(h#x), R.(the_result_sort_of o)) by Lem16a
.= Den(o,A).(h#x) by NFALG;
end;
let a be Element of S;
J2: 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 AA;
let x;
assume
J3: x in dom(f.a);
J5: 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 J3,FUNCT_2:5;
the Sorts of A = NForms R by NFALG;
hence f.a.x = nf(fax,R.a) by Th98
.= nf(((g.a)|(H.a)).x,R.a) by A6,MSAFREE:def 1
.= nf(g.a.x,R.a) by J3,FUNCT_1:49
.= h.a.x by J5,AA,J2,J3,A3
.= ((h.a)|(G.a)).x by AA,J3,FUNCT_1:49
.= (h||G).a.x by MSAFREE:def 1;
end;
end;