Structure DeepSyntaxTheory


Source File Identifier index Theory binding index

signature DeepSyntaxTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val Aset_def : thm
    val Bset_def : thm
    val alldivide_def : thm
    val deep_form_TY_DEF : thm
    val deep_form_case_def : thm
    val deep_form_size_def : thm
    val eval_form_def : thm
    val neginf_def : thm
    val posinf_def : thm
  
  (*  Theorems  *)
    val add_d_neginf : thm
    val add_d_posinf : thm
    val datatype_deep_form : thm
    val deep_form_11 : thm
    val deep_form_Axiom : thm
    val deep_form_case_cong : thm
    val deep_form_case_eq : thm
    val deep_form_distinct : thm
    val deep_form_induction : thm
    val deep_form_nchotomy : thm
    val in_aset : thm
    val in_bset : thm
    val neginf_disj1_implies_exoriginal : thm
    val neginf_exoriginal_eq_rhs : thm
    val neginf_exoriginal_implies_rhs : thm
    val neginf_ok : thm
    val posinf_disj1_implies_exoriginal : thm
    val posinf_exoriginal_eq_rhs : thm
    val posinf_exoriginal_implies_rhs : thm
    val posinf_ok : thm
  
  val DeepSyntax_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [int_arith] Parent theory of "DeepSyntax"
   
   [Aset_def]  Definition
      
      ⊢ (∀pos f1 f2. Aset pos (Conjn f1 f2) = Aset pos f1 ∪ Aset pos f2) ∧
        (∀pos f1 f2. Aset pos (Disjn f1 f2) = Aset pos f1 ∪ Aset pos f2) ∧
        (∀pos f. Aset pos (Negn f) = Aset (¬pos) f) ∧
        (∀pos b. Aset pos (UnrelatedBool b) = ∅) ∧
        (∀pos i. Aset pos (xLT i) = if pos then {i} else ∅) ∧
        (∀pos i. Aset pos (LTx i) = if pos then ∅ else {i + 1}) ∧
        (∀pos i. Aset pos (xEQ i) = if pos then {i + 1} else {i}) ∧
        ∀pos i1 i2. Aset pos (xDivided i1 i2) = ∅
   
   [Bset_def]  Definition
      
      ⊢ (∀pos f1 f2. Bset pos (Conjn f1 f2) = Bset pos f1 ∪ Bset pos f2) ∧
        (∀pos f1 f2. Bset pos (Disjn f1 f2) = Bset pos f1 ∪ Bset pos f2) ∧
        (∀pos f. Bset pos (Negn f) = Bset (¬pos) f) ∧
        (∀pos b. Bset pos (UnrelatedBool b) = ∅) ∧
        (∀pos i. Bset pos (xLT i) = if pos then ∅ else {i + -1}) ∧
        (∀pos i. Bset pos (LTx i) = if pos then {i} else ∅) ∧
        (∀pos i. Bset pos (xEQ i) = if pos then {i + -1} else {i}) ∧
        ∀pos i1 i2. Bset pos (xDivided i1 i2) = ∅
   
   [alldivide_def]  Definition
      
      ⊢ (∀f1 f2 d.
             alldivide (Conjn f1 f2) d ⇔ alldivide f1 d ∧ alldivide f2 d) ∧
        (∀f1 f2 d.
             alldivide (Disjn f1 f2) d ⇔ alldivide f1 d ∧ alldivide f2 d) ∧
        (∀f d. alldivide (Negn f) d ⇔ alldivide f d) ∧
        (∀b d. alldivide (UnrelatedBool b) d ⇔ T) ∧
        (∀i d. alldivide (xLT i) d ⇔ T) ∧ (∀i d. alldivide (LTx i) d ⇔ T) ∧
        (∀i d. alldivide (xEQ i) d ⇔ T) ∧
        ∀i1 i2 d. alldivide (xDivided i1 i2) d ⇔ i1 int_divides d
   
   [deep_form_TY_DEF]  Definition
      
      ⊢ ∃rep.
            TYPE_DEFINITION
              (λa0'.
                   ∀ $var$('deep_form').
                       (∀a0'.
                            (∃a0 a1.
                                 (a0' =
                                  (λa0 a1.
                                       ind_type$CONSTR 0 (ARB,ARB,ARB)
                                         (ind_type$FCONS a0
                                            (ind_type$FCONS a1
                                               (λn. ind_type$BOTTOM)))) a0
                                    a1) ∧ $var$('deep_form') a0 ∧
                                 $var$('deep_form') a1) ∨
                            (∃a0 a1.
                                 (a0' =
                                  (λa0 a1.
                                       ind_type$CONSTR (SUC 0)
                                         (ARB,ARB,ARB)
                                         (ind_type$FCONS a0
                                            (ind_type$FCONS a1
                                               (λn. ind_type$BOTTOM)))) a0
                                    a1) ∧ $var$('deep_form') a0 ∧
                                 $var$('deep_form') a1) ∨
                            (∃a.
                                 (a0' =
                                  (λa.
                                       ind_type$CONSTR (SUC (SUC 0))
                                         (ARB,ARB,ARB)
                                         (ind_type$FCONS a
                                            (λn. ind_type$BOTTOM))) a) ∧
                                 $var$('deep_form') a) ∨
                            (∃a.
                                 a0' =
                                 (λa.
                                      ind_type$CONSTR (SUC (SUC (SUC 0)))
                                        (a,ARB,ARB) (λn. ind_type$BOTTOM))
                                   a) ∨
                            (∃a.
                                 a0' =
                                 (λa.
                                      ind_type$CONSTR
                                        (SUC (SUC (SUC (SUC 0))))
                                        (ARB,a,ARB) (λn. ind_type$BOTTOM))
                                   a) ∨
                            (∃a.
                                 a0' =
                                 (λa.
                                      ind_type$CONSTR
                                        (SUC (SUC (SUC (SUC (SUC 0)))))
                                        (ARB,a,ARB) (λn. ind_type$BOTTOM))
                                   a) ∨
                            (∃a.
                                 a0' =
                                 (λa.
                                      ind_type$CONSTR
                                        (SUC
                                           (SUC (SUC (SUC (SUC (SUC 0))))))
                                        (ARB,a,ARB) (λn. ind_type$BOTTOM))
                                   a) ∨
                            (∃a0 a1.
                                 a0' =
                                 (λa0 a1.
                                      ind_type$CONSTR
                                        (SUC
                                           (SUC
                                              (SUC
                                                 (SUC (SUC (SUC (SUC 0)))))))
                                        (ARB,a0,a1) (λn. ind_type$BOTTOM))
                                   a0 a1) ⇒
                            $var$('deep_form') a0') ⇒
                       $var$('deep_form') a0') rep
   
   [deep_form_case_def]  Definition
      
      ⊢ (∀a0 a1 f f1 f2 f3 f4 f5 f6 f7.
             deep_form_CASE (Conjn a0 a1) f f1 f2 f3 f4 f5 f6 f7 = f a0 a1) ∧
        (∀a0 a1 f f1 f2 f3 f4 f5 f6 f7.
             deep_form_CASE (Disjn a0 a1) f f1 f2 f3 f4 f5 f6 f7 = f1 a0 a1) ∧
        (∀a f f1 f2 f3 f4 f5 f6 f7.
             deep_form_CASE (Negn a) f f1 f2 f3 f4 f5 f6 f7 = f2 a) ∧
        (∀a f f1 f2 f3 f4 f5 f6 f7.
             deep_form_CASE (UnrelatedBool a) f f1 f2 f3 f4 f5 f6 f7 = f3 a) ∧
        (∀a f f1 f2 f3 f4 f5 f6 f7.
             deep_form_CASE (xLT a) f f1 f2 f3 f4 f5 f6 f7 = f4 a) ∧
        (∀a f f1 f2 f3 f4 f5 f6 f7.
             deep_form_CASE (LTx a) f f1 f2 f3 f4 f5 f6 f7 = f5 a) ∧
        (∀a f f1 f2 f3 f4 f5 f6 f7.
             deep_form_CASE (xEQ a) f f1 f2 f3 f4 f5 f6 f7 = f6 a) ∧
        ∀a0 a1 f f1 f2 f3 f4 f5 f6 f7.
            deep_form_CASE (xDivided a0 a1) f f1 f2 f3 f4 f5 f6 f7 =
            f7 a0 a1
   
   [deep_form_size_def]  Definition
      
      ⊢ (∀a0 a1.
             deep_form_size (Conjn a0 a1) =
             1 + (deep_form_size a0 + deep_form_size a1)) ∧
        (∀a0 a1.
             deep_form_size (Disjn a0 a1) =
             1 + (deep_form_size a0 + deep_form_size a1)) ∧
        (∀a. deep_form_size (Negn a) = 1 + deep_form_size a) ∧
        (∀a. deep_form_size (UnrelatedBool a) = 1 + bool_size a) ∧
        (∀a. deep_form_size (xLT a) = 1) ∧
        (∀a. deep_form_size (LTx a) = 1) ∧
        (∀a. deep_form_size (xEQ a) = 1) ∧
        ∀a0 a1. deep_form_size (xDivided a0 a1) = 1
   
   [eval_form_def]  Definition
      
      ⊢ (∀f1 f2 x.
             eval_form (Conjn f1 f2) x ⇔ eval_form f1 x ∧ eval_form f2 x) ∧
        (∀f1 f2 x.
             eval_form (Disjn f1 f2) x ⇔ eval_form f1 x ∨ eval_form f2 x) ∧
        (∀f x. eval_form (Negn f) x ⇔ ¬eval_form f x) ∧
        (∀b x. eval_form (UnrelatedBool b) x ⇔ b) ∧
        (∀i x. eval_form (xLT i) x ⇔ x < i) ∧
        (∀i x. eval_form (LTx i) x ⇔ i < x) ∧
        (∀i x. eval_form (xEQ i) x ⇔ (x = i)) ∧
        ∀i1 i2 x. eval_form (xDivided i1 i2) x ⇔ i1 int_divides x + i2
   
   [neginf_def]  Definition
      
      ⊢ (∀f1 f2. neginf (Conjn f1 f2) = Conjn (neginf f1) (neginf f2)) ∧
        (∀f1 f2. neginf (Disjn f1 f2) = Disjn (neginf f1) (neginf f2)) ∧
        (∀f. neginf (Negn f) = Negn (neginf f)) ∧
        (∀b. neginf (UnrelatedBool b) = UnrelatedBool b) ∧
        (∀i. neginf (xLT i) = UnrelatedBool T) ∧
        (∀i. neginf (LTx i) = UnrelatedBool F) ∧
        (∀i. neginf (xEQ i) = UnrelatedBool F) ∧
        ∀i1 i2. neginf (xDivided i1 i2) = xDivided i1 i2
   
   [posinf_def]  Definition
      
      ⊢ (∀f1 f2. posinf (Conjn f1 f2) = Conjn (posinf f1) (posinf f2)) ∧
        (∀f1 f2. posinf (Disjn f1 f2) = Disjn (posinf f1) (posinf f2)) ∧
        (∀f. posinf (Negn f) = Negn (posinf f)) ∧
        (∀b. posinf (UnrelatedBool b) = UnrelatedBool b) ∧
        (∀i. posinf (xLT i) = UnrelatedBool F) ∧
        (∀i. posinf (LTx i) = UnrelatedBool T) ∧
        (∀i. posinf (xEQ i) = UnrelatedBool F) ∧
        ∀i1 i2. posinf (xDivided i1 i2) = xDivided i1 i2
   
   [add_d_neginf]  Theorem
      
      ⊢ ∀f x y d.
            alldivide f d ⇒
            (eval_form (neginf f) x ⇔ eval_form (neginf f) (x + y * d))
   
   [add_d_posinf]  Theorem
      
      ⊢ ∀f x y d.
            alldivide f d ⇒
            (eval_form (posinf f) x ⇔ eval_form (posinf f) (x + y * d))
   
   [datatype_deep_form]  Theorem
      
      ⊢ DATATYPE
          (deep_form Conjn Disjn Negn UnrelatedBool xLT LTx xEQ xDivided)
   
   [deep_form_11]  Theorem
      
      ⊢ (∀a0 a1 a0' a1'.
             (Conjn a0 a1 = Conjn a0' a1') ⇔ (a0 = a0') ∧ (a1 = a1')) ∧
        (∀a0 a1 a0' a1'.
             (Disjn a0 a1 = Disjn a0' a1') ⇔ (a0 = a0') ∧ (a1 = a1')) ∧
        (∀a a'. (Negn a = Negn a') ⇔ (a = a')) ∧
        (∀a a'. (UnrelatedBool a = UnrelatedBool a') ⇔ (a ⇔ a')) ∧
        (∀a a'. (xLT a = xLT a') ⇔ (a = a')) ∧
        (∀a a'. (LTx a = LTx a') ⇔ (a = a')) ∧
        (∀a a'. (xEQ a = xEQ a') ⇔ (a = a')) ∧
        ∀a0 a1 a0' a1'.
            (xDivided a0 a1 = xDivided a0' a1') ⇔ (a0 = a0') ∧ (a1 = a1')
   
   [deep_form_Axiom]  Theorem
      
      ⊢ ∀f0 f1 f2 f3 f4 f5 f6 f7.
            ∃fn.
                (∀a0 a1. fn (Conjn a0 a1) = f0 a0 a1 (fn a0) (fn a1)) ∧
                (∀a0 a1. fn (Disjn a0 a1) = f1 a0 a1 (fn a0) (fn a1)) ∧
                (∀a. fn (Negn a) = f2 a (fn a)) ∧
                (∀a. fn (UnrelatedBool a) = f3 a) ∧
                (∀a. fn (xLT a) = f4 a) ∧ (∀a. fn (LTx a) = f5 a) ∧
                (∀a. fn (xEQ a) = f6 a) ∧
                ∀a0 a1. fn (xDivided a0 a1) = f7 a0 a1
   
   [deep_form_case_cong]  Theorem
      
      ⊢ ∀M M' f f1 f2 f3 f4 f5 f6 f7.
            (M = M') ∧
            (∀a0 a1. (M' = Conjn a0 a1) ⇒ (f a0 a1 = f' a0 a1)) ∧
            (∀a0 a1. (M' = Disjn a0 a1) ⇒ (f1 a0 a1 = f1' a0 a1)) ∧
            (∀a. (M' = Negn a) ⇒ (f2 a = f2' a)) ∧
            (∀a. (M' = UnrelatedBool a) ⇒ (f3 a = f3' a)) ∧
            (∀a. (M' = xLT a) ⇒ (f4 a = f4' a)) ∧
            (∀a. (M' = LTx a) ⇒ (f5 a = f5' a)) ∧
            (∀a. (M' = xEQ a) ⇒ (f6 a = f6' a)) ∧
            (∀a0 a1. (M' = xDivided a0 a1) ⇒ (f7 a0 a1 = f7' a0 a1)) ⇒
            (deep_form_CASE M f f1 f2 f3 f4 f5 f6 f7 =
             deep_form_CASE M' f' f1' f2' f3' f4' f5' f6' f7')
   
   [deep_form_case_eq]  Theorem
      
      ⊢ (deep_form_CASE x f f1 f2 f3 f4 f5 f6 f7 = v) ⇔
        (∃d d0. (x = Conjn d d0) ∧ (f d d0 = v)) ∨
        (∃d d0. (x = Disjn d d0) ∧ (f1 d d0 = v)) ∨
        (∃d. (x = Negn d) ∧ (f2 d = v)) ∨
        (∃b. (x = UnrelatedBool b) ∧ (f3 b = v)) ∨
        (∃i. (x = xLT i) ∧ (f4 i = v)) ∨ (∃i. (x = LTx i) ∧ (f5 i = v)) ∨
        (∃i. (x = xEQ i) ∧ (f6 i = v)) ∨
        ∃i i0. (x = xDivided i i0) ∧ (f7 i i0 = v)
   
   [deep_form_distinct]  Theorem
      
      ⊢ (∀a1' a1 a0' a0. Conjn a0 a1 ≠ Disjn a0' a1') ∧
        (∀a1 a0 a. Conjn a0 a1 ≠ Negn a) ∧
        (∀a1 a0 a. Conjn a0 a1 ≠ UnrelatedBool a) ∧
        (∀a1 a0 a. Conjn a0 a1 ≠ xLT a) ∧ (∀a1 a0 a. Conjn a0 a1 ≠ LTx a) ∧
        (∀a1 a0 a. Conjn a0 a1 ≠ xEQ a) ∧
        (∀a1' a1 a0' a0. Conjn a0 a1 ≠ xDivided a0' a1') ∧
        (∀a1 a0 a. Disjn a0 a1 ≠ Negn a) ∧
        (∀a1 a0 a. Disjn a0 a1 ≠ UnrelatedBool a) ∧
        (∀a1 a0 a. Disjn a0 a1 ≠ xLT a) ∧ (∀a1 a0 a. Disjn a0 a1 ≠ LTx a) ∧
        (∀a1 a0 a. Disjn a0 a1 ≠ xEQ a) ∧
        (∀a1' a1 a0' a0. Disjn a0 a1 ≠ xDivided a0' a1') ∧
        (∀a' a. Negn a ≠ UnrelatedBool a') ∧ (∀a' a. Negn a ≠ xLT a') ∧
        (∀a' a. Negn a ≠ LTx a') ∧ (∀a' a. Negn a ≠ xEQ a') ∧
        (∀a1 a0 a. Negn a ≠ xDivided a0 a1) ∧
        (∀a' a. UnrelatedBool a ≠ xLT a') ∧
        (∀a' a. UnrelatedBool a ≠ LTx a') ∧
        (∀a' a. UnrelatedBool a ≠ xEQ a') ∧
        (∀a1 a0 a. UnrelatedBool a ≠ xDivided a0 a1) ∧
        (∀a' a. xLT a ≠ LTx a') ∧ (∀a' a. xLT a ≠ xEQ a') ∧
        (∀a1 a0 a. xLT a ≠ xDivided a0 a1) ∧ (∀a' a. LTx a ≠ xEQ a') ∧
        (∀a1 a0 a. LTx a ≠ xDivided a0 a1) ∧
        ∀a1 a0 a. xEQ a ≠ xDivided a0 a1
   
   [deep_form_induction]  Theorem
      
      ⊢ ∀P.
            (∀d d0. P d ∧ P d0 ⇒ P (Conjn d d0)) ∧
            (∀d d0. P d ∧ P d0 ⇒ P (Disjn d d0)) ∧ (∀d. P d ⇒ P (Negn d)) ∧
            (∀b. P (UnrelatedBool b)) ∧ (∀i. P (xLT i)) ∧ (∀i. P (LTx i)) ∧
            (∀i. P (xEQ i)) ∧ (∀i i0. P (xDivided i i0)) ⇒
            ∀d. P d
   
   [deep_form_nchotomy]  Theorem
      
      ⊢ ∀dd.
            (∃d d0. dd = Conjn d d0) ∨ (∃d d0. dd = Disjn d d0) ∨
            (∃d. dd = Negn d) ∨ (∃b. dd = UnrelatedBool b) ∨
            (∃i. dd = xLT i) ∨ (∃i. dd = LTx i) ∨ (∃i. dd = xEQ i) ∨
            ∃i i0. dd = xDivided i i0
   
   [in_aset]  Theorem
      
      ⊢ ((∃a. a ∈ Aset pos (Conjn f1 f2) ∧ P a) ⇔
         (∃a. a ∈ Aset pos f1 ∧ P a) ∨ ∃a. a ∈ Aset pos f2 ∧ P a) ∧
        ((∃a. a ∈ Aset pos (Disjn f1 f2) ∧ P a) ⇔
         (∃a. a ∈ Aset pos f1 ∧ P a) ∨ ∃a. a ∈ Aset pos f2 ∧ P a) ∧
        ((∃a. a ∈ Aset T (Negn f) ∧ P a) ⇔ ∃a. a ∈ Aset F f ∧ P a) ∧
        ((∃a. a ∈ Aset F (Negn f) ∧ P a) ⇔ ∃a. a ∈ Aset T f ∧ P a) ∧
        ((∃a. a ∈ Aset pos (UnrelatedBool a0) ∧ P a) ⇔ F) ∧
        ((∃a. a ∈ Aset T (xLT i) ∧ P a) ⇔ P i) ∧
        ((∃a. a ∈ Aset F (xLT i) ∧ P a) ⇔ F) ∧
        ((∃a. a ∈ Aset T (LTx i) ∧ P a) ⇔ F) ∧
        ((∃a. a ∈ Aset F (LTx i) ∧ P a) ⇔ P (i + 1)) ∧
        ((∃a. a ∈ Aset T (xEQ i) ∧ P a) ⇔ P (i + 1)) ∧
        ((∃a. a ∈ Aset F (xEQ i) ∧ P a) ⇔ P i) ∧
        ((∃a. a ∈ Aset pos (xDivided i1 i2) ∧ P a) ⇔ F)
   
   [in_bset]  Theorem
      
      ⊢ ((∃b. b ∈ Bset pos (Conjn f1 f2) ∧ P b) ⇔
         (∃b. b ∈ Bset pos f1 ∧ P b) ∨ ∃b. b ∈ Bset pos f2 ∧ P b) ∧
        ((∃b. b ∈ Bset pos (Disjn f1 f2) ∧ P b) ⇔
         (∃b. b ∈ Bset pos f1 ∧ P b) ∨ ∃b. b ∈ Bset pos f2 ∧ P b) ∧
        ((∃b. b ∈ Bset T (Negn f) ∧ P b) ⇔ ∃b. b ∈ Bset F f ∧ P b) ∧
        ((∃b. b ∈ Bset F (Negn f) ∧ P b) ⇔ ∃b. b ∈ Bset T f ∧ P b) ∧
        ((∃b. b ∈ Bset pos (UnrelatedBool b0) ∧ P b) ⇔ F) ∧
        ((∃b. b ∈ Bset T (xLT i) ∧ P b) ⇔ F) ∧
        ((∃b. b ∈ Bset F (xLT i) ∧ P b) ⇔ P (i + -1)) ∧
        ((∃b. b ∈ Bset T (LTx i) ∧ P b) ⇔ P i) ∧
        ((∃b. b ∈ Bset F (LTx i) ∧ P b) ⇔ F) ∧
        ((∃b. b ∈ Bset T (xEQ i) ∧ P b) ⇔ P (i + -1)) ∧
        ((∃b. b ∈ Bset F (xEQ i) ∧ P b) ⇔ P i) ∧
        ((∃b. b ∈ Bset pos (xDivided i1 i2) ∧ P b) ⇔ F)
   
   [neginf_disj1_implies_exoriginal]  Theorem
      
      ⊢ ∀f d i.
            alldivide f d ⇒
            0 < i ∧ i ≤ d ∧ eval_form (neginf f) i ⇒
            ∃x. eval_form f x
   
   [neginf_exoriginal_eq_rhs]  Theorem
      
      ⊢ ∀f d.
            alldivide f d ∧ 0 < d ⇒
            ((∃x. eval_form f x) ⇔
             (∃i. K (0 < i ∧ i ≤ d) i ∧ eval_form (neginf f) i) ∨
             ∃b j.
                 (b ∈ Bset T f ∧ K (0 < j ∧ j ≤ d) j) ∧ eval_form f (b + j))
   
   [neginf_exoriginal_implies_rhs]  Theorem
      
      ⊢ ∀f d x.
            alldivide f d ∧ 0 < d ⇒
            eval_form f x ⇒
            (∃i. 0 < i ∧ i ≤ d ∧ eval_form (neginf f) i) ∨
            ∃j b. 0 < j ∧ j ≤ d ∧ b ∈ Bset T f ∧ eval_form f (b + j)
   
   [neginf_ok]  Theorem
      
      ⊢ ∀f. ∃y. ∀x. x < y ⇒ (eval_form f x ⇔ eval_form (neginf f) x)
   
   [posinf_disj1_implies_exoriginal]  Theorem
      
      ⊢ ∀f d i.
            alldivide f d ⇒
            0 < i ∧ i ≤ d ∧ eval_form (posinf f) i ⇒
            ∃x. eval_form f x
   
   [posinf_exoriginal_eq_rhs]  Theorem
      
      ⊢ ∀f d.
            alldivide f d ∧ 0 < d ⇒
            ((∃x. eval_form f x) ⇔
             (∃i. K (0 < i ∧ i ≤ d) i ∧ eval_form (posinf f) i) ∨
             ∃b j.
                 (b ∈ Aset T f ∧ K (0 < j ∧ j ≤ d) j) ∧
                 eval_form f (b + -1 * j))
   
   [posinf_exoriginal_implies_rhs]  Theorem
      
      ⊢ ∀f d x.
            alldivide f d ∧ 0 < d ⇒
            eval_form f x ⇒
            (∃i. 0 < i ∧ i ≤ d ∧ eval_form (posinf f) i) ∨
            ∃j b. 0 < j ∧ j ≤ d ∧ b ∈ Aset T f ∧ eval_form f (b + -j)
   
   [posinf_ok]  Theorem
      
      ⊢ ∀f. ∃y. ∀x. y < x ⇒ (eval_form f x ⇔ eval_form (posinf f) x)
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-13