Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x0 ⟶ Church6_lt4p (λ x1 x2 x3 x4 x5 x6 . permargs_i_1_0_3_2_4_5 x0 x1 x2 x3 x4 x6 x5)
Let x0 of type ι → ι → ι → ι → ι → ι → ι be given.
Assume H0: Church6_lt4p x0.
Apply H0 with λ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p (λ x2 x3 x4 x5 x6 x7 . permargs_i_1_0_3_2_4_5 x1 x2 x3 x4 x5 x7 x6) leaving 4 subgoals.
The subproof is completed by applying unknownprop_995579645b8886904e46af0dc0ac8e19ee3cd4af7d78809ff698344ead396f5a.
The subproof is completed by applying unknownprop_56ce56513a8af1327555b873c1c6ce07e295bb2d93a34f831bbfdb3328f2809b.
The subproof is completed by applying unknownprop_9ab406e767d5138f84eceb89ae815ef2f93656cc034576ca18ab84af7a608607.
The subproof is completed by applying unknownprop_bd8f81a1227d0cc25cea7c364f7541293f70705efd4999ad0dba8cf8857226a9.
Let x0 of type ι → ι → ι → ι → ι → ι → ι be given.
Assume H1: Church6_p x0.
Apply H1 with λ x1 : ι → ι → ι → ι → ι → ι → ι . ∀ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x2 ⟶ 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 x1 x2) leaving 6 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L0.
The subproof is completed by applying L0.
The subproof is completed by applying L0.
The subproof is completed by applying L0.
The subproof is completed by applying unknownprop_82a18ab52f7ac6281a607a1820c9620c483afb6be383087b7d72855319e580f5.
■