This is the equality congruence rule for disjunction. It takes two boolean equality theorems, and disjoins corresponding sides of the first theorem with the second, unioning the assumptions. A1 |- p1 <=> p2 A2 |- q1 <=> q2 ---------------------------------- A1 u A2 |- p1 \/ q1 <=> p2 \/ q2 See also: mk_disj1_rule, mk_disj2_rule, mk_bin_rule, disj1_rule, disj2_rule.

This is the equality congruence rule for binary function LHS application. It takes a binary function term, an equality theorem and a RHS argument term, and applies the function in curried form to corresponding sides of the theorem as its LHS argument and the supplied RHS argument. The type of the supplied function must be a binary curried function type, with first domain type equal to the type of each side of the theorem, and second domain type equal to the type of the RHS argument term. `f` |- s1 = s2 `t` ---------------------- |- f s1 t = f s2 t See also: mk_bin2_rule, mk_bin_rule, mk_comb_rule.

This is the equality congruence rule for binary function RHS application. It takes a binary function term, a LHS argument term and an equality theorem, and applies the function in curried form to the supplied LHS argument and corresponding sides of the theorem as its RHS argument. The type of the supplied function must be a binary curried function type, with first domain type equal to the type of the LHS argument term, and second domain type equal to the type of each side of the theorem. `f` `s` |- t1 = t2 ---------------------- |- f s t1 = f s t2 See also: mk_bin1_rule, mk_bin_rule, mk_comb_rule.

This is the equality congruence rule for binary function application. It takes a binary function term and two equality theorems, and applies the function in curried form to corresponding sides of each theorem, under their unioned assumptions. The type of the supplied function must be a binary curried function type, with first and second domain types equal to the type of each side of their corresponding theorems. `f` A1 |- s1 = s2 A2 |- t1 = t2 ------------------------------------ A1 u A2 |- f s1 t1 = f s2 t2 See also: mk_bin1_rule, mk_bin2_rule, mk_comb_rule, mk_conj_rule, mk_disj_rule, mk_imp_rule, mk_eq_rule, mk_pair_rule.

This is the equality congruence rule for conjunction LHS. It takes a boolean equality theorem and a boolean term, and conjoins each side of the theorem with the supplied term. A |- p1 <=> p2 `q` ------------------------ A |- p1 /\ q <=> p2 /\ q See also: mk_conj2_rule, mk_conj_rule, mk_bin1_rule, conj_rule.

mk_conj2_rule : term -> thm -> thm This is the equality congruence rule for conjunction RHS. It takes a boolean term and a boolean equality theorem, and conjoins the supplied term with each side of the theorem. `p` A |- q1 <=> q2 ------------------------ A |- p /\ q1 <=> p /\ q2 See also: mk_conj1_rule, mk_conj_rule, mk_bin2_rule, conj_rule.

This is the equality congruence rule for conjunction. It takes two boolean equality theorems, and conjoins corresponding sides of the first theorem with the second, unioning the assumptions. A1 |- p1 <=> p2 A2 |- q1 <=> q2 ---------------------------------- A1 u A2 |- p1 /\ q1 <=> p2 /\ q2 See also: mk_conj1_rule, mk_conj2_rule, mk_bin_rule, conj_rule.

This is the equality congruence rule for disjunction LHS. It takes a boolean equality theorem and a boolean term, and disjoins each side of the theorem with the supplied term. A |- p1 <=> p2 `q` ------------------------ A |- p1 \/ q <=> p2 \/ q See also: mk_disj2_rule, mk_disj_rule, mk_bin1_rule, disj1_rule.

This is the equality congruence rule for disjunction RHS. It takes a boolean term and a boolean equality theorem, and disjoins the supplied term with each side of the theorem. `p` A |- q1 <=> q2 ------------------------ A |- p \/ q1 <=> p \/ q2 See also: mk_disj1_rule, mk_disj_rule, mk_bin2_rule, disj2_rule.

