Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_a056e7e1d4164d24a60c8047a73979083395e5609e36aaee67608ba08eded8a1 with λ x0 x1 . mul_nat 2 x0 = 8.
set y0 to be mul_nat 2 (add_nat 2 2)
set y1 to be 8
Claim L0: ∀ x2 : ι → ο . x2 y1x2 y0
Let x2 of type ιο be given.
Assume H0: x2 8.
Apply mul_add_nat_distrL with 2, 2, 2, λ x3 . x2 leaving 4 subgoals.
The subproof is completed by applying nat_2.
The subproof is completed by applying nat_2.
The subproof is completed by applying nat_2.
Apply unknownprop_74ac8a784913fa4a6f9da3de96c05984e11ff1600ef66d703e49d6ee22ad106d with λ x3 x4 . add_nat x4 x4 = 8, λ x3 . x2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_58ff2b27b026e86dd7175f8c18dac8fe76e7f12b4c3407557df1571fd66d2cbc.
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.