(def-constant alt%failure_q 
    "lambda(f:[uu, sets[sets[action]]], 
          forall(u:uu,x,y:sets[action], y in f(u) and x subseteq y implies x in f(u))
          and
          e in support(f)
          and
        forall(u,v:uu, u in support(f) and v prefix u implies v in support(f))
          and
        forall(u:uu, a:action, x:sets[action],
                x in f(u) and 
                forall(m:uu, germ(m)=a implies not (u**m) in support(f))
                  implies
                  (x union singleton{a}) in f(u))
          and
        total_q{f,[uu ->  sets[sets[action]]]}
          and
        forall(u:uu,s:sets[action], s in f(u) implies not (germ(e)) in s))"
    (theory directed-monoid-theory))

(def-theorem failure-alt-failure-equivalence 
    "forall(f:[uu, sets[sets[action]]], failure_q(f) iff alt%failure_q(f))"
    (theory monoid-transition-system)
    (proof
      (
        unfold-defined-constants
        direct-and-antecedent-inference-strategy
        (block 
            (script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0 0 0 0 0)")
            (backchain "with(p:prop,forall(u:uu,x,y:sets[action],p));")
            auto-instantiate-existential)
        (block 
            (script-comment "`direct-and-antecedent-inference-strategy' at (0 0 2 0 0 0 0)")
            (backchain "with(p:prop,forall(u,v:uu,p));")
            auto-instantiate-existential)
        (block 
            (script-comment "`direct-and-antecedent-inference-strategy' at (0 0 3 0 0 0 0)")
            (backchain "with(p:prop,forall(u:uu,a:action,p));")
            direct-and-antecedent-inference-strategy
            (block 
	(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
	(unfold-single-defined-constant (0) support)
	simplify-insistently
	auto-instantiate-existential)
            (backchain "with(p:prop,forall(m:uu,p implies p));"))
        (block 
            (script-comment "`direct-and-antecedent-inference-strategy' at (0 1 5 0 0 0)")
            (backchain "with(p:prop,forall(u:uu,x,y:sets[action],p));")
            (backchain "with(p:prop,forall(u:uu,s:sets[action],p));")
            auto-instantiate-existential)
        (block 
            (script-comment "`direct-and-antecedent-inference-strategy' at (0 1 0 0 0 0 0)")
            (backchain "with(p:prop,forall(u:uu,x,y:sets[action],p));")
            auto-instantiate-existential)
        (block 
            (script-comment "`direct-and-antecedent-inference-strategy' at (0 1 2 0 0 0 0)")
            (backchain "with(p:prop,forall(u,v:uu,p));")
            auto-instantiate-existential)
        (block 
            (script-comment "`direct-and-antecedent-inference-strategy' at (0 1 3 0 0 0 0 0 0)")
            (backchain "with(p:prop,forall(u:uu,a:action,x:sets[action],p));")
            direct-and-antecedent-inference-strategy
            (backchain "with(p:prop,forall(m:uu,p or p));"))
        )))