meng_scaff_defs[T: TYPE ]: THEORY BEGIN IMPORTING paths[T], subgraphs[T], sep_sets[T],VAR graph[T]VAR TVAR doubleton[T]VAR finite_set[T]VAR prewalkIMPORTING ind_paths[T]IMPORTING graph_deg[T]EXISTS z: edges(G)(e) AND e = dbl(v,z) AND vert(H(G,x,w1,w2))(z))}AND t /= y})): graph[T] =in ?(G,s,t,w1,w2): bool = vert(G)(s) AND vert(G)(t) AND vert(G)(w1)AND vert(G)(w2) AND w1 /= w2 AND w1 /= s AND w2 /= s AND w1 /= t AND w2 /= t) LEMMA vert(G)(s) AND s /= w1 AND s /= w2IMPLIES vert(H(G, s, w1, w2))(s)LEMMA path?(H(G,s,w1,w2),p) IMPLIES NOT verts_of(p)(w1) AND NOT verts_of(p)(w2)% MOVED TO theory subgraph_paths % % walk?_subgraph : LEMMA subgraph?(HH,G) AND walk?(HH, p) % IMPLIES walk?(G, p) % % path?_subgraph : LEMMA subgraph?(HH,G) AND path?(HH, p) % IMPLIES path?(G, p) LEMMA path?(H(G,s,w1,w2),p) IMPLIES path?(G,p)LEMMA walk?(G, p) AND seq(p)(0) = s AND NOT verts_of(p)(w1) AND NOT verts_of(p)(w2) IMPLIES walk?(H(G, s, w1, w2), p)LEMMA in ?(G, s, t, w1, w2) AND disjoint?(s, t, w1, w2)IMPLIES subset?(vert(meng(G, s, t, w1, w2)), vert(G))LEMMA del_vert(del_vert(G,w2),w1) = LEMMA H(G, t, w2, w1) = H(G, t, w1, w2)LEMMA incident(v, G, t, w2, w1) = incident(v, G, t, w1, w2)LEMMA vert(G)(s) AND vert(G)(t) AND AND w1 /= s AND AND w2 /= s IMPLIES meng(G, t, s, w1, w2) = meng(G, t, s, w2, w1)END meng_scaff_defsquality 100%
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
