Theory "defCNF"

Parents rich_list

Signature

Constant	Type
DEF	:(num -> bool) -> num -> ((bool -> bool -> bool) # (num + bool) # (num + bool)) list -> bool
OK	:num -> (bool -> bool -> bool) # (num + bool) # (num + bool) -> bool
OKDEF	:num -> ((bool -> bool -> bool) # (num + bool) # (num + bool)) list -> bool
UNIQUE	:(num -> bool) -> num -> (bool -> bool -> bool) # (num + bool) # (num + bool) -> bool

Definitions

OKDEF_def

⊢ (∀n. defCNF$OKDEF n [] ⇔ T) ∧
  ∀n x xs. defCNF$OKDEF n (x::xs) ⇔ defCNF$OK n x ∧ defCNF$OKDEF (SUC n) xs

DEF_def

⊢ (∀v n. defCNF$DEF v n [] ⇔ T) ∧
  ∀v n x xs.
      defCNF$DEF v n (x::xs) ⇔ defCNF$UNIQUE v n x ∧ defCNF$DEF v (SUC n) xs

Theorems

UNIQUE_ind

⊢ ∀P.
      (∀v n conn i j. P v n (conn,INL i,INL j)) ∧
      (∀v n conn i b. P v n (conn,INL i,INR b)) ∧
      (∀v n conn a j. P v n (conn,INR a,INL j)) ∧
      (∀v n conn a b. P v n (conn,INR a,INR b)) ⇒
      ∀v v1 v2 v3 v4. P v v1 (v2,v3,v4)

UNIQUE_def

⊢ (defCNF$UNIQUE v n (conn,INL i,INL j) ⇔ (v n ⇔ conn (v i) (v j))) ∧
  (defCNF$UNIQUE v n (conn,INL i,INR b) ⇔ (v n ⇔ conn (v i) b)) ∧
  (defCNF$UNIQUE v n (conn,INR a,INL j) ⇔ (v n ⇔ conn a (v j))) ∧
  (defCNF$UNIQUE v n (conn,INR a,INR b) ⇔ (v n ⇔ conn a b))

OKDEF_SNOC

⊢ ∀n x l.
      defCNF$OKDEF n (SNOC x l) ⇔
      defCNF$OKDEF n l ∧ defCNF$OK (n + LENGTH l) x

OK_ind

⊢ ∀P.
      (∀n conn i j. P n (conn,INL i,INL j)) ∧
      (∀n conn i b. P n (conn,INL i,INR b)) ∧
      (∀n conn a j. P n (conn,INR a,INL j)) ∧
      (∀n conn a b. P n (conn,INR a,INR b)) ⇒
      ∀v v1 v2 v3. P v (v1,v2,v3)

OK_def

⊢ (defCNF$OK n (conn,INL i,INL j) ⇔ i < n ∧ j < n) ∧
  (defCNF$OK n (conn,INL i,INR b) ⇔ i < n) ∧
  (defCNF$OK n (conn,INR a,INL j) ⇔ j < n) ∧
  (defCNF$OK n (conn,INR a,INR b) ⇔ T)

FINAL_DEF

⊢ ∀v n x. (v n ⇔ x) ⇔ (v n ⇔ x) ∧ defCNF$DEF v (SUC n) []

DEF_SNOC

⊢ ∀n x l v.
      defCNF$DEF v n (SNOC x l) ⇔
      defCNF$DEF v n l ∧ defCNF$UNIQUE v (n + LENGTH l) x

CONSISTENCY

⊢ ∀n l. defCNF$OKDEF n l ⇒ ∃v. defCNF$DEF v n l

BIGSTEP

⊢ ∀P Q R. (∀v. P v ⇒ (Q ⇔ R v)) ⇒ ((∃v. P v) ∧ Q ⇔ ∃v. P v ∧ R v)