let S be non empty non void ManySortedSign ; :: thesis:
let A be non-empty finite-yielding MSAlgebra over S; :: thesis:
let V be Variables of A; :: thesis:
let X be SetWithCompoundTerm of S,V; :: thesis:
assume A1: for t being Term of S,V
for o being OperSymbol of S holds
( not t in Subtrees X or not t . {} = [o, the carrier of S] or not the_arity_of o = {} ) ; :: thesis:
let q be State of (X -Circuit A); :: thesis:
let f be CompatibleValuation of q; :: thesis:
A2: X -CircuitStr = ManySortedSign(# (Subtrees X),([: the carrier' of S,{ the carrier of S}:] -Subtrees X),([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees X),(incl ([: the carrier' of S,{ the carrier of S}:] -Subtrees X)) #) ;
defpred S₁[ finite DecoratedTree] means ( $1 in Subtrees X implies ( Following (q,(height (dom $1))) is_stable_at $1 & (Following (q,(height (dom $1)))) . $1 = $1 @ (f,A) ) );
A3: for s being SortSymbol of S
for v being Element of V . s holds S₁[ root-tree [v,s]]

proof

let s be SortSymbol of S; :: thesis:
let v be Element of V . s; :: thesis:
assume A4: root-tree [v,s] in Subtrees X ; :: thesis:
then root-tree [v,s] in InputVertices (X -CircuitStr) by Th11;
hence Following (q,(height (dom (root-tree [v,s])))) is_stable_at root-tree [v,s] by FACIRC_1:18; :: thesis:
reconsider t = root-tree [v,s] as c-Term of A,V by MSATERM:8;
A5: t is Term of S,V by MSATERM:4;
dom (root-tree [v,s]) = elementary_tree 0 by TREES_4:3;
hence (Following (q,(height (dom (root-tree [v,s]))))) . (root-tree [v,s]) = q . (root-tree [v,s]) by FACIRC_1:11, TREES_1:42
.= (f . s) . v by A4, Def8
.= (v -term A) @ f by MSATERM:42
.= t @ f by MSATERM:def 4
.= (root-tree [v,s]) @ (f,A) by A5, Def7 ;
:: thesis:

end;

A6: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,V) st ( for t being Term of S,V st t in rng p holds
S₁[t] ) holds
S₁[[o, the carrier of S] -tree p]

proof

let o be OperSymbol of S; :: thesis:
let p be ArgumentSeq of Sym (o,V); :: thesis:
assume that
A7: for t being Term of S,V st t in rng p & t in Subtrees X holds
( Following (q,(height (dom t))) is_stable_at t & (Following (q,(height (dom t)))) . t = t @ (f,A) ) and
A8: [o, the carrier of S] -tree p in Subtrees X ; :: thesis:
consider tt being Element of X, n being Node of tt such that
A9: [o, the carrier of S] -tree p = tt | n by A8, TREES_9:19;
A10: <*> NAT in (dom tt) | n by TREES_1:22;
n ^ {} = n by FINSEQ_1:34;
then tt . n = (tt | n) . {} by A10, TREES_2:def 10
.= [o, the carrier of S] by A9, TREES_4:def 4 ;
then tt . n in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:106;
then reconsider g = [o, the carrier of S] -tree p as Gate of (X -CircuitStr) by A9, TREES_9:24;
A11: the_result_sort_of g = g ;
A12: g . {} = [o, the carrier of S] by TREES_4:def 4;
g = (g . {}) -tree (the_arity_of g) by Th12;
then A13: the_arity_of g = p by TREES_4:15;
A14: rng (the_arity_of g) c= Subtrees X by FINSEQ_1:def 4;
A15: dom ([o, the carrier of S] -tree p) = tree (doms p) by TREES_4:10;

now :: thesis:

assume height (dom ([o, the carrier of S] -tree p)) = 0 ; :: thesis:
then [o, the carrier of S] -tree p = root-tree [o, the carrier of S] by A12, TREES_1:43, TREES_4:5;
then p = {} by TREES_4:17;
then len p = 0 ;
then len (the_arity_of o) = 0 by MSATERM:22;
then A16: the_arity_of o = {} ;
g is Term of S,V by Th4;
hence contradiction by A1, A8, A12, A16; :: thesis:

end;

then consider h being Nat such that
A17: height (dom ([o, the carrier of S] -tree p)) = h + 1 by NAT_1:6;
reconsider h = h as Element of NAT by ORDINAL1:def 12;

now :: thesis:

let x be set ; :: thesis:
assume A18: x in rng (the_arity_of g) ; :: thesis:
then reconsider t = x as Element of Subtrees X by A14;
reconsider t = t as Term of S,V by A2, Th4;
consider z being object such that
A19: z in dom p and
A20: t = p . z by A13, A18, FUNCT_1:def 3;
A21: z in dom (doms p) by A19, A20, FUNCT_6:22;
(doms p) . z = dom t by A19, A20, FUNCT_6:22;
then dom t in rng (doms p) by A21, FUNCT_1:def 3;
then height (dom t) < height (tree (doms p)) by TREES_3:78;
then height (dom t) <= h by A15, A17, NAT_1:13;
then consider i being Nat such that
A22: h = (height (dom t)) + i by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
Following (q,h) = Following ((Following (q,(height (dom t)))),i) by A22, FACIRC_1:13;
hence Following (q,h) is_stable_at x by A7, A13, A18, FACIRC_1:17; :: thesis:

