Proofgold Proposition

∀ x0 x1 x2 . SNo x0 ⟶ (∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ ∀ x4 x5 . SNoCutP x4 x5 ⟶ x3 = SNoCut x4 x5 ⟶ minus_SNo x3 = SNoCut (prim5 x5 minus_SNo) (prim5 x4 minus_SNo)) ⟶ SNoCutP x1 x2 ⟶ (∀ x3 . x3 ∈ x2 ⟶ SNo x3) ⟶ x0 = SNoCut x1 x2 ⟶ SNoCutP (prim5 x2 minus_SNo) (prim5 x1 minus_SNo) ⟶ SNo (SNoCut (prim5 x2 minus_SNo) (prim5 x1 minus_SNo)) ⟶ (∀ x3 . SNo x3 ⟶ (∀ x4 . x4 ∈ prim5 x2 minus_SNo ⟶ SNoLt x4 x3) ⟶ (∀ x4 . x4 ∈ prim5 x1 minus_SNo ⟶ SNoLt x3 x4) ⟶ and (SNoLev (SNoCut (prim5 x2 minus_SNo) (prim5 x1 minus_SNo)) ⊆ SNoLev x3) (SNoEq_ (SNoLev (SNoCut (prim5 x2 minus_SNo) (prim5 x1 minus_SNo))) (SNoCut (prim5 x2 minus_SNo) (prim5 x1 minus_SNo)) x3)) ⟶ (∀ x3 . x3 ∈ prim5 x2 minus_SNo ⟶ SNoLt x3 (minus_SNo x0)) ⟶ (∀ x3 . x3 ∈ prim5 x1 minus_SNo ⟶ SNoLt (minus_SNo x0) x3) ⟶ minus_SNo x0 = SNoCut (prim5 x2 minus_SNo) (prim5 x1 minus_SNo)

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_minus_SNoCut_eq_lem__8__3

proofgold address
TMX2K..^{Conj_minus_SNoCut_eq_lem__8__3}

creator
35053 PrNpY../93de3..

owner
35061 PrNpY../72190..

term root
34872..