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