# proofs involving epsilon

```Hi,

I am writing the CSP theory in PVS (from Camilleri's work using HOL). I
have used the epsilon operator to define CSP's choice operator. But I am
not able to do any proofs involving the epsilon operator. I have looked at
John Rushby's reply to Darryl Dieckman's question in the archive. Though
choose is defined in terms of epsilon, a similar involving "typepred" does
not seem to work. I have attached the dump-file for the theory to this
mail. Can somebody please give me some pointers regarding how to do the
proof? I appreciate your help. Thanks. Bye.

PS: An example of a theorem involving the epsilon operator is
"well_def_alpha_th1". I am stuck with "member(e!1, epsilon(pred_fun(a!1,
f)))" in the consequent.

--
Best Wishes,
-- Murali
***************************************************************************
Murali Rangarajan # rmurali@ececs.uc.edu # http://www.ececs.uc.edu/~rmurali
Knowledge Based Software Engineering Lab # Phone(Work): (785) 864 7759

"Try not. Do. Or do not. There is no try."  -- Yoda, Jedi Master
***************************************************************************
```
```
\$\$\$Choice.pvs
%%-----------------------------------------------------------------------------
%% Copyright (c) 1996 Ohio Board of Regents and the University of
%%
%% UC MAKES NO REPRESENTATIONS OR WARRANTIES ABOUT THE SUITABILITY OF
%% THE SOFTWARE, EITHER EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED
%% TO THE IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A
%% PARTICULAR PURPOSE, OR NON-INFRINGEMENT.  UC SHALL NOT BE LIABLE
%% FOR ANY DAMAGES SUFFERED BY LICENSEE AS A RESULT OF USING,
%% RESULT OF USING, MODIFYING OR DISTRIBUTING THIS SOFTWARE OR ITS
%% DERIVATIVES.
%%
%% By using or copying this Software, Licensee agrees to abide by the
%% intellectual property laws, and all other applicable laws of the
%% U.S., and the terms of this license.
%%
%% author: Murali Rangarajan
%% rmurali@ececs.uc.edu
%%
%% Revision Information:
%% \$Id: Choice.pvs,v 1.4 2000/05/21 16:46:53 rmurali Exp \$
%%
%% Description:
%% This theory defines the CSP choice operator.  Camilleri used a higher-order
%% function to do this. This theory tries to mimic it. This can be combined
%% with the CSP theory, but it is seperated here to facilitate better
%% understanding.
%%-----------------------------------------------------------------------------

Choice [event : TYPE+] : THEORY
BEGIN

IMPORTING CSPBasics[event], functions[event, process]

% This function returns the predicate to be used with "choice" operator.
% The definition is the same as that of well_def_alpha.

pred_fun(a:alphabet, f:[event -> process]) : pred[alphabet] =
EXISTS (a1 : alphabet): (FORALL (x: event):
member(x,a) => alpha(f(x)) = a1) AND subset?(a, a1)

%        LAMBDA EXISTS (a1 : alphabet): (FORALL (x: event):
%            member(x,a) => alpha(f(x)) = a1) AND subset?(a, a1)

% ---------Operator definitions from Choice---------

well_def_alpha(a:alphabet, f: [event -> process]) : bool =
EXISTS (a1 : alphabet): (FORALL (x: event):
member(x,a) => alpha(f(x)) = a1) AND subset?(a, a1)

% choice chooses an event from the alphabet randomly, and returns the
% process obtained by applying the function f to that chosen event.
choice(a: alphabet, f: [event -> process]): process

% ---------Variable declarations for use in theorems and axioms---------

e, x: VAR event
a, new_a: VAR alphabet
a1: VAR alphabet
f: [event -> process]
p: process
t: VAR trace

% ---------Definition of the choice operator---------

% Defines the choice operator
choice_ax1 : AXIOM
well_def_alpha(a,f) =>
(alpha(choice(a,f)) = epsilon(pred_fun(a,f))) AND
(traces(choice(a,f)) = {t | t = null or
(member(car(t), a) and member(cdr(t), traces(f(car(t)))))})

% When the predicate well_def_alpha holds for some function f and
% alphabet a, the above representation of the choice operator is
% well defined
choice_ax2 : AXIOM
well_def_alpha(a,f) => process_rep(choice(a,f))

% ---------Theorems from Choice---------

well_def_alpha_th1 : THEOREM
(well_def_alpha(a,f) AND member(e,a)) =>
member(e, alpha(choice(a,f)))

well_def_alpha_th2 : THEOREM
(well_def_alpha(a,f) AND member(e,a) => process_rep(f(e)))
=> process_rep(choice(a,f))

well_def_alpha_th3 : THEOREM
(well_def_alpha(a,f) and member(e,a)) =>
(alpha(choice(a,f)) = alpha(f(e)))

END Choice

\$\$\$Choice.prf
(|Choice| (|choice_ax1_TCC1| "" (SUBTYPE-TCC) NIL NIL)
(|choice_ax1_TCC2| "" (SUBTYPE-TCC) NIL NIL)
(|well_def_alpha_th1| "" (SKOSIMP*)
(("" (LEMMA "choice_ax1")
(("" (INST -1 "a!1")
(("" (ASSERT)
(("" (EXPAND "well_def_alpha")
(("" (SKOSIMP*)
(("" (INST -3 "e!1")
(("" (ASSERT)
(("" (REPLACE -1 1) (("" (POSTPONE) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))

\$\$\$CSPBasics.pvs

%%-------------------------------------------------------------------------
%% Conversion of Albert J. Camilleri's HOL axiomatization of CSP into LSL.
%% Albert John Camilleri,"Mechanizing CSP Trace Theory in HOL"
%% IEEE Transactions on Software Engineering,16(9):993-1004, September 1990
%%-------------------------------------------------------------------------

CSPBasics [event : TYPE+] : THEORY
BEGIN

% ---------Type definitions from CSPAssumptions---------

alphabet : TYPE = set[event]
trace : TYPE = list[event]
trace_set : TYPE = set[trace]
nonempty_trace : TYPE = {t: trace | length(t) > 0}

% ---------Type Definitions from CSPBasics---------

process : TYPE = [# alpha: alphabet, traces: trace_set #]

% Needed by the parallel operator. Added by rmurali.
process_set : TYPE = set[process]

% ---------General Operator Definitions---------

precat(e: event, t: trace) : trace =
cons(e, t)

% Proofs involving postcat are getting really complex. So, I am
% commenting them out until I findout I need them.
%postcat(t:trace, e: event) : trace = append(t, cons(e, null))

% ---------CSP Operator Definitions from CSPBasics---------

%% Define restriction of a trace to a set of events.
restrict(t:trace, a:alphabet): RECURSIVE trace =
IF t = null
THEN null
ELSE IF member(car(t),a)
THEN cons(car(t),restrict(cdr(t),a))
ELSE restrict(cdr(t),a)
ENDIF
ENDIF
MEASURE length(t)

%% Define set of all possible traces of events in an alphabet.
star(a:alphabet) : trace_set = { t:trace | restrict(t,a) = t }

% 	%% Define when a process tuple actually represents a process.
% 	process_rep(p: process) : bool =
% 		subset?(traces(p),star(alpha(p))) AND
% 		member(null,traces(p)) AND
% 		(FORALL (s1,s2:trace): member(append(s1,s2),traces(p)) =>
% 				member(s1,traces(p)))

%% Define when a process tuple actually represents a process.
process_rep(p: process) : bool =
(FORALL (s1,s2:trace): member(append(s1,s2),traces(p)) =>
member(s1,traces(p)))

% ---------Variable declarations for use in theorems and axioms---------

e, e1, e2: VAR event
s, t: VAR trace
a: VAR alphabet
p, q: VAR process

% ---------Axioms-------------------------------------------------------

process_ax1: AXIOM member(null, traces(p))

% All the events in all the traces of a process have to be from the
% alphabet of the process
process_ax2: AXIOM
member(e,t) and member(t, traces(p)) => member(e, alpha(p))

% Supplimentary axiom to define valid traces of a process
process_ax3: AXIOM member(t, traces(p)) => (restrict(t, alpha(p)) = t)

% This property (of lists in general, actually) should be easy to
% prove, but it is not so in reality. So, I have added it as an axiom.
trace_ax01 : AXIOM
(cons(e1, s) = cons(e2, t)) => ((e1 = e2) and (s = t))

% alternative definition for star
star_defn_ax : AXIOM
star(a) = {t | member(e,t) => member(e,a)}

% ---------Theorems from CSPAssumptions---------
% In this trait, || represents concatenation operator on lists.
% None of the theorems in the implies section is reflected here as
% they are all standard properties of sets and sequences.

% ---------Theorems from CSPBasics---------

member_th0 : THEOREM
member(t, star(a)) AND member(e,a) => member(cons(e,t), star(a))

member_th02 : THEOREM
member(e,a) AND member(cons(e,t),star(a)) => member(t, star(a))

member_th1 : THEOREM
member(e,restrict(t,a)) => member(e,a)

% This theorem, in conjunction with theorem member_restrict_th22, is
% needed for proving member_th2.
% The new proof for member_th2 no longer needs these. It uses the
% alternate definition for star to arrive at a simple solution.
member_restrict_th21: THEOREM
(restrict(s,a) = t) => (member(e,t) => member(e,a))

% The following two theorems are needed for proving the theorem
% member_restrict_th22.
length_restrict_th221: THEOREM
length(restrict(s,a)) <= length(s)

length_trace_th222: THEOREM
(s = t) => (length(s) = length(t))

member_restrict_th22: THEOREM
(restrict(cons(e,s), a) = cons(e,s)) => member(e,a)

% The proof for this theorem uses the alternate definition for star
% given as an axiom.
member_th2 : THEOREM
member(e,t) AND member(t,star(a)) => member(e,a)

% Prove that everything in the traces of a process is also in the
% alphabet of the process.
% This theorem uses the new axiom "process_ax2"
member_th3 : THEOREM
member(t,traces(p)) AND member(e,t)
=> member(e,alpha(p))

% Prove something in the restriction of a trace will also be in the
% restriction of that trace precatted with something else.
member_th4 : THEOREM
member(e1,restrict(t,a))
=> member(e1,restrict(cons(e2,t),a))

% Prove something in a trace that is in some alphabet will also be in
% the trace that results from restricting the trace to the alphabet.
member_th5 : THEOREM
member(e,t) AND member(e,a) => member(e,restrict(t,a))

length_trace_th61: THEOREM
length(restrict(s,a)) < length(cons(e,s))

% Prove if the restriction of a trace equals the trace, everything
% in the trace must by in the alphabet.
member_th6 : THEOREM
(restrict(t,a)=t)	=> (member(e,t)	=> member(e,a))

% Prove if the restriction of a trace does not equal the trace, there
% must be something in the trace that is not in the alphabet.
member_th7 : THEOREM
NOT (restrict(t,a)=t) => (EXISTS (e3 : event) :
(member(e3,t) AND NOT member(e3,a)))

%% Prove restriction applies to right half of concatenated trace.
restrict_th1 : THEOREM
( restrict(append(s,t),a) = append(s,t) )
=> ( restrict(t,a) = t)

%% Prove restriction applies to left half of concatenated trace.
restrict_th2 : THEOREM
restrict(append(s,t),a) = append(s,t)
=> restrict(s,a) = s

reverse_null_th3111: THEOREM reverse[trace](null) = null

reverse_cons_th3112: THEOREM reverse(cons(e,null)) /= null

reverse_th3113: THEOREM (t /= null) => (reverse(t) /= null)

reverse_cons_th3114: THEOREM reverse(cons(e,t)) /= null

% Proofs involving postcat and reverse are getting really complicated.
% So, I am commenting them out now, and will do the proofs
% if I find out that I need to use the operators.

%     cons_reverse_th311: THEOREM
%         cons(e1, reverse(cons(e2, reverse(t)))) =
%             reverse(cons(e2, reverse(cons(e1, t))))

%     % The original definition of postcat. It was complicated to prove it
%     % using reverse. Therefore, changed the definition and added the
%     % old definition as theorem.
%     postcat_th31: THEOREM postcat(t, e) = reverse(cons(e, reverse(t)))

% 	%% Prove law similar to law that defines restriction.  This fact just
% 	%% uses postcat as the generator.
% 	restrict_th3 : THEOREM
% 		restrict(postcat(t,e),a) =
% 			IF member(e,a)
% 				THEN	postcat(restrict(t,a),e)
% 				ELSE  restrict(t,a)
% 			ENDIF

%% Prove restriction distributes through concatenation.
restrict_th4 : THEOREM
restrict(append(s,t),a) = append(restrict(s,a),restrict(t,a))

%% This and the definition of process_rep implies the following fact
%% which is needed in one of the CSP proofs.
mem_rest_th1 : THEOREM
( member(restrict(append(s,t),alpha(p)),traces(p))
AND process_rep(p) ) =>
member(restrict(s,alpha(p)),traces(p))

restrict_th51: THEOREM
(restrict(cons(e,t), a) = cons(e,t)) =>
(member(e, a) and (restrict(t,a) = t))

restrict_th52: THEOREM
(member(e,a) and (restrict(t,a) = t)) =>
(restrict(cons(e,t), a) = cons(e,t))

%% Prove how restriction interacts with car and cdr.
restrict_th5 : THEOREM
( (restrict(cons(e,t), a) = cons(e,t)) <=>
(member(car(cons(e,t)), a) AND
(restrict(cdr(cons(e,t)),a) = cdr(cons(e,t)))))

% A different of the axiom process_ax02 needed to prove the
% theorem restrict_th6
process_th61: THEOREM member(t, traces(p)) =>
(member(e,t) => member(e, alpha(p)))

%     restrict_th62: THEOREM (member(e,t) => member(e, a)) =>
%                               (restrict(t, a) = t)

member_cons_th631: THEOREM member(e, cons(e,t))

% Restrict from processes
restrict_th6: THEOREM
(member(e, alpha(p)) and member(t, traces(p))) =>
(restrict(cons(e, t), alpha(p)) = cons(e,t))

% This will simplify the process_rep function definition.
process_th01: THEOREM
subset?(traces(p), star(alpha(p)))

END CSPBasics

\$\$\$CSPBasics.prf
(|CSPBasics| (|restrict_TCC1| "" (SUBTYPE-TCC) NIL NIL)
(|restrict_TCC2| "" (TERMINATION-TCC) NIL NIL)
(|restrict_TCC3| "" (TERMINATION-TCC) NIL NIL)
(|member_th0| "" (SKOSIMP *)
(("" (EXPAND "member")
(("" (EXPAND "star")
(("" (ASSERT)
(("" (EXPAND "restrict" 1)
(("" (LIFT-IF)
(("" (ASSERT)
(("" (EXPAND "member" 1) (("" (PROPAX) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|member_th02| "" (SKOSIMP *)
(("" (EXPAND "member")
(("" (EXPAND "star")
(("" (EXPAND "restrict" -2)
(("" (EXPAND "member" -2)
(("" (ASSERT)
(("" (LEMMA "trace_ax01")
(("" (INST -1 "e!1" "e!1" "restrict(t!1, a!1)" "t!1")
(("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|member_th1| "" (INDUCT "t")
(("1" (SKOSIMP*)
(("1" (EXPAND "restrict")
(("1" (EXPAND "member") (("1" (PROPAX) NIL NIL)) NIL)) NIL))
NIL)
("2" (SKOSIMP *)
(("2" (SKOSIMP *)
(("2" (EXPAND "restrict" -2)
(("2" (ASSERT)
(("2" (INST -1 "a!1" "e!1")
(("2" (CASE "member(cons1_var!1, a!1)")
(("1" (ASSERT)
(("1" (EXPAND "member" -2) (("1" (PROPAX) NIL NIL))
NIL))
NIL)
("2" (ASSERT) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|member_restrict_th21| "" (INDUCT "s")
(("1" (SKOSIMP*) (("1" (ASSERT) (("1" (GRIND) NIL NIL)) NIL)) NIL)
("2" (SKOSIMP*)
(("2" (INST -1 "a!1" "e!1" "t!1")
(("2" (EXPAND "restrict" -2)
(("2" (LIFT-IF)
(("2" (CASE "member(cons1_var!1, a!1)")
(("1" (ASSERT)
(("1" (REPLACE -2 -3 RL)
(("1" (EXPAND "member" -3)
(("1" (LEMMA "member_th1")
(("1" (INST -1 "a!1" "e!1" "cons2_var!1")
(("1" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
("2" (ASSERT) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|length_restrict_th221| "" (INDUCT "s")
(("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
("2" (SKOSIMP*)
(("2" (INST -1 "a!1")
(("2" (EXPAND "restrict" 1)
(("2" (ASSERT)
(("2" (CASE "member(cons1_var!1, a!1)")
(("1" (ASSERT)
(("1" (EXPAND "length" 1) (("1" (ASSERT) NIL NIL)) NIL))
NIL)
("2" (ASSERT)
(("2" (EXPAND "length" 2)
(("2" (ASSERT)
(("2" (EXPAND "length" -1)
(("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|length_trace_th222| "" (SKOSIMP*) (("" (GRIND) NIL NIL)) NIL)
(|member_restrict_th22| "" (INDUCT "s")
(("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
("2" (SKOSIMP*)
(("2" (INST -1 "a!1" "e!1")
(("2" (EXPAND "restrict" -2)
(("2" (LIFT-IF)
(("2" (ASSERT 1)
(("2" (DO-REWRITE)
(("2" (GRIND)
(("1" (LEMMA "trace_ax01")
(("1"
(INST -1 "cons1_var!1" "e!1"
" restrict(cons2_var!1, a!1)"
"cons(cons1_var!1, cons2_var!1)")
(("1" (ASSERT) NIL NIL)) NIL))
NIL)
("2" (LEMMA "length_trace_th222")
(("2"
(INST -1 "restrict(cons2_var!1, a!1)"
"cons(e!1, cons(cons1_var!1, cons2_var!1))")
(("2" (ASSERT)
(("2" (LEMMA "length_restrict_th221")
(("2" (INST -1 "a!1" "cons2_var!1")
(("2" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|member_th2| "" (SKOSIMP*)
(("" (LEMMA "star_defn_ax")
(("" (INST -1 "a!1" "e!1")
(("" (REPLACE -1) (("" (ASSERT) (("" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|member_th3| "" (SKOSIMP*)
(("" (ASSERT)
(("" (LEMMA "process_ax2")
(("" (INST -1 "e!1" "p!1" "t!1") (("" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL)
(|member_th4| "" (INDUCT "t")
(("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
("2" (SKOSIMP*) (("2" (INST?) (("2" (GRIND) NIL NIL)) NIL)) NIL))
NIL)
(|member_th5| "" (INDUCT "t")
(("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
("2" (SKOSIMP*) (("2" (INST?) (("2" (GRIND) NIL NIL)) NIL)) NIL))
NIL)
(|length_trace_th61| "" (SKOSIMP*)
(("" (EXPAND "length")
(("" (ASSERT)
(("" (GRIND)
(("" (LEMMA "length_restrict_th221")
(("" (INST?) (("" (GRIND) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|member_th6| "" (INDUCT "t")
(("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
("2" (SKOSIMP*)
(("2" (INST?)
(("2" (EXPAND "member" -3)
(("2" (SPLIT)
(("1" (PROPAX) NIL NIL)
("2" (ASSERT)
(("2" (REPLACE -2 * RL)
(("2" (EXPAND "restrict" -1)
(("2" (LEMMA "length_trace_th222")
(("2"
(INST -1 "restrict(cons2_var!1, a!1)"
"cons(e!1, cons2_var!1)")
(("2" (LEMMA "length_trace_th61")
(("2" (INST?)
(("2" (INST -1 "e!1") (("2" (GRIND) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("3" (GRIND)
(("1" (LEMMA "length_trace_th222")
(("1"
(INST -1 "restrict(cons2_var!1, a!1)"
"cons(cons1_var!1, cons2_var!1)")
(("1" (ASSERT)
(("1" (LEMMA "length_restrict_th221")
(("1" (INST -1 "a!1" "cons2_var!1")
(("1" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
("2" (GRIND)
(("2" (LEMMA "trace_ax01")
(("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
NIL)
("3" (LEMMA "length_trace_th222")
(("3"
(INST -1 "restrict(cons2_var!1, a!1)"
"cons(cons1_var!1, cons2_var!1)")
(("3" (ASSERT)
(("3" (LEMMA "length_restrict_th221")
(("3" (INST -1 "a!1" "cons2_var!1")
(("3" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|member_th7| "" (INDUCT "t")
(("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
("2" (SKOSIMP*)
(("2" (INST -1 "a!1")
(("2" (ASSERT)
(("2" (EXPAND "restrict" 1)
(("2" (SPLIT)
(("1" (SKOSIMP*)
(("1" (INST 3 "e3!1")
(("1" (EXPAND "member" 3)
(("1" (ASSERT)
(("1" (EXPAND "member" 1) (("1" (PROPAX) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
("2" (CASE "member(cons1_var!1, a!1)")
(("1" (ASSERT) NIL NIL)
("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|restrict_th1| "" (INDUCT "s")
(("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
("2" (SKOSIMP*)
(("2" (INST -1 "a!1" "t!1")
(("2" (SPLIT)
(("1" (PROPAX) NIL NIL)
("2" (EXPAND "append" -1)
(("2" (EXPAND "restrict" -1)
(("2" (ASSERT)
(("2" (CASE "member(cons1_var!1, a!1)")
(("1" (ASSERT)
(("1" (LEMMA "trace_ax01")
(("1"
(INST -1 "cons1_var!1" "cons1_var!1"
"restrict(append(cons2_var!1, t!1), a!1)"
"append(cons2_var!1, t!1)")
(("1" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
("2" (ASSERT)
(("2" (LEMMA "length_trace_th222")
(("2"
(INST -1
"restrict(append(cons2_var!1, t!1), a!1)"
"cons(cons1_var!1, append(cons2_var!1, t!1))")
(("2" (LEMMA "length_restrict_th221")
(("2"
(INST -1 "a!1" "append(cons2_var!1, t!1)")
(("2" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|restrict_th2| "" (INDUCT "s")
(("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
("2" (SKOSIMP*)
(("2" (INST -1 "a!1" "t!1")
(("2" (ASSERT)
(("2" (EXPAND "append" -2)
(("2" (EXPAND "restrict" -2)
(("2" (CASE "member(cons1_var!1, a!1)")
(("1" (ASSERT)
(("1" (LEMMA "trace_ax01")
(("1"
(INST -1 "cons1_var!1" "cons1_var!1"
" restrict(append(cons2_var!1, t!1), a!1)"
" append(cons2_var!1, t!1)")
(("1" (ASSERT)
(("1" (EXPAND "restrict" 1)
(("1" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
("2" (ASSERT)
(("2" (LEMMA "length_trace_th222")
(("2"
(INST -1 "restrict(append(cons2_var!1, t!1), a!1)"
"cons(cons1_var!1, append(cons2_var!1, t!1))")
(("2" (LEMMA "length_restrict_th221")
(("2" (INST -1 "a!1" "append(cons2_var!1, t!1)")
(("2" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|reverse_null_th3111| "" (EXPAND "reverse") (("" (PROPAX) NIL NIL))
NIL)
(|reverse_cons_th3112| "" (SKOSIMP*)
(("" (LEMMA "length_trace_th222")
(("" (INST -1 "reverse(cons(e!1, null))" "null")
(("" (GRIND) NIL NIL)) NIL))
NIL))
NIL)
(|reverse_th3113| "" (SKOSIMP*)
(("" (LEMMA "length_reverse" ("l" "t!1")) (("" (GRIND) NIL NIL))
NIL))
NIL)
(|reverse_cons_th3114| "" (INDUCT "t")
(("1" (SKOSIMP*)
(("1" (LEMMA "reverse_cons_th3112")
(("1" (INST -1 "e!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL))
NIL)
("2" (SKOSIMP*)
(("2" (INST -1 "cons1_var!1")
(("2" (EXPAND "reverse" -2)
(("2" (EXPAND "append") (("2" (ASSERT) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL)
(|restrict_th4| "" (INDUCT "s")
(("1" (SKOSIMP*)
(("1" (EXPAND "append")
(("1" (EXPAND "restrict") (("1" (PROPAX) NIL NIL)) NIL)) NIL))
NIL)
("2" (SKOSIMP*)
(("2" (INST -1 "a!1" "t!1")
(("2" (EXPAND "append" 1)
(("2" (EXPAND "restrict" 1)
(("2" (ASSERT)
(("2" (LIFT-IF)
(("2" (LIFT-IF) (("2" (GRIND) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|mem_rest_th1| "" (SKOSIMP*)
(("" (EXPAND "process_rep")
(("" (ASSERT)
(("" (LEMMA "restrict_th4")
(("" (INST -1 "alpha(p!1)" "s!1" "t!1")
(("" (REPLACE -1 -2)
(("" (ASSERT)
((""
(INST -3 "restrict(s!1, alpha(p!1))"
"restrict(t!1, alpha(p!1))")
(("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|restrict_th51| "" (INDUCT "t")
(("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
("2" (SKOSIMP*)
(("2" (INST -1 "a!1" "e!1")
(("2" (EXPAND "restrict" -2)
(("2" (CASE "member(e!1, a!1)")
(("1" (ASSERT)
(("1" (LEMMA "trace_ax01")
(("1"
(INST -1 "e!1" "e!1"
"restrict(cons(cons1_var!1, cons2_var!1), a!1)"
"cons(cons1_var!1, cons2_var!1)")
(("1" (ASSERT) NIL NIL)) NIL))
NIL))
NIL)
("2" (ASSERT)
(("2" (LEMMA "length_trace_th222")
(("2"
(INST -1
"restrict(cons(cons1_var!1, cons2_var!1), a!1)"
"cons(e!1, cons(cons1_var!1, cons2_var!1))")
(("2" (LEMMA "length_restrict_th221")
(("2"
(INST -1 "a!1" "cons(cons1_var!1, cons2_var!1)")
(("2" (GRIND) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|restrict_th52| "" (INDUCT "t")
(("1" (SKOSIMP*) (("1" (GRIND) NIL NIL)) NIL)
("2" (SKOSIMP*)
(("2" (INST -1 "a!1" "e!1")
(("2" (ASSERT)
(("2" (EXPAND "restrict" 1)
(("2" (REPLACE -3 1) (("2" (PROPAX) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|restrict_th5| "" (SKOSIMP*)
(("" (LEMMA "restrict_th51")
(("" (INST -1 "a!1" "e!1" "t!1")
(("" (LEMMA "restrict_th52")
(("" (INST -1 "a!1" "e!1" "t!1")
(("" (ASSERT) (("" (GRIND) NIL NIL)) NIL)) NIL))
NIL))
NIL))
NIL))
NIL)
(|process_th61| "" (SKOSIMP*)
(("" (LEMMA "process_ax2")
(("" (INST -1 "e!1" "p!1" "t!1") (("" (GRIND) NIL NIL)) NIL)) NIL))
NIL)
(|restrict_th62| "" (INDUCT "t")
(("1" (POSTPONE) NIL NIL)
("2" (SKOSIMP*)
(("2" (EXPAND "restrict" 1)
(("2" (INST -1 "a!1" "e!1")
(("2" (LIFT-IF)
(("2" (SIMPLIFY)
(("2" (SPLIT)
(("1" (SPLIT)
(("1" (PROP)
(("1" (REPLACE -3 1) (("1" (PROPAX) NIL NIL)) NIL)
("2" (POSTPONE) NIL NIL))
NIL)
("2" (POSTPONE) NIL NIL))
NIL)
("2" (POSTPONE) NIL NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|member_cons_th631| "" (SKOSIMP*)
(("" (ASSERT) (("" (EXPAND "member") (("" (PROPAX) NIL NIL)) NIL))
NIL))
NIL)
(|restrict_th6| "" (SKOSIMP*)
(("" (LEMMA "process_ax2")
(("" (INST -1 "e!1" "p!1" "t!1")
(("" (EXPAND "restrict")
(("" (ASSERT)
(("" (GRIND)
(("" (LEMMA "process_ax3")
(("" (INST -1 "p!1" "t!1") (("" (ASSERT) NIL NIL)) NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL))
NIL)
(|process_th01| "" (SKOSIMP*)
(("" (EXPAND "star")
(("" (LEMMA "process_ax3")
(("" (INST -1 "p!1" "_") (("" (GRIND) NIL NIL)) NIL)) NIL))
NIL))
NIL))

```