let G1, G2 be non empty non void Circuit-like ManySortedSign ; :: thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let f, g be Function; :: thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let C1 be non-empty Circuit of G1; :: thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let C2 be non-empty Circuit of G2; :: thesis: ( f,g form_embedding_of C1,C2 implies for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1 )
assume that
f is one-to-one and
g is one-to-one and
A1: f,g form_morphism_between G1,G2 and
the Sorts of C1 = the Sorts of C2 * f and
the Charact of C1 = the Charact of C2 * g ; :: according to CIRCTRM1:def 12 :: thesis: for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let o1 be Gate of G1; :: thesis: for o2 being Gate of G2 st o2 = g . o1 holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let o2 be Gate of G2; :: thesis: ( o2 = g . o1 implies for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1 )
assume A2: o2 = g . o1 ; :: thesis: for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let s1 be State of C1; :: thesis: for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let s2 be State of C2; :: thesis: ( s1 = s2 * f implies o2 depends_on_in s2 = o1 depends_on_in s1 )
assume A3: s1 = s2 * f ; :: thesis: o2 depends_on_in s2 = o1 depends_on_in s1
thus o2 depends_on_in s2 = s2 * (the_arity_of o2) by CIRCUIT1:def 3
.= s2 * (f * (the_arity_of o1)) by A1, A2
.= s1 * (the_arity_of o1) by A3, RELAT_1:36
.= o1 depends_on_in s1 by CIRCUIT1:def 3 ; :: thesis: verum