Proof of Nuprl Lemma : Veldman-Coquand

Step * 4 2 1 1 1 1 1 3 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))
∧ (λs.(R seq-append(1;n;seq-single(x);s)) ∈ n - 1-aryRel(X))
∧ (Wsup(ff;p) ∈ wfd-tree(X))
∧ (Wsup(ff;q) ∈ wfd-tree(X))
17. 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)))

18. 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))

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

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

∨ (([[λs.(R seq-append(1;n;seq-single(x);s))]] m s)

                          ∧ ([[λs.(S seq-append(1;n;seq-single(x);s))]] m s)));tree-tensor(n

- 1;tree-tensor(n;p x;Wsup(ff;q));tree-tensor(n;Wsup(ff;p);q x)))

⊢ tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)))[x];tree-tensor(n - 1;tree-tensor(n;p x;<ff, q\000C>);tree-tensor(n;<ff, p>;q x)))

BY
{ TACTIC:(Fold `Wsup` 0 THEN (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)))

18. 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))

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

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

∨ (([[λs.(R seq-append(1;n;seq-single(x);s))]] m s)

                          ∧ ([[λs.(S seq-append(1;n;seq-single(x);s))]] m s)));tree-tensor(n

- 1;tree-tensor(n;p x;Wsup(ff;q));tree-tensor(n;Wsup(ff;p);q x)))
⊢ ∀n1:ℕ. ∀s:ℕn1 ⟶ X.
(((λm,s. ((((λm,s. (((A[x] m s) ∨ (([[R]] m s) ∧ ([[S]] m s))) ∨ (B m s))) m s)
∨ ((λm,s. ((A m s) ∨ (B[x] m s) ∨ (([[R]] m s) ∧ ([[S]] m s)))) m s))

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

      n1
      s)
    ⇒ (λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)))[x] 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)) \mwedge{} (\mlambda{}s.(R seq-append(1;n;seq-single(x);s)) \mmember{} n - 1-aryRel(X)) \mwedge{} (Wsup(ff;p) \mmember{} wfd-tree(X)) \mwedge{} (Wsup(ff;q) \mmember{} wfd-tree(X)) 17. 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))) 18. 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)) 19. 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{}m,s. ((A m s) \mvee{} (B[x] m s) \mvee{} (([[R]] m s) \mwedge{} ([[S]] m s)))) m s)) \mvee{} (([[\mlambda{}s.(R seq-append(1;n;seq-single(x);s))]] m s) \mwedge{} ([[\mlambda{}s.(S seq-append(1;n;seq-single(x);s))]] m s)));tree-tensor(n - 1;tree-tensor(n;p x;Wsup(ff;q));tree-tensor(n;Wsup(ff;p);q x))) \mvdash{} tree-secures(X;\mlambda{}m,s. (((A m s) \mvee{} (B m s)) \mvee{} (([[R]] m s) \mwedge{} ([[S]] m s)))[x];tree-tensor(n - 1;tree-tensor(n;p x;<ff, q>);tree-tensor(n;<ff, p>q x))) By Latex: TACTIC:(Fold `Wsup` 0 THEN (TreeSecuresFunctionality THENA Auto)) Home Index