FPL Field: Message Field Definitions for Flight Planning

LeanSpec.FPL.Field defines the numbered ICAO fields that compose flight planning messages. Each field corresponds to a specific piece of flight information as defined in ICAO Doc 4444 (PANS-ATM), and the Lean types here capture both the structure and the validity constraints of each field. The module builds on LeanSpec.FPL.Core and LeanSpec.lib.Temporal, and also defines cross-field consistency checks — predicates that must hold between related fields when they appear together in a message. These inter-field constraints arise because the legacy flight plan format distributes related information across multiple fields, making explicit consistency proofs essential.

import LeanSpec.FPL.Core
import LeanSpec.lib.Temporal

open Core Temporal

namespace FPL.Field

Field 7: Aircraft Identification and SSR Mode and Code

Field 7 identifies how a flight is known to air traffic control. It combines the aircraft identification (call sign) with an optional SSR transponder code.

structure Field7 where
  f7a  : AircraftIdentification
  f7bc : Option SsrCode
deriving DecidableEq

Sub-field	Type	Description
`f7a`	`AircraftIdentification`	The ATC call sign or registration mark (2–7 chars)
`f7bc`	`Option SsrCode`	Optional SSR transponder code (4 octal chars); `none` if not assigned

Example: -SAS912/A5100

example := Field7.mk ⟨"SAS912", by trivial⟩ (some ⟨"5100", by trivial⟩)

Field 8: Flight Rules and Type of Flight

Field 8 provides information that determines how a flight is handled by ATC — the rules under which it operates and its broad category.

structure Field8 where
  f8a : FlightRules
  f8b : Option TypeOfFlight
deriving DecidableEq

Sub-field	Type	Description
`f8a`	`FlightRules`	Operating rules: `i` (IFR), `v` (VFR), `y` (IFR→VFR), `z` (VFR→IFR)
`f8b`	`Option TypeOfFlight`	Optional flight category: scheduled, non-scheduled, GA, military, other

Example: -IS

example := Field8.mk .i (some .s)

Field 9: Number and Type of Aircraft and Wake Turbulence Category

Field 9 describes the aircraft that will conduct the flight, including its type, wake turbulence category, and — for formation flights — the number of aircraft.

structure Field9 where
  f9a : Option NumberOfAircraft    -- only included for formation flights
  f9b : Option Doc8643.Designator  -- `none` indicates ZZZZ (refer field 18 TYP)
  f9c : WakeTurbulenceCategory
deriving DecidableEq

Sub-field	Type	Description
`f9a`	`Option NumberOfAircraft`	Number of aircraft (2–99); `none` for single aircraft
`f9b`	`Option Doc8643.Designator`	ICAO type designator (2–4 chars); `none` means ZZZZ — type given in Field 18 TYP
`f9c`	`WakeTurbulenceCategory`	Wake turbulence: `h` (heavy), `m` (medium), `l` (light)

Examples: -2FK27/M — formation of two FK27 aircraft, medium wake:

example := Field9.mk (some ⟨2, by trivial⟩) (some ⟨"FK27", by trivial⟩) .m

-ZZZZ/L — unknown type, light wake:

example := Field9.mk none none .l

Field 10: Equipment and Capabilities

Field 10 documents the communication, navigation, and surveillance equipment on board the aircraft, along with its capabilities. These items tell ATC what services the flight can participate in and what limitations apply.

structure Field10 where
  f10a : Set CommNavAppCode    -- empty set indicates `N` (no equipment)
  f10b : Set SurveillanceCode  -- empty set indicates `N` (no surveillance)
  -- Exclude invalid combinations.
  inv  : ¬ (.b1 ∈ f10b ∧ .b2 ∈ f10b) ∧
         ¬ (.u1 ∈ f10b ∧ .u2 ∈ f10b) ∧
         ¬ (.v1 ∈ f10b ∧ .v2 ∈ f10b)
deriving DecidableEq

Sub-field	Type	Description
`f10a`	`Set CommNavAppCode`	Comm/nav/approach aid codes; empty set = `N` (nil equipment)
`f10b`	`Set SurveillanceCode`	Surveillance codes; empty set = `N`

