[isabelle] SOME simplification
in IOA logic I want to demonstrate:
a: "prob((%e. (L (SOME i. (L i e)) e)) ~> Q, q)"
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and