Theory: rules

Rule: baseEquality

This rule proved as lemma rule_base_equality_true3 in file rules/rules_base.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ Base = Base ∈ Type

  BY baseEquality ()

  No Subgoals

Rule: imageEquality

This rule proved as lemma rule_image_equality_true in file rules/rules_image.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ Image(A1,f1) = Image(A2,f2) ∈ Type

  BY imageEquality !parameter{i:l} ()

  H  ⊢ f1 = f2 ∈ Base
  H  ⊢ A1 = A2 ∈ Type

Rule: equalityEquality
H  ⊢ (a11 = a12 ∈ A1) = (a21 = a22 ∈ A2) ∈ Type

  BY equalityEquality X Y x y u z ()

  H  ⊢ A1 = A2 ∈ Type
  H  ⊢ a11 = a21 ∈ X
  H  ⊢ a12 = a22 ∈ Y
  H x:Base, y:Base, u:(x = y ∈ X), z:(x ∈ A1) ⊢ x = y ∈ A1
  H x:Base, y:Base, u:(x = y ∈ Y), z:(x ∈ A1) ⊢ x = y ∈ A1

Rule: baseAtom
This rule proved as lemma rule_atom_subtype_base_true in file rules/rules_squiggle5.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ t1 = t2 ∈ Base

  BY baseAtom ()

  H  ⊢ t1 = t2 ∈ Atom

Rule: lessTrichotomy
H  ⊢ a = b ∈ ℤ

  BY lessTrichotomy ()

  H  ⊢ if (a) < (b)  then False  else True
  H  ⊢ if (b) < (a)  then False  else True
  H  ⊢ a ∈ ℤ
  H  ⊢ b ∈ ℤ

Rule: baseInt
This rule proved as lemma rule_int_subtype_base_true in file rules/rules_squiggle5.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ t1 = t2 ∈ Base

  BY baseInt ()

  H  ⊢ t1 = t2 ∈ ℤ

Rule: addMonotonic
H  ⊢ if (a + c) < (b + c)  then True  else False

  BY addMonotonic ()

  H  ⊢ if (a) < (b)  then True  else False
  H  ⊢ a ∈ ℤ
  H  ⊢ b ∈ ℤ
  H  ⊢ c ∈ ℤ

Rule: baseAtomn
This rule proved as lemma rule_uatom_subtype_base_true in file rules/rules_squiggle5.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ Base

  BY baseAtomn !parameter{$n:n}

  H  ⊢ a = b ∈ Atom$n

Rule: atomn_eqEquality
H  ⊢ if a1=$n b1 then s1 else t1 = if a2=$n b2 then s2 else t2 ∈ T

  BY atomn_eqEquality v

  H  ⊢ a1 = a2 ∈ Atom$n
  H  ⊢ b1 = b2 ∈ Atom$n
  H v:(a1 = b1 ∈ Atom$n) ⊢ s1 = s2 ∈ T
  H v:((a1 = b1 ∈ Atom$n) ⟶ Void) ⊢ t1 = t2 ∈ T

Rule: freeFromAtomEquality
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a1#x1:T1 = a2#x2:T2 ∈ Type

  BY freeFromAtomEquality ()

  H  ⊢ T1 = T2 ∈ Type
  H  ⊢ x1 = x2 ∈ T1
  H  ⊢ a1 = a2 ∈ Atom$n

Rule: bottomDiverges
This rule proved as lemma rule_bottom_diverges_true3 in file rules/rules_false.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ ¬(⊥)↓

  BY bottomDiverges ()

  No Subgoals

Rule: sqleIntensionalEquality
H  ⊢ (a ≤ b) = (c ≤ d) ∈ Type

  BY sqleIntensionalEquality ()

     Let SubGoals = CallLisp(SQLE-EQUALITY)
  SubGoals

Rule: isatom1Cases
H  ⊢ C ext !((!\\x.isatom1(t;ea;eb)) Ax)

  BY isatom1Cases x t u v ()

  H  ⊢ 0 ≤ eval x = t in 0
  H  ⊢ t ∈ Base
  H x:(t ∈ Atom1) ⊢ C ext ea
  H x:(∀[u,v:Base].  (isatom1(t;u;v) ~ v)) ⊢ C ext eb

Rule: isatom2Cases
H  ⊢ C ext !((!\\x.isatom2(t;ea;eb)) Ax)

  BY isatom2Cases x t u v ()

  H  ⊢ 0 ≤ eval x = t in 0
  H  ⊢ t ∈ Base
  H x:(t ∈ Atom2) ⊢ C ext ea
  H x:(∀[u,v:Base].  (isatom2(t;u;v) ~ v)) ⊢ C ext eb

Rule: exceptionNotBottom
This rule proved as lemma rule_exception_not_bottom_true in file rules/rules_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ C

  BY exceptionNotBottom x y ()

  H  ⊢ exception(x; y) ≤ ⊥

Rule: exceptionNotAxiom
This rule proved as lemma rule_exception_not_axiom_true in file rules/rules_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ C

  BY exceptionNotAxiom x y ()


  H  ⊢ Ax ≤ exception(x; y)

Rule: isAtom1ReduceTrue
H  ⊢ isatom1(z;a;b) ~ a

  BY isAtom1ReduceTrue ()

  H  ⊢ z = z ∈ Atom1

Rule: callbyvalueAtom
H  ⊢ 0 ≤ eval x = a in 0

  BY callbyvalueAtom ()

  H  ⊢ a ∈ Atom

Rule: callbyvalueAtom1
H  ⊢ 0 ≤ eval x = a in 0

  BY callbyvalueAtom1 ()

  H  ⊢ a ∈ Atom1

Rule: callbyvalueAtom2
H  ⊢ 0 ≤ eval x = a in 0

  BY callbyvalueAtom2 ()

  H  ⊢ a ∈ Atom2

Rule: callbyvalueType
This rule proved as lemma rule_callbyvalue_type_true3 in file rules/rules_uni.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ 0 ≤ eval x = T in 0

  BY callbyvalueType !parameter{i:l}

  H  ⊢ T ∈ Type

Rule: applyInt
This rule proved as lemma rule_apply_int_true in file rules/rules_apply_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ m b ≤ ⊥

  BY applyInt ()

  H  ⊢ m ∈ ℤ

Rule: isatomCases
H  ⊢ C ext !((!\\x.if t is an atom then ea otherwise eb) Ax)

  BY isatomCases x t u v ()

  H  ⊢ 0 ≤ eval x = t in 0
  H  ⊢ t ∈ Base
  H x:(t ∈ Atom) ⊢ C ext ea
  H x:(∀[u,v:Base].  (if t is an atom then u otherwise v ~ v)) ⊢ C ext eb

Rule: callbyvalueTry
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY callbyvalueTry m u x y t n v c ()

  H  ⊢ (t?n:v.c)↓
  H x:(t)↓, y:(t?n:v.c ~ if n=2 n then t else ⊥) ⊢ a = b ∈ T

  H m:Base, u:Base, x:(t ~ exception(m; u)), y:(t?n:v.c ~ if n=2 m then c[u/v] else (exception(m; u))) ⊢ a = b ∈ T

  H  ⊢ t ∈ Base
  H  ⊢ n ∈ Base
  H v:Base ⊢ c ∈ Base

Rule: callbyvalueInt
This rule proved as lemma rule_callbyvalue_int_true3 in file rules/rules_number.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ 0 ≤ eval x = a in 0

  BY callbyvalueInt ()

  H  ⊢ a ∈ ℤ

Rule: exceptionMultiply
This rule proved as lemma rule_exception_arith_true3 in file rules/rules_arith_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ x * (exception(u; v)) ~ exception(u; v)

  BY exceptionMultiply ()

  H  ⊢ x ∈ ℤ

Rule: exceptionDivide
This rule proved as lemma rule_exception_arith_true3 in file rules/rules_arith_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ x ÷ exception(u; v) ~ exception(u; v)

  BY exceptionDivide ()

  H  ⊢ x ∈ ℤ

Rule: exceptionRemainder
This rule proved as lemma rule_exception_arith_true3 in file rules/rules_arith_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ x rem exception(u; v) ~ exception(u; v)

  BY exceptionRemainder ()

  H  ⊢ x ∈ ℤ

Rule: addAssociative
This rule proved as lemma rule_add_associative_true in file rules/rules_integer_ring.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ ((m + n) + k) = (m + n + k) ∈ ℤ

  BY addAssociative ()

  H  ⊢ m = m ∈ ℤ
  H  ⊢ n = n ∈ ℤ
  H  ⊢ k = k ∈ ℤ

Rule: addCommutative
This rule proved as lemma rule_add_commutative_true in file rules/rules_integer_ring.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (m + n) = (n + m) ∈ ℤ

  BY addCommutative ()

  H  ⊢ m = m ∈ ℤ
  H  ⊢ n = n ∈ ℤ

Rule: addInverse
This rule proved as lemma rule_add_inverse_true in file rules/rules_integer_ring.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (n + (-n)) = 0 ∈ ℤ

  BY addInverse ()

  H  ⊢ n = n ∈ ℤ

Rule: multiplyCommutative
This rule proved as lemma rule_mul_commutative_true in file rules/rules_integer_ring.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (m * n) = (n * m) ∈ ℤ

  BY multiplyCommutative ()

  H  ⊢ m = m ∈ ℤ
  H  ⊢ n = n ∈ ℤ

Rule: addZero
This rule proved as lemma rule_add_zero_true in file rules/rules_integer_ring.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (0 + n) = n ∈ ℤ

  BY addZero ()

  H  ⊢ n = n ∈ ℤ

Rule: multiplyOne

This rule proved as lemma rule_mul_one_true in file rules/rules_integer_ring.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ (1 * n) = n ∈ ℤ

  BY multiplyOne ()

  H  ⊢ n = n ∈ ℤ

Rule: multiplyAssociative
This rule proved as lemma rule_mul_associative_true in file rules/rules_integer_ring.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ ((m * n) * k) = (m * n * k) ∈ ℤ

  BY multiplyAssociative ()

  H  ⊢ m = m ∈ ℤ
  H  ⊢ n = n ∈ ℤ
  H  ⊢ k = k ∈ ℤ

Rule: multiplyDistributive
This rule proved as lemma rule_mul_distributive_true in file rules/rules_integer_ring.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (m * (n + k)) = ((m * n) + (m * k)) ∈ ℤ

  BY multiplyDistributive ()

  H  ⊢ m = m ∈ ℤ
  H  ⊢ n = n ∈ ℤ
  H  ⊢ k = k ∈ ℤ

Rule: lessTransitive
H  ⊢ if (a) < (c)  then True  else False

  BY lessTransitive b

  H  ⊢ if (a) < (b)  then True  else False
  H  ⊢ if (b) < (c)  then True  else False
  H  ⊢ a ∈ ℤ
  H  ⊢ b ∈ ℤ
  H  ⊢ c ∈ ℤ

Rule: lessDiscrete
H  ⊢ (1 + a) = b ∈ ℤ

  BY lessDiscrete ()

  H  ⊢ if (a) < (b)  then True  else False
  H  ⊢ if (1 + a) < (b)  then False  else True
  H  ⊢ a ∈ ℤ
  H  ⊢ b ∈ ℤ

Rule: multiplyPositive
H  ⊢ if (0) < (a * b)  then True  else False

  BY multiplyPositive ()

  H  ⊢ if (0) < (a)  then True  else False
  H  ⊢ if (0) < (b)  then True  else False
  H  ⊢ a ∈ ℤ
  H  ⊢ b ∈ ℤ

