Closed Ayertienna closed 11 years ago
This was started (work on part 1 only for now, not yet finished - problems with good strong_norm definition)
part 1 is now finished, part 2 was started For the sake of satisfying my curiosity I will try to write an alternative version of this - using label-free language (current version uses labeled - and in the de Bruijn flavor - so a rewrite at some point is inevitable)
still work in progress for 1&2 together (but in LF case, so it's a cheaty cheat)
We need to formalize strong normalization using Tait's method. This will be done in 3 steps: