TaPAS  0.2
Functions
batof-formulas.h File Reference
#include "prestaf-batof-p.h"

Go to the source code of this file.

Functions

armoise_treebtf_form_crt_synform (struct msa2form_compilation_data *cd, armoise_tree *P)
 
armoise_treebtf_form_crt_VH_definition (struct msa2form_compilation_data *cd, const char *id, tla_vec_t rho, tla_vec_t xhi, tla_vsp_t V, tla_vec_t alpha, int op)
 

Function Documentation

armoise_tree* btf_form_crt_synform ( struct msa2form_compilation_data *  cd,
armoise_tree P 
)

let SynForm := R; in { (X[0], ..., X[m-1]) | (X[0], ..., X[m-1]) in (nat, ..., nat) && SynForm };

armoise_tree* btf_form_crt_VH_definition ( struct msa2form_compilation_data *  cd,
const char *  id,
tla_vec_t  rho,
tla_vec_t  xhi,
tla_vsp_t  V,
tla_vec_t  alpha,
int  op 
)

$Z^m (x_0 + (V_G H))$