61 in wina induction prooving lemma 2 cheap wins imply cheap strat formulas

equivio / silent-step-spectroscopy

Isabelle formalization of linear-time–branching-time spectroscopy accounting for silent steps

Other

0 stars 0 forks source link

Closed Vervada closed 10 months ago

Vervada commented 10 months ago

Open:

[x] Prove lemma expr_imm_conj
[x] Prove lemma expr_conj
[x] Prove case 2.1. (attacker immediate) when the reached defender_conj is a leaf
[x] Use some magic on prove 3.6 (defender branching conj)
[x] Prove lemma expr_br_conj

crmrtz commented 10 months ago

Ready for merge

crmrtz commented 10 months ago

Impressive work! 🥳

I think you can do with slightly simpler strategy formulas.

And maybe , some of the price calculations could be moved.

Thanks for the feedback. The according changes are implemented.