Invariant: Mutually exclusive surveillance code pairs are prohibited: b1/b2, u1/u2, and v1/v2 cannot be simultaneously present. Example: -SAFR/SV1

example := (⟨{.s, .a, .f, .r}, {.s, .v1}, sorry⟩ : Field10)

Field 13: Departure Aerodrome and Time

Field 13 records where and when the flight departs. A flight plan may be filed in the air (AFIL), in which case the departure point field carries a special indicator rather than an aerodrome designator.

`ADep`

inductive ADep
  | adep (_ : Doc7910.Designator)  -- known ICAO aerodrome
  | afil                           -- air-filed flight plan
deriving DecidableEq

`Field13a`

The departure aerodrome field, which is optional: none indicates ZZZZ (refer to Field 18 DEP for name/position).

def Field13a := Option ADep  -- `none` indicates ZZZZ (refer field 18 DEP)
deriving DecidableEq

`Field13`

structure Field13 where
  f13a : Field13a
  f13b : DTG
deriving DecidableEq

Sub-field	Type	Description
`f13a`	`Field13a`	Departure point: ICAO designator, AFIL, or ZZZZ (`none`)
`f13b`	`DTG`	Estimated off-block time (EOBT) as a date-time group

Examples: -EHAM0730

example := Field13.mk (some (.adep ⟨"EHAM", by trivial⟩)) 63072027000

-AFIL1625

example : Field13 := ⟨some .afil, 63072059100⟩

`Field13.desigOf`

Extracts the aerodrome designator from a Field13 if one is present. Returns none for AFIL or ZZZZ entries.

def Field13.desigOf : Field13 → Option Doc7910.Designator
  | {f13a := some (.adep desig), ..} => desig
  | _                                => none

Field 15: Route

Field 15 describes the route the aircraft will follow from departure to destination, including the initial cruising speed and level. Route descriptions can be complex: they reference named waypoints, ATS routes, direct segments, and may include in-route speed/level changes and flight rules changes.

`UpperLevel`

When climbing through levels, the upper target level can be specified explicitly or indicated as unbounded (plus).

inductive UpperLevel
  | level (_ : VerticalPositionOfAircraft)
  | plus
deriving DecidableEq

`SpeedLevelChange`

An in-route change of speed and level, with an optional upper bound on the climb.

structure SpeedLevelChange where
  speed : TrueAirspeed
  level : VerticalPositionOfAircraft
  upper : Option UpperLevel
deriving DecidableEq

Example: N0540A055PLUS

example : SpeedLevelChange where
  speed := ⟨⟨540, .kt, .ias, by simp⟩, sorry⟩
  level := ⟨5500, .feet, .altitude⟩
  upper := some .plus

`RoutePoint`

A specific geographic point along the route, at which speed, level, and/or flight rules changes may be specified.

structure RoutePoint where
  pos  : Position
  chg  : Option SpeedLevelChange
  frul : Option FlightRule
deriving DecidableEq

`Connector`

The path between two consecutive route points: either a named ATS route or a direct (DCT) segment.

inductive Connector
  | rte (_ : RouteDesignator)
  | dct
deriving DecidableEq

`RouteElement`

A route element pairs an optional point with the connector leading to the next element. At least one of the two must be present.

structure RouteElement where
  point : Option RoutePoint
  rte   : Option Connector
  -- At least one of point or connecting route must be populated.
  inv   : ¬ (point.isNone ∧ rte.isNone)
deriving DecidableEq

Accessor functions:

-- The named waypoint in a route element, if there is one.
def RouteElement.waypointOf : RouteElement → Option Waypoint
  | {point := some rp, ..} => rp.pos.waypointOf
  | _                      => none

-- The ATS route designator in a route element, if there is one.
def RouteElement.atsRteOf : RouteElement → Option RouteDesignator
  | {rte := some (.rte rd), ..} => rd
  | _                           => none