Rule: divremEquality
This rule proved as lemma rule_arithop_equality_true3 in file rules/rules_arith.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ divrem(m1; n1) = divrem(m2; n2) ∈ (ℤ × ℤ)

  BY divremEquality ()

  H  ⊢ m1 = m2 ∈ ℤ
  H  ⊢ n1 = n2 ∈ ℤ
  H  ⊢ n1 ≠ 0

Rule: divideRemainderSum
H  ⊢ a = (((a ÷ b) * b) + (a rem b)) ∈ ℤ

  BY divideRemainderSum ()

  H  ⊢ if b=0 then False else True
  H  ⊢ a ∈ ℤ
  H  ⊢ b ∈ ℤ

Rule: remZero
H  ⊢ (0 rem b) = 0 ∈ ℤ

  BY remZero ()

  H  ⊢ if b=0 then False else True
  H  ⊢ b ∈ ℤ

Rule: remainderBounds1
H  ⊢ if (a rem b) < (b)  then True  else False

  BY remainderBounds1 ()

  H  ⊢ if (0) < (a)  then True  else False
  H  ⊢ if (0) < (b)  then True  else False
  H  ⊢ a ∈ ℤ
  H  ⊢ b ∈ ℤ

Rule: remainderBounds2
H  ⊢ if (-b) < (a rem b)  then True  else False

  BY remainderBounds2 ()

  H  ⊢ if (a) < (0)  then True  else False
  H  ⊢ if (0) < (b)  then True  else False
  H  ⊢ a ∈ ℤ
  H  ⊢ b ∈ ℤ

Rule: remainderBounds3
H  ⊢ if (b) < (a rem b)  then True  else False

  BY remainderBounds3 ()

  H  ⊢ if (a) < (0)  then True  else False
  H  ⊢ if (b) < (0)  then True  else False
  H  ⊢ a ∈ ℤ
  H  ⊢ b ∈ ℤ

Rule: remNegative
H  ⊢ if (0) < (a rem b)  then False  else True

  BY remNegative ()

  H  ⊢ if (a) < (0)  then True  else False
  H  ⊢ if b=0 then False else True
  H  ⊢ a ∈ ℤ
  H  ⊢ b ∈ ℤ

Rule: remainderBounds4
H  ⊢ if (a rem b) < (-b)  then True  else False

  BY remainderBounds4 ()

  H  ⊢ if (0) < (a)  then True  else False
  H  ⊢ if (b) < (0)  then True  else False
  H  ⊢ a ∈ ℤ
  H  ⊢ b ∈ ℤ

Rule: remPositive
H  ⊢ if (a rem b) < (0)  then False  else True

  BY remPositive ()

  H  ⊢ if (0) < (a)  then True  else False
  H  ⊢ if b=0 then False else True
  H  ⊢ a ∈ ℤ
  H  ⊢ b ∈ ℤ

Rule: isAtom2ReduceTrue
H  ⊢ isatom2(z;a;b) ~ a

  BY isAtom2ReduceTrue ()

  H  ⊢ z = z ∈ Atom2

Rule: exceptionAtomeq2
H  ⊢ if x=2 exception(u; v) then y else z ~ exception(u; v)

  BY exceptionAtomeq2 ()

  H  ⊢ x ∈ Atom2

Rule: exceptionAtomeq1
H  ⊢ if x=1 exception(u; v) then y else z ~ exception(u; v)

  BY exceptionAtomeq1 ()

  H  ⊢ x ∈ Atom1

Rule: atomn_eqReduceFalseSq
H  ⊢ if a=$n b then s else t ~ u

  BY atomn_eqReduceFalseSq ()

  H  ⊢ t ~ u
  H  ⊢ (a = b ∈ Atom$n) ⟶ Void

Rule: isinrExceptionCases
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY isinrExceptionCases x t u v ()

  H  ⊢ is-exception(if t is inr then u else v)
  H x:(t)↓ ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueIsinr
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (p)↓

  BY callbyvalueIsinr a b ()

  H  ⊢ 0 ≤ eval if p is inr then a else b; 0

Rule: isatom1ExceptionCases
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY isatom1ExceptionCases x t u v ()

  H  ⊢ is-exception(isatom1(t;u;v))
  H x:(t)↓ ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueIsatom1
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (p)↓

  BY callbyvalueIsatom1 a b ()

  H  ⊢ 0 ≤ eval isatom1(p;a;b); 0

Rule: isatom2ExceptionCases
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY isatom2ExceptionCases x t u v ()

  H  ⊢ is-exception(isatom2(t;u;v))
  H x:(t)↓ ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueIsatom2
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (p)↓

  BY callbyvalueIsatom2 a b ()

  H  ⊢ 0 ≤ eval isatom2(p;a;b); 0

Rule: atom1_eqExceptionCases
H  ⊢ a = b ∈ T

  BY atom1_eqExceptionCases x y t u z w ()

  H  ⊢ is-exception(if t=1 u then z else w)
  H x:(t ∈ Atom1), y:(u ∈ Atom1) ⊢ a = b ∈ T
  H x:(t ∈ Atom1), y:is-exception(u) ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ u ∈ Base

Rule: remainderExceptionCases
This rule proved as lemma rule_arith_exception_cases_true in file rules/rules_arith_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY remainderExceptionCases x y t u ()

  H  ⊢ is-exception(t rem u)
  H x:(t ∈ ℤ), y:is-exception(u) ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ u ∈ Base

Rule: callbyvalueRemainder
This rule proved as lemma rule_callbyvalue_arith_true in file rules/rules_arith_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (a ∈ ℤ) ∧ (b ∈ ℤ) ext <Ax, Ax>

  BY callbyvalueRemainder ()

  H  ⊢ 0 ≤ eval a rem b; 0
  H  ⊢ a ∈ Base
  H  ⊢ b ∈ Base

Rule: exceptionAtomeq
H  ⊢ if x=exception(u; v) then y else z fi  ~ exception(u; v)

  BY exceptionAtomeq ()

  H  ⊢ x ∈ Atom

Rule: atom_eqExceptionCases
H  ⊢ a = b ∈ T

  BY atom_eqExceptionCases x y t u z w ()

  H  ⊢ is-exception(if t=u then z else w fi )
  H x:(t ∈ Atom), y:(u ∈ Atom) ⊢ a = b ∈ T
  H x:(t ∈ Atom), y:is-exception(u) ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ u ∈ Base

Rule: atom_eqReduceFalseSq
H  ⊢ if a=b then s else t fi  ~ u

  BY atom_eqReduceFalseSq ()

  H  ⊢ t ~ u
  H  ⊢ (a = b ∈ Atom) ⟶ Void

Rule: atom_eqReduceTrueSq
H  ⊢ if a=b then s else t fi  ~ u

  BY atom_eqReduceTrueSq ()

  H  ⊢ s ~ u
  H  ⊢ a = b ∈ Atom

Rule: bar_Induction
H  ⊢ f 0 c ∈ X 0 c

  BY bar_Induction T B !parameter{i:l} a s x m n t ()

     n,s can not occur free in B
  H  ⊢ T ∈ Type
  H n:ℕ, s:(ℕn ⟶ T) ⊢ (B n s) ∨ (¬(B n s))
  H a:(ℕ ⟶ T) ⊢ ↓∃n:ℕ. (B n a)
  H n:ℕ, s:(ℕn ⟶ T), x:B n s ⊢ f n s ∈ X n s

  H n:ℕ, s:(ℕn ⟶ T), x:(∀t:T. (f (n + 1) (λm.if m=n then t else (s m)) ∈ X (n + 1) (λm.if m=n then t else (s m))))

     ⊢ f n s ∈ X n s

Rule: sqequalnIntensionalEquality
H  ⊢ (a ~n b) = (c ~m d) ∈ Type

  BY sqequalnIntensionalEquality ()

  H  ⊢ n = m ∈ ℕ
  H  ⊢ a = c ∈ Base
  H  ⊢ b = d ∈ Base

Rule: sqlenIntensionalEquality
H  ⊢ (a ≤n b) = (c ≤m d) ∈ Type

  BY sqlenIntensionalEquality ()

  H  ⊢ n = m ∈ ℕ
  H  ⊢ a = c ∈ Base
  H  ⊢ b = d ∈ Base

Rule: sqlenSubtypeRel
H x:(a ≤n + 1 b), J ⊢ a ≤n b

  BY sqlenSubtypeRel #$i

  H  ⊢ n = n ∈ ℕ

Rule: sqequalnSqlen
H  ⊢ a ~n b

  BY sqequalnSqlen ()

  H  ⊢ a ≤n b
  H  ⊢ b ≤n a

Rule: sqequalnSymm
H  ⊢ a ~n b

  BY sqequalnSymm ()

  H  ⊢ b ~n a

Rule: applyInr
This rule proved as lemma rule_apply_inr_true in file rules/rules_apply_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (inr a ) b ≤ ⊥

  BY applyInr ()

  No Subgoals

Rule: applyInl
This rule proved as lemma rule_apply_inl_true in file rules/rules_apply_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (inl a) b ≤ ⊥

  BY applyInl ()

  No Subgoals

Rule: applyPair
This rule proved as lemma rule_apply_pair_true in file rules/rules_apply_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ <a, b> c ≤ ⊥

  BY applyPair ()

  No Subgoals

Rule: isinlExceptionCases
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY isinlExceptionCases x t u v ()

  H  ⊢ is-exception(if t is inl then u else v)
  H x:(t)↓ ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueIsinl
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (p)↓

  BY callbyvalueIsinl a b ()

  H  ⊢ 0 ≤ eval if p is inl then a else b; 0

Rule: isintExceptionCases
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY isintExceptionCases x t u v ()

  H  ⊢ is-exception(if t is an integer then u else v)
  H x:(t)↓ ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueIsint
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (p)↓

  BY callbyvalueIsint a b ()

  H  ⊢ 0 ≤ eval if p is an integer then a else b; 0

Rule: isatomExceptionCases
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY isatomExceptionCases x t u v ()

  H  ⊢ is-exception(if t is an atom then u otherwise v)
  H x:(t)↓ ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueIsatom
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (p)↓

  BY callbyvalueIsatom a b ()

  H  ⊢ 0 ≤ eval if p is an atom then a otherwise b; 0

Rule: imageEqInduction
H y:(t2 = (f t1) ∈ Image(A,f)) ⊢ t2 = (f t1) ∈ T

  BY imageEqInduction #$i a b z ()

  H  ⊢ f ∈ Base
  H  ⊢ t1 ∈ A
  H  ⊢ f t1 ∈ T
  H a:Base, b:Base, y:(f a ∈ T), z:(a = b ∈ A) ⊢ (f a) = (f b) ∈ T

Rule: tryReduceValue
This rule proved as lemma rule_try_reduce_value_true in file rules/rules_exception2.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ t1?n:x.t2 ~ if n=2 n then t1 else ⊥

  BY tryReduceValue ()

  H  ⊢ 0 ≤ eval t1; 0

Rule: universeMemberTYPE
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ T ∈ TYPE

  BY universeMemberTYPE !parameter{i:l} ()

  H  ⊢ T = T ∈ Type

Rule: callbyvalueAtomEq
H  ⊢ (a ∈ Atom) ∧ (b ∈ Atom) ext <Ax, Ax>

  BY callbyvalueAtomEq u v ()

  H  ⊢ 0 ≤ eval if a=b then u else v fi ; 0
  H  ⊢ a ∈ Base
  H  ⊢ b ∈ Base

