[isabelle] SOME simplification



Hello everybody,
in IOA logic I want to demonstrate:
a: "prob((%e. (L (SOME i. (L i e)) e)) ~> Q, q)"
knowing:
g: "FORALL i::nat. prob (%e. (L i e) ~> Q,  q)"
where "~>" is the Leadsto operator of TLS, the temporal logic of step
developed in Muller's PhD thesis.
L and Q are predicates of type " 'a Seq => bool ", while prob is a function
of type " ('a Seq => bool) x fraction => bool ".

Knowing from "g" that the result is true for every natural number I'm not
able to demonstrate "a", but I think it's correct because "(SOME i. (L i
e))" is just a particular natural number.
I tried using spec theorem but it don't work.

Can someone help me?

Thanks
Gabriele Pozzani




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.