{-# OPTIONS --cubical-compatible #-}

open import Padova2025-zh-TW.ProgrammingBasics.Naturals.Base
open import Padova2025-zh-TW.ProvingBasics.Connectives.Conjunction
open import Padova2025-zh-TW.ProvingBasics.Connectives.More
import Padova2025-zh-TW.Recreational.Choice.Boxes.Base as Base
import Padova2025-zh-TW.Recreational.Choice.Boxes.Stage1 as Stage1
import Padova2025-zh-TW.Recreational.Choice.Boxes.Stage2 as Stage2

module Padova2025-zh-TW.Recreational.Choice.Boxes.Stage3
  (ℝ : Set) (n : ℕ) (R : Normalizer ℕ ℝ)
  (open Base ℝ n)
  (p : Player)
  (open Stage1 ℝ n p)
  (their-box-contents : I → ℝ)
  (open Stage2 ℝ n R p their-box-contents)
  (our-box-contents : J → ℝ)
  where

階段 3#

open Normalizer R

dummy : ℝ
dummy = our-box-contents (zero , λ ())

-- 我們這條通道（lane）的盒子，其中那個唯一未打開的盒子以 `dummy` 作為佔位符
mostly-our-lane : Config
mostly-our-lane = insert (succ M) our-box-contents dummy

our-guess : ℝ
our-guess = rep mostly-our-lane (succ M)