A variable $v$ is fresh for the relevant context when it occurs free in none of its undischarged assumptions. For the existential quantifier elimination rule, it must also not occur free in the final conclusion $\kappa$ or the existential premise: it is a new eigenvariable, allowed in the temporary witness assumption $\varphi (v)$ and formulas inside that witness subproof. Bound variable names can always be renamed to avoid collisions.

The premise $\exists x\varphi (x)$ guarantees some witness, without saying which object it is. Temporarily call one such witness $v$ and assume $\varphi (v)$. If the subproof yields $\kappa$ without depending on any special identity or extra property of $v$, its conclusion holds whichever witness exists. The existential quantifier elimination rule therefore discharges $\varphi (v)$ and retains only the original existential premise and other open assumptions.This eigenvariable condition prevents inferring $\varphi (v)$ for a previously chosen object merely from existence. In particular, $\exists xQ(x)$ does not license $Q(v)$ outside the discharged witness subproof.

Work backwards from the outermost available logical connective. One strategy applies the disjunction elimination rule to the premise first, constructs the whole target in each case, and then closes the cases. In the tables, a context such as $\{1,2\}$ means that assumptions on lines 1 and 2 remain open. A range in a discharge rule denotes the entire local subproof.

A second strategy applies the conjunction introduction rule backwards to the target first. Prove $P$ and $Q\vee R$ separately, each by the disjunction elimination rule on the premise, and combine them:

Both derivations establishCounting only applications of inference rules, each proof has nine steps: four conjunction elimination rule applications, two disjunction introduction rule applications, and three remaining applications. The first uses two conjunction introduction rule applications and one disjunction elimination rule; the second uses one and two, respectively. The second has two additional temporary-assumption lines, giving 14 displayed lines instead of 12, but assumptions are not additional inference applications. Its duplicated case analysis is exchanged for avoiding construction of the complete logical conjunction separately in both cases. In a proof tree it also repeats the use of the original premise.

The conjunction introduction rule derives $\varphi \wedge \psi$ from proofs of $\varphi$ and $\psi$ in the current context. The disjunction elimination rule derives a common conclusion $\kappa$ from $\varphi \vee \psi$, a subproof of $\kappa$ under temporary assumption $\varphi$, and a subproof of $\kappa$ under temporary assumption $\psi$. The implication introduction rule derives $\varphi \to \psi$ by temporarily assuming $\varphi$ and proving $\psi$.

The rectangular boxes delimit subproofs and the scope of their temporary assumptions. The disjunction elimination rule discharges the two case assumptions; the implication introduction rule discharges its antecedent assumption. Formulas depending on a boxed assumption cannot simply escape that box. Other undischarged assumptions remain in force, and nested boxes can access the assumptions of enclosing boxes.

A triangular matrix has determinant equal to the product of its diagonal entries. Since $L$ is a unit lower triangular matrix, $\det L=1$. ThusEquivalently, the elimination used only row additions, which leave the determinant unchanged; there were no row swaps or row scalings to account for.

Solve two triangular linear systems, rather than forming an inverse matrix:For this LU decomposition, forward substitution gives $y_1=b_1$, $y_2=b_2+2y_1$ and $y_3=b_3-3y_1+y_2$. Then back substitution givesAll diagonal entries used as divisors are nonzero. The same LU decomposition can be reused for many right-hand vectors, with only these two triangular solves repeated.

Use $R_2\leftarrow R_2+2R_1$ and $R_3\leftarrow R_3-3R_1$, followed by $R_3\leftarrow R_3+R_2$. These elementary row operations giveThe elimination multipliers are $m_{21}=-2$, $m_{31}=3$, $m_{32}=-1$. Record them in the unit lower triangular matrix $L$:To see the elementary matrix relation directly, let $F_{21}=I+2e_{21}$, $F_{31}=I-3e_{31}$ and $F_{32}=I+e_{32}$, where $e_{ij}$ has a single 1 in position $(i,j)$. Then $U=F_{32}{F}_{31}{F}_{21}A$, and reversing and inverting these operations gives $L=F_{21}^{-1}{F}_{31}^{-1}{F}_{32}^{-1}$. Direct matrix multiplication also verifies the stated LU decomposition.

An elementary matrix acts on rows by multiplication on the left. Apply the desired elementary row operation to the identity matrix to construct it. In the order requested, the three elementary matrices and their inverse matrices areThe inverse operations halve row 1, add twice row 1 to row 3, and interchange rows 2 and 3 again, respectively.

