Step
*
1
2
1
1
1
of Lemma
mFOL-proveable-evidence
1. hyps : mFOL() List
2. concl : mFOL()
3. rule : FOLRule()
4. subgoals : mFOL-sequent() List
5. mFOLeffect(<<hyps, concl>, rule>) = (inl subgoals) ∈ (mFOL-sequent() List?)
6. ∀i:ℕ||subgoals||. mFOL-sequent-evidence(subgoals[i])
⊢ mFOL-sequent-evidence(<hyps, concl>)
BY
{ (MoveToConcl 3
THEN InstLemma `FOLRule-induction-ext` [⌜parm{i'}⌝]⋅
THEN (BHyp -1 THENA Auto)
THEN Thin (-1)⋅
THEN Auto
THEN RepUR ``mFOLeffect mFO-dest-connective mFO-dest-quantifier`` (-1)
THEN Try ((MoveToConcl (-1) THEN Progress (Repeat (AutoSplit))⋅ THEN Auto THEN Reduce (-1)))
THEN Try (((Assert mFOL-sequent-evidence(subgoals[0]) BY
Complete (BackThruSomeHyp))
THEN (StrongRevHypSubst (-2) (-1) THENA (Auto THEN HypSubst (-1) 0 THEN Reduce 0 THEN Auto))
THEN Reduce (-1)))
THEN Try (((Assert mFOL-sequent-evidence(subgoals[1]) BY
Complete ((BackThruSomeHyp THEN (Eliminate ⌜subgoals⌝⋅ THENA Auto) THEN Reduce 0 THEN Auto)))
THEN (StrongRevHypSubst (-3) (-1) THENA (Auto THEN HypSubst (-1) 0 THEN Reduce 0 THEN Auto))
THEN Reduce (-1)))) }
1
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. ∀i:ℕ||subgoals||. mFOL-sequent-evidence(subgoals[i])
5. ↑mFOconnect?(concl)
6. mFOconnect-knd(concl) = "and" ∈ Atom
7. [<hyps, mFOconnect-left(concl)>; <hyps, mFOconnect-right(concl)>] = subgoals ∈ (mFOL-sequent() List)
8. mFOL-sequent-evidence(<hyps, mFOconnect-left(concl)>)
9. mFOL-sequent-evidence(<hyps, mFOconnect-right(concl)>)
⊢ mFOL-sequent-evidence(<hyps, concl>)
2
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. ∀i:ℕ||subgoals||. mFOL-sequent-evidence(subgoals[i])
5. ↑mFOconnect?(concl)
6. mFOconnect-knd(concl) = "imp" ∈ Atom
7. [<[mFOconnect-left(concl) / hyps], mFOconnect-right(concl)>] = subgoals ∈ (mFOL-sequent() List)
8. mFOL-sequent-evidence(<[mFOconnect-left(concl) / hyps], mFOconnect-right(concl)>)
⊢ mFOL-sequent-evidence(<hyps, concl>)
3
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. ∀i:ℕ||subgoals||. mFOL-sequent-evidence(subgoals[i])
5. var : ℤ
6. ¬(var ∈ mFOL-sequent-freevars(<hyps, concl>))
7. ↑mFOquant?(concl)
8. mFOquant-isall(concl) = tt
9. [<hyps, mFOquant-body(concl)[var/mFOquant-var(concl)]>] = subgoals ∈ (mFOL-sequent() List)
10. mFOL-sequent-evidence(<hyps, mFOquant-body(concl)[var/mFOquant-var(concl)]>)
⊢ mFOL-sequent-evidence(<hyps, concl>)
4
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. ∀i:ℕ||subgoals||. mFOL-sequent-evidence(subgoals[i])
5. var : ℤ
6. (var ∈ mFOL-sequent-freevars(<hyps, concl>))
7. ↑mFOquant?(concl)
8. mFOquant-isall(concl) = ff
9. [<hyps, mFOquant-body(concl)[var/mFOquant-var(concl)]>] = subgoals ∈ (mFOL-sequent() List)
10. mFOL-sequent-evidence(<hyps, mFOquant-body(concl)[var/mFOquant-var(concl)]>)
⊢ mFOL-sequent-evidence(<hyps, concl>)
5
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. ∀i:ℕ||subgoals||. mFOL-sequent-evidence(subgoals[i])
5. left : 𝔹
6. ↑mFOconnect?(concl)
7. mFOconnect-knd(concl) = "or" ∈ Atom
8. ↑left
9. [<hyps, mFOconnect-left(concl)>] = subgoals ∈ (mFOL-sequent() List)
10. mFOL-sequent-evidence(<hyps, mFOconnect-left(concl)>)
⊢ mFOL-sequent-evidence(<hyps, concl>)
6
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. ∀i:ℕ||subgoals||. mFOL-sequent-evidence(subgoals[i])
5. left : 𝔹
6. ¬↑left
7. ↑mFOconnect?(concl)
8. mFOconnect-knd(concl) = "or" ∈ Atom
9. [<hyps, mFOconnect-right(concl)>] = subgoals ∈ (mFOL-sequent() List)
10. mFOL-sequent-evidence(<hyps, mFOconnect-right(concl)>)
⊢ mFOL-sequent-evidence(<hyps, concl>)
7
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. ∀i:ℕ||subgoals||. mFOL-sequent-evidence(subgoals[i])
5. (concl ∈ hyps)
6. [] = subgoals ∈ (mFOL-sequent() List)
⊢ mFOL-sequent-evidence(<hyps, concl>)
8
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. ∀i:ℕ||subgoals||. mFOL-sequent-evidence(subgoals[i])
5. hypnum : ℕ
6. hypnum < ||hyps||
7. ↑mFOconnect?(hyps[hypnum])
8. mFOconnect-knd(hyps[hypnum]) = "and" ∈ Atom
9. [<[mFOconnect-left(hyps[hypnum]); [mFOconnect-right(hyps[hypnum]) / hyps]], concl>] = subgoals ∈ (mFOL-sequent() List\000C)
10. mFOL-sequent-evidence(<[mFOconnect-left(hyps[hypnum]); [mFOconnect-right(hyps[hypnum]) / hyps]], concl>)
⊢ mFOL-sequent-evidence(<hyps, concl>)
9
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. ∀i:ℕ||subgoals||. mFOL-sequent-evidence(subgoals[i])
5. hypnum : ℕ
6. hypnum < ||hyps||
7. ↑mFOconnect?(hyps[hypnum])
8. mFOconnect-knd(hyps[hypnum]) = "or" ∈ Atom
9. [<[mFOconnect-left(hyps[hypnum]) / hyps], concl>; <[mFOconnect-right(hyps[hypnum]) / hyps], concl>] = subgoals ∈ (mFO\000CL-sequent() List)
10. mFOL-sequent-evidence(<[mFOconnect-left(hyps[hypnum]) / hyps], concl>)
11. mFOL-sequent-evidence(<[mFOconnect-right(hyps[hypnum]) / hyps], concl>)
⊢ mFOL-sequent-evidence(<hyps, concl>)
10
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. ∀i:ℕ||subgoals||. mFOL-sequent-evidence(subgoals[i])
5. hypnum : ℕ
6. hypnum < ||hyps||
7. ↑mFOconnect?(hyps[hypnum])
8. mFOconnect-knd(hyps[hypnum]) = "imp" ∈ Atom
9. [<hyps, mFOconnect-left(hyps[hypnum])>; <[mFOconnect-right(hyps[hypnum]) / hyps], concl>] = subgoals ∈ (mFOL-sequent(\000C) List)
10. mFOL-sequent-evidence(<hyps, mFOconnect-left(hyps[hypnum])>)
11. mFOL-sequent-evidence(<[mFOconnect-right(hyps[hypnum]) / hyps], concl>)
⊢ mFOL-sequent-evidence(<hyps, concl>)
11
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. ∀i:ℕ||subgoals||. mFOL-sequent-evidence(subgoals[i])
5. hypnum : ℕ
6. var : ℤ
7. hypnum < ||hyps||
8. (var ∈ mFOL-sequent-freevars(<hyps, concl>))
9. ↑mFOquant?(hyps[hypnum])
10. mFOquant-isall(hyps[hypnum]) = tt
11. [<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>] = subgoals ∈ (mFOL-sequent() List)
12. mFOL-sequent-evidence(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>)
⊢ mFOL-sequent-evidence(<hyps, concl>)
12
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. ∀i:ℕ||subgoals||. mFOL-sequent-evidence(subgoals[i])
5. hypnum : ℕ
6. var : ℤ
7. ¬(var ∈ mFOL-sequent-freevars(<hyps, concl>))
8. hypnum < ||hyps||
9. ↑mFOquant?(hyps[hypnum])
10. mFOquant-isall(hyps[hypnum]) = ff
11. [<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>] = subgoals ∈ (mFOL-sequent() List)
12. mFOL-sequent-evidence(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>)
⊢ mFOL-sequent-evidence(<hyps, concl>)
13
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. ∀i:ℕ||subgoals||. mFOL-sequent-evidence(subgoals[i])
5. hypnum : ℕ
6. (inr ⋅ ) = (inl subgoals) ∈ (mFOL-sequent() List?)
7. mFOL-sequent-evidence(subgoals[0])
8. mFOL-sequent-evidence(subgoals[1])
⊢ mFOL-sequent-evidence(<hyps, concl>)
Latex:
Latex:
1. hyps : mFOL() List
2. concl : mFOL()
3. rule : FOLRule()
4. subgoals : mFOL-sequent() List
5. mFOLeffect(<<hyps, concl>, rule>) = (inl subgoals)
6. \mforall{}i:\mBbbN{}||subgoals||. mFOL-sequent-evidence(subgoals[i])
\mvdash{} mFOL-sequent-evidence(<hyps, concl>)
By
Latex:
(MoveToConcl 3
THEN InstLemma `FOLRule-induction-ext` [\mkleeneopen{}parm\{i'\}\mkleeneclose{}]\mcdot{}
THEN (BHyp -1 THENA Auto)
THEN Thin (-1)\mcdot{}
THEN Auto
THEN RepUR ``mFOLeffect mFO-dest-connective mFO-dest-quantifier`` (-1)
THEN Try ((MoveToConcl (-1) THEN Progress (Repeat (AutoSplit))\mcdot{} THEN Auto THEN Reduce (-1)))
THEN Try (((Assert mFOL-sequent-evidence(subgoals[0]) BY
Complete (BackThruSomeHyp))
THEN (StrongRevHypSubst (-2) (-1)
THENA (Auto THEN HypSubst (-1) 0 THEN Reduce 0 THEN Auto)
)
THEN Reduce (-1)))
THEN Try (((Assert mFOL-sequent-evidence(subgoals[1]) BY
Complete ((BackThruSomeHyp
THEN (Eliminate \mkleeneopen{}subgoals\mkleeneclose{}\mcdot{} THENA Auto)
THEN Reduce 0
THEN Auto)))
THEN (StrongRevHypSubst (-3) (-1)
THENA (Auto THEN HypSubst (-1) 0 THEN Reduce 0 THEN Auto)
)
THEN Reduce (-1))))
Home
Index