let S be non empty non void ManySortedSign ; :: thesis:
let A be non-empty finite-yielding MSAlgebra of S; :: thesis:
let V be Variables of A; :: thesis:
let X be SetWithCompoundTerm of S,V; :: thesis:
let q be State of (X -Circuit A); :: thesis:
let f be CompatibleValuation of q; :: thesis:
A1: 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,(1 + (height (dom $1))) is_stable_at $1 & (Following q,(1 + (height (dom $1)))) . $1 = $1 @ f,A ) );
A2: 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 A3: root-tree [v,s] in Subtrees X ; :: thesis:
then A4: root-tree [v,s] in InputVertices (X -CircuitStr ) by Th12;
hence Following q,(1 + (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;
q is_stable_at root-tree [v,s] by A4, FACIRC_1:18;
hence (Following q,(1 + (height (dom (root-tree [v,s]))))) . (root-tree [v,s]) = q . (root-tree [v,s]) by FACIRC_1:def 9
.= (f . s) . v by A3, 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,(1 + (height (dom t))) is_stable_at t & (Following q,(1 + (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:20;
( <*> NAT in (dom tt) | n & n ^ {} = n ) by FINSEQ_1:47, TREES_1:47;
then tt . n = (tt | n) . {} by TREES_2:def 11
.= [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:129;
then reconsider g = [o,the carrier of S] -tree p as Gate of (X -CircuitStr ) by A9, TREES_9:25;
A10: the_result_sort_of g = g by FUNCT_1:34;
A11: g . {} = [o,the carrier of S] by TREES_4:def 4;
g = (g . {} ) -tree (the_arity_of g) by Th13;
then A12: the_arity_of g = p by TREES_4:15;
A13: rng (the_arity_of g) c= Subtrees X by FINSEQ_1:def 4;
A14: dom ([o,the carrier of S] -tree p) = tree (doms p) by TREES_4:10;

now

let x be set ; :: thesis:
assume A15: x in rng (the_arity_of g) ; :: thesis:
then reconsider t = x as Element of Subtrees X by A13;
reconsider t = t as Term of S,V by A1, Th4;
A16: ( Following q,(1 + (height (dom t))) is_stable_at t & (Following q,(1 + (height (dom t)))) . t = t @ f,A ) by A7, A12, A15;
consider z being set such that
A17: ( z in dom p & t = p . z ) by A12, A15, FUNCT_1:def 5;
( z in dom (doms p) & (doms p) . z = dom t ) by A17, FUNCT_6:31;
then dom t in rng (doms p) by FUNCT_1:def 5;
then height (dom t) < height (tree (doms p)) by TREES_3:81;
then 1 + (height (dom t)) <= height (tree (doms p)) by NAT_1:13;
then consider i being Nat such that
A18: height (tree (doms p)) = (1 + (height (dom t))) + i by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
Following q,(height (dom ([o,the carrier of S] -tree p))) = Following (Following q,(1 + (height (dom t)))),i by A14, A18, FACIRC_1:13;
hence Following q,(height (dom ([o,the carrier of S] -tree p))) is_stable_at x by A16, FACIRC_1:17; :: thesis:

end;

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

now

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

end;

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

now

let i be Nat; :: thesis:
assume A26: i in dom p ; :: thesis:
let t be c-Term of A,V; :: thesis:
assume A27: t = p . i ; :: thesis:
then A28: t in rng p by A26, FUNCT_1:def 5;
then reconsider tt = t as Element of Subtrees X by A12, A13;
reconsider tt = tt as Term of S,V by A1, Th4;
A29: ( Following q,(1 + (height (dom t))) is_stable_at tt & (Following q,(1 + (height (dom t)))) . tt = tt @ f,A ) by A7, A28;
A30: vp . i = (Following q,(height (dom ([o,the carrier of S] -tree p)))) . t by A20, A22, A23, A26, A27;
( i in dom (doms p) & (doms p) . i = dom t ) by A26, A27, FUNCT_6:31;
then dom t in rng (doms p) by FUNCT_1:def 5;
then height (dom t) < height (tree (doms p)) by TREES_3:81;
then 1 + (height (dom t)) <= height (tree (doms p)) by NAT_1:13;
then consider j being Nat such that
A31: height (tree (doms p)) = (1 + (height (dom t))) + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
Following q,(height (dom ([o,the carrier of S] -tree p))) = Following (Following q,(1 + (height (dom t)))),j by A14, A31, FACIRC_1:13;
then (Following q,(height (dom ([o,the carrier of S] -tree p)))) . t = (Following q,(1 + (height (dom t)))) . t by A29, FACIRC_1:def 9;
hence vp . i = t @ f by A29, A30, Def7; :: thesis:

end;

then A32: ((Sym o,(the Sorts of A \/ V)) -tree p') @ f = (Den o,A) . vp by A21, MSATERM:43;

now

( rng p c= the carrier of (X -CircuitStr ) & dom (Following q,(height (dom t))) = the carrier of (X -CircuitStr ) ) by A12, CIRCUIT1:4, FINSEQ_1:def 4;
hence dom ((Following q,(height (dom t))) * p) = dom p by RELAT_1:46; :: thesis:
let z be set ; :: thesis:
assume A33: z in Seg (len p) ; :: thesis:
then reconsider i = z as Element of NAT ;
vp . i = (Following q,(height (dom t))) . (p . i) by A22, A33, A23;
hence vp . z = ((Following q,(height (dom t))) * p) . z by A23, A33, FUNCT_1:23; :: thesis:

end;

then A34: vp = (Following q,(height (dom t))) * (the_arity_of g) by A12, A23, FUNCT_1:9;
Den g,(X -Circuit A) = Den o,A by A11, Th17;
then (Den o,A) . vp = (Following (Following q,(height (dom t)))) . t by A10, A20, A34, FACIRC_1:10;
hence (Following q,(1 + (height (dom ([o,the carrier of S] -tree p))))) . ([o,the carrier of S] -tree p) = t @ f by A19, A32, FACIRC_1:12
.= ([o,the carrier of S] -tree p) @ f,A by A19, Def7 ;
:: thesis:

end;

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