rainbow.math.lemmas.ncd-readings

signed/ncd-step

TheoremFor all inputsNo axiomsSource

signed/ncd-step :
  (ns-c ns-x ns-M ns-v : ℚ)
  (ns-hv : ns-v = data/Bool.rec (fun x₁₂ => ℚ) 0 (data/Bool.rec (fun x₁₆ => ℚ) (ns-x + 1) ns-M (signed/decide-at-most ns-M (ns-x + 1))) (signed/decide-at-most ns-c 0))
  → proposition/conjunction (disjunction) (∀ (ns-x0 : 0 ≤ ns-x), ∀ (ns-xM : ns-x ≤ ns-M), ∀ (ns-M0 : 0 ≤ ns-M), conjunction)
  where conjunction := proposition/conjunction (0 ≤ ns-v) (ns-v ≤ ns-M)
  where disjunction := proposition/disjunction (proposition/conjunction (ns-c ≤ 0) (proposition/conjunction (ns-v ≤ ns-M) (proposition/conjunction (ns-v ≤ ns-x + 1) (proposition/disjunction (ns-v = ns-M) (ns-v = ns-x + 1))))) (ns-v = 0)

+ = signed/add0 = signed/zero1 = signed/one= = signed/equivalent: equality of rational valuesℚ = signed/SignedRational≤ = signed/at-most