'NimAudit.Barrier.extraction_enc' depends on axioms: [propext, Quot.sound] 'NimAudit.Barrier.barrier_core' depends on axioms: [propext, Quot.sound] 'NimAudit.Barrier.size_le_tsize' depends on axioms: [propext, Quot.sound] 'NimAudit.Barrier.bbound_of_forms' depends on axioms: [propext, Quot.sound] 'NimAudit.Barrier.bbound_mono' depends on axioms: [propext, Quot.sound] 'NimAudit.Barrier.enc_poly' depends on axioms: [propext, Quot.sound] 'NimAudit.Barrier.barrier_fam' depends on axioms: [propext, Quot.sound] 'NimAudit.Barrier.decisionMove_winsOnEnc' depends on axioms: [propext, Quot.sound] 'NimAudit.Barrier.winsOnEnc_congr' depends on axioms: [propext] 'NimAudit.Barrier.barrier_map' depends on axioms: [propext, Quot.sound] 'NimAudit.Barrier.binMove_netBCirc' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.Barrier.barrier_net' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.Barrier.mhMove_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.Barrier.cinit_fits' depends on axioms: [propext, Quot.sound] 'NimAudit.Barrier.recMove_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.Barrier.width2_encode' depends on axioms: [propext, Quot.sound] 'NimAudit.Barrier.mhMove_winsOnEnc' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.Barrier.recMove_winsOnEnc' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.Barrier.no_ac0_mh' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.Barrier.no_ac0_rec' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.Barrier.no_net_mh' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.Barrier.no_net_rec' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.Barrier.no_ac0_mh_allBoards' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.Barrier.no_ac0_rec_allBoards' depends on axioms: [propext, Classical.choice, Quot.sound] 'NimAudit.Barrier.move_split' does not depend on any axioms 'NimAudit.Barrier.getD_split'' depends on axioms: [propext, Quot.sound] 'NimAudit.Barrier.promised_pred_parity' depends on axioms: [propext, Quot.sound] 'NimAudit.Barrier.lowEnc_eval' depends on axioms: [propext, Quot.sound] 'NimAudit.Barrier.no_ac0_predecessor' depends on axioms: [propext, Quot.sound] 'NimAudit.Barrier.twoFrame_on_encoding' depends on axioms: [propext, Classical.choice, Quot.sound]