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 t being Term of S,V st t in Subtrees X holds
ex v being Vertex of G st
for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at v & ex f being SortMap of X,A,C st
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)))) . v = 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 t being Term of S,V st t in Subtrees X holds
ex v being Vertex of G st
for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at v & ex f being SortMap of X,A,C st
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)))) . v = 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 t being Term of S,V st t in Subtrees X holds
ex v being Vertex of G st
for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at v & ex f being SortMap of X,A,C st
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)))) . v = 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 t being Term of S,V st t in Subtrees X holds
ex v being Vertex of G st
for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at v & ex f being SortMap of X,A,C st
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)))) . v = 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 t being Term of S,V st t in Subtrees X holds
ex v being Vertex of G st
for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at v & ex f being SortMap of X,A,C st
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)))) . v = t @ h,A )
let C be non-empty Circuit of G; :: thesis: ( C calculates X,A implies for t being Term of S,V st t in Subtrees X holds
ex v being Vertex of G st
for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at v & ex f being SortMap of X,A,C st
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)))) . v = t @ h,A ) )
assume A1: C calculates X,A ; :: thesis: for t being Term of S,V st t in Subtrees X holds
ex v being Vertex of G st
for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at v & ex f being SortMap of X,A,C st
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)))) . v = t @ h,A )
then consider f, g being Function such that
A2: f,g form_embedding_of X -Circuit A,C and
A3: f preserves_inputs_of X -CircuitStr ,G by Def15;
f is one-to-one by A2, Def12;
then reconsider f = f as SortMap of X,A,C by A1, A2, A3, Def17;
let t be Term of S,V; :: thesis: ( t in Subtrees X implies ex v being Vertex of G st
for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at v & ex f being SortMap of X,A,C st
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)))) . v = t @ h,A ) )
assume A4: t in Subtrees X ; :: thesis: ex v being Vertex of G st
for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at v & ex f being SortMap of X,A,C st
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)))) . v = t @ h,A )
A5: f,g form_morphism_between X -CircuitStr ,G by A2, Def12;
reconsider t9 = t as Vertex of (X -CircuitStr ) by A4;
reconsider v = f . t9 as Vertex of G by A5, Th31;
take v ; :: thesis: for s being State of C holds
( Following s,(1 + (height (dom t))) is_stable_at v & ex f being SortMap of X,A,C st
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)))) . v = t @ h,A )
let s be State of C; :: thesis: ( Following s,(1 + (height (dom t))) is_stable_at v & ex f being SortMap of X,A,C st
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)))) . v = t @ h,A )
thus Following s,(1 + (height (dom t))) is_stable_at v by A1, Th60; :: thesis: ex f being SortMap of X,A,C st
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)))) . v = t @ h,A
take f ; :: thesis: 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)))) . v = t @ h,A
thus 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)))) . v = t @ h,A by A1, Th60; :: thesis: verum