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 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 over 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 Th11;
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]) ;
hence (f . x) . v = (Following (s,n)) . (root-tree [v,x]) by A1, Def8; :: thesis: verum