corner-cases/alg-conv-trans-acc-right

Test "corner-cases/alg-conv-trans-acc-right"

Expected: 🤷 either · Size: 67.3 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

The mechanical half of corner-cases/alg-conv-trans-acc. With a constructor in the major premise, Acc.rec fires and step descends to the predecessor 0.

Checker	Result	⏱️	🧠
mathgraph	👍	2 ms	75.8 MB
sokonanoda	👍	2 ms	61.6 MB
nanoclo	👍	3 ms	51.4 MB
con-ron	👍	26 ms	58.7 MB
lazylean	👍	3 ms	22.1 MB
nanoda	👍	3 ms	3.2 MB
nanobruijn	👍	5 ms	12.0 MB
con-leche	👍	9 ms	28.3 MB
eink0rn	👍	5 ms	17.1 MB
ind-models	👍	84 ms	109.7 MB
official	👍	34 ms	65.6 MB
lean4lean	👍	35 ms	100.0 MB
tenet	👍	149 ms	46.0 MB
nanoclo-fortran	👍	5 ms	5.2 MB
lean4cobol	👍	55 ms	13.9 MB
evmlean	👍	39.2 s	303.6 MB
mini	👍	203 ms	74.0 MB
overfull	💥	1.7 m	49.3 MB
kiota	👍	3 ms	11.0 MB
canonical-min	🚫	403 ms	1.1 GB
rpylean	👍	3 ms	8.0 MB
vow-lean-kernel	👍	357 ms	8.8 MB
official-v4.28.0	👍	41 ms	73.5 MB
still-nanoda	👍	3 ms	3.2 MB
nyaya	👍	14 ms	12.1 MB
parse-only	👍	31 ms	65.5 MB