audit-session038b-axioms.txt
8 declarations audited · 3 standard axioms only · updated 08-25-2026
Raw #print axioms transcript
'NguyenRH1.lagarias_4_10_a' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sf_eq_resW1' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.gFun_one_sub_fun' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.iteratedDeriv_gFun_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.gFun_one_add_punctured' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.gFun_one_add_eventuallyEq' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.iteratedDeriv_one_div_one_add' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.iteratedDeriv_gFun_one' depends on axioms: [propext, Classical.choice, Quot.sound]