---

Step * of Lemma FOLRule-induction-ext

∀[P:FOLRule() ⟶ ℙ]
  (P[andI]
  ⇒ P[impI]
  ⇒ (∀var:ℤ. P[allI with var])
  ⇒ (∀var:ℤ. P[existsI with var])
  ⇒ (∀left:𝔹. P[fRuleorI(left)])
  ⇒ P[hyp]
  ⇒ (∀hypnum:ℕ. P[andE on hypnum])
  ⇒ (∀hypnum:ℕ. P[orE on hypnum])
  ⇒ (∀hypnum:ℕ. P[impE on hypnum])
  ⇒ (∀hypnum:ℕ. ∀var:ℤ.  P[allE on hypnum with var])
  ⇒ (∀hypnum:ℕ. ∀var:ℤ.  P[existsE on hypnum with var])
  ⇒ (∀hypnum:ℕ. P[falseE on hypnum])
  ⇒ {∀v:FOLRule(). P[v]})
BY
{ ((Unfold `guard` 0 THEN Intro)
   THEN UseWitness ⌜λandI,impI,allI,exI,orI,hh,andE,orE,impE,allE,exE,falseE,v. let lbl,v1 = v 
                                                                                in if lbl="andI" then andI
                                                                                   if lbl="impI" then impI
                                                                                   if lbl="allI" then allI v1
                                                                                   if lbl="existsI" then exI v1
                                                                                   if lbl="orI" then orI v1
                                                                                   if lbl="orI" then Ax
                                                                                   if lbl="hyp" then hh
                                                                                   if lbl="andE" then andE v1
                                                                                   if lbl="orE" then orE v1
                                                                                   if lbl="impE" then impE v1
                                                                                   if lbl="allE"
                                                                                     then allE (fst(v1)) (snd(v1))
                                                                                   if lbl="existsE"
                                                                                     then exE (fst(v1)) (snd(v1))
                                                                                   else falseE v1
                                                                                   fi ⌝⋅
   THEN RepeatFor 13 ((MemCD THENL [Id; Auto]))
   THEN D -1
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P:FOLRule()  {}\mrightarrow{}  \mBbbP{}]
    (P[andI]
    {}\mRightarrow{}  P[impI]
    {}\mRightarrow{}  (\mforall{}var:\mBbbZ{}.  P[allI  with  var])
    {}\mRightarrow{}  (\mforall{}var:\mBbbZ{}.  P[existsI  with  var])
    {}\mRightarrow{}  (\mforall{}left:\mBbbB{}.  P[fRuleorI(left)])
    {}\mRightarrow{}  P[hyp]
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  P[andE  on  hypnum])
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  P[orE  on  hypnum])
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  P[impE  on  hypnum])
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  \mforall{}var:\mBbbZ{}.    P[allE  on  hypnum  with  var])
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  \mforall{}var:\mBbbZ{}.    P[existsE  on  hypnum  with  var])
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  P[falseE  on  hypnum])
    {}\mRightarrow{}  \{\mforall{}v:FOLRule().  P[v]\})


By

---

Latex:
((Unfold  `guard`  0  THEN  Intro)
  THEN  UseWitness  \mkleeneopen{}\mlambda{}andI,impI,allI,exI,orI,hh,andE,orE,impE,allE,exE,falseE,v.  let  lbl,v1  =  v 
                                                                                                                                                            in  if  lbl="andI"
                                                                                                                                                                      then  andI
                                                                                                                                                                  if  lbl="impI"
                                                                                                                                                                      then  impI
                                                                                                                                                                  if  lbl="allI"
                                                                                                                                                                      then  allI  v1
                                                                                                                                                                  if  lbl="existsI"
                                                                                                                                                                      then  exI  v1
                                                                                                                                                                  if  lbl="orI"
                                                                                                                                                                      then  orI  v1
                                                                                                                                                                  if  lbl="orI"
                                                                                                                                                                      then  Ax
                                                                                                                                                                  if  lbl="hyp"
                                                                                                                                                                      then  hh
                                                                                                                                                                  if  lbl="andE"
                                                                                                                                                                      then  andE  v1
                                                                                                                                                                  if  lbl="orE"
                                                                                                                                                                      then  orE  v1
                                                                                                                                                                  if  lbl="impE"
                                                                                                                                                                      then  impE  v1
                                                                                                                                                                  if  lbl="allE"
                                                                                                                                                                      then  allE 
                                                                                                                                                                                (fst(v1)) 
                                                                                                                                                                                (snd(v1))
                                                                                                                                                                  if  lbl="existsE"
                                                                                                                                                                      then  exE 
                                                                                                                                                                                (fst(v1)) 
                                                                                                                                                                                (snd(v1))
                                                                                                                                                                  else  falseE  v1
                                                                                                                                                                  fi  \mkleeneclose{}\mcdot{}
  THEN  RepeatFor  13  ((MemCD  THENL  [Id;  Auto]))
  THEN  D  -1
  THEN  Reduce  0
  THEN  Auto)

---

Home Index