AP-NAV-03 Atomic property → executable check

When “Skip to main” does not skip

Use ← → to present
Atomic property

A bypass must reach its exact target.

LTL presentation form

G(activate(skip) →
F≤2s(focus=main ∨ reading=main))

Bombadil implementation always(() =>
fullGateV2VerdictHolds("AP-NAV-03"))
Northstar
A long header comes
before the content.

Main content

s₀ · Focusskip link
a₀ · ActivateEnter
s₁ · Observetarget not reached
Verdictviolation