-- Does the route element indicate _direct_ to the next point?
def RouteElement.isDct : RouteElement → Bool
  | {rte := some .dct, ..} => true
  | _                      => false

-- The flight rules change in a route element, if there is one.
def RouteElement.ruleOf : RouteElement → Option FlightRule
  | {point := some rp, ..} => rp.frul
  | _                      => none

`Truncate`

A marker indicating that the route description has been truncated (the full route is too long for the message field).

inductive Truncate | t
deriving DecidableEq

`Route`

The full route description, consisting of an optional standard instrument departure (SID), the non-empty list of route elements, and an optional standard arrival route (STAR) or truncation indicator. Four structural invariants are enforced:

structure Route where
  sid            : Option RouteDesignator
  elements       : List RouteElement
  starOrTruncate : Option (RouteDesignator ⊕ Truncate)
  inv            : elements ≠ ∅ ∧
                   -- Consecutive flight rules changes must be distinct.
                   let rules := (elements.map RouteElement.ruleOf).reduceOption
                   rules.Chain' (· ≠ ·) ∧
                   -- DCT must be followed by an explicit point.
                   elements.Chain' (·.isDct → ·.point.isSome) ∧
                   -- An ATS route designator must connect to another designator or a named point.
                   elements.Chain'
                     (fun re₁ re₂ ↦ re₁.atsRteOf.isSome →
                        re₂.waypointOf.isSome ∨ (re₂.point.isNone ∧ re₂.atsRteOf.isSome))
deriving DecidableEq

Invariants:

At least one route element must be present.
Consecutive flight rules changes must be distinct (no redundant change).
A DCT connector must be followed by an element with an explicit point.
An ATS route designator must connect to either a named waypoint or another ATS route.

`Route.waypoints`

The set of all named waypoints explicitly referenced in a route.

def Route.waypoints (rte : Route) : Set Waypoint :=
  (rte.elements.map RouteElement.waypointOf).reduceOption.toSet

`Field15`

The complete Field 15, combining the initial speed, optional initial level (or VFR if absent), and the route.

structure Field15 where
  f15a : TrueAirspeed
  f15b : Option VerticalPositionOfAircraft  -- `none` indicates VFR
  f15c : Route
deriving DecidableEq

Sub-field	Type	Description
`f15a`	`TrueAirspeed`	Initial requested cruising speed
`f15b`	`Option VerticalPositionOfAircraft`	Initial requested cruising level; `none` = VFR (level at pilot’s discretion)
`f15c`	`Route`	Full route description

Example: -M079F380 DCT WOL H65 RAZZI Q29 LIZZI DCT

def exElems := [
  RouteElement.mk none (some .dct) (by trivial),
  RouteElement.mk (mkWpt ⟨"WOL", by trivial⟩) (some (.rte ⟨"H65", by trivial⟩)) (sorry),
  RouteElement.mk (mkWpt ⟨"RAZZI", by trivial⟩) (some (.rte ⟨"Q29", by trivial⟩)) (sorry),
  RouteElement.mk (mkWpt ⟨"LIZZI", by trivial⟩) (some .dct) (sorry)
]
where mkWpt (wpt : Waypoint) : Option RoutePoint :=
  some ⟨.wpt wpt, none, none⟩

example := {
  f15a := ⟨⟨790, .mach, .tas, by simp⟩, by simp⟩,  -- M079
  f15b := some ⟨380, .feet, .flightLevel⟩,          -- F380
  f15c := ⟨none, exElems, none, sorry⟩ : Field15    -- DCT WOL H65 RAZZI Q29 LIZZI DCT
}

Field 16: Destination Aerodrome, Total Estimated Elapsed Time, and Alternates

Field 16 records the planned destination aerodrome, the estimated total flight duration (TEET), and up to two alternate aerodromes in case diversion becomes necessary.

`Field16a`

The destination aerodrome field. none indicates ZZZZ — the destination has no ICAO designator and details are in Field 18 DEST.

abbrev Field16a := Option Doc7910.Designator  -- `none` indicates ZZZZ (refer field 18 DEST)

`maxAlternateDestinations`

def maxAlternateDestinations := 2

