- UNIQUE_tupled_primitive_def
-
|- UNIQUE_tupled =
WFREC (@R. WF R)
(λUNIQUE_tupled a'.
case a' of
(v,n,conn,INL i,INL j) => I (v n ⇔ conn (v i) (v j))
| (v,n,conn,INL i,INR b) => I (v n ⇔ conn (v i) b)
| (v,n,conn,INR a,INL j') => I (v n ⇔ conn a (v j'))
| (v,n,conn,INR a,INR b') => I (v n ⇔ conn a b'))
- UNIQUE_curried_def
-
|- ∀x x1 x2. defCNF$UNIQUE x x1 x2 ⇔ UNIQUE_tupled (x,x1,x2)
- 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
- OK_tupled_primitive_def
-
|- OK_tupled =
WFREC (@R. WF R)
(λOK_tupled a'.
case a' of
(n,conn,INL i,INL j) => I (i < n ∧ j < n)
| (n,conn,INL i,INR b) => I (i < n)
| (n,conn,INR a,INL j') => I (j' < n)
| (n,conn,INR a,INR b') => I T)
- OK_curried_def
-
|- ∀x x1. defCNF$OK x x1 ⇔ OK_tupled (x,x1)
- OKDEF_def
-
|- (∀n. defCNF$OKDEF n [] ⇔ T) ∧
∀n x xs. defCNF$OKDEF n (x::xs) ⇔ defCNF$OK n x ∧ defCNF$OKDEF (SUC n) xs
- 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))
- 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)
- 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
- OKDEF_SNOC
-
|- ∀n x l.
defCNF$OKDEF n (SNOC x l) ⇔ defCNF$OKDEF n l ∧ defCNF$OK (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)
- FINAL_DEF
-
|- ∀v n x. (v n ⇔ x) ⇔ (v n ⇔ x) ∧ defCNF$DEF v (SUC n) []