is mentioned by
Thm* ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [trace_inv_induction] |
Def (M |= x,tr.P(x;tr) while Q(x;tr))
== (M |= x,x',tr,tr'.P(x;tr) ![]() ![]() ![]() ![]() ![]() ![]() | [while] |
Def (M |= x,x',tr,tr'.R(x;x';tr;tr'))
== ![]() ![]() ![]() ![]() ![]() | [tla] |
Def (M |= always s,t.P(s;t))
== ![]() ![]() ![]() ![]() ![]() | [trace_inv] |
Def (M |= initially x,tr.P(x;tr)) == ![]() ![]() ![]() | [initially] |
In prior sections: core well fnd int 1 bool 1 sqequal 1 fun 1 int 2 list 1 prog 1 rel 1 mb basic mb nat union num thy 1 mb list 1 mb label
Try larger context: GenAutomata