let S1, S2, S be non empty non void Circuit-like ManySortedSign ; :: thesis: ( S = S1 +* S2 & S1 tolerates S2 implies for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for g being Gate of S
for g1 being Gate of S1 st g = g1 holds
g depends_on_in s = g1 depends_on_in s1 )
assume that
A1: S = S1 +* S2 and
A2: S1 tolerates S2 ; :: thesis: for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for g being Gate of S
for g1 being Gate of S1 st g = g1 holds
g depends_on_in s = g1 depends_on_in s1
let A1 be non-empty Circuit of S1; :: thesis: for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for g being Gate of S
for g1 being Gate of S1 st g = g1 holds
g depends_on_in s = g1 depends_on_in s1
let A2 be non-empty Circuit of S2; :: thesis: for A being non-empty Circuit of S
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for g being Gate of S
for g1 being Gate of S1 st g = g1 holds
g depends_on_in s = g1 depends_on_in s1
let A be non-empty Circuit of S; :: thesis: for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for g being Gate of S
for g1 being Gate of S1 st g = g1 holds
g depends_on_in s = g1 depends_on_in s1
let s be State of A; :: thesis: for s1 being State of A1 st s1 = s | the carrier of S1 holds
for g being Gate of S
for g1 being Gate of S1 st g = g1 holds
g depends_on_in s = g1 depends_on_in s1
let s1 be State of A1; :: thesis: ( s1 = s | the carrier of S1 implies for g being Gate of S
for g1 being Gate of S1 st g = g1 holds
g depends_on_in s = g1 depends_on_in s1 )
assume A3: s1 = s | the carrier of S1 ; :: thesis: for g being Gate of S
for g1 being Gate of S1 st g = g1 holds
g depends_on_in s = g1 depends_on_in s1
let o be Gate of S; :: thesis: for g1 being Gate of S1 st o = g1 holds
o depends_on_in s = g1 depends_on_in s1
let o1 be Gate of S1; :: thesis: ( o = o1 implies o depends_on_in s = o1 depends_on_in s1 )
assume A4: o = o1 ; :: thesis: o depends_on_in s = o1 depends_on_in s1
A5: the carrier of S1 |` (the_arity_of o1) = the_arity_of o1 ;
thus o depends_on_in s = s * (the_arity_of o) by CIRCUIT1:def 3
.= s * (the_arity_of o1) by A1, A2, A4, Th16
.= s1 * (the_arity_of o1) by A3, A5, MONOID_1:1
.= o1 depends_on_in s1 by CIRCUIT1:def 3 ; :: thesis: verum