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 s being State of (X -Circuit A)
for f being CompatibleValuation of s
for n being Element of NAT holds f is CompatibleValuation of Following s,n
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 s being State of (X -Circuit A)
for f being CompatibleValuation of s
for n being Element of NAT holds f is CompatibleValuation of Following s,n
let V be Variables of A; :: thesis: for X being SetWithCompoundTerm of S,V
for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for n being Element of NAT holds f is CompatibleValuation of Following s,n
let X be SetWithCompoundTerm of S,V; :: thesis: for s being State of (X -Circuit A)
for f being CompatibleValuation of s
for n being Element of NAT holds f is CompatibleValuation of Following s,n
let s be State of (X -Circuit A); :: thesis: for f being CompatibleValuation of s
for n being Element of NAT holds f is CompatibleValuation of Following s,n
let f be CompatibleValuation of s; :: thesis: for n being Element of NAT holds f is CompatibleValuation of Following s,n
let n be Element of NAT ; :: thesis: f is CompatibleValuation of Following s,n
let x be Vertex of S; :: according to CIRCTRM1:def 8 :: thesis: for v being Element of V . x st root-tree [v,x] in Subtrees X holds
(f . x) . v = (Following s,n) . (root-tree [v,x])
let v be Element of V . x; :: thesis: ( root-tree [v,x] in Subtrees X implies (f . x) . v = (Following s,n) . (root-tree [v,x]) )
assume A1: root-tree [v,x] in Subtrees X ; :: thesis: (f . x) . v = (Following s,n) . (root-tree [v,x])
then root-tree [v,x] in InputVertices (X -CircuitStr ) by Th12;
then s is_stable_at root-tree [v,x] by FACIRC_1:18;
then (Following s,n) . (root-tree [v,x]) = s . (root-tree [v,x]) by FACIRC_1:def 9;
hence (f . x) . v = (Following s,n) . (root-tree [v,x]) by A1, Def8; :: thesis: verum