`Field16`

structure Field16 where
  f16a : Field16a
  f16b : Duration
  f16c : List Field16a
  inv  : f16b < Duration.oneDay ∧
         f16c.length ≤ maxAlternateDestinations
deriving DecidableEq

Sub-field	Type	Description
`f16a`	`Field16a`	Planned destination aerodrome
`f16b`	`Duration`	Total estimated elapsed time (TEET) — estimated flight duration
`f16c`	`List Field16a`	Alternate destination aerodromes (up to 2)

Invariants:

TEET must be less than one day.
No more than maxAlternateDestinations (2) alternate aerodromes.

Example: -EHAM0645 EBBR ZZZZ

example := Field16.mk (some ⟨"EHAM", by trivial⟩) 24300 [some ⟨"EBBR", by trivial⟩, none] (by trivial)

`adepIsAdes`

A helper predicate: returns true when the departure aerodrome (from Field 13a) and the destination aerodrome (from Field 16a) refer to the same location. Used in flight time estimation.

def adepIsAdes : Field13a → Field16a → Bool
  | none, none                       => True
  | some (.adep desig₁), some desig₂ => desig₁ = desig₂
  | _, _                             => False

Field 17: Arrival Aerodrome and Time

Field 17 records the actual arrival aerodrome and time. This may differ from the planned destination in Field 16 if the flight was diverted. It is only populated in arrival (ARR) messages.

structure Field17 where
  f17a : Option Doc7910.Designator  -- `none` indicates ZZZZ
  f17b : DTG
  f17c : Option FreeText
  -- Exactly one of designator and aerodrome name must be populated.
  inv  : f17a.isNone ↔ f17c.isSome
deriving DecidableEq

Sub-field	Type	Description
`f17a`	`Option Doc7910.Designator`	Actual arrival aerodrome designator; `none` = ZZZZ
`f17b`	`DTG`	Actual time of arrival
`f17c`	`Option FreeText`	Name of arrival aerodrome when no designator exists

Invariant: Exactly one of the aerodrome designator (f17a) and the aerodrome name (f17c) must be populated — if the designator is absent (ZZZZ), a name must be provided, and vice versa. Example: -ZZZZ1620 DEN HELDER

example := Field17.mk none 63072058800 (some ⟨"DEN HELDER", by trivial⟩)

Field 18: Other Information

Field 18 is a catch-all for diverse additional information that does not fit elsewhere in the flight plan. The current flight plan format has been in use for over 50 years, and backwards compatibility constraints mean that newer data — such as PBN codes — have been appended here rather than given dedicated fields. As a result Field 18 is a heterogeneous collection, and much of the inter-field constraint machinery exists to maintain consistency between Field 18 sub-items and the corresponding primary fields.

Supporting Types

`maxPbnCodes`

def maxPbnCodes := 8

`ElapsedTimePoint`

An elapsed time entry — the cumulative flight time from departure to a specific en-route point, typically a FIR boundary where control is transferred between ATS providers.

structure ElapsedTimePoint where
  point    : Doc7910.FIRDesignator ⊕ Position
  duration : Duration
deriving DecidableEq

instance : LT ElapsedTimePoint where
  lt et₁ et₂ := LT.lt et₁.duration et₂.duration

instance (x y : ElapsedTimePoint) : Decidable (x < y) :=
  inferInstanceAs (Decidable (x.duration < y.duration))

`DelayPoint`

A route point at which the flight goes off-plan for a specified duration. Used, for example, by law enforcement flights conducting covert operations.

structure DelayPoint where
  point    : Waypoint
  duration : Duration
deriving DecidableEq

`RouteToRevisedDestination`

A revised routing if the flight decides to divert en-route to an alternate destination.

structure RouteToRevisedDestination where
  destination : Doc7910.Designator
  route       : FreeText
deriving DecidableEq

`F18Dep`

The Field 18 DEP sub-item, which provides either a name/position for a departure without an ICAO designator, or the ATS unit responsible for an air-filed flight plan.

inductive F18Dep
  | namePos (_ : NameAndPosition)
  | unit (_ : ATSUnit)