This is the equality congruence rule for equality LHS. It takes an equality theorem and a term, and equates each side of the theorem with the supplied term. The type of the supplied term must equal the types of each side of the supplied theorem. A |- s1 = s2 `t` ---------------------- A |- s1 = t <=> s2 = t See also: mk_eq2_rule, mk_eq_rule, mk_eq1_rule.

This is the equality congruence rule for equality RHS. It takes a term and an equality theorem, and equates the term to each side of the theorem. The type of the supplied term must equal the types of each side of the supplied theorem. `s` A |- t1 = t2 ---------------------- A |- s = t1 <=> s = t2 See also: mk_eq1_rule, mk_eq_rule, mk_eq2_rule.

This is the equality congruence rule for equality. It takes two equality theorems, and equates corresponding sides of the first theorem with the second, unioning the assumptions. The types of each side of each equation must all be equal. A1 |- s1 = s2 A2 |- t1 = t2 ------------------------------ A1 u A2 |- s1 = t1 <=> s2 = t2 See also: mk_eq1_rule, mk_eq2_rule, mk_eq_rule.

This is the equality congruence rule for existential quantification. It takes a variable and an equality theorem, and existentially quantifies the variable on both sides of the theorem. The variable must not occur free in the assumptions of the supplied theorem. `x` A |- p1 <=> p2 [ "x" not free in `A` ] -------------------------- A |- (?x. p1) <=> (?x. p2) See also: mk_uexists_rule, mk_abs_rule, mk_comb_rule, exists_rule.

This is the equality congruence rule for universal quantification. It takes a variable and an equality theorem, and universally quantifies the variable on both sides of the theorem. The variable must not occur free in the assumptions of the supplied theorem. `x` A |- p1 <=> p2 [ "x" not free in `A` ] -------------------------- A |- (!x. p1) <=> (!x. p2) See also: mk_abs_rule, mk_comb_rule, gen_rule.

This is the equality congruence rule for implication LHS. It takes a boolean equality theorem and a boolean term, and creates implications out of each side of the theorem, with the theorem side as the antecedent and the term as the consequent. A |- p1 <=> p2 `q` -------------------------- A |- p1 ==> q <=> p2 ==> q See also: mk_imp2_rule, mk_imp_rule, mk_bin1_rule.

This is the equality congruence rule for implication RHS. It takes a boolean term and a boolean equality theorem, and makes the term an antecedent of each side of the theorem. `p` A |- q1 <=> q2 -------------------------- A |- p ==> q1 <=> p ==> q2 See also: mk_imp1_rule, mk_imp_rule, mk_bin2_rule.

This is the equality congruence rule for implication. It takes two boolean equality theorems, and creates implications out of corresponding sides of the first theorem and the second, unioning the assumptions. A1 |- p1 <=> p2 A2 |- q1 <=> q2 ---------------------------------- A1 u A2 |- p1 ==> q1 <=> p2 ==> q2 See also: mk_imp1_rule, mk_imp2_rule, mk_bin_rule.

This is the equality congruence rule for logical negation. Its takes a boolean equality theorem, and logically negates each side of the theorem. A |- p1 <=> p2 ------------------ A |- ~ p1 <=> ~ p2 See also: mk_comb_rule, eqf_intro_rule, eqf_elim_rule.

This is the equality congruence rule for selection. It takes a variable and an equality theorem, and selects the variable from both sides of the theorem. The variable must not occur free in the assumptions of the supplied theorem. `x` A |- p1 <=> p2 [ "x" not free in `A` ] ------------------------ A |- (@x. p1) = (@x. p2) See also: mk_abs_rule, mk_comb_rule.

This is the equality congruence rule for unique existential quantification. It takes a variable and an equality theorem, and unique- existentially quantifies the variable on both sides of the theorem. The variable must not occur free in the assumptions of the supplied theorem. `x` A |- p1 <=> p2 [ "x" not free in `A` ] ---------------------------- A |- (?!x. p1) <=> (?!x. p2) See also: mk_exists_rule, mk_abs_rule, mk_comb_rule