45. Declining an airline change🔗

Requirement ONE-703. Of its 4 acceptance criteria, 2 are proven and 2 are open.

rule

Rules.OneOrder.AirlineChange.declineOffer
  (e : Rules.OneOrder.Change.ExcessPenalty)
  (w : Rules.OneOrder.AirlineChange.DeclineFees)
  (inv : Rules.OneOrder.AirlineChange.InvoluntaryReading)
  (n : Rules.OneOrder.AirlineChange.ChangeNotice)
  (affected : Rules.Core.Money)
  (t : Rules.OneOrder.AirlineChange.DeclineTerms)
  (d : Rules.OneOrder.AirlineChange.Decline) :
  Except Rules.OneOrder.Change.QuoteRejection
    Rules.OneOrder.Change.PriceDifferential
Rules.OneOrder.AirlineChange.declineOffer
  (e :
    Rules.OneOrder.Change.ExcessPenalty)
  (w :
    Rules.OneOrder.AirlineChange.DeclineFees)
  (inv :
    Rules.OneOrder.AirlineChange.InvoluntaryReading)
  (n :
    Rules.OneOrder.AirlineChange.ChangeNotice)
  (affected : Rules.Core.Money)
  (t :
    Rules.OneOrder.AirlineChange.DeclineTerms)
  (d :
    Rules.OneOrder.AirlineChange.Decline) :
  Except
    Rules.OneOrder.Change.QuoteRejection
    Rules.OneOrder.Change.PriceDifferential

EARS: When a customer declines an airline change through Cancel or Reshop, the system shall price it as a cancellation or change of the affected order items, with the airline's cancellation or change fee as the penalty.

Story: As a customer, I want to know what declining a change the airline made will cost me, so that I can choose between the changed trip, another trip and my money back.

Acceptance criteria:

ONE-703.1: When a customer declines an airline change through Cancel or Auto-cancellation, the system shall price a cancellation of the affected order items with a new price of zero.
ONE-703.2: When a customer declines an airline change through Reshop, the system shall price a change from the affected order items to the new items at their price.
ONE-703.4: If a customer declines an involuntary change through Cancel or Auto-cancellation, then the system shall charge no cancellation penalty.
ONE-703.5: If a customer declines an involuntary change through Reshop, then the system shall charge no change fee.

The differential comes from priceDifferential, with the reading of a penalty above the refundable value given. The sources do not say what Auto-cancellation cancels and refunds; the model prices it as a Cancel of the affected items. Whether the fees apply is the reading's (DeclineFees), and which changes are involuntary is another reading's (InvoluntaryReading).

45.1. How each acceptance criterion is checked🔗

A criterion is proven when a guarantee below proves it for every input, and example only when only examples check it.

Criterion	Status	Checked by
ONE-703.1	Proven	Auto cancellation, Carrier change declined, Decline by cancel, Cancel is priced as a cancellation
ONE-703.2	Proven	Decline by reshop, Reshop is priced as a change
ONE-703.4	Open	Auto cancellation, Decline by cancel, Penalty when declining an airline change
ONE-703.5	Open	Decline by reshop, Price of reshopping after airline change

45.2. Guarantees🔗

45.2.1. Cancel is priced as a cancellation🔗

guarantee

Rules.OneOrder.AirlineChange.decline_cancel_prices
  (e : Rules.OneOrder.Change.ExcessPenalty)
  (w : Rules.OneOrder.AirlineChange.DeclineFees)
  (inv : Rules.OneOrder.AirlineChange.InvoluntaryReading)
  (n : Rules.OneOrder.AirlineChange.ChangeNotice)
  (affected : Rules.Core.Money)
  (t : Rules.OneOrder.AirlineChange.DeclineTerms)
  (d : Rules.OneOrder.Change.PriceDifferential)
  (h :
    Rules.OneOrder.AirlineChange.declineOffer e w inv n affected t
        Rules.OneOrder.AirlineChange.Decline.cancel =
      Except.ok d) :
  d.oldPrice = affected ∧ d.newPrice.amount = 0