The reduced row echelon form yieldsTake the free variables in a linear system to be $s=x_2$, $t=x_4$, $u=x_5$. ThenThusEach listed vector lies in the null space, and every solution has the displayed form. Their coordinates in positions 2, 4 and 5 prove linear independence. The dimension also follows from the rank-nullity theorem: $5-2=3$.

The right-hand vector is in the column space, becauseConsequently the linear system is consistent. A concrete solution isAs a compatibility check, the original rows satisfy $r_1+11r_2-5r_3=0$, and the right-hand entries satisfy the same relation $1+11\cdot 4-5\cdot 9=0$. There are infinitely many solutions, obtained by adding any vector in the null space to the displayed solution.

The pivot columns of the reduced row echelon form are columns 1 and 3. Take those columns of the original matrix, since elementary row operations need not preserve the original column space:For an explicit spanning check, column 2 is $-2a_1$, column 4 is $-a_1+2a_3$, and column 5 is $3a_1-2a_3$. The first two coordinates of the displayed columns form a $2\times 2$ matrix of determinant $-5\ne 0$, proving their linear independence. They are therefore a basis of the column space.

Swap the first two rows, then perform $R_2\leftarrow R_2+R_1$ and $R_3\leftarrow R_3-2R_1$. These elementary row operations giveScale row 2 by $1/5$, subtract it from row 3, and finally subtract twice row 2 from row 1. The reduced row echelon form isElementary row operations preserve the row space. The two nonzero rows of $R$ are linearly independent, since their leading entries lie in different columns. Hence

Write the columns of $A$ as $a_1,\dots ,a_n$ and the coordinates of the vector $x$ as $x_1,\dots ,x_n$. By the definition of matrix multiplication,Indeed, its $i$th coordinate is ${\sum }_{j=1}^n{A}_{ij}{x}_j$, exactly the $i$th coordinate of this linear combination. Since the column space contains every linear combination of the columns, the claim holds for every vector $x$.

For a real $m\times n$ matrix $A$, the row space is the linear span of its rows in ${\mathbb{R}}^n$, and the column space is the linear span of its columns in ${\mathbb{R}}^m$. Its null space consists of the input vectors sent to zero:The rank of a matrix isThe equality of row and column dimensions is the row-rank/column-rank theorem. Each displayed space is a linear subspace of the indicated ambient vector space.

Summing the flow conservation equations over all four junctions cancels every internal flow. The total entering flow is $300+500+250+50+100=1200$, and the known exiting flow is $700+200=900$. ThusThe original arrows point $A\to B$, $C\to A$, $B\to D$, and $C\to D$ for $f_2,f_3,f_4,f_5$, respectively. In particular, $f_1$ exits north from $A$.^[ref]

The individual flow conservation equations areChoose $t=f_5$. Substitution gives all solutions of these linear equations:The inequalities enforce nonnegative flows on all one-way streets. The last junction equation follows from the first three and total flow conservation, so it introduces no further restriction.

The maximum is $\boxed{f_5=150}$. It makes $f_2=f_3=0$. At $A$, all 300 vehicles arriving from the west turn north and leave along $f_1$; none arrives from $C$ or continues east to $B$.

Apply the elementary row operations from bottom to top: $R_4\leftarrow R_4-R_3$, $R_3\leftarrow R_3-R_2$, and $R_2\leftarrow R_2-R_1$. This order ensures that each subtraction uses the original preceding row. The result is the upper triangular matrixPut ${\delta }_1=a$, ${\delta }_2=b-a$, ${\delta }_3=c-b$, ${\delta }_4=d-c$. Row $i$ is either zero if ${\delta }_i=0$, or has its first nonzero entry in column $i$. Thus, for arbitrary real parameters, a row echelon form is obtained by retaining the nonzero rows of $T$ in their existing order and moving every zero row to the bottom. This deals explicitly with vanishing parameters; an upper triangular matrix with an intermediate zero row is not yet a row echelon form.

The subtractions preserve the determinant, so the original matrix hasA square matrix is invertible exactly when its determinant is nonzero. Consequently,These conditions concern consecutive parameters: no ordering, positivity, or pairwise distinctness of all four is required. More generally the rank of a matrix here is the number of nonzero ${\delta }_i$, because the retained nonzero rows have distinct leading columns.