Proof of Nuprl Lemma : Veldman-Coquand

Step * 4 2 1 1 1 1 1 1 of Lemma Veldman-Coquand

1. X : Type
2. n : ℤ
3. [%1] : 0 < n
4. ∀p,q:wfd-tree(X).
     ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:n - 1-aryRel(X)].
       (tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s));p)
       ⇒ tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s));q)
       ⇒

 tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(n - 1;p;q)))

5. p : X ⟶ wfd-tree(X)
6. ∀b:X. ∀q:wfd-tree(X).
     ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:n-aryRel(X)].
       (tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s));p b)
       ⇒ tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s));q)
       ⇒ tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(n;p b;q)))
7. q : X ⟶ wfd-tree(X)
8. ∀b:X
     ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:n-aryRel(X)].
       (tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s));Wsup(ff;p))
       ⇒ tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s));q b)
       ⇒

 tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(n;Wsup(ff;p);q b)))

9. [A] : n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ
10. [B] : n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ
11. [R] : n-aryRel(X)
12. [S] : n-aryRel(X)
13. ∀x:X. tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s))[x];p x)
14. ∀x:X. tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s))[x];q x)
15. x : X
16. λs.(S seq-append(1;n;seq-single(x);s)) ∈ n - 1-aryRel(X)
17. λs.(R seq-append(1;n;seq-single(x);s)) ∈ n - 1-aryRel(X)
18. Wsup(ff;p) ∈ wfd-tree(X)
19. Wsup(ff;q) ∈ wfd-tree(X)
20. tree-secures(X;λm,s. ((((λm,s. ((A[x] m s) ∨ ([[R]]_x m s))) m s) ∨ (B m s))

                        ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(n;p x;Wsup(ff;q)))

21. tree-secures(X;λm,s. (((A m s) ∨ ((λm,s. ((B[x] m s) ∨ ([[S]]_x m s))) m s))

                        ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(n;Wsup(ff;p);q x))

⊢ tree-secures(X;λm,s. (((λm,s. (((A[x] m s) ∨ (([[R]] m s) ∧ ([[S]] m s))) ∨ (B m s))) m s)

                      ∨ ([[λs.(R seq-append(1;n;seq-single(x);s))]] m s));tree-tensor(n;p x;Wsup(ff;q)))

BY
{ TACTIC:(TreeSecuresFunctionality THENA Auto) }

1
1. X : Type
2. n : ℤ
3. [%1] : 0 < n
4. ∀p,q:wfd-tree(X).
     ∀[A,B:n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ]. ∀[R,S:n - 1-aryRel(X)].
       (tree-secures(X;λm,s. ((A m s) ∨ ([[R]] m s));p)
       ⇒ tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s));q)
       ⇒

 tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(n - 1;p;q)))

 tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(n;Wsup(ff;p);q b)))

                        ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(n;p x;Wsup(ff;q)))

21. tree-secures(X;λm,s. (((A m s) ∨ ((λm,s. ((B[x] m s) ∨ ([[S]]_x m s))) m s))

                        ∨ (([[R]] m s) ∧ ([[S]] m s)));tree-tensor(n;Wsup(ff;p);q x))

⊢ ∀n1:ℕ. ∀s:ℕn1 ⟶ X.

    (((λm,s. ((((λm,s. ((A[x] m s) ∨ ([[R]]_x m s))) m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)))) n1 s)

    ⇒ ((λm,s. (((λm,s. (((A[x] m s) ∨ (([[R]] m s) ∧ ([[S]] m s))) ∨ (B m s))) m s)
              ∨ ([[λs.(R seq-append(1;n;seq-single(x);s))]] m s)))
        n1
        s))

Latex:

