# principia-generalized-petersen: `#print axioms` の出力（1 モジュール）。全行が propext / Classical.choice / Quot.sound の部分集合。

## Principia.GeneralizedPetersen.Chk  (188 行)
'GeneralizedPetersen.Base.GP_adj' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Base.GP_adj_outer' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Base.GP_adj_inner' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Base.GP_adj_spoke' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Base.GP_adj_shift' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Base.GP_adj_rot_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.rotIso' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.rot_pow_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.rot_pow_free' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.rotIso_hamiltonian' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.GPfin_iso' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.quotMap_adj' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Base.quotHom' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Base.quotMap_rot' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Base.quotMap_rot_pow_self' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.quotMap_eq_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.lift_connected_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.lift_connected_three' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.Flow.W_sub_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.Flow.W_const' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.Flow.sum_W' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.Flow.winding' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.Win.Z_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.Win.p_eq_q' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.Win.sum_Z_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.Win.sum_Z_eq'' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.Win.x_eq_p' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.Win.sp_abs_le_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.Win.no_gap_dist_three' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.Win.no_three_consecutive' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.Win.x_eq_pairs' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.Win.pairs_eq_q' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.sign_eq_orbCount' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.sign_eq_neg_one_of_odd_orbCount' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.sign_eq_neg_one_of_full_cycle' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.not_full_cycle_of_odd_orbCount' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.next_theta_not_full_cycle' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.orbCount_of_no_fixed' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.winEx' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.winEx_counts' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Base.winEx_x_p' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.q_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.n1_eq_ends' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.succ_mem_Ends' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.image_Doms' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.ends_has_pred' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.chain_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.odd_pair' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.block' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.block_sep' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.Z_eq_one_iff' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Blocks.outer_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.thrHom_eq_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.thr_card_odd' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.n2_eq_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.q_eq_two_n1' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.quot_two_factor_not_cycle' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.IsCovering.eq_of_adj' does not depend on any axioms
'GeneralizedPetersen.Blocks.exists_lift' depends on axioms: [propext]
'GeneralizedPetersen.Blocks.lift_unique' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Blocks.GP_neighbor' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Blocks.exists_nbr_lift' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.quot_inj_on_nbrs' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.GP_isCovering' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.GP3_covering_conditions' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.quot_map_support' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Blocks.quotMap_surjective' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Blocks.exists_lift_winding' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.lift_unique_GP' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.retP_ex' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Blocks.ret_mem' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Blocks.ret_sameThread' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Blocks.ret_inj' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.next3' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.card_Gi_type' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.next3_theta_not_full_cycle' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.next3_pow_val' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.reach' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.sameThread_of_not_dvd' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.next3_ne_self' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.next3_isCycle' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.sign_next3' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Blocks.next3_theta_not_full_cycle_of_not_dvd' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.subtypePerm_pow_val' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.sign_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.sign_transitive' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.card_subtype_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.sign_split3' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.castHom3_eq_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.thr3_next3' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.thr3_trans' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.sign_next3_dvd' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.sign_next3_all' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.next3_theta_not_full_cycle_general' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.exists_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.exists_loop' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.loop_covers' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.exists_loop_covering' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.prev_mem' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Count.prev_inj' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.theta_pow_val' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.reach_prev' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.two_le_card_Gi' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.theta_ne_self' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.theta_isCycle' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.next3_theta_of_Win' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.mem_HamEdges' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.toFinset_map_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.rotE_iterate' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.rotE_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.rotE_pow_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.gp_dvd_numHC' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Count.gp3_dvd_hc' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.cycle_local' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.cycle_local'' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.symm_notMem_darts' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Descent.TwoFactor.p_eq_q' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.TwoFactor.abs_winding_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.TwoFactor.even_winding' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.TwoFactor.winding_cases' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.TwoFactor.exists_win' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.hamTF' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.support_subset_of_closed'' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.exists_oW_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.exists_iW_zero_thread' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.TwoFactor.descend' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.TwoFactor.descend_W_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.win_of_dartInv' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.winBridge_of' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.gp3_dvd_hc'' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.fwd_or_bwd' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.preserves_of_odd_order' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.dartBridge' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.closed_walk_darts' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.WS_eq_flow' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.windingBridge' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.nxt_reach' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.IsHamiltonianCycle.reverse'' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.trace' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.reach_of_nxt' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.cycleBridge' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.gp3_dvd_hc_odd' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Descent.gp3_dvd_hc_odd'' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Small.GP7_hc_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Small.GP9_hc_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Small.GP11_hc_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Small.GP13_hc_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Small.GP15_hc_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Small.card_hamRep' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Small.mem_ext' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Small.nodup_ext' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.Small.cnt_eq_length' depends on axioms: [propext]
'GeneralizedPetersen.Small.hamRep_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Small.hamRep_covers' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Small.adjB7_iff_GP' depends on axioms: [propext]
'GeneralizedPetersen.Small.adjB15_iff_GP' depends on axioms: [propext]
'GeneralizedPetersen.Small.GP15_degree' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Small.num15' depends on axioms: [propext]
'GeneralizedPetersen.Small.s15_1_2' depends on axioms: [propext]
'GeneralizedPetersen.Small.s15_15_27' depends on axioms: [propext]
'GeneralizedPetersen.Small.card_dvd_of_stabilizer_bot' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Small.card_dvd_of_free' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Small.card_dvd_of_free_cyclic' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.Small.card_dvd_of_perm_free' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.GP7_dvd_rot' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.GP9_dvd_rot' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.GP11_dvd_rot' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.GP13_dvd_rot' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.GP15_dvd_rot' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.gp7_dvd_by_rotation' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.gp13_dvd_by_rotation' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.gp15_dvd_by_rotation' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.val_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.dvd_card_of_iterate_free' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.dvd_card_of_family_free' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.L7_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.L13_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.L15_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.ractMem15' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.FreeAction.ractComp15' does not depend on any axioms
'GeneralizedPetersen.FreeAction.ractOrd15' does not depend on any axioms
'GeneralizedPetersen.FreeAction.ractEmask15' depends on axioms: [propext]
'GeneralizedPetersen.FreeAction.ractFree15' depends on axioms: [propext, Quot.sound]
'GeneralizedPetersen.FreeAction.GP7_dvd_any' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.GP13_dvd_any' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.GP15_dvd_any' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.no_rho_fixed13'' depends on axioms: [propext, Classical.choice, Quot.sound]
'GeneralizedPetersen.FreeAction.no_rho_fixed15'' depends on axioms: [propext, Classical.choice, Quot.sound]

