Limitations (Calculemus)

Limitations Module

Namespace: Calculemus
Assembly: Calculemus.dll

Undecidability.

Types

Type	Description
config
direction
formulaclass
symbol
tape

Functions and values

Function or value	Description
`add_0` Full Usage: `add_0` Returns: `thm`	Returns: `thm`
`add_suc` Full Usage: `add_suc` Returns: `thm`	Returns: `thm`
`bounded_prove (a, x, t, q)` Full Usage: `bounded_prove (a, x, t, q)` Parameters: a : `string` x : `string` t : `term` q : `formula<fol>` Returns: `thm`	a : `string` x : `string` t : `term` q : `formula<fol>` Returns: `thm`
`boundednum_prove (a, x, t, q)` Full Usage: `boundednum_prove (a, x, t, q)` Parameters: a : `string` x : `string` t : `term` q : `formula<fol>` Returns: `thm`	a : `string` x : `string` t : `term` q : `formula<fol>` Returns: `thm`
`boundquant_step th0 th1` Full Usage: `boundquant_step th0 th1` Parameters: th0 : `thm` th1 : `thm` Returns: `thm`	th0 : `thm` th1 : `thm` Returns: `thm`
`classify c n fm` Full Usage: `classify c n fm` Parameters: c : `formulaclass` n : `int` fm : `formula<fol>` Returns: `bool`	c : `formulaclass` n : `int` fm : `formula<fol>` Returns: `bool`
`dholds v fm` Full Usage: `dholds v fm` Parameters: v : `func<string, bigint>` fm : `formula<fol>` Returns: `bool`	v : `func<string, bigint>` fm : `formula<fol>` Returns: `bool`
`dhquant pred v x y a t p` Full Usage: `dhquant pred v x y a t p` Parameters: pred : `(bigint -> bool) -> bigint list -> bool` v : `func<string, bigint>` x : `string` y : `string` a : `string` t : `term` p : `formula<fol>` Returns: `bool`	pred : `(bigint -> bool) -> bigint list -> bool` v : `func<string, bigint>` x : `string` y : `string` a : `string` t : `term` p : `formula<fol>` Returns: `bool`
`diag001 s` Full Usage: `diag001 s` Parameters: s : `string` Returns: `string`	s : `string` Returns: `string`
`diag002 x p` Full Usage: `diag002 x p` Parameters: x : `string` p : `formula<fol>` Returns: `formula<fol>`	x : `string` p : `formula<fol>` Returns: `formula<fol>`
`dtermval v tm` Full Usage: `dtermval v tm` Parameters: v : `func<string, bigint>` tm : `term` Returns: `bigint`	v : `func<string, bigint>` tm : `term` Returns: `bigint`
`elim_bex fm` Full Usage: `elim_bex fm` Parameters: fm : `formula<fol>` Returns: `thm`	fm : `formula<fol>` Returns: `thm`
`exec prog args` Full Usage: `exec prog args` Parameters: prog : `func<(int * symbol), (symbol * direction * int)>` args : `int list` Returns: `int`	prog : `func<(int * symbol), (symbol * direction * int)>` args : `int list` Returns: `int`
`expand_le` Full Usage: `expand_le` Returns: `thm`	Returns: `thm`
`expand_lt` Full Usage: `expand_lt` Returns: `thm`	Returns: `thm`
`expand_nle` Full Usage: `expand_nle` Returns: `thm`	Returns: `thm`
`expand_nlt` Full Usage: `expand_nlt` Returns: `thm`	Returns: `thm`
`first n p` Full Usage: `first n p` Parameters: n : `BigInteger` p : `BigInteger -> bool` Returns: `BigInteger`	n : `BigInteger` p : `BigInteger -> bool` Returns: `BigInteger`
`gform fm` Full Usage: `gform fm` Parameters: fm : `formula<fol>` Returns: `BigInteger`	fm : `formula<fol>` Returns: `BigInteger`
`gnumeral n` Full Usage: `gnumeral n` Parameters: n : `BigInteger` Returns: `BigInteger`	n : `BigInteger` Returns: `BigInteger`
`gterm tm` Full Usage: `gterm tm` Parameters: tm : `term` Returns: `BigInteger`	tm : `term` Returns: `BigInteger`
`input_tape` Full Usage: `input_tape` Returns: `int list -> tape`	Returns: `int list -> tape`
`introduce_connective fm` Full Usage: `introduce_connective fm` Parameters: fm : `formula<fol>` Returns: `thm`	fm : `formula<fol>` Returns: `thm`
`le_0` Full Usage: `le_0` Returns: `thm`	Returns: `thm`
`le_def` Full Usage: `le_def` Returns: `thm`	Returns: `thm`
`le_suc` Full Usage: `le_suc` Returns: `thm`	Returns: `thm`
`look arg1` Full Usage: `look arg1` Parameters: arg0 : `tape` Returns: `symbol`	arg0 : `tape` Returns: `symbol`
`lt_0` Full Usage: `lt_0` Returns: `thm`	Returns: `thm`
`lt_def` Full Usage: `lt_def` Returns: `thm`	Returns: `thm`
`lt_suc` Full Usage: `lt_suc` Returns: `thm`	Returns: `thm`
`move dir arg2` Full Usage: `move dir arg2` Parameters: dir : `direction` arg1 : `tape` Returns: `tape`	dir : `direction` arg1 : `tape` Returns: `tape`
`mul_0` Full Usage: `mul_0` Returns: `thm`	Returns: `thm`
`mul_suc` Full Usage: `mul_suc` Returns: `thm`	Returns: `thm`
`num_cases` Full Usage: `num_cases` Returns: `thm`	Returns: `thm`
`num_lecases` Full Usage: `num_lecases` Returns: `thm`	Returns: `thm`
`number s` Full Usage: `number s` Parameters: s : `string` Returns: `bigint`	s : `string` Returns: `bigint`
`numeral n` Full Usage: `numeral n` Parameters: n : `BigInteger` Returns: `term`	n : `BigInteger` Returns: `term`
`opp _arg1` Full Usage: `opp _arg1` Parameters: _arg1 : `formulaclass` Returns: `formulaclass`	_arg1 : `formulaclass` Returns: `formulaclass`
`output_tape tape` Full Usage: `output_tape tape` Parameters: tape : `tape` Returns: `int`	tape : `tape` Returns: `int`
`pair x y` Full Usage: `pair x y` Parameters: x : `bigint` y : `bigint` Returns: `BigInteger`	x : `bigint` y : `bigint` Returns: `BigInteger`
`phi001` Full Usage: `phi001` Returns: `string`	Returns: `string`
`phi002` Full Usage: `phi002` Returns: `string -> string -> string`	Returns: `string -> string -> string`
`qdiag001 s` Full Usage: `qdiag001 s` Parameters: s : `'a` Returns: `string -> string -> string`	s : `'a` Returns: `string -> string -> string`
`qdiag002 x p` Full Usage: `qdiag002 x p` Parameters: x : `string` p : `formula<fol>` Returns: `formula<fol>`	x : `string` p : `formula<fol>` Returns: `formula<fol>`
`right_imp_trans th1 th2` Full Usage: `right_imp_trans th1 th2` Parameters: th1 : `thm` th2 : `thm` Returns: `thm`	th1 : `thm` th2 : `thm` Returns: `thm`
`right_mp ith th` Full Usage: `right_mp ith th` Parameters: ith : `thm` th : `thm` Returns: `thm`	ith : `thm` th : `thm` Returns: `thm`
`right_spec t th` Full Usage: `right_spec t th` Parameters: t : `term` th : `thm` Returns: `thm`	t : `term` th : `thm` Returns: `thm`
`right_sym th` Full Usage: `right_sym th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`
`right_trans th1 th2` Full Usage: `right_trans th1 th2` Parameters: th1 : `thm` th2 : `thm` Returns: `thm`	th1 : `thm` th2 : `thm` Returns: `thm`
`rob_eq s t` Full Usage: `rob_eq s t` Parameters: s : `term` t : `term` Returns: `thm`	s : `term` t : `term` Returns: `thm`
`rob_ne s t` Full Usage: `rob_ne s t` Parameters: s : `term` t : `term` Returns: `thm`	s : `term` t : `term` Returns: `thm`
`rob_nen (s, t)` Full Usage: `rob_nen (s, t)` Parameters: s : `term` t : `term` Returns: `thm`	s : `term` t : `term` Returns: `thm`
`robeval tm` Full Usage: `robeval tm` Parameters: tm : `term` Returns: `thm`	tm : `term` Returns: `thm`
`robinson` Full Usage: `robinson` Returns: `formula<fol>`	Returns: `formula<fol>`
`robinson_consequences` Full Usage: `robinson_consequences` Returns: `formula<fol>`	Returns: `formula<fol>`
`robinson_thm` Full Usage: `robinson_thm` Returns: `thm`	Returns: `thm`
`robop tm` Full Usage: `robop tm` Parameters: tm : `term` Returns: `thm`	tm : `term` Returns: `thm`
`run prog config` Full Usage: `run prog config` Parameters: prog : `func<(int * symbol), (symbol * direction * int)>` config : `config` Returns: `config`	prog : `func<(int * symbol), (symbol * direction * int)>` config : `config` Returns: `config`
`sholds` Full Usage: `sholds` Returns: `bigint -> func<string, bigint> -> formula<fol> -> bool`	Returns: `bigint -> func<string, bigint> -> formula<fol> -> bool`
`sigma_bound fm` Full Usage: `sigma_bound fm` Parameters: fm : `formula<fol>` Returns: `BigInteger`	fm : `formula<fol>` Returns: `BigInteger`
`sigma_elim fm` Full Usage: `sigma_elim fm` Parameters: fm : `formula<fol>` Returns: `thm`	fm : `formula<fol>` Returns: `thm`
`sigma_prove fm` Full Usage: `sigma_prove fm` Parameters: fm : `formula<fol>` Returns: `thm`	fm : `formula<fol>` Returns: `thm`
`suc_0_l` Full Usage: `suc_0_l` Returns: `thm`	Returns: `thm`
`suc_0_r` Full Usage: `suc_0_r` Returns: `thm`	Returns: `thm`
`suc_inj` Full Usage: `suc_inj` Returns: `thm`	Returns: `thm`
`suc_inj_false` Full Usage: `suc_inj_false` Returns: `thm`	Returns: `thm`
`veref sign m v fm` Full Usage: `veref sign m v fm` Parameters: sign : `bool -> bool` m : `bigint` v : `func<string, bigint>` fm : `formula<fol>` Returns: `bool`	sign : `bool -> bool` m : `bigint` v : `func<string, bigint>` fm : `formula<fol>` Returns: `bool`
`verefboundquant m v x y a t sign p` Full Usage: `verefboundquant m v x y a t sign p` Parameters: m : `bigint` v : `func<string, bigint>` x : `string` y : `string` a : `string` t : `term` sign : `bool -> bool` p : `formula<fol>` Returns: `bool`	m : `bigint` v : `func<string, bigint>` x : `string` y : `string` a : `string` t : `term` sign : `bool -> bool` p : `formula<fol>` Returns: `bool`
`write s arg2` Full Usage: `write s arg2` Parameters: s : `symbol` arg1 : `tape` Returns: `tape`	s : `symbol` arg1 : `tape` Returns: `tape`