Redlog Documentation Center

This new documentation in under construction. For functions not covered yet, please use the old documentation.

mkand, mkor – big conjunction and disjunction for loop actions

Calling Sequence

for each $$x$$ in $$L$$ mkand $$E$$
for $$x := n$$ : $$m$$ mkand $$E$$
for each $$a$$ in $$L$$ mkor $$E$$
for $$x := n$$ : $$m$$ mkor $$E$$

Arguments

 $$x$$ — identifier $$L$$ — list $$E$$ — expression evaluating to a first-order formulas and typically depending on $$x$$ $$n$$ — integer $$m$$ — integer

Returns

 $$\varphi′$$ — first-order formula

Description

Reduce has a quite general concept of for loops. On the one hand, the synopsis show that the condition of the loop allows to run over a range $$n\dots m$$ of integers as well as over the elements of a given list $$L$$. In fact there even further options for conditions can be found in the Reduce manual. On the other hand, the iterator actions allow not only to evaluate the body of the loop with each iteration but to perform certain constructive actions with the corresponding evaluation results.

With mkand and mkor corresponding conjunctions and disjunctions are constructed, respectively. Note that those conjunctions and disjunctions generally start with the corresponding neutral element for the 0-th iteration of the loop.

Examples

for each at in rlatl(a=0 and (b=0 or c=0)) mkand at;
for i:=1:3 mkand
for j:=1:3 mkor
if j<>i then mkid(x,i)+mkid(x,j)=0;