:: deftheorem defines BCI_S-EXAMPLE BCIALG_4:def 3 :
BCI_S-EXAMPLE = BCIStr_1(# {0},op2,op2,op0 #);