'FRC.Nat.add_left_cancel' does not depend on any axioms
'FRC.Nat.add_right_cancel' does not depend on any axioms
'FRC.Nat.add_sub_cancel' does not depend on any axioms
'FRC.Nat.add_sub_cancel_left' does not depend on any axioms
'FRC.Nat.sub_add_cancel' does not depend on any axioms
'FRC.Nat.sub_add_self_eq_zero' does not depend on any axioms
'FRC.Nat.sub_eq_zero_of_le' does not depend on any axioms
'FRC.Nat.add_sub_of_le' does not depend on any axioms
'FRC.Nat.sub_lt_of_lt_add' does not depend on any axioms
'FRC.Nat.le_of_add_le_add_left' does not depend on any axioms
'FRC.Nat.le_of_add_le_add_right' does not depend on any axioms
'FRC.Nat.sub_le_of_le_add' does not depend on any axioms
'FRC.Nat.le_add_of_sub_le' does not depend on any axioms
'FRC.Nat.le_sub_of_add_le' does not depend on any axioms
'FRC.Nat.succ_ne_zero' does not depend on any axioms
'FRC.Nat.pos_of_lt' does not depend on any axioms
'FRC.Nat.mul_assoc' does not depend on any axioms
'FRC.Nat.add_mul' does not depend on any axioms
'FRC.Nat.add_add_add_comm' does not depend on any axioms
'FRC.Nat.mul_left_comm' does not depend on any axioms
'FRC.Nat.mul_lt_mul_of_lt_of_pos' does not depend on any axioms
'FRC.Nat.modCore_go_fuel' does not depend on any axioms
'FRC.Nat.modCore_eq'' does not depend on any axioms
'FRC.Nat.modCore_eq_mod'' does not depend on any axioms
'FRC.Nat.mod_eq_of_lt' does not depend on any axioms
'FRC.Nat.mod_eq_sub_mod' does not depend on any axioms
'FRC.Nat.mod_spec' does not depend on any axioms
'FRC.Nat.quot_unique' does not depend on any axioms
'FRC.Nat.mod_unique' does not depend on any axioms
'FRC.Nat.mod_mod' does not depend on any axioms
'FRC.Nat.add_mod' does not depend on any axioms
'FRC.Nat.add_mul_mod_self_left' does not depend on any axioms
'FRC.Nat.mul_mod_left'' does not depend on any axioms
'FRC.Nat.mul_mod' does not depend on any axioms
'FRC.Nat.mod_self' does not depend on any axioms
'FRC.Nat.zero_mod' does not depend on any axioms
'FRC.Nat.mod_add_mod' does not depend on any axioms
'FRC.Nat.add_mod_mod' does not depend on any axioms
'FRC.Nat.mod_mul_mod' does not depend on any axioms
'FRC.Nat.mul_mod_mod' does not depend on any axioms
'FRC.Nat.mod_lt'' does not depend on any axioms
'FRC.Nat.pow_succ'' does not depend on any axioms
'FRC.Nat.pow_add' does not depend on any axioms
'FRC.Nat.pow_mul' does not depend on any axioms
'FRC.Nat.pos_pow_of_pos' does not depend on any axioms
'FRC.Nat.isPrime' does not depend on any axioms
'FRC.Nat.isPrime_of_bounded' does not depend on any axioms
'FRC.Pigeonhole.mem' does not depend on any axioms
'FRC.Pigeonhole.decMem' does not depend on any axioms
'FRC.Pigeonhole.NoDup' does not depend on any axioms
'FRC.Pigeonhole.erase' does not depend on any axioms
'FRC.Pigeonhole.length_erase_of_mem' does not depend on any axioms
'FRC.Pigeonhole.mem_of_mem_erase' does not depend on any axioms
'FRC.Pigeonhole.mem_erase_of_ne' does not depend on any axioms
'FRC.Pigeonhole.nodup_erase' does not depend on any axioms
'FRC.Pigeonhole.not_mem_erase_self' does not depend on any axioms
'FRC.Pigeonhole.length_le_of_nodup' does not depend on any axioms
'FRC.Pigeonhole.mem_of_nodup_of_length' does not depend on any axioms
'FRC.Pigeonhole.length_le_of_nodup_lt' does not depend on any axioms
'FRC.Pigeonhole.mem_of_nodup_of_length_lt' does not depend on any axioms
'FRC.Shell.ext' does not depend on any axioms
'FRC.Shell.val_injective' does not depend on any axioms
'FRC.Shell.ofNat' does not depend on any axioms
'FRC.Shell.pow' does not depend on any axioms
'FRC.Shell.hp' does not depend on any axioms
'FRC.Shell.val_ofNat' does not depend on any axioms
'FRC.Shell.val_add' does not depend on any axioms
'FRC.Shell.val_mul' does not depend on any axioms
'FRC.Shell.val_neg' does not depend on any axioms
'FRC.Shell.val_lit' does not depend on any axioms
'FRC.Shell.val_zero' does not depend on any axioms
'FRC.Shell.val_one' does not depend on any axioms
'FRC.Shell.pow_zero' does not depend on any axioms
'FRC.Shell.pow_succ' does not depend on any axioms
'FRC.Shell.ofNat_val' does not depend on any axioms
'FRC.Shell.ofNat_mod' does not depend on any axioms
'FRC.Shell.add_comm' does not depend on any axioms
'FRC.Shell.add_assoc' does not depend on any axioms
'FRC.Shell.zero_add' does not depend on any axioms
'FRC.Shell.add_zero' does not depend on any axioms
'FRC.Shell.add_left_comm' does not depend on any axioms
'FRC.Shell.add_add_add_comm' does not depend on any axioms
'FRC.Shell.mul_comm' does not depend on any axioms
'FRC.Shell.mul_assoc' does not depend on any axioms
'FRC.Shell.one_mul' does not depend on any axioms
'FRC.Shell.mul_one' does not depend on any axioms
'FRC.Shell.zero_mul' does not depend on any axioms
'FRC.Shell.mul_zero' does not depend on any axioms
'FRC.Shell.mul_left_comm' does not depend on any axioms
'FRC.Shell.left_distrib' does not depend on any axioms
'FRC.Shell.right_distrib' does not depend on any axioms
'FRC.Shell.add_neg' does not depend on any axioms
'FRC.Shell.neg_add' does not depend on any axioms
'FRC.Shell.neg_unique' does not depend on any axioms
'FRC.Shell.neg_eq_of_add_eq_zero' does not depend on any axioms
'FRC.Shell.neg_neg' does not depend on any axioms
'FRC.Shell.neg_zero' does not depend on any axioms
'FRC.Shell.neg_mul' does not depend on any axioms
'FRC.Shell.mul_neg' does not depend on any axioms
'FRC.Shell.neg_mul_neg' does not depend on any axioms
'FRC.Shell.neg_add_rev' does not depend on any axioms
'FRC.Shell.add_right_cancel' does not depend on any axioms
'FRC.Shell.eq_neg_of_add_eq_zero' does not depend on any axioms
'FRC.Shell.neg_one_mul' does not depend on any axioms
'FRC.Shell.pow_one' does not depend on any axioms
'FRC.Shell.one_pow' does not depend on any axioms
'FRC.Shell.pow_add' does not depend on any axioms
'FRC.Shell.pow_mul' does not depend on any axioms
'FRC.Shell.pow_mul_comm' does not depend on any axioms
'FRC.Shell.mul_pow' does not depend on any axioms
'FRC.Shell.pow_two' does not depend on any axioms
'FRC.Shell.neg_pow_two' does not depend on any axioms
'FRC.Shell.neg_one_pow' does not depend on any axioms
'FRC.Shell.mul_mul_mul_comm' does not depend on any axioms
'FRC.Shell.decExistsLT' does not depend on any axioms
'FRC.Shell.decForallLT' does not depend on any axioms
'FRC.Shell.sumRange' does not depend on any axioms
'FRC.Shell.sumRange_zero' does not depend on any axioms
'FRC.Shell.sumRange_succ' does not depend on any axioms
'FRC.Shell.sum_congr' does not depend on any axioms
'FRC.Shell.sum_add' does not depend on any axioms
'FRC.Shell.sum_mul_right' does not depend on any axioms
'FRC.Shell.sum_mul_left' does not depend on any axioms
'FRC.Shell.sum_neg' does not depend on any axioms
'FRC.Shell.sum_const' does not depend on any axioms
'FRC.Shell.sum_zero' does not depend on any axioms
'FRC.Shell.sum_eq_single' does not depend on any axioms
'FRC.Shell.geom_sum_mul' does not depend on any axioms
'FRC.Shell.sumRange_succ'' does not depend on any axioms
'FRC.Shell.sumList' does not depend on any axioms
'FRC.Shell.listRange' does not depend on any axioms
'FRC.Shell.imageList' does not depend on any axioms
'FRC.Shell.sumList_imageList' does not depend on any axioms
'FRC.Shell.sumList_erase' does not depend on any axioms
'FRC.Shell.imageList_length' does not depend on any axioms
'FRC.Shell.mem_imageList' does not depend on any axioms
'FRC.Shell.imageList_nodup' does not depend on any axioms
'FRC.Shell.sumList_eq_sumRange' does not depend on any axioms
'FRC.Shell.sum_perm' does not depend on any axioms
'FRC.Shell.prodRange' does not depend on any axioms
'FRC.Shell.prodRange_zero' does not depend on any axioms
'FRC.Shell.prodRange_succ' does not depend on any axioms
'FRC.Shell.prodRange_congr' does not depend on any axioms
'FRC.Shell.prodRange_mul_left' does not depend on any axioms
'FRC.Shell.prodList' does not depend on any axioms
'FRC.Shell.prodList_imageList' does not depend on any axioms
'FRC.Shell.prodList_erase' does not depend on any axioms
'FRC.Shell.prodList_eq_prodRange' does not depend on any axioms
'FRC.Shell.prod_perm' does not depend on any axioms
'FRC.Logic.no_mirror' does not depend on any axioms
'FRC.Cycle.cyc' does not depend on any axioms
'FRC.Cycle.cyc_mod' does not depend on any axioms
'FRC.Cycle.cyc_add_mod' does not depend on any axioms
'FRC.Cycle.cyc_add_n' does not depend on any axioms
'FRC.Cycle.shift_lt' does not depend on any axioms
'FRC.Cycle.no_lower_quot' does not depend on any axioms
'FRC.Cycle.shift_inj' does not depend on any axioms
'FRC.Cycle.sum_shift' does not depend on any axioms
'FRC.Shell.Frame.scale_periodic' does not depend on any axioms
'FRC.Shell.Frame.affineMul' does not depend on any axioms
'FRC.Shell.Frame.affine_frame_unit' does not depend on any axioms
'FRC.Shell.Frame.window_injective' does not depend on any axioms
'FRC.Shell.Frame.ofNat_add' does not depend on any axioms
'FRC.Shell.Frame.ofNat_mul' does not depend on any axioms
'FRC.Shell.Frame.ofNat_self' does not depend on any axioms
'FRC.Shell.Frame.ofNat_add_self' does not depend on any axioms
'FRC.Shell.Frame.window_add_readback' does not depend on any axioms
'FRC.Shell.Frame.window_mul_readback' does not depend on any axioms
'FRC.Shell.Frame.window_signed' does not depend on any axioms
'FRC.Shell.Frame.quarter_turn_exists' does not depend on any axioms
'FRC.Shell.Frame.fourth_roots' does not depend on any axioms
'FRC.Shell.Frame.meridian_involution' does not depend on any axioms
'FRC.Shell.Frame.cmul' does not depend on any axioms
'FRC.Shell.Frame.complex_chart_zero_divisor' does not depend on any axioms
'FRC.Shell.Frame.approx_obstruction' does not depend on any axioms
'FRC.Shell.Frame.natCount' does not depend on any axioms
'FRC.Shell.Frame.natCount_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.root_pair' does not depend on any axioms
'FRC.Shell.Frame.natCount_eq_zero' does not depend on any axioms
'FRC.Shell.Frame.natCount_congr' does not depend on any axioms
'FRC.Shell.Frame.geom_sum_eq_zero' does not depend on any axioms
'FRC.Shell.Frame.ofNat_n' does not depend on any axioms
'FRC.Shell.Frame.principal_root' does not depend on any axioms
'FRC.Shell.Frame.pow_shift_eq_one_iff' does not depend on any axioms
'FRC.Shell.Frame.dft_inverse' does not depend on any axioms
'FRC.Shell.Frame.pow_add_eq_one_iff' does not depend on any axioms
'FRC.Shell.Frame.W_sq' does not depend on any axioms
'FRC.Shell.Frame.rev' does not depend on any axioms
'FRC.Shell.Frame.rev_lt' does not depend on any axioms
'FRC.Shell.Frame.rev_zero' does not depend on any axioms
'FRC.Shell.Frame.rev_of_pos' does not depend on any axioms
'FRC.Shell.Frame.rev_add_mod' does not depend on any axioms
'FRC.Shell.Frame.rev_rev' does not depend on any axioms
'FRC.Shell.Frame.add_mod_eq_zero_iff' does not depend on any axioms
'FRC.Shell.Frame.W' does not depend on any axioms
'FRC.Shell.Frame.J' does not depend on any axioms
'FRC.Shell.Frame.Fmat' does not depend on any axioms
'FRC.Shell.Frame.J_eq' does not depend on any axioms
'FRC.Shell.Frame.W_sq'' does not depend on any axioms
'FRC.Shell.Frame.J_sq' does not depend on any axioms
'FRC.Shell.Frame.F_sq' does not depend on any axioms
'FRC.Shell.Frame.W_J_comm' does not depend on any axioms
'FRC.Shell.Frame.sum_units_eq_sum_pow' does not depend on any axioms
'FRC.Shell.frame13' does not depend on any axioms
'FRC.Shell.Coprime' does not depend on any axioms
'FRC.Shell.Frame.primitive_pow_of_coprime' does not depend on any axioms
'FRC.Shell.Frame.of_primitive' does not depend on any axioms
'FRC.Shell.Frame.generator_orbit' does not depend on any axioms
'FRC.Shell.Frame.fermat' does not depend on any axioms
'FRC.Shell.Frame.klein_orbit_four' does not depend on any axioms
'FRC.Shell.Frame.InOrbit' does not depend on any axioms
'FRC.Shell.Frame.two_mul_eq' does not depend on any axioms
'FRC.Shell.Frame.three_mul_eq' does not depend on any axioms
'FRC.Shell.Frame.four_mul_eq' does not depend on any axioms
'FRC.Shell.Frame.orbit_rep_of_exp' does not depend on any axioms
'FRC.Shell.Frame.exp_not_fourth' does not depend on any axioms
'FRC.Shell.Frame.orbit_rep' does not depend on any axioms
'FRC.Shell.Frame.neg_mul_of_mul_neg' does not depend on any axioms
'FRC.Shell.Frame.inOrbit_symm' does not depend on any axioms
'FRC.Shell.Frame.neg_eq_neg' does not depend on any axioms
'FRC.Shell.Frame.inOrbit_trans' does not depend on any axioms
'FRC.Shell.Frame.orbit_exponent' does not depend on any axioms
'FRC.Shell.Frame.orbit_rep_unique' does not depend on any axioms
'FRC.Shell.Frame.lit_mul' does not depend on any axioms
'FRC.Shell.Frame.add_one_add_one_neg' does not depend on any axioms
'FRC.Shell.Frame.even_capacity_powers' does not depend on any axioms
'FRC.Shell.Frame.octant_residue' does not depend on any axioms
'FRC.Shell.Frame.tsirelson_square' does not depend on any axioms
'FRC.Shell.Frame.two_is_square' does not depend on any axioms
'FRC.Shell.Frame.lit_add' does not depend on any axioms
'FRC.Shell.Frame.neg_one_ne_one' does not depend on any axioms
'FRC.Shell.Frame.neg_one_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.octant_of_two_square' does not depend on any axioms
'FRC.Shell.Frame.even_of_order_eight' does not depend on any axioms
'FRC.Shell.Frame.even_capacity_of_octant' does not depend on any axioms
'FRC.Shell.Frame.octant_iff' does not depend on any axioms
'FRC.Shell.Frame.even_capacity_of_two_square' does not depend on any axioms
'FRC.Shell.Frame.two_is_square_iff' does not depend on any axioms
'FRC.Shell.Frame.dft' does not depend on any axioms
'FRC.Shell.Frame.polyEval' does not depend on any axioms
'FRC.Shell.Frame.dft_eq_polyEval' does not depend on any axioms
'FRC.Shell.Frame.mul_mod_inj' does not depend on any axioms
'FRC.Shell.Frame.dft_covariance' does not depend on any axioms
'FRC.Shell.Frame.Symm' does not depend on any axioms
'FRC.Shell.Frame.Antisymm' does not depend on any axioms
'FRC.Shell.Frame.rev_eq_sub' does not depend on any axioms
'FRC.Shell.Frame.symm_determined' does not depend on any axioms
'FRC.Shell.Frame.symm_extend' does not depend on any axioms
'FRC.Shell.Frame.antisymm_fixed' does not depend on any axioms
'FRC.Shell.Frame.antisymm_determined' does not depend on any axioms
'FRC.Shell.Frame.antisymm_extend' does not depend on any axioms
'FRC.Shell.Frame.symm_antisymm_decomp' does not depend on any axioms
'FRC.Shell.Frame.symm_antisymm_unique' does not depend on any axioms
'FRC.Domain.Lift.mul' does not depend on any axioms
'FRC.Domain.Lift.inv' does not depend on any axioms
'FRC.Domain.Lift.one' does not depend on any axioms
'FRC.Domain.Lift.L' does not depend on any axioms
'FRC.Domain.Lift.T' does not depend on any axioms
'FRC.Domain.Lift.flag' does not depend on any axioms
'FRC.Domain.Lift.speed' does not depend on any axioms
'FRC.Domain.Lift.accel' does not depend on any axioms
'FRC.Domain.Lift.energy' does not depend on any axioms
'FRC.Domain.Lift.hbar' does not depend on any axioms
'FRC.Domain.Lift.kB' does not depend on any axioms
'FRC.Domain.Lift.temp' does not depend on any axioms
'FRC.Domain.Lift.mass' does not depend on any axioms
'FRC.Domain.Lift.force' does not depend on any axioms
'FRC.Domain.Lift.momentum' does not depend on any axioms
'FRC.Domain.Lift.power' does not depend on any axioms
'FRC.Domain.Lift.pressure' does not depend on any axioms
'FRC.Domain.Lift.G' does not depend on any axioms
'FRC.Domain.Lift.unruh' does not depend on any axioms
'FRC.Domain.Lift.classical' does not depend on any axioms
'FRC.Domain.Lift.temp_eq_accel' does not depend on any axioms
'FRC.Domain.Lift.temp_flag_free' does not depend on any axioms
'FRC.Domain.Lift.unruh_closes' does not depend on any axioms
'FRC.Domain.Lift.not_primitive' does not depend on any axioms
'FRC.Domain.Lift.classical_exponents' does not depend on any axioms
'FRC.Domain.Lift.classical_arity' does not depend on any axioms
'FRC.Domain.Lift.reduce' does not depend on any axioms
'FRC.Domain.Lift.modular_shadow' does not depend on any axioms
'FRC.Shell.Frame.Affine.apply' does not depend on any axioms
'FRC.Shell.Frame.Affine.ext'' does not depend on any axioms
'FRC.Shell.Frame.Affine.one' does not depend on any axioms
'FRC.Shell.Frame.Affine.comp' does not depend on any axioms
'FRC.Shell.Frame.Affine.comp_apply' does not depend on any axioms
'FRC.Shell.Frame.Affine.one_apply' does not depend on any axioms
'FRC.Shell.Frame.Affine.comp_assoc' does not depend on any axioms
'FRC.Shell.Frame.Affine.inv' does not depend on any axioms
'FRC.Shell.Frame.Affine.comp_inv' does not depend on any axioms
'FRC.Shell.Frame.Affine.simply_transitive' does not depend on any axioms
'FRC.Shell.Frame.frame_count' does not depend on any axioms
'FRC.Shell.Frame.M2.ext'' does not depend on any axioms
'FRC.Shell.Frame.M2.ext'_a' does not depend on any axioms
'FRC.Shell.Frame.M2.ext'_b' does not depend on any axioms
'FRC.Shell.Frame.M2.ext'_c' does not depend on any axioms
'FRC.Shell.Frame.M2.ext'_d' does not depend on any axioms
'FRC.Shell.Frame.M2.mul' does not depend on any axioms
'FRC.Shell.Frame.M2.smul' does not depend on any axioms
'FRC.Shell.Frame.M2.det' does not depend on any axioms
'FRC.Shell.Frame.M2.act' does not depend on any axioms
'FRC.Shell.Frame.boost' does not depend on any axioms
'FRC.Shell.Frame.borel' does not depend on any axioms
'FRC.Shell.Frame.PEq' does not depend on any axioms
'FRC.Shell.Frame.eq_of_add_neg_eq_zero' does not depend on any axioms
'FRC.Shell.Frame.fld' does not depend on any axioms
'FRC.Shell.Frame.Fld.norm_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.Fld.hopf_section' does not depend on any axioms
'FRC.Shell.Frame.hopf_section' does not depend on any axioms
'FRC.Shell.Frame.Fld.hopf_counts' does not depend on any axioms
'FRC.Shell.Frame.hopf_counts' does not depend on any axioms
'FRC.Shell.Frame.M2.adj' does not depend on any axioms
'FRC.Shell.Frame.M2.mul_adj' does not depend on any axioms
'FRC.Shell.Frame.M2.adj_mul' does not depend on any axioms
'FRC.Shell.Frame.M2.mul_assoc'' does not depend on any axioms
'FRC.Shell.Frame.M2.smul_mul' does not depend on any axioms
'FRC.Shell.Frame.M2.mul_smul' does not depend on any axioms
'FRC.Shell.Frame.M2.diag_mul' does not depend on any axioms
'FRC.Shell.Frame.M2.mul_diag' does not depend on any axioms
'FRC.Shell.Frame.M2.smul_cancel' does not depend on any axioms
'FRC.Shell.Frame.Fld.frame_triple' does not depend on any axioms
'FRC.Shell.Frame.frame_triple' does not depend on any axioms
'FRC.Shell.Frame.unit_split_let' does not depend on any axioms
'FRC.Shell.Frame.unit' does not depend on any axioms
'FRC.Shell.Frame.diag' does not depend on any axioms
'FRC.Shell.Frame.unit_split' does not depend on any axioms
'FRC.Shell.Frame.frame_counts' does not depend on any axioms
'FRC.Shell.Frame.quat' does not depend on any axioms
'FRC.Shell.Frame.sphere_det' does not depend on any axioms
'FRC.Shell.Frame.red1' does not depend on any axioms
'FRC.Shell.Frame.red2' does not depend on any axioms
'FRC.Shell.Frame.frft_aux' does not depend on any axioms
'FRC.Shell.Frame.conv0_aux' does not depend on any axioms
'FRC.Shell.Frame.conv1_aux' does not depend on any axioms
'FRC.Shell.Frame.conv2_aux' does not depend on any axioms
'FRC.Shell.Frame.conv3_aux' does not depend on any axioms
'FRC.Shell.Frame.card00_aux' does not depend on any axioms
'FRC.Shell.Frame.card01_aux' does not depend on any axioms
'FRC.Shell.Frame.card02_aux' does not depend on any axioms
'FRC.Shell.Frame.card03_aux' does not depend on any axioms
'FRC.Shell.Frame.card10_aux' does not depend on any axioms
'FRC.Shell.Frame.card11_aux' does not depend on any axioms
'FRC.Shell.Frame.card12_aux' does not depend on any axioms
'FRC.Shell.Frame.card13_aux' does not depend on any axioms
'FRC.Shell.Frame.card20_aux' does not depend on any axioms
'FRC.Shell.Frame.card21_aux' does not depend on any axioms
'FRC.Shell.Frame.card22_aux' does not depend on any axioms
'FRC.Shell.Frame.card23_aux' does not depend on any axioms
'FRC.Shell.Frame.card30_aux' does not depend on any axioms
'FRC.Shell.Frame.card31_aux' does not depend on any axioms
'FRC.Shell.Frame.card32_aux' does not depend on any axioms
'FRC.Shell.Frame.card33_aux' does not depend on any axioms
'FRC.Shell.Frame.idm' does not depend on any axioms
'FRC.Shell.Frame.FJ' does not depend on any axioms
'FRC.Shell.Frame.comb' does not depend on any axioms
'FRC.Shell.Frame.mm_I_X' does not depend on any axioms
'FRC.Shell.Frame.mm_X_I' does not depend on any axioms
'FRC.Shell.Frame.mm_J_X' does not depend on any axioms
'FRC.Shell.Frame.mm_X_J' does not depend on any axioms
'FRC.Shell.Frame.J_rev_right' does not depend on any axioms
'FRC.Shell.Frame.J_rev_left' does not depend on any axioms
'FRC.Shell.Frame.J_rev_rev' does not depend on any axioms
'FRC.Shell.Frame.F_rev' does not depend on any axioms
'FRC.Shell.Frame.mm_II' does not depend on any axioms
'FRC.Shell.Frame.mm_IF' does not depend on any axioms
'FRC.Shell.Frame.mm_IJ' does not depend on any axioms
'FRC.Shell.Frame.mm_IG' does not depend on any axioms
'FRC.Shell.Frame.mm_FI' does not depend on any axioms
'FRC.Shell.Frame.mm_JI' does not depend on any axioms
'FRC.Shell.Frame.mm_GI' does not depend on any axioms
'FRC.Shell.Frame.mm_FF' does not depend on any axioms
'FRC.Shell.Frame.mm_FJ' does not depend on any axioms
'FRC.Shell.Frame.mm_FG' does not depend on any axioms
'FRC.Shell.Frame.mm_JF' does not depend on any axioms
'FRC.Shell.Frame.mm_JJ' does not depend on any axioms
'FRC.Shell.Frame.mm_JG' does not depend on any axioms
'FRC.Shell.Frame.mm_GF' does not depend on any axioms
'FRC.Shell.Frame.mm_GJ' does not depend on any axioms
'FRC.Shell.Frame.mm_GG' does not depend on any axioms
'FRC.Shell.Frame.comb_mul' does not depend on any axioms
'FRC.Shell.Frame.NF0' does not depend on any axioms
'FRC.Shell.Frame.NF1' does not depend on any axioms
'FRC.Shell.Frame.NF2' does not depend on any axioms
'FRC.Shell.Frame.NF3' does not depend on any axioms
'FRC.Shell.Frame.proj' does not depend on any axioms
'FRC.Shell.Frame.frft' does not depend on any axioms
'FRC.Shell.Frame.mpow' does not depend on any axioms
'FRC.Shell.Frame.hjj' does not depend on any axioms
'FRC.Shell.Frame.hq' does not depend on any axioms
'FRC.Shell.Frame.frft_eq' does not depend on any axioms
'FRC.Shell.Frame.conv0' does not depend on any axioms
'FRC.Shell.Frame.conv1' does not depend on any axioms
'FRC.Shell.Frame.conv2' does not depend on any axioms
'FRC.Shell.Frame.conv3' does not depend on any axioms
'FRC.Shell.Frame.card_one' does not depend on any axioms
'FRC.Shell.Frame.card_i' does not depend on any axioms
'FRC.Shell.Frame.card_m1' does not depend on any axioms
'FRC.Shell.Frame.card_mi' does not depend on any axioms
'FRC.Shell.Frame.inv_pow_kappa' does not depend on any axioms
'FRC.Shell.Frame.inv_pow_n' does not depend on any axioms
'FRC.Shell.Frame.frft_cardinal' does not depend on any axioms
'FRC.Shell.Frame.frft_add' does not depend on any axioms
'FRC.Shell.Frame.frft_period' does not depend on any axioms
'FRC.Shell.Frame.frft_pow' does not depend on any axioms
'FRC.Shell.Frame.scale_shift' does not depend on any axioms
'FRC.Shell.Frame.frft_dilation' does not depend on any axioms
'FRC.Shell.Frame.inv_frame' does not depend on any axioms
'FRC.Shell.Frame.inv_quarter' does not depend on any axioms
'FRC.Shell.Frame.Fmat_conj' does not depend on any axioms
'FRC.Shell.Frame.FJ_conj' does not depend on any axioms
'FRC.Shell.Frame.comb_conj' does not depend on any axioms
'FRC.Shell.Frame.neg_sq_pow' does not depend on any axioms
'FRC.Shell.Frame.cube_pow' does not depend on any axioms
'FRC.Shell.Frame.neg_cube_pow' does not depend on any axioms
'FRC.Shell.Frame.proj_conj' does not depend on any axioms
'FRC.Shell.Frame.orientation' does not depend on any axioms
'FRC.Cycle.pow_mod' does not depend on any axioms
'FRC.Cycle.dft' does not depend on any axioms
'FRC.Cycle.dft_kick' does not depend on any axioms
'FRC.Cycle.dft_shift' does not depend on any axioms
'FRC.Shell.Frame.comb_add_id' does not depend on any axioms
'FRC.Shell.Frame.comb_smul_id' does not depend on any axioms
'FRC.Shell.Frame.comb_zero_id' does not depend on any axioms
'FRC.Shell.Frame.comb_idm_id' does not depend on any axioms
'FRC.Shell.Frame.comb_Fmat_id' does not depend on any axioms
'FRC.Shell.Frame.comb_J_id' does not depend on any axioms
'FRC.Shell.Frame.comb_FJ_id' does not depend on any axioms
'FRC.Shell.Frame.even_sum_id' does not depend on any axioms
'FRC.Shell.Frame.odd_sum_id' does not depend on any axioms
'FRC.Shell.Frame.proj1_c2' does not depend on any axioms
'FRC.Shell.Frame.proj1_c3' does not depend on any axioms
'FRC.Shell.Frame.proj2_c1' does not depend on any axioms
'FRC.Shell.Frame.proj2_c2' does not depend on any axioms
'FRC.Shell.Frame.proj2_c3' does not depend on any axioms
'FRC.Shell.Frame.proj3_c1' does not depend on any axioms
'FRC.Shell.Frame.proj3_c2' does not depend on any axioms
'FRC.Shell.Frame.proj3_c3' does not depend on any axioms
'FRC.Shell.Frame.neg_w_id' does not depend on any axioms
'FRC.Shell.Frame.self_c0' does not depend on any axioms
'FRC.Shell.Frame.self_c1' does not depend on any axioms
'FRC.Shell.Frame.self_c2' does not depend on any axioms
'FRC.Shell.Frame.self_c3' does not depend on any axioms
'FRC.Shell.Frame.ne_c0' does not depend on any axioms
'FRC.Shell.Frame.ne_c1' does not depend on any axioms
'FRC.Shell.Frame.ne_c2' does not depend on any axioms
'FRC.Shell.Frame.ne_c3' does not depend on any axioms
'FRC.Shell.Frame.F_c0' does not depend on any axioms
'FRC.Shell.Frame.F_c1' does not depend on any axioms
'FRC.Shell.Frame.F_c2' does not depend on any axioms
'FRC.Shell.Frame.F_c3' does not depend on any axioms
'FRC.Shell.Frame.sum_c0' does not depend on any axioms
'FRC.Shell.Frame.sum_c1' does not depend on any axioms
'FRC.Shell.Frame.sum_c2' does not depend on any axioms
'FRC.Shell.Frame.sum_c3' does not depend on any axioms
'FRC.Shell.Frame.half_id' does not depend on any axioms
'FRC.Shell.Frame.frft_mul_id' does not depend on any axioms
'FRC.Shell.Frame.entry21_one' does not depend on any axioms
'FRC.Shell.Frame.entry21_three' does not depend on any axioms
'FRC.Shell.Frame.entry00_zero' does not depend on any axioms
'FRC.Shell.Frame.entry00_two' does not depend on any axioms
'FRC.Shell.Frame.row_zero_id' does not depend on any axioms
'FRC.Shell.Frame.comb_add' does not depend on any axioms
'FRC.Shell.Frame.comb_smul' does not depend on any axioms
'FRC.Shell.Frame.comb_zero' does not depend on any axioms
'FRC.Shell.Frame.comb_idm' does not depend on any axioms
'FRC.Shell.Frame.comb_Fmat' does not depend on any axioms
'FRC.Shell.Frame.comb_J' does not depend on any axioms
'FRC.Shell.Frame.comb_FJ' does not depend on any axioms
'FRC.Shell.Frame.pow_two_mul' does not depend on any axioms
'FRC.Shell.Frame.pow_three_mul' does not depend on any axioms
'FRC.Shell.Frame.w_sq' does not depend on any axioms
'FRC.Shell.Frame.w_four' does not depend on any axioms
'FRC.Shell.Frame.u_four' does not depend on any axioms
'FRC.Shell.Frame.w_pow_mod' does not depend on any axioms
'FRC.Shell.Frame.minus_one_ne_one' does not depend on any axioms
'FRC.Shell.Frame.neg_w' does not depend on any axioms
'FRC.Shell.Frame.quarter_eq' does not depend on any axioms
'FRC.Shell.Frame.quarter_pow' does not depend on any axioms
'FRC.Shell.Frame.w_ne_one' does not depend on any axioms
'FRC.Shell.Frame.w_sq_ne_one' does not depend on any axioms
'FRC.Shell.Frame.w_cube_ne_one' does not depend on any axioms
'FRC.Shell.Frame.w_pow_ne_one' does not depend on any axioms
'FRC.Shell.Frame.orth_index' does not depend on any axioms
'FRC.Shell.Frame.geo_zero' does not depend on any axioms
'FRC.Shell.Frame.proj_eq' does not depend on any axioms
'FRC.Shell.Frame.proj_zero_eq' does not depend on any axioms
'FRC.Shell.Frame.proj_one_eq' does not depend on any axioms
'FRC.Shell.Frame.proj_two_eq' does not depend on any axioms
'FRC.Shell.Frame.proj_three_eq' does not depend on any axioms
'FRC.Shell.Frame.proj_mul_pt' does not depend on any axioms
'FRC.Shell.Frame.proj_mul_self' does not depend on any axioms
'FRC.Shell.Frame.proj_mul_ne' does not depend on any axioms
'FRC.Shell.Frame.sum_proj' does not depend on any axioms
'FRC.Shell.Frame.Fmat_proj_pt' does not depend on any axioms
'FRC.Shell.Frame.Fmat_proj' does not depend on any axioms
'FRC.Shell.Frame.proj_even_sum' does not depend on any axioms
'FRC.Shell.Frame.proj_odd_sum' does not depend on any axioms
'FRC.Shell.Frame.half' does not depend on any axioms
'FRC.Shell.Frame.proj_mul' does not depend on any axioms
'FRC.Shell.Frame.frft_mul_pt' does not depend on any axioms
'FRC.Shell.Frame.frft_proj' does not depend on any axioms
'FRC.Shell.Frame.idm_ne' does not depend on any axioms
'FRC.Shell.Frame.idm_self' does not depend on any axioms
'FRC.Shell.Frame.Fmat_zero_row' does not depend on any axioms
'FRC.Shell.Frame.FJ_zero_row' does not depend on any axioms
'FRC.Shell.Frame.J_zero_zero' does not depend on any axioms
'FRC.Shell.Frame.J_zero_row' does not depend on any axioms
'FRC.Shell.Frame.three_lt_n' does not depend on any axioms
'FRC.Shell.Frame.J_two_one' does not depend on any axioms
'FRC.Shell.Frame.hii' does not depend on any axioms
'FRC.Shell.Frame.q_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.half_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.quarter_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.one_add_quarter_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.one_sub_quarter_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.even_proj_entry' does not depend on any axioms
'FRC.Shell.Frame.even_proj_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.odd_proj_entry' does not depend on any axioms
'FRC.Shell.Frame.four_lt_n' does not depend on any axioms
'FRC.Shell.Frame.sq_ne_inv_sq' does not depend on any axioms
'FRC.Shell.Frame.odd_proj_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.frft_injective' does not depend on any axioms
'FRC.Shell.Frame.frame5_two' does not depend on any axioms
'FRC.Shell.Frame.frame5_three' does not depend on any axioms
'FRC.Shell.Frame.five_frames' does not depend on any axioms
'FRC.Shell.Frame.five_odd_proj' does not depend on any axioms
'FRC.Shell.Frame.five_faithful' does not depend on any axioms
'FRC.Shell.Frame.frft_inverse' does not depend on any axioms
'FRC.Shell.Frame.frft_half_turn' does not depend on any axioms
'FRC.Shell.Frame.frft_row_zero' does not depend on any axioms
'FRC.Shell.Frame.double_mod_n' does not depend on any axioms
'FRC.Shell.Frame.frft_row_zero_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.mul_lift_id' does not depend on any axioms
'FRC.Shell.Frame.lift_add_id' does not depend on any axioms
'FRC.Shell.Frame.scaled_id' does not depend on any axioms
'FRC.Shell.Frame.diff_sq_id' does not depend on any axioms
'FRC.Shell.Frame.pow_four_mod' does not depend on any axioms
'FRC.Shell.Frame.quarter_four' does not depend on any axioms
'FRC.Shell.Frame.four_select' does not depend on any axioms
'FRC.Shell.Frame.lift' does not depend on any axioms
'FRC.Shell.Frame.lift_mul_pt' does not depend on any axioms
'FRC.Shell.Frame.lift_proj' does not depend on any axioms
'FRC.Shell.Frame.lift_mul_lift_pt' does not depend on any axioms
'FRC.Shell.Frame.lift_add' does not depend on any axioms
'FRC.Shell.Frame.lift_cardinal' does not depend on any axioms
'FRC.Shell.Frame.lift_pow' does not depend on any axioms
'FRC.Shell.Frame.W_chart' does not depend on any axioms
'FRC.Shell.Frame.W_mul_chart' does not depend on any axioms
'FRC.Shell.Frame.chart_mul_W' does not depend on any axioms
'FRC.Shell.Frame.one_lt_n' does not depend on any axioms
'FRC.Shell.Frame.minus_one_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.chart_noncommute' does not depend on any axioms
'FRC.Shell.Frame.odd_sq_mod_four' does not depend on any axioms
'FRC.Shell.Frame.Fmat_chart' does not depend on any axioms
'FRC.Shell.Frame.trace' does not depend on any axioms
'FRC.Shell.Frame.frame13_six' does not depend on any axioms
'FRC.Shell.Frame.thirteen_tuples' does not depend on any axioms
'FRC.Shell.Frame.sqrt_neg_one' does not depend on any axioms
'FRC.Shell.Frame.scaled_W_sq_iff' does not depend on any axioms
'FRC.Shell.Frame.gauss_pt_id' does not depend on any axioms
'FRC.Shell.Frame.one_add_i_mul' does not depend on any axioms
'FRC.Shell.Frame.conj_sign_id' does not depend on any axioms
'FRC.Shell.Frame.tuple_plus_0' does not depend on any axioms
'FRC.Shell.Frame.tuple_plus_1' does not depend on any axioms
'FRC.Shell.Frame.tuple_plus_2' does not depend on any axioms
'FRC.Shell.Frame.tuple_plus_3' does not depend on any axioms
'FRC.Shell.Frame.tuple_minus_0' does not depend on any axioms
'FRC.Shell.Frame.tuple_minus_1' does not depend on any axioms
'FRC.Shell.Frame.tuple_minus_2' does not depend on any axioms
'FRC.Shell.Frame.tuple_minus_3' does not depend on any axioms
'FRC.Shell.Frame.gauss' does not depend on any axioms
'FRC.Shell.Frame.trace_comb' does not depend on any axioms
'FRC.Shell.Frame.trace_idm' does not depend on any axioms
'FRC.Shell.Frame.trace_Fmat' does not depend on any axioms
'FRC.Shell.Frame.J_diag' does not depend on any axioms
'FRC.Shell.Frame.trace_J' does not depend on any axioms
'FRC.Shell.Frame.W_rev_diag' does not depend on any axioms
'FRC.Shell.Frame.trace_FJ' does not depend on any axioms
'FRC.Shell.Frame.trace_powers' does not depend on any axioms
'FRC.Shell.Frame.trace_proj' does not depend on any axioms
'FRC.Shell.Frame.sum_swap' does not depend on any axioms
'FRC.Shell.Frame.shift_inj' does not depend on any axioms
'FRC.Shell.Frame.gauss_pt' does not depend on any axioms
'FRC.Shell.Frame.gauss_inner' does not depend on any axioms
'FRC.Shell.Frame.gauss_mul' does not depend on any axioms
'FRC.Shell.Frame.gauss_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.gauss_conj' does not depend on any axioms
'FRC.Shell.Frame.sign_sq' does not depend on any axioms
'FRC.Shell.Frame.trace_tuples' does not depend on any axioms
'FRC.Shell.Frame.frame17_three' does not depend on any axioms
'FRC.Shell.Frame.frame29_two' does not depend on any axioms
'FRC.Shell.Frame.frame37_two' does not depend on any axioms
'FRC.Shell.Frame.frame41_six' does not depend on any axioms
'FRC.Shell.Frame.six_signs' does not depend on any axioms
'FRC.Shell.Frame.six_tuples' does not depend on any axioms
'FRC.Shell.Frame.red3' does not depend on any axioms
'FRC.Shell.Frame.rot_eq_id' does not depend on any axioms
'FRC.Shell.Frame.rot_conj_id' does not depend on any axioms
'FRC.Shell.Frame.rot_circle_id' does not depend on any axioms
'FRC.Shell.Frame.rot_mul_c_id' does not depend on any axioms
'FRC.Shell.Frame.rot_mul_d_id' does not depend on any axioms
'FRC.Shell.Frame.card_c_zero' does not depend on any axioms
'FRC.Shell.Frame.card_d_zero' does not depend on any axioms
'FRC.Shell.Frame.card_c_kappa' does not depend on any axioms
'FRC.Shell.Frame.card_d_kappa' does not depend on any axioms
'FRC.Shell.Frame.card_c_two' does not depend on any axioms
'FRC.Shell.Frame.card_d_two' does not depend on any axioms
'FRC.Shell.Frame.card_c_three' does not depend on any axioms
'FRC.Shell.Frame.card_d_three' does not depend on any axioms
'FRC.Shell.Frame.orbit_u_id' does not depend on any axioms
'FRC.Shell.Frame.orbit_v_id' does not depend on any axioms
'FRC.Shell.Frame.surj_c_id' does not depend on any axioms
'FRC.Shell.Frame.surj_d_id' does not depend on any axioms
'FRC.Shell.Frame.norm_id' does not depend on any axioms
'FRC.Shell.Frame.cs' does not depend on any axioms
'FRC.Shell.Frame.ds' does not depend on any axioms
'FRC.Shell.Frame.rot_eq' does not depend on any axioms
'FRC.Shell.Frame.rot_circle' does not depend on any axioms
'FRC.Shell.Frame.rot_hom' does not depend on any axioms
'FRC.Shell.Frame.rot_inj' does not depend on any axioms
'FRC.Shell.Frame.rot_surj' does not depend on any axioms
'FRC.Shell.Frame.rot_cardinal' does not depend on any axioms
'FRC.Shell.Frame.rot_uv' does not depend on any axioms
'FRC.Shell.Frame.orbit_free' does not depend on any axioms
'FRC.Shell.Frame.plane_count' does not depend on any axioms
'FRC.Shell.Frame.countRow' does not depend on any axioms
'FRC.Shell.Frame.countCircle' does not depend on any axioms
'FRC.Shell.Frame.six_circles' does not depend on any axioms
'FRC.Shell.Frame.shift_id' does not depend on any axioms
'FRC.Shell.Frame.modul_id' does not depend on any axioms
'FRC.Shell.Frame.assoc4_id' does not depend on any axioms
'FRC.Shell.Frame.coeff1_id' does not depend on any axioms
'FRC.Shell.Frame.coeff2_id' does not depend on any axioms
'FRC.Shell.Frame.coeff3_id' does not depend on any axioms
'FRC.Shell.Frame.eigenline_a_id' does not depend on any axioms
'FRC.Shell.Frame.eigenline_b_id' does not depend on any axioms
'FRC.Shell.Frame.frft_intertwine' does not depend on any axioms
'FRC.Shell.Frame.rot_eigenline' does not depend on any axioms
'FRC.Shell.Frame.shift' does not depend on any axioms
'FRC.Shell.Frame.shiftInv' does not depend on any axioms
'FRC.Shell.Frame.modul' does not depend on any axioms
'FRC.Shell.Frame.shift_single' does not depend on any axioms
'FRC.Shell.Frame.shiftInv_single' does not depend on any axioms
'FRC.Shell.Frame.modul_left' does not depend on any axioms
'FRC.Shell.Frame.modul_right' does not depend on any axioms
'FRC.Shell.Frame.add_n_mod' does not depend on any axioms
'FRC.Shell.Frame.succ_pred_mod' does not depend on any axioms
'FRC.Shell.Frame.pred_succ_mod' does not depend on any axioms
'FRC.Shell.Frame.pow_succ_mod' does not depend on any axioms
'FRC.Shell.Frame.Fmat_shift' does not depend on any axioms
'FRC.Shell.Frame.pow_mod_succ' does not depend on any axioms
'FRC.Shell.Frame.Fmat_modul' does not depend on any axioms
'FRC.Shell.Frame.ite_iff' does not depend on any axioms
'FRC.Shell.Frame.J_shift' does not depend on any axioms
'FRC.Shell.Frame.shift_inverse' does not depend on any axioms
'FRC.Shell.Frame.pow_rev_mul' does not depend on any axioms
'FRC.Shell.Frame.FJ_shift' does not depend on any axioms
'FRC.Shell.Frame.heisenberg' does not depend on any axioms
'FRC.Shell.Frame.frft_coeff' does not depend on any axioms
'FRC.Shell.Frame.w_eq_pow_kappa' does not depend on any axioms
'FRC.Shell.Frame.act' does not depend on any axioms
'FRC.Shell.Frame.mmul' does not depend on any axioms
'FRC.Shell.Frame.IsEigen' does not depend on any axioms
'FRC.Shell.Frame.act_mmul' does not depend on any axioms
'FRC.Shell.Frame.act_smul' does not depend on any axioms
'FRC.Shell.Frame.act_idm' does not depend on any axioms
'FRC.Shell.Frame.shift_act' does not depend on any axioms
'FRC.Shell.Frame.pow_mod_of_root' does not depend on any axioms
'FRC.Shell.Frame.unit_pow_n' does not depend on any axioms
'FRC.Shell.Frame.shift_eigen' does not depend on any axioms
'FRC.Shell.Frame.shift_eigen_exists' does not depend on any axioms
'FRC.Shell.Frame.four_select'' does not depend on any axioms
'FRC.Shell.Frame.proj_frft_pt' does not depend on any axioms
'FRC.Shell.Frame.proj_frft' does not depend on any axioms
'FRC.Shell.Frame.act_sum_proj' does not depend on any axioms
'FRC.Shell.Frame.four_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.frft_eigen' does not depend on any axioms
'FRC.Shell.Frame.find4' does not depend on any axioms
'FRC.Shell.Frame.find4_lt' does not depend on any axioms
'FRC.Shell.Frame.find4_spec' does not depend on any axioms
'FRC.Shell.Frame.spectral_obstruction' does not depend on any axioms
'FRC.Shell.Frame.quad_diff_id' does not depend on any axioms
'FRC.Shell.Frame.quad_lin_id' does not depend on any axioms
'FRC.Shell.Frame.row_quad_id' does not depend on any axioms
'FRC.Shell.Frame.even_coeff_id' does not depend on any axioms
'FRC.Shell.Frame.odd_coeff_id' does not depend on any axioms
'FRC.Shell.Frame.geom4_id' does not depend on any axioms
'FRC.Shell.Frame.row_comb_id' does not depend on any axioms
'FRC.Shell.Frame.last_row_id' does not depend on any axioms
'FRC.Shell.Frame.col_sum_id' does not depend on any axioms
'FRC.Shell.Frame.quad_roots' does not depend on any axioms
'FRC.Shell.Frame.last_lt' does not depend on any axioms
'FRC.Shell.Frame.last_pos' does not depend on any axioms
'FRC.Shell.Frame.Fmat_last' does not depend on any axioms
'FRC.Shell.Frame.FJ_last' does not depend on any axioms
'FRC.Shell.Frame.J_last' does not depend on any axioms
'FRC.Shell.Frame.sum_idm_col' does not depend on any axioms
'FRC.Shell.Frame.sum_J_col' does not depend on any axioms
'FRC.Shell.Frame.sum_F_col' does not depend on any axioms
'FRC.Shell.Frame.sum_FJ_col' does not depend on any axioms
'FRC.Shell.Frame.frft_col_sum' does not depend on any axioms
'FRC.Shell.Frame.frft_last' does not depend on any axioms
'FRC.Shell.Frame.succ_mod_zero' does not depend on any axioms
'FRC.Shell.Frame.row_shift' does not depend on any axioms
'FRC.Shell.Frame.row_entry' does not depend on any axioms
'FRC.Shell.Frame.three_kappa_lt' does not depend on any axioms
'FRC.Shell.Frame.kappa_lt_n' does not depend on any axioms
'FRC.Shell.Frame.even_coeff_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.quad_mod_n' does not depend on any axioms
'FRC.Shell.Frame.pow_sub_eq' does not depend on any axioms
'FRC.Shell.Frame.odd_coeff_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.exclusivity' does not depend on any axioms
'FRC.Extension.Ext.fixed_conj' does not depend on any axioms
'FRC.Shell.Frame.Quat.mul' does not depend on any axioms
'FRC.Shell.Frame.Quat.conj' does not depend on any axioms
'FRC.Shell.Frame.Quat.nrm' does not depend on any axioms
'FRC.Shell.Frame.Quat.vec' does not depend on any axioms
'FRC.Shell.Frame.Quat.sc' does not depend on any axioms
'FRC.Shell.Frame.Quat.smul' does not depend on any axioms
'FRC.Shell.Frame.Quat.add' does not depend on any axioms
'FRC.Shell.Frame.Quat.neg' does not depend on any axioms
'FRC.Shell.Frame.Quat.cross' does not depend on any axioms
'FRC.Shell.Frame.Quat.dot' does not depend on any axioms
'FRC.Shell.Frame.Quat.conjBy' does not depend on any axioms
'FRC.Shell.Frame.Quat.ext4' does not depend on any axioms
'FRC.Shell.Frame.Quat.pure_eq' does not depend on any axioms
'FRC.Shell.Frame.QR.eval' does not depend on any axioms
'FRC.Shell.Frame.QR.mul' does not depend on any axioms
'FRC.Shell.Frame.QR.conj' does not depend on any axioms
'FRC.Shell.Frame.QR.nrm' does not depend on any axioms
'FRC.Shell.Frame.QR.vec' does not depend on any axioms
'FRC.Shell.Frame.QR.sc' does not depend on any axioms
'FRC.Shell.Frame.QR.smul' does not depend on any axioms
'FRC.Shell.Frame.QR.add' does not depend on any axioms
'FRC.Shell.Frame.QR.neg' does not depend on any axioms
'FRC.Shell.Frame.QR.cross' does not depend on any axioms
'FRC.Shell.Frame.QR.dot' does not depend on any axioms
'FRC.Shell.Frame.QR.conjBy' does not depend on any axioms
'FRC.Shell.Frame.QR.v' does not depend on any axioms
'FRC.Shell.Frame.QR.pv' does not depend on any axioms
'FRC.Shell.Frame.QR.check' does not depend on any axioms
'FRC.Shell.Frame.QR.sound' does not depend on any axioms
'FRC.Shell.Frame.nrm_mul' does not depend on any axioms
'FRC.Shell.Frame.IsSquare' does not depend on any axioms
'FRC.Shell.Frame.no_causal_root' does not depend on any axioms
'FRC.Shell.Frame.sq_mul' does not depend on any axioms
'FRC.Shell.Frame.neg_sq_is_square' does not depend on any axioms
'FRC.Shell.Frame.neg_one_is_square' does not depend on any axioms
'FRC.Shell.Frame.absorb' does not depend on any axioms
'FRC.Shell.Frame.Q2' does not depend on any axioms
'FRC.Shell.Frame.aniso_tx' does not depend on any axioms
'FRC.Shell.Frame.null_yz' does not depend on any axioms
'FRC.Shell.Frame.null_tx_of_square' does not depend on any axioms
'FRC.Shell.Frame.sq_add' does not depend on any axioms
'FRC.Shell.Frame.regroup' does not depend on any axioms
'FRC.Shell.Frame.norm_mul' does not depend on any axioms
'FRC.Shell.Frame.boostT' does not depend on any axioms
'FRC.Shell.Frame.boostX' does not depend on any axioms
'FRC.Shell.Frame.boost_preserves' does not depend on any axioms
'FRC.Shell.Frame.boost_comp_t' does not depend on any axioms
'FRC.Shell.Frame.boost_comp_x' does not depend on any axioms
'FRC.Shell.Frame.norm_one_mul' does not depend on any axioms
'FRC.Shell.Frame.gamma_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.gamma_velocity' does not depend on any axioms
'FRC.Shell.Frame.velocity_addition' does not depend on any axioms
'FRC.Shell.Frame.sumTo' does not depend on any axioms
'FRC.Shell.Frame.nullCount' does not depend on any axioms
'FRC.Shell.Frame.normOneCount' does not depend on any axioms
'FRC.Shell.Frame.null13' does not depend on any axioms
'FRC.Shell.Frame.euclid13' does not depend on any axioms
'FRC.Shell.Frame.null5' does not depend on any axioms
'FRC.Shell.Frame.null17' does not depend on any axioms
'FRC.Shell.Frame.normOne_values' does not depend on any axioms
'FRC.Extension.lit_add' does not depend on any axioms
'FRC.Extension.two_eq' does not depend on any axioms
'FRC.Extension.ext_add_comm' does not depend on any axioms
'FRC.Extension.ext_mul_add' does not depend on any axioms
'FRC.Extension.ext_conj_one' does not depend on any axioms
'FRC.Extension.ext_tally_line' does not depend on any axioms
'FRC.Extension.ext_conj_pow' does not depend on any axioms
'FRC.Extension.ext_mul_pow' does not depend on any axioms
'FRC.Extension.ext_ofShell_pow' does not depend on any axioms
'FRC.Extension.ext_trace_add' does not depend on any axioms
'FRC.Extension.ext_trace_smul' does not depend on any axioms
'FRC.Extension.ext_cayley_hamilton' does not depend on any axioms
'FRC.Extension.two_way_tally' does not depend on any axioms
'FRC.Extension.Wp' does not depend on any axioms
'FRC.Extension.core_weights' does not depend on any axioms
'FRC.Extension.root_two_two_way' does not depend on any axioms
'FRC.Extension.conjugate_pair_tally' does not depend on any axioms
'FRC.Extension.trace_recurrence' does not depend on any axioms
'FRC.Extension.geom_sum_zero' does not depend on any axioms
'FRC.Extension.dial_shift' does not depend on any axioms
'FRC.Extension.dial_tally' does not depend on any axioms
'FRC.Extension.gridPoint' does not depend on any axioms
'FRC.Extension.nth' does not depend on any axioms
'FRC.Extension.remainderRank' does not depend on any axioms
'FRC.Extension.largestRemainder' does not depend on any axioms
'FRC.Extension.framed_readout' does not depend on any axioms
'FRC.Extension.Tally.GI.add' does not depend on any axioms
'FRC.Extension.Tally.GI.mul' does not depend on any axioms
'FRC.Extension.Tally.GI.conj' does not depend on any axioms
'FRC.Extension.Tally.GI.smul' does not depend on any axioms
'FRC.Extension.Tally.GI.zero' does not depend on any axioms
'FRC.Extension.Tally.GI.i' does not depend on any axioms
'FRC.Extension.Tally.GI.ipow' does not depend on any axioms
'FRC.Extension.Tally.GI.tally' does not depend on any axioms
'FRC.Extension.Tally.sum4' does not depend on any axioms
'FRC.Extension.Tally.eta' does not depend on any axioms
'FRC.Extension.Tally.kernel' does not depend on any axioms
'FRC.Extension.Tally.psi' does not depend on any axioms
'FRC.Extension.Tally.F' does not depend on any axioms
'FRC.Extension.Tally.coeff' does not depend on any axioms
'FRC.Extension.Tally.inversion' does not depend on any axioms
'FRC.Extension.Tally.responses' does not depend on any axioms
'FRC.Extension.Tally.support' does not depend on any axioms
'FRC.Extension.Tally.winding_fixing' does not depend on any axioms
'FRC.Extension.Tally.tally_criterion' does not depend on any axioms
'FRC.Extension.Tally.two_way' does not depend on any axioms
'FRC.Extension.Tally.fourier_inversion' does not depend on any axioms
'FRC.Extension.Tally.channel_selectivity' does not depend on any axioms
'FRC.Extension.Tally.dft_det' does not depend on any axioms
'FRC.Extension.Tally.B' does not depend on any axioms
'FRC.Extension.Tally.fibreNorm' does not depend on any axioms
'FRC.Extension.Tally.kout' does not depend on any axioms
'FRC.Extension.Tally.psiA' does not depend on any axioms
'FRC.Extension.Tally.psiB' does not depend on any axioms
'FRC.Extension.Tally.cone_boundary' does not depend on any axioms
'FRC.Extension.Tally.linear_exclusion' does not depend on any axioms
'FRC.Shell.Poly.Frame.root_bound' does not depend on any axioms
'FRC.Shell.Poly.Frame.xpx_bound' does not depend on any axioms
'FRC.Shell.Poly.Frame.xpx_p' does not depend on any axioms
'FRC.Shell.Poly.Frame.eval_xpx' does not depend on any axioms
'FRC.Shell.Poly.Frame.CommonFactor' does not depend on any axioms
'FRC.Shell.Poly.Frame.root_iff_common_factor' does not depend on any axioms
'FRC.Logic.mx' does not depend on any axioms
'FRC.Logic.le_mx_left' does not depend on any axioms
'FRC.Logic.le_mx_right' does not depend on any axioms
'FRC.Logic.lt_of_mx_lt_left' does not depend on any axioms
'FRC.Logic.lt_of_mx_lt_right' does not depend on any axioms
'FRC.Logic.cons' does not depend on any axioms
'FRC.Logic.evalT' does not depend on any axioms
'FRC.Logic.allBelow' does not depend on any axioms
'FRC.Logic.evalF' does not depend on any axioms
'FRC.Logic.evalT' does not depend on any axioms
'FRC.Logic.evalF' does not depend on any axioms
'FRC.Logic.boundT' does not depend on any axioms
'FRC.Logic.maxBelow' does not depend on any axioms
'FRC.Logic.boundF' does not depend on any axioms
'FRC.Logic.le_maxBelow' does not depend on any axioms
'FRC.Logic.allBelow_congr' does not depend on any axioms
'FRC.Logic.evalT_frame' does not depend on any axioms
'FRC.Logic.stable' does not depend on any axioms
'FRC.Logic.records' does not depend on any axioms
'FRC.Logic.records_lt' does not depend on any axioms
'FRC.Logic.iter' does not depend on any axioms
'FRC.Logic.iter_lt' does not depend on any axioms
'FRC.Logic.iter_add' does not depend on any axioms
'FRC.Logic.repeat_below' does not depend on any axioms
'FRC.Logic.sub_pos' does not depend on any axioms
'FRC.Logic.eventually_periodic' does not depend on any axioms
'FRC.Logic.halts_iff_halts_below' does not depend on any axioms
'FRC.Logic.cantor_finite' does not depend on any axioms
'FRC.Logic.leastBelow' does not depend on any axioms
'FRC.Logic.leastBelow_some' does not depend on any axioms
'FRC.Logic.leastBelow_spec' does not depend on any axioms
'FRC.Logic.leastBelow_congr' does not depend on any axioms
'FRC.Logic.or_intro_left' does not depend on any axioms
'FRC.Logic.or_intro_right' does not depend on any axioms
'FRC.Logic.and_true'' does not depend on any axioms
'FRC.Logic.and_false'' does not depend on any axioms
'FRC.Logic.and_self'' does not depend on any axioms
'FRC.Logic.or_false'' does not depend on any axioms
'FRC.Logic.and_assoc'' does not depend on any axioms
'FRC.Logic.inj_onto' does not depend on any axioms
'FRC.Logic.no_finite_successor' does not depend on any axioms
'FRC.Logic.part_collides' does not depend on any axioms
'FRC.Logic.sentences_outnumber' does not depend on any axioms
'FRC.Logic.count' does not depend on any axioms
'FRC.Logic.count_full' does not depend on any axioms
'FRC.Logic.cond_or_le' does not depend on any axioms
'FRC.Logic.count_or_le' does not depend on any axioms
'FRC.Logic.count_shift' does not depend on any axioms
'FRC.Logic.count_false' does not depend on any axioms
'FRC.Logic.count_single' does not depend on any axioms
'FRC.Logic.count_shift_by' does not depend on any axioms
'FRC.Logic.dense_coding' does not depend on any axioms
'FRC.Logic.pow_lt_pow_base' does not depend on any axioms
'FRC.Logic.digit_bound' does not depend on any axioms
'FRC.Logic.anyBelow' does not depend on any axioms
'FRC.Logic.anyBelow_congr' does not depend on any axioms
'FRC.Logic.anyBelow_false' does not depend on any axioms
'FRC.Logic.allBelow_const' does not depend on any axioms
'FRC.Logic.anyBelow_and_const' does not depend on any axioms
'FRC.Logic.allBelow_and_const' does not depend on any axioms
'FRC.Logic.anyBelow_pick' does not depend on any axioms
'FRC.Logic.Sat' does not depend on any axioms
'FRC.Logic.fval' does not depend on any axioms
'FRC.Logic.allBelow_iff' does not depend on any axioms
'FRC.Logic.fin_theory_decidable' does not depend on any axioms
'FRC.Logic.fin_theory_complete' does not depend on any axioms
'FRC.Logic.fin_theory_consistent' does not depend on any axioms
'FRC.Logic.succOf' does not depend on any axioms
'FRC.Logic.band_l' does not depend on any axioms
'FRC.Logic.band_r' does not depend on any axioms
'FRC.Logic.no_finite_Q' does not depend on any axioms
'FRC.Logic.no_interpretation' does not depend on any axioms
'FRC.Logic.memBit' does not depend on any axioms
'FRC.Logic.tupleIndex' does not depend on any axioms
'FRC.Logic.Sat2' does not depend on any axioms
'FRC.Logic.sval2' does not depend on any axioms
'FRC.Logic.so_theory_decidable' does not depend on any axioms
'FRC.Logic.so_theory_complete' does not depend on any axioms
'FRC.Logic.so_theory_consistent' does not depend on any axioms
'FRC.Logic.so_evaluation_terminates' does not depend on any axioms
'FRC.Formation.Universe.Closed' does not depend on any axioms
'FRC.Formation.Passes' does not depend on any axioms
'FRC.Formation.minimal' does not depend on any axioms
'FRC.Formation.minimal_size' does not depend on any axioms
'FRC.Formation.atoms_functional' does not depend on any axioms
'FRC.Formation.realized' does not depend on any axioms
'FRC.Formation.minimal_closed' does not depend on any axioms
'FRC.Formation.pad' does not depend on any axioms
'FRC.Formation.pad_size' does not depend on any axioms
'FRC.Formation.pad_form' does not depend on any axioms
'FRC.Formation.passes_pad' does not depend on any axioms
'FRC.Formation.realization_at_size' does not depend on any axioms
'FRC.Formation.cyc' does not depend on any axioms
'FRC.Formation.cyc_lt' does not depend on any axioms
'FRC.Formation.cyc_iter' does not depend on any axioms
'FRC.Formation.cyc_return' does not depend on any axioms
'FRC.Formation.cyc_inj' does not depend on any axioms
'FRC.Formation.cyc_onto' does not depend on any axioms
'FRC.Formation.double' does not depend on any axioms
'FRC.Formation.swap' does not depend on any axioms
'FRC.Formation.swap_lt' does not depend on any axioms
'FRC.Formation.swap_swap' does not depend on any axioms
'FRC.Formation.swap_ne' does not depend on any axioms
'FRC.Formation.double_form_left' does not depend on any axioms
'FRC.Formation.double_form_right' does not depend on any axioms
'FRC.Formation.double_form_right'' does not depend on any axioms
'FRC.Formation.swap_form' does not depend on any axioms
'FRC.Formation.passes_double' does not depend on any axioms
'FRC.Formation.count_add' does not depend on any axioms
'FRC.Formation.count_congr' does not depend on any axioms
'FRC.Formation.invariant_count_even' does not depend on any axioms
'FRC.Formation.no_unique_invariant' does not depend on any axioms
'FRC.Formation.no_preimage_in_minimal' does not depend on any axioms
'FRC.Formation.finite_induction' does not depend on any axioms
'FRC.Formation.buffer' does not depend on any axioms
'FRC.Formation.buffer_size' does not depend on any axioms
'FRC.Formation.buffer_forms' does not depend on any axioms
'FRC.Formation.buffer_fresh' does not depend on any axioms
'FRC.Formation.chain' does not depend on any axioms
'FRC.Formation.chain_level' does not depend on any axioms
'FRC.Formation.illusion' does not depend on any axioms
'FRC.Formation.illusion_instance' does not depend on any axioms
'FRC.Formation.decPasses' does not depend on any axioms
'FRC.Formation.rowList' does not depend on any axioms
'FRC.Formation.length_append' does not depend on any axioms
'FRC.Formation.rowList_length' does not depend on any axioms
'FRC.Formation.record' does not depend on any axioms
'FRC.Formation.record_length' does not depend on any axioms
'FRC.Formation.record_square' does not depend on any axioms
'FRC.Nat.mod_eq_zero_of_add' does not depend on any axioms
'FRC.Nat.mul_mod_eq_zero_left' does not depend on any axioms
'FRC.Nat.prime_not_dvd_mul_aux' does not depend on any axioms
'FRC.Nat.prime_mul_mod' does not depend on any axioms
'FRC.Nat.dvd_iff_mod' does not depend on any axioms
'FRC.Nat.mod_two_cases' does not depend on any axioms
'FRC.Nat.succ_lt_of_lt_pred' does not depend on any axioms
'FRC.Nat.pred_lt_pred' does not depend on any axioms
'FRC.Nat.eq_of_pred_eq' does not depend on any axioms
'FRC.Nat.parity_split' does not depend on any axioms
'FRC.Shell.Poly.xn1' does not depend on any axioms
'FRC.Shell.Poly.xn1_bound' does not depend on any axioms
'FRC.Shell.Poly.xn1_top' does not depend on any axioms
'FRC.Shell.Poly.eval_xn1' does not depend on any axioms
'FRC.Shell.Prime.one_lt' does not depend on any axioms
'FRC.Shell.Prime.one_ne_zero' does not depend on any axioms
'FRC.Shell.Prime.eq_zero_of_val_mod' does not depend on any axioms
'FRC.Shell.Prime.mul_eq_zero' does not depend on any axioms
'FRC.Shell.Prime.mul_ne_zero' does not depend on any axioms
'FRC.Shell.Prime.eq_of_sub_eq_zero' does not depend on any axioms
'FRC.Shell.Prime.mul_left_cancel' does not depend on any axioms
'FRC.Shell.Prime.sq_eq_sq' does not depend on any axioms
'FRC.Shell.Prime.sq_eq_one' does not depend on any axioms
'FRC.Shell.Prime.val_pos' does not depend on any axioms
'FRC.Shell.Prime.ofNat_ne_zero' does not depend on any axioms
'FRC.Shell.Prime.prodRange_ne_zero' does not depend on any axioms
'FRC.Shell.Prime.nonzero' does not depend on any axioms
'FRC.Shell.Prime.nonzeroIndex' does not depend on any axioms
'FRC.Shell.Prime.nonzero_ne_zero' does not depend on any axioms
'FRC.Shell.Prime.fermat' does not depend on any axioms
'FRC.Shell.Prime.two_le' does not depend on any axioms
'FRC.Shell.Prime.neg_one_ne_one' does not depend on any axioms
'FRC.Shell.Prime.ne_zero_of_mul_self' does not depend on any axioms
'FRC.Shell.Prime.neg_one_ne_zero' does not depend on any axioms
'FRC.Shell.Prime.exists_pow_ne_one' does not depend on any axioms
'FRC.Shell.Prime.exists_pow_half' does not depend on any axioms
'FRC.Shell.Prime.exists_quarter_turn' does not depend on any axioms
'FRC.Shell.Prime.ofNat_mul' does not depend on any axioms
'FRC.Shell.Prime.ofNat_self' does not depend on any axioms
'FRC.Shell.Prime.isPrime_of_no_zero_divisors' does not depend on any axioms
'FRC.Shell.Prime.chart_gt_two' does not depend on any axioms
'FRC.Shell.Prime.two_eq' does not depend on any axioms
'FRC.Shell.Prime.add_one_add_one_neg' does not depend on any axioms
'FRC.Shell.Prime.octant_sector' does not depend on any axioms
'FRC.Shell.Prime.tsirelson' does not depend on any axioms
'FRC.Shell.Prime.two_mul_chart_half' does not depend on any axioms
'FRC.Shell.Prime.half_square_iff' does not depend on any axioms
'FRC.Shell.Prime.parity_flips' does not depend on any axioms
'FRC.Shell.Prime.isPrime_iff_complete' does not depend on any axioms
'FRC.Shell.Prime.pow_mod_eq_one' does not depend on any axioms
'FRC.Shell.Prime.quarter_turn_iff' does not depend on any axioms
'FRC.Shell.Prime.isPrime_iff_no_zero_divisors' does not depend on any axioms
'FRC.Foundation.succIter' does not depend on any axioms
'FRC.Foundation.ofNat_add' does not depend on any axioms
'FRC.Foundation.succIter_eq' does not depend on any axioms
'FRC.Foundation.ofNat_eq_zero_iff' does not depend on any axioms
'FRC.Foundation.add_eq_self_iff' does not depend on any axioms
'FRC.Foundation.successor_cycle' does not depend on any axioms
'FRC.Foundation.observer_part' does not depend on any axioms
'FRC.Foundation.Registered' does not depend on any axioms
'FRC.Foundation.Registered.lt' does not depend on any axioms
'FRC.Foundation.register' does not depend on any axioms
'FRC.Foundation.registered_finite' does not depend on any axioms
'FRC.Foundation.no_unlimited_supply' does not depend on any axioms
'FRC.Foundation.registration_onto' does not depend on any axioms
'FRC.Foundation.complete_needs_whole' does not depend on any axioms
'FRC.Foundation.agent_bound' does not depend on any axioms
'FRC.Foundation.mutual_registration_count' does not depend on any axioms
'FRC.Foundation.translation_torsor' does not depend on any axioms
'FRC.Nat.dvd_trans'' does not depend on any axioms
'FRC.Nat.pos_of_dvd' does not depend on any axioms
'FRC.Nat.le_of_dvd'' does not depend on any axioms
'FRC.Nat.eq_one_of_mul_eq_one' does not depend on any axioms
'FRC.Nat.exists_least' does not depend on any axioms
'FRC.Nat.exists_prime_dvd' does not depend on any axioms
'FRC.Nat.exists_pow_mul' does not depend on any axioms
'FRC.Nat.dvd_prime_pow' does not depend on any axioms
'FRC.Shell.Prime.HasOrder' does not depend on any axioms
'FRC.Shell.Prime.pow_ne_zero' does not depend on any axioms
'FRC.Shell.Prime.exists_order' does not depend on any axioms
'FRC.Shell.Prime.pow_eq_one_of_dvd' does not depend on any axioms
'FRC.Shell.Prime.dvd_of_pow_eq_one' does not depend on any axioms
'FRC.Shell.Prime.eq_one_of_pows' does not depend on any axioms
'FRC.Shell.Prime.hasOrder_mul' does not depend on any axioms
'FRC.Shell.Prime.exists_order_prime_pow' does not depend on any axioms
'FRC.Shell.Prime.exists_order_of_dvd' does not depend on any axioms
'FRC.Shell.Prime.exists_primitive' does not depend on any axioms
'FRC.Shell.Prime.primitive_pow_inj' does not depend on any axioms
'FRC.Shell.Prime.exists_drive' does not depend on any axioms
'FRC.Carrier.mod_of_eq' does not depend on any axioms
'FRC.Carrier.mod12_table' does not depend on any axioms
'FRC.Carrier.substrate_arith' does not depend on any axioms
'FRC.Carrier.mod12_table'' does not depend on any axioms
'FRC.Carrier.mod12_iff' does not depend on any axioms
'FRC.Carrier.cube_identity' does not depend on any axioms
'FRC.Carrier.three_ne_zero' does not depend on any axioms
'FRC.Carrier.triality_iff' does not depend on any axioms
'FRC.Carrier.substrate_shell' does not depend on any axioms
'FRC.Carrier.substrate_residue' does not depend on any axioms
'FRC.Carrier.grav' does not depend on any axioms
'FRC.Carrier.csq' does not depend on any axioms
'FRC.Carrier.two_mul_half' does not depend on any axioms
'FRC.Carrier.grav_eq' does not depend on any axioms
'FRC.Carrier.two_ne_zero' does not depend on any axioms
'FRC.Carrier.kB_sq' does not depend on any axioms
'FRC.Carrier.partner' does not depend on any axioms
'FRC.Carrier.c_exists_iff' does not depend on any axioms
'FRC.Carrier.register' does not depend on any axioms
'FRC.Carrier.lt_of_mul_self_lt' does not depend on any axioms
'FRC.Carrier.nested_windows' does not depend on any axioms
'FRC.Carrier.saturated_windows' does not depend on any axioms
'FRC.Carrier.nesting' does not depend on any axioms
'FRC.Carrier.lab_ladder' does not depend on any axioms
'FRC.Carrier.window_ladder' does not depend on any axioms
'FRC.Carrier.square_pair_blind' does not depend on any axioms
'FRC.Carrier.sign_sector' does not depend on any axioms
'FRC.Carrier.octant' does not depend on any axioms
'FRC.Carrier.chart_gt_two' does not depend on any axioms
'FRC.Carrier.two_eq' does not depend on any axioms
'FRC.Carrier.add_one_add_one_neg' does not depend on any axioms
'FRC.Carrier.octant_sector' does not depend on any axioms
'FRC.Carrier.tsirelson' does not depend on any axioms
'FRC.Carrier.parity_flips' does not depend on any axioms
'FRC.Subject.frame_isPrime' does not depend on any axioms
'FRC.Subject.inv' does not depend on any axioms
'FRC.Subject.mul_inv' does not depend on any axioms
'FRC.Subject.inv_ne_zero' does not depend on any axioms
'FRC.Subject.even_add' does not depend on any axioms
'FRC.Subject.frame_web' does not depend on any axioms
'FRC.Subject.signature' does not depend on any axioms
'FRC.Subject.square_class' does not depend on any axioms
'FRC.Subject.half_class' does not depend on any axioms
'FRC.Subject.channel' does not depend on any axioms
'FRC.Subject.channel_233' does not depend on any axioms
'FRC.Subject.exponent_ladder' does not depend on any axioms
'FRC.Subject.parity_ne' does not depend on any axioms
'FRC.Subject.quarter_turn_odd' does not depend on any axioms
'FRC.Subject.qr4' does not depend on any axioms
'FRC.Subject.qr4_spec' does not depend on any axioms
'FRC.Subject.fold_eq' does not depend on any axioms
'FRC.Subject.pow_ne_zero' does not depend on any axioms
'FRC.Subject.quarter_pow_inj' does not depend on any axioms
'FRC.Subject.spinor' does not depend on any axioms
'FRC.Subject.no_iso' does not depend on any axioms
'FRC.Subject.pow_dvd_odd' does not depend on any axioms
'FRC.Subject.two_part' does not depend on any axioms
'FRC.Subject.dir' does not depend on any axioms
'FRC.Subject.ratio' does not depend on any axioms
'FRC.Subject.ext_mul4' does not depend on any axioms
'FRC.Subject.ratio_ofShell' does not depend on any axioms
'FRC.Subject.ratio_mul' does not depend on any axioms
'FRC.Subject.ratio_scale' does not depend on any axioms
'FRC.Subject.norm_ratio' does not depend on any axioms
'FRC.Subject.nonsquare_ne_zero' does not depend on any axioms
'FRC.Subject.horizon_antipode' does not depend on any axioms
'FRC.Subject.horizon_generator' does not depend on any axioms
'FRC.Subject.boost_unique' does not depend on any axioms
'FRC.Pair.tower_solvable' does not depend on any axioms
'FRC.Pair.window' does not depend on any axioms
'FRC.Pair.window_sum' does not depend on any axioms
'FRC.Pair.leak_rate' does not depend on any axioms
'FRC.Pair.mod_mul_self' does not depend on any axioms
'FRC.Pair.joint_cycle' does not depend on any axioms
'FRC.Pair.joint_cycle_frame' does not depend on any axioms
'FRC.Pair.joint_return_iff' does not depend on any axioms
'FRC.Pair.joint_return_eight' does not depend on any axioms
'FRC.Pair.tick' does not depend on any axioms
'FRC.Pair.tick_home' does not depend on any axioms
'FRC.Pair.tick_half' does not depend on any axioms
'FRC.Pair.half_turn' does not depend on any axioms
'FRC.Pair.reflection_identity' does not depend on any axioms
'FRC.Pair.mu' does not depend on any axioms
'FRC.Pair.mu_mod' does not depend on any axioms
'FRC.Pair.parity_table' does not depend on any axioms
'FRC.Pair.odd_sum_residue' does not depend on any axioms
'FRC.Pair.covering_parity' does not depend on any axioms
'FRC.Pair.count' does not depend on any axioms
'FRC.Pair.pair_frame' does not depend on any axioms
'FRC.Pair.pair_register' does not depend on any axioms
'FRC.Pair.channel_instance' does not depend on any axioms
'FRC.Pair.carrier_frame' does not depend on any axioms
'FRC.Pair.carrier_roots' does not depend on any axioms
'FRC.Pair.half_instance' does not depend on any axioms
'FRC.Pair.window_instance' does not depend on any axioms
'FRC.Pair.label' does not depend on any axioms
'FRC.Pair.node_field' does not depend on any axioms
'FRC.Pair.mounting' does not depend on any axioms
'FRC.Pair.sky_chronon' does not depend on any axioms
'FRC.Pair.recurrence' does not depend on any axioms
'FRC.Pair.frame_leak' does not depend on any axioms
'FRC.Pair.flow_stations' does not depend on any axioms
'FRC.Pair.ownership' does not depend on any axioms
'FRC.Pair.half_turn_instance' does not depend on any axioms
'FRC.Pair.kill_test' does not depend on any axioms
'FRC.Pair.two_faces' does not depend on any axioms
'FRC.Pair.tent' does not depend on any axioms
'FRC.Pair.sheet' does not depend on any axioms
'FRC.Pair.shellOf' does not depend on any axioms
'FRC.Pair.isParam' does not depend on any axioms
'FRC.Pair.mult' does not depend on any axioms
'FRC.Pair.stations' does not depend on any axioms
'FRC.Pair.step_law' does not depend on any axioms
'FRC.Pair.tower_period' does not depend on any axioms
'FRC.Pair.quarter_classes' does not depend on any axioms
'FRC.Pair.momentum_dual' does not depend on any axioms
'FRC.Pair.covering_instance' does not depend on any axioms
'FRC.Pair.ramification' does not depend on any axioms
'FRC.Pair.fusion' does not depend on any axioms
'FRC.Pair.inv13' does not depend on any axioms
'FRC.Pair.parity_instance' does not depend on any axioms
'FRC.Pair.mult_eq_mu' does not depend on any axioms
'FRC.Shell.Frame.quat_bijective' does not depend on any axioms
'FRC.Shell.Prime.exists_inv' does not depend on any axioms
'FRC.Shell.Prime.fld' does not depend on any axioms
'FRC.Shell.Prime.hopf_section' does not depend on any axioms
'FRC.Shell.Prime.hopf_counts' does not depend on any axioms
'FRC.Shell.Prime.frame_triple' does not depend on any axioms
'FRC.Symbol.sum_swap' does not depend on any axioms
'FRC.Symbol.lin2_zero' does not depend on any axioms
'FRC.Symbol.lin2_step' does not depend on any axioms
'FRC.Symbol.sum_lin2' does not depend on any axioms
'FRC.Symbol.lin3_zero' does not depend on any axioms
'FRC.Symbol.lin3_step' does not depend on any axioms
'FRC.Symbol.sum_lin3' does not depend on any axioms
'FRC.Symbol.lin6_zero' does not depend on any axioms
'FRC.Symbol.lin6_step' does not depend on any axioms
'FRC.Symbol.sum_lin6' does not depend on any axioms
'FRC.Symbol.dot' does not depend on any axioms
'FRC.Symbol.comm_pt' does not depend on any axioms
'FRC.Symbol.dot_comm' does not depend on any axioms
'FRC.Symbol.dot_zero_left' does not depend on any axioms
'FRC.Symbol.lin2_pt' does not depend on any axioms
'FRC.Symbol.dot_lin2' does not depend on any axioms
'FRC.Symbol.lin3_pt' does not depend on any axioms
'FRC.Symbol.dot_lin3' does not depend on any axioms
'FRC.Symbol.quad2_pt' does not depend on any axioms
'FRC.Symbol.dot_quad2' does not depend on any axioms
'FRC.Symbol.quad3_pt' does not depend on any axioms
'FRC.Symbol.dot_quad3' does not depend on any axioms
'FRC.Symbol.shift' does not depend on any axioms
'FRC.Symbol.vecForm' does not depend on any axioms
'FRC.Symbol.vec_ring' does not depend on any axioms
'FRC.Symbol.vec_shift' does not depend on any axioms
'FRC.Symbol.vec_invariant' does not depend on any axioms
'FRC.Symbol.vec_null' does not depend on any axioms
'FRC.Symbol.eq_zero_of_add_left' does not depend on any axioms
'FRC.Symbol.sub_one_zero' does not depend on any axioms
'FRC.Symbol.lc2' does not depend on any axioms
'FRC.Symbol.lc4' does not depend on any axioms
'FRC.Symbol.cancel3_ring' does not depend on any axioms
'FRC.Symbol.cancel3' does not depend on any axioms
'FRC.Symbol.cancel4_ring' does not depend on any axioms
'FRC.Symbol.cancel4' does not depend on any axioms
'FRC.Symbol.unit_ring' does not depend on any axioms
'FRC.Symbol.vec_iff_unit' does not depend on any axioms
'FRC.Symbol.basis' does not depend on any axioms
'FRC.Symbol.basis_self' does not depend on any axioms
'FRC.Symbol.basis_ne' does not depend on any axioms
'FRC.Symbol.basis_mul_ne' does not depend on any axioms
'FRC.Symbol.dot_basis_self' does not depend on any axioms
'FRC.Symbol.dot_basis_ne' does not depend on any axioms
'FRC.Symbol.maxwell_unique' does not depend on any axioms
'FRC.Symbol.tr' does not depend on any axioms
'FRC.Symbol.ctr' does not depend on any axioms
'FRC.Symbol.pair' does not depend on any axioms
'FRC.Symbol.gauge' does not depend on any axioms
'FRC.Symbol.tensForm' does not depend on any axioms
'FRC.Symbol.tr_pt' does not depend on any axioms
'FRC.Symbol.tr_gauge' does not depend on any axioms
'FRC.Symbol.ctr_pt' does not depend on any axioms
'FRC.Symbol.ctr_gauge' does not depend on any axioms
'FRC.Symbol.rows_pt' does not depend on any axioms
'FRC.Symbol.ctr_dot' does not depend on any axioms
'FRC.Symbol.rows' does not depend on any axioms
'FRC.Symbol.sym_pt' does not depend on any axioms
'FRC.Symbol.ctr_symm' does not depend on any axioms
'FRC.Symbol.row_pt' does not depend on any axioms
'FRC.Symbol.pair_pt' does not depend on any axioms
'FRC.Symbol.pair_gauge' does not depend on any axioms
'FRC.Symbol.tens_ring' does not depend on any axioms
'FRC.Symbol.tens_shift' does not depend on any axioms
'FRC.Symbol.fp_ring' does not depend on any axioms
'FRC.Symbol.fierz_pauli_invariant' does not depend on any axioms
'FRC.Symbol.zero2' does not depend on any axioms
'FRC.Symbol.unit11' does not depend on any axioms
'FRC.Symbol.var_ring' does not depend on any axioms
'FRC.Symbol.var_zero' does not depend on any axioms
'FRC.Symbol.ctr_zero2' does not depend on any axioms
'FRC.Symbol.tr_zero2' does not depend on any axioms
'FRC.Symbol.u11_pt' does not depend on any axioms
'FRC.Symbol.ctr_unit11' does not depend on any axioms
'FRC.Symbol.tr_unit11' does not depend on any axioms
'FRC.Symbol.t1_ring' does not depend on any axioms
'FRC.Symbol.t2_ring' does not depend on any axioms
'FRC.Symbol.t3_ring' does not depend on any axioms
'FRC.Symbol.line_a1' does not depend on any axioms
'FRC.Symbol.line_a2' does not depend on any axioms
'FRC.Symbol.fierz_pauli_unique' does not depend on any axioms
'FRC.Symbol.char_two_not_unique' does not depend on any axioms
'FRC.Grav.natEval' does not depend on any axioms
'FRC.Grav.negFree' does not depend on any axioms
'FRC.Grav.nlook' does not depend on any axioms
'FRC.Grav.mEvalN' does not depend on any axioms
'FRC.Grav.pEvalN' does not depend on any axioms
'FRC.Grav.mEvalN_append' does not depend on any axioms
'FRC.Grav.pEvalN_append' does not depend on any axioms
'FRC.Grav.pEvalN_row' does not depend on any axioms
'FRC.Grav.pEvalN_mul' does not depend on any axioms
'FRC.Grav.pMul_nil' does not depend on any axioms
'FRC.Grav.toP_neg_nil' does not depend on any axioms
'FRC.Grav.natEval_toP' does not depend on any axioms
'FRC.Grav.mEvalN_insM' does not depend on any axioms
'FRC.Grav.mEvalN_sortM' does not depend on any axioms
'FRC.Grav.add_left_comm'' does not depend on any axioms
'FRC.Grav.pEvalN_insP' does not depend on any axioms
'FRC.Grav.pEvalN_nfP' does not depend on any axioms
'FRC.Grav.nat_sound' does not depend on any axioms
'FRC.Grav.nsum' does not depend on any axioms
'FRC.Grav.nsum_congr' does not depend on any axioms
'FRC.Grav.nsum_add' does not depend on any axioms
'FRC.Grav.nsum_zero' does not depend on any axioms
'FRC.Grav.nsum_const' does not depend on any axioms
'FRC.Grav.nsum_mul_left' does not depend on any axioms
'FRC.Grav.nsum_comm' does not depend on any axioms
'FRC.Grav.nsum_succ'' does not depend on any axioms
'FRC.Grav.nsumList' does not depend on any axioms
'FRC.Grav.nsumList_imageList' does not depend on any axioms
'FRC.Grav.nsumList_erase' does not depend on any axioms
'FRC.Grav.nsumList_eq_nsum' does not depend on any axioms
'FRC.Grav.nsum_perm' does not depend on any axioms
'FRC.Grav.natCount_eq_nsum' does not depend on any axioms
'FRC.Grav.natCount_single' does not depend on any axioms
'FRC.Grav.natCount_or' does not depend on any axioms
'FRC.Grav.natCount_true' does not depend on any axioms
'FRC.Grav.count' does not depend on any axioms
'FRC.Grav.count_congr' does not depend on any axioms
'FRC.Grav.ofNat_inj' does not depend on any axioms
'FRC.Grav.count_bij' does not depend on any axioms
'FRC.Grav.count_eq' does not depend on any axioms
'FRC.Grav.count_true' does not depend on any axioms
'FRC.Grav.count_false' does not depend on any axioms
'FRC.Grav.ite_iff' does not depend on any axioms
'FRC.Grav.red1' does not depend on any axioms
'FRC.Grav.conic_row' does not depend on any axioms
'FRC.Grav.conic_count' does not depend on any axioms
'FRC.Grav.sphere_count' does not depend on any axioms
'FRC.Grav.count_sq' does not depend on any axioms
'FRC.Grav.quad' does not depend on any axioms
'FRC.Grav.sphereCount' does not depend on any axioms
'FRC.Grav.sphere_area_rung' does not depend on any axioms
'FRC.Grav.sphere_area' does not depend on any axioms
'FRC.Grav.count_identity' does not depend on any axioms
'FRC.Grav.record_mass' does not depend on any axioms
'FRC.Grav.record_response' does not depend on any axioms
'FRC.Grav.record_response_rate' does not depend on any axioms
'FRC.Grav.temperature_rate' does not depend on any axioms
'FRC.Grav.smarr' does not depend on any axioms
'FRC.Grav.merger_area' does not depend on any axioms
'FRC.Grav.calibration' does not depend on any axioms
'FRC.Grav.newton_residue' does not depend on any axioms
'FRC.Grav.hbar_root' does not depend on any axioms
'FRC.Grav.closed_chart' does not depend on any axioms
'FRC.Grav.two_face_count' does not depend on any axioms
'FRC.Grav.register13_17' does not depend on any axioms
'FRC.Grav.merger_instance' does not depend on any axioms
'FRC.Grav.lab_register' does not depend on any axioms
'FRC.Grav.chart_plane_overflows' does not depend on any axioms
'FRC.Grav.chart_space_overflows' does not depend on any axioms
'FRC.Grav.chart_line_fits' does not depend on any axioms
'FRC.Grav.chart_lab_instance' does not depend on any axioms
'FRC.Lattice.cdiff' does not depend on any axioms
'FRC.Lattice.fdiff' does not depend on any axioms
'FRC.Lattice.bdiff' does not depend on any axioms
'FRC.Lattice.lap' does not depend on any axioms
'FRC.Lattice.sum_shift_pair' does not depend on any axioms
'FRC.Lattice.central_difference_adjoint' does not depend on any axioms
'FRC.Lattice.forward_difference_adjoint' does not depend on any axioms
'FRC.Lattice.chi' does not depend on any axioms
'FRC.Lattice.chi_cyc' does not depend on any axioms
'FRC.Lattice.laplacian_symbol' does not depend on any axioms
'FRC.Drift.channel_q4' does not depend on any axioms
'FRC.Drift.cover_triangle' does not depend on any axioms
'FRC.Drift.cover_deviation' does not depend on any axioms
'FRC.Drift.least' does not depend on any axioms
'FRC.Drift.least_le' does not depend on any axioms
'FRC.Drift.least_bound' does not depend on any axioms
'FRC.Drift.least_min' does not depend on any axioms
'FRC.Drift.least_hit' does not depend on any axioms
'FRC.Drift.isReturn' does not depend on any axioms
'FRC.Drift.isReturn_iff' does not depend on any axioms
'FRC.Drift.firstReturn' does not depend on any axioms
'FRC.Drift.firstReturn_pos' does not depend on any axioms
'FRC.Drift.firstReturn_le' does not depend on any axioms
'FRC.Drift.firstReturn_returns' does not depend on any axioms
'FRC.Drift.firstReturn_min' does not depend on any axioms
'FRC.Drift.return_iff' does not depend on any axioms
'FRC.Drift.defect_instance' does not depend on any axioms
'FRC.Drift.pair_tally' does not depend on any axioms
'FRC.Drift.tally_weight' does not depend on any axioms
'FRC.Drift.locked_sum' does not depend on any axioms
'FRC.Drift.character_composition' does not depend on any axioms
'FRC.Drift.ind' does not depend on any axioms
'FRC.Drift.antisymmetric_sum' does not depend on any axioms
'FRC.Drift.gauss_law' does not depend on any axioms
'FRC.Drift.pn_coefficients' does not depend on any axioms
'FRC.Drift.frobenius_trace' does not depend on any axioms
'FRC.Drift.registration_root' does not depend on any axioms
'FRC.Drift.conj_pow' does not depend on any axioms
'FRC.Drift.conj_branch' does not depend on any axioms
'FRC.Drift.compression' does not depend on any axioms
'FRC.Drift.character_unique' does not depend on any axioms
'FRC.Drift.cut_ordering' does not depend on any axioms
'FRC.Drift.nesting_bound' does not depend on any axioms
'FRC.Drift.cut_area_monotone' does not depend on any axioms
'FRC.Drift.fold_collision' does not depend on any axioms
'FRC.Drift.fold_return' does not depend on any axioms
'FRC.Quantum.mod_zero_of_eq_mul' does not depend on any axioms
'FRC.Quantum.eq_mul_of_mod_zero' does not depend on any axioms
'FRC.Quantum.mul_mod_zero' does not depend on any axioms
'FRC.Quantum.mod_of_add_mod' does not depend on any axioms
'FRC.Quantum.mod_mod_of_dvd' does not depend on any axioms
'FRC.Quantum.mod_add_left_cancel' does not depend on any axioms
'FRC.Quantum.lt_of_mul_lt_mul' does not depend on any axioms
'FRC.Quantum.sub_pos' does not depend on any axioms
'FRC.Quantum.Joint' does not depend on any axioms
'FRC.Quantum.prodN' does not depend on any axioms
'FRC.Quantum.prodN_pos' does not depend on any axioms
'FRC.Quantum.prodN_joint' does not depend on any axioms
'FRC.Quantum.joint_recurrence' does not depend on any axioms
'FRC.Quantum.joint_least' does not depend on any axioms
'FRC.Quantum.mulIdx' does not depend on any axioms
'FRC.Quantum.mulIdx_spec' does not depend on any axioms
'FRC.Quantum.pair_offset' does not depend on any axioms
'FRC.Quantum.prodRange_pow' does not depend on any axioms
'FRC.Quantum.prodRange_one' does not depend on any axioms
'FRC.Quantum.dephasing' does not depend on any axioms
'FRC.Quantum.absorbed' does not depend on any axioms
'FRC.Quantum.pow_mod_of_not_mod' does not depend on any axioms
'FRC.Quantum.unique_home' does not depend on any axioms
'FRC.Quantum.sign_both' does not depend on any axioms
'FRC.Quantum.visibility_cap' does not depend on any axioms
'FRC.Quantum.two_part_homes' does not depend on any axioms
'FRC.Quantum.registration_instances' does not depend on any axioms
'FRC.Observation.pow_inj_of_order' does not depend on any axioms
'FRC.Observation.pow_mod_order' does not depend on any axioms
'FRC.Observation.pow_eq_pow_iff_mod' does not depend on any axioms
'FRC.Observation.pow_eq_one_iff_mod' does not depend on any axioms
'FRC.Observation.power_maps' does not depend on any axioms
'FRC.Observation.stationary' does not depend on any axioms
'FRC.Observation.roots_of_order' does not depend on any axioms
'FRC.Observation.character_is_power_map' does not depend on any axioms
'FRC.Observation.stationary_modes' does not depend on any axioms
'FRC.Observation.geom_sum_zero' does not depend on any axioms
'FRC.Observation.character_sum' does not depend on any axioms
'FRC.Observation.shift_mod' does not depend on any axioms
'FRC.Observation.orthogonality' does not depend on any axioms
'FRC.Observation.selection' does not depend on any axioms
'FRC.Observation.lueders' does not depend on any axioms
'FRC.Observation.sum_mul_sum' does not depend on any axioms
'FRC.Observation.sum_comm' does not depend on any axioms
'FRC.Observation.pair_count' does not depend on any axioms
'FRC.Observation.pure_winding_weight' does not depend on any axioms
'FRC.Observation.cross_mod' does not depend on any axioms
'FRC.Observation.parseval' does not depend on any axioms
'FRC.Observation.ofNat_add' does not depend on any axioms
'FRC.Observation.nsum' does not depend on any axioms
'FRC.Observation.ofNat_nsum' does not depend on any axioms
'FRC.Observation.shadow' does not depend on any axioms
'FRC.Observation.conv' does not depend on any axioms
'FRC.Observation.reduce_add' does not depend on any axioms
'FRC.Observation.reduce_mul' does not depend on any axioms
'FRC.Observation.reduce_wrap' does not depend on any axioms
'FRC.Observation.window_lift' does not depend on any axioms
'FRC.Observation.wrap_quantised' does not depend on any axioms
'FRC.Observation.shared_core' does not depend on any axioms
'FRC.Observation.no_quarter_turn' does not depend on any axioms
'FRC.Observation.classicality_index' does not depend on any axioms
'FRC.Observation.transport_trichotomy_raw' does not depend on any axioms
'FRC.Observation.mul_mod_mul_left'' does not depend on any axioms
'FRC.Observation.transport_residues' does not depend on any axioms
'FRC.Observation.transport_trichotomy' does not depend on any axioms
'FRC.Observation.transport_cases' does not depend on any axioms
'FRC.Observation.exponent_negation' does not depend on any axioms
'FRC.Observation.inv_spec' does not depend on any axioms
'FRC.Observation.eq_zero_of_norm_eq_zero' does not depend on any axioms
'FRC.Observation.ext_mul_eq_zero' does not depend on any axioms
'FRC.Observation.ext_add_neg' does not depend on any axioms
'FRC.Observation.ext_sq_eq_sq' does not depend on any axioms
'FRC.Observation.ext_decompose' does not depend on any axioms
'FRC.Observation.frobenius_unique' does not depend on any axioms
'FRC.Observation.torus_conj_inv' does not depend on any axioms
'FRC.Interference.Additive' does not depend on any axioms
'FRC.Interference.weight' does not depend on any axioms
'FRC.Interference.mixedDiff' does not depend on any axioms
'FRC.Interference.mixedDiff_zero' does not depend on any axioms
'FRC.Interference.mixedDiff_succ' does not depend on any axioms
'FRC.Interference.weight_diff1' does not depend on any axioms
'FRC.Interference.sorkin_second' does not depend on any axioms
'FRC.Interference.sorkin_third' does not depend on any axioms
'FRC.Interference.sorkin_hierarchy' does not depend on any axioms
'FRC.Interference.additive_id' does not depend on any axioms
'FRC.Interference.sorkin_second_witness' does not depend on any axioms
'FRC.Interference.ofNat_pow' does not depend on any axioms
'FRC.Interference.hadamard_sq' does not depend on any axioms
'FRC.Interference.hadamard_even' does not depend on any axioms
'FRC.Interference.hadamard_odd' does not depend on any axioms
'FRC.Interference.tallyNorm' does not depend on any axioms
'FRC.Interference.tally_norm_mono' does not depend on any axioms
'FRC.Interference.ceiling_641' does not depend on any axioms
'FRC.Composite.offset_invariant' does not depend on any axioms
'FRC.Composite.cluster_offset' does not depend on any axioms
'FRC.Composite.winding_period' does not depend on any axioms
'FRC.Composite.locked_norm' does not depend on any axioms
'FRC.Composite.tsum' does not depend on any axioms
'FRC.Composite.tsum_zero' does not depend on any axioms
'FRC.Composite.tsum_succ' does not depend on any axioms
'FRC.Composite.tsum_congr' does not depend on any axioms
'FRC.Composite.tsum_add' does not depend on any axioms
'FRC.Composite.tsum_const' does not depend on any axioms
'FRC.Composite.tsum_mul_left' does not depend on any axioms
'FRC.Composite.tsum_mul_right' does not depend on any axioms
'FRC.Composite.tsum_sum' does not depend on any axioms
'FRC.Composite.tsum_cell' does not depend on any axioms
'FRC.Composite.tsum_cross' does not depend on any axioms
'FRC.Composite.spread_average' does not depend on any axioms
'FRC.Composite.field_linear' does not depend on any axioms
'FRC.Composite.eta_zero' does not depend on any axioms
'FRC.Composite.half_turn_sixteen' does not depend on any axioms
'FRC.Composite.order_eight_of_sixteen' does not depend on any axioms
'FRC.Composite.doublet_readout' does not depend on any axioms
'FRC.Composite.singlet_square' does not depend on any axioms
'FRC.Composite.no_signalling' does not depend on any axioms
'FRC.Composite.channel_complementarity' does not depend on any axioms
'FRC.Composite.channel_product_at_zero' does not depend on any axioms
'FRC.Composite.drive_norm' does not depend on any axioms
'FRC.Composite.revival' does not depend on any axioms
'FRC.Composite.prodRange_const' does not depend on any axioms
'FRC.Composite.branch_phase' does not depend on any axioms
'FRC.Composite.pair_product' does not depend on any axioms
'FRC.Composite.spread_cancels' does not depend on any axioms
'FRC.Composite.channel_assembly' does not depend on any axioms
'FRC.Composite.order_independence' does not depend on any axioms
'FRC.Composite.joint_refinement' does not depend on any axioms
'FRC.Composite.decHasOrder' does not depend on any axioms
'FRC.Composite.carrier_157' does not depend on any axioms
'FRC.Composite.carrier_421' does not depend on any axioms
'FRC.Composite.carrier_641' does not depend on any axioms
'FRC.Unitary.x_add_comm' does not depend on any axioms
'FRC.Unitary.x_add_assoc' does not depend on any axioms
'FRC.Unitary.x_add_left_comm' does not depend on any axioms
'FRC.Unitary.x_zero_add' does not depend on any axioms
'FRC.Unitary.x_add_zero' does not depend on any axioms
'FRC.Unitary.x_neg_add' does not depend on any axioms
'FRC.Unitary.x_neg_neg' does not depend on any axioms
'FRC.Unitary.x_neg_zero' does not depend on any axioms
'FRC.Unitary.x_neg_add_rev' does not depend on any axioms
'FRC.Unitary.x_add_right_cancel' does not depend on any axioms
'FRC.Unitary.x_zero_mul' does not depend on any axioms
'FRC.Unitary.x_left_distrib' does not depend on any axioms
'FRC.Unitary.x_neg_mul' does not depend on any axioms
'FRC.Unitary.x_mul_zero' does not depend on any axioms
'FRC.Unitary.x_right_distrib' does not depend on any axioms
'FRC.Unitary.x_mul_neg' does not depend on any axioms
'FRC.Unitary.x_neg_mul_neg' does not depend on any axioms
'FRC.Unitary.x_mul_left_comm' does not depend on any axioms
'FRC.Unitary.conj_add' does not depend on any axioms
'FRC.Unitary.xeval' does not depend on any axioms
'FRC.Unitary.xlook' does not depend on any axioms
'FRC.Unitary.xmEval' does not depend on any axioms
'FRC.Unitary.xpEval' does not depend on any axioms
'FRC.Unitary.xmEval_append' does not depend on any axioms
'FRC.Unitary.xpEval_append' does not depend on any axioms
'FRC.Unitary.xpEval_row' does not depend on any axioms
'FRC.Unitary.xpEval_mul' does not depend on any axioms
'FRC.Unitary.xring_add' does not depend on any axioms
'FRC.Unitary.xring_mul' does not depend on any axioms
'FRC.Unitary.xring_neg' does not depend on any axioms
'FRC.Unitary.xtoP_eval' does not depend on any axioms
'FRC.Unitary.xmEval_insM' does not depend on any axioms
'FRC.Unitary.xmEval_sortM' does not depend on any axioms
'FRC.Unitary.xpEval_insP' does not depend on any axioms
'FRC.Unitary.xpEval_nfP' does not depend on any axioms
'FRC.Unitary.xsound' does not depend on any axioms
'FRC.Unitary.red1' does not depend on any axioms
'FRC.Unitary.red2' does not depend on any axioms
'FRC.Unitary.red3' does not depend on any axioms
'FRC.Unitary.root_off_base' does not depend on any axioms
'FRC.Unitary.cube_root_conj' does not depend on any axioms
'FRC.Unitary.cube_one' does not depend on any axioms
'FRC.Unitary.mod3_step' does not depend on any axioms
'FRC.Unitary.pow_mod_three' does not depend on any axioms
'FRC.Unitary.pow_eq_one_iff' does not depend on any axioms
'FRC.Unitary.triality_scalar' does not depend on any axioms
'FRC.Unitary.omega' does not depend on any axioms
'FRC.Unitary.omega_root' does not depend on any axioms
'FRC.Unitary.nonsquare' does not depend on any axioms
'FRC.Unitary.three_eq' does not depend on any axioms
'FRC.Unitary.neg_three' does not depend on any axioms
'FRC.Unitary.mext' does not depend on any axioms
'FRC.Unitary.mmul' does not depend on any axioms
'FRC.Unitary.dag' does not depend on any axioms
'FRC.Unitary.det' does not depend on any axioms
'FRC.Unitary.adj' does not depend on any axioms
'FRC.Unitary.scal' does not depend on any axioms
'FRC.Unitary.mone' does not depend on any axioms
'FRC.Unitary.smul' does not depend on any axioms
'FRC.Unitary.ents' does not depend on any axioms
'FRC.Unitary.SU' does not depend on any axioms
'FRC.Unitary.assoc_entry' does not depend on any axioms
'FRC.Unitary.mmul_assoc' does not depend on any axioms
'FRC.Unitary.conj_dot' does not depend on any axioms
'FRC.Unitary.dag_mul' does not depend on any axioms
'FRC.Unitary.det_mul' does not depend on any axioms
'FRC.Unitary.sandwich' does not depend on any axioms
'FRC.Unitary.e0' does not depend on any axioms
'FRC.Unitary.e1' does not depend on any axioms
'FRC.Unitary.e2' does not depend on any axioms
'FRC.Unitary.f0' does not depend on any axioms
'FRC.Unitary.f1' does not depend on any axioms
'FRC.Unitary.f2' does not depend on any axioms
'FRC.Unitary.scal_mul' does not depend on any axioms
'FRC.Unitary.mul_scal' does not depend on any axioms
'FRC.Unitary.smul_smul' does not depend on any axioms
'FRC.Unitary.one_smul' does not depend on any axioms
'FRC.Unitary.conj_zero' does not depend on any axioms
'FRC.Unitary.conj_one' does not depend on any axioms
'FRC.Unitary.one_cube' does not depend on any axioms
'FRC.Unitary.dag_scal' does not depend on any axioms
'FRC.Unitary.det_scal' does not depend on any axioms
'FRC.Unitary.scal_SU' does not depend on any axioms
'FRC.Unitary.mul_adj' does not depend on any axioms
'FRC.Unitary.adj_mul' does not depend on any axioms
'FRC.Unitary.det_adj' does not depend on any axioms
'FRC.Unitary.su_group' does not depend on any axioms
'FRC.Unitary.triality_frame' does not depend on any axioms
'FRC.Interactions.bit' does not depend on any axioms
'FRC.Interactions.cnt' does not depend on any axioms
'FRC.Interactions.disj' does not depend on any axioms
'FRC.Interactions.inv' does not depend on any axioms
'FRC.Interactions.emul' does not depend on any axioms
'FRC.Interactions.assocL' does not depend on any axioms
'FRC.Interactions.assocR' does not depend on any axioms
'FRC.Interactions.gen16' does not depend on any axioms
'FRC.Interactions.fifth' does not depend on any axioms
'FRC.Interactions.reflection_algebra' does not depend on any axioms
'FRC.Interactions.fifth_direction' does not depend on any axioms
'FRC.Interactions.col' does not depend on any axioms
'FRC.Interactions.wk' does not depend on any axioms
'FRC.Interactions.y6' does not depend on any axioms
'FRC.Interactions.t3h' does not depend on any axioms
'FRC.Interactions.q6' does not depend on any axioms
'FRC.Interactions.isum' does not depend on any axioms
'FRC.Interactions.one_generation' does not depend on any axioms
'FRC.Interactions.three_eq' does not depend on any axioms
'FRC.Interactions.two_eq' does not depend on any axioms
'FRC.Interactions.koide_parseval' does not depend on any axioms
'FRC.Interactions.koide_two_thirds' does not depend on any axioms
'FRC.Interactions.omega3' does not depend on any axioms
'FRC.Interactions.hat1' does not depend on any axioms
'FRC.Interactions.hat2' does not depend on any axioms
'FRC.Interactions.red2i' does not depend on any axioms
'FRC.Interactions.koide_extension' does not depend on any axioms
'FRC.Interactions.koide_half' does not depend on any axioms
'FRC.Horizon.sum_comm' does not depend on any axioms
'FRC.Horizon.half_inverse' does not depend on any axioms
'FRC.Horizon.zero_slot' does not depend on any axioms
'FRC.Horizon.modeCoeff' does not depend on any axioms
'FRC.Horizon.mode_expansion' does not depend on any axioms
'FRC.Horizon.shift_power_character' does not depend on any axioms
'FRC.Horizon.eigenphase' does not depend on any axioms
'FRC.Horizon.shift_trace' does not depend on any axioms
'FRC.Horizon.readout' does not depend on any axioms
'FRC.Horizon.readout_on_line' does not depend on any axioms
'FRC.Horizon.readout_slot_index' does not depend on any axioms
'FRC.Horizon.slot_complementarity' does not depend on any axioms
'FRC.Horizon.quarter_turn_eq_pow' does not depend on any axioms
'FRC.Horizon.subject_constants' does not depend on any axioms
'FRC.Horizon.constants13' does not depend on any axioms
'FRC.Horizon.pow_mod_of_pow_eq_one' does not depend on any axioms
'FRC.Horizon.ramanujan_sum' does not depend on any axioms
'FRC.Horizon.ramanujan_zero' does not depend on any axioms
'FRC.Horizon.ramanujan53' does not depend on any axioms
'FRC.Horizon.rho' does not depend on any axioms
'FRC.Horizon.sigma' does not depend on any axioms
'FRC.Horizon.klein_four' does not depend on any axioms
'FRC.Horizon.critical_line' does not depend on any axioms
'FRC.Horizon.fixed_half_turn' does not depend on any axioms
'FRC.Horizon.norm_on_line' does not depend on any axioms
'FRC.Horizon.quarter_turn_off_circle' does not depend on any axioms
'FRC.Horizon.circle13' does not depend on any axioms
'FRC.Horizon.le_mul_self' does not depend on any axioms
'FRC.Horizon.window_readback' does not depend on any axioms
'FRC.Horizon.factorisation_iff' does not depend on any axioms
'FRC.Horizon.frame_coincidence' does not depend on any axioms
'FRC.Horizon.lab_pair' does not depend on any axioms
'FRC.Horizon.closure' does not depend on any axioms
'FRC.Horizon.closure_lab' does not depend on any axioms
'FRC.Horizon.negative_control13' does not depend on any axioms
'FRC.Horizon.sumTo_le' does not depend on any axioms
'FRC.Horizon.cells_clean_iff_cycle' does not depend on any axioms
'FRC.Horizon.fixedCount' does not depend on any axioms
'FRC.Horizon.fixedCount_le' does not depend on any axioms
'FRC.Horizon.clean_iff_count' does not depend on any axioms
'FRC.Horizon.fixedCount_mono' does not depend on any axioms
'FRC.Horizon.turing_chain' does not depend on any axioms
'FRC.Horizon.turing_equal' does not depend on any axioms
'FRC.Horizon.turing_phantom' does not depend on any axioms
'FRC.Ladder.power_index' does not depend on any axioms
'FRC.Ladder.iter' does not depend on any axioms
'FRC.Ladder.phase_index' does not depend on any axioms
'FRC.Ladder.ascent_step' does not depend on any axioms
'FRC.Ladder.tower_reduces' does not depend on any axioms
'FRC.Ladder.mul_perm' does not depend on any axioms
'FRC.Ladder.recentre' does not depend on any axioms
'FRC.Ladder.recentre_witness' does not depend on any axioms
'FRC.Ladder.recentre_inj' does not depend on any axioms
'FRC.Ladder.recentre_surj' does not depend on any axioms
'FRC.Ladder.power_bijective_of_unit' does not depend on any axioms
'FRC.Ladder.power_image' does not depend on any axioms
'FRC.Ladder.power_image_index' does not depend on any axioms
'FRC.Ladder.compressive_of_gcd' does not depend on any axioms
'FRC.Ladder.half' does not depend on any axioms
'FRC.Ladder.par' does not depend on any axioms
'FRC.Ladder.half_par' does not depend on any axioms
'FRC.Ladder.par_lt_two' does not depend on any axioms
'FRC.Ladder.half_lt' does not depend on any axioms
'FRC.Ladder.lt_of_mul_lt_mul_left'' does not depend on any axioms
'FRC.Ladder.bitsAux' does not depend on any axioms
'FRC.Ladder.bits' does not depend on any axioms
'FRC.Ladder.bitsAux_eq' does not depend on any axioms
'FRC.Ladder.bitsAux_le_of_lt_pow' does not depend on any axioms
'FRC.Ladder.bits_le_of_lt_pow' does not depend on any axioms
'FRC.Ladder.lt_pow_bits' does not depend on any axioms
'FRC.Ladder.pow_bits_pred_le' does not depend on any axioms
'FRC.Ladder.bits_bracket' does not depend on any axioms
'FRC.Ladder.distSum' does not depend on any axioms
'FRC.Ladder.two_mul_distSum' does not depend on any axioms
'FRC.Ladder.dist_le' does not depend on any axioms
'FRC.Ladder.sqmulAux' does not depend on any axioms
'FRC.Ladder.sqmul' does not depend on any axioms
'FRC.Ladder.sqmulAux_spec' does not depend on any axioms
'FRC.Ladder.sqmul_spec' does not depend on any axioms
'FRC.Ladder.sqmulAux_count' does not depend on any axioms
'FRC.Ladder.sqmul_count' does not depend on any axioms
'FRC.Ladder.sqmul_count_of_lt_pow' does not depend on any axioms
'FRC.Ladder.findLT' does not depend on any axioms
'FRC.Ladder.findLT_some' does not depend on any axioms
'FRC.Ladder.findLT_of_exists' does not depend on any axioms
'FRC.Ladder.giantAux' does not depend on any axioms
'FRC.Ladder.bsgs' does not depend on any axioms
'FRC.Ladder.baby_step' does not depend on any axioms
'FRC.Ladder.giantAux_count' does not depend on any axioms
'FRC.Ladder.giantAux_spec' does not depend on any axioms
'FRC.Ladder.giantAux_of_exists' does not depend on any axioms
'FRC.Ladder.descendsB' does not depend on any axioms
'FRC.Ladder.descendsB_spec' does not depend on any axioms
'FRC.Ladder.bsgs_spec' does not depend on any axioms
'FRC.Ladder.bsgs_total' does not depend on any axioms
'FRC.Ladder.eigenvalues13' does not depend on any axioms
'FRC.Ladder.phase13' does not depend on any axioms
'FRC.Ladder.tower13' does not depend on any axioms
'FRC.Ladder.recentre13' does not depend on any axioms
'FRC.Ladder.powers13' does not depend on any axioms
'FRC.Ladder.sqmul13' does not depend on any axioms
'FRC.Ladder.descent13_101' does not depend on any axioms
'FRC.Ledger.p00032' does not depend on any axioms
'FRC.Ledger.p01004' does not depend on any axioms
'FRC.Ledger.p01005' does not depend on any axioms
'FRC.Ledger.p01006' does not depend on any axioms
'FRC.Ledger.p01011' does not depend on any axioms
'FRC.Ledger.p01013' does not depend on any axioms
'FRC.Ledger.p01015' does not depend on any axioms
'FRC.Ledger.p01019' does not depend on any axioms
'FRC.Ledger.p01020' does not depend on any axioms
'FRC.Ledger.p02007' does not depend on any axioms
'FRC.Ledger.p02013' does not depend on any axioms
'FRC.Ledger.p02014' does not depend on any axioms
'FRC.Ledger.p02015' does not depend on any axioms
'FRC.Ledger.p02017' does not depend on any axioms
'FRC.Ledger.p02018' does not depend on any axioms
'FRC.Ledger.p02019' does not depend on any axioms
'FRC.Ledger.p02025' does not depend on any axioms
'FRC.Ledger.p02027' does not depend on any axioms
'FRC.Ledger.p02028' does not depend on any axioms
'FRC.Ledger.p02029' does not depend on any axioms
'FRC.Ledger.p06009' does not depend on any axioms
'FRC.Ledger.p06010' does not depend on any axioms
'FRC.Ledger.p06012' does not depend on any axioms
'FRC.Ledger.p06014' does not depend on any axioms
'FRC.Ledger.p06027' does not depend on any axioms
'FRC.Ledger.p08011' does not depend on any axioms
'FRC.Ledger.p13044' does not depend on any axioms
'FRC.Ledger.p13051' does not depend on any axioms
'FRC.Ledger.p13053' does not depend on any axioms
'FRC.Ledger.p14031' does not depend on any axioms
'FRC.Ledger.p26048' does not depend on any axioms
'FRC.Ledger.p00030' does not depend on any axioms
'FRC.Ledger.p03006' does not depend on any axioms
'FRC.Ledger.p03007' does not depend on any axioms
'FRC.Ledger.p03008' does not depend on any axioms
'FRC.Ledger.p03009' does not depend on any axioms
'FRC.Ledger.p03013' does not depend on any axioms
'FRC.Ledger.p03014' does not depend on any axioms
'FRC.Ledger.p03017' does not depend on any axioms
'FRC.Ledger.p08002' does not depend on any axioms
'FRC.Ledger.p08012' does not depend on any axioms
'FRC.Ledger.p22027' does not depend on any axioms
'FRC.Ledger.p22028' does not depend on any axioms
'FRC.Ledger.p00190' does not depend on any axioms
'FRC.Ledger.p01009' does not depend on any axioms
'FRC.Ledger.p04015' does not depend on any axioms
'FRC.Ledger.p38051' does not depend on any axioms
'FRC.Ledger.p00022' does not depend on any axioms
'FRC.Ledger.p00189' does not depend on any axioms
'FRC.Ledger.p06013' does not depend on any axioms
'FRC.Ledger.p06016' does not depend on any axioms
'FRC.Ledger.p06017' does not depend on any axioms
'FRC.Ledger.p06018' does not depend on any axioms
'FRC.Ledger.p06019' does not depend on any axioms
'FRC.Ledger.p06020' does not depend on any axioms
'FRC.Ledger.p06021' does not depend on any axioms
'FRC.Ledger.p06022' does not depend on any axioms
'FRC.Ledger.p06023' does not depend on any axioms
'FRC.Ledger.p06024' does not depend on any axioms
'FRC.Ledger.p06025' does not depend on any axioms
'FRC.Ledger.p06031' does not depend on any axioms
'FRC.Ledger.p06032' does not depend on any axioms
'FRC.Ledger.p06034' does not depend on any axioms
'FRC.Ledger.p06035' does not depend on any axioms
'FRC.Ledger.p06036' does not depend on any axioms
'FRC.Ledger.p06050' does not depend on any axioms
'FRC.Ledger.p06052' does not depend on any axioms
'FRC.Ledger.p06053' does not depend on any axioms
'FRC.Ledger.p06054' does not depend on any axioms
'FRC.Ledger.p06056' does not depend on any axioms
'FRC.Ledger.p01026' does not depend on any axioms
'FRC.Ledger.p00186' does not depend on any axioms
'FRC.Ledger.p05013' does not depend on any axioms
'FRC.Ledger.p05016' does not depend on any axioms
'FRC.Ledger.p05019' does not depend on any axioms
'FRC.Ledger.p05027' does not depend on any axioms
'FRC.Ledger.p05028' does not depend on any axioms
'FRC.Ledger.p05031' does not depend on any axioms
'FRC.Ledger.p25010' does not depend on any axioms
'FRC.Ledger.p25014' does not depend on any axioms
'FRC.Ledger.p25015' does not depend on any axioms
'FRC.Ledger.p25048' does not depend on any axioms
'FRC.Ledger.p29006' does not depend on any axioms
'FRC.Ledger.p29007' does not depend on any axioms
'FRC.Ledger.p29010' does not depend on any axioms
'FRC.Ledger.p29011' does not depend on any axioms
'FRC.Ledger.p29012' does not depend on any axioms
'FRC.Ledger.p29014' does not depend on any axioms
'FRC.Ledger.p29015' does not depend on any axioms
'FRC.Ledger.p29016' does not depend on any axioms
'FRC.Ledger.p29022' does not depend on any axioms
'FRC.Ledger.p29024' does not depend on any axioms
'FRC.Ledger.p29026' does not depend on any axioms
'FRC.Ledger.p29027' does not depend on any axioms
'FRC.Ledger.p00003' does not depend on any axioms
'FRC.Ledger.p00004' does not depend on any axioms
'FRC.Ledger.p00162' does not depend on any axioms
'FRC.Ledger.p00163' does not depend on any axioms
'FRC.Ledger.p00164' does not depend on any axioms
'FRC.Ledger.p00188' does not depend on any axioms
'FRC.Ledger.p00197' does not depend on any axioms
'FRC.Ledger.p26038' does not depend on any axioms
'FRC.Ledger.p00015' does not depend on any axioms
'FRC.Ledger.p00165' does not depend on any axioms
'FRC.Ledger.p00166' does not depend on any axioms
'FRC.Ledger.p00168' does not depend on any axioms
'FRC.Ledger.p00170' does not depend on any axioms
'FRC.Ledger.p00021' does not depend on any axioms
'FRC.Ledger.p00028' does not depend on any axioms
'FRC.Ledger.p00034' does not depend on any axioms
'FRC.Ledger.p00040' does not depend on any axioms
'FRC.Ledger.p00139' does not depend on any axioms
'FRC.Ledger.p00150' does not depend on any axioms
'FRC.Ledger.p00151' does not depend on any axioms
'FRC.Ledger.p38001' does not depend on any axioms
'FRC.Ledger.p38002' does not depend on any axioms
'FRC.Ledger.p38003' does not depend on any axioms
'FRC.Ledger.p38004' does not depend on any axioms
'FRC.Ledger.p38006' does not depend on any axioms
'FRC.Ledger.p38007' does not depend on any axioms
'FRC.Ledger.p38008' does not depend on any axioms
'FRC.Ledger.p38009' does not depend on any axioms
'FRC.Ledger.p38010' does not depend on any axioms
'FRC.Ledger.p38011' does not depend on any axioms
'FRC.Ledger.p38012' does not depend on any axioms
'FRC.Ledger.p38013' does not depend on any axioms
'FRC.Ledger.p38015' does not depend on any axioms
'FRC.Ledger.p38016' does not depend on any axioms
'FRC.Ledger.p38018' does not depend on any axioms
'FRC.Ledger.p38019' does not depend on any axioms
'FRC.Ledger.p38020' does not depend on any axioms
'FRC.Ledger.p38021' does not depend on any axioms
'FRC.Ledger.p38025' does not depend on any axioms
'FRC.Ledger.p38026' does not depend on any axioms
'FRC.Ledger.p38030' does not depend on any axioms
'FRC.Ledger.p38031' does not depend on any axioms
'FRC.Ledger.p38032' does not depend on any axioms
'FRC.Ledger.p38033' does not depend on any axioms
'FRC.Ledger.p38036' does not depend on any axioms
'FRC.Ledger.p38037' does not depend on any axioms
'FRC.Ledger.p38044' does not depend on any axioms
'FRC.Ledger.p38046' does not depend on any axioms
'FRC.Ledger.p38048' does not depend on any axioms
'FRC.Ledger.p38054' does not depend on any axioms
'FRC.Ledger.p00052' does not depend on any axioms
'FRC.Ledger.p00055' does not depend on any axioms
'FRC.Ledger.p00056' does not depend on any axioms
'FRC.Ledger.p00058' does not depend on any axioms
'FRC.Ledger.p00147' does not depend on any axioms
'FRC.Ledger.p00154' does not depend on any axioms
'FRC.Ledger.p00176' does not depend on any axioms
'FRC.Ledger.p00199' does not depend on any axioms
'FRC.Ledger.p21001' does not depend on any axioms
'FRC.Ledger.p21009' does not depend on any axioms
'FRC.Ledger.p21016' does not depend on any axioms
'FRC.Ledger.p21017' does not depend on any axioms
'FRC.Ledger.p21018' does not depend on any axioms
'FRC.Ledger.p21020' does not depend on any axioms
'FRC.Ledger.p21021' does not depend on any axioms
'FRC.Ledger.p21022' does not depend on any axioms
'FRC.Ledger.p21023' does not depend on any axioms
'FRC.Ledger.p21024' does not depend on any axioms
'FRC.Ledger.p21026' does not depend on any axioms
'FRC.Ledger.p21030' does not depend on any axioms
'FRC.Ledger.p21031' does not depend on any axioms
'FRC.Ledger.p21035' does not depend on any axioms
'FRC.Ledger.p21036' does not depend on any axioms
'FRC.Ledger.p21040' does not depend on any axioms
'FRC.Ledger.p21041' does not depend on any axioms
'FRC.Ledger.p21043' does not depend on any axioms
'FRC.Ledger.p21055' does not depend on any axioms
'FRC.Ledger.p21062' does not depend on any axioms
'FRC.Ledger.p21064' does not depend on any axioms
'FRC.Ledger.p38014' does not depend on any axioms
'FRC.Ledger.p38022' does not depend on any axioms
'FRC.Ledger.p38027' does not depend on any axioms
'FRC.Ledger.p38029' does not depend on any axioms
'FRC.Ledger.p38050' does not depend on any axioms
'FRC.Ledger.p38053' does not depend on any axioms
'FRC.Ledger.p00191' does not depend on any axioms
'FRC.Ledger.p00194' does not depend on any axioms
'FRC.Ledger.p22002' does not depend on any axioms
'FRC.Ledger.p22017' does not depend on any axioms
'FRC.Ledger.p22018' does not depend on any axioms
'FRC.Ledger.p22019' does not depend on any axioms
'FRC.Ledger.p22020' does not depend on any axioms
'FRC.Ledger.p22021' does not depend on any axioms
'FRC.Ledger.p22022' does not depend on any axioms
'FRC.Ledger.p22023' does not depend on any axioms
'FRC.Ledger.p22024' does not depend on any axioms
'FRC.Ledger.p22025' does not depend on any axioms
'FRC.Ledger.p22026' does not depend on any axioms
'FRC.Ledger.p22029' does not depend on any axioms
'FRC.Ledger.p22030' does not depend on any axioms
'FRC.Ledger.p22031' does not depend on any axioms
'FRC.Ledger.p22032' does not depend on any axioms
'FRC.Ledger.p22033' does not depend on any axioms
'FRC.Ledger.p22034' does not depend on any axioms
'FRC.Ledger.p22035' does not depend on any axioms
'FRC.Ledger.p22036' does not depend on any axioms
'FRC.Ledger.p22037' does not depend on any axioms
'FRC.Ledger.p22038' does not depend on any axioms
'FRC.Ledger.p22039' does not depend on any axioms
'FRC.Ledger.p22040' does not depend on any axioms
'FRC.Ledger.p22041' does not depend on any axioms
'FRC.Ledger.p22042' does not depend on any axioms
'FRC.Ledger.p22043' does not depend on any axioms
'FRC.Ledger.p22044' does not depend on any axioms
'FRC.Ledger.p22045' does not depend on any axioms
'FRC.Ledger.p22046' does not depend on any axioms
'FRC.Ledger.p22047' does not depend on any axioms
'FRC.Ledger.p22048' does not depend on any axioms
'FRC.Ledger.p22049' does not depend on any axioms
'FRC.Ledger.p22050' does not depend on any axioms
'FRC.Ledger.p22051' does not depend on any axioms
'FRC.Ledger.p22052' does not depend on any axioms
'FRC.Ledger.p22053' does not depend on any axioms
'FRC.Ledger.p22054' does not depend on any axioms
'FRC.Ledger.p22055' does not depend on any axioms
'FRC.Ledger.p22056' does not depend on any axioms
'FRC.Ledger.p00081' does not depend on any axioms
'FRC.Ledger.p00155' does not depend on any axioms
'FRC.Ledger.p27020' does not depend on any axioms
'FRC.Ledger.p20008' does not depend on any axioms
'FRC.Ledger.p20009' does not depend on any axioms
'FRC.Ledger.p20011' does not depend on any axioms
'FRC.Ledger.p20012' does not depend on any axioms
'FRC.Ledger.p20013' does not depend on any axioms
'FRC.Ledger.p20014' does not depend on any axioms
'FRC.Ledger.p20015' does not depend on any axioms
'FRC.Ledger.p20016' does not depend on any axioms
'FRC.Ledger.p20017' does not depend on any axioms
'FRC.Ledger.p20029' does not depend on any axioms
'FRC.Ledger.p20032' does not depend on any axioms
'FRC.Ledger.p20043' does not depend on any axioms
'FRC.Ledger.p20047' does not depend on any axioms
'FRC.Ledger.p20079' does not depend on any axioms
'FRC.Ledger.p20081' does not depend on any axioms
'FRC.Ledger.p20083' does not depend on any axioms
'FRC.Ledger.p26009' does not depend on any axioms
'FRC.Ledger.p26011' does not depend on any axioms
'FRC.Ledger.p26025' does not depend on any axioms
'FRC.Ledger.p26027' does not depend on any axioms
'FRC.Ledger.p26030' does not depend on any axioms
'FRC.Ledger.p26031' does not depend on any axioms
'FRC.Ledger.p26041' does not depend on any axioms
'FRC.Ledger.p26042' does not depend on any axioms
'FRC.Ledger.p26043' does not depend on any axioms
'FRC.Ledger.p26044' does not depend on any axioms
'FRC.Shell.meridian' does not depend on any axioms
'FRC.Shell.scale' does not depend on any axioms
'FRC.Shell.map_scale_aux' does not depend on any axioms
'FRC.Shell.meridian_scale' does not depend on any axioms
'FRC.Shell.ofNat_succ' does not depend on any axioms
'FRC.Shell.meridian_step' does not depend on any axioms
'FRC.Shell.scale_periodic' does not depend on any axioms
'FRC.Shell.ladder13' does not depend on any axioms
'FRC.Fourier.p06009' does not depend on any axioms
'FRC.Fourier.p06010' does not depend on any axioms
'FRC.Fourier.p06012' does not depend on any axioms
'FRC.Fourier.p06013' does not depend on any axioms
'FRC.Fourier.p06014' does not depend on any axioms
'FRC.Fourier.p06016' does not depend on any axioms
'FRC.Fourier.p06017' does not depend on any axioms
'FRC.Fourier.p06018' does not depend on any axioms
'FRC.Fourier.p06019' does not depend on any axioms
'FRC.Fourier.p06020' does not depend on any axioms
'FRC.Fourier.p06021' does not depend on any axioms
'FRC.Fourier.p06022' does not depend on any axioms
'FRC.Fourier.p06023' does not depend on any axioms
'FRC.Fourier.p06052' does not depend on any axioms
'FRC.Fourier.p06024' does not depend on any axioms
'FRC.Fourier.p06025' does not depend on any axioms
'FRC.Fourier.p06027' does not depend on any axioms
'FRC.Fourier.p06053' does not depend on any axioms
'FRC.Fourier.p06031' does not depend on any axioms
'FRC.Fourier.p06032' does not depend on any axioms
'FRC.Fourier.p06034' does not depend on any axioms
'FRC.Fourier.p06035' does not depend on any axioms
'FRC.Fourier.p06036' does not depend on any axioms
'FRC.Fourier.p06050' does not depend on any axioms
'FRC.Fourier.p06054' does not depend on any axioms
'FRC.Fourier.p06056' does not depend on any axioms
'FRC.Algebra.p01004' does not depend on any axioms
'FRC.Algebra.p01005' does not depend on any axioms
'FRC.Algebra.p01006' does not depend on any axioms
'FRC.Algebra.p01009' does not depend on any axioms
'FRC.Algebra.p01011' does not depend on any axioms
'FRC.Algebra.p01013' does not depend on any axioms
'FRC.Algebra.p01015' does not depend on any axioms
'FRC.Algebra.p01019' does not depend on any axioms
'FRC.Algebra.p01026' does not depend on any axioms
'FRC.Algebra.p01020' does not depend on any axioms
'FRC.Epi.fact' does not depend on any axioms
'FRC.Epi.dr' does not depend on any axioms
'FRC.Epi.dr_zero' does not depend on any axioms
'FRC.Epi.dr_one' does not depend on any axioms
'FRC.Epi.dr_add_two' does not depend on any axioms
'FRC.Epi.kur' does not depend on any axioms
'FRC.Epi.cb' does not depend on any axioms
'FRC.Epi.factS' does not depend on any axioms
'FRC.Epi.factS_eq' does not depend on any axioms
'FRC.Epi.kurS' does not depend on any axioms
'FRC.Epi.altS' does not depend on any axioms
'FRC.Epi.kurS_eq' does not depend on any axioms
'FRC.Epi.invSearch' does not depend on any axioms
'FRC.Epi.inv' does not depend on any axioms
'FRC.Epi.readE' does not depend on any axioms
'FRC.Epi.readW' does not depend on any axioms
'FRC.Epi.readV' does not depend on any axioms
'FRC.Epi.neg_one_pow_succ' does not depend on any axioms
'FRC.Epi.dr_succ' does not depend on any axioms
'FRC.Epi.four_kappa_add_one_mod_two' does not depend on any axioms
'FRC.Epi.neg_one_pow_p' does not depend on any axioms
'FRC.Epi.dr_antiperiodic' does not depend on any axioms
'FRC.Epi.tower_e_exact' does not depend on any axioms
'FRC.Epi.odd_of_coprime_four' does not depend on any axioms
'FRC.Epi.mod_four_of_odd' does not depend on any axioms
'FRC.Epi.orientation_transport' does not depend on any axioms
'FRC.Epi.wrap_free' does not depend on any axioms
'FRC.Epi.coincidence13' does not depend on any axioms
'FRC.Epi.terminal13' does not depend on any axioms
'FRC.Epi.residue_line_e13' does not depend on any axioms
'FRC.Epi.residue_line_pi13' does not depend on any axioms
'FRC.Epi.revivals13' does not depend on any axioms
'FRC.Epi.kurepa_alt_values' does not depend on any axioms
'FRC.Epi.noDivisorFrom' does not depend on any axioms
'FRC.Epi.isPrimeB' does not depend on any axioms
'FRC.Epi.all_append_nat' does not depend on any axioms
'FRC.Epi.filter_cons_true_nat' does not depend on any axioms
'FRC.Epi.filter_cons_false_nat' does not depend on any axioms
'FRC.Epi.filter_append_nat' does not depend on any axioms
'FRC.Epi.length_append_nat' does not depend on any axioms
'FRC.Epi.blindFold' does not depend on any axioms
'FRC.Epi.blindCount' does not depend on any axioms
'FRC.Epi.primes1000to1300' does not depend on any axioms
'FRC.Epi.blind_census' does not depend on any axioms
'FRC.Epi.sigmaFold' does not depend on any axioms
'FRC.Epi.sigmaZero' does not depend on any axioms
'FRC.Epi.oddPrimesC1' does not depend on any axioms
'FRC.Epi.oddPrimesC2' does not depend on any axioms
'FRC.Epi.oddPrimesC3' does not depend on any axioms
'FRC.Epi.oddPrimesC4' does not depend on any axioms
'FRC.Epi.oddPrimesC5' does not depend on any axioms
'FRC.Epi.oddPrimesC6' does not depend on any axioms
'FRC.Epi.oddPrimesC7' does not depend on any axioms
'FRC.Epi.oddPrimesBelow3000' does not depend on any axioms
'FRC.Epi.oddPrimesBelow3000_complete' does not depend on any axioms
'FRC.Epi.sigma_vanishes_c1' does not depend on any axioms
'FRC.Epi.sigma_vanishes_c2' does not depend on any axioms
'FRC.Epi.sigma_vanishes_c3' does not depend on any axioms
'FRC.Epi.sigma_vanishes_c4' does not depend on any axioms
'FRC.Epi.sigma_vanishes_c5' does not depend on any axioms
'FRC.Epi.sigma_vanishes_c6' does not depend on any axioms
'FRC.Epi.sigma_vanishes_c7' does not depend on any axioms
'FRC.Epi.sigma_vanishes_all' does not depend on any axioms
'FRC.Epi.primes5to300' does not depend on any axioms
'FRC.Epi.sigma_vanishes_mod_sq' does not depend on any axioms
'FRC.Epi.fermatQuotient4' does not depend on any axioms
'FRC.Epi.invariants_13_1093' does not depend on any axioms
'FRC.Epi.arcsinChain' does not depend on any axioms
'FRC.Epi.piLo' does not depend on any axioms
'FRC.Epi.piHi' does not depend on any axioms
'FRC.Epi.tailWithin' does not depend on any axioms
'FRC.Epi.arcsin_tail_bound' does not depend on any axioms
'FRC.Epi.noCalibration' does not depend on any axioms
'FRC.Epi.shellsQ1' does not depend on any axioms
'FRC.Epi.shellsQ2' does not depend on any axioms
'FRC.Epi.shellsQ3' does not depend on any axioms
'FRC.Epi.shellsQ4' does not depend on any axioms
'FRC.Epi.shells8009' does not depend on any axioms
'FRC.Epi.shells8009_complete' does not depend on any axioms
'FRC.Epi.no_exact_calibration' does not depend on any axioms
'FRC.Epi.readoutWithin' does not depend on any axioms
'FRC.Epi.readout_e_core' does not depend on any axioms
'FRC.Epi.derangement_cost_core' does not depend on any axioms
'FRC.Epi.calibrated_shell_core' does not depend on any axioms
'FRC.Epi.primeFactorsFrom' does not depend on any axioms
'FRC.Epi.primeFactors' does not depend on any axioms
'FRC.Epi.isPrimRoot' does not depend on any axioms
'FRC.Epi.primRootFrom' does not depend on any axioms
'FRC.Epi.smallestPrimRoot' does not depend on any axioms
'FRC.Epi.ctrAbs' does not depend on any axioms
'FRC.Epi.heightSearch' does not depend on any axioms
'FRC.Epi.height' does not depend on any axioms
'FRC.Epi.expUnit' does not depend on any axioms
'FRC.Epi.expUnitConj' does not depend on any axioms
'FRC.Epi.heightE' does not depend on any axioms
'FRC.Epi.height_run_q1' does not depend on any axioms
'FRC.Epi.height_run_q2' does not depend on any axioms
'FRC.Epi.height_run_q3' does not depend on any axioms
'FRC.Epi.height_run_q4' does not depend on any axioms
'FRC.Epi.height_run' does not depend on any axioms
'FRC.Epi.pin_contrast' does not depend on any axioms
'FRC.Epi.ofNat_self' does not depend on any axioms
'FRC.Epi.ofNat_add_self' does not depend on any axioms
'FRC.Epi.p13009' does not depend on any axioms
'FRC.Epi.p13010' does not depend on any axioms
'FRC.Epi.p13020' does not depend on any axioms
'FRC.Epi.p13021' does not depend on any axioms
'FRC.Epi.p13024' does not depend on any axioms
'FRC.Epi.p13026' does not depend on any axioms
'FRC.Epi.p13028' does not depend on any axioms
'FRC.Epi.p13029' does not depend on any axioms
'FRC.Epi.p13030' does not depend on any axioms
'FRC.Epi.p13031' does not depend on any axioms
'FRC.Epi.p13032' does not depend on any axioms
'FRC.Epi.p13033' does not depend on any axioms
'FRC.Epi.p13034' does not depend on any axioms
'FRC.Epi.p13038' does not depend on any axioms
'FRC.Epi.p13039' does not depend on any axioms
'FRC.Epi.p13040' does not depend on any axioms
'FRC.Epi.p13041' does not depend on any axioms
'FRC.Epi.p13044' does not depend on any axioms
'FRC.Epi.p13045' does not depend on any axioms
'FRC.Epi.p13069' does not depend on any axioms
'FRC.Epi.p13048' does not depend on any axioms
'FRC.Epi.p13049' does not depend on any axioms
'FRC.Epi.p13050' does not depend on any axioms
'FRC.Epi.p13051' does not depend on any axioms
'FRC.Epi.p13068' does not depend on any axioms
'FRC.Epi.p13052' does not depend on any axioms
'FRC.Epi.p13053' does not depend on any axioms
'FRC.Epi.p13054' does not depend on any axioms
'FRC.Epi.p13056' does not depend on any axioms
'FRC.Epi.p13057' does not depend on any axioms
'FRC.Dimensions.Dom.ext' does not depend on any axioms
'FRC.Dimensions.Dom.r_congr' does not depend on any axioms
'FRC.Dimensions.Dom.s_congr' does not depend on any axioms
'FRC.Dimensions.Dom.mul' does not depend on any axioms
'FRC.Dimensions.Dom.one' does not depend on any axioms
'FRC.Dimensions.Dom.inv' does not depend on any axioms
'FRC.Dimensions.Dom.pow' does not depend on any axioms
'FRC.Dimensions.Dom.mul_def' does not depend on any axioms
'FRC.Dimensions.Dom.one_def' does not depend on any axioms
'FRC.Dimensions.Dom.inv_def' does not depend on any axioms
'FRC.Dimensions.Dom.pow_zero' does not depend on any axioms
'FRC.Dimensions.Dom.pow_succ' does not depend on any axioms
'FRC.Dimensions.Dom.mul_comm' does not depend on any axioms
'FRC.Dimensions.Dom.mul_assoc' does not depend on any axioms
'FRC.Dimensions.Dom.one_mul' does not depend on any axioms
'FRC.Dimensions.Dom.mul_one' does not depend on any axioms
'FRC.Dimensions.Dom.mul_inv' does not depend on any axioms
'FRC.Dimensions.Dom.inv_mul' does not depend on any axioms
'FRC.Dimensions.Dom.inv_inv' does not depend on any axioms
'FRC.Dimensions.Dom.pow_add' does not depend on any axioms
'FRC.Dimensions.Dom.pow_eq' does not depend on any axioms
'FRC.Dimensions.Dom.mul_pow' does not depend on any axioms
'FRC.Dimensions.instDecForallDom' does not depend on any axioms
'FRC.Dimensions.instPosFour' does not depend on any axioms
'FRC.Dimensions.L' does not depend on any axioms
'FRC.Dimensions.T' does not depend on any axioms
'FRC.Dimensions.flag' does not depend on any axioms
'FRC.Dimensions.energy' does not depend on any axioms
'FRC.Dimensions.mom' does not depend on any axioms
'FRC.Dimensions.deltaC' does not depend on any axioms
'FRC.Dimensions.flag_eq_pow' does not depend on any axioms
'FRC.Dimensions.val_ofNat_mul_kappa' does not depend on any axioms
'FRC.Dimensions.ofNat_kappa_ne_zero' does not depend on any axioms
'FRC.Dimensions.ofNat_two_kappa_ne_zero' does not depend on any axioms
'FRC.Dimensions.ofNat_three_kappa_ne_zero' does not depend on any axioms
'FRC.Dimensions.ofNat_four_kappa' does not depend on any axioms
'FRC.Dimensions.flag_pow' does not depend on any axioms
'FRC.Dimensions.flag_pow_four' does not depend on any axioms
'FRC.Dimensions.flag_order_four' does not depend on any axioms
'FRC.Dimensions.flag_inv' does not depend on any axioms
'FRC.Dimensions.no_flag_of_space' does not depend on any axioms
'FRC.Dimensions.order_two_13' does not depend on any axioms
'FRC.Dimensions.order_four_13' does not depend on any axioms
'FRC.Dimensions.meridian_transport' does not depend on any axioms
'FRC.Dimensions.deltaC_involutive' does not depend on any axioms
'FRC.Dimensions.record_values' does not depend on any axioms
'FRC.Dimensions.flagged_readings' does not depend on any axioms
'FRC.Dimensions.G_unique' does not depend on any axioms
'FRC.Dimensions.linkage' does not depend on any axioms
'FRC.Dimensions.carrier233' does not depend on any axioms
'FRC.Dimensions.carrierLab' does not depend on any axioms
'FRC.Dimensions.admissible' does not depend on any axioms
'FRC.Dimensions.minimality' does not depend on any axioms
'FRC.Dimensions.realized13' does not depend on any axioms
'FRC.Dimensions.flag_inaccessible13' does not depend on any axioms
'FRC.Dimensions.window_ladder' does not depend on any axioms
'FRC.Dimensions.resolution_floor' does not depend on any axioms
'FRC.Dimensions.recovery13' does not depend on any axioms
'FRC.Dimensions.energy_momentum13' does not depend on any axioms
'FRC.Dimensions.charge13' does not depend on any axioms
'FRC.Dimensions.charge29' does not depend on any axioms
'FRC.Dimensions.no_charge17' does not depend on any axioms
'FRC.Dimensions.no_charge41' does not depend on any axioms
'FRC.Dimensions.isPrime' does not depend on any axioms
'FRC.Dimensions.root_pair' does not depend on any axioms
'FRC.Dimensions.decForallLT' does not depend on any axioms
'FRC.Dimensions.instDecForallLT' does not depend on any axioms
'FRC.Dimensions.instDecForallShell' does not depend on any axioms
'FRC.Dimensions.p10012' does not depend on any axioms
'FRC.Dimensions.p10013' does not depend on any axioms
'FRC.Dimensions.p10016' does not depend on any axioms
'FRC.Dimensions.p10017' does not depend on any axioms
'FRC.Dimensions.p10018' does not depend on any axioms
'FRC.Dimensions.p10019' does not depend on any axioms
'FRC.Dimensions.p10022' does not depend on any axioms
'FRC.Dimensions.p10027' does not depend on any axioms
'FRC.Dimensions.p10028' does not depend on any axioms
'FRC.Dimensions.p10032' does not depend on any axioms
'FRC.Dimensions.p10034' does not depend on any axioms
'FRC.Dimensions.p10035' does not depend on any axioms
'FRC.Dimensions.p10036' does not depend on any axioms
'FRC.Dimensions.p10047' does not depend on any axioms
'FRC.Dimensions.p10037' does not depend on any axioms
'FRC.Dimensions.p10038' does not depend on any axioms
'FRC.Dimensions.p10039' does not depend on any axioms
'FRC.Dimensions.p10052' does not depend on any axioms
'FRC.Dimensions.p10053' does not depend on any axioms
'FRC.Dimensions.p10054' does not depend on any axioms
'FRC.Dimensions.p10048' does not depend on any axioms
'FRC.Dimensions.p10049' does not depend on any axioms
'FRC.Dimensions.p10050' does not depend on any axioms
'FRC.Dimensions.p10051' does not depend on any axioms
'FRC.Shell.sum_split' does not depend on any axioms
'FRC.Shell.sum_triangle' does not depend on any axioms
'FRC.Shell.Poly.Bound' does not depend on any axioms
'FRC.Shell.Poly.mul' does not depend on any axioms
'FRC.Shell.Poly.eval' does not depend on any axioms
'FRC.Shell.Poly.linear' does not depend on any axioms
'FRC.Shell.Poly.xpx' does not depend on any axioms
'FRC.Shell.Poly.eval_congr' does not depend on any axioms
'FRC.Shell.Poly.eval_bound' does not depend on any axioms
'FRC.Shell.Poly.mul_bound' does not depend on any axioms
'FRC.Shell.Poly.eval_mul' does not depend on any axioms
'FRC.Shell.Poly.linear_bound' does not depend on any axioms
'FRC.Shell.Poly.mul_linear_zero' does not depend on any axioms
'FRC.Shell.Poly.mul_linear_succ' does not depend on any axioms
'FRC.Shell.Poly.quotLinear' does not depend on any axioms
'FRC.Shell.Poly.quot_linear_spec' does not depend on any axioms
'FRC.Shell.Poly.eval_linear' does not depend on any axioms
'FRC.Shell.Poly.eval_mul_linear' does not depend on any axioms
'FRC.Shell.Poly.root_bound_of' does not depend on any axioms
'FRC.Shell.Poly.Frame.ofNat_inj_lt' does not depend on any axioms
'FRC.Shell.Frame.sread' does not depend on any axioms
'FRC.Shell.Frame.sadd' does not depend on any axioms
'FRC.Shell.Frame.sneg' does not depend on any axioms
'FRC.Shell.Frame.smul' does not depend on any axioms
'FRC.Shell.Frame.snorm' does not depend on any axioms
'FRC.Shell.Frame.prod_ext' does not depend on any axioms
'FRC.Shell.Frame.sread_add' does not depend on any axioms
'FRC.Shell.Frame.sread_neg' does not depend on any axioms
'FRC.Shell.Frame.sread_mul' does not depend on any axioms
'FRC.Shell.Frame.sread_norm' does not depend on any axioms
'FRC.Shell.Frame.SBound' does not depend on any axioms
'FRC.Shell.Frame.sneg_bound' does not depend on any axioms
'FRC.Shell.Frame.smul_bound' does not depend on any axioms
'FRC.Shell.Frame.sum4_bound' does not depend on any axioms
'FRC.Shell.Frame.snorm_bound' does not depend on any axioms
'FRC.Shell.Frame.sread_inj' does not depend on any axioms
'FRC.Shell.Frame.IQuat.mul' does not depend on any axioms
'FRC.Shell.Frame.IQuat.read' does not depend on any axioms
'FRC.Shell.Frame.IQuat.norm' does not depend on any axioms
'FRC.Shell.Frame.QBound' does not depend on any axioms
'FRC.Shell.Frame.IQuat.ext'' does not depend on any axioms
'FRC.Shell.Frame.read_mul' does not depend on any axioms
'FRC.Shell.Frame.read_norm' does not depend on any axioms
'FRC.Shell.Frame.norm_bound' does not depend on any axioms
'FRC.Shell.Frame.quaternion_window' does not depend on any axioms
'FRC.Shell.Frame.rot_pure' does not depend on any axioms
'FRC.Shell.Frame.rot_cayley' does not depend on any axioms
'FRC.Shell.Frame.half_turn' does not depend on any axioms
'FRC.Shell.Frame.cayley_key' does not depend on any axioms
'FRC.Shell.Frame.add_neg_q' does not depend on any axioms
'FRC.Shell.Frame.key_zero' does not depend on any axioms
'FRC.Shell.Frame.cayley_inj' does not depend on any axioms
'FRC.Shell.Frame.one_add_mul' does not depend on any axioms
'FRC.Shell.Frame.bracket' does not depend on any axioms
'FRC.Shell.Frame.rot_mul' does not depend on any axioms
'FRC.Shell.Frame.rot_smul' does not depend on any axioms
'FRC.Shell.Frame.one_add_mul_half' does not depend on any axioms
'FRC.Shell.Frame.rot_neg' does not depend on any axioms
'FRC.Shell.Frame.smul_sc_add' does not depend on any axioms
'FRC.Shell.Frame.smul_one_q' does not depend on any axioms
'FRC.Shell.Frame.smul_smul_q' does not depend on any axioms
'FRC.Shell.Frame.conjBy_smul' does not depend on any axioms
'FRC.Shell.Frame.inv_chain' does not depend on any axioms
'FRC.Shell.Frame.compose' does not depend on any axioms
'FRC.Shell.Frame.add_cancel_q' does not depend on any axioms
'FRC.Shell.Frame.cayley_trivial_id' does not depend on any axioms
'FRC.Shell.Frame.rot_trivial' does not depend on any axioms
'FRC.Algebra.p01030' does not depend on any axioms
'FRC.Algebra.p01032' does not depend on any axioms
'FRC.Algebra.p01033' does not depend on any axioms
'FRC.Shell.Frame.mul_mul_mul_comm' does not depend on any axioms
'FRC.Causality.p03006' does not depend on any axioms
'FRC.Causality.p03007' does not depend on any axioms
'FRC.Causality.p03008' does not depend on any axioms
'FRC.Causality.p03009' does not depend on any axioms
'FRC.Causality.p03013' does not depend on any axioms
'FRC.Causality.p03014' does not depend on any axioms
'FRC.Causality.p03017' does not depend on any axioms
'FRC.Representation.adequate_inj' does not depend on any axioms
'FRC.Representation.transition' does not depend on any axioms
'FRC.Representation.transition_spec' does not depend on any axioms
'FRC.Representation.transitionBij' does not depend on any axioms
'FRC.Representation.transition_unique' does not depend on any axioms
'FRC.Representation.iota' does not depend on any axioms
'FRC.Representation.iota_inj' does not depend on any axioms
'FRC.Representation.canonical_chart' does not depend on any axioms
'FRC.Representation.chart_inj' does not depend on any axioms
'FRC.Representation.transition_graph' does not depend on any axioms
'FRC.Representation.lift' does not depend on any axioms
'FRC.Representation.lift_g' does not depend on any axioms
'FRC.Representation.lift_unique' does not depend on any axioms
'FRC.Representation.consistency' does not depend on any axioms
'FRC.Representation.three_pow_mod_two' does not depend on any axioms
'FRC.Representation.two_mul_mod_two' does not depend on any axioms
'FRC.Representation.three_pow_inj' does not depend on any axioms
'FRC.Representation.godel2_inj' does not depend on any axioms
'FRC.Representation.mod_injective' does not depend on any axioms
'FRC.Representation.Shell.charChart' does not depend on any axioms
'FRC.Representation.Shell.charChart_shift' does not depend on any axioms
'FRC.Representation.Shell.charChart_norm' does not depend on any axioms
'FRC.Representation.p04008' does not depend on any axioms
'FRC.Representation.p04009' does not depend on any axioms
'FRC.Representation.p04010' does not depend on any axioms
'FRC.Representation.p04011' does not depend on any axioms
'FRC.Representation.p04012' does not depend on any axioms
'FRC.Representation.p04013' does not depend on any axioms
'FRC.Representation.p04014' does not depend on any axioms
'FRC.Representation.p04015' does not depend on any axioms
'FRC.Representation.p04018' does not depend on any axioms
'FRC.Representation.p04020' does not depend on any axioms
'FRC.Reductio.num' does not depend on any axioms
'FRC.Reductio.bex' does not depend on any axioms
'FRC.Reductio.prime' does not depend on any axioms
'FRC.Reductio.even0' does not depend on any axioms
'FRC.Reductio.goldbach' does not depend on any axioms
'FRC.Reductio.goldbach_ten' does not depend on any axioms
'FRC.Reductio.goldbach_ten_bound' does not depend on any axioms
'FRC.Reductio.goldbach_ten_frame' does not depend on any axioms
'FRC.Reductio.goldbach_ten_stable' does not depend on any axioms
'FRC.Reductio.obstruction_five' does not depend on any axioms
'FRC.Reductio.mx' does not depend on any axioms
'FRC.Reductio.le_mx_left' does not depend on any axioms
'FRC.Reductio.le_mx_right' does not depend on any axioms
'FRC.Reductio.lt_of_mx_lt_left' does not depend on any axioms
'FRC.Reductio.lt_of_mx_lt_right' does not depend on any axioms
'FRC.Reductio.Term' does not depend on any axioms
'FRC.Reductio.Form' does not depend on any axioms
'FRC.Reductio.cons' does not depend on any axioms
'FRC.Reductio.evalT' does not depend on any axioms
'FRC.Reductio.allBelow' does not depend on any axioms
'FRC.Reductio.evalF' does not depend on any axioms
'FRC.Reductio.evalT' does not depend on any axioms
'FRC.Reductio.evalF' does not depend on any axioms
'FRC.Reductio.boundT' does not depend on any axioms
'FRC.Reductio.maxBelow' does not depend on any axioms
'FRC.Reductio.boundF' does not depend on any axioms
'FRC.Reductio.le_maxBelow' does not depend on any axioms
'FRC.Reductio.allBelow_congr' does not depend on any axioms
'FRC.Reductio.evalT_frame' does not depend on any axioms
'FRC.Reductio.stable' does not depend on any axioms
'FRC.Reductio.records' does not depend on any axioms
'FRC.Reductio.records_lt' does not depend on any axioms
'FRC.Reductio.no_mirror' does not depend on any axioms
'FRC.Reductio.iter' does not depend on any axioms
'FRC.Reductio.iter_lt' does not depend on any axioms
'FRC.Reductio.iter_add' does not depend on any axioms
'FRC.Reductio.repeat_below' does not depend on any axioms
'FRC.Reductio.sub_pos' does not depend on any axioms
'FRC.Reductio.eventually_periodic' does not depend on any axioms
'FRC.Reductio.halts_iff_halts_below' does not depend on any axioms
'FRC.Reductio.cantor_finite' does not depend on any axioms
'FRC.Reductio.leastBelow' does not depend on any axioms
'FRC.Reductio.leastBelow_some' does not depend on any axioms
'FRC.Reductio.leastBelow_spec' does not depend on any axioms
'FRC.Reductio.leastBelow_congr' does not depend on any axioms
'FRC.Reductio.p05010' does not depend on any axioms
'FRC.Reductio.p05013' does not depend on any axioms
'FRC.Reductio.p05016' does not depend on any axioms
'FRC.Reductio.p05019' does not depend on any axioms
'FRC.Reductio.p05027' does not depend on any axioms
'FRC.Reductio.p05028' does not depend on any axioms
'FRC.Reductio.p05030' does not depend on any axioms
'FRC.Reductio.p05031' does not depend on any axioms
'FRC.Godel.val' does not depend on any axioms
'FRC.Godel.Agree' does not depend on any axioms
'FRC.Godel.leaves' does not depend on any axioms
'FRC.Godel.lookups' does not depend on any axioms
'FRC.Godel.trace_transport' does not depend on any axioms
'FRC.Godel.wrap_equation' does not depend on any axioms
'FRC.Godel.lookups_succ' does not depend on any axioms
'FRC.Godel.value_leaves' does not depend on any axioms
'FRC.Godel.equal_leaves_equal_value' does not depend on any axioms
'FRC.Godel.records_lt' does not depend on any axioms
'FRC.Godel.reach_vanishes' does not depend on any axioms
'FRC.Godel.tval' does not depend on any axioms
'FRC.Godel.holds' does not depend on any axioms
'FRC.Godel.occT' does not depend on any axioms
'FRC.Godel.occ' does not depend on any axioms
'FRC.Godel.tsize' does not depend on any axioms
'FRC.Godel.size' does not depend on any axioms
'FRC.Godel.tval_congr' does not depend on any axioms
'FRC.Godel.holds_congr' does not depend on any axioms
'FRC.Godel.upd' does not depend on any axioms
'FRC.Godel.mention' does not depend on any axioms
'FRC.Godel.tcount_le' does not depend on any axioms
'FRC.Godel.fcount_le' does not depend on any axioms
'FRC.Godel.arity_le_size' does not depend on any axioms
'FRC.Godel.mention_cost' does not depend on any axioms
'FRC.Godel.fcount_lt' does not depend on any axioms
'FRC.Godel.arity_lt_size' does not depend on any axioms
'FRC.Godel.mention_cost_lt' does not depend on any axioms
'FRC.Godel.sub_size' does not depend on any axioms
'FRC.Godel.no_self_reading' does not depend on any axioms
'FRC.Godel.ex' does not depend on any axioms
'FRC.Godel.exBlock' does not depend on any axioms
'FRC.Godel.size_exBlock' does not depend on any axioms
'FRC.Godel.template_size' does not depend on any axioms
'FRC.Godel.no_template' does not depend on any axioms
'FRC.Godel.split_scale' does not depend on any axioms
'FRC.Godel.direct' does not depend on any axioms
'FRC.Godel.paired' does not depend on any axioms
'FRC.Godel.prefix_simulation' does not depend on any axioms
'FRC.Godel.prefix_simulation_closed' does not depend on any axioms
'FRC.Godel.or_intro_left' does not depend on any axioms
'FRC.Godel.or_intro_right' does not depend on any axioms
'FRC.Godel.and_true'' does not depend on any axioms
'FRC.Godel.and_false'' does not depend on any axioms
'FRC.Godel.and_self'' does not depend on any axioms
'FRC.Godel.or_false'' does not depend on any axioms
'FRC.Godel.and_assoc'' does not depend on any axioms
'FRC.Godel.inj_onto' does not depend on any axioms
'FRC.Godel.no_finite_successor' does not depend on any axioms
'FRC.Godel.part_collides' does not depend on any axioms
'FRC.Godel.sentences_outnumber' does not depend on any axioms
'FRC.Godel.count' does not depend on any axioms
'FRC.Godel.count_full' does not depend on any axioms
'FRC.Godel.cond_or_le' does not depend on any axioms
'FRC.Godel.count_or_le' does not depend on any axioms
'FRC.Godel.count_shift' does not depend on any axioms
'FRC.Godel.count_false' does not depend on any axioms
'FRC.Godel.count_single' does not depend on any axioms
'FRC.Godel.count_shift_by' does not depend on any axioms
'FRC.Godel.dense_coding' does not depend on any axioms
'FRC.Godel.pow_lt_pow_base' does not depend on any axioms
'FRC.Godel.digit_bound' does not depend on any axioms
'FRC.Godel.anyBelow' does not depend on any axioms
'FRC.Godel.anyBelow_congr' does not depend on any axioms
'FRC.Godel.anyBelow_false' does not depend on any axioms
'FRC.Godel.allBelow_const' does not depend on any axioms
'FRC.Godel.anyBelow_and_const' does not depend on any axioms
'FRC.Godel.allBelow_and_const' does not depend on any axioms
'FRC.Godel.anyBelow_pick' does not depend on any axioms
'FRC.Godel.p25010' does not depend on any axioms
'FRC.Godel.p25014' does not depend on any axioms
'FRC.Godel.p25015' does not depend on any axioms
'FRC.Godel.p25018' does not depend on any axioms
'FRC.Godel.p25019' does not depend on any axioms
'FRC.Godel.p25020' does not depend on any axioms
'FRC.Godel.p25023' does not depend on any axioms
'FRC.Godel.p25024' does not depend on any axioms
'FRC.Godel.p25025' does not depend on any axioms
'FRC.Godel.p25048' does not depend on any axioms
'FRC.Godel.p25031' does not depend on any axioms
'FRC.Finitism.p29006' does not depend on any axioms
'FRC.Finitism.p25010' does not depend on any axioms
'FRC.Finitism.p29007' does not depend on any axioms
'FRC.Finitism.p29010' does not depend on any axioms
'FRC.Finitism.p29011' does not depend on any axioms
'FRC.Finitism.p29012' does not depend on any axioms
'FRC.Finitism.p29014' does not depend on any axioms
'FRC.Finitism.p29015' does not depend on any axioms
'FRC.Finitism.p29016' does not depend on any axioms
'FRC.Finitism.p05013' does not depend on any axioms
'FRC.Finitism.p29022' does not depend on any axioms
'FRC.Finitism.p29024' does not depend on any axioms
'FRC.Finitism.p29026' does not depend on any axioms
'FRC.Finitism.p29027' does not depend on any axioms
'FRC.Geometry.euler_characteristic' does not depend on any axioms
'FRC.Geometry.fixed_shell_gap' does not depend on any axioms
'FRC.Geometry.fixed_shell_bound' does not depend on any axioms
'FRC.Geometry.fixed_shell_bound_lt_one' does not depend on any axioms
'FRC.Geometry.Adj' does not depend on any axioms
'FRC.Geometry.rho' does not depend on any axioms
'FRC.Geometry.rho_adj_iff' does not depend on any axioms
'FRC.Geometry.rotation_adj' does not depend on any axioms
'FRC.Geometry.label' does not depend on any axioms
'FRC.Geometry.label_covariance' does not depend on any axioms
'FRC.Geometry.p02007' does not depend on any axioms
'FRC.Geometry.p02013' does not depend on any axioms
'FRC.Geometry.p02014' does not depend on any axioms
'FRC.Geometry.p02015' does not depend on any axioms
'FRC.Geometry.p02017' does not depend on any axioms
'FRC.Geometry.p02018' does not depend on any axioms
'FRC.Geometry.p02019' does not depend on any axioms
'FRC.Geometry.p02023' does not depend on any axioms
'FRC.Geometry.p02025' does not depend on any axioms
'FRC.Geometry.p02027' does not depend on any axioms
'FRC.Geometry.p02028' does not depend on any axioms
'FRC.Geometry.p02029' does not depend on any axioms
'FRC.Complex.vtx' does not depend on any axioms
'FRC.Complex.south' does not depend on any axioms
'FRC.Complex.faces' does not depend on any axioms
'FRC.Complex.sides' does not depend on any axioms
'FRC.Complex.vertexCount' does not depend on any axioms
'FRC.Complex.withSides' does not depend on any axioms
'FRC.Complex.adjacentAt' does not depend on any axioms
'FRC.Complex.nextFaces' does not depend on any axioms
'FRC.Complex.walk' does not depend on any axioms
'FRC.Complex.linkIsCycle' does not depend on any axioms
'FRC.Complex.count' does not depend on any axioms
'FRC.Complex.edgesInTwoFaces' does not depend on any axioms
'FRC.Complex.closed' does not depend on any axioms
'FRC.Complex.rhoV' does not depend on any axioms
'FRC.Complex.sigmaV' does not depend on any axioms
'FRC.Complex.cellularMap' does not depend on any axioms
'FRC.Complex.cellular' does not depend on any axioms
'FRC.Complex.poleExchange' does not depend on any axioms
'FRC.Complex.counts13' does not depend on any axioms
'FRC.Complex.closed5' does not depend on any axioms
'FRC.Complex.closed13' does not depend on any axioms
'FRC.Complex.closed17' does not depend on any axioms
'FRC.Complex.facesOpen' does not depend on any axioms
'FRC.Complex.open13' does not depend on any axioms
'FRC.Complex.census13' does not depend on any axioms
'FRC.Geometry.p02008' does not depend on any axioms
'FRC.Geometry.p02010' does not depend on any axioms
'FRC.Geometry.p02011' does not depend on any axioms
'FRC.Geometry.p02012' does not depend on any axioms
'FRC.Shell.generates13' does not depend on any axioms
'FRC.Shell.s13_datum' does not depend on any axioms
'FRC.Shell.s13_euler' does not depend on any axioms
'FRC.Shell.frame17a' does not depend on any axioms
'FRC.Shell.frame17b' does not depend on any axioms
'FRC.Shell.s17_orientation' does not depend on any axioms
'FRC.Shell.frame29' does not depend on any axioms
'FRC.Shell.s13_klein' does not depend on any axioms
'FRC.Shell.s13_orbit' does not depend on any axioms
'FRC.Rh.ofNat_succ_ne_zero' does not depend on any axioms
'FRC.Rh.frame53' does not depend on any axioms
'FRC.Rh.ofNat_p' does not depend on any axioms
'FRC.Rh.ofNat_add_p' does not depend on any axioms
'FRC.Rh.natCount_eq_zero' does not depend on any axioms
'FRC.Rh.natCount_congr' does not depend on any axioms
'FRC.Rh.sumRange_succ'' does not depend on any axioms
'FRC.Rh.sum_units_eq_sum_pow' does not depend on any axioms
'FRC.Rh.zero_slot' does not depend on any axioms
'FRC.Rh.half_inverse' does not depend on any axioms
'FRC.Rh.shift_power_character' does not depend on any axioms
'FRC.Rh.shift_trace' does not depend on any axioms
'FRC.Rh.slot_complementarity' does not depend on any axioms
'FRC.Rh.quarter_turn_eq_pow' does not depend on any axioms
'FRC.Rh.subject_constants' does not depend on any axioms
'FRC.Rh.constants13' does not depend on any axioms
'FRC.Rh.pow_mod_of_pow_eq_one' does not depend on any axioms
'FRC.Rh.ramanujan_sum' does not depend on any axioms
'FRC.Rh.ramanujan53' does not depend on any axioms
'FRC.Rh.le_mul_self' does not depend on any axioms
'FRC.Rh.window_readback' does not depend on any axioms
'FRC.Rh.factorisation_iff' does not depend on any axioms
'FRC.Rh.frame_coincidence' does not depend on any axioms
'FRC.Rh.lab_pair' does not depend on any axioms
'FRC.Rh.Ext' does not depend on any axioms
'FRC.Rh.Ext.ext' does not depend on any axioms
'FRC.Rh.Ext.re_congr' does not depend on any axioms
'FRC.Rh.Ext.im_congr' does not depend on any axioms
'FRC.Rh.Ext.conj' does not depend on any axioms
'FRC.Rh.Ext.trace' does not depend on any axioms
'FRC.Rh.Ext.norm' does not depend on any axioms
'FRC.Rh.Ext.pow' does not depend on any axioms
'FRC.Rh.Ext.mul_conj' does not depend on any axioms
'FRC.Rh.Ext.conj_inv_of_norm_one' does not depend on any axioms
'FRC.Rh.Ext.fixed_conj' does not depend on any axioms
'FRC.Rh.Ext.rho' does not depend on any axioms
'FRC.Rh.Ext.sigma' does not depend on any axioms
'FRC.Rh.Ext.klein_four' does not depend on any axioms
'FRC.Rh.Ext.critical_line' does not depend on any axioms
'FRC.Rh.Ext.fixed_half_turn' does not depend on any axioms
'FRC.Rh.Ext.norm_on_line' does not depend on any axioms
'FRC.Rh.Ext.quarter_turn_off_circle' does not depend on any axioms
'FRC.Rh.Ext.circle13' does not depend on any axioms
'FRC.Rh.Ext.mul' does not depend on any axioms
'FRC.Rh.Ext.one' does not depend on any axioms
'FRC.Rh.Ext.readout' does not depend on any axioms
'FRC.Rh.Ext.readout_on_line' does not depend on any axioms
'FRC.Rh.Ext.readout_slot_index' does not depend on any axioms
'FRC.Rh.decForallLT' does not depend on any axioms
'FRC.Rh.instDecForallLT' does not depend on any axioms
'FRC.Rh.closure' does not depend on any axioms
'FRC.Rh.closure_lab' does not depend on any axioms
'FRC.Rh.p00004' does not depend on any axioms
'FRC.Rh.p00003' does not depend on any axioms
'FRC.Rh.p00197' does not depend on any axioms
'FRC.Rh.p20008' does not depend on any axioms
'FRC.Rh.p20009' does not depend on any axioms
'FRC.Rh.p20011' does not depend on any axioms
'FRC.Rh.p20012' does not depend on any axioms
'FRC.Rh.p20013' does not depend on any axioms
'FRC.Rh.p20014' does not depend on any axioms
'FRC.Rh.p20015' does not depend on any axioms
'FRC.Rh.p20016' does not depend on any axioms
'FRC.Rh.p20017' does not depend on any axioms
'FRC.Rh.p20029' does not depend on any axioms
'FRC.Rh.p20083' does not depend on any axioms
'FRC.Rh.p20032' does not depend on any axioms
'FRC.Rh.p20043' does not depend on any axioms
'FRC.Rh.p20047' does not depend on any axioms
'FRC.Rh.p20081' does not depend on any axioms
'FRC.Rh.p20079' does not depend on any axioms
'FRC.Entropy.quarter_identity' does not depend on any axioms
'FRC.Entropy.triality_residues' does not depend on any axioms
'FRC.Entropy.octant_divides' does not depend on any axioms
'FRC.Entropy.octant_count' does not depend on any axioms
'FRC.Entropy.closure_count' does not depend on any axioms
'FRC.Entropy.nesting_bound' does not depend on any axioms
'FRC.Entropy.isPrime_of_bounded' does not depend on any axioms
'FRC.Entropy.octant17' does not depend on any axioms
'FRC.Entropy.octant233' does not depend on any axioms
'FRC.Entropy.lab_carrier' does not depend on any axioms
'FRC.Entropy.carrierLab_prime' does not depend on any axioms
'FRC.Entropy.capacity_axis' does not depend on any axioms
'FRC.Entropy.lab_nesting' does not depend on any axioms
'FRC.Entropy.mul_mul_mul_comm' does not depend on any axioms
'FRC.Entropy.lit_mul' does not depend on any axioms
'FRC.Entropy.add_one_add_one_neg' does not depend on any axioms
'FRC.Entropy.even_capacity_powers' does not depend on any axioms
'FRC.Entropy.octant_residue' does not depend on any axioms
'FRC.Entropy.tsirelson_square' does not depend on any axioms
'FRC.Entropy.two_is_square' does not depend on any axioms
'FRC.Entropy.lit_add' does not depend on any axioms
'FRC.Entropy.neg_one_ne_one' does not depend on any axioms
'FRC.Entropy.neg_one_ne_zero' does not depend on any axioms
'FRC.Entropy.octant_of_two_square' does not depend on any axioms
'FRC.Entropy.even_of_order_eight' does not depend on any axioms
'FRC.Entropy.even_capacity_of_octant' does not depend on any axioms
'FRC.Entropy.octant_iff' does not depend on any axioms
'FRC.Entropy.even_capacity_of_two_square' does not depend on any axioms
'FRC.Entropy.two_is_square_iff' does not depend on any axioms
'FRC.Entropy.sumN' does not depend on any axioms
'FRC.Entropy.sumN_congr' does not depend on any axioms
'FRC.Entropy.sumN_mul' does not depend on any axioms
'FRC.Entropy.additive_window_bound' does not depend on any axioms
'FRC.Entropy.additive_window_attained' does not depend on any axioms
'FRC.Entropy.additive_window_every' does not depend on any axioms
'FRC.Entropy.additive_window' does not depend on any axioms
'FRC.Entropy.additive_window_hydrogen' does not depend on any axioms
'FRC.Entropy.lock_recurrence' does not depend on any axioms
'FRC.Entropy.lock_orbits' does not depend on any axioms
'FRC.Entropy.shells_of_capacity' does not depend on any axioms
'FRC.Entropy.fusion_capacity' does not depend on any axioms
'FRC.Entropy.concordance' does not depend on any axioms
'FRC.Entropy.p14001' does not depend on any axioms
'FRC.Entropy.p14002' does not depend on any axioms
'FRC.Entropy.p14010' does not depend on any axioms
'FRC.Entropy.p14017' does not depend on any axioms
'FRC.Entropy.p14044' does not depend on any axioms
'FRC.Entropy.p14046' does not depend on any axioms
'FRC.Entropy.p14047' does not depend on any axioms
'FRC.Entropy.p14048' does not depend on any axioms
'FRC.Entropy.p14019' does not depend on any axioms
'FRC.Entropy.p14021' does not depend on any axioms
'FRC.Entropy.p14022' does not depend on any axioms
'FRC.Entropy.p14023' does not depend on any axioms
'FRC.Entropy.p14027' does not depend on any axioms
'FRC.Entropy.p14031' does not depend on any axioms
'FRC.Gravity.calibration' does not depend on any axioms
'FRC.Gravity.newton_residue' does not depend on any axioms
'FRC.Gravity.hbar_root' does not depend on any axioms
'FRC.Gravity.two_face_count' does not depend on any axioms
'FRC.Gravity.register13_17' does not depend on any axioms
'FRC.Gravity.merger_instance' does not depend on any axioms
'FRC.Gravity.lab_register' does not depend on any axioms
'FRC.Gravity.count_identity' does not depend on any axioms
'FRC.Gravity.p21001' does not depend on any axioms
'FRC.Gravity.p21009' does not depend on any axioms
'FRC.Gravity.p21016' does not depend on any axioms
'FRC.Gravity.p21017' does not depend on any axioms
'FRC.Gravity.p21018' does not depend on any axioms
'FRC.Gravity.p21020' does not depend on any axioms
'FRC.Gravity.p21021' does not depend on any axioms
'FRC.Gravity.p21022' does not depend on any axioms
'FRC.Gravity.p21023' does not depend on any axioms
'FRC.Gravity.p21024' does not depend on any axioms
'FRC.Gravity.p21026' does not depend on any axioms
'FRC.Gravity.p21062' does not depend on any axioms
'FRC.Gravity.p21030' does not depend on any axioms
'FRC.Gravity.p21031' does not depend on any axioms
'FRC.Gravity.p21064' does not depend on any axioms
'FRC.Gravity.p21035' does not depend on any axioms
'FRC.Gravity.p21036' does not depend on any axioms
'FRC.Gravity.p21040' does not depend on any axioms
'FRC.Gravity.p21041' does not depend on any axioms
'FRC.Gravity.p21043' does not depend on any axioms
'FRC.Gravity.p21055' does not depend on any axioms
'FRC.S13.p38001' does not depend on any axioms
'FRC.S13.p38002' does not depend on any axioms
'FRC.S13.p38003' does not depend on any axioms
'FRC.S13.p38004' does not depend on any axioms
'FRC.S13.p38006' does not depend on any axioms
'FRC.S13.p38007' does not depend on any axioms
'FRC.S13.p38008' does not depend on any axioms
'FRC.S13.p38050' does not depend on any axioms
'FRC.S13.p38009' does not depend on any axioms
'FRC.S13.p38010' does not depend on any axioms
'FRC.S13.p38011' does not depend on any axioms
'FRC.S13.p38012' does not depend on any axioms
'FRC.S13.p38013' does not depend on any axioms
'FRC.S13.p38014' does not depend on any axioms
'FRC.S13.p38015' does not depend on any axioms
'FRC.S13.p38016' does not depend on any axioms
'FRC.S13.p38018' does not depend on any axioms
'FRC.S13.p38019' does not depend on any axioms
'FRC.S13.p38020' does not depend on any axioms
'FRC.S13.p38021' does not depend on any axioms
'FRC.S13.p38022' does not depend on any axioms
'FRC.S13.p38044' does not depend on any axioms
'FRC.S13.p38053' does not depend on any axioms
'FRC.S13.p38054' does not depend on any axioms
'FRC.S13.p38025' does not depend on any axioms
'FRC.S13.p38026' does not depend on any axioms
'FRC.S13.p38027' does not depend on any axioms
'FRC.S13.p38029' does not depend on any axioms
'FRC.S13.p38030' does not depend on any axioms
'FRC.S13.p38031' does not depend on any axioms
'FRC.S13.p38032' does not depend on any axioms
'FRC.S13.p38033' does not depend on any axioms
'FRC.S13.p38036' does not depend on any axioms
'FRC.S13.p38037' does not depend on any axioms
'FRC.S13.p38046' does not depend on any axioms
'FRC.S13.p38048' does not depend on any axioms
'FRC.S13.p38051' does not depend on any axioms
'FRC.Qm.p22002' does not depend on any axioms
'FRC.Qm.p22017' does not depend on any axioms
'FRC.Qm.p22018' does not depend on any axioms
'FRC.Qm.p22019' does not depend on any axioms
'FRC.Qm.p22020' does not depend on any axioms
'FRC.Qm.p22021' does not depend on any axioms
'FRC.Qm.p22022' does not depend on any axioms
'FRC.Qm.p22023' does not depend on any axioms
'FRC.Qm.p22024' does not depend on any axioms
'FRC.Qm.p22025' does not depend on any axioms
'FRC.Qm.p22026' does not depend on any axioms
'FRC.Qm.p22027' does not depend on any axioms
'FRC.Qm.p22028' does not depend on any axioms
'FRC.Qm.p22029' does not depend on any axioms
'FRC.Qm.p22030' does not depend on any axioms
'FRC.Qm.p22031' does not depend on any axioms
'FRC.Qm.p22032' does not depend on any axioms
'FRC.Qm.p22033' does not depend on any axioms
'FRC.Qm.p22034' does not depend on any axioms
'FRC.Qm.p22035' does not depend on any axioms
'FRC.Qm.p22036' does not depend on any axioms
'FRC.Qm.p22037' does not depend on any axioms
'FRC.Qm.p22038' does not depend on any axioms
'FRC.Qm.p22039' does not depend on any axioms
'FRC.Qm.p22040' does not depend on any axioms
'FRC.Qm.p22041' does not depend on any axioms
'FRC.Qm.p22042' does not depend on any axioms
'FRC.Qm.p22043' does not depend on any axioms
'FRC.Qm.p22044' does not depend on any axioms
'FRC.Qm.p22045' does not depend on any axioms
'FRC.Qm.p22046' does not depend on any axioms
'FRC.Qm.p22047' does not depend on any axioms
'FRC.Qm.p22048' does not depend on any axioms
'FRC.Qm.p22049' does not depend on any axioms
'FRC.Qm.p22050' does not depend on any axioms
'FRC.Qm.p22051' does not depend on any axioms
'FRC.Qm.p22052' does not depend on any axioms
'FRC.Qm.p22053' does not depend on any axioms
'FRC.Qm.p22054' does not depend on any axioms
'FRC.Qm.p22055' does not depend on any axioms
'FRC.Qm.p22056' does not depend on any axioms
'FRC.Pnp.p26009' does not depend on any axioms
'FRC.Pnp.p26011' does not depend on any axioms
'FRC.Pnp.p26025' does not depend on any axioms
'FRC.Pnp.p26027' does not depend on any axioms
'FRC.Pnp.p26030' does not depend on any axioms
'FRC.Pnp.p26031' does not depend on any axioms
'FRC.Pnp.p26038' does not depend on any axioms
'FRC.Pnp.p26041' does not depend on any axioms
'FRC.Pnp.p26042' does not depend on any axioms
'FRC.Pnp.p26043' does not depend on any axioms
'FRC.Pnp.p26044' does not depend on any axioms
'FRC.Pnp.p26048' does not depend on any axioms
'FRC.Dirac.quarterTurn_eq_pow' does not depend on any axioms
'FRC.Dirac.quarter_class' does not depend on any axioms
'FRC.Dirac.two_class' does not depend on any axioms
'FRC.Dirac.nu_factorisation' does not depend on any axioms
'FRC.Dirac.ladder' does not depend on any axioms
'FRC.Dirac.four_kappa' does not depend on any axioms
'FRC.Dirac.terminal_latitude' does not depend on any axioms
'FRC.Dirac.drive_eigen' does not depend on any axioms
'FRC.Dirac.exceptional_eigen' does not depend on any axioms
'FRC.Dirac.isotropy' does not depend on any axioms
'FRC.Dirac.sector_separation' does not depend on any axioms
'FRC.Dirac.count2' does not depend on any axioms
'FRC.Dirac.count4' does not depend on any axioms
'FRC.Dirac.normOneCount' does not depend on any axioms
'FRC.Dirac.unitCircleCount' does not depend on any axioms
'FRC.Dirac.euclidZeros' does not depend on any axioms
'FRC.Dirac.lorentzZeros' does not depend on any axioms
'FRC.Dirac.zeros5' does not depend on any axioms
'FRC.Dirac.zeros13' does not depend on any axioms
'FRC.Dirac.torus_counts' does not depend on any axioms
'FRC.Dirac.Mat.nth' does not depend on any axioms
'FRC.Dirac.Mat.dot' does not depend on any axioms
'FRC.Dirac.Mat.col' does not depend on any axioms
'FRC.Dirac.Mat.transpose' does not depend on any axioms
'FRC.Dirac.Mat.mul' does not depend on any axioms
'FRC.Dirac.Mat.add' does not depend on any axioms
'FRC.Dirac.Mat.neg' does not depend on any axioms
'FRC.Dirac.Mat.smul' does not depend on any axioms
'FRC.Dirac.Mat.ident' does not depend on any axioms
'FRC.Dirac.Mat.pow' does not depend on any axioms
'FRC.Dirac.Mat.dagger' does not depend on any axioms
'FRC.Dirac.gamma0' does not depend on any axioms
'FRC.Dirac.gamma1' does not depend on any axioms
'FRC.Dirac.gamma2' does not depend on any axioms
'FRC.Dirac.gamma3' does not depend on any axioms
'FRC.Dirac.gamma' does not depend on any axioms
'FRC.Dirac.eta' does not depend on any axioms
'FRC.Dirac.clifford' does not depend on any axioms
'FRC.Dirac.clifford_values' does not depend on any axioms
'FRC.Dirac.spinLift' does not depend on any axioms
'FRC.Dirac.spinLiftInv' does not depend on any axioms
'FRC.Dirac.spinConj' does not depend on any axioms
'FRC.Dirac.spin_conjugation_values' does not depend on any axioms
'FRC.Dirac.spinorForm' does not depend on any axioms
'FRC.Dirac.spinor_form_values' does not depend on any axioms
'FRC.Dirac.invS' does not depend on any axioms
'FRC.Dirac.cyc' does not depend on any axioms
'FRC.Dirac.cycId' does not depend on any axioms
'FRC.Dirac.cycAdd' does not depend on any axioms
'FRC.Dirac.cycSmul' does not depend on any axioms
'FRC.Dirac.cycPow' does not depend on any axioms
'FRC.Dirac.kineticRow' does not depend on any axioms
'FRC.Dirac.cayleyRow' does not depend on any axioms
'FRC.Dirac.cayley13' does not depend on any axioms
'FRC.Dirac.cayley13_values' does not depend on any axioms
'FRC.Dirac.phi' does not depend on any axioms
'FRC.Dirac.orderIn' does not depend on any axioms
'FRC.Dirac.potentialOrder' does not depend on any axioms
'FRC.Dirac.potentialNormOne' does not depend on any axioms
'FRC.Dirac.potential_orders' does not depend on any axioms
'FRC.Dirac.hasOrderThree' does not depend on any axioms
'FRC.Dirac.triality_values' does not depend on any axioms
'FRC.Dirac.powerImage' does not depend on any axioms
'FRC.Dirac.power_map13' does not depend on any axioms
'FRC.Dirac.anchors' does not depend on any axioms
'FRC.Dirac.shellAdmissible' does not depend on any axioms
'FRC.Dirac.minimal_admissible' does not depend on any axioms
'FRC.Dirac.carrier_constants' does not depend on any axioms
'FRC.Dirac.two_mul_mod' does not depend on any axioms
'FRC.Dirac.mod_two_of_mod_four_mul' does not depend on any axioms
'FRC.Dirac.mod_n_mod_two' does not depend on any axioms
'FRC.Dirac.parity_iff' does not depend on any axioms
'FRC.Dirac.drive_nonsquare' does not depend on any axioms
'FRC.Dirac.mod_two_cases' does not depend on any axioms
'FRC.Dirac.succ_mod_two_eq_zero_iff' does not depend on any axioms
'FRC.Dirac.inv_drive_odd' does not depend on any axioms
'FRC.Dirac.inv_drive_nonsquare' does not depend on any axioms
'FRC.Dirac.Ext' does not depend on any axioms
'FRC.Dirac.Ext.ext'' does not depend on any axioms
'FRC.Dirac.Ext.ofShell' does not depend on any axioms
'FRC.Dirac.Ext.w' does not depend on any axioms
'FRC.Dirac.Ext.conj' does not depend on any axioms
'FRC.Dirac.Ext.norm' does not depend on any axioms
'FRC.Dirac.Ext.pow' does not depend on any axioms
'FRC.Dirac.Ext.mul_re' does not depend on any axioms
'FRC.Dirac.Ext.mul_im' does not depend on any axioms
'FRC.Dirac.Ext.ofShell_re' does not depend on any axioms
'FRC.Dirac.Ext.ofShell_im' does not depend on any axioms
'FRC.Dirac.Ext.conj_re' does not depend on any axioms
'FRC.Dirac.Ext.conj_im' does not depend on any axioms
'FRC.Dirac.Ext.w_sq' does not depend on any axioms
'FRC.Dirac.Ext.mul_conj' does not depend on any axioms
'FRC.Dirac.Ext.conj_mul' does not depend on any axioms
'FRC.Dirac.Ext.norm_scale' does not depend on any axioms
'FRC.Dirac.p08002' does not depend on any axioms
'FRC.Dirac.p08005' does not depend on any axioms
'FRC.Dirac.p08009' does not depend on any axioms
'FRC.Dirac.p08010' does not depend on any axioms
'FRC.Dirac.p08011' does not depend on any axioms
'FRC.Dirac.p08012' does not depend on any axioms
'FRC.Dirac.p08013' does not depend on any axioms
'FRC.Dirac.p08019' does not depend on any axioms
'FRC.Dirac.p08020' does not depend on any axioms
'FRC.Dirac.p08022' does not depend on any axioms
'FRC.Dirac.p08025' does not depend on any axioms
'FRC.Dirac.p08026' does not depend on any axioms
'FRC.Dirac.p08027' does not depend on any axioms
'FRC.Dirac.p08029' does not depend on any axioms
'FRC.Dirac.p08032' does not depend on any axioms
'FRC.Dirac.p08035' does not depend on any axioms
'FRC.Dirac.p08037' does not depend on any axioms
'FRC.Dirac.p08039' does not depend on any axioms
'FRC.Dirac.p08040' does not depend on any axioms
'FRC.Dirac.p08041' does not depend on any axioms
'FRC.Shell.IsPrimitive' does not depend on any axioms
'FRC.Shell.Generates' does not depend on any axioms
'FRC.Shell.instDecForallLT' does not depend on any axioms
'FRC.Shell.instDecForallShell' does not depend on any axioms
'FRC.Shell.Frame.inv_unique' does not depend on any axioms
'FRC.Shell.Frame.n_eq' does not depend on any axioms
'FRC.Shell.Frame.n_pos' does not depend on any axioms
'FRC.Shell.Frame.one_lt_p' does not depend on any axioms
'FRC.Shell.Frame.one_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.pow_n' does not depend on any axioms
'FRC.Shell.Frame.pow_mod' does not depend on any axioms
'FRC.Shell.Frame.pow_eq_one_of_mod' does not depend on any axioms
'FRC.Shell.Frame.mod_eq_zero_of_pow_eq_one' does not depend on any axioms
'FRC.Shell.Frame.pow_inj' does not depend on any axioms
'FRC.Shell.Frame.g_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.pow_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.powList' does not depend on any axioms
'FRC.Shell.Frame.powList_length' does not depend on any axioms
'FRC.Shell.Frame.mem_powList' does not depend on any axioms
'FRC.Shell.Frame.powList_nodup' does not depend on any axioms
'FRC.Shell.Frame.generates' does not depend on any axioms
'FRC.Shell.Frame.eq_pow_of_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.exists_inv' does not depend on any axioms
'FRC.Shell.Frame.mul_eq_zero' does not depend on any axioms
'FRC.Shell.Frame.mul_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.mul_left_cancel' does not depend on any axioms
'FRC.Shell.Frame.sq_eq_one' does not depend on any axioms
'FRC.Shell.Frame.halfPeriod' does not depend on any axioms
'FRC.Shell.Frame.quarterTurn' does not depend on any axioms
'FRC.Shell.Frame.two_kappa_lt' does not depend on any axioms
'FRC.Shell.Frame.two_kappa_pos' does not depend on any axioms
'FRC.Shell.Frame.four_kappa' does not depend on any axioms
'FRC.Shell.Frame.half_period' does not depend on any axioms
'FRC.Shell.Frame.quarter_turn_sq' does not depend on any axioms
'FRC.Shell.Frame.quarter_turn_order' does not depend on any axioms
'FRC.Shell.Frame.orientation_class' does not depend on any axioms
'FRC.Shell.Frame.sq_mod_two' does not depend on any axioms
'FRC.Shell.Frame.euler_identity' does not depend on any axioms
'FRC.Shell.Frame.two_pi' does not depend on any axioms
'FRC.Shell.Frame.two_lt_p' does not depend on any axioms
'FRC.Shell.Frame.two_ne_zero' does not depend on any axioms
'FRC.Shell.Frame.two_eq_one_add_one' does not depend on any axioms
'FRC.Shell.Frame.two_mul'' does not depend on any axioms
'FRC.Shell.Frame.eq_zero_of_eq_neg' does not depend on any axioms
'FRC.Shell.Frame.no_south_pole' does not depend on any axioms
'FRC.Shell.Frame.two_mul_mod' does not depend on any axioms
'FRC.Shell.Frame.mod_two_of_mod_four_mul' does not depend on any axioms
'FRC.Shell.Frame.mod_n_mod_two' does not depend on any axioms
'FRC.Shell.Frame.parity_iff' does not depend on any axioms
'FRC.Shell.Frame.drive_nonsquare' does not depend on any axioms
'FRC.Shell.Frame.mod_two_cases' does not depend on any axioms
'FRC.Shell.Frame.succ_mod_two_eq_zero_iff' does not depend on any axioms
'FRC.Shell.Frame.inv_drive_odd' does not depend on any axioms
'FRC.Shell.Frame.inv_drive_nonsquare' does not depend on any axioms
'FRC.Shell.Frame.RE.eval' does not depend on any axioms
'FRC.Shell.Frame.look' does not depend on any axioms
'FRC.Shell.Frame.mEval' does not depend on any axioms
'FRC.Shell.Frame.pEval' does not depend on any axioms
'FRC.Shell.Frame.pRow' does not depend on any axioms
'FRC.Shell.Frame.pMul' does not depend on any axioms
'FRC.Shell.Frame.RE.toP' does not depend on any axioms
'FRC.Shell.Frame.insM' does not depend on any axioms
'FRC.Shell.Frame.sortM' does not depend on any axioms
'FRC.Shell.Frame.lexLe' does not depend on any axioms
'FRC.Shell.Frame.insP' does not depend on any axioms
'FRC.Shell.Frame.sortP' does not depend on any axioms
'FRC.Shell.Frame.nfP' does not depend on any axioms
'FRC.Shell.Frame.mEval_append' does not depend on any axioms
'FRC.Shell.Frame.pEval_append' does not depend on any axioms
'FRC.Shell.Frame.pEval_row' does not depend on any axioms
'FRC.Shell.Frame.pEval_mul' does not depend on any axioms
'FRC.Shell.Frame.ring_add' does not depend on any axioms
'FRC.Shell.Frame.ring_mul' does not depend on any axioms
'FRC.Shell.Frame.ring_neg' does not depend on any axioms
'FRC.Shell.Frame.RE.toP_eval' does not depend on any axioms
'FRC.Shell.Frame.mEval_insM' does not depend on any axioms
'FRC.Shell.Frame.mEval_sortM' does not depend on any axioms
'FRC.Shell.Frame.pEval_insP' does not depend on any axioms
'FRC.Shell.Frame.pEval_nfP' does not depend on any axioms
'FRC.Shell.Frame.nbeq' does not depend on any axioms
'FRC.Shell.Frame.pbeq' does not depend on any axioms
'FRC.Shell.Frame.and_true_left' does not depend on any axioms
'FRC.Shell.Frame.and_true_right' does not depend on any axioms
'FRC.Shell.Frame.nbeq_eq' does not depend on any axioms
'FRC.Shell.Frame.pbeq_eq' does not depend on any axioms
'FRC.Shell.Frame.RE.sound' does not depend on any axioms
'FRC.Shell.Frame.RE.check' does not depend on any axioms
'FRC.Extension.Ext.ext' does not depend on any axioms
'FRC.Extension.Ext.re_congr' does not depend on any axioms
'FRC.Extension.Ext.im_congr' does not depend on any axioms
'FRC.Extension.Ext.ofShell' does not depend on any axioms
'FRC.Extension.Ext.w' does not depend on any axioms
'FRC.Extension.Ext.conj' does not depend on any axioms
'FRC.Extension.Ext.trace' does not depend on any axioms
'FRC.Extension.Ext.norm' does not depend on any axioms
'FRC.Extension.Ext.pow' does not depend on any axioms
'FRC.Extension.Ext.mul_re' does not depend on any axioms
'FRC.Extension.Ext.mul_im' does not depend on any axioms
'FRC.Extension.Ext.ofShell_re' does not depend on any axioms
'FRC.Extension.Ext.ofShell_im' does not depend on any axioms
'FRC.Extension.Ext.conj_re' does not depend on any axioms
'FRC.Extension.Ext.conj_im' does not depend on any axioms
'FRC.Extension.Ext.w_sq' does not depend on any axioms
'FRC.Extension.Ext.mul_conj' does not depend on any axioms
'FRC.Extension.Ext.conj_mul' does not depend on any axioms
'FRC.Extension.Ext.norm_scale' does not depend on any axioms
'FRC.Extension.Ext.conj_conj' does not depend on any axioms
'FRC.Extension.Ext.conj_inv_of_norm_one' does not depend on any axioms
'FRC.Extension.Ext.ofShell_mul_eq' does not depend on any axioms
'FRC.Extension.Ext.ofShell_mul' does not depend on any axioms
'FRC.Extension.Ext.one_mul' does not depend on any axioms
'FRC.Extension.Ext.mul_comm' does not depend on any axioms
'FRC.Extension.Ext.mul_assoc' does not depend on any axioms
'FRC.Extension.Ext.norm_mul' does not depend on any axioms
'FRC.Extension.Ext.norm_ofShell' does not depend on any axioms
'FRC.Extension.Ext.mul_one' does not depend on any axioms
'FRC.Extension.Ext.pow_add' does not depend on any axioms
'FRC.Extension.Ext.norm_pow' does not depend on any axioms
'FRC.Bridge.frame_isPrime' does not depend on any axioms
'FRC.Bridge.frame_neg_one_ne_one' does not depend on any axioms
'FRC.Bridge.B7_10E4.Clause' does not depend on any axioms
'FRC.Bridge.B7_10E4.from_master' does not depend on any axioms
'FRC.Bridge.B7_10E4.from_paper' does not depend on any axioms
'FRC.Bridge.B14_14C6.Clause' does not depend on any axioms
'FRC.Bridge.B14_14C6.from_master' does not depend on any axioms
'FRC.Bridge.B14_14C6.from_paper' does not depend on any axioms
'FRC.Bridge.frame_exists' does not depend on any axioms
'FRC.Bridge.frame_iff_isPrime' does not depend on any axioms
'FRC.Bridge.PartClause' does not depend on any axioms
'FRC.Bridge.part_of_master' does not depend on any axioms
'FRC.Bridge.A5_5C2.Clause' does not depend on any axioms
'FRC.Bridge.A5_5C2.from_master' does not depend on any axioms
'FRC.Bridge.A5_5C2.from_paper' does not depend on any axioms
'FRC.Bridge.A5_25D1.Clause' does not depend on any axioms
'FRC.Bridge.A5_25D1.from_master' does not depend on any axioms
'FRC.Bridge.A5_25D1.from_paper' does not depend on any axioms
'FRC.Bridge.b14_of_14C6' does not depend on any axioms
'FRC.Bridge.A6_29B4.Clause' does not depend on any axioms
'FRC.Bridge.A6_29B4.succIter_val' does not depend on any axioms
'FRC.Bridge.A6_29B4.from_master' does not depend on any axioms
'FRC.Bridge.A6_29B4.from_paper' does not depend on any axioms
'FRC.Bridge.C2_6B5.Clause' does not depend on any axioms
'FRC.Bridge.C2_6B5.from_master' does not depend on any axioms
'FRC.Bridge.C2_6B5.from_paper' does not depend on any axioms
'FRC.Bridge.C2_6D4.Clause' does not depend on any axioms
'FRC.Bridge.C2_6D4.from_master' does not depend on any axioms
'FRC.Bridge.C2_6D4.from_paper' does not depend on any axioms
'FRC.Bridge.C2_6C3.Clause' does not depend on any axioms
'FRC.Bridge.C2_6C3.from_master' does not depend on any axioms
'FRC.Bridge.C2_6C3.from_paper' does not depend on any axioms
'FRC.Bridge.C7_1B3.Clause' does not depend on any axioms
'FRC.Bridge.C7_1B3.from_master' does not depend on any axioms
'FRC.Bridge.C7_1B3.from_paper' does not depend on any axioms
'FRC.Bridge.Z1_25C1.Clause' does not depend on any axioms
'FRC.Bridge.Z1_25C1.from_master' does not depend on any axioms
'FRC.Bridge.Z1_25C1.from_paper' does not depend on any axioms
'FRC.Bridge.C1_2D1.Clause' does not depend on any axioms
'FRC.Bridge.C1_2D1.from_master' does not depend on any axioms
'FRC.Bridge.C1_2D1.from_paper' does not depend on any axioms
'FRC.Bridge.C3_8B3.Clause' does not depend on any axioms
'FRC.Bridge.C3_8B3.from_master' does not depend on any axioms
'FRC.Bridge.C3_8B3.from_paper' does not depend on any axioms
'FRC.Bridge.C3_8B4.Clause' does not depend on any axioms
'FRC.Bridge.C3_8B4.from_master' does not depend on any axioms
'FRC.Bridge.C3_8B4.from_paper' does not depend on any axioms
'FRC.Bridge.C8_8B5.Clause' does not depend on any axioms
'FRC.Bridge.C8_8B5.from_master' does not depend on any axioms
'FRC.Bridge.C8_8B5.from_paper' does not depend on any axioms
'FRC.Bridge.C8_8B6.Clause' does not depend on any axioms
'FRC.Bridge.C8_8B6.from_master' does not depend on any axioms
'FRC.Bridge.C8_8B6.from_paper' does not depend on any axioms
'FRC.Bridge.C14_Euler.Clause' does not depend on any axioms
'FRC.Bridge.C14_Euler.from_master' does not depend on any axioms
'FRC.Bridge.C14_Euler.from_2D6' does not depend on any axioms
'FRC.Bridge.C14_Euler.from_6B2' does not depend on any axioms
'FRC.Bridge.C14_13B2.Clause' does not depend on any axioms
'FRC.Bridge.C14_13B2.from_master' does not depend on any axioms
'FRC.Bridge.C14_13B2.from_paper' does not depend on any axioms
'FRC.Bridge.C20_8F4.Clause' does not depend on any axioms
'FRC.Bridge.C20_8F4.from_master' does not depend on any axioms
'FRC.Bridge.C20_8F4.from_paper' does not depend on any axioms
'FRC.Bridge.C13_10G2.Clause' does not depend on any axioms
'FRC.Bridge.C13_10G2.from_theme' does not depend on any axioms
'FRC.Bridge.C13_10G2.from_paper' does not depend on any axioms