---

Step * of Lemma maybe_new_var-distinct

No Annotations
∀[a:varname()]. ∀[vs:varname() List].  (∀v∈vs.¬(maybe_new_var(a;vs) = v ∈ varname()))
BY
{ ((Auto THEN (Assert a ∈ Base BY (D 1 THEN Reduce 0 THEN Auto)))
   THEN BLemma `l_all_iff`
   THEN Auto
   THEN Unfold `maybe_new_var` 0
   THEN AutoSplit
   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. v : varname()
6. (v ∈ vs)
7. t : Atom
8. if a is an atom then a otherwise fst(a) = t ∈ Atom
9. i : ℤ
10. v2 : {b:varname()| var-num(t;b) = i ∈ ℤ} 
11. (v2 ∈ vs)
12. var-num(t;v2) = i ∈ ℤ
13. (∀y∈vs.var-num(t;y) ≤ i)
⊢ ¬(if i <z 0 then a else <t, i> fi  = v ∈ varname())

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  (Assert  a  \mmember{}  Base  BY  (D  1  THEN  Reduce  0  THEN  Auto)))
  THEN  BLemma  `l\_all\_iff`
  THEN  Auto
  THEN  Unfold  `maybe\_new\_var`  0
  THEN  AutoSplit
  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