Proofgold Address

Definition Church6_p := λ x0 : ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (ι → ι → ι → ι → ι → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 . x2) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x3) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x4) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x5) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x6) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x7) ⟶ x1 x0
Definition Church6_lt4p := λ x0 : ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (ι → ι → ι → ι → ι → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 . x2) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x3) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x4) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 . x5) ⟶ x1 x0
Definition permargs_i_1_0_3_2_4_5 := λ x0 : ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 . x0 x2 x1 x4 x3
Definition Church6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5 := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι . λ x2 x3 x4 x5 x6 x7 . x0 (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x6 x7)
Known 3f4a9.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x0 ⟶ Church6_lt4p (permargs_i_1_0_3_2_4_5 x0)
Known bc219.. : Church6_lt4p (λ x0 x1 x2 x3 x4 x5 . x1)
Known 39a8c.. : Church6_lt4p (λ x0 x1 x2 x3 x4 x5 . x0)
Known 22a13.. : Church6_lt4p (λ x0 x1 x2 x3 x4 x5 . x3)
Known a050d.. : Church6_lt4p (λ x0 x1 x2 x3 x4 x5 . x2)
Theorem 3a34f.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0 ⟶ ∀ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x1 ⟶ Church6_lt4p (Church6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5 x0 x1) (proof)
Definition permargs_i_2_3_0_1_4_5 := λ x0 : ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 . x0 x3 x4 x1 x2
Definition Church6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5 := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι . λ x2 x3 x4 x5 x6 x7 . x0 (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x6 x7)
Known bc9c2.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x0 ⟶ Church6_lt4p (permargs_i_2_3_0_1_4_5 x0)
Theorem ca554.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0 ⟶ ∀ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x1 ⟶ Church6_lt4p (Church6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5 x0 x1) (proof)
Definition permargs_i_3_2_1_0_4_5 := λ x0 : ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 . x0 x4 x3 x2 x1
Definition Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι . λ x2 x3 x4 x5 x6 x7 . x0 (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x6 x7) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x7 x6) (permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x6 x7)
Known bcfec.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x0 ⟶ Church6_lt4p (permargs_i_3_2_1_0_4_5 x0)
Theorem 5bea3.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0 ⟶ ∀ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x1 ⟶ Church6_lt4p (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 x0 x1) (proof)