import Papers

-- The paper's results: each must list no axiom beyond propext, Classical.choice and Quot.sound.
#print axioms Papers.OaiBoundDyadicTriangular.dyadic_triangular_bound
#print axioms Papers.OaiBoundDyadicTriangular.matrixEnergy_hessian
#print axioms Papers.OaiBoundDyadicTriangular.hessForm_order
#print axioms Papers.OaiBoundDyadicTriangular.matrixEnergy_midpoint_gap
#print axioms Papers.OaiBoundDyadicTriangular.abs_trace_le_hessForm_sum
#print axioms Papers.OaiBoundDyadicTriangular.energyIncrement_controls_trace
#print axioms Papers.OaiBoundDyadicTriangular.totalEnergy_bound_and_telescope
#print axioms Papers.OaiBoundDyadicTriangular.localForm_one_scale_bound