deriving DecidableEq

`Field18`

The complete Field 18 structure. Most sub-items are optional; their presence is governed by cross-field constraints (see below).

structure Field18 where
  sts  : Set SpecialHandling
  pbn  : Set PBNCode
  nav  : Option FreeText
  com  : Option FreeText
  dat  : Option FreeText
  sur  : Option FreeText
  dep  : Option F18Dep
  dest : Option NameAndPosition
  reg  : Set Registration
  eet  : List ElapsedTimePoint
  sel  : Option SelcalCode
  typ  : Set (Option NumberOfAircraft × AircraftType)
  code : Option AircraftAddress
  dle  : Set DelayPoint
  opr  : Option FreeText
  orgn : Option FreeText
  per  : Option AircraftPerformance
  altn : List NameAndPosition
  ralt : Set LandingSite
  talt : Set LandingSite
  rif  : Option RouteToRevisedDestination
  rmk  : Option FreeText
  inv  : pbn.card ≤ maxPbnCodes ∧
         altn.length ≤ maxAlternateDestinations ∧
         eet.ascendingStrict
deriving DecidableEq

Sub-item	Type	Description
`sts`	`Set SpecialHandling`	Special handling indicators (e.g. `medevac`, `head`, `sar`)
`pbn`	`Set PBNCode`	PBN capability codes (max 8)
`nav`	`Option FreeText`	Other navigation equipment
`com`	`Option FreeText`	Communication capability details (required when `Z` in Field 10a)
`dat`	`Option FreeText`	Data link capability
`sur`	`Option FreeText`	Surveillance equipment details
`dep`	`Option F18Dep`	Departure point details (ZZZZ or AFIL)
`dest`	`Option NameAndPosition`	Destination details when Field 16a is ZZZZ
`reg`	`Set Registration`	Aircraft registration mark(s)
`eet`	`List ElapsedTimePoint`	Elapsed time entries in ascending duration order
`sel`	`Option SelcalCode`	SELCAL code
`typ`	`Set (Option NumberOfAircraft × AircraftType)`	Aircraft type details when Field 9b is ZZZZ
`code`	`Option AircraftAddress`	24-bit ICAO aircraft address (6 hex chars)
`dle`	`Set DelayPoint`	Delay points along the route
`opr`	`Option FreeText`	Aircraft operator
`orgn`	`Option FreeText`	Originator of the flight plan
`per`	`Option AircraftPerformance`	Aircraft performance category
`altn`	`List NameAndPosition`	Name/position of ZZZZ alternate aerodromes (max 2)
`ralt`	`Set LandingSite`	En-route alternate aerodromes
`talt`	`Set LandingSite`	Take-off alternate aerodromes
`rif`	`Option RouteToRevisedDestination`	Route to revised destination
`rmk`	`Option FreeText`	Free-text remarks

Invariants:

At most 8 PBN codes.
At most 2 ALTN entries.
EET list must be in strictly ascending duration order.

Example: -PBN/A1B1C1D1O2S2T1 NAV/RNP2 REG/VHXYZ SEL/AFPQ CODE/7C6DDF OPR/FLYOU ORGN/YSSYABCO PER/C

example : Field18 := {
  sts  := ∅,
  pbn  := {.a1, .b1, .c1, .d1, .o2, .s2, .t1},
  nav  := some ⟨"RNP2", by trivial⟩,
  com  := none, dat := none, sur := none,
  dep  := none, dest := none,
  reg  := {⟨"VHXYZ", by trivial⟩},
  eet  := [],
  sel  := some ⟨"AFPQ", by trivial⟩,
  typ  := ∅,
  code := some ⟨"7C6DDF", by trivial⟩,
  dle  := ∅,
  opr  := some ⟨"FLYOU", by trivial⟩,
  orgn := some ⟨"YSSYABCO", by trivial⟩,
  per  := some .c,
  altn := [], ralt := ∅, talt := ∅,
  rif  := none, rmk := none,
  inv  := by trivial
}

Cross-Field Consistency Checks

