[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] what kind of induction


 If I have the following definitions, who can hint me  which induction method shall be used to prove "Config_Inv"?
 I think it must hold.  thank you in advance!

 SEQB: TYPE = sequence[bool]

 sgm: VAR SEQB

 n: VAR nat

 config(sgm)(n): RECURSIVE nat =  IF n = 0 THEN 0
      ELSE LET pre = config(sgm)(n - 1) IN
              IF sgm(n) THEN pre + 1 ELSE pre ENDIF

 Config_Inv: LEMMA FORALL (m: upfrom(n)):   config(sgm)(m) = config(sgm)(n) => (FORALL (i: subrange(n + 1, m)): NOT sgm(i))

Best Regards
Qingguo XU