**Equivalence-transformation** is a proof system used alongside classical truth-functional [[pred-logic|predicate logic]]. It is the foundation upon which [[pred-trans|predicate transformers]] are based.
A [[prop-logic|proposition]] is said to be a **tautology** if it evaluates to $T$ in every state it is well-defined in. We say propositions $E1$ and $E2$ are **equivalent** if $E1 = E2$ is a tautology. In this case, we say $E1 = E2$ is an **equivalence**.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707251673361-->
END%%
### De Morgan's
For propositions $E1$ and $E2$:
* $\neg (E1 \land E2) = \neg E1 \lor \neg E2$
* $\neg (E1 \lor E2) = \neg E1 \land \neg E2$
%%ANKI
Basic
Which of the basic logical operators do De Morgan's laws involve?
Back: $\neg$, $\land$, and $\lor$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707251673363-->
END%%
%%ANKI
Basic
How is De Morgan's law (distributing $\land$) expressed as an equivalence?
Back: $\neg (E1 \land E2) = \neg E1 \lor \neg E2$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707251673364-->
END%%
### Law of Negation
For any proposition $E1$, it follows that $\neg (\neg E1) = E1$.
%%ANKI
Basic
How is the law of negation expressed as an equivalence?
Back: $\neg (\neg E1) = E1$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707251673365-->
END%%
### Law of Excluded Middle
For any proposition $E1$, it follows that $E1 \lor \neg E1 = T$.
%%ANKI
Basic
Which of the basic logical operators does the law of excluded middle involve?
Back: $\lor$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707251673367-->
END%%
%%ANKI
Basic
How is the law of excluded middle expressed as an equivalence?
Back: $E1 \lor \neg E1 = T$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707251673368-->
END%%
%%ANKI
Basic
"This sentence is false" questions which classical principle?
Back: The law of excluded middle.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707251779153-->
END%%
### Law of Contradiction
For any proposition $E1$, it follows that $E1 \land \neg E1 = F$.
%%ANKI
Basic
Which of the basic logical operators does the law of contradiction involve?
Back: $\land$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707251673370-->
END%%
%%ANKI
Basic
How is the law of contradiction expressed as an equivalence?
Back: $E1 \land \neg E1 = F$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707251673371-->
END%%
%%ANKI
Cloze
The law of {1:excluded middle} is to {2:$\lor$} whereas the law of {2:contradiction} is to {1:$\land$}.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707251673373-->
END%%
%%ANKI
Basic
What does the principle of explosion state?
Back: That any statement can be proven from a contradiction.
Reference: “Principle of Explosion,” in _Wikipedia_, July 3, 2024, [https://en.wikipedia.org/w/index.php?title=Principle_of_explosion](https://en.wikipedia.org/w/index.php?title=Principle_of_explosion&oldid=1232334233).
<!--ID: 1721354092779-->
END%%
%%ANKI
Basic
How is the principle of explosion stated in first-order logic?
Back: $\forall P, F \Rightarrow P$
Reference: “Principle of Explosion,” in _Wikipedia_, July 3, 2024, [https://en.wikipedia.org/w/index.php?title=Principle_of_explosion](https://en.wikipedia.org/w/index.php?title=Principle_of_explosion&oldid=1232334233).
<!--ID: 1721354092783-->
END%%
%%ANKI
Basic
What does the law of contradiction say?
Back: For any proposition $P$, it holds that $\neg (P \land \neg P)$.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1721354092786-->
END%%
%%ANKI
Basic
How does the principle of explosion relate to the law of contradiction?
Reference: “Principle of Explosion,” in _Wikipedia_, July 3, 2024, [https://en.wikipedia.org/w/index.php?title=Principle_of_explosion](https://en.wikipedia.org/w/index.php?title=Principle_of_explosion&oldid=1232334233).
<!--ID: 1721354092789-->
END%%
%%ANKI
Basic
Suppose $P$ and $\neg P$. Show schematically how to use the principle of explosion to prove $Q$.
Back: $$\begin{align*} P \\ \neg P \\ P \lor Q \\ \hline Q \end{align*}$$Reference: “Principle of Explosion,” in _Wikipedia_, July 3, 2024, [https://en.wikipedia.org/w/index.php?title=Principle_of_explosion](https://en.wikipedia.org/w/index.php?title=Principle_of_explosion&oldid=1232334233).
<!--ID: 1721354092792-->
END%%
%%ANKI
Cloze
The law of {contradiction} and law of {excluded middle} create a dichotomy in "logical space".
Reference: “Law of Noncontradiction,” in _Wikipedia_, June 14, 2024, [https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction](https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction&oldid=1229006759).
<!--ID: 1721354092795-->
END%%
%%ANKI
Basic
Which property of partitions is analagous to the law of contradiction on "logical space"?
Back: Disjointedness.
Reference: “Law of Noncontradiction,” in _Wikipedia_, June 14, 2024, [https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction](https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction&oldid=1229006759).
<!--ID: 1721354092798-->
END%%
%%ANKI
Basic
Which property of partitions is analagous to the law of excluded middle on "logical space"?
Back: Exhaustiveness.
Reference: “Law of Noncontradiction,” in _Wikipedia_, June 14, 2024, [https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction](https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction&oldid=1229006759).
<!--ID: 1721354092801-->
END%%
%%ANKI
Cloze
The law of {1:contradiction} is to "{2:mutually exclusive}" whereas the law of {2:excluded middle} is "{1:jointly exhaustive}".
Reference: “Law of Noncontradiction,” in _Wikipedia_, June 14, 2024, [https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction](https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction&oldid=1229006759).
<!--ID: 1721354092805-->
END%%
%%ANKI
Basic
Which logical law proves equivalence of the law of contradiction and excluded middle?
Back: De Morgan's law.
Reference: “Law of Noncontradiction,” in _Wikipedia_, June 14, 2024, [https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction](https://en.wikipedia.org/w/index.php?title=Law_of_noncontradiction&oldid=1229006759).
<!--ID: 1721355020261-->
END%%
### Law of Implication
For any propositions $E1$ and $E2$, it follows that $E1 \Rightarrow E2 = \neg E1 \lor E2$.
### Law of Equality
For any propositions $E1$ and $E2$, it follows that $(E1 = E2) = (E1 \Rightarrow E2) \land (E2 \Rightarrow E1)$.
### Law of Or-Simplification
For any propositions $E1$ and $E2$, it follows that:
* $E1 \lor E1 = E1$
* $E1 \lor T = T$
* $E1 \lor F = E1$
* $E1 \lor (E1 \land E2) = E1$
### Law of And-Simplification
For any propositions $E1$ and $E2$, it follows that:
A **selector** denotes a finite sequence of subscript expressions, each enclosed in brackets. $\epsilon$ denotes the empty selector. For example, variable $x$ is equivalently denoted as $x \circ \epsilon$ whereas for array $b$, $b[i]$ is equivalently denoted as $b \circ [i]$.
**Selector update** syntax allows specifying a new value with previous subscripted values overridden. For instance, $(b; i{:}e)$ denotes $b$ with $b[i]$ now referring to $e$. More formally, for any $j \in \mathop{domain}(b)$, $$(b; i{:}e)[j] = \begin{cases} i = j \rightarrow e \\ i \neq j \rightarrow b[j] \end{cases}$$
**Textual substitution** refers to the replacement of a [[pred-logic#Identifiers|free]] identifier with an expression, introducing parentheses as necessary. This concept amounts to the [[#Equivalence Rules|Substitution Rule]] with different notation.
%%ANKI
Basic
Textual substitution is derived from what equivalence rule?
Back: The substitution rule.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707762304123-->
END%%
### Simple
If $x$ denotes a variable and $e$ an expression, substitution of $x$ by $e$ is denoted as $$\large{E_e^x}$$
%%ANKI
Basic
What term refers to $x$ in textual substitution $E_e^x$?
Back: The reference.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707939006275-->
END%%
%%ANKI
Basic
What term refers to $e$ in textual substitution $E_e^x$?
Back: The expression.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707939006283-->
END%%
%%ANKI
Basic
What term refers to both $x$ and $e$ together in textual substitution $E_e^x$?
Back: The reference-expression pair.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707939006288-->
END%%
%%ANKI
Basic
What identifier is guaranteed to not occur freely in $E_e^x$?
Back: N/A.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707937867036-->
END%%
%%ANKI
Basic
What identifier is guaranteed to not occur freely in $E_{s(e)}^x$?
Back: $x$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707937867039-->
END%%
%%ANKI
Basic
*Why* does $x$ not occur freely in $E_{s(e)}^x$?
Back: Because $s(e)$ evaluates to a constant proposition.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707937867042-->
END%%
%%ANKI
Basic
What is the role of $E$ in textual substitution $E_e^x$?
Back: It is the expression in which free occurrences of $x$ are replaced.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1708347042194-->
END%%
%%ANKI
Basic
What is the role of $e$ in textual substitution $E_e^x$?
Back: It is the expression that is evaluated and substituted into $E$.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1708347042199-->
END%%
%%ANKI
Basic
What is the role of $x$ in textual substitution $E_e^x$?
Back: It is the identifier matching free occurrences in $E$ that are replaced.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1708347042203-->
END%%
%%ANKI
Basic
How is textual substitution $E_e^x$ interpreted as a function?
Back: As $E(e)$, where $E$ is a function of $x$.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707762304130-->
END%%
%%ANKI
Basic
Why does Gries prefer notation $E_e^x$ over e.g. $E(e)$?
Back: The former indicates the identifier to replace.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707762304132-->
END%%
%%ANKI
Basic
What two scenarios ensure $E_e^x = E$ is an equivalence?
Back: $x = e$ or no free occurrences of $x$ exist in $E$.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707762304133-->
END%%
%%ANKI
Basic
If $x \neq e$, why might $E_e^x = E$ be an equivalence despite $x$ existing in $E$?
Back: The only occurrences of $x$ in $E$ may be bound.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707762304135-->
END%%
%%ANKI
Basic
What is required for $E_e^x$ to be valid?
Back: Substitution must result in a syntactically valid expression.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707762304137-->
END%%
%%ANKI
Basic
What is the result of the following? $$(x <y \land(\foralli:0 \leqi<n:b[i]<y))_z^x$$
Back: $$(z <y \land(\foralli:0 \leqi<n:b[i]<y))$$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707762304139-->
END%%
%%ANKI
Basic
What is the result of the following? $$(x <y \land(\foralli:0 \leqi<n:b[i]<y))_z^y$$
Back: $$(x <z \land(\foralli:0 \leqi<n:b[i]<z))$$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707762304140-->
END%%
%%ANKI
Basic
What is the result of the following? $$(x <y \land(\foralli:0 \leqi<n:b[i]<y))_z^i$$
Back: $$(x <y \land(\foralli:0 \leqi<n:b[i]<y))$$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707762304141-->
END%%
### General
We can generalize textual substitution to operate on a vector of reference-expression pairs, where each reference corresponds to some identifier concatenated with a selector. Let $\bar{x} = \langle x_1, \ldots, x_n \rangle$ denote a vector of identifiers concatenated with selectors and $\bar{e} = \langle e_1, \ldots, e_n \rangle$ denote a vector of expressions. Then textual substitition of $\bar{x}$ with $\bar{e}$ in expression $E$ is denoted as $$\large{E_{\bar{e}}^{\bar{x}}}$$
Substitution is defined recursively as follows:
1. If each $x_i$ is a distinct identifier with a null selector, then $E_{\bar{e}}^{\bar{x}}$ is the simultaneous substitution of $\bar{x}$ with $\bar{e}$.
2. Adjacent reference-expression pairs may be permuted as long as they begin with different identifiers. That is, for all distinct $b$ and $c$, $$\Large{E_{\bar{e}, \,f, \,h, \,\bar{g}}^{\bar{x}, \,b, \,c, \,\bar{y}} = E_{\bar{x}, \,h, \,f, \,\bar{g}}^{\bar{x}, \,c, \,b, \,\bar{y}}}$$
3. Multiple assignments to subparts of an object $b$ can be viewed as a single assignment to $b$. That is, provided $b$ does not begin any of the $x_i$, $$\Large{E_{e_1, \,\ldots, \,e_m, \,\bar{g}}^{b \,\circ\, s_1, \,\ldots, \,b \,\circ\, s_m, \,\bar{x}} = E_{(b; \,s_1{:}e_1; \,\cdots; \,s_m{:}e_m), \,\bar{g}}^{b, \,\bar{x}}}$$
Suppose $x \neq y$. What next simplification step can be taken before substitution? $$\large{E_{(x; \,\epsilon{:}e_1; \,\epsilon{:}e_3), e_2}^{x, y}}$$
Suppose $x \neq y$. *Why* isn't the following a tautology? $$\large{E_{e_1, e_2, e_3, e_4}^{x[1], x[2], y, x[3]}} = E_{(x; \,[1]{:}e_1; \,[2]{:}e_2), e_3, e_4}^{x, y, x[3]}$$
Consider identifier $x$, array $b$ and $i \in \mathop{domain}(b)$. What next simplification step can be taken before substitution? $$\large{E_{b[i]}^{x}}$$
* $y$ may not be free in $E$ but substituting $x$ with $u$ can introduce a free occurrence. It doesn't matter if we perform the substitution first or second though.
%%ANKI
Basic
In what two scenarios is $(E_u^x)_v^y = E_{u_v^y}^x$ always an equivalence?
Back: $x = y$ or $y$ is not free in $E$.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707762304148-->
END%%
%%ANKI
Basic
If $x \neq y$, when is $(E_u^x)_v^y = E_{u_v^y}^x$?
Back: When $y$ is not free in $E$.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
A **state** is a function that maps identifiers to $T$ or $F$. A proposition can be equivalently seen as a representation of the set of states in which it is true.
%%ANKI
Basic
What is a state?
Back: A function mapping identifiers to values.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861314-->
END%%
%%ANKI
Basic
Is $(b \land c)$ well-defined in $\{\langle b, T \rangle, \langle c, F \rangle\}$?
Back: Yes.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861318-->
END%%
%%ANKI
Basic
Is $(b \lor d)$ well-defined in $\{\langle b, T \rangle, \langle c, F \rangle\}$?
Back: No.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861320-->
END%%
%%ANKI
Basic
A proposition is well-defined with respect to what?
Back: A state to evaluate against.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861316-->
END%%
%%ANKI
Basic
What proposition represents states $\{(b, T), (c, T)\}$ and $\{(b, F), (c, F)\}$?
Back: $(b \land c) \lor (\neg b \land \neg c)$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861337-->
END%%
%%ANKI
Basic
What set of states does proposition $a \land b$ represent?
Back: $\{\{\langle a, T \rangle, \langle b, T \rangle\}\}$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861339-->
END%%
%%ANKI
Basic
What set of states does proposition $a \lor b$ represent?
Back: $\{\{\langle a, T \rangle, \langle b, T \rangle\}, \{\langle a, T \rangle, \langle b, F \rangle\}, \{\langle a, F \rangle, \langle b, T \rangle\}\}$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1715895996324-->
END%%
%%ANKI
Basic
What is sloppy about phrase "the states in $b \lor \neg c$"?
Back: $b \lor \neg c$ is not a set but a representation of a set (of states).
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861341-->
END%%
%%ANKI
Basic
What is the weakest proposition?
Back: $T$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861348-->
END%%
%%ANKI
Basic
What set of states does $T$ represent?
Back: The set of all states.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861350-->
END%%
%%ANKI
Basic
What is the strongest proposition?
Back: $F$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861352-->
END%%
%%ANKI
Basic
What set of states does $F$ represent?
Back: The set of no states.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861354-->
END%%
%%ANKI
Basic
What does a proposition *represent*?
Back: The set of states in which it is true.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861335-->
END%%
%%ANKI
Basic
When is $p$ stronger than $q$?
Back: When $p \Rightarrow q$.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861343-->
END%%
%%ANKI
Basic
If $p \Rightarrow q$, which of $p$ or $q$ is considered stronger?
Back: $p$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1715631869202-->
END%%
%%ANKI
Basic
When is $p$ weaker than $q$?
Back: When $q \Rightarrow p$.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861346-->
END%%
%%ANKI
Basic
If $p \Rightarrow q$, which of $p$ or $q$ is considered weaker?
Back: $q$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1715631869207-->
END%%
%%ANKI
Basic
Why is $b \land c$ stronger than $b \lor c$?
Back: The former represents a subset of the states the latter represents.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1706994861356-->
END%%
%%ANKI
Basic
Given sets $a$ and $b$, $a = b$ is equivalent to the conjunction of what two expressions?
Back: $a \subseteq b$ and $b \subseteq a$.
Reference: Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1715969047071-->
END%%
%%ANKI
Cloze
{$a \Rightarrow b$} is to propositional logic as {$a \subseteq b$} is to sets.
Reference: Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1715969047073-->
END%%
%%ANKI
Cloze
{$a \Leftrightarrow b$} is to propositional logic as {$a = b$} is to sets.
Reference: Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1715969047074-->
END%%
%%ANKI
Basic
Is $(i \geq 0)$ well-defined in $\{(i, -10)\}$?
Back: Yes.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1715898219881-->
END%%
%%ANKI
Basic
Is $(i \geq 0)$ well-defined in $\{(j, -10)\}$?
Back: No.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1715898219890-->
END%%
%%ANKI
Basic
What predicate represents states $\{(i, 0), (i, 2), (i, 4), \ldots\}$?
Back: $i \geq 0$ is even.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1715898219895-->
END%%
%%ANKI
Basic
What is sloppy about phrase "the states in $i + j = 0$"?
Back: $i + j = 0$ is not a set but a representation of a set (of states).
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