Because the legacy format distributes related information across multiple fields, a set of consistency predicates must hold whenever those fields appear together. These predicates are used as invariants in Flight, FPL, and Field22. The notation x ▹ y ‖ z is a conditional defined in LeanSpec.lib.Util: when x is none, it reduces to y; when x is some v, it reduces to z v.

`F8F15Level` — Fields 8 and 15 (Requested Level)

If the initial requested cruising level in Field 15 is absent (indicating VFR), then the initial flight rules in Field 8 must be v (VFR) or z (VFR first).

def F8F15Level (f8 : Field8) (f15 : Field15) : Prop :=
  f15.f15b ▹ f8.f8a ∈ [.v, .z] ‖ (fun _ ↦ True)

`F8F15Rule` — Fields 8 and 15 (Flight Rules)

The initial flight rules in Field 8 must be consistent with any in-route rules changes in Field 15:

No changes → Field 8 must be i or v (no change expected).
First change to VFR → Field 8 must be y (IFR first).
First change to IFR → Field 8 must be z (VFR first).

def F8F15Rule (f8 : Field8) (f15 : Field15) : Prop :=
  match (f15.f15c.elements.map RouteElement.ruleOf).reduceOption with
  | []        => f8.f8a ∈ [.i, .v]
  | .vfr :: _ => f8.f8a = .y
  | .ifr :: _ => f8.f8a = .z

`F9F18Typ` — Fields 9 and 18 (Aircraft Type)

If Field 9b contains a designator, Field 18 TYP must be empty.
If Field 9b is ZZZZ (none), Field 18 TYP must be non-empty.

def F9F18Typ : Field9 → Option Field18 → Prop
  | {f9b := some _, ..}, none                 => True
  | {f9b := some _, ..}, some {typ := ts, ..} => ts = ∅
  | {f9b := none, ..}, some {typ := ts, ..}   => ts ≠ ∅
  | {f9b := none, ..}, none                   => False

`F10F18Sts` — Fields 10 and 18 (RVSM)

RVSM capability (w in Field 10a) and NONRVSM status in Field 18 STS are mutually exclusive.

def F10F18Sts (f10 : Field10) (f18 : Option Field18) : Prop :=
  f18 ▹ (.w ∉ f10.f10a ∨ .nonrvsm ∉ ·.sts)

`F10F18Pbn` — Fields 10 and 18 (PBN)

If PBN-capable (r in Field 10a), then Field 18 PBN must be non-empty, and vice versa.

def F10F18Pbn (f10 : Field10) (f18 : Option Field18) : Prop :=
  f18 ▹ .r ∉ f10.f10a ‖ (.r ∈ f10.f10a ↔ ·.pbn ≠ ∅)

`F10F18Z` — Fields 10 and 18 (COM/NAV/DAT)

If z is specified in Field 10a (other communication/navigation equipment), at least one of Field 18 COM, NAV, or DAT must be populated.

def F10F18Z (f10 : Field10) (f18 : Option Field18) : Prop :=
  f18 ▹ .z ∉ f10.f10a
      ‖ (fun f18 ↦ .z ∈ f10.f10a ↔ f18.com.isSome ∨ f18.nav.isSome ∨ f18.dat.isSome)

`F13F18Dep` — Fields 13 and 18 (Departure)

The relationship between Field 13a and Field 18 DEP:

Known designator in 13a → Field 18 DEP absent.
ZZZZ in 13a → Field 18 DEP must carry a name and position.
AFIL in 13a → Field 18 DEP must carry an ATS unit.

def F13F18Dep : Field13 → Option Field18 → Prop
  | ⟨(some (.adep _)), _⟩, none
  | ⟨some (.adep _), _⟩, some {dep := none, ..}
  | ⟨none, _⟩, some {dep := some (.namePos _), ..}
  | ⟨some .afil, _⟩, some {dep := some (.unit _), ..} => True
  | _, _                                              => False

`F15F18Dle` — Fields 15 and 18 (Delay Points)

Every delay point named in Field 18 DLE must be explicitly listed as a waypoint in the Field 15 route.

