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

[PVS-Help] The problem with self-stability example



Hi,

   I'm learning the self-stability example which was downloaded from the
link: ftp://ftp.csl.sri.com/pub/pvs/examples/self-stability/  ,and I try
to prove the "update_active" Lemma in the stability THEORY. I follow the
steps in stability.dmp file,but I find that I can not complete the
proof,I don't know why, who can help me or tell me how what's the
problem? thanks.


                                                (|update_active|
                                                 ""
                                                 (SKOSIMP*)
                                                 ((""
                                                   (EXPAND "update_P")
                                                   ((""
                                                     (FLATTEN)
                                                     ((""
                                                       (CASE
                                                        "active(s1!1)(p!
1)")
                                                       (("1"
                                                         (HIDE 1)
                                                         (("1"
                                                           (PROP)
                                                           (("1"
                                                             (LEMMA
                                                              "mod_inc"
                                                              ("u" "s0!
1(0)"))
                                                             (("1"
                                                               (GRIND
                                                                :EXCLUDE
                                                                "mod")
                                                               NIL)))
                                                            ("2"
                                                             (GRIND
                                                              :EXCLUDE
                                                              "mod")
                                                             NIL)))))


This completes the proof of update_active.1.  


                                                        ("2"

(APPLY-EXTENSIONALITY
                                                          :HIDE?
                                                          T)


but after I apply (apply-extensionality :hide? t) command, it yields
4 subgoals, and the proof can not be completed with the commands shows
below, so what's the problem? thanks in advance.


                                                         (("2"
                                                           (LEMMA
                                                            "mod_lt_nat"
                                                            ("n"
                                                             "x!1"
                                                             "m"
                                                             "N"))
                                                           (("2"
                                                             (GRIND
                                                              :EXCLUDE
                                                              "mod"
                                                              :REWRITES

"mod_eq_arg")

NIL)))))))))))))



lingzhao
Best Regards.