import MaxLeafFormal.RSCCheck

/-! `#print axioms` for every public theorem of `RSCCheck`: the checkers' soundness lemmas report only
`propext`, `Classical.choice` and `Quot.sound`. Needs no generated data. -/

#print axioms MaxLeafFormal.RSCCheck.val_nonneg
#print axioms MaxLeafFormal.RSCCheck.okPt_parts_aux
#print axioms MaxLeafFormal.RSCCheck.ehat_eq
#print axioms MaxLeafFormal.RSCCheck.val_mergeI
#print axioms MaxLeafFormal.RSCCheck.okPt_mergeI
#print axioms MaxLeafFormal.RSCCheck.val_initI
#print axioms MaxLeafFormal.RSCCheck.okPt_initI
#print axioms MaxLeafFormal.RSCCheck.val_initInfI
#print axioms MaxLeafFormal.RSCCheck.okPt_initInfI
#print axioms MaxLeafFormal.RSCCheck.kpos_of_peel
#print axioms MaxLeafFormal.RSCCheck.inK_sound
#print axioms MaxLeafFormal.RSCCheck.getPt_chunksAux_aux
#print axioms MaxLeafFormal.RSCCheck.getPt_chunks32
#print axioms MaxLeafFormal.RSCCheck.dom_aux_okdims
#print axioms MaxLeafFormal.RSCCheck.dom_aux_getD
#print axioms MaxLeafFormal.RSCCheck.dom_aux_coe
#print axioms MaxLeafFormal.RSCCheck.dom_aux_map_getD
#print axioms MaxLeafFormal.RSCCheck.dom_aux_spec
#print axioms MaxLeafFormal.RSCCheck.dom_aux_conv
#print axioms MaxLeafFormal.RSCCheck.dom_aux_val_mem
#print axioms MaxLeafFormal.RSCCheck.dom_aux_nonneg
#print axioms MaxLeafFormal.RSCCheck.dom_sound
#print axioms MaxLeafFormal.RSCCheck.checkBlock_sound
#print axioms MaxLeafFormal.RSCCheck.okPts_of_subset
#print axioms MaxLeafFormal.RSCCheck.okPt_pos
#print axioms MaxLeafFormal.RSCCheck.ltLex_lex
#print axioms MaxLeafFormal.RSCCheck.ltLex_vlist
#print axioms MaxLeafFormal.RSCCheck.chain_vlist
#print axioms MaxLeafFormal.RSCCheck.nodup_vlist
#print axioms MaxLeafFormal.RSCCheck.list8_of_length
#print axioms MaxLeafFormal.RSCCheck.vlist_eq_of_val
#print axioms MaxLeafFormal.RSCCheck.checkZ_okPts
#print axioms MaxLeafFormal.RSCCheck.checkZ_length
#print axioms MaxLeafFormal.RSCCheck.checkZ_nodup
#print axioms MaxLeafFormal.RSCCheck.checkZ_fin
#print axioms MaxLeafFormal.RSCCheck.fam_mem_finsetOf
#print axioms MaxLeafFormal.RSCCheck.fam_finsetOf_nonneg
#print axioms MaxLeafFormal.RSCCheck.fam_leaf_mem
#print axioms MaxLeafFormal.RSCCheck.fam_inf_mem
#print axioms MaxLeafFormal.RSCCheck.checkC2_sound
#print axioms MaxLeafFormal.RSCCheck.checkLeaves_sound
#print axioms MaxLeafFormal.RSCCheck.chainFact_of_stages
#print axioms MaxLeafFormal.RSCCheck.checkChain1_sound
#print axioms MaxLeafFormal.RSCCheck.cover_blocks
#print axioms MaxLeafFormal.RSCCheck.init00_mem
#print axioms MaxLeafFormal.RSCCheck.foldl_mem_PZ
#print axioms MaxLeafFormal.RSCCheck.foldl_merge_add_left
#print axioms MaxLeafFormal.RSCCheck.foldl_merge_smul_left
#print axioms MaxLeafFormal.RSCCheck.mem_lattice5
#print axioms MaxLeafFormal.RSCCheck.mem_lattice4
#print axioms MaxLeafFormal.RSCCheck.scS_spec
#print axioms MaxLeafFormal.RSCCheck.scG_spec
#print axioms MaxLeafFormal.RSCCheck.sc_uF_ratio
#print axioms MaxLeafFormal.RSCCheck.sc_wF_ratio
#print axioms MaxLeafFormal.RSCCheck.init_eq_vecN
#print axioms MaxLeafFormal.RSCCheck.vecN_smul
#print axioms MaxLeafFormal.RSCCheck.vecN_add
#print axioms MaxLeafFormal.RSCCheck.vecN_zero
#print axioms MaxLeafFormal.RSCCheck.sc_listSum
#print axioms MaxLeafFormal.RSCCheck.combWitness_sound
#print axioms MaxLeafFormal.RSCCheck.rsc5_list_sum_eq
#print axioms MaxLeafFormal.RSCCheck.rsc5_convex_sum
#print axioms MaxLeafFormal.RSCCheck.rsc5_foldl_sum
#print axioms MaxLeafFormal.RSCCheck.rsc5_foldl_conv
#print axioms MaxLeafFormal.RSCCheck.rsc5_smul_sum
#print axioms MaxLeafFormal.RSCCheck.rsc5_finset_nonneg
#print axioms MaxLeafFormal.RSCCheck.rsc5_chain
#print axioms MaxLeafFormal.RSCCheck.rsc5_shape5
#print axioms MaxLeafFormal.RSCCheck.rsc4_shape4
#print axioms MaxLeafFormal.RSCCheck.rsc5_point
#print axioms MaxLeafFormal.RSCCheck.rsc4_dat
#print axioms MaxLeafFormal.RSCCheck.rsc4_point
#print axioms MaxLeafFormal.RSCCheck.checkLattice5_sound
#print axioms MaxLeafFormal.RSCCheck.checkLattice4_sound
#print axioms MaxLeafFormal.RSCCheck.forall_mem_append'
#print axioms MaxLeafFormal.RSCCheck.forall_lt_of_forall_range
#print axioms MaxLeafFormal.RSCCheck.agg_getD_okPts
#print axioms MaxLeafFormal.RSCCheck.agg_stage_aux
#print axioms MaxLeafFormal.RSCCheck.c1_of_blocks
#print axioms MaxLeafFormal.RSCCheck.stage_of_blocks
#print axioms MaxLeafFormal.RSCCheck.stage_X_ok
#print axioms MaxLeafFormal.RSCCheck.stage_Yt_ok
#print axioms MaxLeafFormal.RSCCheck.chain1_table
#print axioms MaxLeafFormal.RSCCheck.chain_stages_table
#print axioms MaxLeafFormal.RSCCheck.leaf_table