def F15F18Dle (f15 : Field15) (f18 : Option Field18) : Prop :=
  f18 ▹ (·.dle.map (·.point) ⊆ f15.f15c.waypoints)

`F16F18Dest` — Fields 16 and 18 (Destination)

Known designator in Field 16a → Field 18 DEST absent.
ZZZZ in Field 16a → Field 18 DEST must carry a name and position.

def F16F18Dest : Field16 → Option Field18 → Prop
  | {f16a := some _, ..}, none
  | {f16a := some _, ..}, some {dest := none, ..}
  | {f16a := none, ..}, some {dest := some _, ..} => True
  | _, _                                          => False

`F16F18Eet` — Fields 16 and 18 (EET)

All elapsed time entries in Field 18 EET must be less than the total flight duration in Field 16b.

def F16F18Eet (f16 : Field16) (f18 : Option Field18) : Prop :=
  f18 ▹ (·.eet.all (·.duration < f16.f16b))

`F16F18Dle` — Fields 16 and 18 (Delay Duration)

The sum of all delay durations specified in Field 18 DLE must be less than the total flight duration in Field 16b.

def F16F18Dle (f16 : Field16) (f18 : Option Field18) : Prop :=
  f18 ▹ (fun x ↦ (x.dle.map (·.duration)).add 0 < f16.f16b)

`F16F18Altn` — Fields 16 and 18 (Alternates)

For each ZZZZ entry (none) in the Field 16c alternate list, there must be a corresponding name/position entry in Field 18 ALTN.

def F16F18Altn : Field16 → Option Field18 → Prop
  | {f16c := [], ..}, none => True
  | {f16c := altn16, ..}, some {altn := altn18, ..}
                           => (altn16.filter (·.isNone)).length = altn18.length
  | _, _                   => False

`F16F17Dest` — Fields 16 and 17 (Destination vs. Arrival)

The planned destination (Field 16a) must differ from the actual arrival aerodrome (Field 17a). If they were the same, an ARR message would be redundant.

def F16F17Dest (f16a : Field16a) (f17 : Option Field17) : Prop :=
  f17 ▹ (f16a ≠ ·.f17a)

Field 22: Amendment

Field 22 specifies modifications to an existing flight plan. If any sub-item of a field changes, the entire new field content must appear in Field 22 — partial updates are not permitted. At least one field must be present, and all changed fields must satisfy the same cross-field consistency constraints as the original flight plan.

structure Field22 where
  f7  : Option Field7
  f8  : Option Field8
  f9  : Option Field9
  f10 : Option Field10
  f13 : Option Field13
  f15 : Option Field15
  f16 : Option Field16
  f18 : Option Field18
  inv : (f7.isSome ∨ f8.isSome ∨ f9.isSome ∨ f10.isSome ∨
         f13.isSome ∨ f15.isSome ∨ f16.isSome ∨ f18.isSome) ∧
        (f8 ▹ fun f8 ↦ f15 ▹ (F8F15Level f8 ·)) ∧
        (f8 ▹ fun f8 ↦ f15 ▹ (F8F15Rule f8 ·)) ∧
        (f9 ▹ (F9F18Typ · f18)) ∧
        (f10 ▹ (F10F18Sts · f18)) ∧
        (f10 ▹ (F10F18Pbn · f18)) ∧
        (f10 ▹ (F10F18Z · f18)) ∧
        (f13 ▹ (F13F18Dep · f18)) ∧
        (f15 ▹ (F15F18Dle · f18)) ∧
        (f16 ▹ (F16F18Dest · f18)) ∧
        (f16 ▹ (F16F18Eet · f18)) ∧
        (f16 ▹ (F16F18Dle · f18)) ∧
        (f16 ▹ (F16F18Altn · f18))
deriving DecidableEq

Example: -8/IX-13/EDDN1230

example : Field22 where
  f7  := none
  f8  := some ⟨.i, some .x⟩
  f9  := none
  f10 := none
  f13 := some ⟨some (.adep ⟨"EDDN", by trivial⟩), 63072027000⟩
  f15 := none
  f16 := none
  f18 := none
  inv := by trivial

