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:
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 Th12;
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:79
.= (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: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

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 A11, TREES_1:80, TREES_4:5;
then p = {} by TREES_4:17;
then len p = 0 ;
then len (the_arity_of o) = 0 by MSATERM:22;
then ( the_arity_of o = {} & g is Term of S,V ) by Th4;
hence contradiction by A1, A8, A11; :: thesis:

end;

then consider h being Nat such that
A15: 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 13;

now

let x be set ; :: thesis:
assume A16: 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 A2, Th4;
A17: ( Following q,(height (dom t)) is_stable_at t & (Following q,(height (dom t))) . t = t @ f,A ) by A7, A12, A16;
consider z being set such that
A18: ( z in dom p & t = p . z ) by A12, A16, FUNCT_1:def 5;
( z in dom (doms p) & (doms p) . z = dom t ) by A18, 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 height (dom t) <= h by A14, A15, NAT_1:13;
then consider i being Nat such that
A19: h = (height (dom t)) + i by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
Following q,h = Following (Following q,(height (dom t))),i by A19, FACIRC_1:13;
hence Following q,h is_stable_at x by A17, FACIRC_1:17; :: thesis:

end;

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

now

let i be Nat; :: thesis:
assume A26: 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 A26, MSATERM:23; :: thesis:

end;

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

now

let i be Nat; :: thesis:
assume A27: i in dom p ; :: thesis:
let t be c-Term of A,V; :: thesis:
assume A28: t = p . i ; :: thesis:
then A29: t in rng p by A27, 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 A2, Th4;
A30: ( Following q,(height (dom t)) is_stable_at tt & (Following q,(height (dom t))) . tt = tt @ f,A ) by A7, A29;
A31: vp . i = (Following q,h) . t by A23, A24, A27, A28;
( i in dom (doms p) & (doms p) . i = dom t ) by A27, A28, 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 height (dom t) <= h by A14, A15, NAT_1:13;
then consider j being Nat such that
A32: h = (height (dom t)) + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
Following q,h = Following (Following q,(height (dom t))),j by A32, FACIRC_1:13;
then (Following q,h) . t = (Following q,(height (dom t))) . t by A30, FACIRC_1:def 9;
hence vp . i = t @ f by A30, A31, Def7; :: thesis:

end;

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

now

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

end;

then A35: vp = (Following q,h) * (the_arity_of g) by A12, A24, FUNCT_1:9;
Den g,(X -Circuit A) = Den o,A by A11, Th17;
then (Den o,A) . vp = (Following (Following q,h)) . t by A10, A21, A35, 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 A15, A20, A33, FACIRC_1:12
.= ([o,the carrier of S] -tree p) @ f,A by A20, Def7 ;
:: thesis:

end;

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