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

[PVS-Help] what kind of induction



Hi:

 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
    ENDIF   MEASURE n


 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