Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ u17.
Let x1 of type ο be given.
Apply unknownprop_14e19ebc7e16f882d3be4482dbe497cecb7597969c9cae0a9f87fe87a0ee217a with x0, λ x2 . (∀ x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x3 ⟶ x2 = x3 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 ⟶ x1) ⟶ x1 leaving 18 subgoals.
The subproof is completed by applying H0.
Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2 ⟶ 0 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 ⟶ x1.
Apply H1 with λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_e6619adff47bbbf90a12e5475c1b155ebb1e2991a2d17411fd40e422e21ff562.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 0 0.
The subproof is completed by applying H2.
Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2 ⟶ u1 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 ⟶ x1.
Apply H1 with λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x3 leaving 2 subgoals.
The subproof is completed by applying unknownprop_93ed18843f4a06fdb1762e5b7fc89edc8da24a5d38de418508f9aca3fe120f8f.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 u1 u1.
The subproof is completed by applying H2.
Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2 ⟶ u2 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 ⟶ x1.
Apply H1 with λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x4 leaving 2 subgoals.
The subproof is completed by applying unknownprop_233906471c2a36e258793125988364b5b4be5e26b5df943569d8a15ce4c97b59.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 u2 u2.
The subproof is completed by applying H2.
Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2 ⟶ u3 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 ⟶ x1.
Apply H1 with λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x5 leaving 2 subgoals.
The subproof is completed by applying unknownprop_497df65ae9348f62989259dc92fffa35cd477d735ac36c17e9f5dc63bcd5da15.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 u3 u3.
The subproof is completed by applying H2.
Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2 ⟶ u4 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 ⟶ x1.
Apply H1 with λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x6 leaving 2 subgoals.
The subproof is completed by applying unknownprop_aeac4ee3d08fd60f864a3d40a6422b2070323f5bdb4e126705e59ff4ccf8fa26.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 u4 u4.
The subproof is completed by applying H2.
Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2 ⟶ u5 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 ⟶ x1.
Apply H1 with λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x7 leaving 2 subgoals.
The subproof is completed by applying unknownprop_398a24facf4ebb42cf838f8cb0f1d64c4d83d480adfd36e0fa2e0b1bde52df48.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 u5 u5.
The subproof is completed by applying H2.
Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2 ⟶ u6 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 u13 u14 u15 u16 ⟶ x1.
Apply H1 with ... leaving 2 subgoals.
...
...
...
...
...
...
...
...
...
...
...
...
■