Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type (CT2 (ι → ι → ι)) → ι → ι → ι be given.
Assume H0: ∀ x1 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 64789.. x1 ⟶ fb516.. (x0 x1).
Claim L1: ...
...
Apply unknownprop_673b5a0ff482ed303e49c4de91639680dfe4eefa3123a40c753c65a98569c7a1 with λ x1 : ι → ι → ι . f9ee2.. (λ x2 : ι → ι → ι . x0 (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2)), λ x1 x2 : ο . x2 = ∀ x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 64789.. x3 ⟶ 6fb7f.. (x0 x3) leaving 2 subgoals.
The subproof is completed by applying L1.
Apply prop_ext_2 with ∀ x1 : ι → ι → ι . fb516.. x1 ⟶ 6fb7f.. (f9ee2.. (λ x2 : ι → ι → ι . x0 (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2))), ∀ x1 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 64789.. x1 ⟶ 6fb7f.. (x0 x1) leaving 2 subgoals.
Assume H2: ∀ x1 : ι → ι → ι . fb516.. x1 ⟶ 6fb7f.. (f9ee2.. (λ x2 : ι → ι → ι . x0 (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2))).
Let x1 of type CT2 (ι → ι → ι) be given.
Assume H3: 64789.. x1.
Apply H3 with 6fb7f.. (x0 x1).
Assume H4: and (x1 = λ x2 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x2 (x1 (λ x3 x4 : ι → ι → ι . x3)) (x1 (λ x3 x4 : ι → ι → ι . x4))) (fb516.. (x1 (λ x2 x3 : ι → ι → ι . x2))).
Apply H4 with fb516.. (x1 (λ x2 x3 : ι → ι → ι . x3)) ⟶ 6fb7f.. (x0 x1).
Assume H5: x1 = λ x2 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x2 (x1 (λ x3 x4 : ι → ι → ι . x3)) (x1 (λ x3 x4 : ι → ι → ι . x4)).
Assume H6: fb516.. (x1 (λ x2 x3 : ι → ι → ι . x2)).
Assume H7: fb516.. (x1 (λ x2 x3 : ι → ι → ι . x3)).
Apply H5 with λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 6fb7f.. (x0 x3).
Claim L8: 6fb7f.. (f9ee2.. (λ x2 : ι → ι → ι . x0 (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 (x1 (λ x4 x5 : ι → ι → ι . x4)) x2)))
Apply H2 with x1 (λ x2 x3 : ι → ι → ι . x2).
The subproof is completed by applying H6.
Claim L9: ∀ x2 : ι → ι → ι . fb516.. x2 ⟶ fb516.. (x0 (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 (x1 (λ x4 x5 : ι → ι → ι . x4)) x2))
Let x2 of type ι → ι → ι be given.
Assume H9: fb516.. x2.
Apply H0 with λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 (x1 (λ x4 x5 : ι → ι → ι . x4)) x2.
Apply and3I with (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 (x1 (λ x4 x5 : ι → ι → ι . x4)) x2) = λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 (x1 (λ x4 x5 : ι → ι → ι . x4)) x2, fb516.. (x1 (λ x3 x4 : ι → ι → ι . x3)), fb516.. x2 leaving 3 subgoals.
Let x3 of type (CT2 (ι → ι → ι)) → (CT2 (ι → ι → ι)) → ο be given.
Assume H10: x3 (λ x4 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x4 (x1 (λ x5 x6 : ι → ι → ι . x5)) x2) (λ x4 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x4 (x1 (λ x5 x6 : ι → ι → ι . x5)) x2).
The subproof is completed by applying H10.
The subproof is completed by applying H6.
The subproof is completed by applying H9.
Claim L10: ∀ x2 : ι → ι → ι . fb516.. x2 ⟶ 6fb7f.. (x0 (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 (x1 (λ x4 x5 : ι → ι → ι . x4)) x2))
Apply unknownprop_673b5a0ff482ed303e49c4de91639680dfe4eefa3123a40c753c65a98569c7a1 with λ x2 : ι → ι → ι . x0 (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 (x1 (λ x4 x5 : ι → ι → ι . x4)) x2), λ x2 x3 : ο . x2 leaving 2 subgoals.
The subproof is completed by applying L9.
The subproof is completed by applying L8.
Apply L10 with x1 (λ x2 x3 : ι → ι → ι . x3).
The subproof is completed by applying H7.
Assume H2: ∀ x1 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 64789.. x1 ⟶ 6fb7f.. (x0 x1).
Let x1 of type ι → ι → ι be given.
Assume H3: fb516.. x1.
Claim L4: ...
...
Apply unknownprop_673b5a0ff482ed303e49c4de91639680dfe4eefa3123a40c753c65a98569c7a1 with λ x2 : ι → ι → ι . x0 (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2), λ x2 x3 : ο . x3 leaving 2 subgoals.
The subproof is completed by applying L4.
Let x2 of type ι → ι → ι be given.
Assume H5: fb516.. x2.
Apply H2 with λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2.
Apply and3I with (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2) = λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2, fb516.. x1, fb516.. x2 leaving 3 subgoals.
Let x3 of type (CT2 (ι → ι → ι)) → (CT2 (ι → ι → ι)) → ο be given.
Assume H6: x3 (λ x4 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x4 x1 x2) (λ x4 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x4 x1 x2).
The subproof is completed by applying H6.
...
...
■