Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_9282c4fc031a36c9b2eafd476b3c98b0d2f015723908debe89fc7acd2c78f947 with 6, λ x0 x1 . x1 = ChurchNum_ii_7 ChurchNum2 ordsucc 0 leaving 2 subgoals.
The subproof is completed by applying nat_6.
Apply unknownprop_180b0fd5c0d77d89fc7c74d0519e38ad47b1b50cde73428ffe5103966c8941b7 with λ x0 x1 . add_nat (exp_nat 2 6) x1 = ChurchNum_ii_6 ChurchNum2 ordsucc (ChurchNum_ii_6 ChurchNum2 ordsucc 0).
Claim L0: ∀ x2 : ι → ο . x2 y1x2 y0
Let x2 of type ιο be given.
Apply unknownprop_1ecba3dd5eafa4f5c4681522469f6140788e091a78ad9f01e97cc0b6f2c0488f with ordsucc, nat_p, λ x3 . add_nat (exp_nat 2 6) x3, 0, λ x3 . x2 leaving 4 subgoals.
The subproof is completed by applying nat_ordsucc.
The subproof is completed by applying add_nat_SR with exp_nat 2 6.
The subproof is completed by applying nat_0.
Apply add_nat_0R with exp_nat 2 6, λ x3 x4 . ChurchNum_ii_6 ChurchNum2 ordsucc x4 = ChurchNum_ii_6 ChurchNum2 ordsucc (ChurchNum_ii_6 ChurchNum2 ordsucc 0), λ x3 . x2 leaving 2 subgoals.
Apply unknownprop_180b0fd5c0d77d89fc7c74d0519e38ad47b1b50cde73428ffe5103966c8941b7 with λ x3 x4 . ChurchNum_ii_6 ChurchNum2 ordsucc x4 = ChurchNum_ii_6 ChurchNum2 ordsucc (ChurchNum_ii_6 ChurchNum2 ordsucc 0).
Let x3 of type ιιο be given.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Let x2 of type ιιο be given.
Apply L0 with λ x3 . x2 x3 y1x2 y1 x3.
Assume H1: x2 y1 y1.
The subproof is completed by applying H1.