Rules.OneOrder.AirlineChange.decline_cancel_prices
  (e :
    Rules.OneOrder.Change.ExcessPenalty)
  (w :
    Rules.OneOrder.AirlineChange.DeclineFees)
  (inv :
    Rules.OneOrder.AirlineChange.InvoluntaryReading)
  (n :
    Rules.OneOrder.AirlineChange.ChangeNotice)
  (affected : Rules.Core.Money)
  (t :
    Rules.OneOrder.AirlineChange.DeclineTerms)
  (d :
    Rules.OneOrder.Change.PriceDifferential)
  (h :
    Rules.OneOrder.AirlineChange.declineOffer
        e w inv n affected t
        Rules.OneOrder.AirlineChange.Decline.cancel =
      Except.ok d) :
  d.oldPrice = affected ∧
    d.newPrice.amount = 0

Declining through Cancel is priced as a cancellation of the affected items, with a new price of zero.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria ONE-703.1.

45.2.2. Reshop is priced as a change🔗

guarantee

Rules.OneOrder.AirlineChange.decline_reshop_prices
  (e : Rules.OneOrder.Change.ExcessPenalty)
  (w : Rules.OneOrder.AirlineChange.DeclineFees)
  (inv : Rules.OneOrder.AirlineChange.InvoluntaryReading)
  (n : Rules.OneOrder.AirlineChange.ChangeNotice)
  (affected : Rules.Core.Money)
  (t : Rules.OneOrder.AirlineChange.DeclineTerms) (p : Rules.Core.Money)
  (d : Rules.OneOrder.Change.PriceDifferential)
  (h :
    Rules.OneOrder.AirlineChange.declineOffer e w inv n affected t
        (Rules.OneOrder.AirlineChange.Decline.reshop p) =
      Except.ok d) :
  d.oldPrice = affected ∧ d.newPrice = p
Rules.OneOrder.AirlineChange.decline_reshop_prices
  (e :
    Rules.OneOrder.Change.ExcessPenalty)
  (w :
    Rules.OneOrder.AirlineChange.DeclineFees)
  (inv :
    Rules.OneOrder.AirlineChange.InvoluntaryReading)
  (n :
    Rules.OneOrder.AirlineChange.ChangeNotice)
  (affected : Rules.Core.Money)
  (t :
    Rules.OneOrder.AirlineChange.DeclineTerms)
  (p : Rules.Core.Money)
  (d :
    Rules.OneOrder.Change.PriceDifferential)
  (h :
    Rules.OneOrder.AirlineChange.declineOffer
        e w inv n affected t
        (Rules.OneOrder.AirlineChange.Decline.reshop
          p) =
      Except.ok d) :
  d.oldPrice = affected ∧ d.newPrice = p

Declining through Reshop is priced as a change from the affected items to the new items at their price.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria ONE-703.2.

45.2.3. Penalty when declining an airline change🔗

guarantee

Rules.OneOrder.AirlineChange.decline_cancel_no_penalty
  (e : Rules.OneOrder.Change.ExcessPenalty)
  (w : Rules.OneOrder.AirlineChange.DeclineFees)
  (inv : Rules.OneOrder.AirlineChange.InvoluntaryReading)
  (n : Rules.OneOrder.AirlineChange.ChangeNotice)
  (affected : Rules.Core.Money)
  (t : Rules.OneOrder.AirlineChange.DeclineTerms)
  (d : Rules.OneOrder.Change.PriceDifferential)
  (hinv : inv.involuntary n.reason = true)
  (h :
    Rules.OneOrder.AirlineChange.declineOffer e w inv n affected t
        Rules.OneOrder.AirlineChange.Decline.cancel =
      Except.ok d) :
  d.penalty.amount = 0
