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 G st C calculates X,A holds
for f being SortMap of X,A,C
for t being Term of S,V st t in Subtrees X holds
for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of (X -Circuit A) 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 G st C calculates X,A holds
for f being SortMap of X,A,C
for t being Term of S,V st t in Subtrees X holds
for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of (X -Circuit A) 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 G st C calculates X,A holds
for f being SortMap of X,A,C
for t being Term of S,V st t in Subtrees X holds
for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of (X -Circuit A) 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 G st C calculates X,A holds
for f being SortMap of X,A,C
for t being Term of S,V st t in Subtrees X holds
for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of (X -Circuit A) 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 G st C calculates X,A holds
for f being SortMap of X,A,C
for t being Term of S,V st t in Subtrees X holds
for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of (X -Circuit A) 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 G; :: thesis: ( C calculates X,A implies for f being SortMap of X,A,C
for t being Term of S,V st t in Subtrees X holds
for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of (X -Circuit A) st s' = s * f holds
for h being CompatibleValuation of s' holds (Following s,(1 + (height (dom t)))) . (f . t) = t @ h,A ) ) )
assume A1: C calculates X,A ; :: thesis: for f being SortMap of X,A,C
for t being Term of S,V st t in Subtrees X holds
for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of (X -Circuit A) st s' = s * f holds
for h being CompatibleValuation of s' holds (Following s,(1 + (height (dom t)))) . (f . t) = t @ h,A ) )
let f be SortMap of X,A,C; :: thesis: for t being Term of S,V st t in Subtrees X holds
for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of (X -Circuit A) st s' = s * f holds
for h being CompatibleValuation of s' holds (Following s,(1 + (height (dom t)))) . (f . t) = t @ h,A ) )
consider g being Function such that
A2: f,g form_embedding_of X -Circuit A,C by A1, Def17;
A3: f preserves_inputs_of X -CircuitStr ,G by A1, Def17;
A4: f,g form_morphism_between X -CircuitStr ,G by A2, Def12;
let t be Term of S,V; :: thesis: ( t in Subtrees X implies for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of (X -Circuit A) st s' = s * f holds
for h being CompatibleValuation of s' holds (Following s,(1 + (height (dom t)))) . (f . t) = t @ h,A ) ) )
assume A5: t in Subtrees X ; :: thesis: for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of (X -Circuit A) st s' = s * f holds
for h being CompatibleValuation of s' holds (Following s,(1 + (height (dom t)))) . (f . t) = t @ h,A ) )
let s be State of C; :: thesis: ( Following s,(1 + (height (dom t))) is_stable_at f . t & ( for s' being State of (X -Circuit A) st s' = s * f holds
for h being CompatibleValuation of s' holds (Following s,(1 + (height (dom t)))) . (f . t) = t @ h,A ) )
reconsider s' = s * f as State of (X -Circuit A) by A2, Th45;
reconsider t' = t as Vertex of (X -CircuitStr ) by A5;
A6: ( Following s',(1 + (height (dom t))) is_stable_at t' & Following s',(1 + (height (dom t))) = (Following s,(1 + (height (dom t)))) * f ) by A2, A3, Th22, Th48;
hence Following s,(1 + (height (dom t))) is_stable_at f . t by A2, A3, Th50; :: thesis: for s' being State of (X -Circuit A) st s' = s * f holds
for h being CompatibleValuation of s' holds (Following s,(1 + (height (dom t)))) . (f . t) = t @ h,A
let s' be State of (X -Circuit A); :: thesis: ( s' = s * f implies for h being CompatibleValuation of s' holds (Following s,(1 + (height (dom t)))) . (f . t) = t @ h,A )
assume A7: s' = s * f ; :: thesis: for h being CompatibleValuation of s' holds (Following s,(1 + (height (dom t)))) . (f . t) = t @ h,A
let h be CompatibleValuation of s'; :: thesis: (Following s,(1 + (height (dom t)))) . (f . t) = t @ h,A
( dom f = the carrier of (X -CircuitStr ) & (Following s',(1 + (height (dom t)))) . t' = t @ h,A ) by A4, Th22, PUA2MSS1:def 13;
hence (Following s,(1 + (height (dom t)))) . (f . t) = t @ h,A by A6, A7, FUNCT_1:23; :: thesis: verum