PMRS Assertion

Current used assertion in database:

Existence of:

1.local assumption

2."case_of" constant

3."Conjunction" as outmost constant

4."For all" constant

5.associated "pinduct" rule.

6.associated "psimps" rule.

7.associated "pelims" rule.

8.associated "cases" rule.

9.associated "intro" rule.

10.associated recursive "simp" rule

11.constant with prefix "Num"

12.Constant defined by lift_definition

13.Constant defined by primcorec

14.Constant defined by interpretation (Not working accurately)

15.Check if the length of outmost constant is greater than 1.(a function Constant)

Currently written but not used assertion:

Check if all constants are defined in Main

Check if there is a constant with prefix "Real"

Possible future assertion:

Expanding into integer feature:

#subgoal

Length of proof obligation

Check if there is a record typed variable

Check for typeclass definition

Constant "===>"