Rules.OneOrder.AirlineChange.decline_cancel_no_penalty
  (e :
    Rules.OneOrder.Change.ExcessPenalty)
  (w :
    Rules.OneOrder.AirlineChange.DeclineFees)
  (inv :
    Rules.OneOrder.AirlineChange.InvoluntaryReading)
  (n :
    Rules.OneOrder.AirlineChange.ChangeNotice)
  (affected : Rules.Core.Money)
  (t :
    Rules.OneOrder.AirlineChange.DeclineTerms)
  (d :
    Rules.OneOrder.Change.PriceDifferential)
  (hinv : inv.involuntary n.reason = true)
  (h :
    Rules.OneOrder.AirlineChange.declineOffer
        e w inv n affected t
        Rules.OneOrder.AirlineChange.Decline.cancel =
      Except.ok d) :
  d.penalty.amount = 0

A customer who declines an involuntary change through Cancel, or whose seller lets it lapse into Auto-cancellation, pays no cancellation penalty.

Open question for the business. The sources offer Cancel as an answer to an airline change and never say whether the airline's fees apply; the cancellation page leaves penalties to the airline. Under the reading that applies the item's fees, the 50 EUR cancellation fee of the itinerary change worked example is charged for leaving a change the airline made. The example declineByCancel shows it. Do the airline's cancellation fees apply when the customer declines a change the airline imposed?

Open The proof is not complete. See the open questions chapter.

Checks acceptance criteria ONE-703.4.

45.2.4. Price of reshopping after airline change🔗

guarantee

Rules.OneOrder.AirlineChange.decline_reshop_no_fee
  (e : Rules.OneOrder.Change.ExcessPenalty)
  (w : Rules.OneOrder.AirlineChange.DeclineFees)
  (inv : Rules.OneOrder.AirlineChange.InvoluntaryReading)
  (n : Rules.OneOrder.AirlineChange.ChangeNotice)
  (affected : Rules.Core.Money)
  (t : Rules.OneOrder.AirlineChange.DeclineTerms) (p : Rules.Core.Money)
  (d : Rules.OneOrder.Change.PriceDifferential)
  (hinv : inv.involuntary n.reason = true)
  (h :
    Rules.OneOrder.AirlineChange.declineOffer e w inv n affected t
        (Rules.OneOrder.AirlineChange.Decline.reshop p) =
      Except.ok d) :
  d.penalty.amount = 0
Rules.OneOrder.AirlineChange.decline_reshop_no_fee
  (e :
    Rules.OneOrder.Change.ExcessPenalty)
  (w :
    Rules.OneOrder.AirlineChange.DeclineFees)
  (inv :
    Rules.OneOrder.AirlineChange.InvoluntaryReading)
  (n :
    Rules.OneOrder.AirlineChange.ChangeNotice)
  (affected : Rules.Core.Money)
  (t :
    Rules.OneOrder.AirlineChange.DeclineTerms)
  (p : Rules.Core.Money)
  (d :
    Rules.OneOrder.Change.PriceDifferential)
  (hinv : inv.involuntary n.reason = true)
  (h :
    Rules.OneOrder.AirlineChange.declineOffer
        e w inv n affected t
        (Rules.OneOrder.AirlineChange.Decline.reshop
          p) =
      Except.ok d) :
  d.penalty.amount = 0

A customer who declines an involuntary change through Reshop pays no change fee.

Open question for the business. The sources say a reshop after an airline change may or may not cost the customer more, and give no rule. Under the reading that applies the item's fees, the 40 EUR change fee of the itinerary change worked example is charged when the customer reshops away from flights the airline moved. The example declineByReshop shows it. Do change fees and fare differences apply when the customer reshops after an airline change, and which alternatives must the airline offer?

Open The proof is not complete. See the open questions chapter.

Checks acceptance criteria ONE-703.5.

45.3. Examples🔗

45.3.1. Auto cancellation🔗

example

Rules.OneOrder.AirlineChange.autoCancellation :
  List Rules.OneOrder.AirlineChange.AutoCancelled
