Folderived (Calculemus)

Folderived Module

Namespace: Calculemus
Assembly: Calculemus.dll

First-order reasoning by inference.

Functions and values

Function or value	Description
`alpha z fm` Full Usage: `alpha z fm` Parameters: z : `string` fm : `formula<fol>` Returns: `thm`	z : `string` fm : `formula<fol>` Returns: `thm`
`eq_sym s t` Full Usage: `eq_sym s t` Parameters: s : `term` t : `term` Returns: `thm`	s : `term` t : `term` Returns: `thm`
`eq_trans s t u` Full Usage: `eq_trans s t u` Parameters: s : `term` t : `term` u : `term` Returns: `thm`	s : `term` t : `term` u : `term` Returns: `thm`
`exists_left x th` Full Usage: `exists_left x th` Parameters: x : `string` th : `thm` Returns: `thm`	x : `string` th : `thm` Returns: `thm`
`exists_left_th x p q` Full Usage: `exists_left_th x p q` Parameters: x : `string` p : `formula<fol>` q : `formula<fol>` Returns: `thm`	x : `string` p : `formula<fol>` q : `formula<fol>` Returns: `thm`
`gen_right x th` Full Usage: `gen_right x th` Parameters: x : `string` th : `thm` Returns: `thm`	x : `string` th : `thm` Returns: `thm`
`gen_right_th x p q` Full Usage: `gen_right_th x p q` Parameters: x : `string` p : `formula<fol>` q : `formula<fol>` Returns: `thm`	x : `string` p : `formula<fol>` q : `formula<fol>` Returns: `thm`
`genimp x th` Full Usage: `genimp x th` Parameters: x : `string` th : `thm` Returns: `thm`	x : `string` th : `thm` Returns: `thm`
`icongruence s t stm ttm` Full Usage: `icongruence s t stm ttm` Parameters: s : `term` t : `term` stm : `term` ttm : `term` Returns: `thm`	s : `term` t : `term` stm : `term` ttm : `term` Returns: `thm`
`ispec t fm` Full Usage: `ispec t fm` Parameters: t : `term` fm : `formula<fol>` Returns: `thm`	t : `term` fm : `formula<fol>` Returns: `thm`
`isubst s t sfm tfm` Full Usage: `isubst s t sfm tfm` Parameters: s : `term` t : `term` sfm : `formula<fol>` tfm : `formula<fol>` Returns: `thm`	s : `term` t : `term` sfm : `formula<fol>` tfm : `formula<fol>` Returns: `thm`
`spec t th` Full Usage: `spec t th` Parameters: t : `term` th : `thm` Returns: `thm`	t : `term` th : `thm` Returns: `thm`
`subalpha th` Full Usage: `subalpha th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`
`subspec th` Full Usage: `subspec th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`