FDL > PVS > Prelude > wf_induction : Theory

PVS-2.4 prelude.pvs

 wf_induction defines induction for any type that has a well-founded
 relation.

wf_induction [T:TYPE, < : (well founded?[T]) ] : THEORY
BEGIN

wf induction: LEMMA FORALL (p:pred[T]) : (FORALL (x:T) : (FORALL (y:T) : (y < x) IMPLIES p(y)) IMPLIES p(x)) IMPLIES (FORALL (x:T) : p(x))

END wf_induction