Proof of Nuprl Lemma : Veldman-Coquand

Step * 4 2 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)))

⊢ 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
{ (Assert (λ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)) BY
         (SplitAndConcl
          THEN Try ((RepUR ``nary-rel seq-append`` 0 THEN Auto))

          THEN Try ((Unfold `wfd-tree` 0 THEN MemCD THEN Reduce 0 THEN Auto THEN Try (Fold `wfd-tree` 0) THEN 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)))

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

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

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 \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: (Assert (\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)) BY (SplitAndConcl THEN Try ((RepUR ``nary-rel seq-append`` 0 THEN Auto)) THEN Try ((Unfold `wfd-tree` 0 THEN MemCD THEN Reduce 0 THEN Auto THEN Try (Fold `wfd-tree` 0) THEN Auto)))) Home Index