[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Automaton composition



Hello, I'm a beginner in PVS and I have this problem:
I'd like to prove invariant INVAR above puInputN (unspecified nat 
constant < 2^16) same aoutomata (automaton array) sequential composition 
with
recursive function:puInputTF with measure puInputN (theory Sc), but PVS 
rewrites in the proof this function to
puInputTF rewrites
  puInputTF(puInputN,
            (# puInputD
                 := LAMBDA (i_1: below(puInputN)): (# bInput := 
i!1`pbInput(i_1), sState := sS0 #),
               dOutputD := (# oCnt := 0, sState := sPassive, bOutput := 
FALSE #) #))
  to puInputTF(puInputN - 1, ...
and this subgoal ends with
-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

Can you help me with recursive function for N automata definition? PVS 
files are attached.

Thanks,

    Robert Kolcava, Czech Republic




sc1.prf

%
% sc1.pvs
% 
% sequential composition of automaton 
%
% 070209
% 
%
Sc: THEORY
BEGIN

IMPORTING dtyp
IMPORTING asetn
IMPORTING UInput
IMPORTING DOutput

  puInputN: ITER

  SCI:  TYPE = [# pbInput: ASet[ puInputN, BIT ] #]
  SCD:  TYPE = [# puInputD: ASet[ puInputN, UInput.D ],
                  dOutputD: DOutput.D #]

  initSCD:  Sc.SCD =	(#
    puInputD := LAMBDA(i: below(puInputN)): UInput.initD,
    dOutputD := DOutput.initD #)

  IL:   TYPE = list[SCI]

  sCDIM(sci_: SCI, scd_: SCD): SCD = 
    scd_ WITH [ puInputD := LAMBDA(i: below(puInputN)): 
                              scd_`puInputD(i) WITH [ bInput := sci_`pbInput(i) ]]
  
  
  puInputTF(n: ITER, scd_: SCD): RECURSIVE SCD = 
    IF n = 0 THEN 
      scd_ WITH 
        [ puInputD := scd_`puInputD WITH 
            [ (0) := UInput.tF((# uInputD := scd_`puInputD(0), dOutputD := scd_`dOutputD #))`uInputD ],
          dOutputD := UInput.tF((# uInputD := scd_`puInputD(0), dOutputD := scd_`dOutputD #))`dOutputD ]
    ELSE puInputTF(n - 1, scd_) WITH
        [ puInputD := scd_`puInputD WITH       
            [ (n - 1) := 
                UInput.tF((# uInputD := scd_`puInputD(n-1), dOutputD := scd_`dOutputD #))`uInputD ],
          dOutputD := UInput.tF((# uInputD := 
                scd_`puInputD(n - 1), dOutputD := scd_`dOutputD #))`dOutputD ]
    ENDIF
  MEASURE n
%
  uOutputTF(scd_: SCD): SCD = 
    LET
      dOutputRD = DOutput.tF((# dOutputD := scd_`dOutputD #))
    IN
    scd_ WITH [ dOutputD := dOutputRD`dOutputD ]
%    
  sCDTF(i_: SCI, scd_: SCD): SCD = 
    uOutputTF(puInputTF(puInputN, sCDIM(i_, scd_)))
%
  curSCD(iL_: IL): RECURSIVE SCD = 
    CASES iL_ OF
      null:        initSCD, 
      cons(i, r):  sCDTF(i, curSCD(r))
    ENDCASES
    MEASURE length(iL_)
%
i_:   VAR SCI
iL_:  VAR IL
%
  Invar: PROPOSITION % = ASSERT
      (EXISTS(i: below(puInputN)): i_`pbInput(i))
    IMPLIES    
      curSCD(cons(i_, iL_))`dOutputD`bOutput
%
END Sc



%
% asetn.pvs
%
asetn[ N_: nat, T_: TYPE ]: THEORY

BEGIN

IMPORTING dtyp

  ASet: TYPE = [ below(N_) -> T_ ]

  valid_iter?(i: nat, a: ASet): bool = i < N_

%  asetConv(a: ASet): [ below[N_] -> T_ ] = a(a)

%  CONVERSION asetConv
  asetAssign(a: ASet, i: below[N_], v: T_): ASet = 
    a WITH [ (i) := v ]
%  
END asetn
%
%
%
asetOper[ T_: TYPE ]: THEORY
BEGIN
%
% <asetn> := LAMBDA(i: below(N)): <expr>

%
END asetOper
%
% dtyp.pvs
% 30.07.06
%
% basic data types
%

dtyp: THEORY

BEGIN

% Data types

  BIT:      TYPE = bool
  CMD:      TYPE = bool
  UI8:      TYPE = below(2 ^ 8)
  UI16:     TYPE = below(2 ^ 16)
  TMR16:    TYPE = UI16
  ITER:     TYPE = nat

END dtyp

%
% io.pvs
%
% 070201 inc
%
UInput: THEORY
BEGIN

IMPORTING dtyp
IMPORTING DOutput

S:	  TYPE = { sS0, sS1 }
D:	  TYPE = [# bInput: BIT, sState: S #]
RD:   TYPE = [# uInputD: UInput.D, dOutputD: DOutput.D #]

initD:  D =	 (#   bInput    := FALSE,
                  sState  := sS0 #)

tF(rd_: RD): RD = 
    LET 
      iD = rd_`uInputD,
      oD = rd_`dOutputD,
      s  = rd_`uInputD`sState
    IN
    COND 
      sS0?(s) ->
              IF iD`bInput THEN rd_ WITH 
                [ uInputD := iD WITH 
                  [ sState := sS1 ],
                dOutputD := oD WITH 
                  [ oCnt := succ(oD`oCnt) ] ] 
              ELSE rd_
              ENDIF,
      sS1?(s) ->
              IF NOT iD`bInput THEN rd_ WITH 
                [ uInputD := iD WITH 
                  [ sState := sS0 ],
                dOutputD := oD WITH
                  [ oCnt := pred(oD`oCnt) ] ] 
              ELSE rd_ 
              ENDIF
    ENDCOND
END UInput

DOutput: THEORY
BEGIN

IMPORTING dtyp

S:	  TYPE = { sPassive, sActive }
D:	  TYPE = [# sState: S, oCnt: UI8, bOutput: BIT #]
RD:   TYPE = [# dOutputD: DOutput.D #]

initD:  D =	 (# oCnt    := 0,
                sState  := sPassive,
                bOutput := FALSE #)

tF(rd_: RD): RD = 
    LET 
      oD = rd_`dOutputD,
      s  = rd_`dOutputD`sState
    IN
    COND
      sPassive?(s) ->
                IF oD`oCnt > 0 THEN rd_ WITH 
                  [ dOutputD := oD WITH 
                    [ sState := sActive,
                      bOutput := TRUE ] ] 
                ELSE rd_
                ENDIF,
      sActive?(s) ->
                IF oD`oCnt = 0 THEN rd_ WITH 
                  [ dOutputD := oD WITH 
                    [ sState := sPassive,
                      bOutput := FALSE ] ] 
                ELSE rd_
                ENDIF
    ENDCOND
%
%
%
END DOutput
Starting pvs-allegro -qq ...
Allegro CL Enterprise Edition
8.0 [Linux (x86)] (Nov 28, 2006 16:50)
Copyright (C) 1985-2005, Franz Inc., Oakland, CA, USA.  All Rights Reserved.

This dynamic runtime copy of Allegro CL was built by:
   [TC8101] SRI International

;; Optimization settings: safety 1, space 1, speed 3, debug 1.
;; For a complete description of all compiler switches given the
;; current optimization settings evaluate (explain-compiler-settings).
;;---
;; Current reader case mode: :case-sensitive-lower

pvs(1): 
pvs(2): 

Invar :  

  |-------
{1}   FORALL (iL_: IL, i_: SCI):
        (EXISTS (i: below(puInputN)): i_`pbInput(i)) IMPLIES curSCD(cons(i_, iL_))`dOutputD`bOutput

Rule? (induct "iL_")
Inducting on iL_ on formula 1,
this yields  2 subgoals: 
Invar.1 :  

  |-------
{1}   FORALL (i_: SCI):
        (EXISTS (i: below(puInputN)): i_`pbInput(i)) IMPLIES curSCD(cons(i_, null))`dOutputD`bOutput

Rule? (grind$)
Auto-rewriting with all the definitions relevant to conjecture,
this simplifies to: 
Invar.1 :  

  |-------
[1]   FORALL (i_: SCI):
        (EXISTS (i: below(puInputN)): i_`pbInput(i)) IMPLIES curSCD(cons(i_, null))`dOutputD`bOutput

No change on: (auto-rewrite-theories :theories nil)
Invar.1 :  

  |-------
[1]   FORALL (i_: SCI):
        (EXISTS (i: below(puInputN)): i_`pbInput(i)) IMPLIES curSCD(cons(i_, null))`dOutputD`bOutput

No change on: (auto-rewrite :names nil)
Invar.1 :  

  |-------
[1]   FORALL (i_: SCI):
        (EXISTS (i: below(puInputN)): i_`pbInput(i)) IMPLIES curSCD(cons(i_, null))`dOutputD`bOutput

No change on: (skip)
Invar.1 :  

  |-------
[1]   FORALL (i_: SCI):
        (EXISTS (i: below(puInputN)): i_`pbInput(i)) IMPLIES curSCD(cons(i_, null))`dOutputD`bOutput

No change on: (skip)
Invar.1 :  

  |-------
[1]   FORALL (i_: SCI):
        (EXISTS (i: below(puInputN)): i_`pbInput(i)) IMPLIES curSCD(cons(i_, null))`dOutputD`bOutput

Postponing Invar.1.

Invar.1 :  

  |-------
[1]   FORALL (i_: SCI):
        (EXISTS (i: below(puInputN)): i_`pbInput(i)) IMPLIES curSCD(cons(i_, null))`dOutputD`bOutput

No change on: (bddsimp)
Invar.1 :  

  |-------
[1]   FORALL (i_: SCI):
        (EXISTS (i: below(puInputN)): i_`pbInput(i)) IMPLIES curSCD(cons(i_, null))`dOutputD`bOutput

initD rewrites UInput.initD
  to (# bInput := FALSE, sState := sS0 #)
initD rewrites DOutput.initD
  to (# oCnt := 0, sState := sPassive, bOutput := FALSE #)
initSCD rewrites initSCD
  to (# puInputD := LAMBDA (i: below(puInputN)): (# bInput := FALSE, sState := sS0 #),
         dOutputD := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #)
curSCD rewrites curSCD(null)
  to (# puInputD := LAMBDA (i: below(puInputN)): (# bInput := FALSE, sState := sS0 #),
         dOutputD := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #)
sCDIM rewrites 
  sCDIM(i_,
        (# puInputD := LAMBDA (i: below(puInputN)): (# bInput := FALSE, sState := sS0 #),
           dOutputD := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))
  to (# puInputD := LAMBDA (i_1: below(puInputN)): (# bInput := i_`pbInput(i_1), sState := sS0 #),
         dOutputD := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #)
tF rewrites 
  DOutput.tF
      ((# dOutputD
            := puInputTF(puInputN,
                         (# puInputD
                              := LAMBDA (i_1: below(puInputN)):
                                   (# bInput := i_`pbInput(i_1), sState := sS0 #),
                            dOutputD
                              := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))`dOutputD #))
  to COND sPassive?(puInputTF(puInputN,
                               (# puInputD
                                    := LAMBDA (i_1: below(puInputN)):
                                         (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                  dOutputD
                                    := (# oCnt := 0,
                                          sState := sPassive,
                                          bOutput := FALSE #) #))`dOutputD`sState)
             ->
             IF puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i_`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`oCnt
                 > 0
               THEN (# dOutputD
                         := puInputTF(puInputN,
                                      (# puInputD
                                           := LAMBDA (i_1: below(puInputN)):
                                                (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                         dOutputD
                                           := (# oCnt := 0,
                                                 sState := sPassive,
                                                 bOutput := FALSE #) #))`dOutputD
                              WITH [sState := sActive, bOutput := TRUE] #)
             ELSE (# dOutputD
                       := puInputTF(puInputN,
                                    (# puInputD
                                         := LAMBDA (i_1: below(puInputN)):
                                              (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                       dOutputD
                                         := (# oCnt := 0,
                                               sState := sPassive,
                                               bOutput := FALSE #) #))`dOutputD #)
             ENDIF,
           ELSE ->
             IF puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i_`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`oCnt
                 = 0
               THEN (# dOutputD
                         := puInputTF(puInputN,
                                      (# puInputD
                                           := LAMBDA (i_1: below(puInputN)):
                                                (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                         dOutputD
                                           := (# oCnt := 0,
                                                 sState := sPassive,
                                                 bOutput := FALSE #) #))`dOutputD
                              WITH [sState := sPassive, bOutput := FALSE] #)
             ELSE (# dOutputD
                       := puInputTF(puInputN,
                                    (# puInputD
                                         := LAMBDA (i_1: below(puInputN)):
                                              (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                       dOutputD
                                         := (# oCnt := 0,
                                               sState := sPassive,
                                               bOutput := FALSE #) #))`dOutputD #)
             ENDIF
      ENDCOND
uOutputTF rewrites 
  uOutputTF(puInputTF(puInputN,
                      (# puInputD
                           := LAMBDA (i_1: below(puInputN)):
                                (# bInput := i_`pbInput(i_1), sState := sS0 #),
                         dOutputD := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #)))
  to puInputTF(puInputN,
                (# puInputD
                     := LAMBDA (i_1: below(puInputN)): (# bInput := i_`pbInput(i_1), sState := sS0 #),
                   dOutputD := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))
        WITH [dOutputD
                := IF sPassive?(puInputTF(puInputN,
                                          (# puInputD
                                               := LAMBDA (i_1: below(puInputN)):
                                                    (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                             dOutputD
                                               := (# oCnt := 0,
                                                     sState := sPassive,
                                                     bOutput := FALSE #) #))`dOutputD`sState)
                     THEN IF puInputTF(puInputN,
                                       (# puInputD
                                            := LAMBDA (i_1: below(puInputN)):
                                                 (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                          dOutputD
                                            := (# oCnt := 0,
                                                  sState := sPassive,
                                                  bOutput := FALSE #) #))`dOutputD`oCnt
                              > 0
                            THEN puInputTF(puInputN,
                                           (# puInputD
                                                := LAMBDA (i_1: below(puInputN)):
                                                     (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                              dOutputD
                                                := (# oCnt := 0,
                                                      sState := sPassive,
                                                      bOutput := FALSE #) #))`dOutputD
                                   WITH [sState := sActive, bOutput := TRUE]
                          ELSE puInputTF(puInputN,
                                         (# puInputD
                                              := LAMBDA (i_1: below(puInputN)):
                                                   (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                            dOutputD
                                              := (# oCnt := 0,
                                                    sState := sPassive,
                                                    bOutput := FALSE #) #))`dOutputD
                          ENDIF
                   ELSE IF puInputTF(puInputN,
                                     (# puInputD
                                          := LAMBDA (i_1: below(puInputN)):
                                               (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                        dOutputD
                                          := (# oCnt := 0,
                                                sState := sPassive,
                                                bOutput := FALSE #) #))`dOutputD`oCnt
                            = 0
                          THEN puInputTF(puInputN,
                                         (# puInputD
                                              := LAMBDA (i_1: below(puInputN)):
                                                   (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                            dOutputD
                                              := (# oCnt := 0,
                                                    sState := sPassive,
                                                    bOutput := FALSE #) #))`dOutputD
                                 WITH [sState := sPassive, bOutput := FALSE]
                        ELSE puInputTF(puInputN,
                                       (# puInputD
                                            := LAMBDA (i_1: below(puInputN)):
                                                 (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                          dOutputD
                                            := (# oCnt := 0,
                                                  sState := sPassive,
                                                  bOutput := FALSE #) #))`dOutputD
                        ENDIF
                   ENDIF]
sCDTF rewrites 
  sCDTF(i_,
        (# puInputD := LAMBDA (i: below(puInputN)): (# bInput := FALSE, sState := sS0 #),
           dOutputD := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))
  to puInputTF(puInputN,
                (# puInputD
                     := LAMBDA (i_1: below(puInputN)): (# bInput := i_`pbInput(i_1), sState := sS0 #),
                   dOutputD := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))
        WITH [dOutputD
                := IF sPassive?(puInputTF(puInputN,
                                          (# puInputD
                                               := LAMBDA (i_1: below(puInputN)):
                                                    (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                             dOutputD
                                               := (# oCnt := 0,
                                                     sState := sPassive,
                                                     bOutput := FALSE #) #))`dOutputD`sState)
                     THEN IF puInputTF(puInputN,
                                       (# puInputD
                                            := LAMBDA (i_1: below(puInputN)):
                                                 (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                          dOutputD
                                            := (# oCnt := 0,
                                                  sState := sPassive,
                                                  bOutput := FALSE #) #))`dOutputD`oCnt
                              > 0
                            THEN puInputTF(puInputN,
                                           (# puInputD
                                                := LAMBDA (i_1: below(puInputN)):
                                                     (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                              dOutputD
                                                := (# oCnt := 0,
                                                      sState := sPassive,
                                                      bOutput := FALSE #) #))`dOutputD
                                   WITH [sState := sActive, bOutput := TRUE]
                          ELSE puInputTF(puInputN,
                                         (# puInputD
                                              := LAMBDA (i_1: below(puInputN)):
                                                   (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                            dOutputD
                                              := (# oCnt := 0,
                                                    sState := sPassive,
                                                    bOutput := FALSE #) #))`dOutputD
                          ENDIF
                   ELSE IF puInputTF(puInputN,
                                     (# puInputD
                                          := LAMBDA (i_1: below(puInputN)):
                                               (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                        dOutputD
                                          := (# oCnt := 0,
                                                sState := sPassive,
                                                bOutput := FALSE #) #))`dOutputD`oCnt
                            = 0
                          THEN puInputTF(puInputN,
                                         (# puInputD
                                              := LAMBDA (i_1: below(puInputN)):
                                                   (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                            dOutputD
                                              := (# oCnt := 0,
                                                    sState := sPassive,
                                                    bOutput := FALSE #) #))`dOutputD
                                 WITH [sState := sPassive, bOutput := FALSE]
                        ELSE puInputTF(puInputN,
                                       (# puInputD
                                            := LAMBDA (i_1: below(puInputN)):
                                                 (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                          dOutputD
                                            := (# oCnt := 0,
                                                  sState := sPassive,
                                                  bOutput := FALSE #) #))`dOutputD
                        ENDIF
                   ENDIF]
curSCD rewrites curSCD(cons(i_, null))
  to puInputTF(puInputN,
                (# puInputD
                     := LAMBDA (i_1: below(puInputN)): (# bInput := i_`pbInput(i_1), sState := sS0 #),
                   dOutputD := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))
        WITH [dOutputD
                := IF sPassive?(puInputTF(puInputN,
                                          (# puInputD
                                               := LAMBDA (i_1: below(puInputN)):
                                                    (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                             dOutputD
                                               := (# oCnt := 0,
                                                     sState := sPassive,
                                                     bOutput := FALSE #) #))`dOutputD`sState)
                     THEN IF puInputTF(puInputN,
                                       (# puInputD
                                            := LAMBDA (i_1: below(puInputN)):
                                                 (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                          dOutputD
                                            := (# oCnt := 0,
                                                  sState := sPassive,
                                                  bOutput := FALSE #) #))`dOutputD`oCnt
                              > 0
                            THEN puInputTF(puInputN,
                                           (# puInputD
                                                := LAMBDA (i_1: below(puInputN)):
                                                     (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                              dOutputD
                                                := (# oCnt := 0,
                                                      sState := sPassive,
                                                      bOutput := FALSE #) #))`dOutputD
                                   WITH [sState := sActive, bOutput := TRUE]
                          ELSE puInputTF(puInputN,
                                         (# puInputD
                                              := LAMBDA (i_1: below(puInputN)):
                                                   (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                            dOutputD
                                              := (# oCnt := 0,
                                                    sState := sPassive,
                                                    bOutput := FALSE #) #))`dOutputD
                          ENDIF
                   ELSE IF puInputTF(puInputN,
                                     (# puInputD
                                          := LAMBDA (i_1: below(puInputN)):
                                               (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                        dOutputD
                                          := (# oCnt := 0,
                                                sState := sPassive,
                                                bOutput := FALSE #) #))`dOutputD`oCnt
                            = 0
                          THEN puInputTF(puInputN,
                                         (# puInputD
                                              := LAMBDA (i_1: below(puInputN)):
                                                   (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                            dOutputD
                                              := (# oCnt := 0,
                                                    sState := sPassive,
                                                    bOutput := FALSE #) #))`dOutputD
                                 WITH [sState := sPassive, bOutput := FALSE]
                        ELSE puInputTF(puInputN,
                                       (# puInputD
                                            := LAMBDA (i_1: below(puInputN)):
                                                 (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                          dOutputD
                                            := (# oCnt := 0,
                                                  sState := sPassive,
                                                  bOutput := FALSE #) #))`dOutputD
                        ENDIF
                   ENDIF]
Simplifying, rewriting, and recording with decision procedures,
this simplifies to: 
Invar.1 :  

  |-------
{1}   FORALL (i_: SCI):
        (EXISTS (i: below(puInputN)): i_`pbInput(i)) IMPLIES
         IF sPassive?(puInputTF(puInputN,
                                (# puInputD
                                     := LAMBDA (i_1: below(puInputN)):
                                          (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                   dOutputD
                                     := (# oCnt := 0,
                                           sState := sPassive,
                                           bOutput := FALSE #) #))`dOutputD`sState)
           THEN IF puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`oCnt
                    > 0
                  THEN TRUE
                ELSE puInputTF(puInputN,
                               (# puInputD
                                    := LAMBDA (i_1: below(puInputN)):
                                         (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                  dOutputD
                                    := (# oCnt := 0,
                                          sState := sPassive,
                                          bOutput := FALSE #) #))`dOutputD`bOutput
                ENDIF
         ELSE IF puInputTF(puInputN,
                           (# puInputD
                                := LAMBDA (i_1: below(puInputN)):
                                     (# bInput := i_`pbInput(i_1), sState := sS0 #),
                              dOutputD
                                := (# oCnt := 0,
                                      sState := sPassive,
                                      bOutput := FALSE #) #))`dOutputD`oCnt
                  = 0
                THEN FALSE
              ELSE puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`bOutput
              ENDIF
         ENDIF

Postponing Invar.1.

Invar.1 :  

  |-------
{1}   FORALL (i_: SCI):
        (EXISTS (i: below(puInputN)): i_`pbInput(i)) IMPLIES
         IF sPassive?(puInputTF(puInputN,
                                (# puInputD
                                     := LAMBDA (i_1: below(puInputN)):
                                          (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                   dOutputD
                                     := (# oCnt := 0,
                                           sState := sPassive,
                                           bOutput := FALSE #) #))`dOutputD`sState)
           THEN IF puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`oCnt
                    > 0
                  THEN TRUE
                ELSE puInputTF(puInputN,
                               (# puInputD
                                    := LAMBDA (i_1: below(puInputN)):
                                         (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                  dOutputD
                                    := (# oCnt := 0,
                                          sState := sPassive,
                                          bOutput := FALSE #) #))`dOutputD`bOutput
                ENDIF
         ELSE IF puInputTF(puInputN,
                           (# puInputD
                                := LAMBDA (i_1: below(puInputN)):
                                     (# bInput := i_`pbInput(i_1), sState := sS0 #),
                              dOutputD
                                := (# oCnt := 0,
                                      sState := sPassive,
                                      bOutput := FALSE #) #))`dOutputD`oCnt
                  = 0
                THEN FALSE
              ELSE puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`bOutput
              ENDIF
         ENDIF

No change on: (replace*)
Invar.1 :  

  |-------
{1}   FORALL (i_: SCI):
        (EXISTS (i: below(puInputN)): i_`pbInput(i)) IMPLIES
         IF sPassive?(puInputTF(puInputN,
                                (# puInputD
                                     := LAMBDA (i_1: below(puInputN)):
                                          (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                   dOutputD
                                     := (# oCnt := 0,
                                           sState := sPassive,
                                           bOutput := FALSE #) #))`dOutputD`sState)
           THEN IF puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`oCnt
                    > 0
                  THEN TRUE
                ELSE puInputTF(puInputN,
                               (# puInputD
                                    := LAMBDA (i_1: below(puInputN)):
                                         (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                  dOutputD
                                    := (# oCnt := 0,
                                          sState := sPassive,
                                          bOutput := FALSE #) #))`dOutputD`bOutput
                ENDIF
         ELSE IF puInputTF(puInputN,
                           (# puInputD
                                := LAMBDA (i_1: below(puInputN)):
                                     (# bInput := i_`pbInput(i_1), sState := sS0 #),
                              dOutputD
                                := (# oCnt := 0,
                                      sState := sPassive,
                                      bOutput := FALSE #) #))`dOutputD`oCnt
                  = 0
                THEN FALSE
              ELSE puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`bOutput
              ENDIF
         ENDIF

No change on: (assert :let-reduce? t :quant-simp? nil
                      :implicit-typepreds? nil :cases-rewrite? nil)
Invar.1 :  

  |-------
[1]   FORALL (i_: SCI):
        (EXISTS (i: below(puInputN)): i_`pbInput(i)) IMPLIES
         IF sPassive?(puInputTF(puInputN,
                                (# puInputD
                                     := LAMBDA (i_1: below(puInputN)):
                                          (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                   dOutputD
                                     := (# oCnt := 0,
                                           sState := sPassive,
                                           bOutput := FALSE #) #))`dOutputD`sState)
           THEN IF puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`oCnt
                    > 0
                  THEN TRUE
                ELSE puInputTF(puInputN,
                               (# puInputD
                                    := LAMBDA (i_1: below(puInputN)):
                                         (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                  dOutputD
                                    := (# oCnt := 0,
                                          sState := sPassive,
                                          bOutput := FALSE #) #))`dOutputD`bOutput
                ENDIF
         ELSE IF puInputTF(puInputN,
                           (# puInputD
                                := LAMBDA (i_1: below(puInputN)):
                                     (# bInput := i_`pbInput(i_1), sState := sS0 #),
                              dOutputD
                                := (# oCnt := 0,
                                      sState := sPassive,
                                      bOutput := FALSE #) #))`dOutputD`oCnt
                  = 0
                THEN FALSE
              ELSE puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`bOutput
              ENDIF
         ENDIF

No change on: (bddsimp)
Invar.1 :  

  |-------
[1]   FORALL (i_: SCI):
        (EXISTS (i: below(puInputN)): i_`pbInput(i)) IMPLIES
         IF sPassive?(puInputTF(puInputN,
                                (# puInputD
                                     := LAMBDA (i_1: below(puInputN)):
                                          (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                   dOutputD
                                     := (# oCnt := 0,
                                           sState := sPassive,
                                           bOutput := FALSE #) #))`dOutputD`sState)
           THEN IF puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`oCnt
                    > 0
                  THEN TRUE
                ELSE puInputTF(puInputN,
                               (# puInputD
                                    := LAMBDA (i_1: below(puInputN)):
                                         (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                  dOutputD
                                    := (# oCnt := 0,
                                          sState := sPassive,
                                          bOutput := FALSE #) #))`dOutputD`bOutput
                ENDIF
         ELSE IF puInputTF(puInputN,
                           (# puInputD
                                := LAMBDA (i_1: below(puInputN)):
                                     (# bInput := i_`pbInput(i_1), sState := sS0 #),
                              dOutputD
                                := (# oCnt := 0,
                                      sState := sPassive,
                                      bOutput := FALSE #) #))`dOutputD`oCnt
                  = 0
                THEN FALSE
              ELSE puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`bOutput
              ENDIF
         ENDIF

Couldn't find a suitable quantified formula.
No change on: (inst? :if-match t :polarity? nil)
Invar.1 :  

  |-------
[1]   FORALL (i_: SCI):
        (EXISTS (i: below(puInputN)): i_`pbInput(i)) IMPLIES
         IF sPassive?(puInputTF(puInputN,
                                (# puInputD
                                     := LAMBDA (i_1: below(puInputN)):
                                          (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                   dOutputD
                                     := (# oCnt := 0,
                                           sState := sPassive,
                                           bOutput := FALSE #) #))`dOutputD`sState)
           THEN IF puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`oCnt
                    > 0
                  THEN TRUE
                ELSE puInputTF(puInputN,
                               (# puInputD
                                    := LAMBDA (i_1: below(puInputN)):
                                         (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                  dOutputD
                                    := (# oCnt := 0,
                                          sState := sPassive,
                                          bOutput := FALSE #) #))`dOutputD`bOutput
                ENDIF
         ELSE IF puInputTF(puInputN,
                           (# puInputD
                                := LAMBDA (i_1: below(puInputN)):
                                     (# bInput := i_`pbInput(i_1), sState := sS0 #),
                              dOutputD
                                := (# oCnt := 0,
                                      sState := sPassive,
                                      bOutput := FALSE #) #))`dOutputD`oCnt
                  = 0
                THEN FALSE
              ELSE puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i_`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`bOutput
              ENDIF
         ENDIF

Skolemizing (with typepred on new Skolem constants),
this simplifies to: 
Invar.1 :  

  |-------
{1}   (EXISTS (i: below(puInputN)): i!1`pbInput(i)) IMPLIES
       IF sPassive?(puInputTF(puInputN,
                              (# puInputD
                                   := LAMBDA (i_1: below(puInputN)):
                                        (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                                 dOutputD
                                   := (# oCnt := 0,
                                         sState := sPassive,
                                         bOutput := FALSE #) #))`dOutputD`sState)
         THEN IF puInputTF(puInputN,
                           (# puInputD
                                := LAMBDA (i_1: below(puInputN)):
                                     (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                              dOutputD
                                := (# oCnt := 0,
                                      sState := sPassive,
                                      bOutput := FALSE #) #))`dOutputD`oCnt
                  > 0
                THEN TRUE
              ELSE puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`bOutput
              ENDIF
       ELSE IF puInputTF(puInputN,
                         (# puInputD
                              := LAMBDA (i_1: below(puInputN)):
                                   (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                            dOutputD
                              := (# oCnt := 0,
                                    sState := sPassive,
                                    bOutput := FALSE #) #))`dOutputD`oCnt
                = 0
              THEN FALSE
            ELSE puInputTF(puInputN,
                           (# puInputD
                                := LAMBDA (i_1: below(puInputN)):
                                     (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                              dOutputD
                                := (# oCnt := 0,
                                      sState := sPassive,
                                      bOutput := FALSE #) #))`dOutputD`bOutput
            ENDIF
       ENDIF

Applying disjunctive simplification to flatten sequent,
this simplifies to: 
Invar.1 :  

{-1}  EXISTS (i: below(puInputN)): i!1`pbInput(i)
  |-------
{1}   IF sPassive?(puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`sState)
        THEN IF puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`oCnt
                 > 0
               THEN TRUE
             ELSE puInputTF(puInputN,
                            (# puInputD
                                 := LAMBDA (i_1: below(puInputN)):
                                      (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                               dOutputD
                                 := (# oCnt := 0,
                                       sState := sPassive,
                                       bOutput := FALSE #) #))`dOutputD`bOutput
             ENDIF
      ELSE IF puInputTF(puInputN,
                        (# puInputD
                             := LAMBDA (i_1: below(puInputN)):
                                  (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                           dOutputD
                             := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))`dOutputD`oCnt
               = 0
             THEN FALSE
           ELSE puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`bOutput
           ENDIF
      ENDIF

Postponing Invar.1.

Invar.1 :  

{-1}  EXISTS (i: below(puInputN)): i!1`pbInput(i)
  |-------
{1}   IF sPassive?(puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`sState)
        THEN IF puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`oCnt
                 > 0
               THEN TRUE
             ELSE puInputTF(puInputN,
                            (# puInputD
                                 := LAMBDA (i_1: below(puInputN)):
                                      (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                               dOutputD
                                 := (# oCnt := 0,
                                       sState := sPassive,
                                       bOutput := FALSE #) #))`dOutputD`bOutput
             ENDIF
      ELSE IF puInputTF(puInputN,
                        (# puInputD
                             := LAMBDA (i_1: below(puInputN)):
                                  (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                           dOutputD
                             := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))`dOutputD`oCnt
               = 0
             THEN FALSE
           ELSE puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`bOutput
           ENDIF
      ENDIF

Skolemizing (with typepred on new Skolem constants),
this simplifies to: 
Invar.1 :  

{-1}  i!2 < puInputN
{-2}  i!1`pbInput(i!2)
  |-------
[1]   IF sPassive?(puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`sState)
        THEN IF puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`oCnt
                 > 0
               THEN TRUE
             ELSE puInputTF(puInputN,
                            (# puInputD
                                 := LAMBDA (i_1: below(puInputN)):
                                      (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                               dOutputD
                                 := (# oCnt := 0,
                                       sState := sPassive,
                                       bOutput := FALSE #) #))`dOutputD`bOutput
             ENDIF
      ELSE IF puInputTF(puInputN,
                        (# puInputD
                             := LAMBDA (i_1: below(puInputN)):
                                  (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                           dOutputD
                             := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))`dOutputD`oCnt
               = 0
             THEN FALSE
           ELSE puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`bOutput
           ENDIF
      ENDIF

No change on: (flatten)
Invar.1 :  

{-1}  i!2 < puInputN
{-2}  i!1`pbInput(i!2)
  |-------
[1]   IF sPassive?(puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`sState)
        THEN IF puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`oCnt
                 > 0
               THEN TRUE
             ELSE puInputTF(puInputN,
                            (# puInputD
                                 := LAMBDA (i_1: below(puInputN)):
                                      (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                               dOutputD
                                 := (# oCnt := 0,
                                       sState := sPassive,
                                       bOutput := FALSE #) #))`dOutputD`bOutput
             ENDIF
      ELSE IF puInputTF(puInputN,
                        (# puInputD
                             := LAMBDA (i_1: below(puInputN)):
                                  (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                           dOutputD
                             := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))`dOutputD`oCnt
               = 0
             THEN FALSE
           ELSE puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`bOutput
           ENDIF
      ENDIF

Postponing Invar.1.

Invar.1 :  

{-1}  i!2 < puInputN
{-2}  i!1`pbInput(i!2)
  |-------
[1]   IF sPassive?(puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`sState)
        THEN IF puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`oCnt
                 > 0
               THEN TRUE
             ELSE puInputTF(puInputN,
                            (# puInputD
                                 := LAMBDA (i_1: below(puInputN)):
                                      (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                               dOutputD
                                 := (# oCnt := 0,
                                       sState := sPassive,
                                       bOutput := FALSE #) #))`dOutputD`bOutput
             ENDIF
      ELSE IF puInputTF(puInputN,
                        (# puInputD
                             := LAMBDA (i_1: below(puInputN)):
                                  (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                           dOutputD
                             := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))`dOutputD`oCnt
               = 0
             THEN FALSE
           ELSE puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`bOutput
           ENDIF
      ENDIF

No suitable (+ve FORALL/-ve EXISTS) quantified expression found.

No change on: (skolem-typepred)
Invar.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   IF sPassive?(puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`sState)
        THEN IF puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`oCnt
                 > 0
               THEN TRUE
             ELSE puInputTF(puInputN,
                            (# puInputD
                                 := LAMBDA (i_1: below(puInputN)):
                                      (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                               dOutputD
                                 := (# oCnt := 0,
                                       sState := sPassive,
                                       bOutput := FALSE #) #))`dOutputD`bOutput
             ENDIF
      ELSE IF puInputTF(puInputN,
                        (# puInputD
                             := LAMBDA (i_1: below(puInputN)):
                                  (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                           dOutputD
                             := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))`dOutputD`oCnt
               = 0
             THEN FALSE
           ELSE puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`bOutput
           ENDIF
      ENDIF

No change on: (flatten)
Invar.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   IF sPassive?(puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`sState)
        THEN IF puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`oCnt
                 > 0
               THEN TRUE
             ELSE puInputTF(puInputN,
                            (# puInputD
                                 := LAMBDA (i_1: below(puInputN)):
                                      (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                               dOutputD
                                 := (# oCnt := 0,
                                       sState := sPassive,
                                       bOutput := FALSE #) #))`dOutputD`bOutput
             ENDIF
      ELSE IF puInputTF(puInputN,
                        (# puInputD
                             := LAMBDA (i_1: below(puInputN)):
                                  (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                           dOutputD
                             := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))`dOutputD`oCnt
               = 0
             THEN FALSE
           ELSE puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`bOutput
           ENDIF
      ENDIF

Postponing Invar.1.

Invar.1 :  

{-1}  i!2 < puInputN
{-2}  i!1`pbInput(i!2)
  |-------
[1]   IF sPassive?(puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`sState)
        THEN IF puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`oCnt
                 > 0
               THEN TRUE
             ELSE puInputTF(puInputN,
                            (# puInputD
                                 := LAMBDA (i_1: below(puInputN)):
                                      (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                               dOutputD
                                 := (# oCnt := 0,
                                       sState := sPassive,
                                       bOutput := FALSE #) #))`dOutputD`bOutput
             ENDIF
      ELSE IF puInputTF(puInputN,
                        (# puInputD
                             := LAMBDA (i_1: below(puInputN)):
                                  (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                           dOutputD
                             := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))`dOutputD`oCnt
               = 0
             THEN FALSE
           ELSE puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`bOutput
           ENDIF
      ENDIF

No change on: (skip)
Invar.1 :  

{-1}  i!2 < puInputN
{-2}  i!1`pbInput(i!2)
  |-------
[1]   IF sPassive?(puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`sState)
        THEN IF puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`oCnt
                 > 0
               THEN TRUE
             ELSE puInputTF(puInputN,
                            (# puInputD
                                 := LAMBDA (i_1: below(puInputN)):
                                      (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                               dOutputD
                                 := (# oCnt := 0,
                                       sState := sPassive,
                                       bOutput := FALSE #) #))`dOutputD`bOutput
             ENDIF
      ELSE IF puInputTF(puInputN,
                        (# puInputD
                             := LAMBDA (i_1: below(puInputN)):
                                  (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                           dOutputD
                             := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))`dOutputD`oCnt
               = 0
             THEN FALSE
           ELSE puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`bOutput
           ENDIF
      ENDIF

Postponing Invar.1.

Invar.1 :  

{-1}  i!2 < puInputN
{-2}  i!1`pbInput(i!2)
  |-------
[1]   IF sPassive?(puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`sState)
        THEN IF puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`oCnt
                 > 0
               THEN TRUE
             ELSE puInputTF(puInputN,
                            (# puInputD
                                 := LAMBDA (i_1: below(puInputN)):
                                      (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                               dOutputD
                                 := (# oCnt := 0,
                                       sState := sPassive,
                                       bOutput := FALSE #) #))`dOutputD`bOutput
             ENDIF
      ELSE IF puInputTF(puInputN,
                        (# puInputD
                             := LAMBDA (i_1: below(puInputN)):
                                  (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                           dOutputD
                             := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))`dOutputD`oCnt
               = 0
             THEN FALSE
           ELSE puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`bOutput
           ENDIF
      ENDIF

No change on: (lift-if :updates? t)
Invar.1 :  

{-1}  i!2 < puInputN
{-2}  i!1`pbInput(i!2)
  |-------
[1]   IF sPassive?(puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`sState)
        THEN IF puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`oCnt
                 > 0
               THEN TRUE
             ELSE puInputTF(puInputN,
                            (# puInputD
                                 := LAMBDA (i_1: below(puInputN)):
                                      (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                               dOutputD
                                 := (# oCnt := 0,
                                       sState := sPassive,
                                       bOutput := FALSE #) #))`dOutputD`bOutput
             ENDIF
      ELSE IF puInputTF(puInputN,
                        (# puInputD
                             := LAMBDA (i_1: below(puInputN)):
                                  (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                           dOutputD
                             := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))`dOutputD`oCnt
               = 0
             THEN FALSE
           ELSE puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`bOutput
           ENDIF
      ENDIF

Postponing Invar.1.

Invar.1 :  

{-1}  i!2 < puInputN
{-2}  i!1`pbInput(i!2)
  |-------
[1]   IF sPassive?(puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`sState)
        THEN IF puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`oCnt
                 > 0
               THEN TRUE
             ELSE puInputTF(puInputN,
                            (# puInputD
                                 := LAMBDA (i_1: below(puInputN)):
                                      (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                               dOutputD
                                 := (# oCnt := 0,
                                       sState := sPassive,
                                       bOutput := FALSE #) #))`dOutputD`bOutput
             ENDIF
      ELSE IF puInputTF(puInputN,
                        (# puInputD
                             := LAMBDA (i_1: below(puInputN)):
                                  (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                           dOutputD
                             := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))`dOutputD`oCnt
               = 0
             THEN FALSE
           ELSE puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`bOutput
           ENDIF
      ENDIF

No change on: (replace*)
Invar.1 :  

{-1}  i!2 < puInputN
{-2}  i!1`pbInput(i!2)
  |-------
[1]   IF sPassive?(puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`sState)
        THEN IF puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`oCnt
                 > 0
               THEN TRUE
             ELSE puInputTF(puInputN,
                            (# puInputD
                                 := LAMBDA (i_1: below(puInputN)):
                                      (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                               dOutputD
                                 := (# oCnt := 0,
                                       sState := sPassive,
                                       bOutput := FALSE #) #))`dOutputD`bOutput
             ENDIF
      ELSE IF puInputTF(puInputN,
                        (# puInputD
                             := LAMBDA (i_1: below(puInputN)):
                                  (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                           dOutputD
                             := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))`dOutputD`oCnt
               = 0
             THEN FALSE
           ELSE puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`bOutput
           ENDIF
      ENDIF

Postponing Invar.1.

Invar.1 :  

{-1}  i!2 < puInputN
{-2}  i!1`pbInput(i!2)
  |-------
[1]   IF sPassive?(puInputTF(puInputN,
                             (# puInputD
                                  := LAMBDA (i_1: below(puInputN)):
                                       (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                                dOutputD
                                  := (# oCnt := 0,
                                        sState := sPassive,
                                        bOutput := FALSE #) #))`dOutputD`sState)
        THEN IF puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`oCnt
                 > 0
               THEN TRUE
             ELSE puInputTF(puInputN,
                            (# puInputD
                                 := LAMBDA (i_1: below(puInputN)):
                                      (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                               dOutputD
                                 := (# oCnt := 0,
                                       sState := sPassive,
                                       bOutput := FALSE #) #))`dOutputD`bOutput
             ENDIF
      ELSE IF puInputTF(puInputN,
                        (# puInputD
                             := LAMBDA (i_1: below(puInputN)):
                                  (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                           dOutputD
                             := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))`dOutputD`oCnt
               = 0
             THEN FALSE
           ELSE puInputTF(puInputN,
                          (# puInputD
                               := LAMBDA (i_1: below(puInputN)):
                                    (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                             dOutputD
                               := (# oCnt := 0,
                                     sState := sPassive,
                                     bOutput := FALSE #) #))`dOutputD`bOutput
           ENDIF
      ENDIF

succ rewrites succ(0)
  to 1
tF rewrites 
  UInput.tF
      ((# uInputD := (# bInput := i!1`pbInput(puInputN - 1), sState := sS0 #),
          dOutputD := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))
  to IF i!1`pbInput(puInputN - 1)
        THEN (# uInputD := (# bInput := TRUE, sState := sS1 #),
                dOutputD := (# oCnt := 1, sState := sPassive, bOutput := FALSE #) #)
      ELSE (# uInputD := (# bInput := FALSE, sState := sS0 #),
              dOutputD := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #)
      ENDIF
puInputTF rewrites 
  puInputTF(puInputN,
            (# puInputD
                 := LAMBDA (i_1: below(puInputN)): (# bInput := i!1`pbInput(i_1), sState := sS0 #),
               dOutputD := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))
  to puInputTF(puInputN - 1,
                (# puInputD
                     := LAMBDA (i_1: below(puInputN)): (# bInput := i!1`pbInput(i_1), sState := sS0 #),
                   dOutputD := (# oCnt := 0, sState := sPassive, bOutput := FALSE #) #))
        WITH [puInputD
                := (LAMBDA (i_1: below(puInputN)): (# bInput := i!1`pbInput(i_1), sState := sS0 #))
                     WITH [(puInputN - 1)
                             := IF i!1`pbInput(puInputN - 1) THEN (# bInput := TRUE, sState := sS1 #)
                                ELSE (# bInput := FALSE, sState := sS0 #)
                                ENDIF],
              dOutputD
                := IF i!1`pbInput(puInputN - 1)
                     THEN (# oCnt := 1, sState := sPassive, bOutput := FALSE #)
                   ELSE (# oCnt := 0, sState := sPassive, bOutput := FALSE #)
                   ENDIF]
Simplifying, rewriting, and recording with decision procedures,
this simplifies to: 
Invar.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   IF sPassive?(IF i!1`pbInput(puInputN - 1) THEN sPassive ELSE sPassive ENDIF)
        THEN IF IF i!1`pbInput(puInputN - 1) THEN 1 ELSE 0 ENDIF > 0 THEN TRUE
             ELSE IF i!1`pbInput(puInputN - 1) THEN FALSE ELSE FALSE ENDIF
             ENDIF
      ELSE IF IF i!1`pbInput(puInputN - 1) THEN 1 ELSE 0 ENDIF = 0 THEN FALSE
           ELSE IF i!1`pbInput(puInputN - 1) THEN FALSE ELSE FALSE ENDIF
           ENDIF
      ENDIF

Applying bddsimp,
this yields  2 subgoals: 
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   IF i!1`pbInput(puInputN - 1) THEN 1 ELSE 0 ENDIF > 0

Couldn't find a suitable quantified formula.
No change on: (inst? :if-match t :polarity? nil)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   IF i!1`pbInput(puInputN - 1) THEN 1 ELSE 0 ENDIF > 0

No suitable (+ve FORALL/-ve EXISTS) quantified expression found.

No change on: (skolem-typepred)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   IF i!1`pbInput(puInputN - 1) THEN 1 ELSE 0 ENDIF > 0

No change on: (flatten)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   IF i!1`pbInput(puInputN - 1) THEN 1 ELSE 0 ENDIF > 0

Postponing Invar.1.1.

Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   IF i!1`pbInput(puInputN - 1) THEN 1 ELSE 0 ENDIF > 0

No change on: (skip)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   IF i!1`pbInput(puInputN - 1) THEN 1 ELSE 0 ENDIF > 0

Postponing Invar.1.1.

Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   IF i!1`pbInput(puInputN - 1) THEN 1 ELSE 0 ENDIF > 0

Lifting IF-conditions to the top level,
this simplifies to: 
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   IF i!1`pbInput(puInputN - 1) THEN 1 > 0 ELSE 0 > 0 ENDIF

Postponing Invar.1.1.

Invar.1.2 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   sPassive?(IF i!1`pbInput(puInputN - 1) THEN sPassive ELSE sPassive ENDIF)

Couldn't find a suitable quantified formula.
No change on: (inst? :if-match t :polarity? nil)
Invar.1.2 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   sPassive?(IF i!1`pbInput(puInputN - 1) THEN sPassive ELSE sPassive ENDIF)

No suitable (+ve FORALL/-ve EXISTS) quantified expression found.

No change on: (skolem-typepred)
Invar.1.2 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   sPassive?(IF i!1`pbInput(puInputN - 1) THEN sPassive ELSE sPassive ENDIF)

No change on: (flatten)
Invar.1.2 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   sPassive?(IF i!1`pbInput(puInputN - 1) THEN sPassive ELSE sPassive ENDIF)

Postponing Invar.1.2.

Invar.1.2 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   sPassive?(IF i!1`pbInput(puInputN - 1) THEN sPassive ELSE sPassive ENDIF)

No change on: (skip)
Invar.1.2 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   sPassive?(IF i!1`pbInput(puInputN - 1) THEN sPassive ELSE sPassive ENDIF)

Postponing Invar.1.2.

Invar.1.2 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   sPassive?(IF i!1`pbInput(puInputN - 1) THEN sPassive ELSE sPassive ENDIF)

Lifting IF-conditions to the top level,
this simplifies to: 
Invar.1.2 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   sPassive?(sPassive)

Postponing Invar.1.2.

Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   IF i!1`pbInput(puInputN - 1) THEN 1 > 0 ELSE 0 > 0 ENDIF

No change on: (replace*)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   IF i!1`pbInput(puInputN - 1) THEN 1 > 0 ELSE 0 > 0 ENDIF

Postponing Invar.1.1.

Invar.1.2 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   sPassive?(sPassive)

No change on: (replace*)
Invar.1.2 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   sPassive?(sPassive)

Postponing Invar.1.2.

Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   IF i!1`pbInput(puInputN - 1) THEN 1 > 0 ELSE 0 > 0 ENDIF

Simplifying, rewriting, and recording with decision procedures,
this simplifies to: 
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   IF i!1`pbInput(puInputN - 1) THEN TRUE ELSE FALSE ENDIF

Applying bddsimp,
this simplifies to: 
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   i!1`pbInput(puInputN - 1)

Couldn't find a suitable quantified formula.
No change on: (inst? :if-match t :polarity? nil)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   i!1`pbInput(puInputN - 1)

No suitable (+ve FORALL/-ve EXISTS) quantified expression found.

No change on: (skolem-typepred)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

No change on: (flatten)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

Postponing Invar.1.1.

Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

No change on: (skip)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

Postponing Invar.1.1.

Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   i!1`pbInput(puInputN - 1)

No change on: (lift-if :updates? t)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   i!1`pbInput(puInputN - 1)

Postponing Invar.1.1.

Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   i!1`pbInput(puInputN - 1)

No change on: (replace*)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   i!1`pbInput(puInputN - 1)

Postponing Invar.1.1.

Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   i!1`pbInput(puInputN - 1)

Simplifying, rewriting, and recording with decision procedures,
this simplifies to: 
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

No change on: (bddsimp)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

Couldn't find a suitable quantified formula.
No change on: (inst? :if-match t :polarity? nil)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

No suitable (+ve FORALL/-ve EXISTS) quantified expression found.

No change on: (skolem-typepred)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

No change on: (flatten)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

Postponing Invar.1.1.

Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

No change on: (skip)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

Postponing Invar.1.1.

Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

No change on: (lift-if :updates? t)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

Postponing Invar.1.1.

Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

No change on: (replace*)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

Postponing Invar.1.1.

Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

No change on: (assert :let-reduce? t :quant-simp? nil
                      :implicit-typepreds? nil :cases-rewrite? nil)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

No change on: (bddsimp)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

Couldn't find a suitable quantified formula.
No change on: (inst? :if-match t :polarity? nil)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

No suitable (+ve FORALL/-ve EXISTS) quantified expression found.

No change on: (skolem-typepred)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

No change on: (flatten)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

Postponing Invar.1.1.

Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

No change on: (skip)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

Postponing Invar.1.1.

Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

No change on: (lift-if :updates? t)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

Postponing Invar.1.1.

Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

No change on: (skip)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

Postponing Invar.1.1.

Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

No change on: (skip)
Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

Postponing Invar.1.1.

Invar.1.2 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
{1}   sPassive?(sPassive)

Simplifying, rewriting, and recording with decision procedures,

This completes the proof of Invar.1.2.

Invar.1.1 :  

[-1]  i!2 < puInputN
[-2]  i!1`pbInput(i!2)
  |-------
[1]   i!1`pbInput(puInputN - 1)

Rule? (quit)
Do you really want to quit?  (Y or N): y


Run time  = 1.77 secs.
Real time = 80.99 secs.

Renamed sc1.prf to sc1.prf~
Wrote proof file sc1.prf
nil
pvs(18):