Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNo x1.
Assume H2: SNo x2.
Apply add_SNo_assoc with x0, x1, x2, λ x3 x4 . x4 = add_SNo x1 (add_SNo x0 x2) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply add_SNo_assoc with x1, x0, x2, λ x3 x4 . add_SNo (add_SNo x0 x1) x2 = x4 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
set y3 to be add_SNo (add_SNo x0 x1) x2
set y4 to be add_SNo (add_SNo x2 x1) y3
Claim L3: ∀ x5 : ι → ο . x5 y4x5 y3
Let x5 of type ιο be given.
Assume H3: x5 (add_SNo (add_SNo y3 x2) y4).
set y6 to be λ x6 . x5
Apply add_SNo_com with x2, y3, λ x7 x8 . y6 (add_SNo x7 y4) (add_SNo x8 y4) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Let x5 of type ιιο be given.
Apply L3 with λ x6 . x5 x6 y4x5 y4 x6.
Assume H4: x5 y4 y4.
The subproof is completed by applying H4.