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.
set y3 to be add_SNo x0 (add_SNo x1 x2)
set y4 to be add_SNo y3 (add_SNo x1 x2)
Claim L3: ∀ x5 : ι → ο . x5 y4x5 y3
Let x5 of type ιο be given.
Assume H3: x5 (add_SNo y4 (add_SNo x2 y3)).
set y6 to be add_SNo x2 (add_SNo y3 y4)
set y7 to be add_SNo y3 (add_SNo x5 y4)
Claim L4: ∀ x8 : ι → ο . x8 y7x8 y6
Let x8 of type ιο be given.
Assume H4: x8 (add_SNo y4 (add_SNo y6 x5)).
set y9 to be λ x9 . x8
Apply add_SNo_com with x5, y6, λ x10 x11 . y9 (add_SNo y4 x10) (add_SNo y4 x11) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
set y8 to be λ x8 . y7
Apply L4 with λ x9 . y8 x9 y7y8 y7 x9 leaving 2 subgoals.
Assume H5: y8 y7 y7.
The subproof is completed by applying H5.
Apply add_SNo_assoc with x5, y7, y6, λ x9 . y8 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H2.
set y9 to be add_SNo (add_SNo x5 y7) y6
set y10 to be add_SNo (add_SNo y8 y6) y7
Claim L5: ∀ x11 : ι → ο . x11 y10x11 y9
Let x11 of type ιο be given.
Assume H5: x11 (add_SNo (add_SNo y9 y7) y8).
set y12 to be λ x12 . x11
Apply add_SNo_com with y7, y9, λ x13 x14 . y12 (add_SNo x13 y8) (add_SNo x14 y8) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
set y11 to be λ x11 . y10
Apply L5 with λ x12 . y11 x12 y10y11 y10 x12 leaving 2 subgoals.
Assume H6: y11 y10 y10.
The subproof is completed by applying H6.
set y12 to be λ x12 . y11
Apply add_SNo_assoc with y10, y8, y9, λ x13 x14 . y12 x14 x13 leaving 4 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying L5.
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.