Theory "DeepSyntax"

Parents int_arith

Signature

Type	Arity
deep_form	0
Constant	Type
Aset	:bool -> deep_form -> int -> bool
Bset	:bool -> deep_form -> int -> bool
Conjn	:deep_form -> deep_form -> deep_form
Disjn	:deep_form -> deep_form -> deep_form
LTx	:int -> deep_form
Negn	:deep_form -> deep_form
UnrelatedBool	:bool -> deep_form
alldivide	:deep_form -> int -> bool
deep_form_CASE	:deep_form -> (deep_form -> deep_form -> α) -> (deep_form -> deep_form -> α) -> (deep_form -> α) -> (bool -> α) -> (int -> α) -> (int -> α) -> (int -> α) -> (int -> int -> α) -> α
deep_form_size	:deep_form -> num
eval_form	:deep_form -> int -> bool
neginf	:deep_form -> deep_form
posinf	:deep_form -> deep_form
xDivided	:int -> int -> deep_form
xEQ	:int -> deep_form
xLT	:int -> deep_form

Definitions

deep_form_TY_DEF

|- ∃rep.
     TYPE_DEFINITION
       (λa0'.
          ∀'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) ∧ 'deep_form' a0 ∧ '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) ∧ 'deep_form' a0 ∧ 'deep_form' a1) ∨
               (∃a.
                  (a0' =
                   (λa.
                      ind_type$CONSTR (SUC (SUC 0)) (ARB,ARB,ARB)
                        (ind_type$FCONS a (λn. ind_type$BOTTOM))) a) ∧
                  '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) ⇒
               'deep_form' a0') ⇒
            'deep_form' a0') rep

deep_form_case_def

|- (∀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

|- (∀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

|- (∀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

|- (∀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

|- (∀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

alldivide_def

|- (∀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

Aset_def

|- (∀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

|- (∀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) = ∅

Theorems

datatype_deep_form

|- DATATYPE (deep_form Conjn Disjn Negn UnrelatedBool xLT LTx xEQ xDivided)

deep_form_11

|- (∀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_distinct

|- (∀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_case_cong

|- ∀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_nchotomy

|- ∀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

deep_form_Axiom

|- ∀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_induction

|- ∀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

neginf_ok

|- ∀f. ∃y. ∀x. x < y ⇒ (eval_form f x ⇔ eval_form (neginf f) x)

posinf_ok

|- ∀f. ∃y. ∀x. y < x ⇒ (eval_form f x ⇔ eval_form (posinf f) x)

add_d_neginf

|- ∀f x y d.
     alldivide f d ⇒
     (eval_form (neginf f) x ⇔ eval_form (neginf f) (x + y * d))

add_d_posinf

|- ∀f x y d.
     alldivide f d ⇒
     (eval_form (posinf f) x ⇔ eval_form (posinf f) (x + y * d))

neginf_disj1_implies_exoriginal

|- ∀f d i.
     alldivide f d ⇒
     0 < i ∧ i ≤ d ∧ eval_form (neginf f) i ⇒
     ∃x. eval_form f x

posinf_disj1_implies_exoriginal

|- ∀f d i.
     alldivide f d ⇒
     0 < i ∧ i ≤ d ∧ eval_form (posinf f) i ⇒
     ∃x. eval_form f x

neginf_exoriginal_implies_rhs

|- ∀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)

posinf_exoriginal_implies_rhs

|- ∀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)

neginf_exoriginal_eq_rhs

|- ∀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))

posinf_exoriginal_eq_rhs

|- ∀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))

in_bset

|- ((∃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)

in_aset

|- ((∃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)