This is a formalisation of Wim Ruitenburg's paper "On the Period of Sequences (An(p)) in Intuitionistic Propositional Calculus" (JSL 1984).

Name
Last commit
Last update
.gitignore Loading commit data...
BoundsLists.v Loading commit data...
BoundsSubformulas.v Loading commit data...
HilbertIPCsetup.v Loading commit data...
Ruitenburg1984Aux.v Loading commit data...
Ruitenburg1984KeyTheorem.v Loading commit data...
Ruitenburg1984Main.v Loading commit data...
coqdoc.css Loading commit data...
coqdoc.sty Loading commit data...
f_p_exform1_10_length_fp_haskell.txt Loading commit data...
f_p_exform1_10_output.txt Loading commit data...
make.sh Loading commit data...
ruitenburg_modified.hs Loading commit data...