Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.odd-monitor

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/odd_monitor.clj4 definitions, 4 theorems

AHoF V59 worked ODD monitor over the 2-D operating envelope [0,1] x [0,2]. The operating point (1/2, 1) lies inside the box, so the monitor accepts it. The point (1/2, 3) violates the second-dimension upper bound (3 > 2) and the point (2, 1) violates the first-dimension upper bound (2 > 1); either single violation drives the point outside the ODD, so the monitor rejects both -- the runtime alarm condition. Proved native and axiom-free. Scope (measured by the kernel): this module has 4 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.odd-monitor` prints this classification.

Depends onalgorithms.proofs.odd-monitor

ahof-v59/lo1 :
  → ℚ≥0

ahof-v59/hi1 :
  → ℚ≥0

ahof-v59/lo2 :
  → ℚ≥0

ahof-v59/hi2 :
  → ℚ≥0

ahof-v59/inside-accepted :
  → monitor/in-odd? ahof-v59/lo2 ahof-v59/hi1 1/2 ahof-v59/lo2 ahof-v59/hi2 1 = data/true

ahof-v59/dim2-above-rejected :
  → monitor/in-odd? ahof-v59/lo2 ahof-v59/hi1 1/2 ahof-v59/lo2 ahof-v59/hi2 3 = data/false

ahof-v59/dim1-above-rejected :
  → monitor/in-odd? ahof-v59/lo2 ahof-v59/hi1 2 ahof-v59/lo2 ahof-v59/hi2 1 = data/false

ahof-v59/odd-monitor :
  → proposition/conjunction (odd? = data/true) (odd?₁ = data/false)
  where odd? := monitor/in-odd? ahof-v59/lo2 ahof-v59/hi1 1/2 ahof-v59/lo2 ahof-v59/hi2 1
  where odd?₁ := monitor/in-odd? ahof-v59/lo2 ahof-v59/hi1 1/2 ahof-v59/lo2 ahof-v59/hi2 3