let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty finite-yielding MSAlgebra of 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 non-empty st X,A specifies C holds
for f being SortMap of X,A,C
for s being State of
for t being Term of the carrier of K345(S,b₂), st t in Subtrees X holds
( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of st s' = s * f holds
for h being CompatibleValuation of s' holds (Following s,(1 + (height (dom t)))) . (f . t) = t @ h,A ) )
let A be non-empty finite-yielding MSAlgebra of 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 non-empty st X,A specifies C holds
for f being SortMap of X,A,C
for s being State of
for t being Term of the carrier of K345(S,b₁), st t in Subtrees X holds
( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of st s' = s * f holds
for h being CompatibleValuation of s' 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 non-empty st X,A specifies C holds
for f being SortMap of X,A,C
for s being State of
for t being Term of the carrier of K345(S,V), st t in Subtrees X holds
( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of st s' = s * f holds
for h being CompatibleValuation of s' 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 non-empty st X,A specifies C holds
for f being SortMap of X,A,C
for s being State of
for t being Term of the carrier of K345(S,V), st t in Subtrees X holds
( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of st s' = s * f holds
for h being CompatibleValuation of s' 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 non-empty st X,A specifies C holds
for f being SortMap of X,A,C
for s being State of
for t being Term of the carrier of K345(S,V), st t in Subtrees X holds
( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of st s' = s * f holds
for h being CompatibleValuation of s' holds (Following s,(1 + (height (dom t)))) . (f . t) = t @ h,A ) )
let C be non-empty Circuit of non-empty ; :: thesis: ( X,A specifies C implies for f being SortMap of X,A,C
for s being State of
for t being Term of the carrier of K345(S,V), st t in Subtrees X holds
( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of st s' = s * f holds
for h being CompatibleValuation of s' 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
for t being Term of the carrier of K345(S,V), st t in Subtrees X holds
( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of st s' = s * f holds
for h being CompatibleValuation of s' holds (Following s,(1 + (height (dom t)))) . (f . t) = t @ h,A ) )
then C calculates X,A by Th59;
hence for f being SortMap of X,A,C
for s being State of
for t being Term of the carrier of K345(S,V), st t in Subtrees X holds
( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of st s' = s * f holds
for h being CompatibleValuation of s' holds (Following s,(1 + (height (dom t)))) . (f . t) = t @ h,A ) ) by Th60; :: thesis: verum