end FPL.Field

Support Libraries

Flight Planning Modules

Documentation Index

​Field 7: Aircraft Identification and SSR Mode and Code

​Field 8: Flight Rules and Type of Flight

​Field 9: Number and Type of Aircraft and Wake Turbulence Category

​Field 10: Equipment and Capabilities

​Field 13: Departure Aerodrome and Time

​ADep

​Field13a

​Field13

​Field13.desigOf

​Field 15: Route

​UpperLevel

​SpeedLevelChange

​RoutePoint

​Connector

​RouteElement

​Truncate

​Route

​Route.waypoints

​Field15

​Field 16: Destination Aerodrome, Total Estimated Elapsed Time, and Alternates

​Field16a

​maxAlternateDestinations

​Field16

​adepIsAdes

​Field 17: Arrival Aerodrome and Time

​Field 18: Other Information

​Supporting Types

​maxPbnCodes

​ElapsedTimePoint

​DelayPoint

​RouteToRevisedDestination

​F18Dep

​Field18

​Cross-Field Consistency Checks

​F8F15Level — Fields 8 and 15 (Requested Level)

​F8F15Rule — Fields 8 and 15 (Flight Rules)

​F9F18Typ — Fields 9 and 18 (Aircraft Type)

​F10F18Sts — Fields 10 and 18 (RVSM)

​F10F18Pbn — Fields 10 and 18 (PBN)

​F10F18Z — Fields 10 and 18 (COM/NAV/DAT)

​F13F18Dep — Fields 13 and 18 (Departure)

​F15F18Dle — Fields 15 and 18 (Delay Points)

​F16F18Dest — Fields 16 and 18 (Destination)

​F16F18Eet — Fields 16 and 18 (EET)

​F16F18Dle — Fields 16 and 18 (Delay Duration)

​F16F18Altn — Fields 16 and 18 (Alternates)

​F16F17Dest — Fields 16 and 17 (Destination vs. Arrival)

​Field 22: Amendment

Build docs developers (and LLMs) love

Field 7: Aircraft Identification and SSR Mode and Code

Field 8: Flight Rules and Type of Flight

Field 9: Number and Type of Aircraft and Wake Turbulence Category

Field 10: Equipment and Capabilities

Field 13: Departure Aerodrome and Time

`ADep`

`Field13a`

`Field13`

`Field13.desigOf`

Field 15: Route

`UpperLevel`

`SpeedLevelChange`

`RoutePoint`

`Connector`

`RouteElement`

`Truncate`

`Route`

`Route.waypoints`

`Field15`

Field 16: Destination Aerodrome, Total Estimated Elapsed Time, and Alternates

`Field16a`

`maxAlternateDestinations`

`Field16`

`adepIsAdes`

Field 17: Arrival Aerodrome and Time

Field 18: Other Information

Supporting Types

`maxPbnCodes`

`ElapsedTimePoint`

`DelayPoint`

`RouteToRevisedDestination`

`F18Dep`

`Field18`

Cross-Field Consistency Checks

`F8F15Level` — Fields 8 and 15 (Requested Level)

`F8F15Rule` — Fields 8 and 15 (Flight Rules)

`F9F18Typ` — Fields 9 and 18 (Aircraft Type)

`F10F18Sts` — Fields 10 and 18 (RVSM)

`F10F18Pbn` — Fields 10 and 18 (PBN)

`F10F18Z` — Fields 10 and 18 (COM/NAV/DAT)

`F13F18Dep` — Fields 13 and 18 (Departure)

`F15F18Dle` — Fields 15 and 18 (Delay Points)

`F16F18Dest` — Fields 16 and 18 (Destination)

`F16F18Eet` — Fields 16 and 18 (EET)

`F16F18Dle` — Fields 16 and 18 (Delay Duration)

`F16F18Altn` — Fields 16 and 18 (Alternates)

`F16F17Dest` — Fields 16 and 17 (Destination vs. Arrival)

Field 22: Amendment