[PVS-Help] how to prove this lemma?

```Hi,

Could anyone please show me how to prove the lemma "counterlemma" in the
attached theory "standard_environments"?

Thanks a lot.

Bin

===========================================================================
standard_environments [ domain: type+
,registerRange: posnat ]
: THEORY

BEGIN

% The number of registers in our model.
registerNumber: type = {y:nat | y <= registerRange}

% Suppose we have 2 counters
counterRange: macro posnat = 1

% The number of counters in our model.
counterNumber: type = {y:nat | y <= counterRange}

% Memory location and register are two datatypes in assembly language.
% Also, in order to evaluate branch upward loops, we introduce
% a datatype "counter". The datatype "term" consists of the three elements.
term: DATATYPE
BEGIN
m(n:int): memory?
r(n:registerNumber): register?
counter(n:counterNumber): loopCounter?
END term

% Datatype "register" is injective. A widely used lemma in the proofs later.
r_injective: sublemma
FORALL (m,n:registerNumber): (r(m)=r(n)) = (m=n);

% Datatype "memory" is injective.
m_injective: sublemma
FORALL (s,t:int): (m(s)=m(t)) = (s=t);

% Counter and register are different types.
counter_register: sublemma
FORALL (n:counterNumber, m:registerNumber): counter(n) /= r(m);

% The environment of the assembly language.
env: TYPE = [ term -> domain]

% Types: memory location, register, loop counter.
memory: TYPE = (memory?);
register: TYPE = (register?);
loopCounter: TYPE = (loopCounter?);

counterlemma: lemma
FORALL (ctr:loopCounter): ctr=counter(0) or ctr=counter(1);

END standard_environments

```
```
%% PVS Version 3.1
%% 6.2 [Linux (x86)] (Feb 14, 2003 18:46)
\$\$\$PVSHOME/.pvs.lisp
(defun make-accessor-funtype (domain range deps)
(if deps
(let* ((tdom (typecheck* (copy domain) nil nil nil))
(dtype (if (dep-binding? tdom)
tdom
(mk-dep-binding (make-new-variable 'd
(list tdom range))
tdom)))
(dep-name (make-variable-expr dtype))
(*bound-variables* (cons dtype *bound-variables*))
(subst-range (substit range
(if (dep-binding? domain)
(pairlis
(cons domain (mapcar #'declaration deps))
(cons dtype
(mapcar #'(lambda (dep)
(typecheck* (mk-application (id dep)
dep-name)
(type dep) nil nil))
deps)))
(pairlis
(mapcar #'declaration deps)
(mapcar #'(lambda (dep)
(typecheck* (mk-application (id dep)
dep-name)
(type dep) nil nil))
deps))))))
(mk-funtype dtype subst-range))
(mk-funtype domain range)))

(defmethod substit-binding (expr alist)
(let* ((newtype (substit* (type expr) alist))
(newdtype (if (tc-eq (print-type (type expr))
(declared-type expr))
(if (eq (print-type (type expr)) (print-type newtype))
(declared-type expr)
(print-type newtype))
(substit* (declared-type expr) alist))))
(lcopy expr
'type newtype
'declared-type newdtype)))

(defmethod pp* ((ass assignment))
(with-slots (arguments expression) ass
(pprint-logical-block (nil nil)
(pprint-indent :current 2)
(if (and (typep ass 'uni-assignment)
(simple-name? (caar arguments)))
(pp* (caar arguments))
(pp-arguments* arguments))
(write-char #\space)
(pprint-newline :fill)
(write ":=")
(write-char #\space)
(pp* expression))))

\$\$\$standard_environments.pvs
% Introduce a standard environment of assembly languages. "Term" consists of "memory
% location", "register" and "counter". Data type "counter" is used to count the loops
% in branch upward structures.

standard_environments [ domain: type+
,registerRange: posnat ]
: THEORY

BEGIN

% The number of registers in our model.
registerNumber: type = {y:nat | y <= registerRange}

% Suppose we have 2 counters
counterRange: macro posnat = 1

% The number of counters in our model.
counterNumber: type = {y:nat | y <= counterRange}

% Memory location and register are two datatypes in assembly language.
% Also, in order to evaluate branch upward loops, we introduce
% a datatype "counter". The datatype "term" consists of the three elements.
term: DATATYPE
BEGIN
m(n:int): memory?
r(n:registerNumber): register?
counter(n:counterNumber): loopCounter?
END term

% Datatype "register" is injective. A widely used lemma in the proofs later.
r_injective: sublemma
FORALL (m,n:registerNumber): (r(m)=r(n)) = (m=n);

% Datatype "memory" is injective.
m_injective: sublemma
FORALL (s,t:int): (m(s)=m(t)) = (s=t);

% Counter and register are different types.
counter_register: sublemma
FORALL (n:counterNumber, m:registerNumber): counter(n) /= r(m);

% The environment of the assembly language.
env: TYPE = [ term -> domain]

% Types: memory location, register, loop counter.
memory: TYPE = (memory?);
register: TYPE = (register?);
loopCounter: TYPE = (loopCounter?);

counterlemma: lemma
FORALL (ctr:loopCounter): ctr=counter(0) or ctr=counter(1);

END standard_environments

\$\$\$standard_environments.prf
(standard_environments
(term_r_eta_TCC1 0
(term_r_eta_TCC1-1 nil 3284921102 3297206728
("" (skolem * "x")
(("" (typepred "n(x)") (("" (assert) nil nil)) nil)) nil)
proved
{x: int |
IF memory?(d) THEN TRUE
ELSE IF register?(d) THEN x >= 0 AND x <= registerRange
ELSE x >= 0 AND x <= 1
ENDIF
ENDIF}]" standard_environments nil)
(registerRange formal-const-decl "posnat" standard_environments
nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(<= const-decl "bool" reals nil)
(TRUE const-decl "bool" booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
standard_environments nil)
standard_environments nil)
(term type-decl nil standard_environments nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(FALSE const-decl "bool" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
24 10 t shostak))
(term_counter_eta_TCC1 0
(term_counter_eta_TCC1-1 nil 3284921103 3297206728
("" (skolem * "x")
(("" (typepred "n(x)") (("" (assert) nil nil)) nil)) nil)
proved
{x: int |
IF memory?(d) THEN TRUE
ELSE IF register?(d) THEN x >= 0 AND x <= registerRange
ELSE x >= 0 AND x <= 1
ENDIF
ENDIF}]" standard_environments nil)
(registerRange formal-const-decl "posnat" standard_environments
nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(<= const-decl "bool" reals nil)
(TRUE const-decl "bool" booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
standard_environments nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
standard_environments nil)
standard_environments nil)
(term type-decl nil standard_environments nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(FALSE const-decl "bool" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
14 20 t shostak))
(r_injective 0
(r_injective-1 nil 3284921102 3297206873
("" (skolem * ("m1" "n1"))
(("" (iff)
(("" (ground)
(("" (case "n(r(n1))=n1 and n(r(m1))=m1")
(("1" (flatten)
(("1" (name "rn1" "r(n1)")
(("1" (replace -1)
(("1" (hide -1)
(("1" (name "rm1" "r(m1)")
(("1" (replace -1)
(("1" (hide -1) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (rewrite "term_n_r")
(("2" (rewrite "term_n_r") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
proved
standard_environments nil)
(registerNumber type-eq-decl nil standard_environments nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
{x: int |
IF memory?(d) THEN TRUE
ELSE IF register?(d) THEN x >= 0 AND x <= registerRange
ELSE x >= 0 AND x <= 1
ENDIF
ENDIF}]" standard_environments nil)
(registerRange formal-const-decl "posnat" standard_environments
nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
standard_environments nil)
(TRUE const-decl "bool" booleans nil)
standard_environments nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(term type-decl nil standard_environments nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(term_n_r formula-decl nil standard_environments nil))
61573 2170 t nil))
(m_injective 0
(m_injective-1 nil 3284921102 nil
("" (skolem * ("s1" "t1"))
(("" (iff)
(("" (ground)
(("" (case "n(m(t1))=t1 and n(m(s1))=s1")
(("1" (flatten)
(("1" (name "mt1" "m(t1)")
(("1" (replace -1)
(("1" (hide -1)
(("1" (name "ms1" "m(s1)")
(("1" (replace -1)
(("1" (hide -1) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (rewrite "term_n_m")
(("2" (rewrite "term_n_m") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
unfinished nil nil nil nil nil))
(counter_register 0
(counter_register-1 nil 3284921102 nil
("" (skolem!) (("" (grind) nil nil)) nil) unfinished nil nil nil nil
nil))
(counterlemma 0
(counterlemma-1 nil 3297206732 3297207191
("" (skolem * "C")
(("" (typepred "C")
(("" (bddsimp) (("" (ground) (("" (postpone) nil nil)) nil))
nil))
nil))
nil)
unfinished nil 310521 2090 t shostak)))

```