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 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & s2 is stable holds
s1 is stable
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 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & s2 is stable holds
s1 is stable
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 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & s2 is stable holds
s1 is stable
let C2 be non-empty Circuit of G2; :: thesis: ( f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 implies for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & s2 is stable holds
s1 is stable )
assume A1: ( f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 ) ; :: thesis: for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & s2 is stable holds
s1 is stable
let s2 be State of C2; :: thesis: for s1 being State of C1 st s1 = s2 * f & s2 is stable holds
s1 is stable
let s1 be State of C1; :: thesis: ( s1 = s2 * f & s2 is stable implies s1 is stable )
assume A2: s1 = s2 * f ; :: thesis: ( not s2 is stable or s1 is stable )
assume s2 = Following s2 ; :: according to CIRCUIT2:def 6 :: thesis: s1 is stable
hence s1 = Following s1 by A1, A2, Th47; :: according to CIRCUIT2:def 6 :: thesis: verum