Proofgold Address

Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known and7I^and7I : ∀ x0 x1 x2 x3 x4 x5 x6 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 41253..^and8I : ∀ x0 x1 x2 x3 x4 x5 x6 x7 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7 (proof)
Theorem 7c691..^and9I : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ x8 ⟶ and (and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7) x8 (proof)
Theorem 19e22..^and10I : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ x8 ⟶ x9 ⟶ and (and (and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7) x8) x9 (proof)
Definition Church10_0 := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . x0
Definition Church10_1 := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . x1
Definition Church10_2 := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . x2
Definition Church10_3 := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . x3
Definition Church10_4 := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . x4
Definition Church10_5 := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . x5
Definition Church10_6 := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . x6
Definition Church10_7 := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . x7
Definition Church10_8 := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . x8
Definition Church10_9 := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 . x9
Definition Church10_forall := λ x0 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . and (and (and (and (and (and (and (and (and (x0 Church10_0) (x0 Church10_1)) (x0 Church10_2)) (x0 Church10_3)) (x0 Church10_4)) (x0 Church10_5)) (x0 Church10_6)) (x0 Church10_7)) (x0 Church10_8)) (x0 Church10_9)
Definition Church10_forall2_lt := λ x0 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . and (and (and (and (and (and (and (and (x0 Church10_0 Church10_1) (and (x0 Church10_0 Church10_2) (x0 Church10_1 Church10_2))) (and (and (x0 Church10_0 Church10_3) (x0 Church10_1 Church10_3)) (x0 Church10_2 Church10_3))) (and (and (and (x0 Church10_0 Church10_4) (x0 Church10_1 Church10_4)) (x0 Church10_2 Church10_4)) (x0 Church10_3 Church10_4))) (and (and (and (and (x0 Church10_0 Church10_5) (x0 Church10_1 Church10_5)) (x0 Church10_2 Church10_5)) (x0 Church10_3 Church10_5)) (x0 Church10_4 Church10_5))) (and (and (and (and (and (x0 Church10_0 Church10_6) (x0 Church10_1 Church10_6)) (x0 Church10_2 Church10_6)) (x0 Church10_3 Church10_6)) (x0 Church10_4 Church10_6)) (x0 Church10_5 Church10_6))) (and (and (and (and (and (and (x0 Church10_0 Church10_7) (x0 Church10_1 Church10_7)) (x0 Church10_2 Church10_7)) (x0 Church10_3 Church10_7)) (x0 Church10_4 Church10_7)) (x0 Church10_5 Church10_7)) (x0 Church10_6 Church10_7))) (and (and (and (and (and (and (and (x0 Church10_0 Church10_8) (x0 Church10_1 Church10_8)) (x0 Church10_2 Church10_8)) (x0 Church10_3 Church10_8)) (x0 Church10_4 Church10_8)) (x0 Church10_5 Church10_8)) (x0 Church10_6 Church10_8)) (x0 Church10_7 Church10_8))) (and (and (and (and (and (and (and (and (x0 Church10_0 Church10_9) (x0 Church10_1 Church10_9)) (x0 Church10_2 Church10_9)) (x0 Church10_3 Church10_9)) (x0 Church10_4 Church10_9)) (x0 Church10_5 Church10_9)) (x0 Church10_6 Church10_9)) (x0 Church10_7 Church10_9)) (x0 Church10_8 Church10_9))
Known and4I^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Theorem a46af.. : ∀ x0 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . x0 Church10_0 ⟶ x0 Church10_1 ⟶ x0 Church10_2 ⟶ x0 Church10_3 ⟶ x0 Church10_4 ⟶ x0 Church10_5 ⟶ x0 Church10_6 ⟶ x0 Church10_7 ⟶ x0 Church10_8 ⟶ x0 Church10_9 ⟶ Church10_forall x0 (proof)
Theorem b5d30.. : ∀ x0 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . x0 Church10_0 Church10_0 ⟶ x0 Church10_0 Church10_1 ⟶ x0 Church10_0 Church10_2 ⟶ x0 Church10_0 Church10_3 ⟶ x0 Church10_0 Church10_4 ⟶ x0 Church10_0 Church10_5 ⟶ x0 Church10_0 Church10_6 ⟶ x0 Church10_0 Church10_7 ⟶ x0 Church10_0 Church10_8 ⟶ x0 Church10_0 Church10_9 ⟶ x0 Church10_1 Church10_0 ⟶ x0 Church10_1 Church10_1 ⟶ x0 Church10_1 Church10_2 ⟶ x0 Church10_1 Church10_3 ⟶ x0 Church10_1 Church10_4 ⟶ x0 Church10_1 Church10_5 ⟶ x0 Church10_1 Church10_6 ⟶ x0 Church10_1 Church10_7 ⟶ x0 Church10_1 Church10_8 ⟶ x0 Church10_1 Church10_9 ⟶ x0 Church10_2 Church10_0 ⟶ x0 Church10_2 Church10_1 ⟶ x0 Church10_2 Church10_2 ⟶ x0 Church10_2 Church10_3 ⟶ x0 Church10_2 Church10_4 ⟶ x0 Church10_2 Church10_5 ⟶ x0 Church10_2 Church10_6 ⟶ x0 Church10_2 Church10_7 ⟶ x0 Church10_2 Church10_8 ⟶ x0 Church10_2 Church10_9 ⟶ x0 Church10_3 Church10_0 ⟶ x0 Church10_3 Church10_1 ⟶ x0 Church10_3 Church10_2 ⟶ x0 Church10_3 Church10_3 ⟶ x0 Church10_3 Church10_4 ⟶ x0 Church10_3 Church10_5 ⟶ x0 Church10_3 Church10_6 ⟶ x0 Church10_3 Church10_7 ⟶ x0 Church10_3 Church10_8 ⟶ x0 Church10_3 Church10_9 ⟶ x0 Church10_4 Church10_0 ⟶ x0 Church10_4 Church10_1 ⟶ x0 Church10_4 Church10_2 ⟶ x0 Church10_4 Church10_3 ⟶ x0 Church10_4 Church10_4 ⟶ x0 Church10_4 Church10_5 ⟶ x0 Church10_4 Church10_6 ⟶ x0 Church10_4 Church10_7 ⟶ x0 Church10_4 Church10_8 ⟶ x0 Church10_4 Church10_9 ⟶ x0 Church10_5 Church10_0 ⟶ x0 Church10_5 Church10_1 ⟶ x0 Church10_5 Church10_2 ⟶ x0 Church10_5 Church10_3 ⟶ x0 Church10_5 Church10_4 ⟶ x0 Church10_5 Church10_5 ⟶ x0 Church10_5 Church10_6 ⟶ x0 Church10_5 Church10_7 ⟶ x0 Church10_5 Church10_8 ⟶ x0 Church10_5 Church10_9 ⟶ x0 Church10_6 Church10_0 ⟶ x0 Church10_6 Church10_1 ⟶ x0 Church10_6 Church10_2 ⟶ x0 Church10_6 Church10_3 ⟶ x0 Church10_6 Church10_4 ⟶ x0 Church10_6 Church10_5 ⟶ x0 Church10_6 Church10_6 ⟶ x0 Church10_6 Church10_7 ⟶ x0 Church10_6 Church10_8 ⟶ x0 Church10_6 Church10_9 ⟶ x0 Church10_7 Church10_0 ⟶ x0 Church10_7 Church10_1 ⟶ x0 Church10_7 Church10_2 ⟶ x0 Church10_7 Church10_3 ⟶ x0 Church10_7 Church10_4 ⟶ x0 Church10_7 Church10_5 ⟶ x0 Church10_7 Church10_6 ⟶ x0 Church10_7 Church10_7 ⟶ x0 Church10_7 Church10_8 ⟶ x0 Church10_7 Church10_9 ⟶ x0 Church10_8 Church10_0 ⟶ x0 Church10_8 Church10_1 ⟶ x0 Church10_8 Church10_2 ⟶ x0 Church10_8 Church10_3 ⟶ x0 Church10_8 Church10_4 ⟶ x0 Church10_8 Church10_5 ⟶ x0 Church10_8 Church10_6 ⟶ x0 Church10_8 Church10_7 ⟶ x0 Church10_8 Church10_8 ⟶ x0 Church10_8 Church10_9 ⟶ x0 Church10_9 Church10_0 ⟶ x0 Church10_9 Church10_1 ⟶ x0 Church10_9 Church10_2 ⟶ x0 Church10_9 Church10_3 ⟶ x0 Church10_9 Church10_4 ⟶ x0 Church10_9 Church10_5 ⟶ x0 Church10_9 Church10_6 ⟶ x0 Church10_9 Church10_7 ⟶ x0 Church10_9 Church10_8 ⟶ x0 Church10_9 Church10_9 ⟶ Church10_forall (λ x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church10_forall (x0 x1)) (proof)
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known and5I^and5I : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ and (and (and (and x0 x1) x2) x3) x4
Known and6I^and6I : ∀ x0 x1 x2 x3 x4 x5 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ and (and (and (and (and x0 x1) x2) x3) x4) x5
Theorem df3bd.. : ∀ x0 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . x0 Church10_0 Church10_1 ⟶ x0 Church10_0 Church10_2 ⟶ x0 Church10_1 Church10_2 ⟶ x0 Church10_0 Church10_3 ⟶ x0 Church10_1 Church10_3 ⟶ x0 Church10_2 Church10_3 ⟶ x0 Church10_0 Church10_4 ⟶ x0 Church10_1 Church10_4 ⟶ x0 Church10_2 Church10_4 ⟶ x0 Church10_3 Church10_4 ⟶ x0 Church10_0 Church10_5 ⟶ x0 Church10_1 Church10_5 ⟶ x0 Church10_2 Church10_5 ⟶ x0 Church10_3 Church10_5 ⟶ x0 Church10_4 Church10_5 ⟶ x0 Church10_0 Church10_6 ⟶ x0 Church10_1 Church10_6 ⟶ x0 Church10_2 Church10_6 ⟶ x0 Church10_3 Church10_6 ⟶ x0 Church10_4 Church10_6 ⟶ x0 Church10_5 Church10_6 ⟶ x0 Church10_0 Church10_7 ⟶ x0 Church10_1 Church10_7 ⟶ x0 Church10_2 Church10_7 ⟶ x0 Church10_3 Church10_7 ⟶ x0 Church10_4 Church10_7 ⟶ x0 Church10_5 Church10_7 ⟶ x0 Church10_6 Church10_7 ⟶ x0 Church10_0 Church10_8 ⟶ x0 Church10_1 Church10_8 ⟶ x0 Church10_2 Church10_8 ⟶ x0 Church10_3 Church10_8 ⟶ x0 Church10_4 Church10_8 ⟶ x0 Church10_5 Church10_8 ⟶ x0 Church10_6 Church10_8 ⟶ x0 Church10_7 Church10_8 ⟶ x0 Church10_0 Church10_9 ⟶ x0 Church10_1 Church10_9 ⟶ x0 Church10_2 Church10_9 ⟶ x0 Church10_3 Church10_9 ⟶ x0 Church10_4 Church10_9 ⟶ x0 Church10_5 Church10_9 ⟶ x0 Church10_6 Church10_9 ⟶ x0 Church10_7 Church10_9 ⟶ x0 Church10_8 Church10_9 ⟶ Church10_forall2_lt x0 (proof)
Definition ebe04.. := λ x0 x1 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . and (and (and (Church10_forall (λ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x0 x2 Church10_0 = x2)) (Church10_forall2_lt (λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x0 x2 x3 = x0 x3 x2))) (Church10_forall (λ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church10_forall (λ x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x0 (x1 x2 x3) x3 = x2)))) (Church10_forall (λ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church10_forall (λ x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 (x0 x2 x3) x3 = x2)))
Definition 2b0f2.. := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) (x1 x3 x7 x11 x4 x9 x8 x2 x5 x6 x10) (x1 x4 x11 x3 x7 x8 x10 x5 x6 x2 x9) (x1 x5 x4 x7 x3 x2 x9 x10 x11 x8 x6) (x1 x6 x9 x8 x2 x7 x4 x11 x10 x5 x3) (x1 x7 x8 x10 x9 x4 x6 x3 x2 x11 x5) (x1 x8 x2 x5 x10 x11 x3 x6 x4 x9 x7) (x1 x9 x5 x6 x11 x10 x2 x4 x7 x3 x8) (x1 x10 x6 x2 x8 x5 x11 x9 x3 x7 x4) (x1 x11 x10 x9 x6 x3 x5 x7 x8 x4 x2)
Definition e0abd.. := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 (x1 x2 x8 x10 x6 x5 x9 x3 x7 x4 x11) (x1 x3 x2 x4 x5 x11 x8 x7 x10 x9 x6) (x1 x4 x5 x2 x3 x7 x6 x9 x8 x11 x10) (x1 x5 x9 x8 x2 x10 x11 x4 x3 x6 x7) (x1 x6 x10 x9 x11 x2 x7 x8 x4 x3 x5) (x1 x7 x3 x5 x4 x6 x2 x11 x9 x10 x8) (x1 x8 x7 x6 x10 x4 x3 x2 x11 x5 x9) (x1 x9 x6 x11 x7 x3 x5 x10 x2 x8 x4) (x1 x10 x11 x7 x8 x9 x4 x5 x6 x2 x3) (x1 x11 x4 x3 x9 x8 x10 x6 x5 x7 x2)
Definition 86554.. := λ x0 x1 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x2 x3 x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 (x0 (x0 x4 x2) x3) (x0 x2 x3)