In natural deduction, conjunction introduction combines derivations of $\varphi$ and $\psi$ under the available assumptions into $\varphi \wedge \psi$. Disjunction elimination takes $\varphi \vee \psi$ and two subproofs of the same conclusion $\kappa$, one assuming $\varphi$ and the other assuming $\psi$, and concludes $\kappa$. Implication introduction takes a subproof deriving $\psi$ from a temporary assumption $\varphi$, and concludes $\varphi \to \psi$.

The rectangular boxes mark the scopes of temporary assumptions. The disjunction elimination rule discharges its two case assumptions, while the implication introduction rule discharges the antecedent assumption. Other surrounding assumptions remain in force; intermediate results depending on the boxed assumptions cannot be exported arbitrarily. Schematically,Here the square brackets designate the assumptions discharged by the corresponding inference rule.

Choose fresh arbitrary eigenvariables $u,v$. Under $u=v$, use the equality elimination rule to transport $P(u)$ to $P(v)$. For the reverse direction, first derive $v=u$ by the symmetry derivation above. In full natural deduction form:All temporary assumptions are discharged before either universal quantifier introduction rule application, so both eigenvariable conditions hold. No premises remain:

For transitivity of first-order equality, take $\varphi (v)$ to be $T_1=v$. The equality elimination rule applied to $T_2=T_3$ and $\varphi (T_2)$ givesFor symmetry of first-order equality, first obtain $T_1=T_1$ by the equality introduction rule. Now take $\psi (v)$ to be $v=T_1$ and substitute using $T_1=T_2$:These choices of formula show exactly which occurrence is replaced, so neither argument assumes the property it is establishing.

The equality introduction rule is reflexivity, with no premise. The equality elimination rule is substitution of equal first-order terms into a first-order formula:The indicated substitution must be capture-avoiding substitution in first-order logic: the first-order terms must be free for the replaced variable. One can designate a particular argument occurrence by choosing $\varphi (v)$ appropriately; the rule does not demand replacing every occurrence of an identical-looking term in a formula.

The dot after $\forall x$ gives it scope over the following implication: read the premise as $H=\forall x(P(x)\to Q(x))$. Choose a fresh arbitrary eigenvariable $u$. A natural deduction proof isAt line 6, $u$ is free in no undischarged assumption, so the universal quantifier introduction rule is valid.

The proposed variant is not derivable in a sound first-order logic. For a countermodel, use the two-element domain $\{0,1\}$, interpret both predicates $P,Q$ as $\{0\}$, and assign the free variable $x$ the value 0. Then $\forall x(P(x)\to Q(x))$ is true, as is $P(x)$ under the assignment, but $\forall xQ(x)$ is false at element 1. The premise's bound $x$ and the conclusion's free $x$ have different scopes.Attempting to generalize from $Q(x)$ in the variant would violate the eigenvariable condition, because $x$ remains free in the undischarged assumption $P(x)$.

Apply the negation introduction rule to an assumed existential statement and the existential quantifier elimination rule with a fresh witness $u$:The eigenvariable condition holds: $u$ is absent from the surrounding premise, the existential assumption and the exported conclusion $\perp$. Its local assumption is discharged before the final negation introduction rule.

First obtain $A$ by a double-negation elimination, then obtain $\neg B$ by the negation introduction rule. The following natural deduction proof uses only the printed rules, with $\perp E$ denoting the logical falsity elimination rule:Reiteration only reuses an available line within its scope. In particular, the unused temporary assumption on line 11 is legitimately discharged by the implication introduction rule.

Put $F=(\neg P)\to Q$ and $G=(\neg P)\to \neg Q$. Use the printed implication elimination rule, negation elimination rule, negation introduction rule, double-negation elimination and implication introduction rule:Line 1 is the given premise; the argument actually establishes the conclusion without needing it, since line 2 supplies its own copy of $F$. Introducing and discharging this separate temporary assumption preserves the exact printed conclusion.

Execute this MIPS instruction fragment twice, once with equal operands and once with unequal operands, and observe whether its conditional branch is taken:Use $t0=7,$t1=7 for the first test and $t0=7,$t1=8 for the second. All padding instructions are explicit harmless MIPS instructions. In the pictured single-cycle model, the next program counter after beq is either hit or the sequential address. The branch target is deliberately different from the next sequential instruction. The extra padding also keeps a branch delay slot harmless if a test fixture uses an implementation with one, although the pictured model itself has none.

A healthy zero line reports the first subtraction as zero and the second as nonzero. A line stuck at zero prevents both branches, while a line stuck at one forces both branches. ThereforeObserve the branch decision or execution trace itself; an alleged unconditional beq used to skip result-recording code would also be affected by the fault.

Again use independent externally initialized MIPS instruction tests. First preset $t0=7, $t1=5, and executeThe normal result, also obtained with ALUSrc stuck at zero, is 12. If the line is stuck at one, the second ALU operand is the sign-extended low 16 instruction bits. For this exact instruction they encode rd=10, shift amount zero and function $0x20$, giving $0x5020=20512$. The erroneous result is therefore $7+20512=20519$.

For the second test, preset $s0=L, $t3=4, memory at $L$ to 37 and memory at $L+4$ to 99, with both words valid and aligned. ExecuteNormally, and with ALUSrc stuck at one, the address is $L+0$ and the result is 37. With the line stuck at zero, the second ALU operand is the old $t3=4, so the load reads 99 from $L+4$. Thus

A writing MIPS instruction distinguishes a line stuck at zero. With $t0=7, $t1=5, $t2=99, executeA healthy line or a line stuck at one produces $t2=12; a line stuck at zero leaves $t2=99.

