'NimAudit.AC0.Circ.eval_input' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.eval_const' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.eval_not' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.eval_and' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.eval_or' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.size_input' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.size_const' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.size_not' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.size_and' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.size_or' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.depth_input' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.depth_const' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.depth_not' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.depth_and' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.depth_or' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.maxInput_input' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.maxInput_const' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.maxInput_not' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.maxInput_and' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.maxInput_or' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.subst_input' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.subst_const' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.subst_not' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.subst_and' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.subst_or' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.le_listMax' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.listMax_le' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.all_congr_mem' depends on axioms: [propext]
'NimAudit.AC0.Circ.any_congr_mem' depends on axioms: [propext]
'NimAudit.AC0.Circ.sum_map_le_mem' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.sum_map_mul_right' depends on axioms: [propext]
'NimAudit.AC0.Circ.eval_subst' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.size_subst_le' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.depth_subst_le' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.size_leaf' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.depth_leaf' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.size_subst_leaf' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.depth_subst_leaf' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.maxInput_subst_le' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Circ.eval_congr_below' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.rsum_natCast' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.AC0.gate_rat_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.AC0.nsum_succ' depends on axioms: [propext]
'NimAudit.AC0.nsum_zero' does not depend on any axioms
'NimAudit.AC0.nsum_le' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.nsum_congr' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.nsum_mono' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.nsum_cut' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.length_filter_eq_nsum' depends on axioms: [propext]
'NimAudit.AC0.Gate.psum_succ' depends on axioms: [propext]
'NimAudit.AC0.Gate.psum_mono' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Gate.active_length_le' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Gate.exists_cut' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.Gate.bounded_witness' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.eval_litC' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.mem_boards_of' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.AC0.length_boards' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.eval_termC' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.eval_dnf' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.AC0.size_termC' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.depth_termC' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.maxInput_termC' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.size_dnf' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.depth_dnf' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.maxInput_dnf' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.gate_ac0' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.AC0.eval_compileLayer' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.AC0.eval_compileNet' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.AC0.compileLayer_size' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.compileLayer_depth' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.compileLayer_maxInput' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.sizeBound_succ'' does not depend on any axioms
'NimAudit.AC0.compileNet_sd' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.compileNet_max' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.gfac_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.AC0.pow_step' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.AC0.sizeBound_pos' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.sizeBound_affine' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.AC0.sizeBound_closed' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.AC0.network_ac0' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.AC0.family_ac0' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.AC0.eval_rnnCirc' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.AC0.rnnSize_pos' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.rnn_ac0' depends on axioms: [propext, Classical.choice, Quot.sound]
'NimAudit.AC0.sizeBound_mono_S' depends on axioms: [propext, Quot.sound]
'NimAudit.AC0.rnnSize_closed' depends on axioms: [propext, Classical.choice, Quot.sound]