let S be non empty non void ManySortedSign ; :: thesis: 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) ) )
let A be non-empty finite-yielding MSAlgebra over S; :: thesis: 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) ) )
let V be Variables of A; :: thesis: 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) ) )
let X be SetWithCompoundTerm of S,V; :: thesis: 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) ) )
let G be non empty non void Circuit-like ManySortedSign ; :: thesis: 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) ) )
let C be non-empty Circuit of G; :: thesis: ( X,A specifies C implies 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) ) ) )
assume X,A specifies C ; :: thesis: 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) ) )
then C calculates X,A by Th58;
hence 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) ) ) by Th59; :: thesis: verum