Step
*
4
2
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))
∧ (λ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))
⊢ 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:(InstHyp [⌜tree-tensor(n;p x;Wsup(ff;q))⌝;⌜tree-tensor(n;Wsup(ff;p);q x)⌝;⌜λm,s. (((A[x] m s)
∨ (([[R]] m s) ∧ ([[S]] m s)))
∨ (B m s))⌝;⌜λm,s. ((A m s)
∨ (B[x] m s)
∨ (([[R]] m s)
∧ ([[S]] m s)))\000C⌝;
⌜λs.(R seq-append(1;n;seq-single(x);s))⌝;⌜λs.(S seq-append(1;n;seq-single(x);s))⌝] 4⋅
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)))
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)))
2
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 m s) ∨ (B[x] m s) ∨ (([[R]] m s) ∧ ([[S]] m s)))) m s)
∨ ([[λs.(S seq-append(1;n;seq-single(x);s))]] m s));tree-tensor(n;Wsup(ff;p);q x))
3
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)))
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))
\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:(InstHyp [\mkleeneopen{}tree-tensor(n;p x;Wsup(ff;q))\mkleeneclose{};\mkleeneopen{}tree-tensor(n;Wsup(ff;p);q x)\mkleeneclose{};\mkleeneopen{}\mlambda{}m,s. (((A[x] m s)
\mvee{} (([[R]] m
s)
\mwedge{} ([[S]] m
s)))
\mvee{} (B m s))\mkleeneclose{};
\mkleeneopen{}\mlambda{}m,s. ((A m s) \mvee{} (B[x] m s) \mvee{} (([[R]] m s) \mwedge{} ([[S]] m s)))\mkleeneclose{};
\mkleeneopen{}\mlambda{}s.(R seq-append(1;n;seq-single(x);s))\mkleeneclose{};\mkleeneopen{}\mlambda{}s.(S seq-append(1;n;seq-single(x);s))\mkleeneclose{}] 4\mcdot{}
THENA Auto
)\mcdot{}
Home
Index