end;

then Following (Following (q,h)) is_stable_at [o, the carrier of S] -tree p by A11, FACIRC_1:19;
hence Following (q,(height (dom ([o, the carrier of S] -tree p)))) is_stable_at [o, the carrier of S] -tree p by A17, FACIRC_1:12; :: thesis:
reconsider t = (Sym (o,V)) -tree p as c-Term of A,V by MSATERM:27;
A23: Sym (o,( the Sorts of A (\/) V)) = [o, the carrier of S] by MSAFREE:def 9;
A24: Sym (o,V) = [o, the carrier of S] by MSAFREE:def 9;
A25: t = [o, the carrier of S] -tree p by MSAFREE:def 9;
deffunc H₁( set ) -> set = (Following (q,h)) . (p . $1);
consider vp being FinSequence such that
A26: len vp = len p and
A27: for i being Nat st i in dom vp holds
vp . i = H₁(i) from FINSEQ_1:sch 2();
A28: dom vp = Seg (len p) by A26, FINSEQ_1:def 3;
A29: dom p = Seg (len p) by FINSEQ_1:def 3;
A30: dom p = dom (the_arity_of o) by MSATERM:22;

now :: thesis:

let i be Nat; :: thesis:
assume A31: i in dom p ; :: thesis:
then reconsider t = p . i as Term of S,V by MSATERM:22;
reconsider t9 = t as c-Term of A,V by MSATERM:27;
take t9 = t9; :: thesis:
the_sort_of t = the_sort_of t9 by Th1;
hence ( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i ) by A31, MSATERM:23; :: thesis:

end;

then reconsider p9 = p as ArgumentSeq of o,A,V by A30, MSATERM:24;

now :: thesis:

let i be Nat; :: thesis:
assume A32: i in dom p ; :: thesis:
let t be c-Term of A,V; :: thesis:
assume A33: t = p . i ; :: thesis:
then A34: t in rng p by A32, FUNCT_1:def 3;
then reconsider tt = t as Element of Subtrees X by A13, A14;
reconsider tt = tt as Term of S,V by A2, Th4;
A35: Following (q,(height (dom t))) is_stable_at tt by A7, A34;
A36: (Following (q,(height (dom t)))) . tt = tt @ (f,A) by A7, A34;
A37: vp . i = (Following (q,h)) . t by A27, A28, A29, A32, A33;
A38: i in dom (doms p) by A32, A33, FUNCT_6:22;
(doms p) . i = dom t by A32, A33, FUNCT_6:22;
then dom t in rng (doms p) by A38, FUNCT_1:def 3;
then height (dom t) < height (tree (doms p)) by TREES_3:78;
then height (dom t) <= h by A15, A17, NAT_1:13;
then consider j being Nat such that
A39: h = (height (dom t)) + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
Following (q,h) = Following ((Following (q,(height (dom t)))),j) by A39, FACIRC_1:13;
then (Following (q,h)) . t = (Following (q,(height (dom t)))) . t by A35;
hence vp . i = t @ f by A36, A37, Def7; :: thesis:

end;

then A40: ((Sym (o,( the Sorts of A (\/) V))) -tree p9) @ f = (Den (o,A)) . vp by A26, MSATERM:43;

now :: thesis:

A41: rng p c= the carrier of (X -CircuitStr) by A13, FINSEQ_1:def 4;
dom (Following (q,h)) = the carrier of (X -CircuitStr) by CIRCUIT1:3;
hence dom ((Following (q,h)) * p) = dom p by A41, RELAT_1:27; :: thesis:
let z be object ; :: thesis:
assume A42: z in Seg (len p) ; :: thesis:
then reconsider i = z as Element of NAT ;
vp . i = (Following (q,h)) . (p . i) by A27, A28, A42;
hence vp . z = ((Following (q,h)) * p) . z by A29, A42, FUNCT_1:13; :: thesis:

end;

then A43: vp = (Following (q,h)) * (the_arity_of g) by A13, A28, A29, FUNCT_1:2;
Den (g,(X -Circuit A)) = Den (o,A) by A12, Th16;
then (Den (o,A)) . vp = (Following (Following (q,h))) . t by A11, A25, A43, FACIRC_1:10;
hence (Following (q,(height (dom ([o, the carrier of S] -tree p))))) . ([o, the carrier of S] -tree p) = t @ f by A17, A23, A24, A40, FACIRC_1:12
.= ([o, the carrier of S] -tree p) @ (f,A) by A24, Def7 ;
:: thesis:

end;

thus for t being Term of S,V holds S₁[t] from MSATERM:sch 1(A3, A6); :: thesis: