( ! [V__PA,V__G,V__AN,V__PN,V__M,V__N,V__AA] :
((s__instance(V__PA,s__Object) &
s__instance(V__G,s__Graph) &
s__instance(V__PN,s__Physical) &
s__instance(V__M,s__UnitOfMeasure) &
s__instance(V__N,s__RealNumber))
=>
(s__graphMeasure(V__G,V__M)
&
s__instance(V__AN,s__GraphNode) &
s__graphPart(V__AN,V__G)
&
s__graphPart(V__AA,V__G)
&
s__instance(V__AA,s__GraphArc) &
s__abstractCounterpart(V__AN,V__PN)
&
s__abstractCounterpart(V__AA,V__PA)
&
s__arcWeight(V__AA,s__MeasureFn(V__N,V__M)))
=>
s__measure(V__PA,s__MeasureFn(V__N,V__M))
)
)

Merge.kif 58165826 

( ! [V__ARC,V__GRAPH] :
((s__instance(V__GRAPH,s__DirectedGraph) &
s__instance(V__ARC,s__GraphArc) &
s__graphPart(V__ARC,V__GRAPH))
=>
( ? [V__NODE1, V__NODE2] :
((s__instance(V__NODE1,s__GraphNode) &
s__instance(V__NODE2,s__GraphNode) &
((s__InitialNodeFn(V__ARC)
= V__NODE1)
&
(s__TerminalNodeFn(V__ARC)
= V__NODE2)))))
)
)

Merge.kif 53485356 

( ! [V__NODE,V__ARC,V__GRAPH] :
(s__instance(V__NODE,s__GraphNode) =>
(s__instance(V__GRAPH,s__GraphPath) &
s__instance(V__ARC,s__GraphArc) &
s__graphPart(V__ARC,V__GRAPH))
=>
(s__InitialNodeFn(V__ARC)
= V__NODE)
=>
~(( ? [V__OTHER] :
((s__instance(V__OTHER,s__GraphArc) &
((s__InitialNodeFn(V__OTHER)
= V__NODE)
&
~((V__OTHER = V__ARC)))))))
)
)

Merge.kif 53995409 

( ! [V__NODE,V__ARC,V__GRAPH] :
(s__instance(V__NODE,s__GraphNode) =>
(s__instance(V__GRAPH,s__GraphPath) &
s__instance(V__ARC,s__GraphArc) &
s__graphPart(V__ARC,V__GRAPH))
=>
(s__TerminalNodeFn(V__ARC)
= V__NODE)
=>
~(( ? [V__OTHER] :
((s__instance(V__OTHER,s__GraphArc) &
((s__TerminalNodeFn(V__OTHER)
= V__NODE)
&
~((V__OTHER = V__ARC)))))))
)
)

Merge.kif 54115421 

( ! [V__ARC] :
(s__instance(V__ARC,s__GraphArc) =>
( ? [V__NODE1, V__NODE2] :
((s__instance(V__NODE1,s__GraphNode) &
s__instance(V__NODE2,s__GraphNode) &
s__links(V__NODE1,V__NODE2,V__ARC))))
)
)

Merge.kif 54945497 
