The files contained are a README file and a tarred gzipped file containing the full development, as well as the individual files.

The formal development was performed with Version 6.1 of the Coq proof system, and may not work with more recent releases. Instructions for running the formal proofs with Coq 6.1 are included in the README file.

The files contained are:

• README

• MinMJ.tgz

• autocontra.g
• autocontra.ml
• autocontra.v
• Complete.g
• Complete.v
• Makefile
• MinMJ_booleans.g
• MinMJ_booleans.v
• MinMJ_Bridge.g
• MinMJ_Bridge.v
• MinMJ_Bridge2.g
• MinMJ_Bridge2.v
• MinMJ_Bridge3.g
• MinMJ_Bridge3.v
• MinMJ_Drop.g
• MinMJ_Drop.v
• MinMJ_Exchange.g
• MinMJ_Exchange.v
• MinMJ_Exchange2.g
• MinMJ_Exchange2.v
• MinMJ_Exchange3.g
• MinMJ_Exchange3.v
• MinMJ_F.g
• MinMJ_F.v
• MinMJ_HeightL.g
• MinMJ_HeightL.v
• MinMJ_HeightM.g
• MinMJ_HeightM.v
• MinMJ_Hyps.g
• MinMJ_Hyps.v
• MinMJ_In.g
• MinMJ_In.v
• MinMJ_L.g
• MinMJ_L.v
• MinMJ_L_Admis_RhoBar.g
• MinMJ_L_Admis_RhoBar.v
• MinMJ_Lift.g
• MinMJ_Lift.v
• MinMJ_Lifts.g
• MinMJ_Lifts.v
• MinMJ_LJ.g
• MinMJ_LJ.v
• MinMJ_LMN.g
• MinMJ_LMN.v
• MinMJ_lt.g
• MinMJ_lt.v
• MinMJ_M.g
• MinMJ_M.v
• MinMJ_M_AdmisPsi.g
• MinMJ_M_AdmisPsi.v
• MinMJ_Main.g
• MinMJ_Main.v
• MinMJ_MJ.g
• MinMJ_MJ.v
• MinMJ_Msub.g
• MinMJ_Msub.v
• MinMJ_N.g
• MinMJ_N.v
• MinMJ_N_Admis_Phi.g
• MinMJ_N_Admis_Phi.v
• MinMJ_N_Admis_Theta.g
• MinMJ_N_Admis_Theta.v
• MinMJ_nat.g
• MinMJ_nat.v
• MinMJ_NJ.g
• MinMJ_NJ.v
• MinMJ_Normal_Perm.g
• MinMJ_Normal_Perm.v
• MinMJ_Normal_RhoBar.g
• MinMJ_Normal_RhoBar.v
• MinMJ_NormL.g
• MinMJ_NormL.v
• MinMJ_Nsub.g
• MinMJ_Nsub.v
• MinMJ_Occurs.g
• MinMJ_Occurs.v
• MinMJ_Occurs_Lift.g
• MinMJ_Occurs_Lift.v
• MinMJ_PermDef.g
• MinMJ_PermDef.v
• MinMJ_phi.g
• MinMJ_phi.v
• MinMJ_phibar.g
• MinMJ_phibar.v
• MinMJ_psi.g
• MinMJ_psi.v
• MinMJ_psitheta.g
• MinMJ_psitheta.v
• MinMJ_rhobar.g
• MinMJ_rhobar.v
• MinMJ_Strength.g
• MinMJ_Strength.v
• MinMJ_Syntax.g
• MinMJ_Syntax.v
• MinMJ_theta.g
• MinMJ_theta.v
• MinMJ_thetapsi.g
• MinMJ_thetapsi.v
• MinMJ_Weak.g
• MinMJ_Weak.v