---

Step * 1 1 of Lemma assert-exception-name


1. n : Atom2
2. a1 : Value()
3. ↑(isaxiom(a1?n:x.Ax) ∧b isint(a1?n:x.2))
⊢ False
BY
{ (D 2
   THEN (Subst' a1?n:x.Ax ~ if n=2 n
                             then a1
                             else ⊥ -1
         THENA (Refine_tryReduceValue THEN Try (Fold `has-value` 0) THEN Auto)
         )
   THEN (Subst' a1?n:x.2 ~ if n=2 n
                            then a1
                            else ⊥ -1
         THENA (Refine_tryReduceValue THEN Try (Fold `has-value` 0) THEN Auto)
         )
   THEN (Reduce (-1) THENA Auto)) }

1
1. n : Atom2
2. a1 : Base
3. (a1)↓
4. ↑(isaxiom(a1) ∧b isint(a1))
⊢ False

---

Latex:

---

Latex:

1.  n  :  Atom2
2.  a1  :  Value()
3.  \muparrow{}(isaxiom(a1?n:x.Ax)  \mwedge{}\msubb{}  isint(a1?n:x.2))
\mvdash{}  False


By

---

Latex:
(D  2
  THEN  (Subst'  a1?n:x.Ax  \msim{}  if  n=2  n
                                                      then  a1
                                                      else  \mbot{}  -1
              THENA  (Refine\_tryReduceValue  THEN  Try  (Fold  `has-value`  0)  THEN  Auto)
              )
  THEN  (Subst'  a1?n:x.2  \msim{}  if  n=2  n
                                                    then  a1
                                                    else  \mbot{}  -1
              THENA  (Refine\_tryReduceValue  THEN  Try  (Fold  `has-value`  0)  THEN  Auto)
              )
  THEN  (Reduce  (-1)  THENA  Auto))

---

Home Index