pvs0_factorial_terminating :
|-------
{1} terminating?[nat](pvs0_factorial)
Rule? (PVS0-TERMINATING$ "factorial")
[...]
Using lemma c_bounding_from_gl_termination,
this simplifies to:
pvs0_factorial_terminating :
{-1} bounding_from_graph(ccg_to_mwg(make_ccg
[nat, PVS0Expr[nat],
Conditions[nat], Path[nat], MT,
LAMBDA (m, n: nat): m < n, 1]
(factorial_dg, factorial_measures))
(factorial_mm))
IMPLIES
mwg_termination?(ccg_to_mwg(make_ccg
[nat, PVS0Expr[nat],
Conditions[nat], Path[nat], MT,
LAMBDA (m, n: nat): m < n, 1]
(factorial_dg, factorial_measures))
(factorial_mm))
|-------
[1] mwg_termination?(ccg_to_mwg(make_ccg
[nat, PVS0Expr[nat], Conditions[nat],
Path[nat], MT,
LAMBDA (m, n: nat): m < n, 1]
(factorial_dg, factorial_measures))
(factorial_mm))
Simplifying, rewriting, and recording with decision procedures,
this simplifies to:
pvs0_factorial_terminating :
|-------
{1} bounding_from_graph(ccg_to_mwg(make_ccg
[nat, PVS0Expr[nat],
Conditions[nat], Path[nat], MT,
LAMBDA (m, n: nat): m < n, 1]
(factorial_dg, factorial_measures))
(factorial_mm))
[2] mwg_termination?(ccg_to_mwg(make_ccg
[nat, PVS0Expr[nat], Conditions[nat],
Path[nat], MT,
LAMBDA (m, n: nat): m < n, 1]
(factorial_dg, factorial_measures))
(factorial_mm))
debugger invoked on a COMMON-LISP:TYPE-ERROR @7007712C1C in thread
#<THREAD "main thread" RUNNING {7012FA0443}>:
The value
21065
is not of type
(INTEGER -8192 16383)
when binding SB-ASSEM:LABEL
Type HELP for debugger help, or (SB-EXT:EXIT) to exit from SBCL.
restarts (invokable by number or by possibly-abbreviated name):
0: [ABORT] Exit debugger, returning to top level.
(SB-ARM64-ASM::EMIT-TEST-BRANCH-IMM #<SB-ASSEM:SEGMENT {7037954833}> 0 1 0 21065 12) [external]
0]
On 2a896b1, the error
The value 21065 is not of type (INTEGER -8192 16383) when binding SB-ASSEM:LABELis hit when applyingPVS0-TERMINATING$on NASALib/PVS0@factorial_pvs0.pvs0_factorial_terminating