FDL > PVS > Prelude > bounded_nat_inductions : Theory

PVS-2.4 prelude.pvs

 bounded_nat_inductions provides the weak and strong forms of induction for
 the various bounded subtypes of nat.

bounded_nat_inductions [m: nat] : THEORY
BEGIN

pt: VAR pred[upto(m)]

jt: VAR upto(m)

kt: VAR upto(m)

%%(TCC) upto_induction_TCC1: OBLIGATION

%%(TCC) upto_induction_TCC2: OBLIGATION

upto induction: LEMMA (pt(0) AND (FORALL jt : ((jt < m) AND pt(jt)) IMPLIES pt(jt + 1))) IMPLIES (FORALL jt : pt(jt))

UPTO induction: LEMMA (FORALL jt : (FORALL kt : (kt < jt) IMPLIES pt(kt)) IMPLIES pt(jt)) IMPLIES (FORALL jt : pt(jt))

pb: VAR pred[below(m)]

jb: VAR below(m)

kb: VAR below(m)

%%(TCC) below_induction_TCC1: OBLIGATION

%%(TCC) below_induction_TCC2: OBLIGATION

below induction: LEMMA (((m > 0) IMPLIES pb(0)) AND (FORALL jb : ((jb < (m - 1)) AND pb(jb)) IMPLIES pb(jb + 1))) IMPLIES (FORALL jb : pb(jb))

BELOW induction: LEMMA (FORALL jb : (FORALL kb : (kb < jb) IMPLIES pb(kb)) IMPLIES pb(jb)) IMPLIES (FORALL jb : pb(jb))

END bounded_nat_inductions