# [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)

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):
```