( ! [V__GRAPH] :
((s__instance(V__GRAPH,s__GraphCircuit) =>
( ? [V__NODE] :
((s__instance(V__NODE,s__GraphNode) &
((s__BeginNodeFn(V__GRAPH)
= V__NODE)
&
(s__EndNodeFn(V__GRAPH)
= V__NODE))))))
&
(( ? [V__NODE] :
((s__instance(V__NODE,s__GraphNode) &
((s__BeginNodeFn(V__GRAPH)
= V__NODE)
&
(s__EndNodeFn(V__GRAPH)
= V__NODE)))))
=>
s__instance(V__GRAPH,s__GraphCircuit))
)
)
|
Merge.kif 5429-5434 |
A graph path is an instance of graph circuit if and only if there exists a graph node such that the beginning of the graph path is equal to the graph node and the end of the graph path is equal to the graph node |
( ! [V__END,V__DIST,V__SYS,V__PATH,V__START,V__GRAPH] :
((s__instance(V__END,s__Region) &
s__instance(V__DIST,s__ConstantQuantity) &
s__instance(V__SYS,s__TransitSystem) &
s__instance(V__PATH,s__Transitway) &
s__instance(V__PATH,s__TransitSystem) &
s__instance(V__START,s__Region) &
s__instance(V__GRAPH,s__GraphPath))
=>
(s__distanceOnPath(V__DIST,V__PATH)
&
s__pathInSystem(V__PATH,V__SYS)
&
s__routeStart(V__START,V__PATH)
&
s__routeEnd(V__END,V__PATH)
&
s__abstractCounterpart(V__GRAPH,V__SYS))
=>
( ? [V__S, V__BN, V__EN] :
((s__instance(V__S,s__Graph) &
s__instance(V__BN,s__GraphNode) &
s__instance(V__EN,s__GraphNode) &
(s__subGraph(V__S,V__GRAPH)
&
(V__BN = s__BeginNodeFn(V__GRAPH))
&
(V__EN = s__EndNodeFn(V__GRAPH))
&
s__abstractCounterpart(V__BN,V__START)
&
s__abstractCounterpart(V__EN,V__END)))))
)
)
|
Transportation.kif 2784-2797 |
|
( ! [V__NODE2,V__NODE1,V__GRAPH] :
((s__instance(V__GRAPH,s__Graph) &
s__instance(V__NODE1,s__GraphNode) &
s__instance(V__NODE2,s__GraphNode) &
s__graphPart(V__NODE1,V__GRAPH)
&
s__graphPart(V__NODE2,V__GRAPH)
&
~((V__NODE1 = V__NODE2)))
=>
( ? [V__ARC, V__PATH] :
((s__instance(V__ARC,s__GraphArc) &
(s__links(V__NODE1,V__NODE2,V__ARC)
|
(s__subGraph(V__PATH,V__GRAPH)
&
s__instance(V__PATH,s__GraphPath) &
(((s__BeginNodeFn(V__PATH)
= V__NODE1)
&
(s__EndNodeFn(V__PATH)
= V__NODE2))
|
((s__BeginNodeFn(V__PATH)
= V__NODE2)
&
(s__EndNodeFn(V__PATH)
= V__NODE1))))))))
)
)
|
Merge.kif 5303-5323 |
|
