Search for blocks/addresses/...

Proofgold Asset

asset id
079a56b1a21dbaeb497b6cba19dd7c036efd5134fe0e2510657ad424385eda49
asset hash
47dbb4a1fb34a24025359d1b9e424c32397e327ad6fcd22923c14832c2e829f8
bday / block
4897
tx
ca657..
preasset
doc published by Pr6Pc..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition nInnIn := λ x0 x1 . not (x0x1)
Known In_indIn_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . x2x1x0 x2)x0 x1)∀ x1 . x0 x1
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Theorem 258d1.. : ∀ x0 x1 x2 . x0x1x1x2nIn x2 x0 (proof)
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known Eps_i_axEps_i_ax : ∀ x0 : ι → ο . ∀ x1 . x0 x1x0 (prim0 x0)
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem Eps_i_set_REps_i_set_R : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0x1 x2and (prim0 (λ x3 . and (x3x0) (x1 x3))x0) (x1 (prim0 (λ x3 . and (x3x0) (x1 x3)))) (proof)
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Definition If_iIf_i := λ x0 : ο . λ x1 x2 . prim0 (λ x3 . or (and x0 (x3 = x1)) (and (not x0) (x3 = x2)))
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Known If_i_correctIf_i_correct : ∀ x0 : ο . ∀ x1 x2 . or (and x0 (If_i x0 x1 x2 = x1)) (and (not x0) (If_i x0 x1 x2 = x2))
Known andELandEL : ∀ x0 x1 : ο . and x0 x1x0
Known andERandER : ∀ x0 x1 : ο . and x0 x1x1
Known If_i_0If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0If_i x0 x1 x2 = x2
Known If_i_1If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0If_i x0 x1 x2 = x1
Known If_i_orIf_i_or : ∀ x0 : ο . ∀ x1 x2 . or (If_i x0 x1 x2 = x1) (If_i x0 x1 x2 = x2)
Known If_i_etaIf_i_eta : ∀ x0 : ο . ∀ x1 . If_i x0 x1 x1 = x1
Theorem exandE_iiexandE_ii : ∀ x0 x1 : (ι → ι) → ο . (∀ x2 : ο . (∀ x3 : ι → ι . and (x0 x3) (x1 x3)x2)x2)∀ x2 : ο . (∀ x3 : ι → ι . x0 x3x1 x3x2)x2 (proof)
Theorem exandE_iiiexandE_iii : ∀ x0 x1 : (ι → ι → ι) → ο . (∀ x2 : ο . (∀ x3 : ι → ι → ι . and (x0 x3) (x1 x3)x2)x2)∀ x2 : ο . (∀ x3 : ι → ι → ι . x0 x3x1 x3x2)x2 (proof)
Theorem exandE_iiiiexandE_iiii : ∀ x0 x1 : (ι → ι → ι → ι) → ο . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . and (x0 x3) (x1 x3)x2)x2)∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . x0 x3x1 x3x2)x2 (proof)
Theorem exandE_iioexandE_iio : ∀ x0 x1 : (ι → ι → ο) → ο . (∀ x2 : ο . (∀ x3 : ι → ι → ο . and (x0 x3) (x1 x3)x2)x2)∀ x2 : ο . (∀ x3 : ι → ι → ο . x0 x3x1 x3x2)x2 (proof)
Theorem exandE_iiioexandE_iiio : ∀ x0 x1 : (ι → ι → ι → ο) → ο . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ο . and (x0 x3) (x1 x3)x2)x2)∀ x2 : ο . (∀ x3 : ι → ι → ι → ο . x0 x3x1 x3x2)x2 (proof)
Definition Descr_iiDescr_ii := λ x0 : (ι → ι) → ο . λ x1 . prim0 (λ x2 . ∀ x3 : ι → ι . x0 x3x3 x1 = x2)
Theorem Descr_ii_propDescr_ii_prop : ∀ x0 : (ι → ι) → ο . (∀ x1 : ο . (∀ x2 : ι → ι . x0 x2x1)x1)(∀ x1 x2 : ι → ι . x0 x1x0 x2x1 = x2)x0 (Descr_ii x0) (proof)
Definition Descr_iiiDescr_iii := λ x0 : (ι → ι → ι) → ο . λ x1 x2 . prim0 (λ x3 . ∀ x4 : ι → ι → ι . x0 x4x4 x1 x2 = x3)
Theorem Descr_iii_propDescr_iii_prop : ∀ x0 : (ι → ι → ι) → ο . (∀ x1 : ο . (∀ x2 : ι → ι → ι . x0 x2x1)x1)(∀ x1 x2 : ι → ι → ι . x0 x1x0 x2x1 = x2)x0 (Descr_iii x0) (proof)
Definition Descr_iioDescr_iio := λ x0 : (ι → ι → ο) → ο . λ x1 x2 . ∀ x3 : ι → ι → ο . x0 x3x3 x1 x2
Known prop_ext_2prop_ext_2 : ∀ x0 x1 : ο . (x0x1)(x1x0)x0 = x1
Theorem Descr_iio_propDescr_iio_prop : ∀ x0 : (ι → ι → ο) → ο . (∀ x1 : ο . (∀ x2 : ι → ι → ο . x0 x2x1)x1)(∀ x1 x2 : ι → ι → ο . x0 x1x0 x2x1 = x2)x0 (Descr_iio x0) (proof)
Definition Descr_Vo1Descr_Vo1 := λ x0 : (ι → ο) → ο . λ x1 . ∀ x2 : ι → ο . x0 x2x2 x1
Theorem Descr_Vo1_propDescr_Vo1_prop : ∀ x0 : (ι → ο) → ο . (∀ x1 : ο . (∀ x2 : ι → ο . x0 x2x1)x1)(∀ x1 x2 : ι → ο . x0 x1x0 x2x1 = x2)x0 (Descr_Vo1 x0) (proof)
Definition Descr_Vo2Descr_Vo2 := λ x0 : ((ι → ο) → ο) → ο . λ x1 : ι → ο . ∀ x2 : (ι → ο) → ο . x0 x2x2 x1
Theorem Descr_Vo2_propDescr_Vo2_prop : ∀ x0 : ((ι → ο) → ο) → ο . (∀ x1 : ο . (∀ x2 : (ι → ο) → ο . x0 x2x1)x1)(∀ x1 x2 : (ι → ο) → ο . x0 x1x0 x2x1 = x2)x0 (Descr_Vo2 x0) (proof)
Definition If_iiIf_ii := λ x0 : ο . λ x1 x2 : ι → ι . λ x3 . If_i x0 (x1 x3) (x2 x3)
Theorem If_ii_1If_ii_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι . x0If_ii x0 x1 x2 = x1 (proof)
Theorem If_ii_0If_ii_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι . not x0If_ii x0 x1 x2 = x2 (proof)
Definition If_iiiIf_iii := λ x0 : ο . λ x1 x2 : ι → ι → ι . λ x3 x4 . If_i x0 (x1 x3 x4) (x2 x3 x4)
Theorem If_iii_1If_iii_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ι . x0If_iii x0 x1 x2 = x1 (proof)
Theorem If_iii_0If_iii_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ι . not x0If_iii x0 x1 x2 = x2 (proof)
Definition If_Vo1If_Vo1 := λ x0 : ο . λ x1 x2 : ι → ο . λ x3 . and (x0x1 x3) (not x0x2 x3)
Known FalseEFalseE : False∀ x0 : ο . x0
Known notEnotE : ∀ x0 : ο . not x0x0False
Theorem If_Vo1_1If_Vo1_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ο . x0If_Vo1 x0 x1 x2 = x1 (proof)
Theorem If_Vo1_0If_Vo1_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ο . not x0If_Vo1 x0 x1 x2 = x2 (proof)
Definition If_iioIf_iio := λ x0 : ο . λ x1 x2 : ι → ι → ο . λ x3 x4 . and (x0x1 x3 x4) (not x0x2 x3 x4)
Theorem If_iio_1If_iio_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ο . x0If_iio x0 x1 x2 = x1 (proof)
Theorem If_iio_0If_iio_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ο . not x0If_iio x0 x1 x2 = x2 (proof)
Definition If_Vo2If_Vo2 := λ x0 : ο . λ x1 x2 : (ι → ο) → ο . λ x3 : ι → ο . and (x0x1 x3) (not x0x2 x3)
Theorem If_Vo2_1If_Vo2_1 : ∀ x0 : ο . ∀ x1 x2 : (ι → ο) → ο . x0If_Vo2 x0 x1 x2 = x1 (proof)
Theorem If_Vo2_0If_Vo2_0 : ∀ x0 : ο . ∀ x1 x2 : (ι → ο) → ο . not x0If_Vo2 x0 x1 x2 = x2 (proof)
Definition In_rec_i_GIn_rec_i_G := λ x0 : ι → (ι → ι) → ι . λ x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 . ∀ x5 : ι → ι . (∀ x6 . x6x4x3 x6 (x5 x6))x3 x4 (x0 x4 x5))x3 x1 x2
Definition In_rec_iIn_rec_i := λ x0 : ι → (ι → ι) → ι . λ x1 . prim0 (In_rec_i_G x0 x1)
Theorem In_rec_i_G_cIn_rec_i_G_c : ∀ x0 : ι → (ι → ι) → ι . ∀ x1 . ∀ x2 : ι → ι . (∀ x3 . x3x1In_rec_i_G x0 x3 (x2 x3))In_rec_i_G x0 x1 (x0 x1 x2) (proof)
Theorem In_rec_i_G_invIn_rec_i_G_inv : ∀ x0 : ι → (ι → ι) → ι . ∀ x1 x2 . In_rec_i_G x0 x1 x2∀ x3 : ο . (∀ x4 : ι → ι . and (∀ x5 . x5x1In_rec_i_G x0 x5 (x4 x5)) (x2 = x0 x1 x4)x3)x3 (proof)
Theorem In_rec_i_G_fIn_rec_i_G_f : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 x2 x3 . In_rec_i_G x0 x1 x2In_rec_i_G x0 x1 x3x2 = x3 (proof)
Theorem In_rec_i_G_In_rec_iIn_rec_i_G_In_rec_i : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . In_rec_i_G x0 x1 (In_rec_i x0 x1) (proof)
Theorem In_rec_i_G_In_rec_i_dIn_rec_i_G_In_rec_i_d : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . In_rec_i_G x0 x1 (x0 x1 (In_rec_i x0)) (proof)
Theorem In_rec_i_eqIn_rec_i_eq : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . In_rec_i x0 x1 = x0 x1 (In_rec_i x0) (proof)
Definition In_rec_G_iiIn_rec_G_ii := λ x0 : ι → (ι → ι → ι)ι → ι . λ x1 . λ x2 : ι → ι . ∀ x3 : ι → (ι → ι) → ο . (∀ x4 . ∀ x5 : ι → ι → ι . (∀ x6 . x6x4x3 x6 (x5 x6))x3 x4 (x0 x4 x5))x3 x1 x2
Definition In_rec_iiIn_rec_ii := λ x0 : ι → (ι → ι → ι)ι → ι . λ x1 . Descr_ii (In_rec_G_ii x0 x1)
Theorem In_rec_G_ii_cIn_rec_G_ii_c : ∀ x0 : ι → (ι → ι → ι)ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 . x3x1In_rec_G_ii x0 x3 (x2 x3))In_rec_G_ii x0 x1 (x0 x1 x2) (proof)
Theorem In_rec_G_ii_invIn_rec_G_ii_inv : ∀ x0 : ι → (ι → ι → ι)ι → ι . ∀ x1 . ∀ x2 : ι → ι . In_rec_G_ii x0 x1 x2∀ x3 : ο . (∀ x4 : ι → ι → ι . and (∀ x5 . x5x1In_rec_G_ii x0 x5 (x4 x5)) (x2 = x0 x1 x4)x3)x3 (proof)
Theorem In_rec_G_ii_fIn_rec_G_ii_f : ∀ x0 : ι → (ι → ι → ι)ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . ∀ x2 x3 : ι → ι . In_rec_G_ii x0 x1 x2In_rec_G_ii x0 x1 x3x2 = x3 (proof)
Theorem In_rec_G_ii_In_rec_iiIn_rec_G_ii_In_rec_ii : ∀ x0 : ι → (ι → ι → ι)ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . In_rec_G_ii x0 x1 (In_rec_ii x0 x1) (proof)
Theorem In_rec_G_ii_In_rec_ii_dIn_rec_G_ii_In_rec_ii_d : ∀ x0 : ι → (ι → ι → ι)ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . In_rec_G_ii x0 x1 (x0 x1 (In_rec_ii x0)) (proof)
Theorem In_rec_ii_eqIn_rec_ii_eq : ∀ x0 : ι → (ι → ι → ι)ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . In_rec_ii x0 x1 = x0 x1 (In_rec_ii x0) (proof)
Definition In_rec_G_iiiIn_rec_G_iii := λ x0 : ι → (ι → ι → ι → ι)ι → ι → ι . λ x1 . λ x2 : ι → ι → ι . ∀ x3 : ι → (ι → ι → ι) → ο . (∀ x4 . ∀ x5 : ι → ι → ι → ι . (∀ x6 . x6x4x3 x6 (x5 x6))x3 x4 (x0 x4 x5))x3 x1 x2
Definition In_rec_iiiIn_rec_iii := λ x0 : ι → (ι → ι → ι → ι)ι → ι → ι . λ x1 . Descr_iii (In_rec_G_iii x0 x1)
Theorem In_rec_G_iii_cIn_rec_G_iii_c : ∀ x0 : ι → (ι → ι → ι → ι)ι → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι → ι . (∀ x3 . x3x1In_rec_G_iii x0 x3 (x2 x3))In_rec_G_iii x0 x1 (x0 x1 x2) (proof)
Theorem In_rec_G_iii_invIn_rec_G_iii_inv : ∀ x0 : ι → (ι → ι → ι → ι)ι → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι . In_rec_G_iii x0 x1 x2∀ x3 : ο . (∀ x4 : ι → ι → ι → ι . and (∀ x5 . x5x1In_rec_G_iii x0 x5 (x4 x5)) (x2 = x0 x1 x4)x3)x3 (proof)
Theorem In_rec_G_iii_fIn_rec_G_iii_f : ∀ x0 : ι → (ι → ι → ι → ι)ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . ∀ x2 x3 : ι → ι → ι . In_rec_G_iii x0 x1 x2In_rec_G_iii x0 x1 x3x2 = x3 (proof)
Theorem In_rec_G_iii_In_rec_iiiIn_rec_G_iii_In_rec_iii : ∀ x0 : ι → (ι → ι → ι → ι)ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . In_rec_G_iii x0 x1 (In_rec_iii x0 x1) (proof)
Theorem In_rec_G_iii_In_rec_iii_dIn_rec_G_iii_In_rec_iii_d : ∀ x0 : ι → (ι → ι → ι → ι)ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . In_rec_G_iii x0 x1 (x0 x1 (In_rec_iii x0)) (proof)
Theorem In_rec_iii_eqIn_rec_iii_eq : ∀ x0 : ι → (ι → ι → ι → ι)ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . In_rec_iii x0 x1 = x0 x1 (In_rec_iii x0) (proof)
Definition 6b023.. := λ x0 : ι → (ι → ι → ι → ο)ι → ι → ο . λ x1 . λ x2 : ι → ι → ο . ∀ x3 : ι → (ι → ι → ο) → ο . (∀ x4 . ∀ x5 : ι → ι → ι → ο . (∀ x6 . x6x4x3 x6 (x5 x6))x3 x4 (x0 x4 x5))x3 x1 x2
Definition In_rec_iioIn_rec_iio := λ x0 : ι → (ι → ι → ι → ο)ι → ι → ο . λ x1 . Descr_iio (6b023.. x0 x1)
Theorem 6f12d.. : ∀ x0 : ι → (ι → ι → ι → ο)ι → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ι → ο . (∀ x3 . x3x16b023.. x0 x3 (x2 x3))6b023.. x0 x1 (x0 x1 x2) (proof)
Theorem b0c8e.. : ∀ x0 : ι → (ι → ι → ι → ο)ι → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ο . 6b023.. x0 x1 x2∀ x3 : ο . (∀ x4 : ι → ι → ι → ο . and (∀ x5 . x5x16b023.. x0 x5 (x4 x5)) (x2 = x0 x1 x4)x3)x3 (proof)
Theorem 41db9.. : ∀ x0 : ι → (ι → ι → ι → ο)ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . ∀ x2 x3 : ι → ι → ο . 6b023.. x0 x1 x26b023.. x0 x1 x3x2 = x3 (proof)
Theorem 409d6.. : ∀ x0 : ι → (ι → ι → ι → ο)ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . 6b023.. x0 x1 (In_rec_iio x0 x1) (proof)
Theorem 67223.. : ∀ x0 : ι → (ι → ι → ι → ο)ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . 6b023.. x0 x1 (x0 x1 (In_rec_iio x0)) (proof)
Theorem In_rec_iio_eqIn_rec_iio_eq : ∀ x0 : ι → (ι → ι → ι → ο)ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . In_rec_iio x0 x1 = x0 x1 (In_rec_iio x0) (proof)
Definition f6068.. := λ x0 : ι → (ι → ι → ο)ι → ο . λ x1 . λ x2 : ι → ο . ∀ x3 : ι → (ι → ο) → ο . (∀ x4 . ∀ x5 : ι → ι → ο . (∀ x6 . x6x4x3 x6 (x5 x6))x3 x4 (x0 x4 x5))x3 x1 x2
Definition In_rec_Vo1In_rec_Vo1 := λ x0 : ι → (ι → ι → ο)ι → ο . λ x1 . Descr_Vo1 (f6068.. x0 x1)
Theorem 0d2cd.. : ∀ x0 : ι → (ι → ι → ο)ι → ο . ∀ x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1f6068.. x0 x3 (x2 x3))f6068.. x0 x1 (x0 x1 x2) (proof)
Theorem 4d242.. : ∀ x0 : ι → (ι → ι → ο)ι → ο . ∀ x1 . ∀ x2 : ι → ο . f6068.. x0 x1 x2∀ x3 : ο . (∀ x4 : ι → ι → ο . and (∀ x5 . x5x1f6068.. x0 x5 (x4 x5)) (x2 = x0 x1 x4)x3)x3 (proof)
Theorem ebaf1.. : ∀ x0 : ι → (ι → ι → ο)ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . ∀ x2 x3 : ι → ο . f6068.. x0 x1 x2f6068.. x0 x1 x3x2 = x3 (proof)
Theorem 2f624.. : ∀ x0 : ι → (ι → ι → ο)ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . f6068.. x0 x1 (In_rec_Vo1 x0 x1) (proof)
Theorem 722ac.. : ∀ x0 : ι → (ι → ι → ο)ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . f6068.. x0 x1 (x0 x1 (In_rec_Vo1 x0)) (proof)
Theorem In_rec_Vo1_eqIn_rec_Vo1_eq : ∀ x0 : ι → (ι → ι → ο)ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . In_rec_Vo1 x0 x1 = x0 x1 (In_rec_Vo1 x0) (proof)
Definition 2b1c2.. := λ x0 : ι → (ι → (ι → ο) → ο)(ι → ο) → ο . λ x1 . λ x2 : (ι → ο) → ο . ∀ x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . ∀ x5 : ι → (ι → ο) → ο . (∀ x6 . x6x4x3 x6 (x5 x6))x3 x4 (x0 x4 x5))x3 x1 x2
Definition In_rec_Vo2In_rec_Vo2 := λ x0 : ι → (ι → (ι → ο) → ο)(ι → ο) → ο . λ x1 . Descr_Vo2 (2b1c2.. x0 x1)
Theorem 07e5d.. : ∀ x0 : ι → (ι → (ι → ο) → ο)(ι → ο) → ο . ∀ x1 . ∀ x2 : ι → (ι → ο) → ο . (∀ x3 . x3x12b1c2.. x0 x3 (x2 x3))2b1c2.. x0 x1 (x0 x1 x2) (proof)
Theorem 994ef.. : ∀ x0 : ι → (ι → (ι → ο) → ο)(ι → ο) → ο . ∀ x1 . ∀ x2 : (ι → ο) → ο . 2b1c2.. x0 x1 x2∀ x3 : ο . (∀ x4 : ι → (ι → ο) → ο . and (∀ x5 . x5x12b1c2.. x0 x5 (x4 x5)) (x2 = x0 x1 x4)x3)x3 (proof)
Theorem d8d0b.. : ∀ x0 : ι → (ι → (ι → ο) → ο)(ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . ∀ x2 x3 : (ι → ο) → ο . 2b1c2.. x0 x1 x22b1c2.. x0 x1 x3x2 = x3 (proof)
Theorem 2cb7a.. : ∀ x0 : ι → (ι → (ι → ο) → ο)(ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . 2b1c2.. x0 x1 (In_rec_Vo2 x0 x1) (proof)
Theorem 00e25.. : ∀ x0 : ι → (ι → (ι → ο) → ο)(ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . 2b1c2.. x0 x1 (x0 x1 (In_rec_Vo2 x0)) (proof)
Theorem In_rec_Vo2_eqIn_rec_Vo2_eq : ∀ x0 : ι → (ι → (ι → ο) → ο)(ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . x4x1x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3)∀ x1 . In_rec_Vo2 x0 x1 = x0 x1 (In_rec_Vo2 x0) (proof)