Rule: pertypeEquality
This rule proved as lemma rule_pertype_equality_true in file rules/rules_pertype.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ pertype(R) = pertype(R') ∈ Type

  BY pertypeEquality x y z u v ()

  H x:Base, y:Base ⊢ R x y ∈ Type
  H x:Base, y:Base ⊢ R' x y ∈ Type
  H x:Base, y:Base, z:R x y ⊢ R' x y
  H x:Base, y:Base, z:R' x y ⊢ R x y
  H x:Base, y:Base, z:R x y ⊢ R y x
  H x:Base, y:Base, z:Base, u:R x y, v:R y z ⊢ R x z

Rule: old_sqequalHypSubstitution
H j:T[a/x] @lvl, J ⊢ C ext t

  BY sqequalHypSubstitution #$i (a ~ b) x T

  H j:T[a/x] @lvl, J ⊢ a ~ b
  H j:T[b/x] @lvl, J ⊢ C ext t

Rule: old_sqequalSubstitution
H  ⊢ T[a/x] ext t

  BY sqequalSubstitution (a ~ b) x T

  H  ⊢ a ~ b
  H  ⊢ T[b/x] ext t

Rule: sqleExtensionalEquality
This rule proved as lemma rule_approx_extensional_equality_true in file rules/rules_squiggle4.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (a ≤ b) = (c ≤ d) ∈ Type

  BY sqleExtensionalEquality ()

  H  ⊢ ↓a ≤ b ⇐⇒ c ≤ d

Rule: dependentIntersectionEquality
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ x1:a1 ⋂ b1 = x2:a2 ⋂ b2 ∈ Type

  BY dependentIntersectionEquality y

  H  ⊢ a1 = a2 ∈ Type
  H y:a1 ⊢ b1[y/x1] = b2[y/x2] ∈ Type

Rule: depIsectIsType
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ istype(a:A ⋂ B)

  BY depIsectIsType z ()

  H  ⊢ istype(A)
  H z:A ⊢ istype(B[z/a])

Rule: isaxiomCases
This rule proved as lemma rule_isaxiom_cases_true in file rules/rules_axiom_cases.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ C ext !((!\\x.if t = Ax then ea otherwise eb) Ax)

  BY isaxiomCases x t u v ()

  H  ⊢ 0 ≤ eval x = t in 0
  H  ⊢ t ∈ Base
  H x:(t ~ Ax) ⊢ C ext ea
  H x:(∀[u,v:Base].  (if t = Ax then u otherwise v ~ v)) ⊢ C ext eb

Rule: isaxiomExceptionCases
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY isaxiomExceptionCases x t u v ()

  H  ⊢ is-exception(if t = Ax then u otherwise v)
  H x:(t)↓ ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base

Rule: exceptionInteq
H  ⊢ if x=exception(u; v) then y else z ~ exception(u; v)

  BY exceptionInteq ()

  H  ⊢ x ∈ ℤ

Rule: exceptionAdd
This rule proved as lemma rule_exception_arith_true3 in file rules/rules_arith_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ x + (exception(u; v)) ~ exception(u; v)

  BY exceptionAdd ()

  H  ⊢ x ∈ ℤ

Rule: minusExceptionCases
This rule proved as lemma rule_minus_exception_cases_true in file rules/rules_arith_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY minusExceptionCases x t ()

  H  ⊢ is-exception(-t)
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueMinus
This rule proved as lemma rule_callbyvalue_minus_true in file rules/rules_arith_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a ∈ ℤ

  BY callbyvalueMinus ()

  H  ⊢ 0 ≤ eval -a; 0
  H  ⊢ a ∈ Base

Rule: direct_computation
H  ⊢ T ext t

  BY direct_computation S

     Let C = CallLisp(DIRECT-COMPUTATION)
  H  ⊢ C ext t

Rule: reverse_direct_computation
H  ⊢ T ext t

  BY reverse_direct_computation S

     Let C = CallLisp(REVERSE-DIRECT-COMPUTATION)
  H  ⊢ C ext t

Rule: direct_computation_hypothesis
H x:A @lvl, J ⊢ T ext t

  BY direct_computation_hypothesis #$i S

     Let B = CallLisp(DIRECT-COMPUTATION-HYPOTHESIS)
  H x:B @lvl, J ⊢ T ext t

Rule: reverse_direct_computation_hypothesis
H x:A @lvl, J ⊢ T ext t

  BY reverse_direct_computation_hypothesis #$i S

     Let B = CallLisp(REVERSE-DIRECT-COMPUTATION-HYPOTHESIS)
  H x:B @lvl, J ⊢ T ext t

Rule: callbyvalueIsaxiom
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (p)↓

  BY callbyvalueIsaxiom a b ()

  H  ⊢ 0 ≤ eval if p = Ax then a otherwise b; 0

Rule: sqleTransitivity
This rule proved as lemma rule_approx_trans_true3 in file rules/rules_squiggle8.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a ≤ b

  BY sqleTransitivity t

  H  ⊢ a ≤ t
  H  ⊢ t ≤ b

Rule: exceptionCompactness
H z:(exception(u; v) ≤ F fix(f)), J ⊢ C ext !((!\\x.g) Ax)

  BY exceptionCompactness #$i j x ()

  H z:(exception(u; v) ≤ F fix(f)), [j:ℕ], x:(exception(u; v) ≤ F (f^j ⊥)), J ⊢ C ext g

Rule: isinrCases
This rule proved as lemma rule_isinr_cases_true in file rules/rules_inl_inr_cases.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ C ext !((!\\x.if t is inr then ea else eb) Ax)

  BY isinrCases x t u v ()

  H  ⊢ 0 ≤ eval x = t in 0
  H  ⊢ t ∈ Base
  H x:(t ~ inr outr(t) ) ⊢ C ext ea
  H x:(∀[u,v:Base].  (if t is inr then u else v ~ v)) ⊢ C ext eb

Rule: isinlCases
This rule proved as lemma rule_isinl_cases_true in file rules/rules_inl_inr_cases.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ C ext !((!\\x.if t is inl then ea else eb) Ax)

  BY isinlCases x t u v ()

  H  ⊢ 0 ≤ eval x = t in 0
  H  ⊢ t ∈ Base
  H x:(t ~ inl outl(t)) ⊢ C ext ea
  H x:(∀[u,v:Base].  (if t is inl then u else v ~ v)) ⊢ C ext eb

Rule: freeFromAtom1Atom2
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a#x:Atom2

  BY freeFromAtom1Atom2 ()

  H  ⊢ x ∈ Atom2

Rule: pertypeElimination2
This rule proved as lemma rule_pertype_elimination2_true in file rules/rules_pertype.v
at https://github.com/vrahli/NuprlInCoq

H x:pertype(R), J ⊢ C ext e

  BY pertypeElimination2 #$n y ()

  H x:pertype(R), [y:R x x], J ⊢ C ext e
  H x:pertype(R), J ⊢ istype(R x x)

Rule: pertypeMemberEquality
This rule proved as lemma rule_pertype_member_equality_true in file rules/rules_pertype.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ t1 = t2 ∈ pertype(R)

  BY pertypeMemberEquality !parameter{i:l}

  H  ⊢ pertype(R) ∈ Type
  H  ⊢ R t1 t2
  H  ⊢ t1 ∈ Base

Rule: islambdaExceptionCases
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY islambdaExceptionCases x t u v ()

  H  ⊢ is-exception(if t is lambda then u otherwise v)
  H x:(t)↓ ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base

Rule: sqleLambda
H  ⊢ f ~ λx.(f x)

  BY sqleLambda y a ()

     x can not occur free in f
  H  ⊢ f ≤ λy.a
  H  ⊢ (f)↓

Rule: exceptionApplyCases
This rule proved as lemma rule_apply_exception_cases_true in file rules/rules_apply_exception_cases_true.v
at https://github.com/vrahli/NuprlInCoq

H
   ⊢ ↓(exception(⊥; ⊥) ≤ f)
      ∨ (f ~ λx.(f x))

      ∨ (⋂x:Base. ⋂z:(x)↓.  if x is an integer then True else f x ≤ ⊥) ext islambda(f)

  BY exceptionApplyCases a ()

     x ≠ z
     x,z can not occur free in f
  H  ⊢ exception(⊥; ⊥) ≤ f a
  H  ⊢ f ∈ Base

Rule: callbyvalueApplyCases
This rule proved as lemma rule_callbyvalue_apply_cases_true in file rules/rules_apply_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (f ~ λx.(f x)) ∨ (⋂x:Base. ⋂z:(x)↓.  if x is an integer then True else f x ≤ ⊥) ext islambda(f)

  BY callbyvalueApplyCases a ()

     x ≠ z
     x,z can not occur free in f
  H  ⊢ 0 ≤ eval f a; 0
  H  ⊢ f ∈ Base

Rule: callbyvalueIslambda
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (p)↓

  BY callbyvalueIslambda a b ()

  H  ⊢ 0 ≤ eval if p is lambda then a otherwise b; 0

Rule: sqequalExtensionalEquality
This rule proved as lemma rule_cequiv_extensional_equality_true in file rules/rules_squiggle4.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (a ~ b) = (c ~ d) ∈ Type

  BY sqequalExtensionalEquality ()

  H  ⊢ ↓a ~ b ⇐⇒ c ~ d

Rule: islambdaCases
H  ⊢ C ext !((!\\x.if t is lambda then ea otherwise eb) Ax)

  BY islambdaCases x t u v ()

  H  ⊢ 0 ≤ eval x = t in 0
  H  ⊢ t ∈ Base
  H x:(t ~ λu.(t u)) ⊢ C ext ea
  H x:(∀[u,v:Base].  (if t is lambda then u otherwise v ~ v)) ⊢ C ext eb

Rule: StrongContinuity2
This rule proved as lemma rule_strong_continuity_true2_v3_2 in file continuity/stronger_continuity_rule4_v3.v
at https://github.com/vrahli/NuprlInCoq

H

   ⊢ λn,f. ν(v.F (λx.if (x) < (0)  then ⊥  else if (x) < (n)  then f x  else (exception(v; x)))?v:x.<x, x>) ∈ ⇃({M:n:ℕ ─\000C→ (ℕn ⟶ T) ⟶ (ℕ ⋃ (ℕ × ℕ))|

∀f:ℕ ⟶ T
((∃n:ℕ. ((M n f) = (F f) ∈ ℕ))

                          ∧ (∀n:ℕ. (M n f) = (F f) ∈ ℕ supposing M n f is an integer)

                          ∧ (∀n,m:ℕ.  ((n ≤ m) ⇒ M n f is an integer ⇒ M m f is an integer)))} )

  BY StrongContinuity2 ()

  H  ⊢ F ∈ (ℕ ⟶ T) ⟶ ℕ
  H  ⊢ ↓T
  H  ⊢ T ⊆r ℕ

Rule: SquashedBarInduction
H  ⊢ ↓P 0 seq-normalize(0;t)

  BY SquashedBarInduction !parameter{i:l} B n s m x w ()

     n,s can not occur free in B
  H n:ℕ, s:(ℕn ⟶ ℕ) ⊢ B n s ∈ Type
  H s:(ℕ ⟶ ℕ) ⊢ ↓∃n:ℕ. (B n seq-normalize(n;s))
  H n:ℕ, s:(ℕn ⟶ ℕ), w:B n s ⊢ P n s
  H n:ℕ, s:(ℕn ⟶ ℕ), w:(∀m:ℕ. (P (n + 1) (λx.if x=n then m else (s x)))) ⊢ P n s

Rule: parameterizedRecEquality
H  ⊢ pRec(C1;x1.B1;c1) = pRec(C2;x2.B2;c2) ∈ Type

  BY parameterizedRecEquality x y z c ()


  H x:(C1 ⟶ Type) ⊢ B1[x/x1] = B2[x/x2] ∈ (C1 ⟶ Type)

  H x:(C1 ⟶ Type), y:(C1 ⟶ Type), z:(∀c:C1. ((x c) ⊆r (y c))) ⊢ ∀c:C1. ((B1[x/x1] c) ⊆r (B2[y/x2] c))

  H  ⊢ C1 = C2 ∈ Type
  H  ⊢ c1 = c2 ∈ C1

Rule: ispairExceptionCases
This rule proved as lemma rule_can_test_exception_cases_true in file rules/rules_cft_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY ispairExceptionCases x t u v ()

  H  ⊢ is-exception(if t is a pair then u otherwise v)
  H x:(t)↓ ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueIspair
This rule proved as lemma rule_callbyvalue_can_test_true in file rules/rules_cft_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (p)↓

  BY callbyvalueIspair a b ()

  H  ⊢ 0 ≤ eval if p is a pair then a otherwise b; 0

Rule: axiomSqequalN
This rule proved as lemma rule_cequiv_member_eq_true3 in file rules/rules_squiggle6.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ Ax = Ax ∈ (a ~n b)

  BY axiomSqequalN ()

  H  ⊢ a ~n b

Rule: token1Equality
H  ⊢ '$x'1 = '$x'1 ∈ Atom1

  BY token1Equality ()

  No Subgoals

Rule: TYPEIsType
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ istype(TYPE)

  BY TYPEIsType ()

  No Subgoals

Rule: TYPEMemberIsType
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ istype(T)

  BY TYPEMemberIsType ()

  H  ⊢ T ∈ TYPE

Rule: barInduction
H  ⊢ f [] ∈ X []

  BY barInduction T R !parameter{i:l} a s x n t ()

  H  ⊢ T ∈ Type
  H s:(T List) ⊢ (R s) ∨ (¬(R s))
  H a:(ℕ ⟶ T) ⊢ ↓∃n:ℕ. (R map(a;upto(n)))
  H s:(T List), x:R s ⊢ f s ∈ X s
  H s:(T List), x:(∀t:T. (f (s @ [t]) ∈ X (s @ [t]))) ⊢ f s ∈ X s

Rule: isintReduceAtom
H  ⊢ if z is an integer then a else b ~ b

  BY isintReduceAtom ()

  H  ⊢ z = z ∈ Atom

Rule: ispairCases

This rule proved as lemma rule_ispair_cases_true in file rules/rules_cft.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ C ext !((!\\x.if t is a pair then ea otherwise eb) Ax)

  BY ispairCases x t u v ()

  H  ⊢ 0 ≤ eval x = t in 0
  H  ⊢ t ∈ Base
  H x:(t ~ <fst(t), snd(t)>) ⊢ C ext ea
  H x:(∀[u,v:Base].  (if t is a pair then u otherwise v ~ v)) ⊢ C ext eb

Rule: isintCases
H  ⊢ C ext !((!\\x.if t is an integer then ea else eb) Ax)

  BY isintCases x t u v ()

  H  ⊢ 0 ≤ eval x = t in 0
  H  ⊢ t ∈ Base
  H x:(t ∈ ℤ) ⊢ C ext ea
  H x:(∀[u,v:Base].  (if t is an integer then u else v ~ v)) ⊢ C ext eb

Rule: isatomReduceTrue
H  ⊢ if z is an atom then a otherwise b ~ a

  BY isatomReduceTrue ()

  H  ⊢ z = z ∈ Atom

Rule: sqlenSqequaln
H  ⊢ a ≤n b

  BY sqlenSqequaln ()

  H  ⊢ a ~n b

Rule: sqle_n rule
H  ⊢ a ≤n b

  BY sqle_n ()

     Let SubGoals = CallLisp(SQLE-N)
  SubGoals

Rule: divergentSqlen
H  ⊢ a ≤n b

  BY divergentSqlen y !parameter{i:l} ()

  H y:(a)↓ ⊢ a ≤n b
  H y:is-exception(a) ⊢ a ≤n b
  H  ⊢ (a)↓ ∈ ℙ

Rule: sqleZero
H  ⊢ a ≤0 b

  BY sqleZero ()

  No Subgoals

Rule: axiomSqleNEquality
H  ⊢ Ax = Ax ∈ (a ≤n b)

  BY axiomSqleNEquality ()

  H  ⊢ a ≤n b

Rule: sqleDefinition
H  ⊢ a ≤ b

  BY sqleDefinition n

  H n:ℕ ⊢ a ≤n b

Rule: multiplyExceptionCases
This rule proved as lemma rule_arith_exception_cases_true in file rules/rules_arith_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY multiplyExceptionCases x y t u ()

  H  ⊢ is-exception(t * u)
  H x:(t ∈ ℤ), y:is-exception(u) ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ u ∈ Base

Rule: callbyvalueMultiply
This rule proved as lemma rule_callbyvalue_arith_true in file rules/rules_arith_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (a ∈ ℤ) ∧ (b ∈ ℤ) ext <Ax, Ax>

  BY callbyvalueMultiply ()

  H  ⊢ 0 ≤ eval a * b; 0
  H  ⊢ a ∈ Base
  H  ⊢ b ∈ Base

Rule: exceptionLess
H  ⊢ if (x) < (exception(u; v))  then y  else z ~ exception(u; v)

  BY exceptionLess ()

  H  ⊢ x ∈ ℤ

Rule: int_eqExceptionCases
H  ⊢ a = b ∈ T

  BY int_eqExceptionCases x y t u z w ()

  H  ⊢ is-exception(if t=u then z else w)
  H x:(t ∈ ℤ), y:(u ∈ ℤ) ⊢ a = b ∈ T
  H x:(t ∈ ℤ), y:is-exception(u) ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ u ∈ Base

Rule: callbyvalueIntEq
H  ⊢ (a ∈ ℤ) ∧ (b ∈ ℤ) ext <Ax, Ax>

  BY callbyvalueIntEq u v ()

  H  ⊢ 0 ≤ eval if a=b then u else v; 0
  H  ⊢ a ∈ Base
  H  ⊢ b ∈ Base

Rule: lessExceptionCases
This rule proved as lemma rule_less_exception_cases_true in file rules/rules_less_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY lessExceptionCases x y t u z w ()

  H  ⊢ is-exception(if (t) < (u)  then z  else w)
  H x:(t ∈ ℤ), y:(u ∈ ℤ) ⊢ a = b ∈ T
  H x:(t ∈ ℤ), y:is-exception(u) ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ u ∈ Base

Rule: callbyvalueLess
H  ⊢ (a ∈ ℤ) ∧ (b ∈ ℤ) ext <Ax, Ax>

  BY callbyvalueLess u v ()

  H  ⊢ 0 ≤ eval if (a) < (b)  then u  else v; 0
  H  ⊢ a ∈ Base
  H  ⊢ b ∈ Base

Rule: compactness
H z:(F fix(f))↓, J ⊢ C ext !((!\\x.g) Ax)

  BY compactness #$i j x ()

  H z:(F fix(f))↓, [j:ℕ], x:(F (f^j ⊥))↓, J ⊢ C ext g

Rule: divideExceptionCases
This rule proved as lemma rule_arith_exception_cases_true in file rules/rules_arith_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY divideExceptionCases x y t u ()

  H  ⊢ is-exception(t ÷ u)
  H x:(t ∈ ℤ), y:is-exception(u) ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ u ∈ Base

Rule: callbyvalueDivide
This rule proved as lemma rule_callbyvalue_arith_true in file rules/rules_arith_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (a ∈ ℤ) ∧ (b ∈ ℤ) ext <Ax, Ax>

  BY callbyvalueDivide ()

  H  ⊢ 0 ≤ eval a ÷ b; 0
  H  ⊢ a ∈ Base
  H  ⊢ b ∈ Base

Rule: Continuity
This rule proved as lemma rule_continuity_true3 in file continuity/continuity_rule_gen.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ ↓∃n:ℕ. ∀[g:ℤ ⟶ ℤ]. (F f) = (F g) ∈ ℤ supposing ∀[i:ℤ]. (f i) = (g i) ∈ ℤ supposing |i| < n

  BY Continuity ()

  H  ⊢ F ∈ (ℤ ⟶ ℤ) ⟶ ℤ
  H  ⊢ f ∈ ℤ ⟶ ℤ

Rule: strong_bar_Induction
H  ⊢ f 0 c ∈ X 0 c

  BY strong_bar_Induction T R B !parameter{i:l} a s con x m n t ()

  H  ⊢ T ∈ Type
  H n:ℕ, s:(ℕn ⟶ T), t:T ⊢ R n s t ∈ Type
  H n:ℕ, s:(ℕn ⟶ T), con:(∀x:ℕn. (R x s (s x))) ⊢ (B n s) ∨ (¬(B n s))
  H a:(ℕ ⟶ T), con:(∀n:ℕ. (R n a (a n))) ⊢ ↓∃n:ℕ. (B n a)
  H n:ℕ, s:(ℕn ⟶ T), con:(∀x:ℕn. (R x s (s x))), m:B n s ⊢ f n s ∈ X n s
  H n:ℕ, s:(ℕn ⟶ T), con:(∀x:ℕn. (R x s (s x))), x:(∀t:{t:T| R n s t}

                                                         (f (n + 1) (λm.if m=n then t else (s m)) ∈ X (n + 1)

                                                                                                    (λm.if m=n

                                                                                                        then t

                                                                                                        else (s m))))

     ⊢ f n s ∈ X n s

Rule: isintReduceTrue
This rule proved as lemma rule_isint_reduce_true_true3 in file rules/rules_isint.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ if z is an integer then a else b ~ a

  BY isintReduceTrue ()

  H  ⊢ z = z ∈ ℤ

Rule: cutEval
H J ⊢ T ext eval x = s in t

  BY cutEval #$i S x

  H J ⊢ S ext s
  H J ⊢ value-type(S)
  H x:S, J ⊢ T ext t

Rule: mlComputation
H  ⊢ t = tt

  BY mlComputation ()

     CallLisp(ML-COMPUTATION)
  No Subgoals

Rule: remainderEquality
This rule proved as lemma rule_arithop_equality_true3 in file rules/rules_arith.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (m1 rem n1) = (m2 rem n2) ∈ ℤ

  BY remainderEquality ()

  H  ⊢ m1 = m2 ∈ ℤ
  H  ⊢ n1 = n2 ∈ ℤ
  H  ⊢ n1 ≠ 0

Rule: pointwiseFunctionalityForEquality
This rule proved as lemma rule_functionaliy_for_equality_true in file rules/rules_functionality.v
at https://github.com/vrahli/NuprlInCoq

H a:A, J ⊢ t1 = t2 ∈ T

  BY pointwiseFunctionalityForEquality #$i !parameter{j:l} b z ()

  H a:A, J ⊢ T ∈ 𝕌{j}
  H a:Base, b:Base, z:(a = b ∈ A), J ⊢ t1 = t2[b/a] ∈ T

Rule: applyExceptionCases
This rule proved as lemma rule_isexc_apply_cases_true in file rules/rules_apply_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY applyExceptionCases x t u ()

  H  ⊢ is-exception(t u)
  H x:(t)↓ ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueApply
This rule proved as lemma rule_callbyvalue_apply_true in file rules/rules_apply_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (f)↓

  BY callbyvalueApply a ()

  H  ⊢ 0 ≤ eval f a; 0

Rule: sqequalElimination
H x:(p ~ q), J ⊢ C ext t

  BY sqequalElimination #$i

  H x:(p ~ q), J[Ax/x] ⊢ C[Ax/x] ext t

Rule: sqequalZero
H  ⊢ a ~0 b

  BY sqequalZero ()

  No Subgoals

Rule: sqequalnReflexivity
H  ⊢ a ~n a

  BY sqequalnReflexivity ()

  H  ⊢ n = n ∈ ℕ

Rule: sqequal_n rule
H  ⊢ a ~n b

  BY sqequal_n ()

     Let SubGoals = CallLisp(SQEQUAL-N)
  SubGoals

Rule: sqequalDefinition
H  ⊢ a ~ b

  BY sqequalDefinition n

  H n:ℕ ⊢ a ~n b

Rule: fixpointLeast
H  ⊢ F[fix(f)/z] ≤ t

  BY fixpointLeast F z f j ()

  H j:ℕ ⊢ F[f^j ⊥/z] ≤ t

Rule: sqleRule
H  ⊢ a ≤ b ext t

  BY sqle ()

     Let SubGoals t = CallLisp(SQLE)
  SubGoals

Rule: callbyvalueCallbyvalue
This rule proved as lemma rule_callbyvalue_cbv_true in file rules/rules_cft_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (a)↓

  BY callbyvalueCallbyvalue z.b ()

  H  ⊢ 0 ≤ eval eval z = a in b; 0

Rule: callbyvalueExceptionCases
This rule proved as lemma rule_cbv_exception_cases_true in file rules/rules_cbv_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY callbyvalueExceptionCases x t y.u ()

  H  ⊢ is-exception(eval y = t in u)
  H x:(t)↓ ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base

Rule: spreadExceptionCases
This rule proved as lemma rule_spread_exception_cases_true in file rules/rules_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY spreadExceptionCases x t y,z.u ()

  H  ⊢ is-exception(let y,z = t in u)
  H x:(t ∈ Top × Top) ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base

Rule: callbyvalueSpread
This rule proved as lemma rule_halt_spread_true in file rules/rules_halts_spread.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ p ∈ Top × Top

  BY callbyvalueSpread y,z.a ()

  H  ⊢ 0 ≤ eval let y,z = p in a; 0

Rule: atom2_eqExceptionCases
H  ⊢ a = b ∈ T

  BY atom2_eqExceptionCases x y t u z w ()

  H  ⊢ is-exception(if t=2 u then z else w)
  H x:(t ∈ Atom2), y:(u ∈ Atom2) ⊢ a = b ∈ T
  H x:(t ∈ Atom2), y:is-exception(u) ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ u ∈ Base

Rule: callbyvalueAtomnEq
H  ⊢ (a ∈ Atom$n) ∧ (b ∈ Atom$n) ext <Ax, Ax>

  BY callbyvalueAtomnEq u v ()

  H  ⊢ 0 ≤ eval if a=$n b then u else v; 0
  H  ⊢ a ∈ Base
  H  ⊢ b ∈ Base

Rule: dependent_set_memberFormation_alt
This rule proved as lemma rule_dependent_set_member_formation_true in file rules/rules_set.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ {x:A| B}  ext a

  BY dependent_set_memberFormation_alt a y ()

  H  ⊢ a = a ∈ A
  H  ⊢ B[a/x]
  H y:A ⊢ istype(B[y/x])

Rule: uallFunctionality
H f:(∀[x1:T]. P) @lvl, J ⊢ ∀[x2:T]. Q ext experimental{uallFunctionality}(λv.((λw.t) f))

  BY uallFunctionality #$i v w ()

  H [v:T] @lvl, w:P[v/x1] @lvl, J ⊢ Q[v/x2] ext t

Rule: sqequalIntensionalEquality
H  ⊢ (a ~ b) = (c ~ d) ∈ Type

  BY sqequalIntensionalEquality ()

  H  ⊢ a = c ∈ Base
  H  ⊢ b = d ∈ Base

Rule: dependent_set_memberFormation
This rule proved as lemma rule_dependent_set_member_formation_true in file rules/rules_set.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ {x:A| B}  ext a

  BY dependent_set_memberFormation !parameter{i:l} a y ()

  H  ⊢ a = a ∈ A
  H  ⊢ B[a/x]
  H y:A ⊢ B[y/x] = B[y/x] ∈ Type

Rule: pertypeElimination
This rule proved as lemma rule_pertype_elimination2_true in file rules/rules_pertype.v
at https://github.com/vrahli/NuprlInCoq

H x:(t1 = t2 ∈ pertype(R)), J ⊢ C ext e

  BY pertypeElimination #$n y ()

  H x:(t1 = t2 ∈ pertype(R)), [y:R t1 t2], J ⊢ C ext e
  H x:(t1 = t2 ∈ pertype(R)), J ⊢ istype(R t1 t2)

Rule: token2Equality
H  ⊢ '$x'2 = '$x'2 ∈ Atom2

  BY token2Equality ()

  No Subgoals

Rule: freeFromAtomSet
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a#x:{v:T| P}

  BY freeFromAtomSet ()

  H  ⊢ a#x:T
  H  ⊢ x ∈ {v:T| P}

Rule: freeFromAtomAxiom
H  ⊢ Ax = Ax ∈ a#x:T

  BY freeFromAtomAxiom ()

  H  ⊢ a#x:T

Rule: freeFromAtomBase
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a#x:Atom$n

  BY freeFromAtomBase ()

  H  ⊢ ¬(x = a ∈ Atom$n)

Rule: atomn_eqReduceTrueSq
H  ⊢ if a=$n b then s else t ~ u

  BY atomn_eqReduceTrueSq ()

  H  ⊢ s ~ u
  H  ⊢ a = b ∈ Atom$n

Rule: freeFromAtomAbsurdity
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
at https://github.com/vrahli/NuprlInCoq

H z:a#a:Atom$n, J ⊢ T ext any z

  BY freeFromAtomAbsurdity #$i

  No Subgoals

Rule: freeFromAtomTriviality
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a#x:T

  BY freeFromAtomTriviality ()

     !call_lisp_wargs{NO-UT-OCCURS:t}($n:n x ())
  H  ⊢ x = x ∈ T

Rule: freeFromAtomApplication
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a#f x:B[x/v]

  BY freeFromAtomApplication v:A ⟶ B

  H  ⊢ a#f:v:A ⟶ B
  H  ⊢ a#x:A

Rule: int_eqReduceFalseSq
H  ⊢ if a=b then s else t ~ u

  BY int_eqReduceFalseSq ()

  H  ⊢ t ~ u
  H  ⊢ (a = b ∈ ℤ) ⟶ Void

Rule: int_eqReduceTrueSq
H  ⊢ if a=b then s else t ~ u

  BY int_eqReduceTrueSq ()

  H  ⊢ s ~ u
  H  ⊢ a = b ∈ ℤ

Rule: lessCases
H  ⊢ C ext !((!\\x.if (t1) < (t2)  then ea  else eb) Ax)

  BY lessCases x t1 t2 u v ()

  H  ⊢ t1 ∈ ℤ
  H  ⊢ t2 ∈ ℤ
  H x:(∀[u,v:Base].  (if (t1) < (t2)  then u  else v ~ u)) ⊢ C ext ea
  H x:(∀[u,v:Base].  (if (t1) < (t2)  then u  else v ~ v)) ⊢ C ext eb

Rule: atomnEquality
H  ⊢ Atom$n = Atom$n ∈ Type

  BY atomnEquality ()

  No Subgoals

Rule: divergentSqle
This rule proved as lemma rule_convergence_true3 in file rules/rules_squiggle3.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a ≤ b

  BY divergentSqle y !parameter{i:l} ()

  H y:(a)↓ ⊢ a ≤ b
  H y:is-exception(a) ⊢ a ≤ b
  H  ⊢ (a)↓ ∈ ℙ
  H  ⊢ is-exception(a) ∈ ℙ

Rule: sqequalSqle
This rule proved as lemma rule_cequiv_approx_true3 in file rules/rules_squiggle.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a ~ b

  BY sqequalSqle ()

  H  ⊢ a ≤ b
  H  ⊢ b ≤ a

Rule: atom_eqEquality
H  ⊢ if a1=b1 then s1 else t1 fi  = if a2=b2 then s2 else t2 fi  ∈ T

  BY atom_eqEquality v

  H  ⊢ a1 = a2 ∈ Atom
  H  ⊢ b1 = b2 ∈ Atom
  H v:(a1 = b1 ∈ Atom) ⊢ s1 = s2 ∈ T
  H v:((a1 = b1 ∈ Atom) ⟶ Void) ⊢ t1 = t2 ∈ T

Rule: dependent_pairEquality_alt
This rule proved as lemma rule_pair_equality_true in file rules/rules_product.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ <a1, b1> = <a2, b2> ∈ (x:A × B)

  BY dependent_pairEquality_alt y ()

  H  ⊢ a1 = a2 ∈ A
  H  ⊢ b1 = b2 ∈ B[a1/x]
  H y:A ⊢ istype(B[y/x])

Rule: dependent_pairEquality
This rule proved as lemma rule_pair_equality_true in file rules/rules_product.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ <a1, b1> = <a2, b2> ∈ (x:A × B)

  BY dependent_pairEquality !parameter{i:l} y ()

  H  ⊢ a1 = a2 ∈ A
  H  ⊢ b1 = b2 ∈ B[a1/x]
  H y:A ⊢ B[y/x] = B[y/x] ∈ Type

Rule: functionExtensionality_alt
H  ⊢ f = g ∈ (x:A ⟶ B)

  BY functionExtensionality_alt u ()

  H u:A ⊢ (f u) = (g u) ∈ B[u/x]
  H  ⊢ istype(A)

Rule: dependentIntersection_memberEquality
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ b1 = b2 ∈ x:A ⋂ B

  BY dependentIntersection_memberEquality ()

  H  ⊢ b1 = b2 ∈ A
  H  ⊢ b1 = b2 ∈ B[b1/x]

Rule: dependentIntersectionEqElimination
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
at https://github.com/vrahli/NuprlInCoq

H z:(a = b ∈ x:A ⋂ B), J ⊢ T ext !(!((!\\u.(!\\v.t)) Ax) Ax)

  BY dependentIntersectionEqElimination #$i u v ()

  H z:(a = b ∈ x:A ⋂ B), u:(a = b ∈ A), v:(a = b ∈ B[a/x]), J ⊢ T ext t

Rule: dependentIntersectionElimination
This rule proved as lemma rule_free_from_atom_equality_true3 in file rules/rules_free_from_atom.v
at https://github.com/vrahli/NuprlInCoq

H z:x:A ⋂ B, J ⊢ T ext !(!((!\\u.(!\\v.t)) Ax) Ax)

  BY dependentIntersectionElimination #$i u v ()

  H z:x:A ⋂ B, u:(z = z ∈ A), v:(z = z ∈ B[z/x]), J ⊢ T ext t

Rule: isectIsType
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ istype(⋂a:A. B)

  BY isectIsType z ()

  H  ⊢ istype(A)
  H z:A ⊢ istype(B[z/a])

Rule: axiomSqleEquality
This rule proved as lemma rule_approx_member_eq_true3 in file rules/rules_squiggle6.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ Ax = Ax ∈ (a ≤ b)

  BY axiomSqleEquality ()

  H  ⊢ a ≤ b

Rule: minusEquality
This rule proved as lemma rule_minus_equality_true3 in file rules/rules_minus.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (-s) = (-t) ∈ ℤ

  BY minusEquality ()

  H  ⊢ s = t ∈ ℤ

Rule: equalityIsType2
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ istype(x = y ∈ T)

  BY equalityIsType2 ()

  H  ⊢ istype(T)
  H  ⊢ x ∈ Base
  H  ⊢ y ∈ T

Rule: multiplyEquality
This rule proved as lemma rule_arithop_equality_true3 in file rules/rules_arith.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (m1 * n1) = (m2 * n2) ∈ ℤ

  BY multiplyEquality ()

  H  ⊢ m1 = m2 ∈ ℤ
  H  ⊢ n1 = n2 ∈ ℤ

Rule: axiomSqEquality
This rule proved as lemma rule_cequiv_member_eq_true3 in file rules/rules_squiggle6.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ Ax = Ax ∈ (a ~ b)

  BY axiomSqEquality ()

  H  ⊢ a ~ b

Rule: callbyvalueReduce
This rule proved as lemma rule_callbyvalue_reduce_true3 in file rules_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq  ⋅

H  ⊢ eval x = a in B ~ t

  BY callbyvalueReduce ()

  H  ⊢ B[a/x] ~ t
  H  ⊢ 0 ≤ eval x = a in 0

Rule: addExceptionCases
This rule proved as lemma rule_arith_exception_cases_true in file rules/rules_arith_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY addExceptionCases x y t u ()

  H  ⊢ is-exception(t + u)
  H x:(t ∈ ℤ), y:is-exception(u) ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base
  H  ⊢ u ∈ Base

Rule: callbyvalueAdd
This rule proved as lemma rule_callbyvalue_arith_true in file rules/rules_arith_callbyvalue.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (a ∈ ℤ) ∧ (b ∈ ℤ) ext <Ax, Ax>

  BY callbyvalueAdd ()

  H  ⊢ 0 ≤ eval a + b; 0
  H  ⊢ a ∈ Base
  H  ⊢ b ∈ Base

Rule: productUniverseElim
H z:((z1:A1 × B1) = (z2:A2 × B2) ∈ Type), J ⊢ C ext e

  BY productUniverseElim #$h a x y ()

  H z:((z1:A1 × B1) = (z2:A2 × B2) ∈ Type), [x:(A1 = A2 ∈ Type)], [y:(∀a:A1. (B1[a/z1] = B2[a/z2] ∈ Type))], J

     ⊢ C ext e

Rule: unionUniverseElim
H z:((A1 + B1) = (A2 + B2) ∈ Type), J ⊢ C ext e

  BY unionUniverseElim #$h x y ()

  H z:((A1 + B1) = (A2 + B2) ∈ Type), [x:(A1 = A2 ∈ Type)], [y:(B1 = B2 ∈ Type)], J ⊢ C ext e

Rule: orLevelFunctionality
H x:(P ∨ Q ∈ 𝕌{lvl}), J ⊢ A ∨ B ∈ 𝕌{lvl} ext experimental{orLevelFunctionality}(Ax)

  BY orLevelFunctionality #$i v ()

  H v:(P ∈ 𝕌{lvl}), J ⊢ A ∈ 𝕌{lvl}
  H v:(Q ∈ 𝕌{lvl}), J ⊢ B ∈ 𝕌{lvl}

Rule: approximateComputation
H  ⊢ C ext !((!\\v.e) Ax)

  BY approximateComputation t v

     Let a () = CallLisp(LISP-COMPUTATION)
  H v:(a ≤ t) ⊢ C ext e

Rule: inlEquality_alt

This rule proved as lemma rule_inl_equality_true in file rules/rules_union.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ (inl a1) = (inl a2) ∈ (A + B)

  BY inlEquality_alt ()

  H  ⊢ a1 = a2 ∈ A
  H  ⊢ istype(B)

Rule: inrEquality_alt

This rule proved as lemma rule_inr_equality_true in file rules/rules_union.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ (inr b1 ) = (inr b2 ) ∈ (A + B)

  BY inrEquality_alt ()

  H  ⊢ b1 = b2 ∈ B
  H  ⊢ istype(A)

Rule: unionIsType
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ istype(A + B)

  BY unionIsType ()

  H  ⊢ istype(A)
  H  ⊢ istype(B)

Rule: equalityIsType3
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ istype(x = y ∈ T)

  BY equalityIsType3 ()

  H  ⊢ istype(T)
  H  ⊢ x ∈ T
  H  ⊢ y ∈ Base

Rule: equalityIsType1
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ istype(x = y ∈ T)

  BY equalityIsType1 ()

  H  ⊢ istype(T)
  H  ⊢ x ∈ T
  H  ⊢ y ∈ T

Rule: pointwiseFunctionality
This rule proved as lemma rule_functionaliy_true in file rules/rules_functionality.v
at https://github.com/vrahli/NuprlInCoq

H z:A, J ⊢ C ext t

  BY pointwiseFunctionality #$i !parameter{j:l} a b c ()

  H [a:Base], [b:Base], [c:(a = b ∈ A)], J[a/z] ⊢ C[a/z] ext t
  H a:Base, b:Base, c:(a = b ∈ A), J[a/z] ⊢ C[a/z] = C[b/z] ∈ 𝕌{j}

Rule: inrEquality

This rule proved as lemma rule_inr_equality_true in file rules/rules_union.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ (inr b1 ) = (inr b2 ) ∈ (A + B)

  BY inrEquality !parameter{i:l} ()

  H  ⊢ b1 = b2 ∈ B
  H  ⊢ A = A ∈ Type

Rule: sqequalBase

This rule proved as lemma rule_cequiv_base_true in file rules/rules_squiggle.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ a ~ b

  BY sqequalBase ()

  H  ⊢ a = b ∈ Base

Rule: spreadEquality
This rule proved as lemma rule_spread_equality_true in file rules/rules_product.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ let x1,y1 = e1 in t1 = let x2,y2 = e2 in t2 ∈ T[e1/z]

  BY spreadEquality z.T (w:A × B) u v a ()

  H  ⊢ e1 = e2 ∈ (w:A × B)
  H u:A, v:B[u/w], a:(e1 = <u, v> ∈ (w:A × B)) ⊢ t1[u,v/x1,y1] = t2[u,v/x2,y2] ∈ T[<u, v>/z]

Rule: andLevelFunctionality
H x:(P ∧ Q ∈ 𝕌{lvl}), J ⊢ A ∧ B ∈ 𝕌{lvl} ext experimental{andLevelFunctionality}(Ax)

  BY andLevelFunctionality #$i v w ()

  H v:(P ∈ 𝕌{lvl}), J ⊢ A ∈ 𝕌{lvl}
  H v:P, w:(Q ∈ 𝕌{lvl}), J ⊢ B ∈ 𝕌{lvl}
  H v:(P ∈ 𝕌{lvl}), w:A @lvl, J ⊢ P

Rule: existsLevelFunctionality

H x:(∃x1:T. P ∈ 𝕌{lvl}), J ⊢ ∃x2:T. Q ∈ 𝕌{lvl} ext experimental{existsLevelFunctionality}(Ax)

  BY existsLevelFunctionality #$i v w ()

  H v:T @lvl, w:P ∈ 𝕌{lvl}[v/x1], J ⊢ Q ∈ 𝕌{lvl}[v/x2]

Rule: existsFunctionality
H p:(∃x1:T. P) @lvl, J ⊢ ∃x2:T. Q ext let v,w = p in <v, t>

  BY existsFunctionality #$i v w ()

  H v:T @lvl, w:P[v/x1] @lvl, J ⊢ Q[v/x2] ext t
  H v:T @lvl, w:P ∈ 𝕌{lvl}[v/x1], J ⊢ Q ∈ 𝕌{lvl}[v/x2]

Rule: inlEquality

This rule proved as lemma rule_inl_equality_true in file rules/rules_union.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ (inl a1) = (inl a2) ∈ (A + B)

  BY inlEquality !parameter{i:l} ()

  H  ⊢ a1 = a2 ∈ A
  H  ⊢ B = B ∈ Type

Rule: impliesLevelFunctionality
H x:(P ⇒ Q ∈ 𝕌{lvl}), J ⊢ A ⇒ B ∈ 𝕌{lvl} ext experimental{impliesLevelFunctionality}(Ax)

  BY impliesLevelFunctionality #$i v w ()

  H v:(P ∈ 𝕌{lvl}), J ⊢ A ∈ 𝕌{lvl}
  H v:A, w:(Q ∈ 𝕌{lvl}), J ⊢ B ∈ 𝕌{lvl}
  H v:(P ∈ 𝕌{lvl}), w:A @lvl, J ⊢ P

Rule: allLevelFunctionality

H x:(∀x1:T. P ∈ 𝕌{lvl}), J ⊢ ∀x2:T. Q ∈ 𝕌{lvl} ext experimental{allLevelFunctionality}(λx.Ax)

  BY allLevelFunctionality #$i v w ()

  H v:T @lvl, w:P ∈ 𝕌{lvl}[v/x1], J ⊢ Q ∈ 𝕌{lvl}[v/x2]

Rule: allFunctionality
H f:(∀x1:T. P) @lvl, J ⊢ ∀x2:T. Q ext experimental{allFunctionality}(λv.!((!\\w.t) f v))

  BY allFunctionality #$i v w ()

  H v:T @lvl, w:P[v/x1] @lvl, J ⊢ Q[v/x2] ext t

Rule: isectEquality
This rule proved as lemma rule_isect_equality_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (⋂x1:a1. b1) = (⋂x2:a2. b2) ∈ Type

  BY isectEquality y ()

  H  ⊢ a1 = a2 ∈ Type
  H y:a1 ⊢ b1[y/x1] = b2[y/x2] ∈ Type

Rule: orFunctionality

H x:(P ∨ Q) @lvl, J ⊢ A ∨ B ext experimental{orFunctionality}(case x of inl(v) => inl a | inr(v) => inr b )

  BY orFunctionality #$i v w ()

  H v:P @lvl, J ⊢ A ext a
  H v:Q @lvl, J ⊢ B ext b
  H v:(Q ∈ 𝕌{lvl}), w:(P ∈ 𝕌{lvl}), J ⊢ A ∈ 𝕌{lvl}
  H v:(P ∈ 𝕌{lvl}), w:(Q ∈ 𝕌{lvl}), J ⊢ B ∈ 𝕌{lvl}

Rule: impliesFunctionality
H f:(P ⇒ Q) @lvl, J ⊢ A ⇒ B ext experimental{impliesFunctionality}(λa.!((!\\w.h) f g))

  BY impliesFunctionality #$i a w ()

  H a:A @lvl, J ⊢ P ext g
  H a:A @lvl, w:Q @lvl, J ⊢ B ext h
  H a:(P ∈ 𝕌{lvl}), J ⊢ A ∈ 𝕌{lvl}

Rule: equalityUniverse
This rule proved as lemma rule_equality_universe_true3 in file rules/rules_equality6.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ A1 = A2 ∈ Type

  BY equalityUniverse x1 y1 x2 y2 ()

  H  ⊢ (x1 = y1 ∈ A1) = (x2 = y2 ∈ A2) ∈ Type

Rule: isectIsTypeImplies
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ istype(A)

  BY isectIsTypeImplies (⋂a:A. B) ()

  H  ⊢ istype(⋂a:A. B)

Rule: dependent_pairFormation_alt
This rule proved as lemma rule_pair_formation_true in file rules/rules_product.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ x:A × B ext <a, b>

  BY dependent_pairFormation_alt a y ()

  H  ⊢ a = a ∈ A
  H  ⊢ B[a/x] ext b
  H y:A ⊢ istype(B[y/x])

Rule: equalityIstype
H  ⊢ istype(a = b ∈ A)

  BY equalityIstype X Y x y u z ()

  H  ⊢ istype(A)
  H  ⊢ a ∈ X
  H  ⊢ b ∈ Y
  H x:Base, y:Base, u:(x = y ∈ X), z:(x ∈ A) ⊢ x = y ∈ A
  H x:Base, y:Base, u:(x = y ∈ Y), z:(x ∈ A) ⊢ x = y ∈ A

Rule: divideEquality
This rule proved as lemma rule_arithop_equality_true3 in file rules/rules_arith.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (m1 ÷ n1) = (m2 ÷ n2) ∈ ℤ

  BY divideEquality ()

  H  ⊢ m1 = m2 ∈ ℤ
  H  ⊢ n1 = n2 ∈ ℤ
  H  ⊢ n1 ≠ 0

Rule: isect_memberFormation_alt
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ ⋂x:A. B ext b

  BY isect_memberFormation_alt z ()

  H [z:A] ⊢ B[z/x] ext b
  H  ⊢ istype(A)

Rule: lemma_by_obid
H  ⊢ C ext t

  BY lemma_by_obid !parameter{$theorem:o} ()

     Let t C = CallLisp(LE-LEMMA-O)
  No Subgoals

Rule: comment
H  ⊢ C ext (λ.T) c

  BY comment c ()

  H  ⊢ C ext T

Rule: equalityElimination
H x:(p = q ∈ A), J ⊢ C ext t

  BY equalityElimination #$i

  H x:(p = q ∈ A), J[Ax/x] ⊢ C[Ax/x] ext t

Rule: addEquality
This rule proved as lemma rule_arithop_equality_true3 in file rules/rules_arith.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (m1 + n1) = (m2 + n2) ∈ ℤ

  BY addEquality ()

  H  ⊢ m1 = m2 ∈ ℤ
  H  ⊢ n1 = n2 ∈ ℤ

Rule: hypothesis_subsumption
H x:A, J ⊢ C ext t

  BY hypothesis_subsumption #$i B ()

  H  ⊢ B ⊆r A
  H x:A, J ⊢ x ∈ B
  H x:B, J ⊢ C ext t

Rule: computeAll
H  ⊢ a ~ b

  BY computeAll ()

     CallLisp(COMPUTE-ALL)
  No Subgoals

Rule: int_eqEquality
H  ⊢ if a1=b1 then s1 else t1 = if a2=b2 then s2 else t2 ∈ T

  BY int_eqEquality v

  H  ⊢ a1 = a2 ∈ ℤ
  H  ⊢ b1 = b2 ∈ ℤ
  H v:(a1 = b1 ∈ ℤ) ⊢ s1 = s2 ∈ T
  H v:((a1 = b1 ∈ ℤ) ⟶ Void) ⊢ t1 = t2 ∈ T

Rule: intWeakElimination
H x:ℤ, J ⊢ a = b ∈ T

  BY intWeakElimination #$i z y v

  H x:ℤ, J, y:ℤ, v:y < 0, z:a = b ∈ T[y + 1/x] ⊢ a = b ∈ T[y/x]
  H x:ℤ, J ⊢ a = b ∈ T[0/x]
  H x:ℤ, J, y:ℤ, v:0 < y, z:a = b ∈ T[y - 1/x] ⊢ a = b ∈ T[y/x]

Rule: isect_memberFormation
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ ⋂x:A. B ext b

  BY isect_memberFormation !parameter{i:l} z ()

  H [z:A] ⊢ B[z/x] ext b
  H  ⊢ A = A ∈ Type

Rule: levelHypothesis
H x:A @i, J ⊢ A = A ∈ Type

  BY levelHypothesis #$h

  No Subgoals

Rule: addLevel
H x:A, J ⊢ C ext t

  BY addLevel !parameter{lvl:l} #$h ()

  H x:A @lvl, J ⊢ C ext t
  H x:A, J ⊢ A = A ∈ 𝕌{lvl}

Rule: dependent_pairFormation
This rule proved as lemma rule_pair_formation_true in file rules/rules_product.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ x:A × B ext <a, b>

  BY dependent_pairFormation !parameter{i:l} a y ()

  H  ⊢ a = a ∈ A
  H  ⊢ B[a/x] ext b
  H y:A ⊢ B[y/x] = B[y/x] ∈ Type

Rule: inlFormation

This rule proved as lemma rule_inr_formation_true3 in file rules/rules_union.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ A + B ext inl a

  BY inlFormation !parameter{i:l} ()

  H  ⊢ A ext a
  H  ⊢ B = B ∈ Type

Rule: exceptionSqequal
This rule proved as lemma rule_exception_sqequal_true in file rules/rules_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ C ext c

  BY exceptionSqequal x u v t ()

  H  ⊢ is-exception(t)
  H [u:Base], [v:Base], [x:(t ~ exception(u; v))] ⊢ C ext c
  H u:Base, v:Base ⊢ t ∈ Base

Rule: inrFormation

This rule proved as lemma rule_inr_formation_true3 in file rules/rules_union.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ A + B ext inr b

  BY inrFormation !parameter{i:l} ()

  H  ⊢ B ext b
  H  ⊢ A = A ∈ Type

Rule: decideExceptionCases
This rule proved as lemma rule_decide_exception_cases_true in file rules/rules_decide_exception.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a = b ∈ T

  BY decideExceptionCases x t y.u z.v ()

  H  ⊢ is-exception(case t of inl(y) => u | inr(z) => v)
  H x:(t ∈ Top + Top) ⊢ a = b ∈ T
  H x:is-exception(t) ⊢ a = b ∈ T
  H  ⊢ t ∈ Base

Rule: baseApply
This rule proved as lemma rule_apply_in_base_true3 in file rules/rules_squiggle6.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ f a ∈ Base

  BY baseApply ()

  H  ⊢ f ∈ Base
  H  ⊢ a ∈ Base

Rule: sqleReflexivity
This rule proved as lemma rule_approx_refl_true3 in file rules/rules_squiggle.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a ≤ a

  BY sqleReflexivity ()

  No Subgoals

Rule: unionElimination
This rule proved as lemma rule_union_elimination_true in file rules/rules_union.v
at https://github.com/vrahli/NuprlInCoq

H z:(A + B), J ⊢ T ext case z of inl(x) => left | inr(y) => right

  BY unionElimination #$i x y

  H z:(A + B), x:A, J[inl x/z] ⊢ T[inl x/z] ext left
  H z:(A + B), y:B, J[inr y /z] ⊢ T[inr y /z] ext right

Rule: unionEquality

This rule proved as lemma rule_union_equality_true in file rules/rules_union.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ (a1 + b1) = (a2 + b2) ∈ Type

  BY unionEquality ()

  H  ⊢ a1 = a2 ∈ Type
  H  ⊢ b1 = b2 ∈ Type

Rule: callbyvalueDecide
This rule proved as lemma rule_halt_decide_true3 in file rules/rules_halts_decide.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ d ∈ Top + Top

  BY callbyvalueDecide y.a z.b ()

  H  ⊢ 0 ≤ eval case d of inl(y) => a | inr(z) => b; 0
  H  ⊢ d ∈ Base

Rule: voidEquality

This rule proved as lemma rule_void_equality_true3 in file rules/rules_void.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ Void = Void ∈ Type

  BY voidEquality ()

  No Subgoals

Rule: isect_memberEquality
This rule proved as lemma rule_isect_member_equality_true in file rules/rules_isect2.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ b1 = b2 ∈ (⋂x:A. B)

  BY isect_memberEquality !parameter{i:l} z ()

  H z:A ⊢ b1 = b2 ∈ B[z/x]
  H  ⊢ A = A ∈ Type

Rule: functionEquality
This rule proved as lemma rule_function_equality_true in file rules/rules_function.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (x1:a1 ⟶ b1) = (x2:a2 ⟶ b2) ∈ Type

  BY functionEquality y

  H  ⊢ a1 = a2 ∈ Type
  H y:a1 ⊢ b1[y/x1] = b2[y/x2] ∈ Type

Rule: setEquality

This rule proved as lemma rule_set_equality_true in file rules/rules_set.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ {x1:A1| B1}  = {x2:A2| B2}  ∈ Type

  BY setEquality x

  H  ⊢ A1 = A2 ∈ Type
  H x:A1 ⊢ B1[x/x1] = B2[x/x2] ∈ Type

Rule: dependent_set_memberEquality
H  ⊢ a1 = a2 ∈ {x:A| B}

  BY dependent_set_memberEquality !parameter{i:l} y ()

  H  ⊢ a1 = a2 ∈ A
  H  ⊢ B[a1/x]
  H y:A ⊢ B[y/x] = B[y/x] ∈ Type

Rule: lambdaEquality
This rule proved as lemma rule_lambda_equality_true in file rules/rules_function.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (λx1.b1) = (λx2.b2) ∈ (x:A ⟶ B)

  BY lambdaEquality !parameter{i:l} z ()

  H z:A ⊢ b1[z/x1] = b2[z/x2] ∈ B[z/x]
  H  ⊢ A = A ∈ Type

Rule: lambdaFormation
This rule proved as lemma rule_lambda_formation_true in file rules/rules_function.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ x:A ⟶ B ext λz.b

  BY lambdaFormation !parameter{i:l} z ()

  H z:A ⊢ B[z/x] ext b
  H  ⊢ A = A ∈ Type

Rule: promote_hyp
H x:A, J, y:B, K ⊢ C ext t

  BY promote_hyp #$i #$j ()

  H y:B, x:A, J, K ⊢ C ext t

Rule: applyLambdaEquality
  This rule combines the rules Error :applyEquality and Error :lambdaEquality
but generates one fewer subgoal because the subgoal H  ⊢ A = A  generated
by `lambdaEquality` is not needed because the subgoal H  ⊢ a1 = a2
generated by `applyEquality` also implies that A is a type.
⋅

H  ⊢ ((λx1.b1) a1) = ((λx2.b2) a2) ∈ B[a1/x]

  BY applyLambdaEquality z (x:A ⟶ B) ()

  H z:A ⊢ b1[z/x1] = b2[z/x2] ∈ B[z/x]
  H  ⊢ a1 = a2 ∈ A

Rule: hyp_replacement

This rule proved as lemma rule_hyp_replacement_true3 in file rules_equality7.v at https://github.com/vrahli/NuprlInCoq

This is the rule that states that types are extensional.
If A is provably equal to B in ⌜Type⌝ then we can replace hypothesis x:A
by hypothesis x:B.
In particular,  from x:B we have ⌜x ∈ B⌝ and therefore ⌜x ∈ A⌝.⋅

H x:A, J ⊢ C ext t

  BY hyp_replacement #$j B !parameter{i:l} ()

  H x:B, J ⊢ C ext t
  H x:A, J ⊢ A = B ∈ Type

Rule: equalityIsType4
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ istype(x = y ∈ T)

  BY equalityIsType4 ()

  H  ⊢ istype(T)
  H  ⊢ x ∈ Base
  H  ⊢ y ∈ Base

Rule: inlFormation_alt

This rule proved as lemma rule_inr_formation_true3 in file rules/rules_union.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ A + B ext inl a

  BY inlFormation_alt ()

  H  ⊢ A ext a
  H  ⊢ istype(B)

Rule: inrFormation_alt

This rule proved as lemma rule_inr_formation_true3 in file rules/rules_union.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ A + B ext inr b

  BY inrFormation_alt ()

  H  ⊢ B ext b
  H  ⊢ istype(A)

Rule: voidElimination
This rule proved as lemma rule_void_elimination_true in file rules/rules_void.v
at https://github.com/vrahli/NuprlInCoq

H z:Void, J ⊢ T ext any z

  BY voidElimination #$i

  No Subgoals

Rule: isect_memberEquality_alt
This rule proved as lemma rule_isect_member_equality_true in file rules/rules_isect2.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ b1 = b2 ∈ (⋂x:A. B)

  BY isect_memberEquality_alt z ()

  H z:A ⊢ b1 = b2 ∈ B[z/x]
  H  ⊢ istype(A)

Rule: independent_pairEquality
H  ⊢ <a1, b1> = <a2, b2> ∈ (A × B)

  BY independent_pairEquality ()

  H  ⊢ a1 = a2 ∈ A
  H  ⊢ b1 = b2 ∈ B

Rule: functionExtensionality
H  ⊢ f = g ∈ (x:A ⟶ B)

  BY functionExtensionality !parameter{i:l} u ()

  H u:A ⊢ (f u) = (g u) ∈ B[u/x]
  H  ⊢ A = A ∈ Type

Rule: functionIsType
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ istype(a:A ⟶ B)

  BY functionIsType z ()

  H  ⊢ istype(A)
  H z:A ⊢ istype(B[z/a])

Rule: functionIsTypeImplies
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ istype(A)

  BY functionIsTypeImplies (a:A ⟶ B) ()

  H  ⊢ istype(a:A ⟶ B)

Rule: axiomEquality
This rule proved as lemma rule_axiom_equality_true3 in file rules/rules_equality4.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ Ax = Ax ∈ (a1 = a2 ∈ A)

  BY axiomEquality ()

  H  ⊢ a1 = a2 ∈ A

Rule: independent_isectElimination
H f:(⋂:A. B), J ⊢ T ext !((!\\y.t) f)

  BY independent_isectElimination #$i y ()

  H f:(⋂:A. B), J ⊢ A
  H f:(⋂:A. B), J, y:B ⊢ T ext t

Rule: intEquality

This rule proved as lemma rule_int_equality_true3 in file rules/rules_number.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ ℤ = ℤ ∈ Type

  BY intEquality ()

  No Subgoals

Rule: productEquality
This rule proved as lemma rule_product_equality_true in file rules/rules_product.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (x1:a1 × b1) = (x2:a2 × b2) ∈ Type

  BY productEquality y

  H  ⊢ a1 = a2 ∈ Type
  H y:a1 ⊢ b1[y/x1] = b2[y/x2] ∈ Type

Rule: productIsType
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ istype(a:A × B)

  BY productIsType z ()

  H  ⊢ istype(A)
  H z:A ⊢ istype(B[z/a])

Rule: baseClosed

This rule proved as lemma rule_base_closed_true in file rules/rules_base.v at https://github.com/vrahli/NuprlInCoq

   ⊢ t = t ∈ Base

  BY baseClosed ()

  No Subgoals

Rule: imageMemberEquality
This rule proved as lemma rule_image_member_equality_true in file rules/rules_image.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (f a1) = (f a2) ∈ Image(A,f)

  BY imageMemberEquality ()

  H  ⊢ a1 = a2 ∈ A
  H  ⊢ f = f ∈ Base

Rule: dependent_set_memberEquality_alt
H  ⊢ a1 = a2 ∈ {x:A| B}

  BY dependent_set_memberEquality_alt y ()

  H  ⊢ a1 = a2 ∈ A
  H  ⊢ B[a1/x]
  H y:A ⊢ istype(B[y/x])

Rule: tokenEquality
H  ⊢ "$tok" = "$tok" ∈ Atom

  BY tokenEquality ()

  No Subgoals

Rule: atomEquality
H  ⊢ Atom = Atom ∈ Type

  BY atomEquality ()

  No Subgoals

Rule: inhabitedIsType
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ istype(T)

  BY inhabitedIsType t ()

  H  ⊢ t ∈ T

Rule: equalitySymmetry
This rule proved as lemma rule_equality_symmetry_true3 in file rules/rules_equality5.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ s = t ∈ T

  BY equalitySymmetry ()

  H  ⊢ t = s ∈ T

Rule: equalityTransitivity
This rule proved as lemma rule_equality_transitivity_true3 in file rules/rules_equality5.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ s = t ∈ T

  BY equalityTransitivity x

  H  ⊢ s = x ∈ T
  H  ⊢ x = t ∈ T

Rule: imageElimination
This rule proved as lemma rule_image_elimination_true in file rules/rules_image.v
at https://github.com/vrahli/NuprlInCoq

H x:Image(A,f), J ⊢ C ext t

  BY imageElimination #$i w ()

  H [w:A], J[f w/x] ⊢ C[f w/x] ext t

Rule: independent_pairFormation
H  ⊢ A × B ext <a, b>

  BY independent_pairFormation ()

  H  ⊢ A ext a
  H  ⊢ B ext b

Rule: independent_functionElimination
H f:F, J ⊢ T ext !((!\\y.t) f a)

  BY independent_functionElimination #$i y

     Let A ⟶ B = F
  H f:F, J ⊢ A ext a
  H f:F, J, y:B ⊢ T ext t

Rule: setIsType
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ istype({a:A| B} )

  BY setIsType z ()

  H  ⊢ istype(A)
  H z:A ⊢ istype(B[z/a])

Rule: because_Cache
H  ⊢ C

  BY because_Cache ()

  No Subgoals

Rule: applyEquality
This rule proved as lemma rule_apply_equality_true in file rules/rules_function.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (f1 a1) = (f2 a2) ∈ B[a1/x]

  BY applyEquality x:A ⟶ B

  H  ⊢ f1 = f2 ∈ (x:A ⟶ B)
  H  ⊢ a1 = a2 ∈ A

Rule: universeEquality
This rule proved as lemma rule_universe_equality_true3 in file rules/rules_uni.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ 𝕌{j} = 𝕌{j} ∈ Type

  BY universeEquality ()

     CallLisp(LE-UNIVERSE-EQUALITY)
  No Subgoals

Rule: closedConclusion
This rule proved as lemma rule_closed_conclusion_true3 in file rules/rules_struct2.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ C ext t

  BY closedConclusion ()

     ⊢ C ext t

Rule: hypothesisEquality
This rule proved as lemma rule_hypothesis_equality_true in file rules/rules_struct.v
at https://github.com/vrahli/NuprlInCoq

H x:T, J ⊢ x = x ∈ T

  BY hypothesisEquality #$i

  No Subgoals

Rule: lambdaEquality_alt
This rule proved as lemma rule_lambda_equality_true in file rules/rules_function.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ (λx1.b1) = (λx2.b2) ∈ (x:A ⟶ B)

  BY lambdaEquality_alt z ()

  H z:A ⊢ b1[z/x1] = b2[z/x2] ∈ B[z/x]
  H  ⊢ istype(A)

Rule: sqequalRule
H  ⊢ a ~ b ext t

  BY sqequal ()

     Let SubGoals t = CallLisp(SQEQ)
  SubGoals

Rule: dependent_functionElimination
H f:(x:A ⟶ B), J ⊢ T ext !((!\y,v.t) f a Ax)

  BY dependent_functionElimination #$i a y v

  H f:(x:A ⟶ B), J ⊢ a = a ∈ A
  H f:(x:A ⟶ B), J, y:B[a/x], v:(y = (f a) ∈ B[a/x]) ⊢ T ext t

Rule: cumulativity

This rule proved as lemma rule_cumulativity_true3 in file rules/rules_uni.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ t = t ∈ Type

  BY cumulativity !parameter{j:l} ()

     CallLisp(LE_CUMULATIVITY)
  H  ⊢ t = t ∈ 𝕌{j}

Rule: instantiate
!subst(J; subs) ⊢ !subst(C; subs) ext !subst(t; subs)

  BY instantiate J C subs ()

  J  ⊢ C ext t

Rule: hypothesis

This rule proved as lemma rule_hypothesis_true3 in file rules/rules_struct.v at https://github.com/vrahli/NuprlInCoq

H x:A, J ⊢ A ext x

  BY hypothesis #$i

  No Subgoals

Rule: natural_numberEquality
This rule proved as lemma rule_natural_number_equality_true3 in file rules/rules_number.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ $i = $i ∈ ℤ

  BY natural_numberEquality ()

  No Subgoals

Rule: isectElimination
H f:(⋂x:A. B), J ⊢ T ext !((!\y,v.t) f Ax)

  BY isectElimination #$i a y v ()

  H f:(⋂x:A. B), J ⊢ a = a ∈ A
  H f:(⋂x:A. B), J, y:B[a/x], v:(y = f ∈ B[a/x]) ⊢ T ext t

Rule: extract_by_obid
H  ⊢ t = t ∈ C

  BY extract_by_obid !parameter{$theorem:o} ()

     Let t C = CallLisp(LE-LEMMA-O)
  No Subgoals

Rule: introduction

This rule proved as lemma rule_introduction_true3 in file rules/rules_struct.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ T ext t

  BY introduction t

  H  ⊢ t = t ∈ T

Rule: universeIsType
This rule proved as lemma rule_isect_member_formation_true3 in file rules/rules_isect.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ istype(T)

  BY universeIsType !parameter{i:l} ()

  H  ⊢ T = T ∈ Type

Rule: productElimination
This rule proved as lemma rule_product_elimination_true in file rules/rules_product.v
at https://github.com/vrahli/NuprlInCoq

H z:(x:A × B), J ⊢ T ext let u,v = z in t

  BY productElimination #$i u v

  H z:(x:A × B), u:A, v:B[u/x], J[<u, v>/z] ⊢ T[<u, v>/z] ext t

Rule: rename
H y:a, J ⊢ C ext !((!\\x.T) y)

  BY rename #$i x ()

  H x:a, J[x/y] ⊢ C[x/y] ext T

Rule: thin

This rule proved as lemma rule_thin_true in file rules/rules_struct.v at https://github.com/vrahli/NuprlInCoq

H x:A, J ⊢ T ext t

  BY thin #$i

  H J ⊢ T ext t

Rule: setElimination

This rule proved as lemma rule_set_elimination_true in file rules/rules_set.v at https://github.com/vrahli/NuprlInCoq

H u:{x:A| B} , J ⊢ T ext !((!\\y.t) u)

  BY setElimination #$i y v

  H u:{x:A| B} , y:A, [v:B[y/x]], J[y/u] ⊢ T[y/u] ext t

Rule: sqequalHypSubstitution
This rule proved as lemma rule_cequiv_subst_hyp_true in file rules/rules_squiggle2.v
at https://github.com/vrahli/NuprlInCoq

H j:T[a/x] @lvl, J ⊢ C ext t

  BY sqequalHypSubstitution #$i (a ~ b) x.T ()

  H j:T[a/x] @lvl, J ⊢ a ~ b
  H j:T[b/x] @lvl, J ⊢ C ext t

Rule: cut

This rule proved as lemma rule_cut_true3 in file rules/rules_struct.v at https://github.com/vrahli/NuprlInCoq

H J ⊢ T ext (λx.t) s

  BY cut #$i S x

  H J ⊢ S ext s
  H x:S, J ⊢ T ext t

Rule: lambdaFormation_alt
This rule proved as lemma rule_lambda_formation_true in file rules/rules_function.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ x:A ⟶ B ext λz.b

  BY lambdaFormation_alt z ()

  H z:A ⊢ B[z/x] ext b
  H  ⊢ istype(A)

Rule: sqequalReflexivity

This rule proved as lemma rule_cequiv_refl_true in file rules/rules_squiggle.v at https://github.com/vrahli/NuprlInCoq

H  ⊢ a ~ a

  BY sqequalReflexivity ()

  No Subgoals

Rule: computationStep
H  ⊢ a ~ b

  BY computationStep ()

     CallLisp(COMPUTATION-STEP)
  No Subgoals

Rule: sqequalTransitivity
This rule proved as lemma rule_cequiv_trans_true3 in file rules/rules_squiggle8.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ a ~ b

  BY sqequalTransitivity c

  H  ⊢ a ~ c
  H  ⊢ c ~ b

Rule: sqequalSubstitution
This rule proved as lemma rule_cequiv_subst_concl_true3 in file rules/rules_squiggle2.v
at https://github.com/vrahli/NuprlInCoq

H  ⊢ T[a/x] ext t

  BY sqequalSubstitution (a ~ b) x.T ()

  H  ⊢ a ~ b
  H  ⊢ T[b/x] ext t

Home Index