Proofgold Address

Param binunion^binunion : ι → ι → ι
Param Sing^Sing : ι → ι
Definition SetAdjoin^SetAdjoin := λ x0 x1 . binunion x0 (Sing x1)
Definition pair_tag^pair_tag := λ x0 x1 x2 . binunion x1 {SetAdjoin x3 x0|x3 ∈ x2}
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known binunionI2^binunionI2 : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ x2 ∈ binunion x0 x1
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Theorem ctagged_notin_F^{ctagged_notin_F} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 . x1 x2 ⟶ nIn (SetAdjoin x3 x0) x2 (proof)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known binunionE^binunionE : ∀ x0 x1 x2 . x2 ∈ binunion x0 x1 ⟶ or (x2 ∈ x0) (x2 ∈ x1)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Known binunionI1^binunionI1 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ binunion x0 x1
Theorem ctagged_eqE_Subq^{ctagged_eqE_Subq} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 . x1 x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . SetAdjoin x4 x0 = SetAdjoin x5 x0 ⟶ x4 ⊆ x5 (proof)
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Theorem ctagged_eqE_eq^{ctagged_eqE_eq} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x3 ⟶ SetAdjoin x4 x0 = SetAdjoin x5 x0 ⟶ x4 = x5 (proof)
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Theorem pair_tag_prop_1_Subq^{pair_tag_prop_1_Subq} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 x4 x5 . x1 x2 ⟶ pair_tag x0 x2 x3 = pair_tag x0 x4 x5 ⟶ x2 ⊆ x4 (proof)
Theorem pair_tag_prop_1^{pair_tag_prop_1} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 x4 x5 . x1 x2 ⟶ x1 x4 ⟶ pair_tag x0 x2 x3 = pair_tag x0 x4 x5 ⟶ x2 = x4 (proof)
Known ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Theorem pair_tag_prop_2_Subq^{pair_tag_prop_2_Subq} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 x4 x5 . x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ pair_tag x0 x2 x3 = pair_tag x0 x4 x5 ⟶ x3 ⊆ x5 (proof)
Theorem pair_tag_prop_2^{pair_tag_prop_2} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 x4 x5 . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ pair_tag x0 x2 x3 = pair_tag x0 x4 x5 ⟶ x3 = x5 (proof)
Known Repl_Empty^Repl_Empty : ∀ x0 : ι → ι . prim5 0 x0 = 0
Known binunion_idr^binunion_idr : ∀ x0 . binunion x0 0 = x0
Theorem pair_tag_0^pair_tag_0 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 . pair_tag x0 x2 0 = x2 (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition CD_carr^CD_carr := λ x0 . λ x1 : ι → ο . λ x2 . ∀ x3 : ο . (∀ x4 . and (x1 x4) (∀ x5 : ο . (∀ x6 . and (x1 x6) (x2 = pair_tag x0 x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem CD_carr_I^CD_carr_I : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 . x1 x2 ⟶ x1 x3 ⟶ CD_carr x0 x1 (pair_tag x0 x2 x3) (proof)
Theorem CD_carr_E^CD_carr_E : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 . CD_carr x0 x1 x2 ⟶ ∀ x3 : ι → ο . (∀ x4 x5 . x1 x4 ⟶ x1 x5 ⟶ x2 = pair_tag x0 x4 x5 ⟶ x3 (pair_tag x0 x4 x5)) ⟶ x3 x2 (proof)
Theorem CD_carr_0ext^CD_carr_0ext : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ x1 0 ⟶ ∀ x2 . x1 x2 ⟶ CD_carr x0 x1 x2 (proof)
Definition CD_proj0^CD_proj0 := λ x0 . λ x1 : ι → ο . λ x2 . prim0 (λ x3 . and (x1 x3) (∀ x4 : ο . (∀ x5 . and (x1 x5) (x2 = pair_tag x0 x3 x5) ⟶ x4) ⟶ x4))
Definition CD_proj1^CD_proj1 := λ x0 . λ x1 : ι → ο . λ x2 . prim0 (λ x3 . and (x1 x3) (x2 = pair_tag x0 (CD_proj0 x0 x1 x2) x3))
Known Eps_i_ex^Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem CD_proj0_1^CD_proj0_1 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 . CD_carr x0 x1 x2 ⟶ and (x1 (CD_proj0 x0 x1 x2)) (∀ x3 : ο . (∀ x4 . and (x1 x4) (x2 = pair_tag x0 (CD_proj0 x0 x1 x2) x4) ⟶ x3) ⟶ x3) (proof)
Theorem CD_proj0_2^CD_proj0_2 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 . x1 x2 ⟶ x1 x3 ⟶ CD_proj0 x0 x1 (pair_tag x0 x2 x3) = x2 (proof)
Theorem CD_proj1_1^CD_proj1_1 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 . CD_carr x0 x1 x2 ⟶ and (x1 (CD_proj1 x0 x1 x2)) (x2 = pair_tag x0 (CD_proj0 x0 x1 x2) (CD_proj1 x0 x1 x2)) (proof)
Theorem CD_proj1_2^CD_proj1_2 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 . x1 x2 ⟶ x1 x3 ⟶ CD_proj1 x0 x1 (pair_tag x0 x2 x3) = x3 (proof)
Theorem CD_proj0R^CD_proj0R : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 . CD_carr x0 x1 x2 ⟶ x1 (CD_proj0 x0 x1 x2) (proof)
Theorem CD_proj1R^CD_proj1R : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 . CD_carr x0 x1 x2 ⟶ x1 (CD_proj1 x0 x1 x2) (proof)
Theorem CD_proj0proj1_eta^{CD_proj0proj1_eta} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 . CD_carr x0 x1 x2 ⟶ x2 = pair_tag x0 (CD_proj0 x0 x1 x2) (CD_proj1 x0 x1 x2) (proof)
Theorem CD_proj0proj1_split^{CD_proj0proj1_split} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 . CD_carr x0 x1 x2 ⟶ CD_carr x0 x1 x3 ⟶ CD_proj0 x0 x1 x2 = CD_proj0 x0 x1 x3 ⟶ CD_proj1 x0 x1 x2 = CD_proj1 x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem CD_proj0_F^CD_proj0_F : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ x1 0 ⟶ ∀ x2 . x1 x2 ⟶ CD_proj0 x0 x1 x2 = x2 (proof)
Theorem CD_proj1_F^CD_proj1_F : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ x1 0 ⟶ ∀ x2 . x1 x2 ⟶ CD_proj1 x0 x1 x2 = 0 (proof)
Definition CD_minus^CD_minus := λ x0 . λ x1 : ι → ο . λ x2 : ι → ι . λ x3 . pair_tag x0 (x2 (CD_proj0 x0 x1 x3)) (x2 (CD_proj1 x0 x1 x3))
Definition CD_conj^CD_conj := λ x0 . λ x1 : ι → ο . λ x2 x3 : ι → ι . λ x4 . pair_tag x0 (x3 (CD_proj0 x0 x1 x4)) (x2 (CD_proj1 x0 x1 x4))
Definition CD_add^CD_add := λ x0 . λ x1 : ι → ο . λ x2 : ι → ι → ι . λ x3 x4 . pair_tag x0 (x2 (CD_proj0 x0 x1 x3) (CD_proj0 x0 x1 x4)) (x2 (CD_proj1 x0 x1 x3) (CD_proj1 x0 x1 x4))
Definition CD_mul^CD_mul := λ x0 . λ x1 : ι → ο . λ x2 x3 : ι → ι . λ x4 x5 : ι → ι → ι . λ x6 x7 . pair_tag x0 (x4 (x5 (CD_proj0 x0 x1 x6) (CD_proj0 x0 x1 x7)) (x2 (x5 (x3 (CD_proj1 x0 x1 x7)) (CD_proj1 x0 x1 x6)))) (x4 (x5 (CD_proj1 x0 x1 x7) (CD_proj0 x0 x1 x6)) (x5 (CD_proj1 x0 x1 x6) (x3 (CD_proj0 x0 x1 x7))))
Param nat_primrec^nat_primrec : ι → (ι → ι → ι) → ι → ι
Param ordsucc^ordsucc : ι → ι
Definition CD_exp_nat^CD_exp_nat := λ x0 . λ x1 : ι → ο . λ x2 x3 : ι → ι . λ x4 x5 : ι → ι → ι . λ x6 . nat_primrec 1 (λ x7 . CD_mul x0 x1 x2 x3 x4 x5 x6)
Theorem CD_minus_CD^CD_minus_CD : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x2 x3)) ⟶ ∀ x3 . CD_carr x0 x1 x3 ⟶ CD_carr x0 x1 (CD_minus x0 x1 x2 x3) (proof)
Theorem CD_minus_proj0^{CD_minus_proj0} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x2 x3)) ⟶ ∀ x3 . CD_carr x0 x1 x3 ⟶ CD_proj0 x0 x1 (CD_minus x0 x1 x2 x3) = x2 (CD_proj0 x0 x1 x3) (proof)
Theorem CD_minus_proj1^{CD_minus_proj1} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x2 x3)) ⟶ ∀ x3 . CD_carr x0 x1 x3 ⟶ CD_proj1 x0 x1 (CD_minus x0 x1 x2 x3) = x2 (CD_proj1 x0 x1 x3) (proof)
Theorem CD_conj_CD^CD_conj_CD : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . x1 x4 ⟶ x1 (x3 x4)) ⟶ ∀ x4 . CD_carr x0 x1 x4 ⟶ CD_carr x0 x1 (CD_conj x0 x1 x2 x3 x4) (proof)
Theorem CD_conj_proj0^{CD_conj_proj0} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . x1 x4 ⟶ x1 (x3 x4)) ⟶ ∀ x4 . CD_carr x0 x1 x4 ⟶ CD_proj0 x0 x1 (CD_conj x0 x1 x2 x3 x4) = x3 (CD_proj0 x0 x1 x4) (proof)
Theorem CD_conj_proj1^{CD_conj_proj1} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x2 x3)) ⟶ ∀ x3 : ι → ι . (∀ x4 . x1 x4 ⟶ x1 (x3 x4)) ⟶ ∀ x4 . CD_carr x0 x1 x4 ⟶ CD_proj1 x0 x1 (CD_conj x0 x1 x2 x3 x4) = x2 (CD_proj1 x0 x1 x4) (proof)
Theorem CD_add_CD^CD_add_CD : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 x4 . x1 x3 ⟶ x1 x4 ⟶ x1 (x2 x3 x4)) ⟶ ∀ x3 x4 . CD_carr x0 x1 x3 ⟶ CD_carr x0 x1 x4 ⟶ CD_carr x0 x1 (CD_add x0 x1 x2 x3 x4) (proof)
Theorem CD_add_proj0^CD_add_proj0 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 x4 . x1 x3 ⟶ x1 x4 ⟶ x1 (x2 x3 x4)) ⟶ ∀ x3 x4 . CD_carr x0 x1 x3 ⟶ CD_carr x0 x1 x4 ⟶ CD_proj0 x0 x1 (CD_add x0 x1 x2 x3 x4) = x2 (CD_proj0 x0 x1 x3) (CD_proj0 x0 x1 x4) (proof)
Theorem CD_add_proj1^CD_add_proj1 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 x4 . x1 x3 ⟶ x1 x4 ⟶ x1 (x2 x3 x4)) ⟶ ∀ x3 x4 . CD_carr x0 x1 x3 ⟶ CD_carr x0 x1 x4 ⟶ CD_proj1 x0 x1 (CD_add x0 x1 x2 x3 x4) = x2 (CD_proj1 x0 x1 x3) (CD_proj1 x0 x1 x4) (proof)
Theorem CD_mul_CD^CD_mul_CD : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . (∀ x6 . x1 x6 ⟶ x1 (x2 x6)) ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x4 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ ∀ x6 x7 . CD_carr x0 x1 x6 ⟶ CD_carr x0 x1 x7 ⟶ CD_carr x0 x1 (CD_mul x0 x1 x2 x3 x4 x5 x6 x7) (proof)
Theorem CD_mul_proj0^CD_mul_proj0 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . (∀ x6 . x1 x6 ⟶ x1 (x2 x6)) ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x4 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ ∀ x6 x7 . CD_carr x0 x1 x6 ⟶ CD_carr x0 x1 x7 ⟶ CD_proj0 x0 x1 (CD_mul x0 x1 x2 x3 x4 x5 x6 x7) = x4 (x5 (CD_proj0 x0 x1 x6) (CD_proj0 x0 x1 x7)) (x2 (x5 (x3 (CD_proj1 x0 x1 x7)) (CD_proj1 x0 x1 x6))) (proof)
Theorem CD_mul_proj1^CD_mul_proj1 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . (∀ x6 . x1 x6 ⟶ x1 (x2 x6)) ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x4 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ ∀ x6 x7 . CD_carr x0 x1 x6 ⟶ CD_carr x0 x1 x7 ⟶ CD_proj1 x0 x1 (CD_mul x0 x1 x2 x3 x4 x5 x6 x7) = x4 (x5 (CD_proj1 x0 x1 x7) (CD_proj0 x0 x1 x6)) (x5 (CD_proj1 x0 x1 x6) (x3 (CD_proj0 x0 x1 x7))) (proof)
Theorem CD_minus_F_eq^{CD_minus_F_eq} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . x1 0 ⟶ x2 0 = 0 ⟶ ∀ x3 . x1 x3 ⟶ CD_minus x0 x1 x2 x3 = x2 x3 (proof)
Theorem CD_conj_F_eq^CD_conj_F_eq : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . x1 0 ⟶ x2 0 = 0 ⟶ ∀ x3 : ι → ι . ∀ x4 . x1 x4 ⟶ CD_conj x0 x1 x2 x3 x4 = x3 x4 (proof)
Theorem CD_add_F_eq^CD_add_F_eq : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι → ι . x1 0 ⟶ x2 0 0 = 0 ⟶ ∀ x3 x4 . x1 x3 ⟶ x1 x4 ⟶ CD_add x0 x1 x2 x3 x4 = x2 x3 x4 (proof)
Theorem CD_mul_F_eq^CD_mul_F_eq : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . x1 0 ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ x2 0 = 0 ⟶ (∀ x6 . x1 x6 ⟶ x4 x6 0 = x6) ⟶ (∀ x6 . x1 x6 ⟶ x5 0 x6 = 0) ⟶ (∀ x6 . x1 x6 ⟶ x5 x6 0 = 0) ⟶ ∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ CD_mul x0 x1 x2 x3 x4 x5 x6 x7 = x5 x6 x7 (proof)
Theorem CD_minus_invol^{CD_minus_invol} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x2 x3)) ⟶ (∀ x3 . x1 x3 ⟶ x2 (x2 x3) = x3) ⟶ ∀ x3 . CD_carr x0 x1 x3 ⟶ CD_minus x0 x1 x2 (CD_minus x0 x1 x2 x3) = x3 (proof)
Theorem CD_conj_invol^{CD_conj_invol} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . (∀ x4 . x1 x4 ⟶ x1 (x2 x4)) ⟶ (∀ x4 . x1 x4 ⟶ x1 (x3 x4)) ⟶ (∀ x4 . x1 x4 ⟶ x2 (x2 x4) = x4) ⟶ (∀ x4 . x1 x4 ⟶ x3 (x3 x4) = x4) ⟶ ∀ x4 . CD_carr x0 x1 x4 ⟶ CD_conj x0 x1 x2 x3 (CD_conj x0 x1 x2 x3 x4) = x4 (proof)
Theorem CD_conj_minus^{CD_conj_minus} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . (∀ x4 . x1 x4 ⟶ x1 (x2 x4)) ⟶ (∀ x4 . x1 x4 ⟶ x1 (x3 x4)) ⟶ (∀ x4 . x1 x4 ⟶ x3 (x2 x4) = x2 (x3 x4)) ⟶ ∀ x4 . CD_carr x0 x1 x4 ⟶ CD_conj x0 x1 x2 x3 (CD_minus x0 x1 x2 x4) = CD_minus x0 x1 x2 (CD_conj x0 x1 x2 x3 x4) (proof)
Theorem CD_minus_add^CD_minus_add : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι . (∀ x4 . x1 x4 ⟶ x1 (x2 x4)) ⟶ (∀ x4 x5 . x1 x4 ⟶ x1 x5 ⟶ x1 (x3 x4 x5)) ⟶ (∀ x4 x5 . x1 x4 ⟶ x1 x5 ⟶ x2 (x3 x4 x5) = x3 (x2 x4) (x2 x5)) ⟶ ∀ x4 x5 . CD_carr x0 x1 x4 ⟶ CD_carr x0 x1 x5 ⟶ CD_minus x0 x1 x2 (CD_add x0 x1 x3 x4 x5) = CD_add x0 x1 x3 (CD_minus x0 x1 x2 x4) (CD_minus x0 x1 x2 x5) (proof)
Theorem CD_conj_add^CD_conj_add : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 : ι → ι → ι . (∀ x5 . x1 x5 ⟶ x1 (x2 x5)) ⟶ (∀ x5 . x1 x5 ⟶ x1 (x3 x5)) ⟶ (∀ x5 x6 . x1 x5 ⟶ x1 x6 ⟶ x1 (x4 x5 x6)) ⟶ (∀ x5 x6 . x1 x5 ⟶ x1 x6 ⟶ x2 (x4 x5 x6) = x4 (x2 x5) (x2 x6)) ⟶ (∀ x5 x6 . x1 x5 ⟶ x1 x6 ⟶ x3 (x4 x5 x6) = x4 (x3 x5) (x3 x6)) ⟶ ∀ x5 x6 . CD_carr x0 x1 x5 ⟶ CD_carr x0 x1 x6 ⟶ CD_conj x0 x1 x2 x3 (CD_add x0 x1 x4 x5 x6) = CD_add x0 x1 x4 (CD_conj x0 x1 x2 x3 x5) (CD_conj x0 x1 x2 x3 x6) (proof)
Theorem CD_add_com^CD_add_com : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 x4 . x1 x3 ⟶ x1 x4 ⟶ x2 x3 x4 = x2 x4 x3) ⟶ ∀ x3 x4 . CD_carr x0 x1 x3 ⟶ CD_carr x0 x1 x4 ⟶ CD_add x0 x1 x2 x3 x4 = CD_add x0 x1 x2 x4 x3 (proof)
Theorem CD_add_assoc^CD_add_assoc : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 x4 . x1 x3 ⟶ x1 x4 ⟶ x1 (x2 x3 x4)) ⟶ (∀ x3 x4 x5 . x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x2 (x2 x3 x4) x5 = x2 x3 (x2 x4 x5)) ⟶ ∀ x3 x4 x5 . CD_carr x0 x1 x3 ⟶ CD_carr x0 x1 x4 ⟶ CD_carr x0 x1 x5 ⟶ CD_add x0 x1 x2 (CD_add x0 x1 x2 x3 x4) x5 = CD_add x0 x1 x2 x3 (CD_add x0 x1 x2 x4 x5) (proof)
Theorem CD_add_0R^CD_add_0R : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι → ι . x1 0 ⟶ (∀ x3 . x1 x3 ⟶ x2 x3 0 = x3) ⟶ ∀ x3 . CD_carr x0 x1 x3 ⟶ CD_add x0 x1 x2 x3 0 = x3 (proof)
Theorem CD_add_0L^CD_add_0L : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι → ι . x1 0 ⟶ (∀ x3 . x1 x3 ⟶ x2 0 x3 = x3) ⟶ ∀ x3 . CD_carr x0 x1 x3 ⟶ CD_add x0 x1 x2 0 x3 = x3 (proof)
Theorem CD_add_minus_linv^{CD_add_minus_linv} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι . (∀ x4 . x1 x4 ⟶ x1 (x2 x4)) ⟶ (∀ x4 . x1 x4 ⟶ x3 (x2 x4) x4 = 0) ⟶ ∀ x4 . CD_carr x0 x1 x4 ⟶ CD_add x0 x1 x3 (CD_minus x0 x1 x2 x4) x4 = 0 (proof)
Theorem CD_add_minus_rinv^{CD_add_minus_rinv} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι . (∀ x4 . x1 x4 ⟶ x1 (x2 x4)) ⟶ (∀ x4 . x1 x4 ⟶ x3 x4 (x2 x4) = 0) ⟶ ∀ x4 . CD_carr x0 x1 x4 ⟶ CD_add x0 x1 x3 x4 (CD_minus x0 x1 x2 x4) = 0 (proof)
Theorem CD_mul_0R^CD_mul_0R : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . x1 0 ⟶ x2 0 = 0 ⟶ x3 0 = 0 ⟶ x4 0 0 = 0 ⟶ (∀ x6 . x1 x6 ⟶ x5 0 x6 = 0) ⟶ (∀ x6 . x1 x6 ⟶ x5 x6 0 = 0) ⟶ ∀ x6 . CD_carr x0 x1 x6 ⟶ CD_mul x0 x1 x2 x3 x4 x5 x6 0 = 0 (proof)
Theorem CD_mul_0L^CD_mul_0L : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . x1 0 ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ x2 0 = 0 ⟶ x4 0 0 = 0 ⟶ (∀ x6 . x1 x6 ⟶ x5 0 x6 = 0) ⟶ (∀ x6 . x1 x6 ⟶ x5 x6 0 = 0) ⟶ ∀ x6 . CD_carr x0 x1 x6 ⟶ CD_mul x0 x1 x2 x3 x4 x5 0 x6 = 0 (proof)
Theorem CD_mul_1R^CD_mul_1R : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . x1 0 ⟶ x1 1 ⟶ x2 0 = 0 ⟶ x3 0 = 0 ⟶ x3 1 = 1 ⟶ (∀ x6 . x1 x6 ⟶ x4 0 x6 = x6) ⟶ (∀ x6 . x1 x6 ⟶ x4 x6 0 = x6) ⟶ (∀ x6 . x1 x6 ⟶ x5 0 x6 = 0) ⟶ (∀ x6 . x1 x6 ⟶ x5 x6 1 = x6) ⟶ ∀ x6 . CD_carr x0 x1 x6 ⟶ CD_mul x0 x1 x2 x3 x4 x5 x6 1 = x6 (proof)
Theorem CD_mul_1L^CD_mul_1L : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . x1 0 ⟶ x1 1 ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ x2 0 = 0 ⟶ (∀ x6 . x1 x6 ⟶ x4 x6 0 = x6) ⟶ (∀ x6 . x1 x6 ⟶ x5 0 x6 = 0) ⟶ (∀ x6 . x1 x6 ⟶ x5 x6 0 = 0) ⟶ (∀ x6 . x1 x6 ⟶ x5 1 x6 = x6) ⟶ (∀ x6 . x1 x6 ⟶ x5 x6 1 = x6) ⟶ ∀ x6 . CD_carr x0 x1 x6 ⟶ CD_mul x0 x1 x2 x3 x4 x5 1 x6 = x6 (proof)
Theorem CD_conj_mul^CD_conj_mul : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . (∀ x6 . x1 x6 ⟶ x1 (x2 x6)) ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x4 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ (∀ x6 . x1 x6 ⟶ x2 (x2 x6) = x6) ⟶ (∀ x6 . x1 x6 ⟶ x3 (x3 x6) = x6) ⟶ (∀ x6 . x1 x6 ⟶ x3 (x2 x6) = x2 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x3 (x4 x6 x7) = x4 (x3 x6) (x3 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x2 (x4 x6 x7) = x4 (x2 x6) (x2 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x4 x6 x7 = x4 x7 x6) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x3 (x5 x6 x7) = x5 (x3 x7) (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x5 x6 (x2 x7) = x2 (x5 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x5 (x2 x6) x7 = x2 (x5 x6 x7)) ⟶ ∀ x6 x7 . CD_carr x0 x1 x6 ⟶ CD_carr x0 x1 x7 ⟶ CD_conj x0 x1 x2 x3 (CD_mul x0 x1 x2 x3 x4 x5 x6 x7) = CD_mul x0 x1 x2 x3 x4 x5 (CD_conj x0 x1 x2 x3 x7) (CD_conj x0 x1 x2 x3 x6) (proof)
Theorem CD_add_mul_distrR^{CD_add_mul_distrR} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . (∀ x6 . x1 x6 ⟶ x1 (x2 x6)) ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x4 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x2 (x4 x6 x7) = x4 (x2 x6) (x2 x7)) ⟶ (∀ x6 x7 x8 . x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x4 (x4 x6 x7) x8 = x4 x6 (x4 x7 x8)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x4 x6 x7 = x4 x7 x6) ⟶ (∀ x6 x7 x8 . x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x5 x6 (x4 x7 x8) = x4 (x5 x6 x7) (x5 x6 x8)) ⟶ (∀ x6 x7 x8 . x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x5 (x4 x6 x7) x8 = x4 (x5 x6 x8) (x5 x7 x8)) ⟶ ∀ x6 x7 x8 . CD_carr x0 x1 x6 ⟶ CD_carr x0 x1 x7 ⟶ CD_carr x0 x1 x8 ⟶ CD_mul x0 x1 x2 x3 x4 x5 (CD_add x0 x1 x4 x6 x7) x8 = CD_add x0 x1 x4 (CD_mul x0 x1 x2 x3 x4 x5 x6 x8) (CD_mul x0 x1 x2 x3 x4 x5 x7 x8) (proof)
Theorem CD_add_mul_distrL^{CD_add_mul_distrL} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . (∀ x6 . x1 x6 ⟶ x1 (x2 x6)) ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x4 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x2 (x4 x6 x7) = x4 (x2 x6) (x2 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x3 (x4 x6 x7) = x4 (x3 x6) (x3 x7)) ⟶ (∀ x6 x7 x8 . x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x4 (x4 x6 x7) x8 = x4 x6 (x4 x7 x8)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x4 x6 x7 = x4 x7 x6) ⟶ (∀ x6 x7 x8 . x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x5 x6 (x4 x7 x8) = x4 (x5 x6 x7) (x5 x6 x8)) ⟶ (∀ x6 x7 x8 . x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x5 (x4 x6 x7) x8 = x4 (x5 x6 x8) (x5 x7 x8)) ⟶ ∀ x6 x7 x8 . CD_carr x0 x1 x6 ⟶ CD_carr x0 x1 x7 ⟶ CD_carr x0 x1 x8 ⟶ CD_mul x0 x1 x2 x3 x4 x5 x6 (CD_add x0 x1 x4 x7 x8) = CD_add x0 x1 x4 (CD_mul x0 x1 x2 x3 x4 x5 x6 x7) (CD_mul x0 x1 x2 x3 x4 x5 x6 x8) (proof)
Theorem CD_minus_mul_distrR^{CD_minus_mul_distrR} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . (∀ x6 . x1 x6 ⟶ x1 (x2 x6)) ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x4 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ (∀ x6 . x1 x6 ⟶ x3 (x2 x6) = x2 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x2 (x4 x6 x7) = x4 (x2 x6) (x2 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x5 x6 (x2 x7) = x2 (x5 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x5 (x2 x6) x7 = x2 (x5 x6 x7)) ⟶ ∀ x6 x7 . CD_carr x0 x1 x6 ⟶ CD_carr x0 x1 x7 ⟶ CD_mul x0 x1 x2 x3 x4 x5 x6 (CD_minus x0 x1 x2 x7) = CD_minus x0 x1 x2 (CD_mul x0 x1 x2 x3 x4 x5 x6 x7) (proof)
Theorem CD_minus_mul_distrL^{CD_minus_mul_distrL} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . (∀ x6 . x1 x6 ⟶ x1 (x2 x6)) ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x4 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x2 (x4 x6 x7) = x4 (x2 x6) (x2 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x5 x6 (x2 x7) = x2 (x5 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x5 (x2 x6) x7 = x2 (x5 x6 x7)) ⟶ ∀ x6 x7 . CD_carr x0 x1 x6 ⟶ CD_carr x0 x1 x7 ⟶ CD_mul x0 x1 x2 x3 x4 x5 (CD_minus x0 x1 x2 x6) x7 = CD_minus x0 x1 x2 (CD_mul x0 x1 x2 x3 x4 x5 x6 x7) (proof)
Known nat_primrec_0^{nat_primrec_0} : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Theorem CD_exp_nat_0^CD_exp_nat_0 : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . ∀ x6 . CD_exp_nat x0 x1 x2 x3 x4 x5 x6 0 = 1 (proof)
Param nat_p^nat_p : ι → ο
Known nat_primrec_S^{nat_primrec_S} : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2 ⟶ nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2)
Theorem CD_exp_nat_S^CD_exp_nat_S : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . ∀ x6 x7 . nat_p x7 ⟶ CD_exp_nat x0 x1 x2 x3 x4 x5 x6 (ordsucc x7) = CD_mul x0 x1 x2 x3 x4 x5 x6 (CD_exp_nat x0 x1 x2 x3 x4 x5 x6 x7) (proof)
Known nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Theorem CD_exp_nat_CD^{CD_exp_nat_CD} : ∀ x0 . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ ∀ x3 . x3 ∈ x2 ⟶ nIn x0 x3) ⟶ ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ι . (∀ x6 . x1 x6 ⟶ x1 (x2 x6)) ⟶ (∀ x6 . x1 x6 ⟶ x1 (x3 x6)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x4 x6 x7)) ⟶ (∀ x6 x7 . x1 x6 ⟶ x1 x7 ⟶ x1 (x5 x6 x7)) ⟶ x1 0 ⟶ x1 1 ⟶ ∀ x6 . CD_carr x0 x1 x6 ⟶ ∀ x7 . nat_p x7 ⟶ CD_carr x0 x1 (CD_exp_nat x0 x1 x2 x3 x4 x5 x6 x7) (proof)