---

Step * of Lemma maybe_new_var-is-null

No Annotations
∀a:varname(). ∀[vs:varname() List]. a = nullvar() ∈ varname() supposing maybe_new_var(a;vs) = nullvar() ∈ varname()
BY
{ (Auto
   THEN Unfold `maybe_new_var` -1
   THEN (SplitOnHypITE -1  THENA Auto)
   THEN Try (Trivial)
   THEN (Assert a ∈ Base BY
               (D 1 THEN Reduce 0 THEN Auto))
   THEN MoveToConcl (-3)
   THEN (GenConcl ⌜if a is an atom then a otherwise fst(a) = t ∈ Atom⌝⋅
         THENA (D 1 THEN Try (D 1) THEN Reduce 0 THEN Auto)
         )
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (InstLemma `list-max-property` [⌜varname()⌝;⌜λ2b.var-num(t;b)⌝;⌜vs⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜list-max(b.var-num(t;b);vs)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN Reduce 0
   THEN Auto) }

1
1. a : varname()
2. vs : varname() List
3. ¬(vs = [] ∈ (varname() List))
4. a ∈ Base
5. t : Atom
6. if a is an atom then a otherwise fst(a) = t ∈ Atom
7. i : ℤ
8. v1 : {b:varname()| var-num(t;b) = i ∈ ℤ} 
9. (v1 ∈ vs)
10. var-num(t;v1) = i ∈ ℤ
11. (∀y∈vs.var-num(t;y) ≤ i)
12. if i <z 0 then a else <t, i> fi  = nullvar() ∈ varname()
⊢ a = nullvar() ∈ varname()

---

Latex:

---

Latex:
No  Annotations
\mforall{}a:varname().  \mforall{}[vs:varname()  List].  a  =  nullvar()  supposing  maybe\_new\_var(a;vs)  =  nullvar()


By

---

Latex:
(Auto
  THEN  Unfold  `maybe\_new\_var`  -1
  THEN  (SplitOnHypITE  -1    THENA  Auto)
  THEN  Try  (Trivial)
  THEN  (Assert  a  \mmember{}  Base  BY
                          (D  1  THEN  Reduce  0  THEN  Auto))
  THEN  MoveToConcl  (-3)
  THEN  (GenConcl  \mkleeneopen{}if  a  is  an  atom  then  a  otherwise  fst(a)  =  t\mkleeneclose{}\mcdot{}
              THENA  (D  1  THEN  Try  (D  1)  THEN  Reduce  0  THEN  Auto)
              )
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (InstLemma  `list-max-property`  [\mkleeneopen{}varname()\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}b.var-num(t;b)\mkleeneclose{};\mkleeneopen{}vs\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}list-max(b.var-num(t;b);vs)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  Reduce  0
  THEN  Auto)

---

Home Index