theorem :: CIRCTRM1:61

for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st X,A specifies C holds
for f being SortMap of X,A,C
for s being State of C
for t being Term of S,V st t in Subtrees X holds
( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) )