var X,Y,Z ;

const deltag = 8, deltaw=4, deltai=6;
--     correct under the condition  deltaw < deltai < deltag
--     deltag = 8, deltaw=4, deltai=1 gives error

define cgate1 as
[] ( [X && !Y]^slen=deltag => slen=deltag^[!Z] )
&&
[] ( [!X && Y]^slen=deltag => slen=deltag^[Z] )
;

define cgate2 as
   [](([X <=> Y]^slen=deltag) && ((slen=deltag && true^[Z])^true) => slen=deltag^[Z])
&&
   [](([X <=> Y]^slen=deltag) && ((slen=deltag && true^[!Z])^true) => slen=deltag^[!Z])
;

define wire as
  [] ([Z]^slen=deltaw => slen=deltaw^[X])
&&
  [] ([!Z]^slen=deltaw => slen=deltaw^[!X])
;

define inverter as
  [] ([Z]^slen=deltai => slen=deltai^[!Y])
&&
  [] ([!Z]^slen=deltai => slen=deltai^[Y])
;

define circuit1 as
cgate1 && cgate2 && wire && inverter ;


define ccgate1 as
[] ( [Z && !Y]^slen=deltag => slen=deltag^[!Z] )
&&
[] ( [!Z && Y]^slen=deltag => slen=deltag^[Z] )
;

define ccgate2 as
   [](([Z <=> Y]^slen=deltag) && ((slen=deltag && true^[Z])^true) => slen=deltag^[Z])
&&
   [](([Z <=> Y]^slen=deltag) && ((slen=deltag && true^[!Z])^true) => slen=deltag^[!Z])
;

define circuit2 as
ccgate1 && ccgate2  && inverter
;

define init1 as
(slen <= deltag => ([Z] || <Z> )) && 
(slen <= deltai => ([Y] || <Y>)) && 
(slen<=deltaw => ([!X] || <!X>))
;

define init as
!(!init1^ext)  ;

infer entire
circuit1 && init => circuit2
.