To distinguish normal operation from stuck at one, execute a normally nonwriting MIPS instruction. The following functional test uses the usual concrete controller choice MemToReg=0 during sw, selecting the ALU result on the write-data bus. Prepare $t0=37 and $s0=L-16384, for an aligned writable address $L\ne 37$, then executeThe ALU computes $L$. Here rt is register 8 ($t0), and immediate $16384=0x4000$ also puts 8 into bits $15\dots 11$. Thus either value of the otherwise irrelevant RegDst selects $t0. With a healthy RegWrite, $t0 remains 37. With RegWrite stuck at one and the specified write-data selection, the unwanted register file write changes $t0 to $L$. Combining the two independent observations gives

Controller qualification. The source diagram does not specify values of otherwise irrelevant control outputs during a store. MemToReg is a don't-care condition when RegWrite=0; its chosen implementation matters when that enable line is faulty. The functional test above explicitly fixes this convention instead of assuming that all implementations resolve it identically. A manufacturing fixture can also observe the register file write-enable directly while executing add followed by sw: the expected pairs are $(1,0)$ normally, $(0,0)$ stuck at zero, and $(1,1)$ stuck at one. This second observation does not depend on unused write-data controls or on whether an unwanted write happens to repeat an old value.

Run the following two MIPS instruction tests separately from externally prepared states, and inspect the register file after the indicated instruction. External preparation is useful in a manufacturing test: code that initializes processor registers through the very control line being tested need not work. Assume the one potentially faulty line is RegDst; all other lines work normally.

For the first test, preset $t0=7, $t1=5, $t2=99, and executeThe encoded rt is $t1, while rd is $t2. A healthy line or a line stuck at one writes 12 into $t2. A line stuck at zero instead writes 12 into $t1, leaving $t2=99.

For the second test, preset $t3=4, $s0=L, and the aligned memory word at $L$ to 37, then executeThe zero immediate makes instruction bits $15\dots 11$ zero. A healthy line or a line stuck at zero writes 37 into $t3; a line stuck at one attempts to write the MIPS zero register, leaving $t3=4. The MIPS zero register ignores attempted writes. Thus, recording the first test's $t2 and the second test's $t3,

There are $N+1-p$ candidate values in $[p,N+1)$ and exactly $N-k$ occurrences there. If $k\ge p$, thenThus the pigeonhole principle givesThis conclusion does not assert that every value on the lower side is present; duplicates may leave both sides deficient.

Take an integer pivot $0\le p\le N+1$. There are $p$ possible values in $[0,p)$ but only $k$ occurrences of such values in the whole array. When $k<p$, the pigeonhole principle givesRepeated values do not invalidate the argument: they can only reduce the number of distinct values represented by those $k$ occurrences. The other side might also contain a missing value.

A list unfold needs an explicit state describing the unvisited work. Use a list of pending rose trees, with the next tree first. Emit that tree's root label, and replace it by its children followed by the remaining pending trees:

dftU :: RTree a -> [a]
dftU t = unfold null label advance [t]
  where
    label :: [RTree a] -> a
    label (Node x _ : _) = x

    advance :: [RTree a] -> [RTree a]
    advance (Node _ children : rest) = children ++ rest

The boxed state transition is $\boxed{\mathrm{Node}(x,children):rest⟼children++rest}$, with output $x$. The stopping test prevents either helper from being applied to [].

The loop invariant is that concatenating the depth-first traversals of the pending trees gives exactly the unproduced output. Removing the next root emits its first label; replacing that tree by its children preserves the remainder of that preorder traversal. Adding children at the front realizes an explicit-stack depth-first tree traversal; placing them at the end would give a different visiting order. The first states for the source example have roots [1], [2,5,6], [3,4,5,6], [4,5,6], [5,6], [6], [7], [].

The child results supplied by the tree fold are already their depth-first traversals. Prepend the current label to their list concatenation:

dftF :: RTree a -> [a]
dftF = foldRTree visit
  where
    visit :: a -> [[a]] -> [a]
    visit x childLists = x : concat childLists

Thus $\boxed{\mathrm{dftF}=\mathrm{foldRTree}(\lambda xrs.x:\mathrm{concat}(rs))}$. Substituting the equation for the tree fold gives exactly the recursive preorder traversal equation from part (i), proving equality by structural induction on a finite rose tree.

Emit the root label, then concatenate the depth-first traversals of the child rose trees in order:

dft :: RTree a -> [a]
dft (Node x ts) = x : concatMap dft ts

This is preorder traversal:The Haskell concatMap function preserves child order and finishes each child subtree before moving to the next. A leaf yields its singleton label; the source example yields [1,2,3,4,5,6,7].

Let $X_i$ be the head indicator random variable for toss $i$. These are independent and identically distributed random variables with a Bernoulli distribution of parameter $1/2$, so $\mu =1/2$, $\sigma =1/2$, and $W=N/n$. Taking $h=1/5$ makes $h\sigma =1/10$. The preceding Chebyshev's inequality bound givesThe endpoints are included because this event is exactly $|W-1/2|\le 1/10$.

By linearity of expectation and independence,For $\sigma >0$, apply Chebyshev's inequality at threshold $h\sigma$ and take the complementary event:If $\sigma =0$, every $X_i=\mu$ almost surely, so $W=\mu$ almost surely and the bound holds directly. This handles the zero-threshold case without applying Chebyshev's inequality at an inadmissible threshold.

The logarithm is strictly increasing, so $\mathbb{P}(Y\le y)=\mathbb{P}(X\le e^y)$. Since $X>1$ almost surely,Thus the logarithm of a Pareto random variable has an exponential distribution with rate $c$. Its probability density function value at the single endpoint can be chosen arbitrarily without changing the law.