%Patch files loaded: patch2 version 1.2.2.102

$$$ceps.pvs
ceps : THEORY

  BEGIN
  % top-level theory: imports the main files with theorems about the
  % query and create_update functions. Each of these in turn import
  % the auxiliary lemmas needed to prove them, which include the PVS
  % translation of the IOSTS for the query and create/update functions.
  
  % for completeness, the PVS 2.3 library for finite sets is also included.
  % to prove every theorem, lemma, type-correcteness condition, and judgement
  % for type ESC-x  prove-importchain <CR> now.

  IMPORTING allslots_props,create_update_props

  END ceps

$$$create_update.pvs
create_update: THEORY
 BEGIN

  StatusType: TYPE =
  {x6A83, x9000, x9101, x9102, x9106, x9110, x9401, x9402, x9409, x940A,
   x9580}

  CompletionCode: TYPE = {x00}

  PowerType: TYPE = {OFF, ON}

  AidType: TYPE = {CEP, ERROR_AID}

  FCIType: TYPE = [# Status: StatusType #]

  CommandCodeType: TYPE =
  {NONE, SPECIFIC, ALLSLOTS00, ALLSLOTS01, REFCURR, LOGINQ00, LOGINQ01,
   LOADINIT, LOADCREDIT, ERROR_INQ}

  TxTypeType: TYPE =
  {TxLoad, TxUnload, TxExchange, TxPurchase, TxCancelLastPurchase}

  CommandType: TYPE =
  [# Command: CommandCodeType,
     Currency: nat,
     TxType: TxTypeType,
     DateTime: nat,
     AcqID: nat,
     LdvID: nat,
     LoadAmt: nat,
     ReturnRcep: bool,
     UpdateSlot: bool,
     UpdateOthr: bool,
     CompCode: CompletionCode,
     MacPresent: bool,
     Mac_S2: nat,
     R_LSAM: nat,
     NewBalMax: nat #]

  LogEntryType: TYPE =
  [# TxType: TxTypeType,
     TxDate: nat,
     TxCurr: nat,
     TxCurr2: nat,
     TxAuth: nat,
     TxAcqID: nat,
     TxRID: nat,
     TxPsamID: nat,
     TxLdvID: nat,
     TxAmt: nat,
     TxAmtStep: nat,
     TxNT: nat,
     TxBal: nat,
     TxBalMax: nat,
     TxBalOld: nat,
     TxBalSrc: nat,
     TxCC: StatusType,
     TxPosLoc: nat #]

  ReplyType: TYPE =
  [# SlotIndex: nat,
     Currency: nat,
     Balance: nat,
     BalMax: nat,
     Count: nat,
     RC_Curr_0: nat,
     RC_Max_0: nat,
     RC_Curr_1: nat,
     RC_Max_1: nat,
     RC_Curr_2: nat,
     RC_Max_2: nat,
     Entry: LogEntryType,
     IssId: nat,
     CardId: nat,
     DateExp: nat,
     NT_CEP: nat,
     S_1: nat,
     H_CEP: nat,
     CompCode: CompletionCode,
     S_3: nat,
     R_CEP: nat,
     Status: StatusType #]

  SlotType: TYPE =
  [# InUse: bool, Currency: nat, Fixed: bool, Balance: nat, BalMax: nat #]

  ReferenceCurrencyType: TYPE = [# Currency: nat, BalMax: nat #]

  LogArray: TYPE = [upto(63) -> LogEntryType];

  TransactionLogType: TYPE =
  [# pLogSize: nat, InUse: nat, NextInsert: nat, Entry: LogArray #]

  SlotArray: TYPE = [upto(15) -> SlotType]

  SlotsReported: TYPE = [upto(15) -> bool];

  ReportArrayType: TYPE = [upto(15) -> ReplyType];

  Action: DATATYPE
   BEGIN
    CepCommand(mCommand: CommandType): CepCommand?
    CepReply(mSlotInfo: ReplyType): CepReply?
    tau_CepIFL_InUse: tau_CepIFL_InUse?
    tau_CepIFL_NotInUse: tau_CepIFL_NotInUse?
   END Action

  Location: TYPE =
  {CepInit_P1, CepIFL_LocateSlot_P2, CepIFL_LoadPending_P3,
   CepCFL_CreditForLoad_P4}

  State: TYPE =
  [# pc: Location,
     vSlots: SlotArray,
     vNT: nat,
     vLoadAmount: nat,
     vSlotIndex: nat,
     vCurrencySought: nat,
     vSlotsAvailable: nat,
     vLastAvailSlot: nat, %%
     vNewBalMax: nat,
     actual: boolean #]

  pSlotCount: {n: nat | 1 <= n AND n <= 15}

  pRefCount: {n: nat | 0 <= n AND n <= 3}

  pLogSize: {n: nat | 0 < n AND n < 64}

  pNT_Limit, vIssId, vCardId, vDateExp: nat

  vDeactivated, vLocked: boolean

  initial(s: State): bool =
      (s`pc = CepInit_P1 AND
        s`actual AND
         (FORALL (i, j: below(pSlotCount)): (s`vSlots(i)`InUse AND 
            s`vSlots(j)`InUse AND i /= j)
               IMPLIES s`vSlots(i)`Currency /= s`vSlots(j)`Currency))

  next(s: State, a: Action): State =
      CASES a
        OF CepCommand(mTP_Inquiry):
             IF s`pc = CepInit_P1 AND
                 mTP_Inquiry`Command = LOADINIT AND
                  NOT (s`vNT >= pNT_Limit) AND
                   NOT vDeactivated AND NOT vLocked
               THEN s
                      WITH [pc := CepIFL_LocateSlot_P2,
                            vLoadAmount := mTP_Inquiry`LoadAmt,
                            vSlotIndex := 0,
                            vCurrencySought := mTP_Inquiry`Currency,
                            vSlotsAvailable := 0,
                            vLastAvailSlot := pSlotCount,
                            vNewBalMax := mTP_Inquiry`NewBalMax]
             ELSIF s`pc = CepIFL_LoadPending_P3 AND
                    mTP_Inquiry`Command = LOADCREDIT
                   THEN s WITH [pc := CepCFL_CreditForLoad_P4]
                   ELSE s WITH [actual := FALSE]
             ENDIF,
           CepReply(mCredLoadResp):
             IF s`pc = CepCFL_CreditForLoad_P4 AND s`vSlotIndex < pSlotCount AND %%
                 (NOT s`vSlots(s`vSlotIndex)`InUse) AND
                  mCredLoadResp`Balance = s`vLoadAmount AND
                   mCredLoadResp`CompCode = x00 AND
                    mCredLoadResp`Status = x9000
                    
               THEN s
                      WITH [pc := CepInit_P1,
                            vSlots
                              := s`vSlots
                                   WITH [(s`vSlotIndex)`InUse := TRUE,
                                         (s`vSlotIndex)`Currency
                                         := s`vCurrencySought,
                                         (s`vSlotIndex)`Fixed := FALSE,
                                         (s`vSlotIndex)`Balance
                                         := s`vLoadAmount,
                                         (s`vSlotIndex)`BalMax
                                         := s`vNewBalMax]]
	             ELSIF s`pc = CepCFL_CreditForLoad_P4 AND s`vSlotIndex < pSlotCount AND %%
                    s`vSlots(s`vSlotIndex)`InUse AND
                     mCredLoadResp`Balance = s`vLoadAmount AND
                      mCredLoadResp`CompCode = x00 AND
                       mCredLoadResp`Status = x9000
                   THEN s
                          WITH [pc := CepInit_P1,
                                vSlots
                                  := s`vSlots
                                     WITH [(s`vSlotIndex)`Balance
                                           := s`vLoadAmount,
                                           (s`vSlotIndex)`BalMax
                                           := s`vNewBalMax]]
                   ELSIF s`pc = CepIFL_LocateSlot_P2 AND
                          s`vSlotIndex >= pSlotCount AND
                           s`vSlotsAvailable /= 0 AND
                            mCredLoadResp`IssId = vIssId AND
                             mCredLoadResp`CardId = vCardId AND
                              mCredLoadResp`DateExp = vDateExp AND
                               mCredLoadResp`NT_CEP = s`vNT AND
                                mCredLoadResp`Status = x9000
                         THEN s
                                WITH [pc := CepIFL_LoadPending_P3,
                                      vSlotIndex := s`vLastAvailSlot,
                                      vNT := s`vNT + 1]
                         ELSIF s`pc = CepIFL_LocateSlot_P2 AND 
                                s`vSlotIndex < pSlotCount AND
                                 s`vSlots(s`vSlotIndex)`InUse AND
                                  s`vSlots(s`vSlotIndex)`Currency =
                                   s`vCurrencySought
                                   AND
                                   s`vSlots(s`vSlotIndex)`Balance +
                                    s`vLoadAmount
                                    <= s`vSlots(s`vSlotIndex)`BalMax
                                    AND
                                    mCredLoadResp`IssId = vIssId
                                    AND
                                    mCredLoadResp`CardId = vCardId
                                    AND
                                    mCredLoadResp`DateExp = vDateExp
                                    AND
                                    mCredLoadResp`NT_CEP = s`vNT
                                    AND
                                    mCredLoadResp`Status = x9000
                               THEN s
                                    WITH [pc := CepIFL_LoadPending_P3,
                                          vNT := s`vNT + 1]
                               ELSE s WITH [actual := FALSE]
             ENDIF,
           tau_CepIFL_InUse:
             IF s`pc = CepIFL_LocateSlot_P2 AND
                 s`vSlotIndex < pSlotCount AND
                  s`vSlots(s`vSlotIndex)`InUse AND
                   s`vSlots(s`vSlotIndex)`Currency /= s`vCurrencySought
               THEN s
                      WITH [pc := CepIFL_LocateSlot_P2,
                            vSlotIndex := s`vSlotIndex + 1]
             ELSE s WITH [actual := FALSE]
             ENDIF,
           tau_CepIFL_NotInUse:
             IF s`pc = CepIFL_LocateSlot_P2 AND
                 s`vSlotIndex < pSlotCount AND
                  NOT s`vSlots(s`vSlotIndex)`InUse
               THEN s
                      WITH [pc := CepIFL_LocateSlot_P2,
                            vSlotIndex := s`vSlotIndex + 1,
                            vSlotsAvailable := s`vSlotsAvailable + 1,
                            vLastAvailSlot := s`vSlotIndex]
             ELSE s WITH [actual := FALSE]
             ENDIF
        ENDCASES

  IMPORTING runs[State,
                 initial,
                 LAMBDA (s: State, s_: State):
                   actual(s) AND
                    actual(s_) AND (EXISTS (a: Action): s_ = next(s, a))]
 END create_update

$$$create_update.prf
(|create_update| (|pSlotCount_TCC1| "" (INST 1 "1") NIL NIL)
 (|pRefCount_TCC1| "" (INST 1 "1") NIL NIL)
 (|pLogSize_TCC1| "" (INST 1 "1") NIL NIL)
 (|initial_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|initial_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|initial_TCC3| "" (SUBTYPE-TCC) NIL NIL)
 (|initial_TCC4| "" (SUBTYPE-TCC) NIL NIL)
 (|next_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|next_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|next_TCC3| "" (SUBTYPE-TCC) NIL NIL)
 (|next_TCC4| "" (SUBTYPE-TCC) NIL NIL)
 (|next_TCC5| "" (SUBTYPE-TCC) NIL NIL))


$$$create_update_aux.pvs
create_update_aux: THEORY
 BEGIN

  IMPORTING create_update

  create_update_aux4: LEMMA
    invariant(LAMBDA (s: State):
                (s`pc = CepIFL_LocateSlot_P2 IMPLIES
                  (FORALL (k: below(pSlotCount)):
                     (k < s`vSlotIndex AND s`vSlots(k)`InUse) IMPLIES
                      s`vSlots(k)`Currency /= s`vCurrencySought)))

  create_update_aux3: LEMMA
    invariant(LAMBDA (s: State):
                (s`pc = CepIFL_LocateSlot_P2 AND s`vSlotsAvailable /= 0)
                 IMPLIES s`vLastAvailSlot < pSlotCount)

  create_update_aux2: LEMMA
    invariant(LAMBDA (s: State):
                (s`pc = CepIFL_LoadPending_P3 OR
                  s`pc = CepCFL_CreditForLoad_P4)
                 IMPLIES s`vSlotIndex < pSlotCount)

  create_update_aux1: LEMMA
    invariant(LAMBDA (s: State):
                (s`pc = CepCFL_CreditForLoad_P4 OR
                  s`pc = CepIFL_LoadPending_P3)
                 IMPLIES
                 (s`vSlotIndex < pSlotCount AND
                   (NOT s`vSlots(s`vSlotIndex)`InUse IMPLIES
                     (FORALL (j: below(pSlotCount)):
                        s`vSlots(j)`InUse IMPLIES
                         s`vSlots(j)`Currency /= s`vCurrencySought))))
 END create_update_aux

$$$create_update_aux.prf
(|create_update_aux|
 (|create_update_aux4_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|create_update_aux4_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|create_update_aux4| "" (LEMMA "invariant_rule")
  (("" (INST?)
    (("1" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (HIDE 2)
        (("2" (SKOLEM 1 "r")
          (("2" (TYPEPRED "r")
            (("2" (BETA)
              (("2" (SPLIT)
                (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL)
                 ("2" (HIDE -2)
                  (("2" (SKOLEM 1 "n")
                    (("2" (FLATTEN)
                      (("2" (EXPAND "run_fragment")
                        (("2" (INST -3 "n")
                          (("2" (GROUND)
                            (("1" (SKOLEM 1 "k")
                              (("1"
                                (TYPEPRED "k")
                                (("1"
                                  (INST -2 "k")
                                  (("1" (GRIND) NIL NIL))
                                  NIL))
                                NIL))
                              NIL)
                             ("2" (GRIND) NIL NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL)
     ("3" (HIDE 2) (("3" (GRIND) NIL NIL)) NIL))
    NIL))
  NIL)
 (|create_update_aux3| "" (LEMMA "invariant_rule")
  (("" (INST?)
    (("" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (HIDE 2)
        (("2" (SKOLEM 1 "r")
          (("2" (TYPEPRED "r")
            (("2" (BETA)
              (("2" (SPLIT)
                (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL)
                 ("2" (HIDE -2)
                  (("2" (SKOLEM 1 "n")
                    (("2" (FLATTEN)
                      (("2" (EXPAND "run_fragment")
                        (("2" (INST -3 "n") (("2" (GRIND) NIL NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|create_update_aux2| "" (LEMMA "invariant_rule")
  (("" (INST?)
    (("" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (HIDE 2)
        (("2" (SKOLEM 1 "r")
          (("2" (TYPEPRED "r")
            (("2" (BETA)
              (("2" (SPLIT)
                (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL)
                 ("2" (HIDE -2)
                  (("2" (SKOLEM 1 "n")
                    (("2" (FLATTEN)
                      (("2" (EXPAND "run_fragment")
                        (("2" (INST -3 "n")
                          (("2" (GRIND)
                            (("2" (LEMMA "create_update_aux3")
                              (("2" (GRIND) NIL NIL)) NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|create_update_aux1_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|create_update_aux1_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|create_update_aux1_TCC3| "" (SUBTYPE-TCC) NIL NIL)
 (|create_update_aux1| "" (LEMMA "invariant_rule")
  (("" (INST?)
    (("1" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (HIDE 2)
        (("2" (SKOLEM 1 "r")
          (("2" (TYPEPRED "r")
            (("2" (BETA)
              (("2" (SPLIT)
                (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL)
                 ("2" (HIDE -2)
                  (("2" (SKOLEM 1 "n")
                    (("2" (FLATTEN)
                      (("2" (EXPAND "run_fragment")
                        (("2" (INST -3 "n")
                          (("2" (GROUND)
                            (("1" (GRIND) NIL NIL)
                             ("2" (SKOLEM 2 "j")
                              (("2"
                                (TYPEPRED "j")
                                (("2"
                                  (INST -3 "j")
                                  (("2" (GRIND) NIL NIL))
                                  NIL))
                                NIL))
                              NIL)
                             ("3" (GRIND) NIL NIL)
                             ("4" (SKOLEM 2 "j")
                              (("4"
                                (TYPEPRED "j")
                                (("4"
                                  (INST -3 "j")
                                  (("4" (GRIND) NIL NIL))
                                  NIL))
                                NIL))
                              NIL)
                             ("5" (GRIND) NIL NIL)
                             ("6" (GRIND) NIL NIL)
                             ("7" (GRIND) NIL NIL)
                             ("8" (GRIND) NIL NIL)
                             ("9" (GRIND) NIL NIL)
                             ("10" (GRIND) NIL NIL)
                             ("11" (GRIND)
                              (("11"
                                (LEMMA "create_update_aux3")
                                (("11" (GRIND) NIL NIL))
                                NIL))
                              NIL)
                             ("12" (SKOLEM 2 "j")
                              (("12"
                                (TYPEPRED "j")
                                (("12"
                                  (GRIND)
                                  (("12"
                                    (LEMMA "create_update_aux4")
                                    (("12"
                                      (EXPAND "invariant")
                                      (("12"
                                        (INST?)
                                        (("12"
                                          (GROUND)
                                          (("12"
                                            (INST -1 "j")
                                            (("12" (GRIND) NIL NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL)
     ("3" (HIDE 2) (("3" (GRIND) NIL NIL)) NIL)
     ("4" (HIDE 2) (("4" (GRIND) NIL NIL)) NIL))
    NIL))
  NIL))


$$$create_update_props.pvs
create_update_props: THEORY
 BEGIN

  IMPORTING create_update_aux

  create_update: THEOREM
    invariant(LAMBDA (s: State):
                FORALL (i, j: below(pSlotCount)):
                  (s`vSlots(i)`InUse AND s`vSlots(j)`InUse AND i /= j)
                   IMPLIES s`vSlots(i)`Currency /= s`vSlots(j)`Currency)

END create_update_props

$$$create_update_props.prf
(|create_update_props| (|create_update_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|create_update_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|create_update| "" (LEMMA "invariant_rule")
  (("" (INST?)
    (("1" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (HIDE 2)
        (("2" (SKOLEM 1 "r")
          (("2" (TYPEPRED "r")
            (("2" (BETA)
              (("2" (SPLIT)
                (("1" (HIDE -1)
                  (("1" (SKOLEM 1 ("i" "j"))
                    (("1" (TYPEPRED "i")
                      (("1" (TYPEPRED "j") (("1" (GRIND) NIL NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL)
                 ("2" (HIDE -2)
                  (("2" (SKOLEM 1 "n")
                    (("2" (FLATTEN)
                      (("2" (SKOLEM 1 ("i" "j"))
                        (("2" (TYPEPRED "i")
                          (("2" (TYPEPRED "j")
                            (("2" (INST -3 "i" "j")
                              (("2"
                                (EXPAND "run_fragment")
                                (("2"
                                  (INST -4 "n")
                                  (("2"
                                    (GRIND)
                                    (("1"
                                      (LEMMA "create_update_aux1")
                                      (("1"
                                        (EXPAND "invariant")
                                        (("1"
                                          (INST?)
                                          (("1"
                                            (GROUND)
                                            (("1"
                                              (INST -1 "j")
                                              (("1" (GRIND) NIL NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL)
                                     ("2"
                                      (LEMMA "create_update_aux1")
                                      (("2"
                                        (EXPAND "invariant")
                                        (("2"
                                          (INST?)
                                          (("2"
                                            (GROUND)
                                            (("2"
                                              (INST -1 "i")
                                              (("2" (GRIND) NIL NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL)
                                     ("3"
                                      (LEMMA "create_update_aux1")
                                      (("3"
                                        (EXPAND "invariant")
                                        (("3"
                                          (INST?)
                                          (("3"
                                            (GROUND)
                                            (("3"
                                              (INST -1 "i")
                                              (("3" (GRIND) NIL NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL)
                                     ("4"
                                      (LEMMA "create_update_aux1")
                                      (("4"
                                        (EXPAND "invariant")
                                        (("4"
                                          (INST?)
                                          (("4"
                                            (GROUND)
                                            (("4"
                                              (INST -1 "j")
                                              (("4" (GRIND) NIL NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL)
     ("3" (HIDE 2) (("3" (GRIND) NIL NIL)) NIL)
     ("4" (HIDE 2) (("4" (GRIND) NIL NIL)) NIL)
     ("5" (HIDE 2) (("5" (GRIND) NIL NIL)) NIL))
    NIL))
  NIL))


$$$runs.pvs


runs[State : TYPE, 
     initial : PRED[State], 
     transition : [State, State -> bool]] : THEORY

BEGIN


%runs are infinite sequences of transition-related states,  starting in an initial state


run_fragment: pred[sequence[State]] =  {r : sequence[State] | FORALL (n : nat):  transition(r(n),r(n+1))}

run : pred[(run_fragment)] =  {r : (run_fragment) | initial(r(0))}

r: VAR (run)
p :VAR [State->boolean]


invariant(p) : bool = FORALL (r : (run), n:nat ): p(r(n))



invariant_rule : LEMMA  (FORALL (r : (run)) : p(r(0)) AND FORALL (n : nat) : p(r(n)) IMPLIES p(r(n+1)))
                          IMPLIES invariant(p)


END runs




$$$runs.prf
(|runs|
 (|invariant_rule| "" (SKOSIMP*)
  (("" (EXPAND "invariant") (("" (INDUCT-AND-SIMPLIFY "n") NIL NIL))
    NIL))
  NIL))


$$$allslots.pvs
allslots: THEORY
 BEGIN

  StatusType: TYPE =
  {x6A83, x9000, x9101, x9102, x9106, x9110, x9401, x9402, x9409, x940A,
   x9580}

  CompletionCode: TYPE = {x00}

  PowerType: TYPE = {OFF, ON}

  AidType: TYPE = {CEP, ERROR_AID}

  FCIType: TYPE = [# Status: StatusType #]

  CommandCodeType: TYPE =
  {NONE, SPECIFIC, ALLSLOTS00, ALLSLOTS01, REFCURR, LOGINQ00, LOGINQ01,
   LOADINIT, LOADCREDIT, ERROR_INQ}

  TxTypeType: TYPE =
  {TxLoad, TxUnload, TxExchange, TxPurchase, TxCancelLastPurchase}

  CommandType: TYPE =
  [# Command: CommandCodeType,
     Currency: nat,
     TxType: TxTypeType,
     DateTime: nat,
     AcqID: nat,
     LdvID: nat,
     LoadAmt: nat,
     ReturnRcep: bool,
     UpdateSlot: bool,
     UpdateOthr: bool,
     CompCode: CompletionCode,
     MacPresent: bool,
     Mac_S2: nat,
     R_LSAM: nat,
     NewBalMax: nat #]

  LogEntryType: TYPE =
  [# TxType: TxTypeType,
     TxDate: nat,
     TxCurr: nat,
     TxCurr2: nat,
     TxAuth: nat,
     TxAcqID: nat,
     TxRID: nat,
     TxPsamID: nat,
     TxLdvID: nat,
     TxAmt: nat,
     TxAmtStep: nat,
     TxNT: nat,
     TxBal: nat,
     TxBalMax: nat,
     TxBalOld: nat,
     TxBalSrc: nat,
     TxCC: StatusType,
     TxPosLoc: nat #]

  ReplyType: TYPE =
  [# SlotIndex: nat,
     Currency: nat,
     Balance: nat,
     BalMax: nat,
     Count: nat,
     RC_Curr_0: nat,
     RC_Max_0: nat,
     RC_Curr_1: nat,
     RC_Max_1: nat,
     RC_Curr_2: nat,
     RC_Max_2: nat,
     Entry: LogEntryType,
     IssId: nat,
     CardId: nat,
     DateExp: nat,
     NT_CEP: nat,
     S_1: nat,
     H_CEP: nat,
     CompCode: CompletionCode,
     S_3: nat,
     R_CEP: nat,
     Status: StatusType #]

  SlotType: TYPE =
  [# InUse: bool, Currency: nat, Fixed: bool, Balance: nat, BalMax: nat #]

  ReferenceCurrencyType: TYPE = [# Currency: nat, BalMax: nat #]

  LogArray: TYPE = [upto(63) -> LogEntryType];

  TransactionLogType: TYPE =
  [# pLogSize: nat, InUse: nat, NextInsert: nat, Entry: LogArray #]

  SlotArray: TYPE = [upto(15) -> SlotType]

  SlotsReported: TYPE = [upto(15) -> bool];

  ReportArrayType: TYPE = [upto(15) -> ReplyType];

  Action: DATATYPE
   BEGIN
    CepCommand(mCommand: CommandType): CepCommand?
    CepReply(mSlotInfo: ReplyType): CepReply?
    tau_CepSIQ_InUse: tau_CepSIQ_InUse?
    tau_CepSIQ_NotInUse: tau_CepSIQ_NotInUse?
    tau_CepSIQ_Complete: tau_CepSIQ_Complete?
   END Action

  Location: TYPE =
  {CepInit_P1, CepSlotInquirySequence_P2, CepSIQ_Reply_P2, CepSIQ_Ready_P2}

  State: TYPE =
  [# pc: Location,
     slotsReported: SlotsReported,
     vSlotIndex: nat,
     vSlotsReported: nat,
     reportSize: nat,
     report: ReportArrayType,
     actual: boolean #]

  pSlotCount: {n: nat | 1 <= n AND n <= 16}

  pRefCount: {n: nat | 0 <= n AND n <= 3}

  pLogSize: {n: nat | 0 < n AND n < 64}

  vSlots:
  {s: SlotArray |
           FORALL (i, j: below(pSlotCount)):
             i /= j AND s(i)`InUse AND s(j)`InUse IMPLIES
              s(i)`Currency /= s(j)`Currency}

  initial(s: State): bool = (s`pc = CepInit_P1 AND s`actual)

  next(s: State, a: Action): State =
      CASES a
        OF CepCommand(mTP_Inquiry):
             IF s`actual AND
                 s`pc = CepInit_P1 AND mTP_Inquiry`Command = ALLSLOTS00
               THEN s
                      WITH [pc := CepSlotInquirySequence_P2,
                            vSlotIndex := 0,
                            vSlotsReported := 0,
                            reportSize := 0]
             ELSIF s`pc = CepSIQ_Ready_P2 AND
                    mTP_Inquiry`Command = ALLSLOTS01
                   THEN s WITH [pc := CepSIQ_Reply_P2]
                   ELSE s WITH [actual := FALSE]
             ENDIF,
           CepReply(mSlotInfo):
             IF s`actual AND
                 s`pc = CepSIQ_Reply_P2 AND
                  s`vSlotsReported < pSlotCount AND
                   0 <= mSlotInfo`SlotIndex AND
                    mSlotInfo`SlotIndex < pSlotCount AND
                     NOT (s`slotsReported(mSlotInfo`SlotIndex)) AND
                      vSlots(mSlotInfo`SlotIndex)`InUse AND
                       mSlotInfo`Currency =
                        vSlots(mSlotInfo`SlotIndex)`Currency
                        AND
                        mSlotInfo`Balance =
                         vSlots(mSlotInfo`SlotIndex)`Balance
                         AND
                         mSlotInfo`BalMax =
                          vSlots(mSlotInfo`SlotIndex)`BalMax
                          AND
                          mSlotInfo`Status = x9000 AND
                           s`reportSize < pSlotCount
               THEN s WITH [pc := CepSIQ_Ready_P2,
                            slotsReported
                              := s`slotsReported
                                   WITH [(mSlotInfo`SlotIndex) := TRUE],
                            vSlotsReported := s`vSlotsReported + 1,
                            reportSize := s`reportSize + 1,
                            report
                              := s`report
                                   WITH [(s`reportSize)`Currency := 
                                         vSlots (mSlotInfo`SlotIndex)`Currency,
                                        (s`reportSize)`Balance := 
                                             vSlots (mSlotInfo`SlotIndex)`Balance,
                                        (s`reportSize)`Status := x9000]]
             ELSIF s`pc = CepSIQ_Reply_P2 AND
                    s`vSlotIndex >= pSlotCount AND
                     s`vSlotsReported >= pSlotCount AND
                      mSlotInfo`Status = x6A83
                   THEN s WITH [pc := CepInit_P1]
                   ELSE s WITH [actual := FALSE]
             ENDIF,
           tau_CepSIQ_InUse:
             IF s`actual AND
                 s`pc = CepSlotInquirySequence_P2 AND
                  s`vSlotIndex < pSlotCount AND vSlots(s`vSlotIndex)`InUse
               THEN s
                      WITH [pc := CepSlotInquirySequence_P2,
                            vSlotIndex := s`vSlotIndex + 1,
                            slotsReported
                              := s`slotsReported
                                   WITH [(s`vSlotIndex) := FALSE]]
             ELSE s WITH [actual := FALSE]
             ENDIF,
           tau_CepSIQ_NotInUse:
             IF s`actual AND
                 s`pc = CepSlotInquirySequence_P2 AND
                  s`vSlotIndex < pSlotCount AND
                   NOT vSlots(s`vSlotIndex)`InUse
               THEN s
                      WITH [pc := CepSlotInquirySequence_P2,
                            vSlotIndex := s`vSlotIndex + 1,
                            vSlotsReported := s`vSlotsReported + 1,
                            slotsReported
                              := s`slotsReported
                                   WITH [(s`vSlotIndex) := TRUE]]
             ELSE s WITH [actual := FALSE]
             ENDIF,
           tau_CepSIQ_Complete:
             IF s`actual AND
                 s`pc = CepSlotInquirySequence_P2 AND
                  s`vSlotIndex = pSlotCount
               THEN s WITH [pc := CepSIQ_Reply_P2]
             ELSE s WITH [actual := FALSE]
             ENDIF
        ENDCASES

  IMPORTING runs[State,
                 initial,
                 LAMBDA (s: State, s_: State):
                   actual(s) AND
                    actual(s_) AND (EXISTS (a: Action): s_ = next(s, a))]
 END allslots

$$$allslots.prf
(|allslots| (|pSlotCount_TCC1| "" (QE) (("" (PROPAX) NIL NIL)) NIL)
 (|pRefCount_TCC1| "" (QE) (("" (PROPAX) NIL NIL)) NIL)
 (|pLogSize_TCC1| "" (QE) (("" (PROPAX) NIL NIL)) NIL)
 (|vSlots_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|vSlots_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|vSlots_TCC3| ""
  (INST 1
   "LAMBDA(i: upto(15)) : (#InUse := false, Currency := i, Fixed:= false, Balance := 0 , BalMax := 0 #)")
  NIL NIL)
 (|next_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|next_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|next_TCC3| "" (SUBTYPE-TCC) NIL NIL)
 (|next_TCC4| "" (SUBTYPE-TCC) NIL NIL)
 (|next_TCC5| "" (SUBTYPE-TCC) NIL NIL)
 (|next_TCC6| "" (SUBTYPE-TCC) NIL NIL))


$$$finite_sets/more_finite_sets.pvs
more_finite_sets[T1: TYPE+,T2: TYPE]: THEORY

BEGIN
IMPORTING finite_sets[T1]



%the image of a finite set through a function is finite
finite_image : LEMMA FORALL (S: finite_set[T1], f: [(S) -> T2]) :
is_finite({y: T2 | EXISTS (x :(S)) : y = f(x)})

%the inverse of an injective function (from its range to its domain) is
% a bijection. Domain need not be finite.



inverse_bijection : LEMMA FORALL (f: [T1 -> T2]) :
                        LET range = {y:T2| EXISTS (x:T1) : y = f(x)} IN
                            LET f_1:[(range) -> T1] = LAMBDA(y : (range)): epsilon({x:T1|y = f(x)})
                            IN injective?(f) IMPLIES bijective?(f_1)

END more_finite_sets

$$$finite_sets/more_finite_sets.prf
(|more_finite_sets|
 (|finite_image| "" (SKOLEM 1 ("S" "f"))
  (("" (TYPEPRED "S")
    (("" (EXPAND "is_finite")
      (("" (SKOLEM -1 ("M" "g"))
        (("" (TYPEPRED "M")
          (("" (INSTANTIATE 1 ("M" "_"))
            ((""
              (INST 1
               "LAMBDA (y:{y: T2 | EXISTS (x: (S)): y = f(x)}) : g(epsilon({x:(S) | y = f(x)}))")
              (("1" (EXPAND "injective?" 1)
                (("1" (GROUND)
                  (("1" (SKOLEM 1 ("x1" "x2"))
                    (("1" (EXPAND "injective?")
                      (("1"
                        (INSTANTIATE -2
                         ("epsilon({x: (S) | x1 = f(x)})"
                          "epsilon({x: (S) | x2 = f(x)})"))
                        (("1" (GROUND)
                          (("1" (HIDE -2 -3)
                            (("1"
                              (NAME "y1"
                                    "epsilon({x: (S) | x1 = f(x)})")
                              (("1"
                                (NAME
                                 "y2"
                                 "epsilon({x: (S) | x2 = f(x)})")
                                (("1"
                                  (REPLACE -1)
                                  (("1"
                                    (REPLACE -2)
                                    (("1"
                                      (CASE "x1 = f(y1)")
                                      (("1"
                                        (CASE "x2 = f(y2)")
                                        (("1" (ASSERT) NIL NIL)
                                         ("2"
                                          (HIDE -1 -3 -4 2)
                                          (("2"
                                            (LEMMA
                                             "epsilons[(S)].epsilon_ax")
                                            (("2"
                                              (INST?)
                                              (("2"
                                                (SPLIT)
                                                (("1" (ASSERT) NIL NIL)
                                                 ("2"
                                                  (TYPEPRED "x2")
                                                  (("2"
                                                    (SKOLEM
                                                     -1
                                                     "x_1444")
                                                    (("2"
                                                      (INST 1 "x_1444")
                                                      (("2"
                                                        (ASSERT)
                                                        NIL
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL)
                                       ("2"
                                        (HIDE -1 -3 2)
                                        (("2"
                                          (LEMMA
                                           "epsilons[(S)].epsilon_ax")
                                          (("2"
                                            (INST?)
                                            (("2"
                                              (SPLIT)
                                              (("1" (GRIND) NIL NIL)
                                               ("2"
                                                (TYPEPRED "x1")
                                                (("2"
                                                  (SKOLEM -1 "x_1444")
                                                  (("2"
                                                    (INST 1 "x_1444")
                                                    (("2"
                                                      (ASSERT)
                                                      NIL
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL)
                               ("2"
                                (TYPEPRED "x1")
                                (("2"
                                  (GROUND)
                                  (("2" (GRIND) NIL NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL)
                         ("2" (TYPEPRED "x1") (("2" (GRIND) NIL NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (SKOLEM 1 "y")
                (("2" (TYPEPRED "y") (("2" (GRIND) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|inverse_bijection| "" (SKOLEM 1 "f")
  (("" (EXPAND "bijective?")
    (("" (FLATTEN)
      (("" (SPLIT)
        (("1" (EXPAND "injective?")
          (("1" (HIDE -1)
            (("1" (SKOLEM 1 ("x1" "x2"))
              (("1" (FLATTEN)
                (("1" (LEMMA "epsilons[T1].epsilon_ax")
                  (("1" (INST?)
                    (("1" (SPLIT)
                      (("1" (LEMMA "epsilons[T1].epsilon_ax")
                        (("1" (INST -1 "{xx: T1 | x2 = f(xx)}")
                          (("1" (SPLIT)
                            (("1" (ASSERT) NIL NIL)
                             ("2" (TYPEPRED "x2")
                              (("2"
                                (SKOLEM -1 "w")
                                (("2"
                                  (INST 1 "w")
                                  (("2" (ASSERT) NIL NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (TYPEPRED "x1")
                        (("2" (SKOLEM -1 "w")
                          (("2" (INST 1 "w") (("2" (ASSERT) NIL NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (EXPAND "surjective?")
          (("2" (SKOLEM 1 "y")
            (("2" (INST 1 "f(y)")
              (("1" (LEMMA "epsilons[T1].epsilon_ax")
                (("1" (INST?)
                  (("1" (SPLIT)
                    (("1" (GROUND) (("1" (GRIND) NIL NIL)) NIL)
                     ("2" (HIDE -1 2)
                      (("2" (INST 1 "y") (("2" (ASSERT) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (INST 1 "y") NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))


$$$finite_sets/finite_sets_eq.pvs
finite_sets_eq[T1, T2 : TYPE] : THEORY
%-------------------------------------------------------------------------
%
%      by Bruno Dutertre    Royal Holloway & Bedford New College
% 
%      Equipotence of finite sets  
%
%-------------------------------------------------------------------------

BEGIN


  N: VAR nat

  IMPORTING finite_sets, func_composition

  E: VAR finite_set[T1]
  F: VAR finite_set[T2]

  S: VAR set[T1]
  U: VAR set[T2]

  injection_to_finite_set    : LEMMA
        (EXISTS (f: [(S)->(F)]): injective?(f)) IMPLIES is_finite(S)

  surjection_from_finite_set : LEMMA
        (EXISTS (f: [(E)->(U)]): surjective?(f)) IMPLIES is_finite(U)

  injection_to_finite_set2   : LEMMA
        (FORALL S, F, (f: [(S)->(F)]): injective?(f) IMPLIES is_finite(S))

  surjection_from_finite_set2: LEMMA
        (FORALL E, U, (f: [(E)->(U)]): surjective?(f) IMPLIES is_finite(U))

  bijection_finite_set1      : LEMMA
        (EXISTS (f: [(S)->(F)]): bijective?(f)) IMPLIES is_finite(S)

  bijection_finite_set2      : LEMMA
        (EXISTS (f: [(E)->(U)]): bijective?(f)) IMPLIES is_finite(U)

END finite_sets_eq

$$$finite_sets/finite_sets_eq.prf
(|finite_sets_eq|
 (|injection_to_finite_set| "" (SKOSIMP*)
  (("" (NAME "n" "card(F!1)")
    (("" (REWRITE "card_bij")
      (("" (EXPAND "bijective?")
        (("" (SKOSIMP)
          (("" (EXPAND "is_finite")
            (("" (INST 1 "n" "f!2 o f!1")
              (("" (REWRITE "composition_injective") NIL)))))))))))))))
 (|surjection_from_finite_set| "" (SKOSIMP*)
  (("" (CASE "empty?(E!1)")
    (("1" (CASE "U!1 = emptyset[T2]")
      (("1" (REPLACE -1) (("1" (REWRITE "finite_emptyset") NIL)))
       ("2" (REWRITE "emptyset_is_empty?" :DIR RL)
        (("2" (DELETE 2) (("2" (GRIND) NIL)))))))
     ("2" (ASSERT)
      (("2" (NAME "g" "inverse(f!1)")
        (("1" (TYPEPRED "E!1")
          (("1" (EXPAND "is_finite")
            (("1" (SKOLEM!)
              (("1" (INST 2 "N!1" "f!2 o g")
                (("1" (REWRITE "composition_injective")
                  (("1" (REPLACE -2 1 RL)
                    (("1" (REWRITE "inj_inv") NIL)))))))))))))
         ("2" (DELETE -1 3) (("2" (GRIND) (("2" (INST + "x!1") NIL)))))))))))))
 (|injection_to_finite_set2| "" (SKOSIMP)
  (("" (USE "injection_to_finite_set" ("F" "F!1"))
    (("" (ASSERT) (("" (INST?) NIL)))))))
 (|surjection_from_finite_set2| "" (SKOSIMP)
  (("" (USE "surjection_from_finite_set" ("E" "E!1"))
    (("" (ASSERT) (("" (INST?) NIL)))))))
 (|bijection_finite_set1| "" (EXPAND "bijective?")
  (("" (SKOSIMP*)
    (("" (LEMMA "injection_to_finite_set" ("S" "S!1" "F" "F!1"))
      (("" (ASSERT) (("" (INST?) NIL)))))))))
 (|bijection_finite_set2| "" (EXPAND "bijective?")
  (("" (SKOSIMP*)
    (("" (LEMMA "surjection_from_finite_set" ("E" "E!1" "U" "U!1"))
      (("" (ASSERT) (("" (INST?) NIL))))))))))

$$$finite_sets/func_composition.pvs
func_composition  [ T1, T2, T3 : TYPE ] : THEORY
%------------------------------------------------------------------------
%      Author:  Bruno Dutertre 
%
%      Composition of injective, surjective, bijective functions
%------------------------------------------------------------------------

  BEGIN

  f1 : VAR [T1 -> T2]
  f2 : VAR [T2 -> T3]

  composition_injective : LEMMA injective?(f1) AND injective?(f2) 
                                   IMPLIES injective?(f2 o f1)

  composition_surjective: LEMMA surjective?(f1) AND surjective?(f2) 
                                   IMPLIES surjective?(f2 o f1)

  composition_bijective : LEMMA bijective?(f1) AND bijective?(f2) 
                                   IMPLIES bijective?(f2 o f1)

  %  ---------------- Cancellation laws ----------------

  f, g : VAR [T1 -> T2]
  h, k : VAR [T2 -> T3]

  composition_def          : LEMMA (FORALL (x : T1) : h(f(x)) = (h o f)(x))
  
  composition_left_cancel1 : LEMMA injective?(h)  
                                      IMPLIES  (h o f = h o g IFF f = g)
  
  composition_left_cancel2 : LEMMA bijective?(h)  
                                      IMPLIES  (h o f = h o g IFF f = g)

 
  composition_right_cancel1: LEMMA surjective?(f)  
                                      IMPLIES  (h o f = k o f IFF h = k)
  
  composition_right_cancel2: LEMMA bijective?(f) 
                                      IMPLIES  (h o f = k o f IFF h = k)

END func_composition


$$$finite_sets/func_composition.prf
(|func_composition|
 (|composition_injective| "" (GRIND :IF-MATCH NIL)
  (("" (INST -2 "f1!1(x1!1)" "f1!1(x2!1)") (("" (INST -1 "x1!1" "x2!1") (("" (GROUND) NIL)))))))
 (|composition_surjective| "" (GRIND) NIL)
 (|composition_bijective| "" (EXPAND "bijective?")
  (("" (SKOSIMP)
    (("" (SPLIT)
      (("1" (REWRITE "composition_injective") NIL)
       ("2" (REWRITE "composition_surjective") NIL)))))))
 (|composition_def| "" (EXPAND "o") (("" (PROPAX) NIL)))
 (|composition_left_cancel1| "" (SKOSIMP)
  (("" (PROP)
    (("1" (APPLY-EXTENSIONALITY :HIDE? T)
      (("1" (EXPAND "injective?")
        (("1" (INST? -2)
          (("1" (ASSERT)
            (("1" (REWRITE "composition_def")
              (("1" (REWRITE "composition_def") (("1" (ASSERT) NIL)))))))))))))
     ("2" (ASSERT) NIL)))))
 (|composition_left_cancel2| "" (EXPAND "bijective?")
  (("" (SKOSIMP) (("" (REWRITE "composition_left_cancel1") NIL)))))
 (|composition_right_cancel1| "" (SKOSIMP)
  (("" (PROP)
    (("1" (APPLY-EXTENSIONALITY :HIDE? T)
      (("1" (EXPAND "surjective?")
        (("1" (INST?)
          (("1" (SKOLEM!)
            (("1" (REPLACE -2 + RL)
              (("1" (REWRITE "composition_def")
                (("1" (REWRITE "composition_def") (("1" (ASSERT) NIL)))))))))))))))
     ("2" (ASSERT) NIL)))))
 (|composition_right_cancel2| "" (EXPAND "bijective?")
  (("" (SKOSIMP) (("" (REWRITE "composition_right_cancel1") NIL))))))

$$$finite_sets/finite_sets_card_eq.pvs
finite_sets_card_eq[T1, T2 : TYPE] : THEORY
%-------------------------------------------------------------------------
%
%      by Bruno Dutertre    Royal Holloway & Bedford New College
% 
% Establishes:
%
%       card_eq_bij : LEMMA card(E) = card(F) IFF 
%                                  EXISTS (f: [(E)->(F)]): bijective?(f)
%
%-------------------------------------------------------------------------

BEGIN

  IMPORTING finite_sets, func_composition

  E: VAR finite_set[T1]
  F: VAR finite_set[T2]

  N: VAR nat
  card_injection         : LEMMA (EXISTS (f : [(E)->below[N]]) : injective?(f)) 
                                     IMPLIES card(E) <= N
  
  card_surjection        : LEMMA (EXISTS (f : [(E)->below[N]]) : surjective?(f)) 
                                     IMPLIES N <= card(E) 
  

  injection_and_cardinal : LEMMA (EXISTS (f : [(E)->(F)]): injective?(f))
                                            IMPLIES card(E) <= card(F)

  surjection_and_cardinal: LEMMA (EXISTS (f: [(E)->(F)]): surjective?(f))
                                            IMPLIES card(F) <= card(E)

  card_eq_bij            : LEMMA card(E) = card(F) IFF 
                                          EXISTS (f: [(E)->(F)]): bijective?(f)

END finite_sets_card_eq

$$$finite_sets/finite_sets_card_eq.prf
(|finite_sets_card_eq|
 (|card_injection| "" (SKOSIMP*)
  (("" (REWRITE "card_def") (("" (REWRITE "Card_injection") (("" (INST?) NIL)))))))
 (|card_surjection| "" (SKOSIMP*)
  (("" (REWRITE "card_def") (("" (REWRITE "Card_surjection") (("" (INST?) NIL)))))))
 (|injection_and_cardinal| "" (SKOSIMP*)
  (("" (NAME-REPLACE "n" "card(F!1)" :HIDE? NIL)
    (("" (REWRITE "card_bij")
      (("" (EXPAND "bijective?")
        (("" (SKOSIMP)
          (("" (REWRITE "card_injection")
            (("" (INST 1 "f!2 o f!1")
              (("" (REWRITE "composition_injective") NIL)))))))))))))))
 (|surjection_and_cardinal| "" (SKOSIMP*)
  (("" (NAME-REPLACE "n" "card(F!1)" :HIDE? NIL)
    (("" (REWRITE "card_bij")
      (("" (EXPAND "bijective?")
        (("" (SKOSIMP)
          (("" (REWRITE "card_surjection")
            (("" (INST 1 "f!2 o f!1")
              (("" (REWRITE "composition_surjective") NIL)))))))))))))))
 (|card_eq_bij| "" (SKOSIMP*)
  (("" (USE "empty_card[T2]")
    (("" (GROUND)
      (("1" (REPLACE -3)
        (("1" (REWRITE "empty_card[T1]" :DIR RL)
          (("1" (DELETE -3)
            (("1" (INST 1 "LAMBDA (x : (E!1)) : epsilon! (y : (F!1)) : true")
              (("1" (GRIND :IF-MATCH NIL) (("1" (INST?) NIL) ("2" (INST?) NIL)))
               ("2" (DELETE -2) (("2" (GRIND) NIL)))))))))))
       ("2" (REPLACE -3)
        (("2" (REWRITE "empty_card[T1]" :DIR RL)
          (("2" (SKOLEM!)
            (("2" (DELETE -1 -3)
              (("2" (GRIND :IF-MATCH NIL)
                (("2" (INST - "f!1(x!1)") (("2" (ASSERT) NIL)))))))))))))
       ("3" (DELETE 2)
        (("3" (NAME-REPLACE "n" "card(F!1)" :HIDE? NIL)
          (("3" (REWRITE "card_bij")
            (("3" (REWRITE "card_bij")
              (("3" (SKOSIMP*)
                (("3" (INST 1 "inverse(f!1) o f!2")
                  (("1" (REWRITE "composition_bijective")
                    (("1" (REWRITE "bij_inv_is_bij")
                      (("1" (DELETE -1 -2 2 3) (("1" (GRIND) NIL)))))
                     ("2" (DELETE -)
                      (("2" (EXPAND "empty?")
                        (("2" (SKOSIMP*)
                          (("2" (EXPAND "member") (("2" (INST + "x!1") NIL)))))))))))
                   ("2" (EXPAND "empty?")
                    (("2" (EXPAND "member")
                      (("2" (SKOSIMP*) (("2" (INST + "x!1") NIL)))))))))))))))))))
       ("4" (NAME-REPLACE "n" "card(F!1)" :HIDE? NIL)
        (("4" (DELETE 2)
          (("4" (REWRITE "card_bij")
            (("4" (REWRITE "card_bij")
              (("4" (SKOSIMP*)
                (("4" (INST 1 "f!1 o f!2")
                  (("4" (REWRITE "composition_bijective") NIL))))))))))))))))))))

$$$finite_sets/finite_sets_below.pvs
finite_sets_below[N: nat]: THEORY
BEGIN

  IMPORTING finite_sets

  A,B,BS: VAR set[below(N)]
  US: VAR set[upto(N)]

  finite_below      : LEMMA is_finite[below(N)](BS)

  card_below_fullset: LEMMA card[below(N)](fullset[below(N)]) = N

  card_below        : LEMMA card[below(N)](BS) <= N

  finite_upto       : LEMMA is_finite[upto(N)](US)

  card_upto_fullset : LEMMA card[upto(N)](fullset[upto(N)]) = N + 1

  card_upto         : LEMMA card[upto(N)](US) <= N + 1

  k: VAR nat
  pidgeon_hole      : LEMMA card(A) + card(B) >= N + k IMPLIES 
                                card(intersection(A,B)) >= k


END finite_sets_below

$$$finite_sets/finite_sets_below.prf
(|finite_sets_below|
 (|finite_below| "" (SKOSIMP*)
  (("" (EXPAND "is_finite")
    (("" (INST 1 "N" "(LAMBDA (i:(BS!1)): i)")
      (("" (EXPAND "injective?") (("" (SKOSIMP*) NIL)))))))))
 (|card_below_fullset_TCC1| "" (REWRITE "finite_below") NIL)
 (|card_below_fullset| "" (EXPAND "fullset")
  (("" (LEMMA "card_bij[below(N)]")
    (("" (INST -1 "N" "{x: below(N) | TRUE}")
      (("1" (REPLACE -1)
        (("1" (HIDE -1)
          (("1" (INST 1 "(LAMBDA (x: {x: below(N) | TRUE}): x)")
            (("1" (EXPAND "bijective?")
              (("1" (PROP)
                (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL)))
                 ("2" (EXPAND "surjective?")
                  (("2" (SKOSIMP*) (("2" (INST 1 "y!1") NIL)))))))))))))))
       ("2" (REWRITE "finite_below") NIL)))))))
 (|card_below_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_below") NIL)))
 (|card_below| "" (SKOSIMP*)
  (("" (LEMMA "card_subset[below(N)]")
    (("" (INST -1 "BS!1" "fullset[below(N)]")
      (("1" (LEMMA "card_below_fullset")
        (("1" (REPLACE -1)
          (("1" (HIDE -1)
            (("1" (ASSERT)
              (("1" (HIDE 2)
                (("1" (EXPAND "subset?")
                  (("1" (EXPAND "fullset")
                    (("1" (EXPAND "member") (("1" (PROPAX) NIL)))))))))))))))))
       ("2" (REWRITE "finite_below") NIL)
       ("3" (REWRITE "finite_below") NIL)))))))
 (|finite_upto| "" (SKOSIMP*)
  (("" (EXPAND "is_finite")
    (("" (INST 1 "N+1" "(LAMBDA (i:(US!1)): i)")
      (("" (EXPAND "injective?") (("" (SKOSIMP*) NIL)))))))))
 (|card_upto_fullset_TCC1| "" (REWRITE "finite_upto") NIL)
 (|card_upto_fullset| "" (EXPAND "fullset")
  (("" (LEMMA "card_bij[upto(N)]")
    (("" (INST -1 "N+1" "{x: upto(N) | TRUE}")
      (("1" (REPLACE -1)
        (("1" (HIDE -1)
          (("1" (INST 1 "(LAMBDA (x: {x: upto(N) | TRUE}): x)")
            (("1" (EXPAND "bijective?")
              (("1" (PROP)
                (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL)))
                 ("2" (EXPAND "surjective?")
                  (("2" (SKOSIMP*) (("2" (INST 1 "y!1") NIL)))))))))))))))
       ("2" (REWRITE "finite_upto") NIL)))))))
 (|card_upto_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_upto") NIL)))
 (|card_upto| "" (SKOSIMP*)
  (("" (LEMMA "card_subset[upto(N)]")
    (("" (INST -1 "US!1" "fullset[upto(N)]")
      (("1" (LEMMA "card_upto_fullset")
        (("1" (REPLACE -1)
          (("1" (HIDE -1)
            (("1" (ASSERT)
              (("1" (HIDE 2)
                (("1" (EXPAND "subset?")
                  (("1" (EXPAND "fullset")
                    (("1" (EXPAND "member") (("1" (PROPAX) NIL)))))))))))))))))
       ("2" (REWRITE "finite_upto") NIL) ("3" (REWRITE "finite_upto") NIL)))))))
 (|pidgeon_hole_TCC1| "" (SKOSIMP*)
  (("" (REWRITE "finite_intersection")
    (("1" (REWRITE "finite_below") NIL) ("2" (REWRITE "finite_below") NIL)))))
 (|pidgeon_hole| "" (SKOSIMP*)
  (("" (LEMMA "card_union[below(N)]")
    (("" (INST?)
      (("1" (LEMMA "card_below") (("1" (INST?) (("1" (ASSERT) NIL)))))
       ("2" (REWRITE "finite_below") NIL)
       ("3" (REWRITE "finite_below") NIL))))))))
$$$finite_sets/finite_sets_pred.pvs
finite_sets_pred[T: TYPE]: THEORY
BEGIN

  IMPORTING finite_sets

  P, P1, P2: VAR pred[T]

  finite_pred: LEMMA is_finite(fullset[T]) IMPLIES
                        is_finite[T]({x: T | P(x)})


  card_implies: LEMMA is_finite(fullset[T]) AND
                      (FORALL (x: T): P1(x) IMPLIES P2(x)) 
             IMPLIES card({x: T | P1(x)}) <= card({x: T | P2(x)})

END finite_sets_pred

$$$finite_sets/finite_sets_pred.prf
(|finite_sets_pred|
 (|finite_pred| "" (EXPAND "fullset")
  (("" (EXPAND "is_finite")
    (("" (SKOSIMP*)
      (("" (INST 1 "N!1" "(LAMBDA (x: {x: T | P!1(x)}): f!1(x))")
        (("" (EXPAND "injective?")
          (("" (SKOSIMP*)
            (("" (INST?) (("" (ASSERT) NIL)))))))))))))))
 (|card_implies_TCC1| "" (SKOSIMP*)
  (("" (REWRITE "finite_pred") NIL)))
 (|card_implies_TCC2| "" (SKOSIMP*)
  (("" (REWRITE "finite_pred") NIL)))
 (|card_implies| "" (SKOSIMP*)
  (("" (CASE "subset?({x: T | P1!1(x)},{x: T | P2!1(x)})")
    (("1" (LEMMA "card_subset[T]")
      (("1" (INST?)
        (("1" (ASSERT) NIL)
         ("2" (HIDE -1 -3 2) (("2" (REWRITE "finite_pred") NIL)))
         ("3" (REWRITE "finite_pred") NIL)))))
     ("2" (HIDE -1 2)
      (("2" (EXPAND "subset?")
        (("2" (EXPAND "member") (("2" (PROPAX) NIL))))))))))))
$$$finite_sets/finite_sets_nat.pvs
finite_sets_nat: THEORY
 BEGIN
  IMPORTING finite_sets[nat]

  n, N: VAR nat
  i, j: VAR nat
  p: VAR pred[nat]

  finite_bounded       : LEMMA is_finite({j: nat | j < N })

  card_bounded         : LEMMA card({j: nat | j < N}) = N    

  finite_bounded_subset: LEMMA is_finite({j: nat | j < N AND p(j)})

  card_bounded_subset  : LEMMA card({j: nat | j < N AND p(j)}) <= N

% ------------------------------------------------------------------------
% The following lemmas apply is_finite[nat] and card[nat] to subtype
% sets.  This should be avoided if possible.  See finite_subint for
% preferred lemmas.
% ------------------------------------------------------------------------

  finite_nat_below   : LEMMA is_finite[nat]({x: below(n) | TRUE})

  card_nat_below     : LEMMA card[nat]({x: below(n) | TRUE}) = n

  finite_nat_upto    : LEMMA is_finite[nat]({x: upto(n) | TRUE})

  card_nat_upto      : LEMMA card[nat]({x: upto(n) | TRUE}) = n + 1

  finite_nat_subrange: LEMMA
      is_finite[nat](restrict[int, nat, bool]({x: subrange(i, j) | TRUE}))

  card_nat_subrange  : LEMMA
      card[nat](restrict[int, nat, bool]({x: subrange(i, j) | TRUE})) =
                               IF i <= j THEN j - i + 1 ELSE 0 ENDIF


END finite_sets_nat

$$$finite_sets/finite_sets_nat.prf
(|finite_sets_nat|
 (|finite_bounded| "" (SKOSIMP*)
  (("" (EXPAND "is_finite")
    (("" (INST 1 "N!1" "(lambda (x: below(N!1)): x)")
      (("" (EXPAND "injective?") (("" (SKOSIMP*) NIL)))))))))
 (|card_bounded_TCC1| "" (SKOSIMP*)
  (("" (ASSERT)
    (("" (EXPAND "is_finite")
      (("" (INST 1 "N!1" "(lambda (x: below(N!1)): x)")
        (("" (EXPAND "injective?") (("" (SKOSIMP*) NIL)))))))))))
 (|card_bounded| "" (SKOSIMP*)
  (("" (REWRITE "card_bij")
    (("1" (INST 1 "(lambda (x:below(N!1)):x)")
      (("1" (EXPAND "bijective?")
        (("1" (SPLIT 1)
          (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL)))
           ("2" (EXPAND "surjective?")
            (("2" (SKOSIMP*) (("2" (INST 1 "y!1") NIL)))))))))))
     ("2" (REWRITE "finite_bounded") NIL)))))
 (|finite_bounded_subset| "" (SKOSIMP*)
  (("" (LEMMA "finite_subset")
    (("" (INST -1 "{j: nat | j < N!1}" "{j: nat | j < N!1 AND p!1(j)}")
      (("1" (ASSERT)
        (("1" (HIDE 2)
          (("1" (EXPAND "subset?")
            (("1" (EXPAND "member") (("1" (SKOSIMP*) NIL)))))))))
       ("2" (REWRITE "finite_bounded") NIL)))))))
 (|card_bounded_subset_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "finite_bounded_subset") (("" (INST?) NIL)))))
 (|card_bounded_subset| "" (SKOSIMP*)
  (("" (LEMMA "card_bounded")
    (("" (INST -1 "N!1")
      (("" (LEMMA "card_subset")
        ((""
          (INST -1 "{j: nat | j < N!1 AND p!1(j)}"
           "{j: nat | j < N!1}")
          (("1" (SPLIT -1)
            (("1" (ASSERT) NIL)
             ("2" (HIDE -1 2)
              (("2" (EXPAND "subset?")
                (("2" (SKOSIMP*)
                  (("2" (EXPAND "member") (("2" (ASSERT) NIL)))))))))))
           ("2" (REWRITE "finite_bounded") NIL)
           ("3" (REWRITE "finite_bounded_subset") NIL)))))))))))
 (|finite_nat_below| "" (SKOSIMP*)
  (("" (EXPAND "is_finite")
    ((""
      (INST 1 "n!1"
       "(LAMBDA (x: (extend[nat, below(n!1), bool, FALSE]({x: below(n!1) | TRUE}))): x)")
      (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL)))
       ("2" (SKOSIMP*)
        (("2" (ASSERT)
          (("2" (TYPEPRED "x!1")
            (("2" (EXPAND "extend") (("2" (PROPAX) NIL)))))))))))))))
 (|card_nat_below_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "finite_nat_below") (("" (INST?) NIL)))))
 (|card_nat_below| "" (SKOSIMP*)
  (("" (LEMMA "card_bij")
    ((""
      (INST -1 "n!1"
       "extend[nat, below(n!1), bool, FALSE]({x: below(n!1) | TRUE})")
      (("1" (REPLACE -1)
        (("1" (HIDE -1)
          (("1"
            (INST 1
             "(LAMBDA (x: (extend[nat, below(n!1), bool, FALSE]({x: below(n!1) | TRUE}))): x)")
            (("1" (EXPAND "bijective?")
              (("1" (PROP)
                (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL)))
                 ("2" (EXPAND "surjective?")
                  (("2" (SKOSIMP*)
                    (("2" (INST 1 "y!1")
                      (("2" (EXPAND "extend")
                        (("2" (PROPAX) NIL)))))))))))))
             ("2" (SKOSIMP*)
              (("2" (TYPEPRED "x!1")
                (("2" (EXPAND "extend") (("2" (ASSERT) NIL)))))))))))))
       ("2" (LEMMA "finite_nat_below") (("2" (INST?) NIL)))))))))
 (|finite_nat_upto| "" (SKOSIMP*)
  (("" (EXPAND "is_finite")
    ((""
      (INST 1 "n!1+1"
       "(LAMBDA (x: (extend[nat, upto(n!1), bool, FALSE]({x: upto(n!1) | TRUE}))): x)")
      (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL)))
       ("2" (SKOSIMP*)
        (("2" (TYPEPRED "x!1")
          (("2" (EXPAND "extend") (("2" (ASSERT) NIL)))))))))))))
 (|card_nat_upto_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "finite_nat_upto") (("" (INST?) NIL)))))
 (|card_nat_upto| "" (SKOSIMP*)
  (("" (LEMMA "card_bij")
    ((""
      (INST -1 "n!1+1"
       "extend[nat, upto(n!1), bool, FALSE]({x: upto(n!1) | TRUE})")
      (("1" (REPLACE -1)
        (("1" (HIDE -1)
          (("1" (INST 1 "(LAMBDA (x: {x: upto(n!1) | TRUE}): x)")
            (("1" (EXPAND "bijective?")
              (("1" (PROP)
                (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL)))
                 ("2" (EXPAND "surjective?")
                  (("2" (SKOSIMP*)
                    (("2" (INST 1 "y!1")
                      (("2" (EXPAND "extend")
                        (("2" (PROPAX) NIL)))))))))))))
             ("2" (SKOSIMP*)
              (("2" (PROP)
                (("1" (EXPAND "extend") (("1" (ASSERT) NIL)))
                 ("2" (EXPAND "extend") (("2" (ASSERT) NIL)))))))
             ("3" (SKOSIMP*)
              (("3" (EXPAND "extend") (("3" (PROPAX) NIL)))))))))))
       ("2" (LEMMA "finite_nat_upto") (("2" (INST?) NIL)))))))))
 (|finite_nat_subrange| "" (SKOSIMP*)
  (("" (EXPAND "is_finite")
    ((""
      (INST 1 "j!1+1" "(LAMBDA (x: (restrict[int, nat,
                   bool](extend[int, subrange(i!1, j!1), bool,
                                FALSE]({x: subrange(i!1, j!1) | TRUE})))): x)")
      (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL)))
       ("2" (SKOSIMP*)
        (("2" (ASSERT)
          (("2" (TYPEPRED "x!1")
            (("2" (EXPAND "restrict")
              (("2" (EXPAND "extend")
                (("2" (PROPAX) NIL)))))))))))))))))
 (|card_nat_subrange_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "finite_nat_subrange") (("" (INST?) NIL)))))
 (|card_nat_subrange| "" (SKOSIMP*)
  (("" (LEMMA "card_bij")
    (("" (INST?)
      (("1" (REPLACE -1)
        (("1" (HIDE -1)
          (("1"
            (INST 1 "(LAMBDA (x: (restrict[int, nat,
                          bool](extend[int, subrange(i!1, j!1), bool,
                                       FALSE]({x: subrange(i!1, j!1) | TRUE})))): 
                        IF i!1 <= j!1 THEN x-i!1 ELSE 0 ENDIF)")
            (("1" (EXPAND "bijective?")
              (("1" (PROP)
                (("1" (EXPAND "injective?")
                  (("1" (SKOSIMP*)
                    (("1" (TYPEPRED "x1!1")
                      (("1" (TYPEPRED "x2!1")
                        (("1" (GRIND) NIL)))))))))
                 ("2" (EXPAND "surjective?")
                  (("2" (SKOSIMP*)
                    (("2" (INST 1 "y!1+i!1")
                      (("1" (TYPEPRED "y!1") (("1" (GRIND) NIL)))
                       ("2" (TYPEPRED "y!1")
                        (("2" (GRIND) NIL)))))))))))))
             ("2" (SKOSIMP*)
              (("2" (TYPEPRED "x!1") (("2" (GRIND) NIL)))))
             ("3" (SKOSIMP*)
              (("3" (TYPEPRED "x!1") (("3" (GRIND) NIL)))))))))))
       ("2" (HIDE 2) (("2" (REWRITE "finite_nat_subrange") NIL)))
       ("3" (HIDE 2) (("3" (FLATTEN) (("3" (ASSERT) NIL))))))))))))

$$$finite_sets/finite_sets_int.pvs
finite_sets_int: THEORY
 BEGIN
  IMPORTING finite_sets[int]

  i, j, x: VAR int

  p: VAR pred[int]

  in_subrng(x,i,j): bool = (i <= x) AND (x <= j)

  finite_subrng       : LEMMA is_finite({x | in_subrng(x,i,j)})

  finite_subrng_subset: LEMMA is_finite({x | in_subrng(x,i,j) AND p(x)})

  card_subrng         : LEMMA card({x | in_subrng(x,i,j)}) =
                                  IF i <= j THEN abs(j-i+1) ELSE 0 ENDIF


% ------------------------------------------------------------------------
% The following lemmas apply is_finite[nat] and card[nat] to subtype
% sets.  This should be avoided if possible.  See finite_subint for
% preferred lemmas.
% ------------------------------------------------------------------------

  finite_int_subrange     : LEMMA is_finite[int]({x: subrange(i, j) | TRUE})

  finite_int_subrange_pred: LEMMA is_finite[int]({x: subrange(i, j) | p(x)})

  card_int_subrange       : LEMMA card[int]({x: subrange(i, j) | TRUE}) =
                                    IF i <= j THEN abs(j-i+1) ELSE 0 ENDIF

END finite_sets_int

$$$finite_sets/finite_sets_int.prf
(|finite_sets_int| (|finite_subrng| "" (SKOSIMP*) (("" (EXPAND "in_subrng") (("" (EXPAND "is_finite") (("" (INST 1 "abs(j!1-i!1+1)" "(LAMBDA (x: {x: int | i!1 <= x AND x <= j!1}): x - i!1)") (("1" (GRIND) NIL NIL) ("2" (SKOSIMP*) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|finite_subrng_subset| "" (SKOSIMP*) (("" (CASE "subset?({x: int | in_subrng(x, i!1, j!1) AND p!1(x)},{x: int | in_subrng(x, i!1, j!1)})") (("1" (LEMMA "finite_subset") (("1" (INST?) (("1" (ASSERT) NIL NIL) ("2" (HIDE -1 2) (("2" (REWRITE "finite_subrng") NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND "subset?") (("2" (EXPAND "member") (("2" (SKOSIMP*) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_subrng_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_subrng") NIL NIL)) NIL) (|card_subrng| "" (SKOSIMP*) (("" (CASE "i!1 > j!1") (("1" (ASSERT) (("1" (CASE "{x: int | in_subrng(x, i!1, j!1)} = emptyset") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "card_emptyset") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (LEMMA "card_bij") (("2" (INST -1 "abs(j!1-i!1+1)" "{x | in_subrng(x, i!1, j!1)}") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (INST 2 "(LAMBDA (x: {x | in_subrng(x, i!1, j!1)}): abs(x -i!1))") (("1" (EXPAND "bijective?") (("1" (PROP) (("1" (EXPAND "injective?") (("1" (SKOSIMP*) (("1" (TYPEPRED "x1!1") (("1" (TYPEPRED "x2!1") (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "surjective?") (("2" (SKOSIMP*) (("2" (TYPEPRED "y!1") (("2" (INST 1 "y!1+i!1") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "x!1") (("2" (EXPAND "in_subrng") (("2" (FLATTEN) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2 3) (("2" (REWRITE "finite_subrng") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|finite_int_subrange| "" (SKOSIMP*) (("" (EXPAND "is_finite") (("" (INST 1 "abs(j!1-i!1+1)" "(LAMBDA (x: (extend[int, subrange(i!1, j!1), bool,
                 FALSE]({x: subrange(i!1, j!1) | TRUE}))): x - i!1)") (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "abs") (("2" (GROUND) (("1" (TYPEPRED "x!1") (("1" (EXPAND "extend") (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (LIFT-IF) (("2" (GROUND) (("1" (TYPEPRED "x!1") (("1" (EXPAND "extend") (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (TYPEPRED "x!1") (("2" (EXPAND "extend") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|finite_int_subrange_pred| "" (SKOSIMP*) (("" (CASE "is_finite({x: subrange(i!1, j!1) | TRUE})") (("1" (LEMMA "finite_subset") (("1" (INST -1 "{x: subrange(i!1, j!1) | TRUE}" "{x: subrange(i!1, j!1) | p!1(x)}") (("1" (ASSERT) (("1" (HIDE -1 2) (("1" (EXPAND "subset?") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (EXPAND "extend") (("1" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND "is_finite") (("2" (SKOSIMP) (("2" (INST 1 "N!1" "LAMBDA (x: (extend[int, subrange(i!1, j!1), bool, FALSE]
                      ({x: subrange(i!1, j!1) | TRUE}))): IF i!1 <= x and x <= j!1 then f!1(x) ELSE 0 ENDIF") (("1" (GRIND :IF-MATCH NIL) (("1" (INST -6 "x1!1" "x2!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (TYPEPRED "x!1") (("2" (EXPAND "extend") (("2" (ASSERT) (("2" (REPLACE 1) (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (LEMMA "finite_int_subrange") (("2" (INST?) (("2" (EXPAND "is_finite") (("2" (SKOSIMP*) (("2" (INST 1 "N!1" "lambda (x: ({x: subrange(i!1, j!1) | TRUE})): f!1(x)") (("1" (GRIND :IF-MATCH NIL) (("1" (INST -5 "x1!1" "x2!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_int_subrange_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_int_subrange") NIL NIL)) NIL) (|card_int_subrange| "" (SKOSIMP*) (("" (CASE "i!1 > j!1") (("1" (ASSERT) (("1" (CASE "extend[int, subrange(i!1, j!1),
                       bool, FALSE]({x: subrange(i!1, j!1)
                                    | TRUE}) = emptyset") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "card_emptyset") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND "extend") (("2" (APPLY-EXTENSIONALITY) (("2" (LIFT-IF) (("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (LEMMA "card_bij") (("2" (INST -1 "abs(j!1-i!1+1)" "extend[int, subrange(i!1, j!1),
                       bool, FALSE]({x: subrange(i!1, j!1)
                                    | TRUE})") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (INST 2 "(LAMBDA (x: (extend[int, subrange(i!1, j!1), bool,
                        FALSE]({x: subrange(i!1, j!1) | TRUE}))): abs(x -i!1))") (("1" (EXPAND "bijective?") (("1" (PROP) (("1" (EXPAND "injective?") (("1" (SKOSIMP*) (("1" (TYPEPRED "x1!1") (("1" (TYPEPRED "x2!1") (("1" (EXPAND "extend") (("1" (EXPAND "abs") (("1" (PROP) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "surjective?") (("2" (SKOSIMP*) (("2" (INST 1 "y!1+i!1") (("1" (EXPAND "abs") (("1" (PROPAX) NIL NIL)) NIL) ("2" (EXPAND "extend") (("2" (ASSERT) (("2" (PROP) (("2" (TYPEPRED "y!1") (("2" (EXPAND "abs") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "abs") (("2" (TYPEPRED "x!1") (("2" (EXPAND "extend") (("2" (PROP) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "finite_int_subrange") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL))

$$$finite_sets/prelude_aux.pvs
prelude_aux[T: TYPE]: THEORY

BEGIN

  % these lemmas should go in prelude

  rest_emptyset: LEMMA (FORALL (S: set[T], t:T): rest(S) = emptyset[T]
                           AND S(t) IMPLIES choose(S) = t)


END prelude_aux

$$$finite_sets/prelude_aux.prf
(|prelude_aux| (|rest_emptyset_TCC1| "" (SUBTYPE-TCC) NIL)
 (|rest_emptyset| "" (SKOSIMP*)
  (("" (LEMMA "rest_empty_lem[T]")
    (("" (INST?)
      (("" (ASSERT)
        (("" (SPLIT -1)
          (("1" (EXPAND "singleton")
            (("1" (EXPAND "extend")
              (("1" (REPLACE -1)
                (("1" (HIDE -1) (("1" (HIDE -1) (("1" (ASSERT) NIL)))))))))))
           ("2" (ASSERT)
            (("2" (EXPAND "empty?")
              (("2" (EXPAND "member") (("2" (INST?) NIL)))))))
           ("3" (REWRITE "emptyset_is_empty?[T]") NIL))))))))))))
$$$finite_sets/finite_sets_sum_real.pvs
finite_sets_sum_real[T: TYPE]: THEORY
%------------------------------------------------------------------------
%
% finite sum over real-valued functions   
%
%   Authors: Ricky W. Butler
%            David Griffioen
%
%   NOTES:
%      -- there are several theorems which are virtually idential to
%         theorems in finite_sets_sum.  They are repeated here to prevent
%         the need for commands such as (LEMMA sum_emptyset[T,real,0,+])
%      -- the theorems with names ending in "_rew" are especially useful
%         for rewriting.  Some of these take advantage of the fact that
%         since we have real-valued functions we have a "-" available.
%------------------------------------------------------------------------
BEGIN


  IMPORTING finite_sets_sum[T,real,0,+], prelude_aux

  S, A, B: VAR finite_set[T]
  t: VAR T
  c,N: VAR real
  f,g: VAR function[T -> real]

  sum_const        : THEOREM sum(S, (LAMBDA t: c)) = c*card(S) 

  sum_1_is_card    : COROLLARY sum(S,(LAMBDA t: 1)) = card(S)

  sum_mult         : THEOREM sum(S,(LAMBDA t: c*f(t))) = c*sum(S,f) 

% ----------- Some rewrite rules using "-" ------------------

  sum_empty?       : THEOREM empty?(S) IMPLIES sum(S,f) = 0

  sum_emptyset_rew : THEOREM S = emptyset[T] IMPLIES sum(S,f) = 0

  sum_singleton_rew: THEOREM card(S) = 1 AND S(t) IMPLIES sum(S,f) = f(t)

  sum_remove_rew   : THEOREM sum(remove(t,S),f) = sum(S,f) -
                                IF member(t,S) THEN f(t) ELSE 0 ENDIF 


  sum_rest_rew     : THEOREM NOT empty?(S) IMPLIES
                                sum(rest(S),f) = sum(S,f) - f(choose(S))

  sum_union_rew    : THEOREM sum(union(A,B),f) = sum(A,f) + sum(B,f)
                                 - sum(intersection(A,B),f) 


% -------- sums of slightly modified functions ----------

  sum_eq_funs       : THEOREM (FORALL (t: (S)): f(t) = g(t)) 
                               IMPLIES sum(S, f) = sum(S, g)

  sum_particular_gen: THEOREM sum(S,f) = sum(S, f WITH [t := c])
			       + IF S(t) THEN f(t) - c ELSE 0 ENDIF 


% ----- some order relationships involving sum -----

  sum_bound    : THEOREM (FORALL (t: (S)): f(t) <= N) 
                             IMPLIES sum(S,f) <= N*card(S)

  sum_order    : THEOREM (FORALL (t:T): f(t) <= g(t)) IMPLIES
                           sum(S,f) <= sum(S,g)

  sum_nonneg   : LEMMA (FORALL (t: (S)): f(t) >= 0) IMPLIES sum(S,f) >= 0

  sum_pos      : LEMMA (FORALL (t: (S)): f(t) > 0) IMPLIES sum(S,f) > 0 OR
                                                    S = emptyset[T]

  JUDGEMENT sum(A: non_empty_finite_set[T], f: [T -> posreal])
            HAS_TYPE posreal

  JUDGEMENT sum(A: finite_set[T], f: [T -> int]) HAS_TYPE int

  JUDGEMENT sum(A: finite_set[T], f: [T -> nat]) HAS_TYPE nat

% ----- Special properties non-negative valued functions -----

  fnr,gnr: VAR [T -> nonneg_real]

  sum_subset   : THEOREM subset?(A,B) IMPLIES sum(A,fnr) <= sum(B,fnr)

  sum_order_sub: THEOREM subset?(A,B) AND (FORALL (t:T): fnr(t) <= gnr(t))
                           IMPLIES sum(A,fnr) <= sum(B,gnr)

  gn:  VAR function[T -> nat]
  gi:  VAR function[T -> nonneg_int]

  sum_0_nat       : THEOREM sum(S,gn) = 0 IMPLIES  S = emptyset[T] OR
                                          (FORALL (t:(S)): gn(t) = 0)

  sum_is_null     : COROLLARY sum(S,gn) = 0 => (S(t) => gn(t) = 0)

  sum_0_int       : THEOREM sum(S,gi) = 0 IMPLIES S = emptyset[T]
                                               OR (FORALL (t:(S)): gi(t) = 0)

  sum_0_non_neg   : THEOREM sum(S,f) = 0 AND (FORALL (t: (S)): f(t) >= 0) 
                             IMPLIES S = emptyset[T] 
                                      OR (FORALL (t:(S)): f(t) = 0)

  JUDGEMENT sum(A: finite_set[T], f: [T -> nonneg_real])
            HAS_TYPE nonneg_real
  JUDGEMENT sum(A: finite_set[T], f: [T -> nonneg_int]) HAS_TYPE nonneg_int
  JUDGEMENT sum(A: non_empty_finite_set[T], f: [T->posnat]) HAS_TYPE posnat

%  JUDGEMENT sum(A: non_empty_finite_set[T], f: [T->negreal]) HAS_TYPE negreal
%  JUDGEMENT sum(A: finite_set[T], f: [T -> nonpos_real]) HAS_TYPE nonpos_real
%  JUDGEMENT sum(A: finite_set[T], f: [T -> negint]) HAS_TYPE negint

END finite_sets_sum_real


$$$finite_sets/finite_sets_sum_real.prf
(|finite_sets_sum_real| (|IMP_finite_sets_sum_TCC1| "" (TCC :DEFS !) NIL NIL) (|IMP_finite_sets_sum_TCC2| "" (TCC :DEFS !) NIL NIL) (|sum_const| "" (INDUCT "S" 1 "finite_set_induction_rest") (("1" (SKOSIMP*) (("1" (REWRITE "sum_emptyset") (("1" (LEMMA "card_emptyset") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sum" 1) (("2" (INST?) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (LEMMA "card_rest") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_1_is_card| "" (LEMMA "sum_const") (("" (SKOSIMP*) (("" (INST -1 "S!1" "1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sum_mult| "" (INDUCT "S" 1 "finite_set_induction_rest") (("1" (SKOSIMP*) (("1" (LEMMA "sum_emptyset") (("1" (INST?) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "sum_emptyset") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sum" 1) (("2" (INST?) (("2" (REPLACE -1) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_empty?| "" (SKOSIMP*) (("" (REWRITE "emptyset_is_empty?[T]") (("" (LEMMA "sum_emptyset[T,real,0,+]") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sum_emptyset_rew| "" (SKOSIMP*) (("" (LEMMA "sum_emptyset[T,real,0,+]") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sum_singleton_rew| "" (SKOSIMP*) (("" (REWRITE "card_one") (("" (SKOSIMP*) (("" (REPLACE -1) (("" (REWRITE "sum_singleton[T,real,0,+]") (("" (HIDE -1) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_remove_rew| "" (SKOSIMP*) (("" (LEMMA "sum_remove[T,real,0,+]") (("" (INST?) (("" (REPLACE -1 + RL) (("" (HIDE -1) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_rest_rew_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|sum_rest_rew| "" (SKOSIMP*) (("" (LEMMA "sum_rest") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sum_union_rew| "" (SKOSIMP*) (("" (LEMMA "sum_union") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sum_eq_funs| "" (SKOSIMP*) (("" (REWRITE "sum_f_g") NIL NIL)) NIL) (|sum_particular_gen| "" (AUTO-REWRITE "member") (("" (INDUCT "S" 1 "finite_set_induction_rest[T]") (("1" (SKOSIMP*) (("1" (REWRITE "sum_emptyset") (("1" (REWRITE "sum_emptyset") (("1" (EXPAND "emptyset") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sum" 1) (("2" (LIFT-IF) (("2" (SPLIT 1) (("1" (FLATTEN) (("1" (INST?) (("1" (ASSERT) (("1" (REPLACE -2 :HIDE? T) (("1" (CASE "rest(SS!1)(t!1)") (("1" (EXPAND "rest") (("1" (REPLACE -2 * RL) (("1" (EXPAND "remove") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (INST?) (("2" (CASE " SS!1(t!1)") (("1" (ASSERT) (("1" (REPLACE -2 :HIDE? T) (("1" (EXPAND "rest") (("1" (EXPAND "remove") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE -1 :HIDE? T) (("2" (EXPAND "rest") (("2" (EXPAND "remove") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_bound| "" (INDUCT "S" 1 "finite_set_induction_rest") (("1" (SKOSIMP*) (("1" (REWRITE "sum_emptyset") (("1" (REWRITE "card_emptyset") (("1" (HIDE -1) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sum" 1) (("2" (INST -1 "N!1" "f!1") (("2" (SPLIT -1) (("1" (INST -2 "choose(SS!1)") (("1" (REWRITE "card_rest") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (SKOSIMP*) (("2" (INST -1 "t!1") (("2" (TYPEPRED "t!1") (("2" (GRIND :EXCLUDE "choose") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_order| "" (INDUCT-AND-SIMPLIFY "S" 1 "finite_set_induction_rest" :EXCLUDE ("rest" "choose")) NIL NIL) (|sum_nonneg| "" (INDUCT "S" 1 "finite_set_induction_rest") (("1" (SKOSIMP*) (("1" (REWRITE "sum_emptyset") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sum" 1) (("2" (INST?) (("2" (SPLIT -1) (("1" (INST -2 "choose(SS!1)") (("1" (ASSERT) NIL NIL)) NIL) ("2" (HIDE 2) (("2" (SKOSIMP*) (("2" (INST?) (("2" (TYPEPRED "t!1") (("2" (LEMMA "rest_member[T]") (("2" (EXPAND "member") (("2" (INST -1 "SS!1" "t!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_pos| "" (INDUCT "S" 1 "finite_set_induction_rest") (("1" (SKOSIMP*) NIL NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sum" 1) (("2" (INST?) (("2" (SPLIT -1) (("1" (INST -2 "choose(SS!1)") (("1" (ASSERT) NIL NIL)) NIL) ("2" (HIDE 2) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (REWRITE "sum_emptyset") (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (INST?) (("3" (TYPEPRED "t!1") (("3" (LEMMA "rest_member[T]") (("3" (EXPAND "member") (("3" (INST -1 "SS!1" "t!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_TCC1| "" (AUTO-REWRITE-THEORY "rationals") (("" (AUTO-REWRITE-THEORY "integers") (("" (INDUCT "A" 1 "finite_set_induction_rest") (("1" (TYPEPRED "A!1") (("1" (PROPAX) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (HIDE 2) (("2" (LEMMA "emptyset_is_empty?[T]") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (ASSERT) (("3" (SPLIT -1) (("1" (INST?) (("1" (FLATTEN) (("1" (ASSERT) (("1" (EXPAND "sum" 2) (("1" (ASSERT) (("1" (TYPEPRED "f!1(choose(SS!1))") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "sum" 2) (("2" (TYPEPRED "f!1(choose(SS!1))") (("2" (CASE "rest(SS!1) = emptyset") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (REWRITE "sum_emptyset") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 -2 2 3) (("2" (LEMMA "emptyset_is_empty?[T]") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_TCC2| "" (AUTO-REWRITE-THEORY "rationals") (("" (AUTO-REWRITE-THEORY "integers") (("" (INDUCT-AND-SIMPLIFY "x1" 1 "finite_set_induction_rest") (("" (INDUCT-AND-SIMPLIFY "A" 1 "finite_set_induction_rest") NIL NIL)) NIL)) NIL)) NIL) (|sum_TCC3| "" (SKOSIMP*) (("" (LEMMA "sum_nonneg") (("" (INST?) (("" (ASSERT) (("" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_subset| "" (SKOSIMP*) (("" (CASE "B!1 = union(A!1,difference(B!1,A!1))") (("1" (REPLACE -1 +) (("1" (HIDE -1) (("1" (LEMMA "sum_union") (("1" (INST?) (("1" (CASE "sum(intersection(A!1, difference(B!1, A!1)), fnr!1) = 0") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (ASSERT) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "sum_nonneg") (("1" (INST -1 "difference(B!1, A!1)" "fnr!1") (("1" (ASSERT) (("1" (HIDE -1) (("1" (SKOSIMP*) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 2) (("2" (CASE "intersection(A!1, difference(B!1, A!1)) = emptyset") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (REWRITE "sum_emptyset") NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sum_order_sub| "" (SKOSIMP*) (("" (LEMMA "sum_subset") (("" (INST?) (("" (INST -1 "B!1") (("" (ASSERT) (("" (LEMMA "sum_order") (("" (INST -1 "B!1" "fnr!1" "gnr!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_0_nat| "" (INDUCT "S" 1 "finite_set_induction_rest") (("1" (SKOSIMP*) NIL NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sum" -2) (("2" (INST?) (("2" (TYPEPRED "sum(rest(SS!1), gn!1)") (("2" (ASSERT) (("2" (TYPEPRED "t!1") (("2" (SPLIT -3) (("1" (ASSERT) (("1" (LEMMA "rest_emptyset[T]") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "choose_rest_or[T]") (("2" (INST?) (("2" (EXPAND "member") (("2" (INST?) (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_is_null| "" (SKOSIMP*) (("" (LEMMA "sum_0_nat") (("" (INST?) (("" (ASSERT) (("" (SPLIT -1) (("1" (HIDE -2 1) (("1" (REWRITE "emptyset_is_empty?[T]" :DIR RL) (("1" (EXPAND "empty?") (("1" (EXPAND "member") (("1" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_0_int| "" (INDUCT "S" 1 "finite_set_induction_rest") (("1" (SKOSIMP*) NIL NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sum" -2) (("2" (INST?) (("2" (TYPEPRED "sum(rest(SS!1), gi!1)") (("2" (ASSERT) (("2" (TYPEPRED "t!1") (("2" (SPLIT -3) (("1" (LEMMA "rest_emptyset[T]") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (LEMMA "choose_rest_or[T]") (("2" (INST?) (("2" (EXPAND "member") (("2" (INST?) (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_0_non_neg| "" (INDUCT "S" 1 "finite_set_induction_rest") (("1" (SKOSIMP*) NIL NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sum" -2) (("2" (INST?) (("2" (LEMMA "sum_nonneg") (("2" (INST?) (("2" (CASE "(FORALL (t: (rest(SS!1))): f!1(t) >= 0)") (("1" (REPLACE -1) (("1" (ASSERT) (("1" (CASE "f!1(choose(SS!1)) = 0") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (ASSERT) (("1" (SPLIT -3) (("1" (CASE "t!1 = choose(SS!1)") (("1" (REVEAL -1) (("1" (ASSERT) NIL NIL)) NIL) ("2" (HIDE -2 -3 -4 -5 3) (("2" (LEMMA "rest_emptyset[T]") (("2" (INST?) (("2" (INST -1 "t!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "choose_rest_or[T]") (("2" (EXPAND "member") (("2" (INST?) (("2" (INST -1 "t!1") (("2" (ASSERT) (("2" (INST -2 "t!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (INST -5 "choose(SS!1)") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 -2 -3 3) (("2" (SKOSIMP*) (("2" (INST -1 "t!2") (("2" (TYPEPRED "t!2") (("2" (LEMMA "rest_member[T]") (("2" (INST?) (("2" (EXPAND "member") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_TCC4| "" (LEMMA "sum_nonneg") (("" (SKOSIMP*) (("" (INST?) (("" (ASSERT) (("" (HIDE 2) (("" (SKOSIMP*) (("" (TYPEPRED "f!1(t!1)") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_TCC5| "" (SUBTYPE-TCC) NIL NIL))

$$$finite_sets/finite_sets_minmax.pvs
finite_sets_minmax[T: TYPE, <= : (total_order?[T])]: THEORY
BEGIN

  IMPORTING  finite_sets_inductions[T] %, sets_aux[T]

  min(x,y:T): T = IF x <= y THEN x ELSE y ENDIF
  max(x,y:T): T = IF x <= y THEN y ELSE x ENDIF

  a,x,y: VAR T
  SS: VAR non_empty_finite_set

  minrec(SS): RECURSIVE T = 
                IF empty?(rest(SS)) THEN choose(SS)
                ELSE min(choose(SS),minrec(rest(SS)))
                ENDIF
              MEASURE (LAMBDA SS: card(SS))

  maxrec(SS): RECURSIVE T = 
                IF empty?(rest(SS)) THEN choose(SS)
                ELSE max(choose(SS),maxrec(rest(SS)))
                ENDIF
              MEASURE (LAMBDA SS: card(SS))

  lt_reflexive:     LEMMA FORALL (x: T): <=(x, x)
  lt_transitive:    LEMMA FORALL (x,y,z:T): <=(x, y) & <=(y, z) => <=(x, z)
  lt_total:         LEMMA FORALL (x,y:T) : x <= y OR y <= x
  lt_antisymmetric: LEMMA FORALL (x,y: T): <=(x, y) & <=(y, x) => x = y

  min(SS): {a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}
  max(SS): {a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}
 

  min_lem: LEMMA (min(SS) = a IFF
                  SS(a) AND (FORALL (x: (SS)): a <= x))

  max_lem: LEMMA (max(SS) = a IFF
                  SS(a) AND (FORALL (x: (SS)): x <= a))

  A,B:   VAR non_empty_finite_set

  min_union: LEMMA min(A) = x AND min(B) = y IMPLIES
                      min(union(A,B)) = min(x,y)

  max_union: LEMMA max(A) = x AND max(B) = y IMPLIES
                      max(union(A,B)) = max(x,y)


END finite_sets_minmax

$$$finite_sets/finite_sets_minmax.prf
(|finite_sets_minmax|
 (|minrec_TCC1| "" (SKOSIMP*) (("" (REWRITE "card_rest") (("" (ASSERT) NIL)))))
 (|lt_reflexive| "" (SKOSIMP*)
  (("" (TYPEPRED "finite_sets_minmax.<=")
    (("" (EXPAND "total_order?")
      (("" (EXPAND "partial_order?")
        (("" (FLATTEN)
          (("" (HIDE -2 3)
            (("" (EXPAND "preorder?")
              (("" (FLATTEN)
                (("" (EXPAND "reflexive?") (("" (INST?) NIL)))))))))))))))))))
 (|lt_transitive| "" (SKOSIMP*)
  (("" (TYPEPRED "finite_sets_minmax.<=")
    (("" (EXPAND "total_order?")
      (("" (EXPAND "partial_order?")
        (("" (FLATTEN)
          (("" (HIDE -2 3)
            (("" (EXPAND "preorder?")
              (("" (FLATTEN)
                (("" (HIDE -1 -3)
                  (("" (EXPAND "transitive?")
                    (("" (INST -1 "x!1" "y!1" "z!1")
                      (("" (ASSERT) NIL)))))))))))))))))))))))
 (|lt_total| "" (SKOSIMP*)
  (("" (TYPEPRED "finite_sets_minmax.<=")
    (("" (EXPAND "total_order?")
      (("" (EXPAND "partial_order?")
        (("" (FLATTEN)
          (("" (HIDE -1 -2)
            (("" (EXPAND "dichotomous?")
              (("" (INST?) (("" (ASSERT) NIL)))))))))))))))))
 (|lt_antisymmetric| "" (SKOSIMP*)
  (("" (TYPEPRED "finite_sets_minmax.<=")
    (("" (EXPAND "total_order?")
      (("" (EXPAND "partial_order?")
        (("" (FLATTEN)
          (("" (HIDE -1 -3)
            (("" (EXPAND "antisymmetric?")
              (("" (INST?) (("" (ASSERT) NIL)))))))))))))))))
 (|min_TCC1| "" (INST 1 "(LAMBDA SS: minrec(SS))")
  (("" (INDUCT "SS" 1 "finite_set_induction_rest")
    (("1" (TYPEPRED "SS!1") (("1" (PROPAX) NIL)))
     ("2" (TYPEPRED "SS!1") (("2" (PROPAX) NIL)))
     ("3" (ASSERT) (("3" (AUTO-REWRITE-THEORY "sets[T]") (("3" (ASSERT) NIL)))))
     ("4" (SKOSIMP*)
      (("4" (EXPAND "minrec" +)
        (("4" (SPLIT 2)
          (("1" (ASSERT) NIL)
           ("2" (FLATTEN)
            (("2" (AUTO-REWRITE-THEORY "sets[T]")
              (("2" (ASSERT)
                (("2" (SKOSIMP*)
                  (("2" (EXPAND "min")
                    (("2" (ASSERT)
                      (("2" (SPLIT)
                        (("1" (FLATTEN)
                          (("1" (LEMMA "epsilon_ax[T]")
                            (("1" (INST?)
                              (("1" (ASSERT) (("1" (INST 1 "x!1") NIL)))))))))
                         ("2" (ASSERT) NIL)))))))))))))))
           ("3" (SKOSIMP*)
            (("3" (LIFT-IF)
              (("3" (SPLIT 1)
                (("1" (HIDE -2)
                  (("1" (FLATTEN)
                    (("1" (LEMMA "choose_rest_or[T]")
                      (("1" (INST?)
                        (("1" (EXPAND "member")
                          (("1" (INST?)
                            (("1" (ASSERT)
                              (("1" (SPLIT -1)
                                (("1" (EXPAND "empty?")
                                  (("1" (INST?)
                                    (("1" (EXPAND "member")
                                      (("1" (PROPAX) NIL)))))))
                                 ("2" (REPLACE -1)
                                  (("2" (HIDE -1)
                                    (("2" (REWRITE "lt_reflexive")
                                      NIL)))))))))))))))))))))
                 ("2" (FLATTEN)
                  (("2" (ASSERT)
                    (("2" (FLATTEN)
                      (("2" (EXPAND "min")
                        (("2" (LIFT-IF)
                          (("2" (ASSERT)
                            (("2" (GROUND)
                              (("1" (LEMMA "choose_rest_or[T]")
                                (("1" (EXPAND "member")
                                  (("1" (INST -1 "SS!1" "x!1")
                                    (("1" (ASSERT)
                                      (("1" (SPLIT -1)
                                        (("1"
                                          (INST -5 "x!1")
                                          (("1"
                                            (ASSERT)
                                            (("1"
                                              (HIDE -1 -3 -4 2 3)
                                              (("1"
                                                (LEMMA "lt_transitive")
                                                (("1"
                                                  (INST
                                                   -1
                                                   "choose(SS!1)"
                                                   " minrec(rest(SS!1))"
                                                   "x!1")
                                                  (("1" (ASSERT) NIL)))))))))))
                                         ("2"
                                          (REPLACE -1)
                                          (("2"
                                            (HIDE -1)
                                            (("2"
                                              (HIDE -1 -2 -3 -4)
                                              (("2"
                                                (REWRITE "lt_reflexive")
                                                NIL)))))))))))))))))
                               ("2" (INST -3 "x!1")
                                (("2" (SPLIT -3)
                                  (("1" (PROPAX) NIL)
                                   ("2" (CASE-REPLACE "x!1 = choose(SS!1)")
                                    (("1" (HIDE -1 -2 -3 1 4 5)
                                      (("1" (LEMMA "lt_total")
                                        (("1" (INST?) (("1" (GROUND) NIL)))))))
                                     ("2" (HIDE 3 4 5 6)
                                      (("2" (LEMMA "choose_rest_or[T]")
                                        (("2"
                                          (INST?)
                                          (("2"
                                            (EXPAND "member")
                                            (("2"
                                              (GROUND)
                                              NIL)))))))))))))))))))))))))))))))))))))))))))))
 (|max_TCC1| "" (INST 1 "(LAMBDA SS: maxrec(SS))")
  (("" (INDUCT "SS" 1 "finite_set_induction_rest")
    (("1" (TYPEPRED "SS!1") (("1" (PROPAX) NIL)))
     ("2" (TYPEPRED "SS!1") (("2" (PROPAX) NIL)))
     ("3" (ASSERT) (("3" (AUTO-REWRITE-THEORY "sets[T]") (("3" (ASSERT) NIL)))))
     ("4" (SKOSIMP*)
      (("4" (EXPAND "maxrec" +)
        (("4" (SPLIT 2)
          (("1" (ASSERT) NIL)
           ("2" (FLATTEN)
            (("2" (AUTO-REWRITE-THEORY "sets[T]")
              (("2" (ASSERT)
                (("2" (SKOSIMP*)
                  (("2" (EXPAND "max")
                    (("2" (ASSERT)
                      (("2" (SPLIT 2)
                        (("1" (ASSERT) NIL)
                         ("2" (FLATTEN)
                          (("2" (LEMMA "epsilon_ax[T]")
                            (("2" (INST?)
                              (("2" (ASSERT)
                                (("2" (INST 1 "x!1") NIL)))))))))))))))))))))))
           ("3" (SKOSIMP*)
            (("3" (LIFT-IF)
              (("3" (SPLIT 1)
                (("1" (HIDE -2)
                  (("1" (FLATTEN)
                    (("1" (CASE-REPLACE "x!1=choose(SS!1)")
                      (("1" (REWRITE "lt_reflexive") NIL)
                       ("2" (HIDE 2)
                        (("2" (LEMMA "choose_rest_or[T]")
                          (("2" (EXPAND "member")
                            (("2" (INST?)
                              (("2" (ASSERT)
                                (("2" (EXPAND "empty?")
                                  (("2" (EXPAND "member")
                                    (("2" (INST?) NIL)))))))))))))))))))))
                 ("2" (FLATTEN)
                  (("2" (ASSERT)
                    (("2" (FLATTEN)
                      (("2" (EXPAND "max")
                        (("2" (LIFT-IF)
                          (("2" (ASSERT)
                            (("2" (PROP)
                              (("1" (HIDE -4)
                                (("1" (LEMMA "choose_rest_or[T]")
                                  (("1" (EXPAND "member")
                                    (("1" (INST -1 "SS!1" "x!1")
                                      (("1" (ASSERT)
                                        (("1"
                                          (REVEAL -2)
                                          (("1"
                                            (INST -1 "x!1")
                                            (("1" (ASSERT) NIL)))))))))))))))
                               ("2" (ASSERT)
                                (("2" (INST -3 "x!1")
                                  (("2" (SPLIT -3)
                                    (("1" (HIDE -2 -3 3 4)
                                      (("1" (LEMMA "lt_total")
                                        (("1"
                                          (INST
                                           -1
                                           "maxrec(rest(SS!1))"
                                           "choose(SS!1) ")
                                          (("1"
                                            (PROP)
                                            (("1"
                                              (LEMMA "lt_transitive")
                                              (("1"
                                                (INST
                                                 -1
                                                 "x!1"
                                                 "maxrec(rest(SS!1))"
                                                 "choose(SS!1)")
                                                (("1" (ASSERT) NIL)))))))))))))
                                     ("2" (LEMMA "choose_rest_or[T]")
                                      (("2" (EXPAND "member")
                                        (("2"
                                          (INST?)
                                          (("2"
                                            (ASSERT)
                                            (("2"
                                              (REPLACE -1)
                                              (("2"
                                                (HIDE -1)
                                                (("2"
                                                  (REWRITE "lt_reflexive")
                                                  NIL)))))))))))))))))))))))))))))))))))))))))))))))))
 (|min_lem| "" (SKOSIMP*)
  (("" (TYPEPRED "min(SS!1)")
    (("" (PROP)
      (("1" (ASSERT) NIL)
       ("2" (SKOSIMP*)
        (("2" (REPLACE -1)
          (("2" (HIDE -1)
            (("2" (TYPEPRED "x!1") (("2" (INST?) (("2" (ASSERT) NIL)))))))))))
       ("3" (INST -4 "a!1")
        (("3" (ASSERT)
          (("3" (INST -2 "min(SS!1)")
            (("3" (ASSERT)
              (("3" (HIDE -1 -3)
                (("3" (REWRITE "lt_antisymmetric") NIL)))))))))))))))))
 (|max_lem| "" (SKOSIMP*)
  (("" (TYPEPRED "max(SS!1)")
    (("" (PROP)
      (("1" (ASSERT) NIL)
       ("2" (SKOSIMP*)
        (("2" (REPLACE -1)
          (("2" (HIDE -1)
            (("2" (TYPEPRED "x!1") (("2" (INST?) (("2" (ASSERT) NIL)))))))))))
       ("3" (INST -4 "a!1")
        (("3" (ASSERT)
          (("3" (INST -2 "max(SS!1)")
            (("3" (ASSERT)
              (("3" (HIDE -1 -3)
                (("3" (REWRITE "lt_antisymmetric") NIL)))))))))))))))))
 (|min_union| "" (SKOSIMP*)
  (("" (AUTO-REWRITE "member" "union")
    (("" (LEMMA "min_lem")
      (("" (INST-CP -1 "A!1" "x!1")
        (("" (INST -1 "B!1" "y!1")
          (("" (ASSERT)
            (("" (LEMMA "min_lem")
              (("" (INST -1 "union(A!1,B!1)" "min(x!1, y!1)")
                (("" (FLATTEN)
                  (("" (HIDE -1)
                    (("" (ASSERT)
                      (("" (HIDE 2)
                        (("" (SPLIT 1)
                          (("1" (FLATTEN)
                            (("1" (EXPAND "min")
                              (("1" (CASE "x!1 <= y!1")
                                (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))
                           ("2" (SKOSIMP*)
                            (("2" (TYPEPRED "x!2")
                              (("2" (EXPAND "union")
                                (("2" (EXPAND "min")
                                  (("2" (EXPAND "member")
                                    (("2" (LIFT-IF)
                                      (("2" (SPLIT 1)
                                        (("1"
                                          (FLATTEN)
                                          (("1"
                                            (SPLIT -2)
                                            (("1" (INST -4 "x!2") NIL)
                                             ("2"
                                              (INST -3 "x!2")
                                              (("2"
                                                (HIDE -1 -4 -5 -6)
                                                (("2"
                                                  (LEMMA "lt_transitive")
                                                  (("2"
                                                    (INST -1 "x!1" "y!1" "x!2")
                                                    (("2"
                                                      (ASSERT)
                                                      NIL)))))))))))))
                                         ("2"
                                          (FLATTEN)
                                          (("2"
                                            (SPLIT -1)
                                            (("1"
                                              (INST -3 "x!2")
                                              (("1"
                                                (ASSERT)
                                                (("1"
                                                  (HIDE -1 -2 -4 -5)
                                                  (("1"
                                                    (LEMMA "lt_transitive")
                                                    (("1"
                                                      (INST
                                                       -1
                                                       "x!1"
                                                       "x!2"
                                                       "y!1")
                                                      (("1"
                                                        (ASSERT)
                                                        (("1"
                                                          (HIDE -1 2)
                                                          (("1"
                                                            (LEMMA "lt_total")
                                                            (("1"
                                                              (INST?)
                                                              (("1"
                                                                (ASSERT)
                                                                NIL)))))))))))))))))))
                                             ("2"
                                              (INST -2 "x!2")
                                              NIL)))))))))))))))))))))))))))))))))))))))))))))
 (|max_union| "" (SKOSIMP*)
  (("" (AUTO-REWRITE "member" "union")
    (("" (LEMMA "max_lem")
      (("" (INST-CP -1 "A!1" "x!1")
        (("" (INST -1 "B!1" "y!1")
          (("" (ASSERT)
            (("" (LEMMA "max_lem")
              (("" (INST -1 "union(A!1,B!1)" "max(x!1, y!1)")
                (("" (FLATTEN)
                  (("" (HIDE -1)
                    (("" (ASSERT)
                      (("" (HIDE 2)
                        (("" (SPLIT 1)
                          (("1" (FLATTEN)
                            (("1" (EXPAND "max")
                              (("1" (CASE "x!1 <= y!1")
                                (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))
                           ("2" (SKOSIMP*)
                            (("2" (TYPEPRED "x!2")
                              (("2" (EXPAND "union")
                                (("2" (EXPAND "max")
                                  (("2" (EXPAND "member")
                                    (("2" (LIFT-IF)
                                      (("2" (SPLIT 1)
                                        (("1"
                                          (FLATTEN)
                                          (("1"
                                            (SPLIT -2)
                                            (("1"
                                              (INST -4 "x!2")
                                              (("1"
                                                (HIDE -1 -3 -5 -6)
                                                (("1"
                                                  (LEMMA "lt_transitive")
                                                  (("1"
                                                    (INST -1 "x!2" "x!1" "y!1")
                                                    (("1" (ASSERT) NIL)))))))))
                                             ("2" (INST -3 "x!2") NIL)))))
                                         ("2"
                                          (FLATTEN)
                                          (("2"
                                            (SPLIT -1)
                                            (("1" (INST -3 "x!2") NIL)
                                             ("2"
                                              (INST -2 "x!2")
                                              (("2"
                                                (HIDE -1 -3 -4 -5)
                                                (("2"
                                                  (LEMMA "lt_transitive")
                                                  (("2"
                                                    (INST -1 "x!2" "y!1" "x!1")
                                                    (("2"
                                                      (ASSERT)
                                                      (("2"
                                                        (HIDE -1 3)
                                                        (("2"
                                                          (LEMMA "lt_total")
                                                          (("2"
                                                            (INST?)
                                                            (("2"
                                                              (ASSERT)
                                                              NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
$$$finite_sets/finite_sets_inductions.pvs
finite_sets_inductions[T: TYPE]: THEORY

BEGIN

  IMPORTING finite_sets[T]

  S, S1, S2 : VAR finite_set
  SS,U : VAR non_empty_finite_set
  e : VAR T
  P : VAR pred[finite_set]
  Q : VAR pred[non_empty_finite_set]
  n : VAR nat

  cardinal_induction       : LEMMA (FORALL S : P(S)) IFF 
                                      (FORALL n, S : card(S) = n IMPLIES P(S)) 

  finite_set_induction     : THEOREM P(emptyset[T])
                                      AND (FORALL e,S: P(S) IMPLIES P(add(e,S)))
                                         IMPLIES (FORALL S: P(S))

  finite_set_ind_modified  : THEOREM  P(emptyset[T]) AND 
                             (FORALL e,S: NOT S(e) AND P(S) IMPLIES P(add(e,S)))
                                       IMPLIES (FORALL S: P(S))

  finite_set_induction_rest: THEOREM P(emptyset[T])
                                     AND (FORALL SS : P(rest(SS)) IMPLIES P(SS))
                                             IMPLIES (FORALL S : P(S))

  finite_set_induction_union: THEOREM P(emptyset[T])
                                      AND (FORALL e: P(singleton(e)))
                  AND (FORALL S1,S2: P(S1) AND P(S2) IMPLIES P(union(S1,S2)))
                                     IMPLIES (FORALL S: P(S))


  finite_set_induction_gen: THEOREM (FORALL S:
                                 (FORALL S2: card(S2) < card(S) IMPLIES P(S2))
                                                IMPLIES P(S))
                                  IMPLIES (FORALL S: P(S))


% -------- Induction rules for non empty sets ----------------


  nonempty_card_induction : LEMMA (FORALL U : Q(U)) IFF 
	                      (FORALL S, n : n > 0 AND card(S) = n IMPLIES Q(S))

  nonempty_finite_set_induct : THEOREM (FORALL e : Q(singleton(e)))
       AND (FORALL e, U : Q(U) AND NOT U(e) IMPLIES Q(add(e, U)))
                                        IMPLIES (FORALL U : Q(U))

END finite_sets_inductions


$$$finite_sets/finite_sets_inductions.prf
(|finite_sets_inductions| (|cardinal_induction| "" (GRIND :DEFS NIL) NIL) (|finite_set_induction| "" (SKOSIMP) (("" (REWRITE "cardinal_induction") (("" (INDUCT "n") (("1" (SKOSIMP) (("1" (REWRITE "empty_card" :DIR RL) (("1" (REWRITE "emptyset_is_empty?") (("1" (EXPAND "emptyset") (("1" (ASSERT) NIL))))))))) ("2" (SKOSIMP*) (("2" (USE "nonempty_card") (("2" (ASSERT) (("2" (REWRITE "nonempty_member") (("2" (SKOLEM!) (("2" (INST -2 "remove(x!1, S!1)") (("2" (INST -5 "x!1" "remove(x!1, S!1)") (("2" (AUTO-REWRITE "card_remove" "add_remove_member") (("2" (ASSERT) (("2" (EXPAND "member") (("2" (ASSERT) NIL))))))))))))))))))))))))))) (|finite_set_ind_modified| "" (SKOSIMP*) (("" (LEMMA "finite_set_induction") (("" (INST?) (("" (SPLIT -1) (("1" (INST -1 "S!1") NIL) ("2" (PROPAX) NIL) ("3" (SKOSIMP*) (("3" (INST -3 "e!1" "S!2") (("3" (ASSERT) (("3" (CASE-REPLACE "add(e!1, S!2) = S!2") (("3" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("3" (GRIND) NIL))))))))))))))))))) (|finite_set_induction_rest| "" (SKOSIMP) (("" (REWRITE "cardinal_induction" 1) (("" (INDUCT "n") (("1" (SKOSIMP*) (("1" (HIDE -3) (("1" (CASE-REPLACE "S!1 = emptyset") (("1" (REWRITE "card_empty?") (("1" (REWRITE "emptyset_is_empty?") NIL))))))))) ("2" (AUTO-REWRITE "card_rest" "nonempty?") (("2" (SKOSIMP*) (("2" (USE "nonempty_card") (("2" (ASSERT) (("2" (INST? -4) (("2" (INST -1 "rest(S!1)") (("2" (ASSERT) NIL))))))))))))))))))) (|finite_set_induction_union| "" (SKOSIMP) (("" (REWRITE "finite_set_induction") (("" (SKOSIMP) (("" (INST? -3) (("" (AUTO-REWRITE "add_as_union" "singleton") (("" (INST -4 "S!1" "singleton(e!1)") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|finite_set_induction_gen| "" (SKOSIMP) (("" (REWRITE "cardinal_induction" +) (("" (INDUCT "n" 1 "NAT_induction") (("" (SKOSIMP*) (("" (INST -3 "S!1") (("" (SPLIT -3) (("1" (PROPAX) NIL) ("2" (SKOSIMP*) (("2" (INST -2 "card(S2!1)") (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))) (|nonempty_card_induction_TCC1| "" (SKOSIMP) (("" (REWRITE "empty_card") (("" (ASSERT) NIL))))) (|nonempty_card_induction| "" (SKOLEM!) (("" (PROP) (("1" (SKOSIMP) (("1" (INST? -1) (("1" (REWRITE "empty_card") (("1" (ASSERT) NIL))))))) ("2" (SKOSIMP :PREDS? T) (("2" (REWRITE "empty_card") (("2" (INST -2 "U!1" "card(U!1)") (("2" (ASSERT) NIL))))))))))) (|nonempty_finite_set_induct| "" (SKOSIMP*) (("" (CASE "FORALL S : empty?(S) OR Q!1(S)") (("1" (INST? -1) (("1" (ASSERT) NIL))) ("2" (AUTO-REWRITE "emptyset_is_empty?[T]" "Emptyset" "Singleton" "singleton_as_add") (("2" (REWRITE "finite_set_ind_modified") (("2" (HIDE 2 3) (("2" (SKOSIMP*) (("2" (SPLIT -1) (("1" (ASSERT) (("1" (INST? -2) (("1" (ASSERT) NIL))))) ("2" (GROUND) (("2" (INST?) (("2" (INST?) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))))))))))

$$$finite_sets/finite_sets_sum.pvs
finite_sets_sum[T, R: TYPE, zero:R, +:[R,R -> R] ]: THEORY
%----------------------------------------------------------------------
%  
%                                              ----
%                                              \     
%  sum(S: finite_set[T], f:[T->R]) = zero +       f(i) 
%                                              /
%                                              ----
%                                              member(i,S)
%  
%----------------------------------------------------------------------
BEGIN

  ASSUMING
     r,r1,r2,r3 : VAR R
     zero_identity: ASSUMPTION identity?(+)(zero)
     plus_ac:       ASSUMPTION associative?(+) AND commutative?(+)
  ENDASSUMING

  plus_zero_right: LEMMA r + zero = r 
  plus_zero_left : LEMMA zero + r = r
  plus_assoc     : LEMMA (r1 + r2) + r3 = r1 + (r2 + r3) 
  plus_comm      : LEMMA r1 + r2 = r2 + r1

  IMPORTING finite_sets[T], finite_sets_inductions[T], sets_lemmas[T]

  f,g: VAR [T -> R]
  S, A, B: VAR finite_set
  x: VAR T

  sum(S,f) : RECURSIVE R = 
    IF (empty?(S)) THEN zero
    ELSE f(choose(S)) + sum(rest(S),f)
    ENDIF MEASURE (LAMBDA S,f: card(S))

  sum_emptyset  : THEOREM sum(emptyset[T],f) = zero

  sum_singleton : THEOREM sum(singleton(x),f) = f(x) + zero ;

  sum_x         : THEOREM (FORALL (x: (S)): 
                              sum(S, f) = f(x) + sum(remove(x, S), f))

  sum_x1_x2     : LEMMA (FORALL (x1,x2: (S)): f(x1) + sum(remove(x1,S),f) 
                              = f(x2) + sum(remove(x2,S),f))

  sum_add       : THEOREM sum(add(x,S),f) 
                          = sum(S,f) + IF member(x,S) THEN zero ELSE f(x) ENDIF

  sum_remove    : THEOREM sum(remove(x,S),f) 
                          + IF member(x,S) THEN f(x) ELSE zero ENDIF = sum(S,f)

  sum_rest      : THEOREM NOT empty?(S) IMPLIES
                            f(choose(S)) + sum(rest(S),f) = sum(S,f)
 
  sum_disj_union: THEOREM disjoint?(A,B) IMPLIES 
                            sum(union(A,B),f) = sum(A,f) + sum(B,f) 

  sum_diff_subset: THEOREM subset?(A, B) IMPLIES 
		            sum(difference(B, A), f) + sum(A, f) = sum(B, f) 

  sum_union      : THEOREM sum(union(A,B),f) + sum(intersection(A,B),f) =
                                         sum(A,f) + sum(B,f) 

  sum_diff_intersection: THEOREM sum(A,f) = 
                            sum(difference(A,B),f) + sum(intersection(A,B),f) 

  sum_f_g         : LEMMA (FORALL (x: (S)): f(x) = g(x)) 
                               IMPLIES sum(S, f) = sum(S, g)

  sum_particular  : THEOREM sum(S,f) = sum(S, f WITH [x := zero])
			       + IF S(x) THEN f(x) ELSE zero ENDIF 

  sum_distributive: THEOREM sum(A,f) + sum(A,g) = 
                                sum(A,(LAMBDA x: f(x) + g(x))) 

END finite_sets_sum

$$$finite_sets/finite_sets_sum.prf
(|finite_sets_sum| (|plus_zero_right| "" (SKOSIMP*) (("" (LEMMA "zero_identity") (("" (EXPAND "identity?") (("" (INST?) (("" (ASSERT) NIL))))))))) (|plus_zero_left| "" (SKOSIMP*) (("" (LEMMA "zero_identity") (("" (EXPAND "identity?") (("" (INST?) (("" (ASSERT) NIL))))))))) (|plus_assoc| "" (LEMMA "plus_ac") (("" (FLATTEN) (("" (EXPAND "associative?") (("" (PROPAX) NIL))))))) (|plus_comm| "" (LEMMA "plus_ac") (("" (FLATTEN) (("" (EXPAND "commutative?") (("" (PROPAX) NIL))))))) (|sum_TCC1| "" (GRIND) NIL) (|sum_TCC2| "" (SKOSIMP*) (("" (REWRITE "card_rest") (("" (ASSERT) NIL))))) (|sum_emptyset| "" (GRIND) NIL) (|sum_singleton| "" (SKOLEM!) (("" (EXPAND "sum") (("" (AUTO-REWRITE "choose_singleton[T]" "rest_singleton[T]" "sum_emptyset") (("" (SMASH) (("" (GRIND) NIL))))))))) (|sum_x| "" (INDUCT "S" :NAME "finite_set_induction_gen") (("" (AUTO-REWRITE "card_rest" "card_remove" "nonempty?[T]") (("" (SKOSIMP*) (("" (EXPAND "sum" 1 1) (("" (SMASH) (("1" (DELETE -1) (("1" (GRIND :EXCLUDE "sum") NIL))) ("2" (INST-CP - "rest(S!1)") (("2" (INST - "remove(x!1, S!1)") (("2" (ASSERT) (("2" (INST - "f!1" "choose(S!1)") (("1" (INST - "f!1" "x!1") (("1" (CASE-REPLACE "remove(choose(S!1), remove(x!1, S!1)) = remove(x!1, rest(S!1))") (("1" (REPLACE*) (("1" (REWRITE "plus_assoc" :DIR RL) (("1" (REWRITE "plus_assoc" :DIR RL) (("1" (LEMMA "plus_comm" ("r1" "f!1(x!1)" "r2" "f!1(choose(S!1))")) (("1" (ASSERT) NIL))))))))) ("2" (DELETE -1 -2 2 3) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND :EXCLUDE ("choose")) NIL))))))) ("2" (DELETE -1 2) (("2" (GRIND :EXCLUDE ("sum" "choose")) NIL))))) ("2" (DELETE -1 2) (("2" (GRIND :EXCLUDE ("sum" "choose")) NIL))))))))))))))))))))) (|sum_x1_x2| "" (SKOLEM!) (("" (REWRITE "sum_x" :DIR RL) (("" (REWRITE "sum_x" :DIR RL) NIL))))) (|sum_add| "" (SKOLEM!) (("" (SMASH) (("1" (REWRITE "member_add") (("1" (REWRITE "plus_zero_right") NIL))) ("2" (USE "sum_x" ("S" "add(x!1, S!1)")) (("1" (REWRITE "remove_add_member") (("1" (REWRITE "plus_comm") NIL))) ("2" (EXPAND "add") (("2" (PROPAX) NIL))))))))) (|sum_remove| "" (SKOLEM!) (("" (SMASH) (("1" (USE "sum_x") (("1" (REWRITE "plus_comm") (("1" (ASSERT) NIL))) ("2" (EXPAND "member") (("2" (PROPAX) NIL))))) ("2" (REWRITE "member_remove") (("2" (REWRITE "plus_zero_right") NIL))))))) (|sum_rest| "" (SKOSIMP) (("" (ASSERT) (("" (EXPAND "sum" 2 2) (("" (PROPAX) NIL))))))) (|sum_disj_union| "" (SKOLEM + ("A!1" _ "f!1")) (("" (AUTO-REWRITE "union_empty[T]" "sum_emptyset" "sum_add" "plus_zero_left" "plus_zero_right" "plus_assoc" "member") (("" (INDUCT "B" :NAME "finite_set_ind_modified") (("1" (ASSERT) NIL) ("2" (SKOSIMP) (("2" (GROUND) (("1" (CASE-REPLACE "union(A!1, add(e!1, S!1)) = add(e!1, union(A!1, S!1))") (("1" (ASSERT) (("1" (SMASH) (("1" (DELETE -1 -2 2) (("1" (GRIND) NIL))) ("2" (REPLACE -2) (("2" (ASSERT) NIL))))))) ("2" (DELETE -1 -2 2 3) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL))))))) ("2" (DELETE 2 3) (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))) (|sum_diff_subset| "" (SKOSIMP) (("" (FORWARD-CHAIN "union_diff_subset") (("" (USE "sum_disj_union" ("A" "A!1")) (("" (REWRITE "difference_disjoint") (("" (GROUND) (("" (REPLACE*) (("" (REWRITE "plus_comm") (("" (ASSERT) NIL))))))))))))))) (|sum_union| "" (AUTO-REWRITE "union_subset1[T]" "intersection_subset1[T]" "plus_assoc") (("" (SKOLEM!) (("" (LEMMA "sum_diff_subset" ("f" "f!1")) (("" (INST-CP - "A!1" "union(A!1, B!1)") (("" (INST - "intersection(A!1, B!1)" "B!1") (("" (GROUND) (("1" (USE "diff_union_inter") (("1" (REWRITE "plus_comm" -2) (("1" (REPLACE -2 + RL) (("1" (REPLACE -3 + RL) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "intersection_commutative") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_diff_intersection| "" (SKOLEM!) (("" (AUTO-REWRITE "sum_emptyset" "plus_zero_right" "plus_zero_left" "plus_assoc") (("" (REWRITE "sum_union" :DIR RL) (("" (CASE-REPLACE "union(difference(A!1, B!1), intersection(A!1, B!1)) = A!1") (("1" (CASE-REPLACE "intersection(difference(A!1, B!1), intersection(A!1, B!1)) = emptyset") (("1" (ASSERT) NIL) ("2" (DELETE -1 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL))))))) ("2" (DELETE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL))))))))))))) (|sum_f_g| "" (AUTO-REWRITE "sum_emptyset" "sum_add" "member") (("" (SKOLEM + (_ "f!1" "g!1")) (("" (INDUCT "S" :NAME "finite_set_ind_modified") (("1" (ASSERT) NIL) ("2" (SKOSIMP) (("2" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL) ("2" (EXPAND "add") (("2" (PROPAX) NIL))))) ("2" (DELETE 2 3) (("2" (GRIND) NIL))))))))))))) (|sum_particular| "" (AUTO-REWRITE "plus_zero_right" "plus_zero_left") (("" (SKOLEM!) (("" (SMASH) (("1" (USE "sum_x") (("1" (USE "sum_x" ("f" "f!1 WITH [x!1 := zero]")) (("1" (ASSERT) (("1" (REWRITE "plus_comm" -2) (("1" (USE "sum_f_g" ("S" "remove(x!1, S!1)" "f" "f!1")) (("1" (ASSERT) (("1" (DELETE -1 -2 -3 2) (("1" (GRIND) NIL))))))))))))))) ("2" (REWRITE "sum_f_g") NIL))))))) (|sum_distributive| "" (AUTO-REWRITE "sum_emptyset" "sum_add" "plus_zero_right" "plus_zero_left" "plus_assoc" "member") (("" (SKOLEM + (_ "f!1" "g!1")) (("" (INDUCT "A" :NAME "finite_set_ind_modified") (("1" (ASSERT) NIL) ("2" (SKOSIMP) (("2" (ASSERT) (("2" (REPLACE -1 + RL) (("2" (LEMMA "plus_comm" ("r1" "f!1(e!1)" "r2" "sum(S!1, g!1) + g!1(e!1)")) (("2" (LEMMA "plus_comm" ("r1" "f!1(e!1)" "r2" "g!1(e!1)")) (("2" (ASSERT) NIL))))))))))))))))))

$$$finite_sets/nat_fun_props.pvs
nat_fun_props : THEORY
%------------------------------------------------------------------------
%      Author:  Bruno Dutertre 
%
%      Special properties of injective/surgective functions over nats
%------------------------------------------------------------------------

BEGIN

  n, m : VAR nat

  injection_n_to_m : THEOREM
	(EXISTS (f : [below[n] -> below[m]]) : injective?(f)) IMPLIES n <= m

  surjection_n_to_m : THEOREM
	(EXISTS (f : [below[n] -> below[m]]) : surjective?(f)) IMPLIES m <= n

  bijection_n_to_m : THEOREM
	(EXISTS (f : [below[n] -> below[m]]) : bijective?(f)) IFF n = m

END nat_fun_props

$$$finite_sets/nat_fun_props.prf
(|nat_fun_props|
 (|injection_n_to_m| "" (INDUCT "n")
  (("1" (ASSERT) NIL)
   ("2" (SKOSIMP*)
    (("2" (TYPEPRED "f!1(0)")
      (("2" (ASSERT)
        (("2" (HIDE -1)
          (("2" (INST -1 "m!1 - 1")
            (("2" (ASSERT)
              (("2" (DELETE 2)
                (("2"
                  (INST 1
                   "LAMBDA (x : below[j!1]) : IF f!1(x) = m!1 - 1 THEN f!1(j!1) ELSE f!1(x) ENDIF")
                  (("1" (EXPAND "injective?")
                    (("1" (SKOSIMP)
                      (("1" (LIFT-IF)
                        (("1" (LIFT-IF)
                          (("1" (INST-CP -2 "x1!1" "j!1")
                            (("1" (INST-CP -2 "x2!1" "j!1")
                              (("1" (INST -2 "x1!1" "x2!1")
                                (("1" (ASSERT) (("1" (ASSERT) NIL)))))))))))))))))
                   ("2" (SKOSIMP) (("2" (ASSERT) NIL)))
                   ("3" (SKOSIMP)
                    (("3" (EXPAND "injective?")
                      (("3" (INST -2 "x!1" "j!1") (("3" (ASSERT) NIL)))))))))))))))))))))))))
 (|surjection_n_to_m| "" (SKOSIMP*)
  (("" (REWRITE "injection_n_to_m")
    (("" (EXPAND "surjective?")
      (("" (INST -1 "0")
        (("" (SKOSIMP)
          (("" (ASSERT)
            (("" (INST 1 "inverse(f!1)")
              (("1" (REWRITE "inj_inv") (("1" (INST 1 "x!1") NIL)))
               ("2" (INST 1 "x!1") NIL)))))))))))))))
 (|bijection_n_to_m| "" (SKOLEM!)
  (("" (PROP)
    (("1" (EXPAND "bijective?")
      (("1" (SKOSIMP)
        (("1" (LEMMA "injection_n_to_m" ("n" "n!1" "m" "m!1"))
          (("1" (LEMMA "surjection_n_to_m" ("n" "n!1" "m" "m!1"))
            (("1" (SPLIT) (("1" (ASSERT) (("1" (INST?) NIL))) ("2" (INST?) NIL)))))))))))
     ("2" (INST 1 "LAMBDA (x : below[n!1]) : x")
      (("1" (GRIND) NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL))))))))))
$$$finite_sets/card_def.pvs
card_def[T: TYPE]: THEORY
%------------------------------------------------------------------------
%
%  Fundamental definition of card
%
%      Authors:  Bruno Dutertre 
%                Ricky W. Butler
%------------------------------------------------------------------------

BEGIN

  IMPORTING finite_sets_def[T],  min_nat,
            nat_fun_props %,  more_function_props   % For proof only

  S, S2: VAR finite_set
  n,m: VAR nat
  x: VAR T
  p : VAR posnat

  inj_set(S): (nonempty?[nat]) = 
                 { n | EXISTS (f : [(S)->below[n]]) : injective?(f) }

  Card(S): nat = min(inj_set(S))

  inj_Card    : LEMMA Card(S) = n IMPLIES 
                          (EXISTS (f : [(S) -> below[n]]) : injective?(f))

  reduce_inj  : LEMMA (FORALL (f : [(S)->below[p]]) :
                          injective?(f) AND NOT surjective?(f) IMPLIES 
                              (EXISTS (g: [(S)->below[p-1]]): injective?(g)))

  Card_injection: LEMMA (EXISTS (f : [(S)->below[n]]) : injective?(f)) 
                            IMPLIES Card(S) <= n
  
  Card_surjection : LEMMA (EXISTS (f : [(S)->below[n]]) : surjective?(f)) 
                              IMPLIES n <= Card(S) 
        
  Card_bijection : THEOREM
        Card(S) = n IFF (EXISTS (f : [(S)->below[n]]) : bijective?(f))

  Card_disj_union: THEOREM disjoint?(S,S2) IMPLIES 
                              Card(union(S,S2)) = Card(S) + Card(S2)

% ------------------------------------------------------------------------
  card(S): {n: nat| n = Card(S)}               % inhibit expansion

  card_def        : THEOREM card(S) = Card(S)  % But if you really need to

END card_def

$$$finite_sets/card_def.prf
(|card_def|
 (|inj_set_TCC1| "" (SKOLEM-TYPEPRED)
  (("" (EXPAND "is_finite")
    (("" (SKOSIMP*)
      (("" (EXPAND "nonempty?")
        (("" (EXPAND "empty?")
          (("" (EXPAND "member") (("" (INST -2 "N!1") (("" (INST?) NIL)))))))))))))))
 (|inj_Card| "" (SKOSIMP)
  (("" (EXPAND "Card")
    (("" (REWRITE "min_def")
      (("" (EXPAND "minimum?")
        (("" (FLATTEN) (("" (EXPAND "inj_set") (("" (PROPAX) NIL)))))))))))))
 (|reduce_inj_TCC1| "" (ASSERT) NIL) (|reduce_inj_TCC2| "" (ASSERT) NIL)
 (|reduce_inj| "" (SKOSIMP)
  (("" (GRIND :IF-MATCH NIL)
    ((""
      (INST 2 "LAMBDA (x : (S!1)) : IF f!1(x) = p!1 - 1 THEN y!1 ELSE f!1(x) ENDIF")
      (("1" (BETA)
        (("1" (SKOSIMP)
          (("1" (INST -2 "x1!1" "x2!1")
            (("1" (LIFT-IF)
              (("1" (LIFT-IF)
                (("1" (ASSERT)
                  (("1" (PROP)
                    (("1" (INST?) NIL)
                     ("2" (INST 3 "x2!1") (("2" (ASSERT) NIL)))))))))))))))))
       ("2" (SKOSIMP) (("2" (ASSERT) NIL)))
       ("3" (SKOSIMP) (("3" (INST 2 "x!1") (("3" (ASSERT) NIL)))))))))))
 (|Card_injection| "" (SKOSIMP*)
  (("" (EXPAND "Card")
    (("" (TYPEPRED "min(inj_set(S!1))")
      (("" (INST?) (("" (ASSERT) (("" (EXPAND "inj_set") (("" (INST?) NIL)))))))))))))
 (|Card_surjection| "" (SKOSIMP*)
  (("" (NAME "CS" "Card(S!1)")
    (("" (REPLACE -1)
      (("" (FORWARD-CHAIN "inj_Card")
        (("" (SKOLEM!)
          (("" (REWRITE "injection_n_to_m")
            (("" (COPY -3)
              (("" (EXPAND "surjective?" -1)
                (("" (INST -1 "0")
                  (("" (SKOSIMP*)
                    (("" (INST 1 "f!2 o inverse(f!1)")
                      (("1" (HIDE -3 2)
                        (("1" (FORWARD-CHAIN "inj_inv[(S!1),below[n!1]]")
                          (("1" (HIDE -4)
                            (("1" (GRIND :IF-MATCH NIL :EXCLUDE INVERSE)
                              (("1"
                                (INST -6 "epsilon! (x: (S!1)): f!1(x) = x1!1"
                                 "epsilon! (x: (S!1)): f!1(x) = x2!1")
                                (("1" (INST -3 "x1!1" "x2!1") (("1" (ASSERT) NIL)))
                                 ("2" (INST 1 "x!1") NIL)))))))
                           ("2" (INST 1 "x!1") NIL)))))
                       ("2" (INST 1 "x!1") NIL)))))))))))))))))))))))
 (|Card_bijection| "" (SKOLEM!)
  (("" (PROP)
    (("1" (FORWARD-CHAIN "inj_Card")
      (("1" (SKOLEM!)
        (("1" (INST?)
          (("1" (EXPAND "bijective?")
            (("1" (ASSERT)
              (("1" (CASE "n!1 = 0")
                (("1" (DELETE -2 -3) (("1" (GRIND) NIL)))
                 ("2" (ASSERT)
                  (("2" (FORWARD-CHAIN "reduce_inj")
                    (("2" (FORWARD-CHAIN "Card_injection")
                      (("2" (ASSERT) NIL)))))))))))))))))))
     ("2" (EXPAND "bijective?")
      (("2" (SKOSIMP)
        (("2" (LEMMA "Card_injection" ("S" "S!1" "n" "n!1"))
          (("2" (SPLIT)
            (("1" (LEMMA "Card_surjection" ("S" "S!1" "n" "n!1"))
              (("1" (GROUND) (("1" (INST?) NIL)))))
             ("2" (INST?) NIL)))))))))))))
 (|Card_disj_union| "" (SKOSIMP)
  (("" (NAME-REPLACE "N1" "Card(S!1)" :HIDE? NIL)
    (("" (NAME-REPLACE "N2" "Card(S2!1)" :HIDE? NIL)
      (("" (AUTO-REWRITE "Card_bijection")
        (("" (DO-REWRITE)
          (("" (SKOSIMP*)
            ((""
              (INST 1
               "LAMBDA (x : (union(S!1, S2!1))) : IF S!1(x) THEN f!2(x) ELSE N1 + f!1(x) ENDIF")
              (("1" (EXPAND "bijective?")
                (("1" (PROP)
                  (("1" (DELETE -2 -4) (("1" (GRIND) NIL)))
                   ("2" (DELETE -1 -3)
                    (("2" (GRIND :IF-MATCH NIL)
                      (("2" (INST -3 "y!1")
                        (("1" (SKOLEM!) (("1" (INST? 1) (("1" (ASSERT) NIL)))))
                         ("2" (ASSERT)
                          (("2" (INST -2 "y!1 - N1")
                            (("2" (SKOLEM!) (("2" (GRIND) NIL)))))))))))))))))
               ("2" (SKOSIMP) (("2" (ASSERT) NIL)))
               ("3" (DELETE -1 -2) (("3" (GRIND) NIL)))
               ("4" (SKOSIMP) (("4" (ASSERT) NIL)))))))))))))))))
 (|card_TCC1| "" (INST 1 "(LAMBDA S: Card(S))") NIL)
 (|card_def| "" (SKOSIMP*) (("" (ASSERT) NIL))))

$$$finite_sets/finite_sets.pvs
finite_sets[T: TYPE]: THEORY

BEGIN

  IMPORTING card_def[T] 

  A, B, S: VAR finite_set
  x: VAR T
  n: VAR nat

  card_emptyset   : THEOREM card(emptyset[T]) = 0

  empty_card      : THEOREM empty?(S) IFF card(S) = 0

  card_empty?     : THEOREM (card(S) = 0) = empty?(S)

  card_is_0       : THEOREM (card(S) = 0) = (S = emptyset)

  nonempty_card   : THEOREM nonempty?(S) IFF card(S) > 0

  card_singleton  : THEOREM card(singleton(x)) = 1

  card_one        : THEOREM card(S) = 1 IFF (EXISTS x : S = singleton(x))

  card_disj_union : THEOREM disjoint?(A,B) IMPLIES 
                              card(union(A,B)) = card(A) + card(B)

  card_diff_subset: THEOREM subset?(A, B) IMPLIES 
                                  card(difference(B, A)) = card(B) - card(A)

  card_subset     : THEOREM subset?(A,B) IMPLIES card(A) <= card(B)

  card_plus       : THEOREM card(A) + card(B) = 
                                card(union(A, B)) + card(intersection(A,B))  

  card_union      : THEOREM card(union(A,B)) = card(A) + card(B) -
                                               card(intersection(A,B))

  card_add        : THEOREM card(add(x, S)) = card(S) 
                                                   + IF S(x) THEN 0 ELSE 1 ENDIF

  card_remove     : THEOREM card(remove(x, S)) = card(S)
                                                   - IF S(x) THEN 1 ELSE 0 ENDIF

  card_rest       : THEOREM NOT empty?(S) IMPLIES card(rest(S)) = card(S) - 1

  same_card_subset: THEOREM subset?(A, B) AND card(A) = card(B) 
                               IMPLIES A = B

  smaller_card_subset : THEOREM subset?(A, B) AND card(A) < card(B) IMPLIES
                                 (EXISTS x : member(x, B) AND NOT member(x, A))

  card_1_has_1    : THEOREM card(S) >= 1 IMPLIES (EXISTS (x: T): S(x))

  card_2_has_2    : THEOREM card(S) >= 2 IMPLIES
                              (EXISTS (x,y: T): x /= y AND S(x) AND S(y))

  card_intersection_le: THEOREM card(intersection(A,B)) <= card(A) AND
                              card(intersection(A,B)) <= card(B)

  N: VAR nat
  card_bij        : THEOREM card(S) = N
                             IFF (EXISTS (f: [(S) -> below[N]]): bijective?(f))

  bij_exists      : COROLLARY (EXISTS (f: [(S) -> below(card(S))]):
                                       bijective?(f))

%  card_n_has_n    : THEOREM card(S) >= n IMPLIES
%                              (EXISTS (X: [below[N] -> T]):
%                                   (FORALL (i: below[N]): S(X(i))) AND
%                                   (FORALL (i,j: below[N]): X(i) /= X(j)))
               
END finite_sets

$$$finite_sets/finite_sets.prf
(|finite_sets| (|card_emptyset| "" (REWRITE "card_def") (("" (REWRITE "Card_bijection") (("" (INST 1 "LAMBDA (x : {x: T | FALSE}) : 0") (("1" (EXPAND "bijective?") (("1" (PROP) (("1" (EXPAND "injective?") (("1" (SKOSIMP*) (("1" (TYPEPRED "x1!1") (("1" (EXPAND "emptyset") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "surjective?") (("2" (SKOSIMP*) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL) ("3" (SKOSIMP*) NIL NIL)) NIL)) NIL)) NIL) (|empty_card| "" (SKOLEM!) (("" (PROP) (("1" (REWRITE "emptyset_is_empty?[T]") (("1" (REPLACE -1) (("1" (USE "card_emptyset") NIL NIL)) NIL)) NIL) ("2" (REWRITE "card_def") (("2" (REWRITE "Card_bijection") (("2" (SKOLEM!) (("2" (DELETE -) (("2" (GRIND) (("2" (TYPEPRED "f!1(x!1)") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_empty?| "" (SKOSIMP*) (("" (REWRITE "empty_card") NIL NIL)) NIL) (|card_is_0| "" (SKOSIMP*) (("" (REWRITE "card_empty?") (("" (REWRITE "emptyset_is_empty?") NIL NIL)) NIL)) NIL) (|nonempty_card| "" (SKOSIMP) (("" (EXPAND "nonempty?") (("" (REWRITE "empty_card") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|card_singleton| "" (SKOSIMP*) (("" (REWRITE "card_def") (("" (REWRITE "Card_bijection") (("" (INST 1 "LAMBDA (y : (singleton(x!1))) : 0") (("" (GRIND) (("" (INST 1 "x!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_one| "" (SKOSIMP*) (("" (REWRITE "card_def") (("" (PROP) (("1" (REWRITE "Card_bijection") (("1" (SKOLEM!) (("1" (GRIND :IF-MATCH NIL) (("1" (INST -2 "0") (("1" (SKOLEM!) (("1" (INST? 1) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (IFF) (("1" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (REWRITE "card_def" :DIR RL) (("2" (REWRITE "card_singleton") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_disj_union| "" (SKOSIMP*) (("" (REWRITE "card_def") (("" (REWRITE "card_def") (("" (REWRITE "card_def") (("" (REWRITE "Card_disj_union") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|card_diff_subset| "" (SKOSIMP) (("" (FORWARD-CHAIN "union_diff_subset") (("" (LEMMA "card_disj_union") (("" (INST?) (("" (ASSERT) (("" (REWRITE "difference_disjoint") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_subset| "" (SKOSIMP) (("" (FORWARD-CHAIN "card_diff_subset") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|card_plus| "" (AUTO-REWRITE "union_subset1[T]" "intersection_subset1[T]") (("" (SKOLEM!) (("" (LEMMA "card_diff_subset") (("" (INST-CP -1 "A!1" "union(A!1, B!1)") (("" (REWRITE "diff_union_inter[T]") (("" (INST? -1) (("" (GROUND) (("" (REWRITE "intersection_commutative" 1) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_union| "" (SKOSIMP*) (("" (LEMMA "card_plus") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|card_add| "" (SKOSIMP*) (("" (LIFT-IF) (("" (PROP) (("1" (REWRITE "member_add") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "member") (("2" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (REWRITE "add_as_union") (("2" (REWRITE "singleton" :DIR RL) (("2" (REWRITE "union_commutative") (("2" (REWRITE "card_disj_union") (("1" (REWRITE "card_singleton") (("1" (ASSERT) (("1" (EXPAND "singleton") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "singleton_disjoint") (("2" (EXPAND "member") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_remove| "" (SKOLEM!) (("" (LIFT-IF) (("" (PROP) (("1" (REWRITE "remove_as_difference") (("1" (REWRITE "card_diff_subset") (("1" (REWRITE "card_singleton") NIL NIL) ("2" (LEMMA "singleton_subset[T]") (("2" (INST?) (("2" (EXPAND "member") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "member_remove") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "member") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_rest| "" (SKOSIMP) (("" (EXPAND "rest") (("" (REWRITE "card_remove") (("1" (LEMMA "choose_member[T]") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (EXPAND "nonempty?") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|same_card_subset| "" (SKOSIMP) (("" (CASE "EXISTS x : member(x, B!1) AND subset?(A!1, remove(x, B!1))") (("1" (SKOSIMP) (("1" (EXPAND "member") (("1" (FORWARD-CHAIN "card_subset") (("1" (REWRITE "card_remove") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND :EXCLUDE "Card" :IF-MATCH NIL) (("1" (INST? -) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST? +) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (ASSERT) (("2" (INST - "x!2") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|smaller_card_subset| "" (SKOSIMP) (("" (FORWARD-CHAIN "card_subset") (("" (CASE-REPLACE "A!1 = B!1") (("1" (ASSERT) NIL NIL) ("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|card_1_has_1| "" (SKOSIMP*) (("" (USE "card_empty?") (("" (IFF) (("" (FLATTEN) (("" (ASSERT) (("" (EXPAND "empty?") (("" (SKOSIMP*) (("" (EXPAND "member") (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_2_has_2| "" (SKOSIMP*) (("" (LEMMA "card_1_has_1") (("" (INST?) (("" (ASSERT) (("" (SKOSIMP*) (("" (LEMMA "card_1_has_1") (("" (INST -1 "remove(x!1,S!1)") (("" (REWRITE "card_remove") (("" (LIFT-IF) (("" (ASSERT) (("" (SKOSIMP*) (("" (EXPAND "remove") (("" (EXPAND "member") (("" (FLATTEN) (("" (INST 2 "x!1" "x!2") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_intersection_le| "" (SKOSIMP*) (("" (CASE "subset?(intersection(A!1, B!1),A!1) AND
             subset?(intersection(A!1, B!1),B!1)") (("1" (FLATTEN) (("1" (LEMMA "card_subset") (("1" (SPLIT 1) (("1" (INST -1 "intersection(A!1, B!1)" "A!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST -1 "intersection(A!1, B!1)" "B!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND "subset?") (("2" (EXPAND "intersection") (("2" (EXPAND "member") (("2" (SPLIT 1) (("1" (SKOSIMP*) NIL NIL) ("2" (SKOSIMP*) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_bij| "" (SKOSIMP*) (("" (REWRITE "card_def") (("" (REWRITE "Card_bijection") NIL NIL)) NIL)) NIL) (|bij_exists| "" (SKOSIMP*) (("" (LEMMA "card_bij") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL))

$$$finite_sets/top.pvs
%------------------------------------------------------------------------
%
%  Top of finite sets theory   Version 2.2    5/22/97
%  --------------------------------------------------------------
%      Authors: Ricky W. Butler   NASA Langley Research Center
%               Bruno Dutertre    Royal Holloway & Bedford New College
%               Damir Jamsek      Odyssey Research Associates
%               Sam Owre          SRI International
%               David Griffioen   CWI and KUN (Catholic University 
%                                 Nijmegen), the Netherlands.
%   


%      Index:
%      ------
%        finite_sets            -- main theory that is imported
%                                  (provides basic type and cardinality)
%        finite_sets_sum        -- summation over a set
%        finite_sets_minmax     -- min and max over a set
%        finite_sets_inductions -- induction schemes
%        finite_sets_sum_real   -- additional properties for summations
%                                  over real-valued functions
%        finite_sets_int        -- special properties of integer sets
%        finite_sets_nat        -- special properties of natural sets
%        finite_sets_pred       -- lemmas involving predicate subtypes
%        finite_sets_below      -- lemmas involving sets of below and upto
%        finite_sets_eq         -- lemmas to show set is finite via mappings
%        finite_sets_card_eq    -- equal cardinality of two dissimilar sets
%        finite_sets_rules      -- experimental AUTO-REWRITE-THEORY rules
%
%
%  This theory was designed for making libraries and is not intended
%  for importing.  One should directly import one of the above listed
%  theories.
%
%------------------------------------------------------------------------
top: THEORY
BEGIN

  IMPORTING finite_sets, finite_sets_sum, 
             finite_sets_minmax, 
             finite_sets_inductions, finite_sets_sum_real, 
             finite_sets_int, finite_sets_nat, finite_sets_pred,
             finite_sets_below, finite_sets_card_eq, finite_sets_eq,


% added by Vlad Rusu
             more_finite_sets

END top

$$$finite_sets/top.prf
(|top| (IMPORTING1_TCC1 "" (REWRITE "zero_identity") NIL)
 (IMPORTING1_TCC2 "" (REWRITE "plus_ac") NIL))
$$$allslots_aux.pvs
allslots_aux: THEORY
 BEGIN

  lib: LIBRARY = "finite_sets"

  IMPORTING lib@top, lib@more_finite_sets, allslots

%%%%%%%%%%%%%%%%%%%%%% auxiliary lemmas for the allslots1 theorem %%%%%%%%%%%
  allslots1_aux0: LEMMA
    invariant(LAMBDA (s: State):
                s`pc = CepSlotInquirySequence_P2 IMPLIES s`reportSize = 0)

  allslots1_aux1: LEMMA
    invariant(LAMBDA (s: State):
                (s`pc = CepSIQ_Reply_P2 OR s`pc = CepSIQ_Ready_P2) IMPLIES
                 s`reportSize <= pSlotCount)

  allslots1_aux2: LEMMA
    invariant(LAMBDA (s: State):
                (s`pc = CepSIQ_Reply_P2 OR s`pc = CepSIQ_Ready_P2) IMPLIES
                 (s`reportSize <= pSlotCount AND
                   (FORALL (i, w: nat):
                      (i < s`reportSize AND
                        w < pSlotCount AND
                         vSlots(w)`Currency = s`report(i)`Currency AND
                          vSlots(w)`InUse)
                       IMPLIES s`slotsReported(w))))

  allslots1_aux3: THEOREM
    invariant(LAMBDA (s: State):
                (s`pc = CepSIQ_Ready_P2 OR s`pc = CepSIQ_Reply_P2) IMPLIES
                 (s`reportSize <= pSlotCount AND
                   (FORALL (i, j: nat):
                      i < s`reportSize AND j < s`reportSize AND i /= j
                       IMPLIES
                       s`report(i)`Currency /= s`report(j)`Currency)))



%%%%%%%%%%%%% judgements and auxiliary lemmas for the allslots2 theorem %%%%%%%%%%%
 
  used_indices: setof[nat] = {k: nat | k < pSlotCount AND vSlots(k)`InUse}

  finite_used_indices: JUDGEMENT used_indices HAS_TYPE finite_set[nat]

  used_currencies: setof[nat] =
      {c: nat | EXISTS (j: (used_indices)): vSlots(j)`Currency = c}

  finite_used_currencies: JUDGEMENT used_currencies HAS_TYPE finite_set[nat]

  reported_currencies(s: State): setof[nat] =
      {c: nat |
         EXISTS (j: nat):
           j < s`reportSize AND
            s`reportSize <= pSlotCount AND s`report(j)`Currency = c}

  finite_reported_currencies: JUDGEMENT reported_currencies HAS_TYPE
      [State -> finite_set[nat]]

  unused_indices(s: State): setof[nat] =
      {k: nat |
         k < s`vSlotIndex AND
          s`vSlotIndex <= pSlotCount AND NOT vSlots(k)`InUse}

  finite_unused_indices: JUDGEMENT unused_indices HAS_TYPE
      [State -> finite_set[nat]]

  inuse_and_reported(s: State): setof[nat] =
      {k: nat |
         k < s`vSlotIndex AND
          s`vSlotIndex <= pSlotCount AND
           s`slotsReported(k) AND vSlots(k)`InUse}

  finite_inuse_and_reported: JUDGEMENT inuse_and_reported HAS_TYPE
      [State -> finite_set[nat]]



allslots2_aux11: LEMMA
    invariant(LAMBDA (s: State):
                (s`pc = CepSIQ_Reply_P2 OR s`pc = CepSIQ_Ready_P2) IMPLIES
                 s`vSlotIndex = pSlotCount)


allslots2_aux10: LEMMA
    invariant(LAMBDA (s: State):
                (s`pc = CepSIQ_Reply_P2 OR
                  s`pc = CepSIQ_Ready_P2 OR
                   s`pc = CepSlotInquirySequence_P2)
                 IMPLIES
                 (s`vSlotsReported <= s`vSlotIndex AND
                   s`vSlotIndex <= pSlotCount))


allslots2_aux9: LEMMA
    invariant(LAMBDA (s: State):
                s`pc = CepSlotInquirySequence_P2 IMPLIES
                 (FORALL (i: nat):
                    (i < s`vSlotIndex AND
                      s`vSlotIndex <= pSlotCount AND vSlots(i)`InUse)
                     IMPLIES NOT s`slotsReported(i)))

  

allslots2_aux8: LEMMA
    invariant(LAMBDA (s: State):
                (s`pc = CepSIQ_Reply_P2 OR
                  s`pc = CepSIQ_Ready_P2 OR
                   s`pc = CepSlotInquirySequence_P2)
                 IMPLIES s`reportSize = card_def[nat].card(inuse_and_reported(s)))

 
 allslots2_aux7: LEMMA
    invariant(LAMBDA (s: State):
                (s`pc = CepSIQ_Reply_P2 OR
                  s`pc = CepSIQ_Ready_P2 OR
                   s`pc = CepSlotInquirySequence_P2)
                 IMPLIES
                 card_def[nat].card(unused_indices(s)) + card_def[nat].card(inuse_and_reported(s)) =
                  s`vSlotsReported)

  


  allslots2_aux6: LEMMA
    invariant(LAMBDA (s: State):
                (s`vSlotsReported = pSlotCount AND
                  s`vSlotIndex = pSlotCount)
                 IMPLIES
                 card_def[nat].card(unused_indices(s)) + card_def[nat].card(used_indices) =
                  s`vSlotsReported)

  allslots2_aux5: LEMMA
    invariant(LAMBDA (s: State):
                ((s`pc = CepSIQ_Reply_P2 OR
                   s`pc = CepSIQ_Ready_P2 OR
                    s`pc = CepSlotInquirySequence_P2)
                  AND s`vSlotsReported >= pSlotCount)
                 IMPLIES card_def[nat].card(used_indices) = s`reportSize)

  allslots2_aux4: LEMMA
    invariant(LAMBDA (s: State):
                ((s`pc = CepSIQ_Reply_P2 OR
                   s`pc = CepSIQ_Ready_P2 OR
                    s`pc = CepSlotInquirySequence_P2)
                  AND s`vSlotsReported >= pSlotCount)
                 IMPLIES card_def[nat].card(used_currencies) = s`reportSize)

  allslots2_aux3: LEMMA
    invariant(LAMBDA (s: State):
                (s`pc = CepSIQ_Reply_P2 OR
                  s`pc = CepSIQ_Ready_P2 OR
                   s`pc = CepSlotInquirySequence_P2)
                 IMPLIES s`reportSize = card_def[nat].card(reported_currencies(s)))

  allslots2_aux2: LEMMA
    invariant(LAMBDA (s: State):
                (s`pc = CepSIQ_Reply_P2 OR
                  s`pc = CepSIQ_Ready_P2 OR
                   s`pc = CepSlotInquirySequence_P2)
                 IMPLIES
                 (s`reportSize <= pSlotCount) AND
                  subset?(reported_currencies(s), used_currencies))

  allslots2_aux1: LEMMA
    invariant(LAMBDA (s: State):
                ((s`pc = CepSIQ_Reply_P2 OR
                   s`pc = CepSIQ_Ready_P2 OR
                    s`pc = CepSlotInquirySequence_P2)
                  AND s`vSlotsReported >= pSlotCount)
                 IMPLIES
                 (s`reportSize <= pSlotCount) AND
                  subset?(used_currencies, reported_currencies(s)))

  allslots2_aux0: LEMMA
    invariant(LAMBDA (s: State):
                (s`pc = CepSIQ_Reply_P2 AND s`vSlotsReported >= pSlotCount)
                 IMPLIES
                 (s`reportSize <= pSlotCount AND
                   (FORALL (i: nat):
                      i < pSlotCount AND vSlots(i)`InUse IMPLIES
                       (EXISTS (j: nat):
                          j < s`reportSize AND
                           s`report(j)`Currency = vSlots(i)`Currency))))
 END allslots_aux



$$$allslots_aux.prf
(|allslots_aux|
 (|allslots1_aux0| "" (LEMMA "invariant_rule")
  (("" (INST?)
    (("" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (HIDE 2)
        (("2" (SKOLEM 1 "r")
          (("2" (TYPEPRED "r")
            (("2" (BETA)
              (("2" (SPLIT)
                (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL)
                 ("2" (HIDE -2)
                  (("2" (SKOLEM 1 "n")
                    (("2" (TYPEPRED "n")
                      (("2" (FLATTEN) (("2" (GRIND) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|allslots1_aux1| "" (LEMMA "invariant_rule")
  (("" (INST?)
    (("" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (HIDE 2)
        (("2" (SKOLEM 1 "r")
          (("2" (TYPEPRED "r")
            (("2" (BETA)
              (("2" (SPLIT)
                (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL)
                 ("2" (HIDE -2)
                  (("2" (SKOLEM 1 "n")
                    (("2" (TYPEPRED "n")
                      (("2" (FLATTEN)
                        (("2" (GRIND)
                          (("2" (LEMMA "allslots1_aux0")
                            (("2" (GRIND) NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|allslots1_aux2_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|allslots1_aux2_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|allslots1_aux2_TCC3| "" (SUBTYPE-TCC) NIL NIL)
 (|allslots1_aux2_TCC4| "" (SUBTYPE-TCC) NIL NIL)
 (|allslots1_aux2| "" (LEMMA "invariant_rule")
  (("" (INST?)
    (("1" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (HIDE 2)
        (("2" (SKOLEM 1 "r")
          (("2" (TYPEPRED "r")
            (("2" (BETA)
              (("2" (SPLIT)
                (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL)
                 ("2" (HIDE -2)
                  (("2" (SKOLEM 1 "n")
                    (("2" (TYPEPRED "n")
                      (("2" (FLATTEN)
                        (("2" (EXPAND "run_fragment")
                          (("2" (INST -4 "n")
                            (("2" (GROUND)
                              (("1" (GRIND :IF-MATCH NIL) NIL NIL)
                               ("2"
                                (SKOLEM + ("i" "w"))
                                (("2"
                                  (INST - "i" "w")
                                  (("2" (GRIND) NIL NIL))
                                  NIL))
                                NIL)
                               ("3" (GRIND :IF-MATCH NIL) NIL NIL)
                               ("4"
                                (SKOLEM 1 ("j" "z"))
                                (("4"
                                  (GRIND :IF-MATCH NIL)
                                  (("1"
                                    (TYPEPRED "vSlots")
                                    (("1"
                                      (INST
                                       -1
                                       "z"
                                       "mSlotInfo(a!1)`SlotIndex")
                                      (("1"
                                        (GRIND :IF-MATCH NIL)
                                        NIL
                                        NIL))
                                      NIL))
                                    NIL)
                                   ("2"
                                    (INST -7 "j" "z")
                                    (("2" (GRIND) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL)
                               ("5"
                                (GRIND)
                                (("5"
                                  (LEMMA "allslots1_aux0")
                                  (("5" (GRIND) NIL NIL))
                                  NIL))
                                NIL)
                               ("6"
                                (GRIND :IF-MATCH NIL)
                                (("6"
                                  (LEMMA "allslots1_aux0")
                                  (("6" (GRIND) NIL NIL))
                                  NIL))
                                NIL)
                               ("7" (GRIND) NIL NIL)
                               ("8" (GRIND :IF-MATCH NIL) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL)
     ("3" (HIDE 2) (("3" (GRIND) NIL NIL)) NIL)
     ("4" (HIDE 2) (("4" (GRIND) NIL NIL)) NIL)
     ("5" (HIDE 2) (("5" (GRIND) NIL NIL)) NIL))
    NIL))
  NIL)
 (|allslots1_aux3_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|allslots1_aux3_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|allslots1_aux3| "" (LEMMA "invariant_rule")
  (("" (INST?)
    (("1" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (HIDE 2)
        (("2" (SKOLEM 1 "r")
          (("2" (TYPEPRED "r")
            (("2" (BETA)
              (("2" (SPLIT)
                (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL)
                 ("2" (HIDE -2)
                  (("2" (SKOLEM 1 "n")
                    (("2" (TYPEPRED "n")
                      (("2" (FLATTEN)
                        (("2" (EXPAND "run_fragment")
                          (("2" (INST -4 "n")
                            (("2" (GROUND)
                              (("1" (GRIND :IF-MATCH NIL) NIL NIL)
                               ("2"
                                (SKOLEM 1 ("i" "j"))
                                (("2"
                                  (INST - "i" "j")
                                  (("2"
                                    (GRIND)
                                    (("1"
                                      (NAME
                                       "m"
                                       "mSlotInfo(a!1)`SlotIndex")
                                      (("1"
                                        (REPLACE -1)
                                        (("1"
                                          (HIDE -1)
                                          (("1"
                                            (LEMMA "allslots1_aux2")
                                            (("1"
                                              (EXPAND "invariant")
                                              (("1"
                                                (INST?)
                                                (("1"
                                                  (GROUND)
                                                  (("1"
                                                    (INST -2 "j" "m")
                                                    (("1"
                                                      (GRIND)
                                                      NIL
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL)
                                     ("2"
                                      (LEMMA "allslots1_aux2")
                                      (("2"
                                        (EXPAND "invariant")
                                        (("2"
                                          (INST?)
                                          (("2"
                                            (GROUND)
                                            (("2"
                                              (INST
                                               -2
                                               "i"
                                               "mSlotInfo(a!1)`SlotIndex")
                                              (("2" (GRIND) NIL NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL)
                                     ("3"
                                      (LEMMA "allslots1_aux2")
                                      (("3"
                                        (EXPAND "invariant")
                                        (("3"
                                          (INST?)
                                          (("3"
                                            (GROUND)
                                            (("3"
                                              (INST
                                               -2
                                               "i"
                                               "mSlotInfo(a!1)`SlotIndex")
                                              (("3" (GRIND) NIL NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL)
                                     ("4"
                                      (LEMMA "allslots1_aux2")
                                      (("4"
                                        (EXPAND "invariant")
                                        (("4"
                                          (INST?)
                                          (("4"
                                            (GROUND)
                                            (("4"
                                              (INST
                                               -2
                                               "j"
                                               "mSlotInfo(a!1)`SlotIndex")
                                              (("4" (GRIND) NIL NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL)
                               ("3" (GRIND :IF-MATCH NIL) NIL NIL)
                               ("4"
                                (SKOLEM 1 ("i" "j"))
                                (("4"
                                  (INST - "i" "j")
                                  (("4" (GRIND) NIL NIL))
                                  NIL))
                                NIL)
                               ("5" (GRIND :IF-MATCH NIL) NIL NIL)
                               ("6"
                                (SKOLEM 1 ("i" "j"))
                                (("6" (GRIND) NIL NIL))
                                NIL)
                               ("7"
                                (GRIND :IF-MATCH NIL)
                                (("7"
                                  (LEMMA "allslots1_aux0")
                                  (("7" (GRIND) NIL NIL))
                                  NIL))
                                NIL)
                               ("8"
                                (SKOLEM 1 ("i" "j"))
                                (("8"
                                  (GRIND)
                                  (("8"
                                    (LEMMA "allslots1_aux0")
                                    (("8" (GRIND) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL)
     ("3" (HIDE 2) (("3" (GRIND) NIL NIL)) NIL))
    NIL))
  NIL)
 (|used_indices_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|finite_used_indices| "" (EXPAND* "is_finite" "used_indices")
  (("" (INST 1 "pSlotCount" "LAMBDA(n: (used_indices)) : n")
    (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL))
  NIL)
 (|used_currencies_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|finite_used_currencies| "" (EXPAND "used_currencies")
  (("" (LEMMA "finite_sets_def[nat].finite_subset")
    ((""
      (INST -1 "{c: nat |
                 EXISTS (j: nat):
                   j < pSlotCount AND vSlots(j)`Currency = c}"
       "{c: nat |
                 EXISTS (j: nat):
                   j < pSlotCount AND
                    vSlots(j)`InUse AND vSlots(j)`Currency = c}")
      (("1" (PROP)
        (("1" (EXPAND "is_finite")
          (("1" (SKOLEM -1 ("N" "f"))
            (("1" (INST 1 "N" "f")
              (("1" (EXPAND "injective?")
                (("1" (SKOLEM 1 ("x1" "x2"))
                  (("1" (INST -1 "x1" "x2")
                    (("1" (TYPEPRED "x2")
                      (("1" (SKOLEM -1 "j")
                        (("1" (INST 1 "j")
                          (("1" (TYPEPRED "j") (("1" (GRIND) NIL NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL)
                     ("2" (TYPEPRED "x1")
                      (("2" (SKOLEM -1 "j")
                        (("2" (TYPEPRED "j") (("2" (GRIND) NIL NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (SKOLEM 1 "x")
                (("2" (PROP)
                  (("1" (SKOLEM -1 "j")
                    (("1" (INST 1 "j")
                      (("1" (ASSERT) NIL NIL) ("2" (GRIND) NIL NIL))
                      NIL))
                    NIL)
                   ("2" (SKOLEM -1 "j")
                    (("2" (INST 1 "j")
                      (("2" (TYPEPRED "j") (("2" (GRIND) NIL NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL))
        NIL)
       ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL)
       ("3" (HIDE 2)
        (("3" (LEMMA "more_finite_sets[nat,nat].finite_image")
          (("3"
            (INST -1 "{c:nat | c< pSlotCount}"
             "LAMBDA(n :{c:nat | c< pSlotCount}) : vSlots(n)`Currency")
            (("1" (EXPAND "is_finite")
              (("1" (SKOLEM -1 ("N" "f"))
                (("1" (INST 1 "N" "f")
                  (("1" (EXPAND "injective?")
                    (("1" (SKOLEM 1 ("x1" "x2"))
                      (("1" (INST -1 "x1" "x2")
                        (("1" (TYPEPRED "x2")
                          (("1" (SKOLEM -1 "j")
                            (("1" (INST 1 "j")
                              (("1" (GROUND) NIL NIL)
                               ("2" (GROUND) NIL NIL))
                              NIL))
                            NIL))
                          NIL)
                         ("2" (TYPEPRED "x1")
                          (("2" (SKOLEM -1 "j")
                            (("2" (INST 1 "j")
                              (("1" (GROUND) NIL NIL)
                               ("2" (GROUND) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL)
                   ("2" (HIDE -1)
                    (("2" (SKOSIMP*)
                      (("2" (PROP)
                        (("1" (SKOLEM -1 "x")
                          (("1" (INST 1 "x")
                            (("1" (TYPEPRED "x")
                              (("1" (GRIND) NIL NIL)) NIL))
                            NIL))
                          NIL)
                         ("2" (SKOLEM -1 "x")
                          (("2" (INST 1 "x")
                            (("1" (GRIND) NIL NIL)
                             ("2" (GRIND) NIL NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL)
             ("3" (HIDE 2)
              (("3" (EXPAND "is_finite")
                (("3"
                  (INST 1 "pSlotCount"
                   "LAMBDA (n : {c: nat | c < pSlotCount}) : n")
                  (("3" (GRIND) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("4" (HIDE 2) (("4" (GRIND) NIL NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|reported_currencies_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|finite_reported_currencies| "" (EXPAND "reported_currencies")
  (("" (SKOLEM 1 "s")
    (("" (LEMMA "finite_sets_def[nat].finite_subset")
      ((""
        (INST -1 "{c: nat |
                 EXISTS (j: nat):
                   j <= 15 AND s`report(j)`Currency = c}" "{c: nat |
                 EXISTS (j: nat):
                   j < s`reportSize AND
                    s`reportSize <= pSlotCount AND s`report(j)`Currency = c}")
        (("1" (SPLIT)
          (("1" (PROPAX) NIL NIL)
           ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL))
          NIL)
         ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL)
         ("3" (HIDE 2)
          (("3" (LEMMA "more_finite_sets[nat,nat].finite_image")
            (("3"
              (INST -1 "{j:nat | j <= 15}"
               "LAMBDA(n : {j:nat | j <= 15}) :s`report(n)`Currency")
              (("1" (EXPAND "is_finite")
                (("1" (SKOLEM -1 ("N" "f"))
                  (("1" (INST 1 "N" "f")
                    (("1" (EXPAND "injective?")
                      (("1" (SKOLEM 1 ("x1" "x2"))
                        (("1" (TYPEPRED "x1")
                          (("1" (TYPEPRED "x2")
                            (("1" (SKOLEM -1 "j1")
                              (("1"
                                (SKOLEM -2 "j2")
                                (("1"
                                  (INST -3 "x1" "x2")
                                  (("1"
                                    (INST 1 "j1")
                                    (("1" (GRIND) NIL NIL)
                                     ("2" (GRIND) NIL NIL))
                                    NIL)
                                   ("2"
                                    (INST 1 "j2")
                                    (("1" (GRIND) NIL NIL)
                                     ("2" (GRIND) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL)
                     ("2" (HIDE -1)
                      (("2" (SKOLEM 1 "y")
                        (("2" (GROUND)
                          (("1" (SKOLEM -1 "x")
                            (("1" (TYPEPRED "x")
                              (("1"
                                (INST 1 "x")
                                (("1" (GRIND) NIL NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (SKOLEM -1 "j")
                            (("2" (INST 1 "j")
                              (("1" (GRIND) NIL NIL)
                               ("2" (GRIND) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (HIDE 2)
                (("2" (EXPAND "is_finite")
                  (("2"
                    (INST 1 "16" "LAMBDA (n: {j: nat | j <= 15}) : n")
                    (("2" (GRIND) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|unused_indices_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|finite_unused_indices| "" (SKOLEM 1 "s")
  (("" (EXPAND* "is_finite" "unused_indices")
    (("" (INST 1 "pSlotCount" "LAMBDA(n : (unused_indices(s))) : n")
      (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL))
    NIL))
  NIL)
 (|finite_inuse_and_reported| "" (SKOLEM 1 "s")
  (("" (EXPAND "inuse_and_reported")
    (("" (EXPAND "is_finite")
      ((""
        (INST 1 "pSlotCount" "LAMBDA (n : {k: nat |
                     k < s`vSlotIndex AND
                      s`vSlotIndex <= pSlotCount AND
                       s`slotsReported(k) AND vSlots(k)`InUse}) : n")
        (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)
         ("3" (GRIND) NIL NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|allslots2_aux11| "" (LEMMA "invariant_rule")
  (("" (INST?)
    (("" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (HIDE 2)
        (("2" (SKOLEM 1 "r")
          (("2" (TYPEPRED "r")
            (("2" (BETA)
              (("2" (SPLIT)
                (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL)
                 ("2" (HIDE -2)
                  (("2" (SKOLEM 1 "n")
                    (("2" (TYPEPRED "n")
                      (("2" (FLATTEN) (("2" (GRIND) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|allslots2_aux10| "" (LEMMA "invariant_rule")
  (("" (INST?)
    (("" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (HIDE 2)
        (("2" (SKOLEM 1 "r")
          (("2" (TYPEPRED "r")
            (("2" (BETA)
              (("2" (SPLIT)
                (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL)
                 ("2" (HIDE -2)
                  (("2" (SKOLEM 1 "n")
                    (("2" (TYPEPRED "n")
                      (("2" (FLATTEN)
                        (("2" (GRIND)
                          (("2" (LEMMA "allslots2_aux11")
                            (("2" (GRIND) NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|allslots2_aux9_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|allslots2_aux9_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|allslots2_aux9| "" (LEMMA "invariant_rule")
  (("" (INST?)
    (("1" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (HIDE 2)
        (("2" (SKOLEM 1 "r")
          (("2" (TYPEPRED "r")
            (("2" (BETA)
              (("2" (SPLIT)
                (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL)
                 ("2" (HIDE -2)
                  (("2" (SKOLEM 1 "n")
                    (("2" (TYPEPRED "n")
                      (("2" (FLATTEN)
                        (("2" (SKOLEM 1 "i")
                          (("2" (EXPAND "run_fragment")
                            (("2" (INST -4 "n")
                              (("2"
                                (SPLIT)
                                (("1"
                                  (INST -1 "i")
                                  (("1" (GRIND) NIL NIL))
                                  NIL)
                                 ("2" (GRIND) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL)
     ("3" (HIDE 2) (("3" (GRIND) NIL NIL)) NIL))
    NIL))
  NIL)
 (|allslots2_aux8| "" (LEMMA "invariant_rule")
  (("" (INST?)
    (("1" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (HIDE 2)
        (("2" (SKOLEM 1 "r")
          (("2" (TYPEPRED "r")
            (("2" (BETA)
              (("2" (SPLIT)
                (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL)
                 ("2" (HIDE -2)
                  (("2" (SKOLEM 1 "n")
                    (("2" (TYPEPRED "n")
                      (("2" (FLATTEN)
                        (("2" (GRIND)
                          (("1"
                            (CASE "inuse_and_reported(r(n)) = inuse_and_reported(r(n) WITH [pc := CepSIQ_Reply_P2])")
                            (("1" (ASSERT) NIL NIL)
                             ("2" (APPLY-EXTENSIONALITY) NIL NIL))
                            NIL)
                           ("2"
                            (CASE "inuse_and_reported(r(n)) = inuse_and_reported(r(n) WITH [pc := CepSIQ_Reply_P2])")
                            (("1" (ASSERT) NIL NIL)
                             ("2" (EXPAND "inuse_and_reported")
                              (("2" (PROPAX) NIL NIL)) NIL))
                            NIL)
                           ("3" (HIDE 2 3 4)
                            (("3"
                              (HIDE -1 -3 -4 -5 -11 -12 -13 -14 -15)
                              (("3"
                                (NAME "s1" "inuse_and_reported(r(n))")
                                (("3"
                                  (NAME
                                   "s2"
                                   "inuse_and_reported(r(n)
                                                                                 WITH [pc := CepSIQ_Ready_P2,
                                                                                       slotsReported
                                                                                       := r(n)`slotsReported
                                                                                          WITH [(mSlotInfo(a!1)`SlotIndex)
                                                                                                := TRUE],
                                                                                       vSlotsReported
                                                                                       := 1 + r(n)`vSlotsReported,
                                                                                       reportSize
                                                                                       := 1
                                                                                          +
                                                                                          card(inuse_and_reported(r(n))),
                                                                                       report
                                                                                       := r(n)`report
                                                                                          WITH [(card
                                                                                                 (inuse_and_reported(r(n))))
                                                                                                (Currency)
                                                                                                := vSlots
                                                                                                   (mSlotInfo
                                                                                                    (a!1)`SlotIndex)`Currency,
                                                                                                (card
                                                                                                 (inuse_and_reported(r(n))))
                                                                                                (Balance)
                                                                                                := vSlots
                                                                                                   (mSlotInfo
                                                                                                    (a!1)`SlotIndex)`Balance,
                                                                                                (card
                                                                                                 (inuse_and_reported(r(n))))
                                                                                                (Status)
                                                                                                := x9000]])")
                                  (("1"
                                    (REPLACE -1)
                                    (("1"
                                      (REPLACE -2)
                                      (("1"
                                        (CASE
                                         "s2 = add(mSlotInfo(a!1)`SlotIndex,s1)")
                                        (("1"
                                          (HIDE -4 -6 -7 -8 -9 -10)
                                          (("1"
                                            (EXPAND
                                             "inuse_and_reported")
                                            (("1"
                                              (LEMMA
                                               "finite_sets[nat].card_add")
                                              (("1"
                                                (INST
                                                 -1
                                                 "s1"
                                                 "mSlotInfo(a!1)`SlotIndex")
                                                (("1"
                                                  (REPLACE -4 (-1) RL)
                                                  (("1"
                                                    (BETA)
                                                    (("1"
                                                      (ASSERT)
                                                      NIL
                                                      NIL))
                                                    NIL))
                                                  NIL)
                                                 ("2"
                                                  (LEMMA
                                                   "finite_inuse_and_reported")
                                                  (("2"
                                                    (INST -1 "r(n)")
                                                    (("2"
                                                      (EXPAND
                                                       "is_finite")
                                                      (("2"
                                                        (SKOLEM
                                                         -1
                                                         ("N" "f"))
                                                        (("2"
                                                          (INST
                                                           1
                                                           "N"
                                                           "f")
                                                          (("1"
                                                            (EXPAND
                                                             "injective?")
                                                            (("1"
                                                              (SKOLEM
                                                               1
                                                               ("x1"
                                                                "x2"))
                                                              (("1"
                                                                (INST
                                                                 -1
                                                                 "x1"
                                                                 "x2")
                                                                (("1"
                                                                  (TYPEPRED
                                                                   "x2")
                                                                  (("1"
                                                                    (REPLACE

                                                                     -4
                                                                     (-1)

                                                                     RL)
                                                                    (("1"
                                                                      (BETA)
                                                                      (("1"
                                                                        (PROPAX)
                                                                        NIL
                                                                        NIL))
                                                                      NIL))
                                                                    NIL))
                                                                  NIL)
                                                                 ("2"
                                                                  (TYPEPRED
                                                                   "x1")
                                                                  (("2"
                                                                    (REPLACE

                                                                     -4
                                                                     (-1)

                                                                     RL)
                                                                    (("2"
                                                                      (BETA)
                                                                      (("2"
                                                                        (PROPAX)
                                                                        NIL
                                                                        NIL))
                                                                      NIL))
                                                                    NIL))
                                                                  NIL))
                                                                NIL))
                                                              NIL))
                                                            NIL)
                                                           ("2"
                                                            (SKOLEM
                                                             1
                                                             "x1")
                                                            (("2"
                                                              (REPLACE

                                                               -4
                                                               (1)

                                                               RL)
                                                              (("2"
                                                                (BETA)
                                                                (("2"
                                                                  (GRIND)
                                                                  NIL
                                                                  NIL))
                                                                NIL))
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL)
                                         ("2"
                                          (HIDE 2 -3 -4 -5 -9)
                                          (("2"
                                            (EXPAND
                                             "inuse_and_reported")
                                            (("2"
                                              (NAME
                                               "m"
                                               "mSlotInfo(a!1)`SlotIndex")
                                              (("2"
                                                (REPLACE -1)
                                                (("2"
                                                  (HIDE -1)
                                                  (("2"
                                                    (EXPAND "add")
                                                    (("2"
                                                      (EXPAND "member")
                                                      (("2"
                                                        (APPLY-EXTENSIONALITY)
                                                        (("2"
                                                          (HIDE 2)
                                                          (("2"
                                                            (TYPEPRED
                                                             "x!1")
                                                            (("2"
                                                              (IFF)
                                                              (("2"
                                                                (GROUND)
                                                                (("1"
                                                                  (REPLACE

                                                                   -3
                                                                   (-1)

                                                                   RL)
                                                                  (("1"
                                                                    (BETA)
                                                                    (("1"
                                                                      (GRIND)
                                                                      (("1"
                                                                        (REPLACE

                                                                         -7
                                                                         (2)

                                                                         RL)
                                                                        (("1"
                                                                          (BETA)
                                                                          (("1"
                                                                            (GRIND)
                                                                            NIL
                                                                            NIL))
                                                                          NIL))
                                                                        NIL))
                                                                      NIL))
                                                                    NIL))
                                                                  NIL)
                                                                 ("2"
                                                                  (REPLACE

                                                                   -1
                                                                   (1)

                                                                   RL)
                                                                  (("2"
                                                                    (HIDE
                                                                     -1
                                                                     -2)
                                                                    (("2"
                                                                      (REPLACE

                                                                       -1
                                                                       (1)

                                                                       RL)
                                                                      (("2"
                                                                        (BETA)
                                                                        (("2"
                                                                          (GRIND)
                                                                          (("1"
                                                                            (REVEAL
                                                                             -6)
                                                                            (("1"
                                                                              (LEMMA
                                                                               "allslots2_aux11")
                                                                              (("1"
                                                                                (GRIND)
                                                                                NIL
                                                                                NIL))
                                                                              NIL))
                                                                            NIL)
                                                                           ("2"
                                                                            (REVEAL
                                                                             -6)
                                                                            (("2"
                                                                              (LEMMA
                                                                               "allslots2_aux11")
                                                                              (("2"
                                                                                (GRIND)
                                                                                NIL
                                                                                NIL))
                                                                              NIL))
                                                                            NIL))
                                                                          NIL))
                                                                        NIL))
                                                                      NIL))
                                                                    NIL))
                                                                  NIL)
                                                                 ("3"
                                                                  (REPLACE

                                                                   -3
                                                                   (1)

                                                                   RL)
                                                                  (("3"
                                                                    (REPLACE

                                                                     -4
                                                                     (-1)

                                                                     RL)
                                                                    (("3"
                                                                      (BETA)
                                                                      (("3"
                                                                        (GRIND)
                                                                        NIL
                                                                        NIL))
                                                                      NIL))
                                                                    NIL))
                                                                  NIL))
                                                                NIL))
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL)
                                   ("2"
                                    (LEMMA "finite_inuse_and_reported")
                                    (("2"
                                      (HIDE 2 -2 -3 -4 -5 -6 -7 -8 -9)
                                      (("2"
                                        (INST -1 "r(n)")
                                        (("2"
                                          (EXPAND "is_finite")
                                          (("2"
                                            (SKOLEM -1 ("N" "f"))
                                            (("2"
                                              (INST 1 "N" "f")
                                              (("2"
                                                (EXPAND "injective?")
                                                (("2"
                                                  (PROPAX)
                                                  NIL
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("4" (EXPAND "inuse_and_reported")
                            (("4" (LEMMA "finite_sets[nat].empty_card")
                              (("4"
                                (INST -1 "{k: nat | FALSE}")
                                (("1" (GRIND) NIL NIL)
                                 ("2"
                                  (INST
                                   1
                                   "0"
                                   "LAMBDA(n: {k: nat | FALSE}) : n")
                                  (("2" (GRIND) NIL NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("5"
                            (CASE "inuse_and_reported(r(n)) = inuse_and_reported(r(n)
                                                                                 WITH [pc := CepSlotInquirySequence_P2,
                                                                                       vSlotIndex := 1 + r(n)`vSlotIndex,
                                                                                       slotsReported
                                                                                       := r(n)`slotsReported
                                                                                          WITH [(r(n)`vSlotIndex)
                                                                                                := FALSE]])")
                            (("1" (ASSERT) NIL NIL)
                             ("2" (EXPAND "inuse_and_reported")
                              (("2"
                                (APPLY-EXTENSIONALITY)
                                (("1" (GRIND) NIL NIL)
                                 ("2" (GRIND) NIL NIL)
                                 ("3" (GRIND) NIL NIL)
                                 ("4" (GRIND) NIL NIL)
                                 ("5" (GRIND) NIL NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("6"
                            (CASE "inuse_and_reported(r(n)) = inuse_and_reported(r(n)
                                                                                 WITH [pc := CepSlotInquirySequence_P2,
                                                                                       vSlotIndex := 1 + r(n)`vSlotIndex,
                                                                                       vSlotsReported
                                                                                       := 1 + r(n)`vSlotsReported,
                                                                                       slotsReported
                                                                                       := r(n)`slotsReported
                                                                                          WITH [(r(n)`vSlotIndex)
                                                                                                := TRUE]])")
                            (("1" (ASSERT) NIL NIL)
                             ("2" (APPLY-EXTENSIONALITY)
                              (("2" (GRIND) NIL NIL)) NIL))
                            NIL)
                           ("7" (EXPAND "inuse_and_reported")
                            (("7" (LEMMA "finite_sets[nat].empty_card")
                              (("7"
                                (INST -1 "{k: nat | FALSE}")
                                (("1" (GRIND) NIL NIL)
                                 ("2"
                                  (INST
                                   1
                                   "0"
                                   "LAMBDA(n: nat | FALSE) : n")
                                  (("2" (GRIND) NIL NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (HIDE 2)
      (("2" (GRIND)
        (("1"
          (INST 1 "pSlotCount"
           "LAMBDA(n : (inuse_and_reported(s!1))) : n")
          (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)
         ("2"
          (INST 1 "pSlotCount"
           "LAMBDA(n : (inuse_and_reported(s!1))) : n")
          (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)
         ("3"
          (INST 1 "pSlotCount"
           "LAMBDA(n : (inuse_and_reported(s!1))) : n")
          (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|allslots2_aux7| "" (LEMMA "invariant_rule")
  (("" (INST?)
    (("1" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (HIDE 2)
        (("2" (SKOLEM 1 "r")
          (("2" (TYPEPRED "r")
            (("2" (BETA)
              (("2" (SPLIT)
                (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL)
                 ("2" (HIDE -2)
                  (("2" (SKOLEM 1 "n")
                    (("2" (TYPEPRED "n")
                      (("2" (FLATTEN)
                        (("2" (GRIND)
                          (("1"
                            (CASE "inuse_and_reported(r(n) WITH [pc := CepSIQ_Reply_P2]) = inuse_and_reported(r(n))")
                            (("1" (REPLACE -1)
                              (("1"
                                (CASE
                                 "unused_indices(r(n) WITH [pc := CepSIQ_Reply_P2]) = unused_indices(r(n))")
                                (("1"
                                  (REPLACE -1)
                                  (("1" (PROPAX) NIL NIL))
                                  NIL)
                                 ("2"
                                  (EXPAND "unused_indices")
                                  (("2" (PROPAX) NIL NIL))
                                  NIL))
                                NIL))
                              NIL)
                             ("2" (EXPAND "inuse_and_reported")
                              (("2" (PROPAX) NIL NIL)) NIL))
                            NIL)
                           ("2"
                            (CASE "unused_indices(r(n) WITH [pc := CepSIQ_Reply_P2]) = unused_indices(r(n))")
                            (("1"
                              (CASE "inuse_and_reported(r(n) WITH [pc := CepSIQ_Reply_P2]) = inuse_and_reported(r(n))")
                              (("1" (REPLACE*) NIL NIL)
                               ("2"
                                (EXPAND "inuse_and_reported")
                                (("2" (PROPAX) NIL NIL))
                                NIL))
                              NIL)
                             ("2" (EXPAND "unused_indices")
                              (("2" (PROPAX) NIL NIL)) NIL))
                            NIL)
                           ("3"
                            (HIDE -1 -3 -4 -5 -11 -12 -13 -14 -16 2 3
                             4)
                            (("3"
                              (NAME "s1" "inuse_and_reported(r(n)
                                                                                                WITH [pc := CepSIQ_Ready_P2,
                                                                                                      slotsReported
                                                                                                      := r(n)`slotsReported
                                                                                                         WITH [(mSlotInfo(a!1)`SlotIndex)
                                                                                                               := TRUE],
                                                                                                      vSlotsReported
                                                                                                      := 1 + r(n)`vSlotsReported,
                                                                                                      reportSize := 1 + r(n)`reportSize,
                                                                                                      report
                                                                                                      := r(n)`report
                                                                                                         WITH [(r(n)`reportSize)(Currency)
                                                                                                               := vSlots
                                                                                                                  (mSlotInfo
                                                                                                                   (a!1)`SlotIndex)`Currency,
                                                                                                               (r(n)`reportSize)(Balance)
                                                                                                               := vSlots
                                                                                                                  (mSlotInfo
                                                                                                                   (a!1)`SlotIndex)`Balance,
                                                                                                               (r(n)`reportSize)(Status)
                                                                                                               := x9000]])")
                              (("3"
                                (REPLACE -1)
                                (("3"
                                  (NAME
                                   "s2"
                                   "unused_indices(r(n)
                                                                                             WITH [pc := CepSIQ_Ready_P2,
                                                                                                   slotsReported
                                                                                                     := r(n)`slotsReported
                                                                                                        WITH [(mSlotInfo(a!1)`SlotIndex)
                                                                                                              := TRUE],
                                                                                                   vSlotsReported
                                                                                                     := 1 + r(n)`vSlotsReported,
                                                                                                   reportSize := 1 + r(n)`reportSize,
                                                                                                   report
                                                                                                     := r(n)`report
                                                                                                        WITH [(r(n)`reportSize)(Currency)
                                                                                                              := vSlots
                                                                                                                 (mSlotInfo
                                                                                                                  (a!1)`SlotIndex)`Currency,
                                                                                                              (r(n)`reportSize)(Balance)
                                                                                                              := vSlots
                                                                                                                 (mSlotInfo
                                                                                                                  (a!1)`SlotIndex)`Balance,
                                                                                                              (r(n)`reportSize)(Status)
                                                                                                              := x9000]])")
                                  (("3"
                                    (REPLACE -1)
                                    (("3"
                                      (NAME
                                       "m"
                                       "mSlotInfo(a!1)`SlotIndex")
                                      (("3"
                                        (REPLACE -1)
                                        (("3"
                                          (HIDE -1)
                                          (("3"
                                            (CASE
                                             "s1 = add(mSlotInfo(a!1)`SlotIndex,inuse_and_reported(r(n)))")
                                            (("1"
                                              (REVEAL -1)
                                              (("1"
                                                (REPLACE -1)
                                                (("1"
                                                  (HIDE -1)
                                                  (("1"
                                                    (CASE
                                                     "unused_indices(r(n)) = unused_indices(r(n)
                                                                                               WITH [pc := CepSIQ_Ready_P2,
                                                                                                     slotsReported
                                                                                                       := r(n)`slotsReported WITH [(m) := TRUE],
                                                                                                     vSlotsReported := 1 + r(n)`vSlotsReported,
                                                                                                     reportSize := 1 + r(n)`reportSize,
                                                                                                     report
                                                                                                       := r(n)`report
                                                                                                            WITH [(r(n)`reportSize)(Currency)
                                                                                                                  := vSlots(m)`Currency,
                                                                                                                  (r(n)`reportSize)(Balance)
                                                                                                                  := vSlots(m)`Balance,
                                                                                                                  (r(n)`reportSize)(Status)
                                                                                                                  := x9000]])")
                                                    (("1"
                                                      (REPLACE

                                                       -1
                                                       (-3)

                                                       RL)
                                                      (("1"
                                                        (REPLACE -3)
                                                        (("1"
                                                          (REPLACE -2)
                                                          (("1"
                                                            (LEMMA
                                                             "finite_sets[nat].card_add")
                                                            (("1"
                                                              (INST
                                                               -1
                                                               "inuse_and_reported(r(n))"
                                                               "m")
                                                              (("1"
                                                                (GROUND)
                                                                NIL
                                                                NIL)
                                                               ("2"
                                                                (LEMMA
                                                                 "finite_inuse_and_reported")
                                                                (("2"
                                                                  (INST
                                                                   -1
                                                                   "r(n)")
                                                                  (("2"
                                                                    (EXPAND
                                                                     "is_finite")
                                                                    (("2"
                                                                      (SKOLEM
                                                                       -1
                                                                       ("N"
                                                                        "f"))
                                                                      (("2"
                                                                        (INST
                                                                         1
                                                                         "N"
                                                                         "f")
                                                                        (("2"
                                                                          (EXPAND
                                                                           "injective?")
                                                                          (("2"
                                                                            (PROPAX)
                                                                            NIL
                                                                            NIL))
                                                                          NIL))
                                                                        NIL))
                                                                      NIL))
                                                                    NIL))
                                                                  NIL))
                                                                NIL))
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL)
                                                     ("2"
                                                      (EXPAND
                                                       "unused_indices")
                                                      (("2"
                                                        (PROPAX)
                                                        NIL
                                                        NIL))
                                                      NIL)
                                                     ("3"
                                                      (ASSERT)
                                                      NIL
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL)
                                             ("2"
                                              (EXPAND*
                                               "unused_indices"
                                               "inuse_and_reported")
                                              (("2"
                                                (EXPAND*
                                                 "add"
                                                 "member")
                                                (("2"
                                                  (APPLY-EXTENSIONALITY)
                                                  (("1"
                                                    (REPLACE -2 (1) RL)
                                                    (("1"
                                                      (BETA)
                                                      (("1"
                                                        (REVEAL -2)
                                                        (("1"
                                                          (GRIND)
                                                          (("1"
                                                            (LEMMA
                                                             "allslots2_aux11")
                                                            (("1"
                                                              (GRIND)
                                                              NIL
                                                              NIL))
                                                            NIL)
                                                           ("2"
                                                            (LEMMA
                                                             "allslots2_aux11")
                                                            (("2"
                                                              (GRIND)
                                                              NIL
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL)
                                                   ("2"
                                                    (GRIND)
                                                    NIL
                                                    NIL)
                                                   ("3"
                                                    (GRIND)
                                                    NIL
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("4"
                            (EXPAND* "inuse_and_reported"
                             "unused_indices")
                            (("4" (LEMMA "finite_sets[nat].empty_card")
                              (("4"
                                (INST -1 "{k: nat | FALSE}")
                                (("1" (GRIND) NIL NIL)
                                 ("2"
                                  (INST
                                   1
                                   "0"
                                   "LAMBDA (n : nat | FALSE) : n")
                                  (("2" (GRIND) NIL NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("5" (NAME "m" "r(n)`vSlotIndex")
                            (("5" (REPLACE -1)
                              (("5"
                                (HIDE -1)
                                (("5"
                                  (NAME
                                   "s1"
                                   "inuse_and_reported(r(n)
                                                                                                WITH [pc := CepSlotInquirySequence_P2,
                                                                                                      vSlotIndex := 1 + m,
                                                                                                      slotsReported
                                                                                                      := r(n)`slotsReported
                                                                                                         WITH [(m) := FALSE]])")
                                  (("1"
                                    (NAME
                                     "s2"
                                     "unused_indices(r(n)
                                                                                                     WITH [pc := CepSlotInquirySequence_P2,
                                                                                                           vSlotIndex := 1 + m,
                                                                                                           slotsReported
                                                                                                             := r(n)`slotsReported
                                                                                                                WITH [(m) := FALSE]])")
                                    (("1"
                                      (REPLACE -1)
                                      (("1"
                                        (REPLACE -2)
                                        (("1"
                                          (CASE
                                           "union(s1,s2) = union(inuse_and_reported(r(n)) , unused_indices(r(n)))")
                                          (("1"
                                            (LEMMA
                                             "finite_sets[nat].card_disj_union")
                                            (("1"
                                              (INST-CP -1 "s1" "s2")
                                              (("1"
                                                (INST
                                                 -1
                                                 "inuse_and_reported(r(n))"
                                                 "unused_indices(r(n))")
                                                (("1"
                                                  (GROUND)
                                                  (("1"
                                                    (EXPAND*
                                                     "disjoint?"
                                                     "member")
                                                    (("1"
                                                      (EXPAND*
                                                       "empty?"
                                                       "intersection"
                                                       "member")
                                                      (("1"
                                                        (REWRITE
                                                         "forall_not")
                                                        (("1"
                                                          (SKOLEM
                                                           -1
                                                           "x")
                                                          (("1"
                                                            (REPLACE

                                                             -4
                                                             (-1)

                                                             RL)
                                                            (("1"
                                                              (REPLACE

                                                               -5
                                                               (-1)

                                                               RL)
                                                              (("1"
                                                                (GRIND)
                                                                NIL
                                                                NIL))
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL)
                                                   ("2"
                                                    (EXPAND*
                                                     "disjoint?"
                                                     "empty"
                                                     "intersection"
                                                     "member")
                                                    (("2"
                                                      (EXPAND*
                                                       "empty?"
                                                       "member")
                                                      (("2"
                                                        (REWRITE
                                                         "forall_not")
                                                        (("2"
                                                          (SKOLEM
                                                           -2
                                                           "x")
                                                          (("2"
                                                            (EXPAND*
                                                             "inuse_and_reported"
                                                             "unused_indices")
                                                            (("2"
                                                              (GROUND)
                                                              NIL
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL)
                                                   ("3"
                                                    (EXPAND*
                                                     "inuse_and_reported"
                                                     "unused_indices")
                                                    (("3"
                                                      (EXPAND*
                                                       "disjoint?"
                                                       "empty?"
                                                       "intersection"
                                                       "member")
                                                      (("3"
                                                        (REWRITE
                                                         "forall_not")
                                                        (("3"
                                                          (SKOLEM
                                                           -1
                                                           "x")
                                                          (("3"
                                                            (REPLACE

                                                             -4
                                                             (-1)

                                                             RL)
                                                            (("3"
                                                              (REPLACE

                                                               -3
                                                               (-1)

                                                               RL)
                                                              (("3"
                                                                (GRIND)
                                                                NIL
                                                                NIL))
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL)
                                                 ("2"
                                                  (LEMMA
                                                   "finite_unused_indices")
                                                  (("2"
                                                    (INST -1 "r(n)")
                                                    (("2"
                                                      (EXPAND
                                                       "is_finite")
                                                      (("2"
                                                        (SKOLEM
                                                         -1
                                                         ("N" "f"))
                                                        (("2"
                                                          (INST
                                                           1
                                                           "N"
                                                           "f")
                                                          (("2"
                                                            (EXPAND
                                                             "injective?")
                                                            (("2"
                                                              (PROPAX)
                                                              NIL
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL)
                                                 ("3"
                                                  (LEMMA
                                                   "finite_inuse_and_reported")
                                                  (("3"
                                                    (INST -1 "r(n)")
                                                    (("3"
                                                      (EXPAND
                                                       "is_finite")
                                                      (("3"
                                                        (SKOLEM
                                                         -1
                                                         ("N" "f"))
                                                        (("3"
                                                          (INST
                                                           1
                                                           "N"
                                                           "f")
                                                          (("3"
                                                            (EXPAND
                                                             "injective?")
                                                            (("3"
                                                              (PROPAX)
                                                              NIL
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL)
                                               ("2"
                                                (INST
                                                 1
                                                 "pSlotCount"
                                                 "LAMBDA(n: (s2)) : n")
                                                (("1"
                                                  (SKOLEM
                                                   1
                                                   ("x1" "x2"))
                                                  (("1"
                                                    (TYPEPRED "x1")
                                                    (("1"
                                                      (TYPEPRED "x2")
                                                      (("1"
                                                        (BETA)
                                                        (("1"
                                                          (FLATTEN)
                                                          NIL
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL)
                                                 ("2"
                                                  (GRIND)
                                                  (("2"
                                                    (REPLACE

                                                     -3
                                                     (-1)

                                                     RL)
                                                    (("2"
                                                      (ASSERT)
                                                      NIL
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL)
                                               ("3"
                                                (INST
                                                 1
                                                 "pSlotCount"
                                                 "LAMBDA(n: (s1)) : n")
                                                (("1"
                                                  (SKOLEM
                                                   1
                                                   ("x1" "x2"))
                                                  (("1"
                                                    (BETA)
                                                    (("1"
                                                      (FLATTEN)
                                                      NIL
                                                      NIL))
                                                    NIL))
                                                  NIL)
                                                 ("2"
                                                  (SKOLEM 1 "w")
                                                  (("2"
                                                    (TYPEPRED "w")
                                                    (("2"
                                                      (REPLACE

                                                       -4
                                                       (-1)

                                                       RL)
                                                      (("2"
                                                        (GRIND)
                                                        NIL
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL)
                                           ("2"
                                            (REPLACE -2 (1) RL)
                                            (("2"
                                              (REPLACE -1 (1) RL)
                                              (("2"
                                                (EXPAND*
                                                 "inuse_and_reported"
                                                 "unused_indices")
                                                (("2"
                                                  (EXPAND*
                                                   "union"
                                                   "member")
                                                  (("2"
                                                    (APPLY-EXTENSIONALITY)
                                                    (("1"
                                                      (CASE
                                                       "CepSlotInquirySequence_P2?(r(n)`pc)")
                                                      (("1"
                                                        (IFF)
                                                        (("1"
                                                          (LEMMA
                                                           "allslots2_aux10")
                                                          (("1"
                                                            (GRIND)
                                                            (("1"
                                                              (REVEAL
                                                               -3)
                                                              (("1"
                                                                (ASSERT)
                                                                NIL
                                                                NIL))
                                                              NIL)
                                                             ("2"
                                                              (REVEAL
                                                               -3)
                                                              (("2"
                                                                (ASSERT)
                                                                NIL
                                                                NIL))
                                                              NIL)
                                                             ("3"
                                                              (REVEAL
                                                               -3)
                                                              (("3"
                                                                (ASSERT)
                                                                NIL
                                                                NIL))
                                                              NIL)
                                                             ("4"
                                                              (REVEAL
                                                               -3)
                                                              (("4"
                                                                (ASSERT)
                                                                NIL
                                                                NIL))
                                                              NIL)
                                                             ("5"
                                                              (REVEAL
                                                               -3)
                                                              (("5"
                                                                (ASSERT)
                                                                NIL
                                                                NIL))
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL)
                                                       ("2"
                                                        (ASSERT)
                                                        NIL
                                                        NIL))
                                                      NIL)
                                                     ("2"
                                                      (GRIND)
                                                      NIL
                                                      NIL)
                                                     ("3"
                                                      (GRIND)
                                                      NIL
                                                      NIL)
                                                     ("4"
                                                      (GRIND)
                                                      NIL
                                                      NIL)
                                                     ("5"
                                                      (GRIND)
                                                      NIL
                                                      NIL)
                                                     ("6"
                                                      (GRIND)
                                                      NIL
                                                      NIL)
                                                     ("7"
                                                      (GRIND)
                                                      NIL
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL)
                                   ("2" (ASSERT) NIL NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("6"
                            (CASE "CepSlotInquirySequence_P2?(r(n)`pc)")
                            (("1" (HIDE 2 3 4 5 6 7)
                              (("1"
                                (HIDE -2 -4 -5 -7 -8)
                                (("1"
                                  (NAME "m" "r(n)`vSlotIndex")
                                  (("1"
                                    (REPLACE -1)
                                    (("1"
                                      (HIDE -1)
                                      (("1"
                                        (NAME
                                         "s1"
                                         "inuse_and_reported(r(n)
                                                                                                        WITH [pc := CepSlotInquirySequence_P2,
                                                                                                              vSlotIndex := 1 + m,
                                                                                                              vSlotsReported
                                                                                                              := 1 + r(n)`vSlotsReported,
                                                                                                              slotsReported
                                                                                                              := r(n)`slotsReported
                                                                                                                 WITH [(m) := TRUE]])")
                                        (("1"
                                          (REPLACE -1)
                                          (("1"
                                            (NAME
                                             "s2"
                                             "unused_indices(r(n)
                                                                                                             WITH [pc := CepSlotInquirySequence_P2,
                                                                                                                   vSlotIndex := 1 + m,
                                                                                                                   vSlotsReported
                                                                                                                     := 1 + r(n)`vSlotsReported,
                                                                                                                   slotsReported
                                                                                                                     := r(n)`slotsReported
                                                                                                                        WITH [(m) := TRUE]])")
                                            (("1"
                                              (REPLACE -1)
                                              (("1"
                                                (REVEAL -1)
                                                (("1"
                                                  (CASE
                                                   "empty?(inuse_and_reported(r(n)))")
                                                  (("1"
                                                    (CASE "empty?(s1)")
                                                    (("1"
                                                      (LEMMA
                                                       "finite_sets[nat].empty_card")
                                                      (("1"
                                                        (INST-CP
                                                         -1
                                                         "inuse_and_reported(r(n))")
                                                        (("1"
                                                          (INST
                                                           -1
                                                           "s1")
                                                          (("1"
                                                            (BDDSIMP)
                                                            (("1"
                                                              (REPLACE*)
                                                              (("1"
                                                                (SIMPLIFY)
                                                                (("1"
                                                                  (CASE
                                                                   "s2 = add(m,unused_indices(r(n)))")
                                                                  (("1"
                                                                    (LEMMA
                                                                     "finite_sets[nat].card_add")
                                                                    (("1"
                                                                      (INST
                                                                       -1
                                                                       "unused_indices(r(n))"
                                                                       "m")
                                                                      (("1"
                                                                        (REPLACE

                                                                         -2
                                                                         (-1)

                                                                         RL)
                                                                        (("1"
                                                                          (REPLACE

                                                                           -1)
                                                                          (("1"
                                                                            (REPLACE

                                                                             -11)
                                                                            (("1"
                                                                              (SIMPLIFY)
                                                                              (("1"
                                                                                (EXPAND
                                                                                 "unused_indices")
                                                                                (("1"
                                                                                  (GRIND)
                                                                                  NIL
                                                                                  NIL))
                                                                                NIL))
                                                                              NIL))
                                                                            NIL))
                                                                          NIL))
                                                                        NIL)
                                                                       ("2"
                                                                        (LEMMA
                                                                         "finite_unused_indices")
                                                                        (("2"
                                                                          (GRIND)
                                                                          NIL
                                                                          NIL))
                                                                        NIL))
                                                                      NIL))
                                                                    NIL)
                                                                   ("2"
                                                                    (REPLACE

                                                                     -6
                                                                     (1)

                                                                     RL)
                                                                    (("2"
                                                                      (EXPAND
                                                                       "unused_indices")
                                                                      (("2"
                                                                        (EXPAND*
                                                                         "add"
                                                                         "member")
                                                                        (("2"
                                                                          (APPLY-EXTENSIONALITY)
                                                                          (("1"
                                                                            (GRIND)
                                                                            NIL
                                                                            NIL)
                                                                           ("2"
                                                                            (GRIND)
                                                                            NIL
                                                                            NIL)
                                                                           ("3"
                                                                            (GRIND)
                                                                            NIL
                                                                            NIL))
                                                                          NIL))
                                                                        NIL))
                                                                      NIL))
                                                                    NIL))
                                                                  NIL))
                                                                NIL))
                                                              NIL))
                                                            NIL)
                                                           ("2"
                                                            (INST
                                                             1
                                                             "0"
                                                             "LAMBDA (x : (s1)) : x")
                                                            (("1"
                                                              (SKOLEM
                                                               1
                                                               ("x1"
                                                                "x2"))
                                                              (("1"
                                                                (BETA)
                                                                (("1"
                                                                  (FLATTEN)
                                                                  NIL
                                                                  NIL))
                                                                NIL))
                                                              NIL)
                                                             ("2"
                                                              (SKOLEM
                                                               1
                                                               "x")
                                                              (("2"
                                                                (TYPEPRED
                                                                 "x")
                                                                (("2"
                                                                  (EXPAND
                                                                   "empty?"
                                                                   -3)
                                                                  (("2"
                                                                    (INST
                                                                     -3
                                                                     "x")
                                                                    (("2"
                                                                      (EXPAND
                                                                       "member")
                                                                      (("2"
                                                                        (PROPAX)
                                                                        NIL
                                                                        NIL))
                                                                      NIL))
                                                                    NIL))
                                                                  NIL))
                                                                NIL))
                                                              NIL))
                                                            NIL))
                                                          NIL)
                                                         ("2"
                                                          (LEMMA
                                                           "finite_inuse_and_reported")
                                                          (("2"
                                                            (GRIND)
                                                            NIL
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL)
                                                     ("2"
                                                      (EXPAND*
                                                       "empty?"
                                                       "member")
                                                      (("2"
                                                        (SKOLEM 1 "x")
                                                        (("2"
                                                          (INST -2 "x")
                                                          (("2"
                                                            (REPLACE

                                                             -4
                                                             (-1)

                                                             RL)
                                                            (("2"
                                                              (EXPAND
                                                               "inuse_and_reported")
                                                              (("2"
                                                                (GRIND)
                                                                NIL
                                                                NIL))
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL)
                                                   ("2"
                                                    (LEMMA
                                                     "allslots2_aux9")
                                                    (("2"
                                                      (GRIND)
                                                      NIL
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL)
                                         ("2" (ASSERT) NIL NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL)
                             ("2" (ASSERT) NIL NIL))
                            NIL)
                           ("7"
                            (EXPAND* "inuse_and_reported"
                             "unused_indices")
                            (("7" (LEMMA "finite_sets[nat].empty_card")
                              (("7"
                                (INST -1 "{k: nat | FALSE}")
                                (("1" (GRIND) NIL NIL)
                                 ("2"
                                  (INST
                                   1
                                   "0"
                                   "LAMBDA (n : nat | FALSE) : n")
                                  (("2" (GRIND) NIL NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (HIDE 2)
      (("2" (LEMMA "finite_inuse_and_reported") (("2" (GRIND) NIL NIL))
        NIL))
      NIL)
     ("3" (HIDE 2)
      (("3" (LEMMA "finite_unused_indices") (("3" (GRIND) NIL NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|allslots2_aux6| "" (EXPAND "invariant")
  (("" (SKOLEM 1 ("r" "n"))
    (("" (GROUND)
      (("" (REPLACE -1)
        (("" (NAME "s" "r(n)")
          (("" (REPLACE -1)
            (("" (HIDE -1)
              (("" (LEMMA "finite_sets[nat].card_disj_union")
                (("" (INST -1 "unused_indices(s)" "used_indices")
                  (("1" (PROP)
                    (("1" (REPLACE -1 (1) RL)
                      (("1" (HIDE -1)
                        (("1"
                          (CASE "union(unused_indices(s), used_indices) = {x: nat | x  < pSlotCount}")
                          (("1" (REPLACE -1)
                            (("1"
                              (LEMMA "finite_sets_nat.card_bounded")
                              (("1" (INST -1 "pSlotCount") NIL NIL))
                              NIL))
                            NIL)
                           ("2"
                            (EXPAND* "unused_indices" "used_indices"
                             "union" "member")
                            (("2" (APPLY-EXTENSIONALITY)
                              (("1" (GRIND) NIL NIL)
                               ("2" (GRIND) NIL NIL)
                               ("3" (GRIND) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL)
                     ("2"
                      (EXPAND* "unused_indices" "used_indices"
                       "disjoint?" "member")
                      (("2" (EXPAND* "empty?" "intersection" "member")
                        (("2" (GRIND) NIL NIL)) NIL))
                      NIL))
                    NIL)
                   ("2" (LEMMA "finite_unused_indices")
                    (("2" (INST -1 "s") NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|allslots2_aux5| "" (LEMMA "allslots2_aux10")
  (("" (EXPAND "invariant")
    (("" (SKOLEM 1 ("r" "n"))
      (("" (INST -1 "r" "n")
        (("" (LEMMA "allslots2_aux11")
          (("" (EXPAND "invariant")
            (("" (INST?)
              (("" (LEMMA "allslots2_aux7")
                (("" (LEMMA "allslots2_aux8")
                  (("" (EXPAND "invariant")
                    (("" (INST?)
                      (("" (INST?)
                        (("" (LEMMA "allslots2_aux6")
                          (("" (EXPAND "invariant")
                            (("" (INST?)
                              ((""
                                (EXPAND*
                                 "inuse_and_reported"
                                 "used_indices"
                                 "unused_indices")
                                (("" (GRIND) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|allslots2_aux4| "" (LEMMA "allslots2_aux5")
  (("" (EXPAND "invariant")
    (("" (SKOLEM 1 ("r" "n"))
      (("" (INST?)
        (("" (FLATTEN)
          ((""
            (NAME "c"
                  "(r(n)`pc = CepSIQ_Reply_P2 OR r(n)`pc = CepSIQ_Ready_P2 OR r(n)`pc = CepSlotInquirySequence_P2)")
            (("" (REPLACE -1)
              (("" (HIDE -1)
                (("" (GROUND)
                  (("" (HIDE -2 -3)
                    (("" (NAME "s" "r(n)")
                      (("" (REPLACE -1)
                        (("" (HIDE -1)
                          (("" (CASE "s`reportSize =0")
                            (("1" (REPLACE -1)
                              (("1"
                                (LEMMA "finite_sets[nat].empty_card")
                                (("1"
                                  (INST-CP -1 "used_indices")
                                  (("1"
                                    (GROUND)
                                    (("1"
                                      (INST -3 "used_currencies")
                                      (("1"
                                        (GROUND)
                                        (("1"
                                          (HIDE -2 -3 -4 1 3)
                                          (("1"
                                            (EXPAND* "empty?" "member")
                                            (("1"
                                              (REWRITE "forall_not")
                                              (("1"
                                                (REWRITE "forall_not")
                                                (("1"
                                                  (EXPAND*
                                                   "used_indices"
                                                   "used_currencies")
                                                  (("1"
                                                    (SKOLEM -1 "cc")
                                                    (("1"
                                                      (SKOLEM -1 "j")
                                                      (("1"
                                                        (TYPEPRED "j")
                                                        (("1"
                                                          (EXPAND
                                                           "used_indices")
                                                          (("1"
                                                            (INST
                                                             1
                                                             "j")
                                                            NIL
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL)
                             ("2" (GROUND)
                              (("2"
                                (LEMMA
                                 "more_finite_sets[(used_indices),nat].inverse_bijection")
                                (("1"
                                  (NAME
                                   F
                                   "LAMBDA (n : (used_indices)) : vSlots(n)`Currency")
                                  (("1"
                                    (INST -2 "F")
                                    (("1"
                                      (BETA)
                                      (("1"
                                        (SPLIT)
                                        (("1"
                                          (LEMMA
                                           "finite_sets_card_eq[nat,nat].card_eq_bij")
                                          (("1"
                                            (INST
                                             -1
                                             "{y: nat | EXISTS (x: ((used_indices))): y = F(x)}"
                                             "used_indices")
                                            (("1"
                                              (GROUND)
                                              (("1"
                                                (REPLACE*)
                                                (("1"
                                                  (EXPAND
                                                   "used_currencies")
                                                  (("1"
                                                    (HIDE -2 -3 1)
                                                    (("1"
                                                      (REPLACE

                                                       -1
                                                       (1)

                                                       RL)
                                                      (("1"
                                                        (HIDE -1)
                                                        (("1"
                                                          (CASE
                                                           "{c: nat | EXISTS (j: (used_indices)): vSlots(j)`Currency = c} = {y: nat | EXISTS (x: ((used_indices))): y = F(x)}")
                                                          (("1"
                                                            (ASSERT)
                                                            NIL
                                                            NIL)
                                                           ("2"
                                                            (HIDE 2)
                                                            (("2"
                                                              (APPLY-EXTENSIONALITY)
                                                              (("1"
                                                                (HIDE
                                                                 2)
                                                                (("1"
                                                                  (IFF)
                                                                  (("1"
                                                                    (GROUND)
                                                                    (("1"
                                                                      (SKOLEM
                                                                       -1
                                                                       "j")
                                                                      (("1"
                                                                        (INST
                                                                         1
                                                                         "j")
                                                                        (("1"
                                                                          (TYPEPRED
                                                                           "j")
                                                                          (("1"
                                                                            (EXPAND
                                                                             "used_indices")
                                                                            (("1"
                                                                              (REPLACE

                                                                               -2
                                                                               (1)

                                                                               RL)
                                                                              (("1"
                                                                                (REPLACE

                                                                                 -3
                                                                                 (1)

                                                                                 RL)
                                                                                (("1"
                                                                                  (BETA)
                                                                                  (("1"
                                                                                    (PROPAX)
                                                                                    NIL
                                                                                    NIL))
                                                                                  NIL))
                                                                                NIL))
                                                                              NIL))
                                                                            NIL))
                                                                          NIL))
                                                                        NIL))
                                                                      NIL)
                                                                     ("2"
                                                                      (SKOLEM
                                                                       -1
                                                                       "x")
                                                                      (("2"
                                                                        (INST
                                                                         1
                                                                         "x")
                                                                        (("2"
                                                                          (REPLACE

                                                                           -1)
                                                                          (("2"
                                                                            (REPLACE

                                                                             -2
                                                                             (1)

                                                                             RL)
                                                                            (("2"
                                                                              (BETA)
                                                                              (("2"
                                                                                (PROPAX)
                                                                                NIL
                                                                                NIL))
                                                                              NIL))
                                                                            NIL))
                                                                          NIL))
                                                                        NIL))
                                                                      NIL))
                                                                    NIL))
                                                                  NIL))
                                                                NIL)
                                                               ("2"
                                                                (GRIND
                                                                 :IF-MATCH
                                                                 NIL)
                                                                NIL
                                                                NIL))
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL)
                                               ("2"
                                                (INST?)
                                                (("2"
                                                  (SKOLEM 1 "y")
                                                  (("2"
                                                    (LEMMA
                                                     "finite_sets[nat].nonempty_card")
                                                    (("2"
                                                      (INST
                                                       -1
                                                       "used_indices")
                                                      (("2"
                                                        (GROUND)
                                                        (("2"
                                                          (EXPAND*
                                                           "nonempty?"
                                                           "empty?"
                                                           "member")
                                                          (("2"
                                                            (REWRITE
                                                             "forall_not")
                                                            (("2"
                                                              (SKOLEM
                                                               -1
                                                               "x")
                                                              (("2"
                                                                (INST
                                                                 1
                                                                 "x")
                                                                NIL
                                                                NIL))
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL)
                                             ("2"
                                              (LEMMA
                                               "finite_used_currencies")
                                              (("2"
                                                (EXPAND
                                                 "used_currencies")
                                                (("2"
                                                  (REPLACE -3 (1) RL)
                                                  (("2"
                                                    (BETA)
                                                    (("2"
                                                      (HIDE
                                                       -2
                                                       -3
                                                       -4
                                                       2
                                                       3)
                                                      (("2"
                                                        (CASE
                                                         "{c: nat | EXISTS (j: (used_indices)): vSlots(j)`Currency = c} = {y: nat | EXISTS (x: ((used_indices))): y = vSlots(x)`Currency}")
                                                        (("1"
                                                          (ASSERT)
                                                          NIL
                                                          NIL)
                                                         ("2"
                                                          (APPLY-EXTENSIONALITY)
                                                          (("1"
                                                            (IFF)
                                                            (("1"
                                                              (PROP)
                                                              (("1"
                                                                (SKOLEM
                                                                 -1
                                                                 "j")
                                                                (("1"
                                                                  (INST
                                                                   1
                                                                   "j")
                                                                  (("1"
                                                                    (TYPEPRED
                                                                     "j")
                                                                    (("1"
                                                                      (ASSERT)
                                                                      NIL
                                                                      NIL))
                                                                    NIL))
                                                                  NIL))
                                                                NIL)
                                                               ("2"
                                                                (SKOLEM
                                                                 -1
                                                                 "j")
                                                                (("2"
                                                                  (INST
                                                                   1
                                                                   "j")
                                                                  (("2"
                                                                    (ASSERT)
                                                                    NIL
                                                                    NIL))
                                                                  NIL))
                                                                NIL))
                                                              NIL))
                                                            NIL)
                                                           ("2"
                                                            (GRIND
                                                             :IF-MATCH
                                                             NIL)
                                                            NIL
                                                            NIL))
                                                          NIL)
                                                         ("3"
                                                          (GRIND
                                                           :IF-MATCH
                                                           NIL)
                                                          NIL
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL)
                                         ("2"
                                          (EXPAND "injective?")
                                          (("2"
                                            (SKOLEM 1 ("x1" "x2"))
                                            (("2"
                                              (TYPEPRED "x1")
                                              (("2"
                                                (TYPEPRED "x2")
                                                (("2"
                                                  (EXPAND
                                                   "used_indices"
                                                   -1)
                                                  (("2"
                                                    (EXPAND
                                                     "used_indices"
                                                     -2)
                                                    (("2"
                                                      (FLATTEN)
                                                      (("2"
                                                        (TYPEPRED
                                                         "vSlots")
                                                        (("2"
                                                          (INST
                                                           -1
                                                           "x1"
                                                           "x2")
                                                          (("1"
                                                            (REPLACE

                                                             -7
                                                             (-6)

                                                             RL)
                                                            (("1"
                                                              (BETA)
                                                              (("1"
                                                                (GROUND)
                                                                NIL
                                                                NIL))
                                                              NIL))
                                                            NIL)
                                                           ("2"
                                                            (ASSERT)
                                                            NIL
                                                            NIL)
                                                           ("3"
                                                            (ASSERT)
                                                            NIL
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL)
                                   ("2" (GRIND :IF-MATCH NIL) NIL NIL))
                                  NIL)
                                 ("2"
                                  (LEMMA
                                   "finite_sets[nat].nonempty_card")
                                  (("2"
                                    (INST -1 "used_indices")
                                    (("2"
                                      (GROUND)
                                      (("2"
                                        (HIDE -2 -3 2 3)
                                        (("2"
                                          (EXPAND "nonempty?")
                                          (("2"
                                            (EXPAND* "empty?" "member")
                                            (("2"
                                              (REWRITE "forall_not")
                                              (("2"
                                                (SKOLEM -1 "x")
                                                (("2"
                                                  (INST 1 "x")
                                                  NIL
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|allslots2_aux3| "" (LEMMA "invariant_rule")
  (("" (INST?)
    (("1" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (HIDE 2)
        (("2" (SKOLEM 1 "r")
          (("2" (TYPEPRED "r")
            (("2" (BETA)
              (("2" (SPLIT)
                (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL)
                 ("2" (HIDE -2)
                  (("2" (SKOLEM 1 "n")
                    (("2" (TYPEPRED "n")
                      (("2" (FLATTEN)
                        (("2" (HIDE -2)
                          (("2" (EXPAND "run_fragment")
                            (("2" (HIDE -3)
                              (("2"
                                (LEMMA "allslots1_aux1")
                                (("2"
                                  (EXPAND "invariant")
                                  (("2"
                                    (INST -1 "r" "n+1")
                                    (("2"
                                      (LEMMA "allslots1_aux0")
                                      (("2"
                                        (EXPAND "invariant")
                                        (("2"
                                          (INST -1 "r" "n+1")
                                          (("2"
                                            (EXPAND
                                             "reported_currencies"
                                             1)
                                            (("2"
                                              (GRIND)
                                              (("1"
                                                (LEMMA
                                                 "finite_sets[nat].card_emptyset")
                                                (("1"
                                                  (EXPAND "emptyset")
                                                  (("1"
                                                    (GRIND)
                                                    NIL
                                                    NIL))
                                                  NIL))
                                                NIL)
                                               ("2"
                                                (HIDE -1 -3 1)
                                                (("2"
                                                  (NAME "s" "r(1 + n)")
                                                  (("2"
                                                    (REPLACE -1)
                                                    (("2"
                                                      (HIDE -1)
                                                      (("2"
                                                        (LEMMA
                                                         "finite_sets[nat].card_bij")
                                                        (("2"
                                                          (INST
                                                           -1
                                                           "s`reportSize"
                                                           "{c: nat |
                          EXISTS (j: nat):
                            j < s`reportSize AND s`report(j)`Currency = c}")
                                                          (("1"
                                                            (GROUND)
                                                            (("1"
                                                              (HIDE
                                                               2
                                                               3)
                                                              (("1"
                                                                (CASE
                                                                 "s`reportSize =0")
                                                                (("1"
                                                                  (INST
                                                                   1
                                                                   "LAMBDA (n : {c: nat |
                                    EXISTS (j: nat):
                                      j < s`reportSize AND s`report(j)`Currency = c}) : n")
                                                                  (("1"
                                                                    (GRIND)
                                                                    NIL
                                                                    NIL)
                                                                   ("2"
                                                                    (GRIND)
                                                                    NIL
                                                                    NIL)
                                                                   ("3"
                                                                    (GRIND)
                                                                    NIL
                                                                    NIL))
                                                                  NIL)
                                                                 ("2"
                                                                  (LEMMA
                                                                   "more_finite_sets[{j:nat | j< s`reportSize},nat].inverse_bijection")
                                                                  (("1"
                                                                    (INST
                                                                     -1
                                                                     "LAMBDA(n : {j: nat | j < reportSize(s)}) : s`report(n)`Currency")
                                                                    (("1"
                                                                      (GROUND)
                                                                      (("1"
                                                                        (GROUND)
                                                                        (("1"
                                                                          (INST?)
                                                                          (("1"
                                                                            (NAME
                                                                             "f"
                                                                             "LAMBDA (y_1079:
                                                     ({y: nat |
                                                         EXISTS (x: {j: nat | j < reportSize(s)}):
                                                           y = s`report(x)`Currency})):
                                             epsilon({x_1080: {j: nat | j < reportSize(s)} |
                                                        y_1079 = s`report(x_1080)`Currency})")
                                                                            (("1"
                                                                              (REPLACE

                                                                               -1)
                                                                              (("1"
                                                                                (EXPAND
                                                                                 "bijective?")
                                                                                (("1"
                                                                                  (PROP)
                                                                                  (("1"
                                                                                    (HIDE
                                                                                     -3)
                                                                                    (("1"
                                                                                      (EXPAND
                                                                                       "injective?")
                                                                                      (("1"
                                                                                        (SKOLEM
                                                                                         1
                                                                                         ("x1"
                                                                                          "x2"))
                                                                                        (("1"
                                                                                          (INST
                                                                                           -2
                                                                                           "x1"
                                                                                           "x2")
                                                                                          (("1"
                                                                                            (HIDE
                                                                                             -1)
                                                                                            (("1"
                                                                                              (TYPEPRED
                                                                                               "x2")
                                                                                              (("1"
                                                                                                (SKOLEM
                                                                                                 -1
                                                                                                 "j")
                                                                                                (("1"
                                                                                                  (INST
                                                                                                   1
                                                                                                   "j")
                                                                                                  (("1"
                                                                                                    (ASSERT)
                                                                                                    NIL
                                                                                                    NIL)
                                                                                                   ("2"
                                                                                                    (ASSERT)
                                                                                                    NIL
                                                                                                    NIL))
                                                                                                  NIL))
                                                                                                NIL))
                                                                                              NIL))
                                                                                            NIL)
                                                                                           ("2"
                                                                                            (TYPEPRED
                                                                                             "x1")
                                                                                            (("2"
                                                                                              (SKOLEM
                                                                                               -1
                                                                                               "j")
                                                                                              (("2"
                                                                                                (INST
                                                                                                 1
                                                                                                 "j")
                                                                                                (("1"
                                                                                                  (ASSERT)
                                                                                                  NIL
                                                                                                  NIL)
                                                                                                 ("2"
                                                                                                  (ASSERT)
                                                                                                  NIL
                                                                                                  NIL))
                                                                                                NIL))
                                                                                              NIL))
                                                                                            NIL))
                                                                                          NIL))
                                                                                        NIL))
                                                                                      NIL))
                                                                                    NIL)
                                                                                   ("2"
                                                                                    (HIDE
                                                                                     -2)
                                                                                    (("2"
                                                                                      (EXPAND
                                                                                       "surjective?")
                                                                                      (("2"
                                                                                        (SKOLEM
                                                                                         1
                                                                                         "y")
                                                                                        (("2"
                                                                                          (INST
                                                                                           -2
                                                                                           "y")
                                                                                          (("2"
                                                                                            (SKOLEM
                                                                                             -2
                                                                                             "x")
                                                                                            (("2"
                                                                                              (INST
                                                                                               1
                                                                                               "x")
                                                                                              (("2"
                                                                                                (TYPEPRED
                                                                                                 "x")
                                                                                                (("2"
                                                                                                  (SKOLEM
                                                                                                   -1
                                                                                                   "j")
                                                                                                  (("2"
                                                                                                    (INST
                                                                                                     1
                                                                                                     "j")
                                                                                                    (("2"
                                                                                                      (ASSERT)
                                                                                                      NIL
                                                                                                      NIL))
                                                                                                    NIL))
                                                                                                  NIL))
                                                                                                NIL))
                                                                                              NIL))
                                                                                            NIL))
                                                                                          NIL))
                                                                                        NIL))
                                                                                      NIL))
                                                                                    NIL))
                                                                                  NIL))
                                                                                NIL))
                                                                              NIL)
                                                                             ("2"
                                                                              (HIDE
                                                                               -1
                                                                               3)
                                                                              (("2"
                                                                                (SKOLEM
                                                                                 1
                                                                                 "y")
                                                                                (("2"
                                                                                  (INST
                                                                                   1
                                                                                   "0")
                                                                                  NIL
                                                                                  NIL))
                                                                                NIL))
                                                                              NIL))
                                                                            NIL)
                                                                           ("2"
                                                                            (SKOLEM
                                                                             1
                                                                             "x1")
                                                                            (("2"
                                                                              (TYPEPRED
                                                                               "x1")
                                                                              (("2"
                                                                                (HIDE
                                                                                 -2)
                                                                                (("2"
                                                                                  (GROUND)
                                                                                  (("1"
                                                                                    (SKOLEM
                                                                                     -1
                                                                                     "j")
                                                                                    (("1"
                                                                                      (INST
                                                                                       1
                                                                                       "j")
                                                                                      (("1"
                                                                                        (ASSERT)
                                                                                        NIL
                                                                                        NIL))
                                                                                      NIL))
                                                                                    NIL)
                                                                                   ("2"
                                                                                    (SKOLEM
                                                                                     -1
                                                                                     "j")
                                                                                    (("2"
                                                                                      (INST
                                                                                       1
                                                                                       "j")
                                                                                      (("1"
                                                                                        (ASSERT)
                                                                                        NIL
                                                                                        NIL)
                                                                                       ("2"
                                                                                        (ASSERT)
                                                                                        NIL
                                                                                        NIL))
                                                                                      NIL))
                                                                                    NIL))
                                                                                  NIL))
                                                                                NIL))
                                                                              NIL))
                                                                            NIL)
                                                                           ("3"
                                                                            (HIDE
                                                                             -1)
                                                                            (("3"
                                                                              (SKOLEM
                                                                               1
                                                                               "y")
                                                                              (("3"
                                                                                (INST
                                                                                 1
                                                                                 "0")
                                                                                NIL
                                                                                NIL))
                                                                              NIL))
                                                                            NIL))
                                                                          NIL)
                                                                         ("2"
                                                                          (HIDE
                                                                           3)
                                                                          (("2"
                                                                            (LEMMA
                                                                             "allslots1_aux3")
                                                                            (("2"
                                                                              (EXPAND
                                                                               "invariant")
                                                                              (("2"
                                                                                (REVEAL
                                                                                 -3)
                                                                                (("2"
                                                                                  (INST
                                                                                   -2
                                                                                   "r"
                                                                                   "1+n")
                                                                                  (("2"
                                                                                    (REVEAL
                                                                                     -5)
                                                                                    (("2"
                                                                                      (GROUND)
                                                                                      (("2"
                                                                                        (SKOLEM
                                                                                         1
                                                                                         ("x1"
                                                                                          "x2"))
                                                                                        (("2"
                                                                                          (INST
                                                                                           -2
                                                                                           "x1"
                                                                                           "x2")
                                                                                          (("2"
                                                                                            (GRIND)
                                                                                            NIL
                                                                                            NIL))
                                                                                          NIL))
                                                                                        NIL))
                                                                                      NIL))
                                                                                    NIL))
                                                                                  NIL))
                                                                                NIL))
                                                                              NIL))
                                                                            NIL))
                                                                          NIL))
                                                                        NIL))
                                                                      NIL))
                                                                    NIL)
                                                                   ("2"
                                                                    (INST
                                                                     1
                                                                     "0")
                                                                    (("2"
                                                                      (ASSERT)
                                                                      NIL
                                                                      NIL))
                                                                    NIL))
                                                                  NIL))
                                                                NIL))
                                                              NIL))
                                                            NIL)
                                                           ("2"
                                                            (HIDE 2)
                                                            (("2"
                                                              (LEMMA
                                                               "finite_reported_currencies")
                                                              (("2"
                                                                (INST
                                                                 -1
                                                                 "s")
                                                                (("2"
                                                                  (EXPAND
                                                                   "is_finite")
                                                                  (("2"
                                                                    (SKOLEM
                                                                     -1
                                                                     ("N"
                                                                      "f"))
                                                                    (("2"
                                                                      (INST
                                                                       1
                                                                       "N"
                                                                       "f")
                                                                      (("1"
                                                                        (EXPAND
                                                                         "injective?")
                                                                        (("1"
                                                                          (SKOLEM
                                                                           1
                                                                           ("x1"
                                                                            "x2"))
                                                                          (("1"
                                                                            (TYPEPRED
                                                                             "x1")
                                                                            (("1"
                                                                              (TYPEPRED
                                                                               "x2")
                                                                              (("1"
                                                                                (INST
                                                                                 -3
                                                                                 "x1"
                                                                                 "x2")
                                                                                (("1"
                                                                                  (SKOLEM
                                                                                   -1
                                                                                   "j")
                                                                                  (("1"
                                                                                    (INST
                                                                                     1
                                                                                     "j")
                                                                                    (("1"
                                                                                      (GROUND)
                                                                                      NIL
                                                                                      NIL))
                                                                                    NIL))
                                                                                  NIL)
                                                                                 ("2"
                                                                                  (SKOLEM
                                                                                   -2
                                                                                   "j")
                                                                                  (("2"
                                                                                    (INST
                                                                                     1
                                                                                     "j")
                                                                                    (("2"
                                                                                      (GROUND)
                                                                                      NIL
                                                                                      NIL))
                                                                                    NIL))
                                                                                  NIL))
                                                                                NIL))
                                                                              NIL))
                                                                            NIL))
                                                                          NIL))
                                                                        NIL)
                                                                       ("2"
                                                                        (SKOLEM
                                                                         1
                                                                         "x")
                                                                        (("2"
                                                                          (GROUND)
                                                                          (("1"
                                                                            (SKOLEM
                                                                             -1
                                                                             "j")
                                                                            (("1"
                                                                              (INST
                                                                               1
                                                                               "j")
                                                                              (("1"
                                                                                (GROUND)
                                                                                NIL
                                                                                NIL))
                                                                              NIL))
                                                                            NIL)
                                                                           ("2"
                                                                            (SKOLEM
                                                                             -1
                                                                             "j")
                                                                            (("2"
                                                                              (INST
                                                                               1
                                                                               "j")
                                                                              (("2"
                                                                                (GROUND)
                                                                                NIL
                                                                                NIL))
                                                                              NIL))
                                                                            NIL))
                                                                          NIL))
                                                                        NIL))
                                                                      NIL))
                                                                    NIL))
                                                                  NIL))
                                                                NIL))
                                                              NIL))
                                                            NIL)
                                                           ("3"
                                                            (HIDE 2)
                                                            (("3"
                                                              (GRIND)
                                                              NIL
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL)
                                               ("3"
                                                (HIDE -1 -3 1)
                                                (("3"
                                                  (NAME "s" "r(1 + n)")
                                                  (("3"
                                                    (REPLACE -1)
                                                    (("3"
                                                      (HIDE -1)
                                                      (("3"
                                                        (LEMMA
                                                         "finite_sets[nat].card_bij")
                                                        (("3"
                                                          (INST
                                                           -1
                                                           "s`reportSize"
                                                           "{c: nat |
                          EXISTS (j: nat):
                            j < s`reportSize AND s`report(j)`Currency = c}")
                                                          (("1"
                                                            (GROUND)
                                                            (("1"
                                                              (HIDE
                                                               2
                                                               3)
                                                              (("1"
                                                                (CASE
                                                                 "s`reportSize =0")
                                                                (("1"
                                                                  (INST
                                                                   1
                                                                   "LAMBDA (n : {c: nat |
                                    EXISTS (j: nat):
                                      j < s`reportSize AND s`report(j)`Currency = c}) : n")
                                                                  (("1"
                                                                    (GRIND)
                                                                    NIL
                                                                    NIL)
                                                                   ("2"
                                                                    (GRIND)
                                                                    NIL
                                                                    NIL)
                                                                   ("3"
                                                                    (GRIND)
                                                                    NIL
                                                                    NIL))
                                                                  NIL)
                                                                 ("2"
                                                                  (LEMMA
                                                                   "more_finite_sets[{j:nat | j< s`reportSize},nat].inverse_bijection")
                                                                  (("1"
                                                                    (INST
                                                                     -1
                                                                     "LAMBDA(n : {j: nat | j < reportSize(s)}) : s`report(n)`Currency")
                                                                    (("1"
                                                                      (GROUND)
                                                                      (("1"
                                                                        (GROUND)
                                                                        (("1"
                                                                          (INST?)
                                                                          (("1"
                                                                            (NAME
                                                                             "f"
                                                                             "LAMBDA (y_1079:
                                                     ({y: nat |
                                                         EXISTS (x: {j: nat | j < reportSize(s)}):
                                                           y = s`report(x)`Currency})):
                                             epsilon({x_1080: {j: nat | j < reportSize(s)} |
                                                        y_1079 = s`report(x_1080)`Currency})")
                                                                            (("1"
                                                                              (REPLACE

                                                                               -1)
                                                                              (("1"
                                                                                (EXPAND
                                                                                 "bijective?")
                                                                                (("1"
                                                                                  (PROP)
                                                                                  (("1"
                                                                                    (HIDE
                                                                                     -3)
                                                                                    (("1"
                                                                                      (EXPAND
                                                                                       "injective?")
                                                                                      (("1"
                                                                                        (SKOLEM
                                                                                         1
                                                                                         ("x1"
                                                                                          "x2"))
                                                                                        (("1"
                                                                                          (INST
                                                                                           -2
                                                                                           "x1"
                                                                                           "x2")
                                                                                          (("1"
                                                                                            (HIDE
                                                                                             -1)
                                                                                            (("1"
                                                                                              (TYPEPRED
                                                                                               "x2")
                                                                                              (("1"
                                                                                                (SKOLEM
                                                                                                 -1
                                                                                                 "j")
                                                                                                (("1"
                                                                                                  (INST
                                                                                                   1
                                                                                                   "j")
                                                                                                  (("1"
                                                                                                    (ASSERT)
                                                                                                    NIL
                                                                                                    NIL)
                                                                                                   ("2"
                                                                                                    (ASSERT)
                                                                                                    NIL
                                                                                                    NIL))
                                                                                                  NIL))
                                                                                                NIL))
                                                                                              NIL))
                                                                                            NIL)
                                                                                           ("2"
                                                                                            (TYPEPRED
                                                                                             "x1")
                                                                                            (("2"
                                                                                              (SKOLEM
                                                                                               -1
                                                                                               "j")
                                                                                              (("2"
                                                                                                (INST
                                                                                                 1
                                                                                                 "j")
                                                                                                (("1"
                                                                                                  (ASSERT)
                                                                                                  NIL
                                                                                                  NIL)
                                                                                                 ("2"
                                                                                                  (ASSERT)
                                                                                                  NIL
                                                                                                  NIL))
                                                                                                NIL))
                                                                                              NIL))
                                                                                            NIL))
                                                                                          NIL))
                                                                                        NIL))
                                                                                      NIL))
                                                                                    NIL)
                                                                                   ("2"
                                                                                    (HIDE
                                                                                     -2)
                                                                                    (("2"
                                                                                      (EXPAND
                                                                                       "surjective?")
                                                                                      (("2"
                                                                                        (SKOLEM
                                                                                         1
                                                                                         "y")
                                                                                        (("2"
                                                                                          (INST
                                                                                           -2
                                                                                           "y")
                                                                                          (("2"
                                                                                            (SKOLEM
                                                                                             -2
                                                                                             "x")
                                                                                            (("2"
                                                                                              (INST
                                                                                               1
                                                                                               "x")
                                                                                              (("2"
                                                                                                (TYPEPRED
                                                                                                 "x")
                                                                                                (("2"
                                                                                                  (SKOLEM
                                                                                                   -1
                                                                                                   "j")
                                                                                                  (("2"
                                                                                                    (INST
                                                                                                     1
                                                                                                     "j")
                                                                                                    (("2"
                                                                                                      (ASSERT)
                                                                                                      NIL
                                                                                                      NIL))
                                                                                                    NIL))
                                                                                                  NIL))
                                                                                                NIL))
                                                                                              NIL))
                                                                                            NIL))
                                                                                          NIL))
                                                                                        NIL))
                                                                                      NIL))
                                                                                    NIL))
                                                                                  NIL))
                                                                                NIL))
                                                                              NIL)
                                                                             ("2"
                                                                              (HIDE
                                                                               -1
                                                                               3)
                                                                              (("2"
                                                                                (SKOLEM
                                                                                 1
                                                                                 "y")
                                                                                (("2"
                                                                                  (INST
                                                                                   1
                                                                                   "0")
                                                                                  NIL
                                                                                  NIL))
                                                                                NIL))
                                                                              NIL))
                                                                            NIL)
                                                                           ("2"
                                                                            (SKOLEM
                                                                             1
                                                                             "x1")
                                                                            (("2"
                                                                              (TYPEPRED
                                                                               "x1")
                                                                              (("2"
                                                                                (HIDE
                                                                                 -2)
                                                                                (("2"
                                                                                  (GROUND)
                                                                                  (("1"
                                                                                    (SKOLEM
                                                                                     -1
                                                                                     "j")
                                                                                    (("1"
                                                                                      (INST
                                                                                       1
                                                                                       "j")
                                                                                      (("1"
                                                                                        (ASSERT)
                                                                                        NIL
                                                                                        NIL))
                                                                                      NIL))
                                                                                    NIL)
                                                                                   ("2"
                                                                                    (SKOLEM
                                                                                     -1
                                                                                     "j")
                                                                                    (("2"
                                                                                      (INST
                                                                                       1
                                                                                       "j")
                                                                                      (("1"
                                                                                        (ASSERT)
                                                                                        NIL
                                                                                        NIL)
                                                                                       ("2"
                                                                                        (ASSERT)
                                                                                        NIL
                                                                                        NIL))
                                                                                      NIL))
                                                                                    NIL))
                                                                                  NIL))
                                                                                NIL))
                                                                              NIL))
                                                                            NIL)
                                                                           ("3"
                                                                            (HIDE
                                                                             -1)
                                                                            (("3"
                                                                              (SKOLEM
                                                                               1
                                                                               "y")
                                                                              (("3"
                                                                                (INST
                                                                                 1
                                                                                 "0")
                                                                                NIL
                                                                                NIL))
                                                                              NIL))
                                                                            NIL))
                                                                          NIL)
                                                                         ("2"
                                                                          (HIDE
                                                                           3)
                                                                          (("2"
                                                                            (LEMMA
                                                                             "allslots1_aux3")
                                                                            (("2"
                                                                              (EXPAND
                                                                               "invariant")
                                                                              (("2"
                                                                                (REVEAL
                                                                                 -3)
                                                                                (("2"
                                                                                  (INST
                                                                                   -2
                                                                                   "r"
                                                                                   "1+n")
                                                                                  (("2"
                                                                                    (REVEAL
                                                                                     -5)
                                                                                    (("2"
                                                                                      (GROUND)
                                                                                      (("2"
                                                                                        (SKOLEM
                                                                                         1
                                                                                         ("x1"
                                                                                          "x2"))
                                                                                        (("2"
                                                                                          (INST
                                                                                           -2
                                                                                           "x1"
                                                                                           "x2")
                                                                                          (("2"
                                                                                            (GRIND)
                                                                                            NIL
                                                                                            NIL))
                                                                                          NIL))
                                                                                        NIL))
                                                                                      NIL))
                                                                                    NIL))
                                                                                  NIL))
                                                                                NIL))
                                                                              NIL))
                                                                            NIL))
                                                                          NIL))
                                                                        NIL))
                                                                      NIL))
                                                                    NIL)
                                                                   ("2"
                                                                    (INST
                                                                     1
                                                                     "0")
                                                                    (("2"
                                                                      (ASSERT)
                                                                      NIL
                                                                      NIL))
                                                                    NIL))
                                                                  NIL))
                                                                NIL))
                                                              NIL))
                                                            NIL)
                                                           ("2"
                                                            (HIDE 2)
                                                            (("2"
                                                              (LEMMA
                                                               "finite_reported_currencies")
                                                              (("2"
                                                                (INST
                                                                 -1
                                                                 "s")
                                                                (("2"
                                                                  (EXPAND
                                                                   "is_finite")
                                                                  (("2"
                                                                    (SKOLEM
                                                                     -1
                                                                     ("N"
                                                                      "f"))
                                                                    (("2"
                                                                      (INST
                                                                       1
                                                                       "N"
                                                                       "f")
                                                                      (("1"
                                                                        (EXPAND
                                                                         "injective?")
                                                                        (("1"
                                                                          (SKOLEM
                                                                           1
                                                                           ("x1"
                                                                            "x2"))
                                                                          (("1"
                                                                            (TYPEPRED
                                                                             "x1")
                                                                            (("1"
                                                                              (TYPEPRED
                                                                               "x2")
                                                                              (("1"
                                                                                (INST
                                                                                 -3
                                                                                 "x1"
                                                                                 "x2")
                                                                                (("1"
                                                                                  (SKOLEM
                                                                                   -1
                                                                                   "j")
                                                                                  (("1"
                                                                                    (INST
                                                                                     1
                                                                                     "j")
                                                                                    (("1"
                                                                                      (GROUND)
                                                                                      NIL
                                                                                      NIL))
                                                                                    NIL))
                                                                                  NIL)
                                                                                 ("2"
                                                                                  (SKOLEM
                                                                                   -2
                                                                                   "j")
                                                                                  (("2"
                                                                                    (INST
                                                                                     1
                                                                                     "j")
                                                                                    (("2"
                                                                                      (GROUND)
                                                                                      NIL
                                                                                      NIL))
                                                                                    NIL))
                                                                                  NIL))
                                                                                NIL))
                                                                              NIL))
                                                                            NIL))
                                                                          NIL))
                                                                        NIL)
                                                                       ("2"
                                                                        (SKOLEM
                                                                         1
                                                                         "x")
                                                                        (("2"
                                                                          (GROUND)
                                                                          (("1"
                                                                            (SKOLEM
                                                                             -1
                                                                             "j")
                                                                            (("1"
                                                                              (INST
                                                                               1
                                                                               "j")
                                                                              (("1"
                                                                                (GROUND)
                                                                                NIL
                                                                                NIL))
                                                                              NIL))
                                                                            NIL)
                                                                           ("2"
                                                                            (SKOLEM
                                                                             -1
                                                                             "j")
                                                                            (("2"
                                                                              (INST
                                                                               1
                                                                               "j")
                                                                              (("2"
                                                                                (GROUND)
                                                                                NIL
                                                                                NIL))
                                                                              NIL))
                                                                            NIL))
                                                                          NIL))
                                                                        NIL))
                                                                      NIL))
                                                                    NIL))
                                                                  NIL))
                                                                NIL))
                                                              NIL))
                                                            NIL)
                                                           ("3"
                                                            (HIDE 2)
                                                            (("3"
                                                              (GRIND)
                                                              NIL
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (HIDE 2)
      (("2" (LEMMA "finite_reported_currencies")
        (("2" (GRIND) NIL NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|allslots2_aux2| "" (LEMMA "invariant_rule")
  (("" (INST?)
    (("" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (HIDE 2)
        (("2" (SKOLEM 1 "r")
          (("2" (TYPEPRED "r")
            (("2" (BETA)
              (("2" (SPLIT)
                (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL)
                 ("2" (HIDE -2)
                  (("2" (SKOLEM 1 "n")
                    (("2" (TYPEPRED "n")
                      (("2" (FLATTEN)
                        (("2" (EXPAND "run_fragment")
                          (("2" (INST -4 "n")
                            (("2" (GROUND)
                              (("1"
                                (HIDE -3)
                                (("1" (GRIND) NIL NIL))
                                NIL)
                               ("2"
                                (EXPAND* "subset?" "member")
                                (("2"
                                  (SKOLEM 1 "x")
                                  (("2"
                                    (INST -3 "x")
                                    (("2"
                                      (GROUND)
                                      (("2"
                                        (GRIND :IF-MATCH NIL)
                                        (("1"
                                          (INST 1 "j!1")
                                          (("1" (ASSERT) NIL NIL))
                                          NIL)
                                         ("2"
                                          (INST 1 "j!1")
                                          (("2" (ASSERT) NIL NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL)
                               ("3"
                                (HIDE -3)
                                (("3" (GRIND) NIL NIL))
                                NIL)
                               ("4"
                                (EXPAND* "subset?" "member")
                                (("4"
                                  (SKOLEM 1 "x")
                                  (("4"
                                    (INST -3 "x")
                                    (("4"
                                      (GROUND)
                                      (("4"
                                        (GRIND :IF-MATCH NIL)
                                        (("1"
                                          (INST
                                           2
                                           "mSlotInfo(a!1)`SlotIndex")
                                          NIL
                                          NIL)
                                         ("2"
                                          (INST 1 "j!1")
                                          (("2" (ASSERT) NIL NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL)
                               ("5"
                                (HIDE -3)
                                (("5" (GRIND) NIL NIL))
                                NIL)
                               ("6"
                                (EXPAND* "subset?" "member")
                                (("6"
                                  (SKOLEM 1 "x")
                                  (("6"
                                    (INST -3 "x")
                                    (("6"
                                      (GROUND)
                                      (("6"
                                        (GRIND :IF-MATCH NIL)
                                        (("1"
                                          (INST 1 "j!1")
                                          (("1" (ASSERT) NIL NIL))
                                          NIL)
                                         ("2"
                                          (INST 1 "j!1")
                                          (("2" (ASSERT) NIL NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL)
                               ("7" (GRIND) NIL NIL)
                               ("8"
                                (HIDE 1)
                                (("8" (GRIND) NIL NIL))
                                NIL)
                               ("9" (GRIND) NIL NIL)
                               ("10"
                                (HIDE 1)
                                (("10" (GRIND) NIL NIL))
                                NIL)
                               ("11" (GRIND) NIL NIL)
                               ("12" (GRIND :IF-MATCH NIL) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|allslots2_aux1| "" (LEMMA "allslots2_aux4")
  (("" (LEMMA "allslots2_aux3")
    (("" (LEMMA "allslots2_aux2")
      (("" (EXPAND "invariant")
        (("" (SKOLEM 1 ("r" "n"))
          (("" (INST - "r" "n")
            (("" (INST - "r" "n")
              (("" (INST - "r" "n")
                (("" (GROUND)
                  (("1" (LEMMA "finite_sets[nat].same_card_subset")
                    (("1"
                      (INST -1 "reported_currencies(r(n))"
                       "used_currencies")
                      (("1" (GROUND) NIL NIL)
                       ("2" (LEMMA "finite_reported_currencies")
                        (("2" (INST -1 "r(n)") NIL NIL)) NIL))
                      NIL))
                    NIL)
                   ("2" (LEMMA "finite_sets[nat].same_card_subset")
                    (("2"
                      (INST -1 "reported_currencies(r(n))"
                       "used_currencies")
                      (("1" (GROUND) NIL NIL)
                       ("2" (LEMMA "finite_reported_currencies")
                        (("2" (INST -1 "r(n)") NIL NIL)) NIL))
                      NIL))
                    NIL)
                   ("3" (LEMMA "finite_sets[nat].same_card_subset")
                    (("3"
                      (INST -1 "reported_currencies(r(n))"
                       "used_currencies")
                      (("1" (GROUND) NIL NIL)
                       ("2" (LEMMA "finite_reported_currencies")
                        (("2" (INST -1 "r(n)") NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|allslots2_aux0_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|allslots2_aux0_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|allslots2_aux0_TCC3| "" (SUBTYPE-TCC) NIL NIL)
 (|allslots2_aux0| "" (LEMMA "invariant_rule")
  (("" (INST?)
    (("1" (SPLIT)
      (("1" (PROPAX) NIL NIL)
       ("2" (HIDE 2)
        (("2" (SKOLEM 1 "r")
          (("2" (TYPEPRED "r")
            (("2" (SPLIT)
              (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL)
               ("2" (HIDE -2)
                (("2" (BETA)
                  (("2" (SKOLEM 1 "n")
                    (("2" (EXPAND "run_fragment")
                      (("2" (INST -1 "n")
                        (("2" (GROUND)
                          (("1" (GRIND :IF-MATCH NIL) NIL NIL)
                           ("2" (SKOLEM 1 "i")
                            (("2" (GRIND :IF-MATCH NIL)
                              (("1"
                                (INST -4 "i")
                                (("1" (GROUND) NIL NIL))
                                NIL)
                               ("2"
                                (INST -4 "i")
                                (("2" (GROUND) NIL NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("3" (GRIND :IF-MATCH NIL)
                            (("1" (LEMMA "allslots1_aux1")
                              (("1" (GRIND) NIL NIL)) NIL)
                             ("2" (LEMMA "allslots1_aux0")
                              (("2" (GRIND) NIL NIL)) NIL))
                            NIL)
                           ("4" (SKOLEM 1 "i")
                            (("4" (GRIND :IF-MATCH NIL)
                              (("1"
                                (LEMMA "allslots2_aux1")
                                (("1"
                                  (EXPAND "invariant")
                                  (("1"
                                    (INST?)
                                    (("1"
                                      (GROUND)
                                      (("1"
                                        (HIDE 4 3 2 -11 -10 -8 -7 -5)
                                        (("1"
                                          (EXPAND* "subset?" "member")
                                          (("1"
                                            (INST
                                             -2
                                             "vSlots(i)`Currency")
                                            (("1"
                                              (SPLIT)
                                              (("1"
                                                (EXPAND
                                                 "reported_currencies")
                                                (("1"
                                                  (PROPAX)
                                                  NIL
                                                  NIL))
                                                NIL)
                                               ("2"
                                                (HIDE 2)
                                                (("2" (GRIND) NIL NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL)
                               ("2"
                                (LEMMA "allslots2_aux1")
                                (("2"
                                  (EXPAND "invariant")
                                  (("2"
                                    (INST?)
                                    (("2"
                                      (GROUND)
                                      (("2"
                                        (EXPAND* "subset?" "member")
                                        (("2"
                                          (INST
                                           -2
                                           "vSlots(i)`Currency")
                                          (("2"
                                            (GROUND)
                                            (("1"
                                              (INST 1 "i")
                                              (("1"
                                                (GRIND :IF-MATCH NIL)
                                                NIL
                                                NIL))
                                              NIL)
                                             ("2"
                                              (EXPAND
                                               "used_currencies")
                                              (("2"
                                                (INST 1 "i")
                                                (("2"
                                                  (ASSERT)
                                                  (("2"
                                                    (GRIND
                                                     :IF-MATCH
                                                     NIL)
                                                    NIL
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("5" (GRIND :IF-MATCH NIL) NIL NIL)
                           ("6" (HIDE 2) (("6" (GRIND) NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL)
     ("3" (HIDE 2) (("3" (GRIND) NIL NIL)) NIL)
     ("4" (HIDE 2) (("4" (GRIND) NIL NIL)) NIL))
    NIL))
  NIL))


$$$allslots_props.pvs
allslots_props: THEORY
%% properties of the allslots command of the CEPS
 BEGIN

  IMPORTING allslots_aux



%%% first requirement : no slot is reported twice  %%%%%%%
  allslots1: THEOREM
    invariant(LAMBDA (s: State):
                s`pc = CepSIQ_Reply_P2 AND s`vSlotsReported>= pSlotCount IMPLIES
                 (s`reportSize <= pSlotCount AND (FORALL (i, j: below(s`reportSize)):
                    i /= j IMPLIES s`report(i)`Currency /= s`report(j)`Currency)))


%%%%% second requirement: all used slots are reported %%%%%%%%%

  allslots2: THEOREM 
    invariant(LAMBDA (s: State):
                s`pc = CepSIQ_Reply_P2 AND s`vSlotsReported>= pSlotCount IMPLIES
                 (s`reportSize <= pSlotCount AND (FORALL (i: below(pSlotCount) | vSlots(i)`InUse) :
                        EXISTS (j: below(s`reportSize)): s`report(j)`Currency = vSlots(i)`Currency)))
 END allslots_props



$$$allslots_props.prf
(|allslots_props| (|allslots1_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|allslots1_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|allslots1| "" (LEMMA "allslots1_aux3")
  (("" (EXPAND "invariant")
    (("" (SKOLEM 1 ("r" "n"))
      (("" (INST -1 "r" "n")
        (("" (GROUND)
          (("" (SKOLEM 1 ("i" "j"))
            (("" (INST -2 "i" "j") (("" (GRIND) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|allslots2_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|allslots2_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|allslots2_TCC3| "" (SUBTYPE-TCC) NIL NIL)
 (|allslots2| "" (LEMMA "allslots2_aux0")
  (("" (EXPAND "invariant")
    (("" (SKOLEM 1 ("r" "n"))
      (("" (INST -1 "r" "n")
        (("" (GROUND)
          (("" (SKOLEM 1 "i")
            (("" (INST -2 "i")
              (("" (GROUND)
                (("" (SKOLEM -1 "j")
                  (("" (INST 1 "j")
                    (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))