# Re: Help with choose and epsilon

```choose is carefully defined so the property you want is encoded in
its type.  There's some explanation of this in the paper at
http://www.csl.sri.com/tse98.html
You have to explicitly bring in the appropriate type constraints with
the typepred command.

Thus, one branch of your proof can be dealt with as shown below
(I haven't tried the other branch).

John

chosen_node_outputs :

|-------
{1}    (FORALL (net: Network, node: Node, pkt: Packet):
member(node, net) AND dest(pkt) = addr(node)
IMPLIES nonempty?(outQ(chooseNode(nextState(pkt, net)))))

Rule? (SKOSIMP)
Skolemizing and flattening,
this simplifies to:
chosen_node_outputs :

{-1}    member(node!1, net!1)
{-2}    dest(pkt!1) = addr(node!1)
|-------
{1}    nonempty?(outQ(chooseNode(nextState(pkt!1, net!1))))

Rule? (EXPAND "chooseNode")
Expanding the definition of chooseNode,
this simplifies to:
chosen_node_outputs :

[-1]    member(node!1, net!1)
[-2]    dest(pkt!1) = addr(node!1)
|-------
{1}    IF
nonempty?(filter(nextState(pkt!1, net!1),
(LAMBDA (n: Node): nonempty?(outQ(n)))))
THEN
nonempty?(outQ(choose(filter(nextState(pkt!1, net!1),
(LAMBDA (n: Node):
nonempty?(outQ(n)))))))
ELSE nonempty?(outQ(choose(nextState(pkt!1, net!1))))
ENDIF

Rule? (GROUND)
Applying propositional simplification and decision procedures,
this yields  2 subgoals:
chosen_node_outputs.1 :

{-1}    nonempty?(filter(nextState(pkt!1, net!1),
(LAMBDA (n: Node): nonempty?(outQ(n)))))
[-2]    member(node!1, net!1)
[-3]    dest(pkt!1) = addr(node!1)
|-------
{1}    nonempty?(outQ(choose(filter(nextState(pkt!1, net!1),
(LAMBDA (n: Node):
nonempty?(outQ(n)))))))

Rule? (TYPEPRED "choose(filter(nextState(pkt!1, net!1),
(LAMBDA (n: Node):
nonempty?(outQ(n)))))")

Adding type constraints for  choose(filter(nextState(pkt!1, net!1),
(LAMBDA (n: Node):
nonempty?(outQ(n))))),
this simplifies to:
chosen_node_outputs.1 :

{-1}    filter(nextState(pkt!1, net!1),
(LAMBDA (n: Node):
nonempty?(outQ(n))))(choose(filter(nextState(pkt!1, net!1),
(LAMBDA (n: Node):
nonempty?(outQ(n))))))
[-2]    nonempty?(filter(nextState(pkt!1, net!1),
(LAMBDA (n: Node): nonempty?(outQ(n)))))
[-3]    member(node!1, net!1)
[-4]    dest(pkt!1) = addr(node!1)
|-------
[1]    nonempty?(outQ(choose(filter(nextState(pkt!1, net!1),
(LAMBDA (n: Node):
nonempty?(outQ(n)))))))

Rule? (EXPAND "filter")
Expanding the definition of filter,
this simplifies to:
chosen_node_outputs.1 :

{-1}    nextState(pkt!1,
net!1)(choose({x: Node |
nextState(pkt!1, net!1)(x) & nonempty?(outQ(x))}))
&
nonempty?(outQ(choose({x: Node |
nextState(pkt!1,
net!1)(x)
&
nonempty?(outQ(x))})))
{-2}    nonempty?({x: Node | nextState(pkt!1, net!1)(x) & nonempty?(outQ(x))})
[-3]    member(node!1, net!1)
[-4]    dest(pkt!1) = addr(node!1)
|-------
{1}    nonempty?(outQ(choose({x: Node |
nextState(pkt!1,
net!1)(x)
&
nonempty?(outQ(x))})))

Rule? (GROUND)
Applying propositional simplification and decision procedures,

This completes the proof of chosen_node_outputs.1.

chosen_node_outputs.2 :

[-1]    member(node!1, net!1)
[-2]    dest(pkt!1) = addr(node!1)
|-------
{1}    nonempty?(filter(nextState(pkt!1, net!1),
(LAMBDA (n: Node): nonempty?(outQ(n)))))
{2}    nonempty?(outQ(choose(nextState(pkt!1, net!1))))

Rule?
-------

```