Latex:
1. X : Type 2. n : \mBbbZ{} 3. [\%1] : 0 < n 4. \mforall{}p,q:wfd-tree(X). \mforall{}[A,B:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} X) {}\mrightarrow{} \mBbbP{}]. \mforall{}[R,S:n - 1-aryRel(X)]. (tree-secures(X;\mlambda{}m,s. ((A m s) \mvee{} ([[R]] m s));p) {}\mRightarrow{} tree-secures(X;\mlambda{}m,s. ((B m s) \mvee{} ([[S]] m s));q) {}\mRightarrow{} tree-secures(X;\mlambda{}m,s. (((A m s) \mvee{} (B m s)) \mvee{} (([[R]] m s) \mwedge{} ([[S]] m s)));tree-tensor(n - 1;p;q))) 5. p : X {}\mrightarrow{} wfd-tree(X) 6. \mforall{}b:X. \mforall{}q:wfd-tree(X). \mforall{}[A,B:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} X) {}\mrightarrow{} \mBbbP{}]. \mforall{}[R,S:n-aryRel(X)]. (tree-secures(X;\mlambda{}m,s. ((A m s) \mvee{} ([[R]] m s));p b) {}\mRightarrow{} tree-secures(X;\mlambda{}m,s. ((B m s) \mvee{} ([[S]] m s));q) {}\mRightarrow{} tree-secures(X;\mlambda{}m,s. (((A m s) \mvee{} (B m s)) \mvee{} (([[R]] m s) \mwedge{} ([[S]] m s)));tree-tensor(n;p b;q))) 7. q : X {}\mrightarrow{} wfd-tree(X) 8. \mforall{}b:X \mforall{}[A,B:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} X) {}\mrightarrow{} \mBbbP{}]. \mforall{}[R,S:n-aryRel(X)]. (tree-secures(X;\mlambda{}m,s. ((A m s) \mvee{} ([[R]] m s));Wsup(ff;p)) {}\mRightarrow{} tree-secures(X;\mlambda{}m,s. ((B m s) \mvee{} ([[S]] m s));q b) {}\mRightarrow{} tree-secures(X;\mlambda{}m,s. (((A m s) \mvee{} (B m s)) \mvee{} (([[R]] m s) \mwedge{} ([[S]] m s)));tree-tensor(n;Wsup(ff;p);q b))) 9. [A] : n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} X) {}\mrightarrow{} \mBbbP{} 10. [B] : n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} X) {}\mrightarrow{} \mBbbP{} 11. [R] : n-aryRel(X) 12. [S] : n-aryRel(X) 13. \mforall{}x:X. tree-secures(X;\mlambda{}m,s. ((A m s) \mvee{} ([[R]] m s))[x];p x) 14. \mforall{}x:X. tree-secures(X;\mlambda{}m,s. ((B m s) \mvee{} ([[S]] m s))[x];q x) 15. x : X 16. \mlambda{}s.(S seq-append(1;n;seq-single(x);s)) \mmember{} n - 1-aryRel(X) 17. \mlambda{}s.(R seq-append(1;n;seq-single(x);s)) \mmember{} n - 1-aryRel(X) 18. Wsup(ff;p) \mmember{} wfd-tree(X) 19. Wsup(ff;q) \mmember{} wfd-tree(X) 20. tree-secures(X;\mlambda{}m,s. ((((\mlambda{}m,s. ((A[x] m s) \mvee{} ([[R]]\_x m s))) m s) \mvee{} (B m s)) \mvee{} (([[R]] m s) \mwedge{} ([[S]] m s)));tree-tensor(n;p x;Wsup(ff;q))) 21. tree-secures(X;\mlambda{}m,s. (((A m s) \mvee{} ((\mlambda{}m,s. ((B[x] m s) \mvee{} ([[S]]\_x m s))) m s)) \mvee{} (([[R]] m s) \mwedge{} ([[S]] m s)));tree-tensor(n;Wsup(ff;p);q x)) \mvdash{} tree-secures(X;\mlambda{}m,s. (((\mlambda{}m,s. (((A[x] m s) \mvee{} (([[R]] m s) \mwedge{} ([[S]] m s))) \mvee{} (B m s))) m s) \mvee{} ([[\mlambda{}s.(R seq-append(1;n;seq-single(x);s))]] m s));tree-tensor(n;p x;Wsup(ff;\000Cq))) By Latex: TACTIC:(TreeSecuresFunctionality THENA Auto) Home Index