import Axiom
import A.d26agzaz
import A.h3cfdqwq
import A.qg6hprvj
import A.s593tfe3
import A.td0atmnm
import A.warhrjns
import A.wwqc19pp
import A.ydh9veyw

namespace t9e0stky

def logic_is_actual : Prop := warhrjns.logic_is_actual

def bfo : Prop := warhrjns.bfo

def clearer_thought_improves_decision_making : Prop := wwqc19pp.clearer_thought_improves_decision_making

def better_decision_making_enables_effective_choice : Prop := wwqc19pp.better_decision_making_enables_effective_choice

def effective_choice_is_greater_potential : Prop := wwqc19pp.effective_choice_is_greater_potential

def god_is_good : Prop := warhrjns.god_is_good

def i_am_a_person : Prop := wwqc19pp.i_am_a_person

def metabias_is_a_person : Prop := wwqc19pp.metabias_is_a_person

def everyone_makes_mistakes : Prop := wwqc19pp.everyone_makes_mistakes

def all_people_are_immoral : Prop := wwqc19pp.all_people_are_immoral

def i_should_work_toward_correcting__rrcgk48g : Prop := ydh9veyw.i_should_work_toward_correcting_my_mistakes

def not_achieved_implies_achievable_v96ypmv3 : Prop := td0atmnm.not_achieved_implies_achievable_v96ypmv3

def animal_ag_impermissible_jz5h9k0q : Prop := s593tfe3.animal_ag_impermissible_jz5h9k0q

def not_animal_ag_impermissible_x4x58rac : Prop := s593tfe3.not_animal_ag_impermissible_x4x58rac

def animal_ag_impermissible_xfstm71p : Prop := s593tfe3.animal_ag_impermissible_xfstm71p

def animal_ag_impermissible_mqgdx63v : Prop := s593tfe3.animal_ag_impermissible_mqgdx63v

def compatibilism_preserves_responsi_x7xv75xk : Prop := d26agzaz.compatibilism_preserves_responsi_x7xv75xk

def compatibilism_preserves_responsi_bp8exze3 : Prop := d26agzaz.compatibilism_preserves_responsi_bp8exze3

def legitimacy_requires_speech_j9arr979 : Prop := h3cfdqwq.legitimacy_requires_speech_j9arr979

def legitimacy_forbids_speech_bans_m1gy87h7 : Prop := h3cfdqwq.legitimacy_forbids_speech_bans_m1gy87h7

def legitimacy_requires_speech_tvz77dj3 : Prop := h3cfdqwq.legitimacy_requires_speech_tvz77dj3

-- Premise 2 of qg6hprvj.Parenting.calm_hypervigilance_standard_asserted_is_false
def calm_hypervigilance_standard_ass_j6g4txeq : Prop := ∀ (p : Type) (q : Prop), qg6hprvj.Parenting.ObligatedTo p q → qg6hprvj.Parenting.CanBringAbout p q

-- Premise 4 of qg6hprvj.Parenting.calm_hypervigilance_standard_asserted_is_false
def calm_hypervigilance_standard_ass_ht8f3mex : Prop := Axiom.Actual.{0} (Exists.{2} fun p => Exists.{2} fun t => qg6hprvj.Parenting.YoungParent.At p t)

-- Premise 3 of qg6hprvj.Parenting.calm_hypervigilance_standard_asserted_is_false
def calm_hypervigilance_standard_ass_j9x1qfkc : Prop := Axiom.Actual.{0}
  (∀ (p t : Type),
    ¬qg6hprvj.Parenting.CanBringAbout p
        (qg6hprvj.Parenting.CalmAt p t ∧ qg6hprvj.Parenting.HypervigilantAt p t))

-- Premise 5 of qg6hprvj.Parenting.calm_hypervigilance_standard_asserted_is_false
def not_calm_hypervigilance_standard_ass_pawmb7zq : Prop := Not (Axiom.Actual.{0} qg6hprvj.Parenting.CalmHypervigilanceParentingStandard)

def userAxiomsList : Axiom.Axioms :=
  [("logic_is_actual", logic_is_actual), ("bfo", bfo), ("clearer_thought_improves_decision_making", clearer_thought_improves_decision_making), ("better_decision_making_enables_effective_choice", better_decision_making_enables_effective_choice), ("effective_choice_is_greater_potential", effective_choice_is_greater_potential), ("god_is_good", god_is_good), ("i_am_a_person", i_am_a_person), ("metabias_is_a_person", metabias_is_a_person), ("everyone_makes_mistakes", everyone_makes_mistakes), ("all_people_are_immoral", all_people_are_immoral), ("i_should_work_toward_correcting__rrcgk48g", i_should_work_toward_correcting__rrcgk48g), ("not_achieved_implies_achievable_v96ypmv3", not_achieved_implies_achievable_v96ypmv3), ("animal_ag_impermissible_jz5h9k0q", animal_ag_impermissible_jz5h9k0q), ("not_animal_ag_impermissible_x4x58rac", not_animal_ag_impermissible_x4x58rac), ("animal_ag_impermissible_xfstm71p", animal_ag_impermissible_xfstm71p), ("animal_ag_impermissible_mqgdx63v", animal_ag_impermissible_mqgdx63v), ("compatibilism_preserves_responsi_x7xv75xk", compatibilism_preserves_responsi_x7xv75xk), ("compatibilism_preserves_responsi_bp8exze3", compatibilism_preserves_responsi_bp8exze3), ("legitimacy_requires_speech_j9arr979", legitimacy_requires_speech_j9arr979), ("legitimacy_forbids_speech_bans_m1gy87h7", legitimacy_forbids_speech_bans_m1gy87h7), ("legitimacy_requires_speech_tvz77dj3", legitimacy_requires_speech_tvz77dj3), ("calm_hypervigilance_standard_ass_j6g4txeq", calm_hypervigilance_standard_ass_j6g4txeq), ("calm_hypervigilance_standard_ass_ht8f3mex", calm_hypervigilance_standard_ass_ht8f3mex), ("calm_hypervigilance_standard_ass_j9x1qfkc", calm_hypervigilance_standard_ass_j9x1qfkc), ("not_calm_hypervigilance_standard_ass_pawmb7zq", not_calm_hypervigilance_standard_ass_pawmb7zq)]

axiom user_axioms_auth : Axiom.AuthenticatedTerm ("sam", userAxiomsList, 1788041781)

def userAxioms : Axiom.UserAxioms "sam" 1788041781 :=
  ⟨userAxiomsList, user_axioms_auth⟩

end t9e0stky