Proof of Nuprl Lemma : Veldman-Coquand

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

BY
{ (Assert 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))) BY

         (BackThruSomeHyp
          THEN Reduce 0
          THEN Auto
          THEN Try ((RecUnfold `tree-secures` 0 THEN RepUR ``Wsup`` 0 THEN Trivial))

          THEN Using [`A',⌜λm,s. ((A m s) ∨ ([[R]] m s))[x]⌝] (BLemma `tree-secures_functionality`)⋅

          THEN Reduce 0
          THEN Auto
          THEN RepUR ``predicate-or-shift predicate-shift`` (-1)
          THEN RepUR ``predicate-or-shift predicate-shift`` 0
          THEN SplitOrHyps
          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)))

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

⊢ 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 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)) \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 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))) BY (BackThruSomeHyp THEN Reduce 0 THEN Auto THEN Try ((RecUnfold `tree-secures` 0 THEN RepUR ``Wsup`` 0 THEN Trivial)) THEN Using [`A',\mkleeneopen{}\mlambda{}m,s. ((A m s) \mvee{} ([[R]] m s))[x]\mkleeneclose{}] (BLemma `tree-secures\_functionality`)\mcdot{} THEN Reduce 0 THEN Auto THEN RepUR ``predicate-or-shift predicate-shift`` (-1) THEN RepUR ``predicate-or-shift predicate-shift`` 0 THEN SplitOrHyps THEN Auto)) Home Index