Step
*
1
1
2
of Lemma
Veldman-Coquand
1. X : Type
2. q : wfd-tree(X)
3. [A] : n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ
4. [B] : n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ
5. [R] : 0-aryRel(X)
6. [S] : 0-aryRel(X)
7. tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s));q)
8. [[R]] 0 (λx.⊥)
⊢ tree-secures(X;λm,s. (((A m s) ∨ (B m s)) ∨ (([[R]] m s) ∧ ([[S]] m s)));q)
BY
{ TACTIC:(Using [`A', ⌜λm,s. ((B m s) ∨ ([[S]] m s))⌝] (BLemma `tree-secures_functionality`)⋅ THEN Reduce 0 THEN Auto) }
1
1. X : Type
2. q : wfd-tree(X)
3. [A] : n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ
4. [B] : n:ℕ ⟶ (ℕn ⟶ X) ⟶ ℙ
5. [R] : 0-aryRel(X)
6. [S] : 0-aryRel(X)
7. tree-secures(X;λm,s. ((B m s) ∨ ([[S]] m s));q)
8. [[R]] 0 (λx.⊥)
9. n : ℕ
10. s : ℕn ⟶ X
11. (B n s) ∨ ([[S]] n s)
⊢ ((A n s) ∨ (B n s)) ∨ (([[R]] n s) ∧ ([[S]] n s))
Latex:
Latex:
1. X : Type
2. q : wfd-tree(X)
3. [A] : n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} X) {}\mrightarrow{} \mBbbP{}
4. [B] : n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} X) {}\mrightarrow{} \mBbbP{}
5. [R] : 0-aryRel(X)
6. [S] : 0-aryRel(X)
7. tree-secures(X;\mlambda{}m,s. ((B m s) \mvee{} ([[S]] m s));q)
8. [[R]] 0 (\mlambda{}x.\mbot{})
\mvdash{} tree-secures(X;\mlambda{}m,s. (((A m s) \mvee{} (B m s)) \mvee{} (([[R]] m s) \mwedge{} ([[S]] m s)));q)
By
Latex:
TACTIC:(Using [`A', \mkleeneopen{}\mlambda{}m,s. ((B m s) \mvee{} ([[S]] m s))\mkleeneclose{}] (BLemma `tree-secures\_functionality`)\mcdot{}
THEN Reduce 0
THEN Auto)
Home
Index