Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: ∀ x0 x1 x2 x3 x4 x5 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo (minus_SNo x2) ⟶ SNo (minus_SNo x5) ⟶ SNo (add_SNo x0 x1) ⟶ SNoLt (add_SNo x0 (add_SNo x1 (minus_SNo x2))) (add_SNo x3 (add_SNo x4 (minus_SNo x5))).
Claim L1: SNo 1
The subproof is completed by applying SNo_1.
Claim L2: SNo 0
The subproof is completed by applying SNo_0.
Claim L3: SNo (minus_SNo 0)
Apply minus_SNo_0 with λ x0 x1 . SNo x1.
The subproof is completed by applying L2.
Claim L4: not (SNo (add_SNo 1 0) ⟶ SNoLt (add_SNo 1 (add_SNo 0 (minus_SNo 0))) (add_SNo 0 (add_SNo 0 (minus_SNo 0))))
Apply add_SNo_minus_SNo_rinv with 0, λ x0 x1 . not (SNo (add_SNo 1 0) ⟶ SNoLt (add_SNo 1 x1) (add_SNo 0 x1)) leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Apply add_SNo_0R with 0, λ x0 x1 . not (SNo (add_SNo 1 0) ⟶ SNoLt (add_SNo 1 0) x1) leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Apply add_SNo_0R with 1, λ x0 x1 . not (SNo x1 ⟶ SNoLt x1 0) leaving 2 subgoals.
The subproof is completed by applying SNo_1.
Assume H4: SNo 1 ⟶ SNoLt 1 0.
Apply SNoLt_irref with 0.
Apply SNoLt_tra with 0, 1, 0 leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNo_0.
The subproof is completed by applying SNoLt_0_1.
Apply H4.
The subproof is completed by applying SNo_1.
Apply L4.
Apply H0 with 1, 0, 0, 0, 0, 0 leaving 8 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
The subproof is completed by applying L2.
The subproof is completed by applying L2.
The subproof is completed by applying L2.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
The subproof is completed by applying L3.
■