:: deftheorem defines BCI-EXAMPLE BCIALG_1:def 9 :
BCI-EXAMPLE = BCIStr_0(# {0},op2,op0 #);