Prove a theorem using FGL with case-splitting.
Def-fgl-param-thm is similar to def-fgl-thm, but runs a clause
processor prior to FGL that splits the goal into several cases based on the
provided arguments. It somewhat replicates the behavior of ACL2::def-gl-param-thm, but ignores the shape specifiers provided for the
The usage of def-fgl-param-thm is similar to that of def-fgl-thm, but it accepts several more keyword arguments:
- :param-bindings is the same as in ACL2::def-gl-param-thm, but
the shape specifier alist in each entry is ignored.
- :param-hyp is the same as in ACL2::def-gl-param-thm.
- :split-params provides the fgl-sat-check parameters object for
proving that case split provided covers all cases.
- :solve-params provides the fgl-sat-check object for proving each case.
- :repeat-concl-p controls whether the conclusion is (if nil)
rewritten/symbolically executed once and then solved separately for each case,
or (if nonnil) rewritten/symbolically executed (and also solved) separately for