Mentions légales du service

Skip to content
  • François Bobot's avatar
    transformation eliminant les quantifications inutiles. · 95c2ea8f
    François Bobot authored
    (exists x. x=t and F) -> F[t/x]
    (forall x. x<>t or F) -> F[t/x]
    
    Cette transformation n'élimine pas les quantifications qui ont des
    triggers mais s'applique sous ces derniers. Le but est de pouvoir
    éliminer les quantifications inutilement ajoutées lors de eliminate
    inductive.
    95c2ea8f