I had done somwhat about this issue. Please see my brog,

http://blog.livedoor.jp/s-koide/archives/1915880.html

http://blog.livedoor.jp/s-koide/archives/1916259.html

http://blog.livedoor.jp/s-koide/archives/1916982.html

http://blog.livedoor.jp/s-koide/archives/1917649.html

http://blog.livedoor.jp/s-koide/archives/1918198.html

http://blog.livedoor.jp/s-koide/archives/1918908.html

Unfortunately, they are in Japanese but you can use DeepL or others, and you can read Lisp code, of cource.

Any question will be welcome, of cource.

There is no problem with the operation, but

There is a typo: unprobable -> unprovable

I think analyzing this article might help you determine the correctness of your approach.

“I am not provable in PM-LISP” https://stopa.io/post/269