Mechanizing Proofs of Computation Equivalence

• zipped MarceloGlusmanThesis.pdf
• zipped seminar.ppt
• indep.pvs, the theory which proves the lemmas comparing definitions of Conditional Commutativity and Functional Independence, and indep.prf, its corresponding .prf file.