Verification of the Redecoration Algorithm for Triangular Matrices

Proof scripts that were working in 2007 on the then current releases of Coq and Isabelle

• Coq vernacular file with functional induction but not for fromListRep
• Coq vernacular file without any functional induction
• The Coq vernacular file that uses functional induction also for fromListRep (experimental!)
• The Isabelle theory file

Added in late 2010

• The Isabelle theory file for Isabelle2009-2

Added in late 2012

• Coq vernacular file with functional induction but not for fromListRep
• Coq vernacular file without any functional induction
• The Coq vernacular file that uses functional induction also for fromListRep (nowadays unproblematic)