Rules.OneOrder.AirlineChange.autoCancellation :
  List
    Rules.OneOrder.AirlineChange.AutoCancelled

Given the same paid trip at 1,000.00 EUR that the airline moved, and a notice that offers Accept until 5 November 12:00 UTC with Auto-cancellation, the pairing the follow-up actions page shows.

When the seller misses the time limit, and the cancellation is priced on 6 November under the reading where the airline's fees apply.

Then Auto-cancellation applies, and the customer loses the trip the airline changed, pays the 50 EUR cancellation fee and gets 950 EUR back.

What Lean computed:

Standing	Penalty	Due by airline
lapsed auto cancel	50.00 EUR	950.00 EUR

Checks acceptance criteria ONE-702.1, ONE-703.1, ONE-703.4.

45.3.2. Carrier change declined🔗

example

Rules.OneOrder.AirlineChange.carrierChangeDeclined :
  List Rules.OneOrder.AirlineChange.ReasonCase
Rules.OneOrder.AirlineChange.carrierChangeDeclined :
  List
    Rules.OneOrder.AirlineChange.ReasonCase

Given the same paid trip at 1,000.00 EUR, now operated by another carrier, and an airline that waives its fees on involuntary changes.

When the customer declines the change through Cancel, under each reading of which changes are involuntary.

Then where only a cancelled flight and a move to other flights count, the change of carrier is voluntary and the customer pays the 50 EUR cancellation fee. Where every change but the customer's own counts, the customer pays nothing.

What Lean computed:

Reading	Involuntary	Penalty	Due by airline
only cancelled and moved flights	no	50.00 EUR	950.00 EUR
every change but the customer's own	yes	0.00 EUR	1000.00 EUR

Checks acceptance criteria ONE-703.1.

45.3.3. Decline by cancel🔗

example

Rules.OneOrder.AirlineChange.declineByCancel :
  List Rules.OneOrder.AirlineChange.DeclineCase
Rules.OneOrder.AirlineChange.declineByCancel :
  List
    Rules.OneOrder.AirlineChange.DeclineCase

Given a paid return trip at 1,000.00 EUR that the airline moved to other flights, with the 50 EUR cancellation fee of the itinerary change worked example.

When the customer declines the change through Cancel, under each reading of the fees.

Then where the airline's fees apply, the customer pays 50 EUR for leaving a change the airline made and gets 950 EUR back. Where they are waived, the customer gets the full 1,000 EUR back.

What Lean computed:

Fees	Penalty	Due to airline	Due by airline	Type
the airline's fees apply	50.00 EUR	0.00 EUR	950.00 EUR	refund
the fees are waived	0.00 EUR	0.00 EUR	1000.00 EUR	refund

Checks acceptance criteria ONE-703.1, ONE-703.4.

45.3.4. Decline by reshop🔗

example

Rules.OneOrder.AirlineChange.declineByReshop :
  List Rules.OneOrder.AirlineChange.DeclineCase
Rules.OneOrder.AirlineChange.declineByReshop :
  List
    Rules.OneOrder.AirlineChange.DeclineCase

Given the same paid trip at 1,000.00 EUR that the airline moved, with the 40 EUR change fee of the itinerary change worked example.

When the customer declines the change through Reshop, to other flights at 1,000.00 EUR, under each reading of the fees.

Then where the airline's fees apply, the customer pays the 40 EUR change fee to move away from flights the airline chose. Where they are waived, the exchange is even.

What Lean computed:

Fees	Penalty	Due to airline	Due by airline	Type
the airline's fees apply	40.00 EUR	40.00 EUR	0.00 EUR	add col
the fees are waived	0.00 EUR	0.00 EUR	0.00 EUR	even exchange

Checks acceptance criteria ONE-703.2, ONE-703.5.

45.4. Open question🔗

The guarantee Penalty when declining an airline change is open: the example Auto cancellation, Decline by cancel shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.

45.5. Open question🔗

The guarantee Price of reshopping after airline change is open: the example Decline by reshop shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.