POPL Tutorial/Properties of Typing and Reduction

This problem (or problems) involves proving three properties of typing and reduction for the language L{num str} from Bob Harper’s book, [http://www.cs.cmu.edu/~rwh/plbook/book.pdf Practical Foundations for Programming Languages].

The System L{num str}

% Natural numbers
%sort nat %.
%term 0 nat %.
%term s %pi nat %-> nat %.
% Addition for natural numbers
%sort plus_op {_ nat} {_ nat} {_ nat} %.
%term plus_op/0 plus_op 0 N N %.
%term plus_op/s %pi (plus_op N M L) %-> (plus_op (s N) M (s L)) %.
% Multiplication for natural numbers
%sort times_op {_ nat} {_ nat} {_ nat} %.
%term times_op/0 times_op 0 N 0 %.
%term times_op/s %pi (times_op (s N) M P) %<- (times_op N M L) %<- (plus_op L M P) %.
%%%%%%%%%%%%%%%% L{num str}: Syntax %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Types
%sort typ %.
%term num typ %.
%term str typ %.
% Expressions.  For simplicity, strings are just natural numbers,
% concatenation is addition, and len is the identity.
%sort exp %.
%term nume %pi nat %-> exp %.
%term stre %pi nat %-> exp %.
%term plus %pi exp %-> exp %-> exp %.
%term times %pi exp %-> exp %-> exp %.
%term cat %pi exp %-> exp %-> exp %.
%term len %pi exp %-> exp %.
%term let %pi exp %-> (%pi exp %-> exp) %-> exp %.
%%%%%%%%%%%%%%%% L{num str}: Static semantics (typing judgment) %%%%%%%%%%%%%%%
%sort of {_ exp} {_ typ} %.
%term of/stre of (stre S) str %.
%term of/nume of (nume N) num %.
%term of/plus %pi (of E1 num) %-> (of E2 num) %-> (of (plus E1 E2) num) %.
%term of/times %pi (of E1 num) %-> (of E2 num) %-> (of (times E1 E2) num) %.
%term of/cat %pi (of E1 str) %-> (of E2 str) %-> (of (cat E1 E2) str) %.
%term of/len %pi (of E1 str) %-> (of (len E1) num) %.
%term of/let
  %pi (of E1 T1)
  %-> ({x} %pi (of x T1) %-> (of (E2 x) T2))
  %-> (of (let E1 ([x] E2 x)) T2) %.
% Assumption block for typing judgment (coming from of/let)
%block of_bind [T typ] {x exp} {ofx of x T}%.
%%%%%%%%%%%%%%%% L{num str}: Dynamic Semantics %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Values
%sort val {_ exp} %.
%term val/stre val (stre N) %.
%term val/nume val (nume N) %.
% Reduction
%sort red {_ exp} {_ exp} %.
%term red/plus/num %pi (plus_op N1 N2 N) %-> (red (plus (nume N1) (nume N2)) (nume N)) %.
%term red/plus1 %pi (red E1 E1') %-> (red (plus E1 E2) (plus E1' E2)) %.
%term red/plus2 %pi (val E1) %-> (red E2 E2') %-> (red (plus E1 E2) (plus E1 E2')) %.
%term red/times/num %pi (times_op N1 N2 N) %-> (red (times (nume N1) (nume N2)) (nume N)) %.
%term red/times1 %pi (red E1 E1') %-> (red (times E1 E2) (times E1' E2)) %.
%term red/times2 %pi (val E1) %-> (red E2 E2') %-> (red (times E1 E2) (times E1 E2')) %.
%term red/cat/str %pi (plus_op S1 S2 S) %-> (red (cat (stre S1) (stre S2)) (stre S)) %.
%term red/cat1 %pi (red E1 E1') %-> (red (cat E1 E2) (cat E1' E2)) %.
%term red/cat2 %pi (val E1) %-> (red E2 E2') %-> (red (cat E1 E2) (cat E1 E2')) %.
%term red/len/str red (len (stre S)) (nume S) %.
%term red/len %pi (red E1 E1') %-> (red (len E1) (len E1')) %.
%term red/let/val %pi (val E1) %-> (red (let E1 ([x] E2 x)) (E2 E1)) %.
%term red/let %pi (red E1 E1') %-> (red (let E1 ([x] E2 x)) (let E1' ([x] E2 x))) %.

Problem 1: Unicity of Typing

%%%%%%%%%%%%%%%% Lemma 9.1 (Unicity of typing) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% If G |- E : T1 and G |- E : T2, then T1 = T2.
% Equality of types
%sort eqtyp {_ typ} {_ typ} %.
%term refl_t eqtyp T T %.
% Congruence for typing assumptions.  Although the proof doesn't
% introduce any parameters or hypotheses, it is used by a theorem that
% does, and so we need to check it in the extended worlds.
%sort cong_of {_ eqtyp A1 A2} {_ {x} %pi (of x A1) %-> (of (E x) T)} {_ {x} %pi (of x A2) %-> (of (E x) T)} %.
%mode cong_of %in %in %out %.
%term _ cong_of refl_t OE1 OE1 %.
%worlds (of_bind) (cong_of _ _ _) %.
%total OE1 (cong_of _ OE1 _) %.
% Statement and proof of Lemma.  Notice that the worlds in this proof
% are an extension (technically, they subsume) the worlds in the
% congruence lemma above.
%sort lemma9-1 {_ of E T1} {_ of E T2} {_ eqtyp T1 T2} %.
%mode lemma9-1 %in %in %out %.
%term _ lemma9-1 of/stre of/stre refl_t %.
%term _ lemma9-1 of/nume of/nume refl_t %.
%term _ lemma9-1 (of/plus OjE11 OjE12) (of/plus OjE21 OjE22) refl_t %.
%term _ lemma9-1 (of/times OjE11 OjE12) (of/times OjE21 OjE22) refl_t %.
%term _ lemma9-1 (of/cat OjE11 OjE12) (of/cat OjE21 OjE22) refl_t %.
%term _ lemma9-1 (of/len OjE1) (of/len OjE2) refl_t %.
%term _
  %pi (lemma9-1 (of/let OjE11 ([x] [ofx1] OjE12 x ofx1)) (of/let OjE21 ([x] [ofx2] OjE22 x ofx2)) Q)
  %<- (lemma9-1 OjE11 OjE21 E1)
  %<- (cong_of E1 OjE12 OjE12')
  %<- ({x} {ofx2} %pi (lemma9-1 ofx2 ofx2 refl_t) %-> (lemma9-1 (OjE12' x ofx2) (OjE22 x ofx2) Q)) %.
%block lemma_block [T typ] {x exp} {ofx of x T} {u lemma9-1 ofx ofx refl_t}%.
%worlds (lemma_block) (lemma9-1 _ _ _) %.
%total OjT2 (lemma9-1 _ OjT2 _) %.

Problem 2: Determinacy of Reduction

%%%%%%%%%%%%%%%% Lemma 10.1 (Determinacy of Reduction) %%%%%%%%%%%%%%%%%%%%%%%
% If E |-> E' and E |-> E'', then E' = E''.
% Equality and congruence for nats
%sort eqnat {_ nat} {_ nat} %.
%term refl_n eqnat N N %.
%sort cong_s {_ eqnat N M} {_ eqnat (s N) (s M)} %.
%mode cong_s %in %out %.
%term _ cong_s refl_n refl_n %.
%worlds () (cong_s _ _) %.
%total {} (cong_s _ _) %.
% Equality for expressions
%sort eqexp {_ exp} {_ exp} %.
%term refl_e eqexp E E %.
% Congruences for expressions
%sort cong_nume {_ eqnat N1 N2} {_ eqexp (nume N1) (nume N2)} %.
%mode cong_nume %in %out %.
%term _ cong_nume refl_n refl_e %.
%worlds () (cong_nume _ _) %.
%total E (cong_nume E _) %.
%sort cong_stre {_ eqnat S1 S2} {_ eqexp (stre S1) (stre S2)} %.
%mode cong_stre %in %out %.
%term _ cong_stre refl_n refl_e %.
%worlds () (cong_stre _ _) %.
%total E (cong_stre E _) %.
%sort cong_plus1 {_ eqexp E1 E2} {_ eqexp (plus E1 F) (plus E2 F)} %.
%mode {%in E1 exp} {%in E2 exp} {%in F exp} {%in E eqexp E1 E2} {%out E' eqexp (plus E1 F) (plus E2 F)} cong_plus1 E E' %.
%term _ cong_plus1 refl_e refl_e %.
%worlds () (cong_plus1 _ _) %.
%total E (cong_plus1 E _) %.
%sort cong_plus2 {_ eqexp F1 F2} {_ eqexp (plus E F1) (plus E F2)} %.
%mode {%in F1 exp} {%in F2 exp} {%in E exp} {%in E1 eqexp F1 F2} {%out E' eqexp (plus E F1) (plus E F2)} cong_plus2 E1 E' %.
%term _ cong_plus2 refl_e refl_e %.
%worlds () (cong_plus2 _ _) %.
%total E (cong_plus2 E _) %.
%sort cong_times1 {_ eqexp E1 E2} {_ eqexp (times E1 F) (times E2 F)} %.
%mode {%in E1 exp} {%in E2 exp} {%in F exp} {%in E eqexp E1 E2} {%out E' eqexp (times E1 F) (times E2 F)} cong_times1 E E' %.
%term _ cong_times1 refl_e refl_e %.
%worlds () (cong_times1 _ _) %.
%total E (cong_times1 E _) %.
%sort cong_times2 {_ eqexp F1 F2} {_ eqexp (times E F1) (times E F2)} %.
%mode {%in F1 exp} {%in F2 exp} {%in E exp} {%in E2 eqexp F1 F2} {%out E' eqexp (times E F1) (times E F2)} cong_times2 E2 E' %.
%term _ cong_times2 refl_e refl_e %.
%worlds () (cong_times2 _ _) %.
%total E (cong_times2 E _) %.
%sort cong_cat1 {_ eqexp E1 E2} {_ eqexp (cat E1 F) (cat E2 F)} %.
%mode {%in E1 exp} {%in E2 exp} {%in F exp} {%in E eqexp E1 E2} {%out E' eqexp (cat E1 F) (cat E2 F)} cong_cat1 E E' %.
%term _ cong_cat1 refl_e refl_e %.
%worlds () (cong_cat1 _ _) %.
%total E (cong_cat1 E _) %.
%sort cong_cat2 {_ eqexp F1 F2} {_ eqexp (cat E F1) (cat E F2)} %.
%mode {%in F1 exp} {%in F2 exp} {%in E exp} {%in E3 eqexp F1 F2} {%out E' eqexp (cat E F1) (cat E F2)} cong_cat2 E3 E' %.
%term _ cong_cat2 refl_e refl_e %.
%worlds () (cong_cat2 _ _) %.
%total E (cong_cat2 E _) %.
%sort cong_len {_ eqexp E1 E2} {_ eqexp (len E1) (len E2)} %.
%mode cong_len %in %out %.
%term _ cong_len refl_e refl_e %.
%worlds () (cong_len _ _) %.
%total E (cong_len E _) %.
%sort cong_let {_ eqexp E1 E2} {_ eqexp (let E1 F) (let E2 F)} %.
%mode {%in E1 exp} {%in E2 exp} {%in F %pi exp %-> exp} {%in E eqexp E1 E2} {%out E' eqexp (let E1 ([x exp] F x)) (let E2 ([x exp] F x))} cong_let E E' %.
%term _ cong_let refl_e refl_e %.
%worlds () (cong_let _ _) %.
%total E (cong_let E _) %.
% Uniqueness of plus
%sort plus! {_ plus_op N M L1} {_ plus_op N M L2} {_ eqnat L1 L2} %.
%mode plus! %in %in %out %.
%term _ plus! plus_op/0 plus_op/0 refl_n %.
%term _
  %pi (plus! (plus_op/s Pj1) (plus_op/s Pj2) ES)
  %<- (plus! Pj1 Pj2 EL)
  %<- (cong_s EL ES) %.
%worlds () (plus! _ _ _) %.
%total Pj1 (plus! Pj1 _ _) %.
% Congruence of plus
%sort plus_cong {_ eqnat N1 N2} {_ plus_op N1 M L1} {_ plus_op N2 M L2} {_ eqnat L1 L2} %.
%mode plus_cong %in %in %in %out %.
%term _ plus_cong refl_n plus_op/0 plus_op/0 refl_n %.
%term _
  %pi (plus_cong refl_n (plus_op/s Pj1) (plus_op/s Pj2) ES)
  %<- (plus_cong refl_n Pj1 Pj2 EL)
  %<- (cong_s EL ES) %.
%worlds () (plus_cong _ _ _ _) %.
%total PjL (plus_cong _ PjL _ _) %.
% Uniqueness of times
%sort times! {_ times_op N M L1} {_ times_op N M L2} {_ eqnat L1 L2} %.
%mode times! %in %in %out %.
%term _ times! times_op/0 times_op/0 refl_n %.
%term _
  %pi (times! (times_op/s Pj1 Tj1) (times_op/s Pj2 Tj2) ES)
  %<- (times! Tj1 Tj2 EL)
  %<- (plus_cong EL Pj1 Pj2 ES) %.
%worlds () (times! _ _ _) %.
%total Tj1 (times! Tj1 _ _) %.
% Proof of Lemma 10.1
%sort lemma10-1 {_ red E E1} {_ red E E2} {_ eqexp E1 E2} %.
%mode lemma10-1 %in %in %out %.
%term _
  %pi (lemma10-1 (red/plus/num PjN1) (red/plus/num PjN2) EE')
  %<- (plus! PjN1 PjN2 EL)
  %<- (cong_nume EL EE') %.
%term _
  %pi (lemma10-1 (red/plus1 RjE1) (red/plus1 RjE2) EE')
  %<- (lemma10-1 RjE1 RjE2 EE)
  %<- (cong_plus1 EE EE') %.
%term _
  %pi (lemma10-1 (red/plus2 _ RjF1) (red/plus2 _ RjF2) EE')
  %<- (lemma10-1 RjF1 RjF2 EF)
  %<- (cong_plus2 EF EE') %.
%term _
  %pi (lemma10-1 (red/times/num TjN1) (red/times/num TjN2) EE')
  %<- (times! TjN1 TjN2 EE)
  %<- (cong_nume EE EE') %.
%term _
  %pi (lemma10-1 (red/times1 RjE1) (red/times1 RjE2) EE')
  %<- (lemma10-1 RjE1 RjE2 EE)
  %<- (cong_times1 EE EE') %.
%term _
  %pi (lemma10-1 (red/times2 _ RjF1) (red/times2 _ RjF2) EE')
  %<- (lemma10-1 RjF1 RjF2 EF)
  %<- (cong_times2 EF EE') %.
%term _
  %pi (lemma10-1 (red/cat/str PjN1) (red/cat/str PjN2) EE')
  %<- (plus! PjN1 PjN2 EE)
  %<- (cong_stre EE EE') %.
%term _
  %pi (lemma10-1 (red/cat1 RjE1) (red/cat1 RjE2) EE')
  %<- (lemma10-1 RjE1 RjE2 EE)
  %<- (cong_cat1 EE EE') %.
%term _
  %pi (lemma10-1 (red/cat2 _ RjF1) (red/cat2 _ RjF2) EE')
  %<- (lemma10-1 RjF1 RjF2 EF)
  %<- (cong_cat2 EF EE') %.
%term _
  %pi (lemma10-1 (%the (red (len (stre S)) (nume S)) red/len/str) red/len/str EE')
  %<- (cong_nume refl_n EE') %.
%term _
  %pi (lemma10-1 (red/len RjE1) (red/len RjE2) EE')
  %<- (lemma10-1 RjE1 RjE2 EE)
  %<- (cong_len EE EE') %.
%term _ lemma10-1 (red/let/val VjE11) (red/let/val VjE12) refl_e %.
%term _
  %pi (lemma10-1 (red/let RjE1) (red/let RjE2) EE')
  %<- (lemma10-1 RjE1 RjE2 EE)
  %<- (cong_let EE EE') %.
%worlds () (lemma10-1 _ _ _) %.
%total RjE (lemma10-1 RjE _ _) %.

Problem 3: Contextual Semantics

In this problem, we define the contextual semantics for L{num str} and proof that it is equivalent to (defines the same relation as) the given dynamic semantics (reduction).

%%%%%%%%%%%%%%%% L{num str}: Contextual Semantics %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Instructions:  E0 ~> E0'
%sort instr {_ exp} {_ exp} %.
%term instr/plus %pi (plus_op N1 N2 N) %-> (instr (plus (nume N1) (nume N2)) (nume N)) %.
%term instr/times %pi (times_op N1 N2 N) %-> (instr (times (nume N1) (nume N2)) (nume N)) %.
%term instr/cat %pi (plus_op S1 S2 S) %-> (instr (cat (stre S1) (stre S2)) (stre S)) %.
%term instr/len instr (len (stre S)) (nume S) %.
%term instr/let %pi (val E1) %-> (instr (let E1 ([x] E2 x)) (E2 E1)) %.
% Expression contexts, represented as "expressions with holes", i.e.,
% functions on expressions.
%sort ectxt {_ %pi exp %-> exp} %.
%term ectxt/hole ectxt ([x] x) %.
%term ectxt/plus1 %pi (ectxt ([x] C1 x)) %-> (ectxt ([x] plus (C1 x) E2)) %.
%term ectxt/plus2 %pi (val E1) %-> (ectxt ([x] C2 x)) %-> (ectxt ([x] plus E1 (C2 x))) %.
%term ectxt/times1 %pi (ectxt ([x] C1 x)) %-> (ectxt ([x] times (C1 x) E2)) %.
%term ectxt/times2 %pi (val E1) %-> (ectxt ([x] C2 x)) %-> (ectxt ([x] times E1 (C2 x))) %.
%term ectxt/cat1 %pi (ectxt ([x] C1 x)) %-> (ectxt ([x] cat (C1 x) E2)) %.
%term ectxt/cat2 %pi (val E1) %-> (ectxt ([x] C2 x)) %-> (ectxt ([x] cat E1 (C2 x))) %.
%term ectxt/len %pi (ectxt ([x] C x)) %-> (ectxt ([x] len (C x))) %.
%term ectxt/let %pi (ectxt ([x] C1 x)) %-> (ectxt ([x] let (C1 x) ([y] E2 y))) %.
% Filling the hole of an expression context with an expression
%sort fill {_ ectxt ([x] C x)} {_ exp} {_ exp} %.
%term fill/hole fill ectxt/hole E E %.
%term fill/plus1
  %pi (fill ECC1 E C1@E)
  %-> (fill (%the (ectxt ([x] plus (C1 x) E2)) (ectxt/plus1 ECC1)) E (plus C1@E E2)) %.
%term fill/plus2 {VjE1 val E1} %pi (fill ECC2 E C2@E) %-> (fill (ectxt/plus2 VjE1 ECC2) E (plus E1 C2@E)) %.
%term fill/times1
  %pi (fill ECC1 E C1@E)
  %-> (fill (%the (ectxt ([x] times (C1 x) E2)) (ectxt/times1 ECC1)) E (times C1@E E2)) %.
%term fill/times2 {VjE1 val E1} %pi (fill ECC2 E C2@E) %-> (fill (ectxt/times2 VjE1 ECC2) E (times E1 C2@E)) %.
%term fill/cat1
  %pi (fill ECC1 E C1@E)
  %-> (fill (%the (ectxt ([x] cat (C1 x) E2)) (ectxt/cat1 ECC1)) E (cat C1@E E2)) %.
%term fill/cat2 {VjE1 val E1} %pi (fill ECC2 E C2@E) %-> (fill (ectxt/cat2 VjE1 ECC2) E (cat E1 C2@E)) %.
%term fill/len %pi (fill ECC1 E C1@E) %-> (fill (ectxt/len ECC1) E (len C1@E)) %.
%term fill/let
  %pi (fill ECC1 E C1@E)
  %-> (fill (%the (ectxt ([x] let (C1 x) ([y] E2 y))) (ectxt/let ECC1)) E (let C1@E ([y] E2 y))) %.
% Contextual reduction rule
%sort cred {_ exp} {_ exp} %.
%term cred/step
  %pi (fill EC E0 C@E0)
  %-> (instr E0 E0')
  %-> (fill EC E0' C@E0')
  %-> (cred C@E0 C@E0') %.
%%%%%%%%%%%%%%%% Theorem 10.2.1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% If E |-> E', then E |->c E'.
%sort thm10-2-1 {_ red E E'} {_ cred E E'} %.
%mode thm10-2-1 %in %out %.
%term _ thm10-2-1 (red/plus/num PjN) (cred/step fill/hole (instr/plus PjN) fill/hole) %.
%term _
  %pi (thm10-2-1 (red/plus1 RjE1) (cred/step (fill/plus1 FjC1@E0) I (fill/plus1 FjC1@E0')))
  %<- (thm10-2-1 RjE1 (cred/step FjC1@E0 I FjC1@E0')) %.
%term _
  %pi (thm10-2-1 (red/plus2 VjE1 RjE2) (cred/step (fill/plus2 VjE1 FjC2@E0) I (fill/plus2 VjE1 FjC2@E0')))
  %<- (thm10-2-1 RjE2 (cred/step FjC2@E0 I FjC2@E0')) %.
%term _ thm10-2-1 (red/times/num TjN) (cred/step fill/hole (instr/times TjN) fill/hole) %.
%term _
  %pi (thm10-2-1 (red/times1 RjE1) (cred/step (fill/times1 FjC1@E0) I (fill/times1 FjC1@E0')))
  %<- (thm10-2-1 RjE1 (cred/step FjC1@E0 I FjC1@E0')) %.
%term _
  %pi (thm10-2-1 (red/times2 VjE1 RjE2) (cred/step (fill/times2 VjE1 FjC2@E0) I (fill/times2 VjE1 FjC2@E0')))
  %<- (thm10-2-1 RjE2 (cred/step FjC2@E0 I FjC2@E0')) %.
%term _ thm10-2-1 (red/cat/str PjN) (cred/step fill/hole (instr/cat PjN) fill/hole) %.
%term _
  %pi (thm10-2-1 (red/cat1 RjE1) (cred/step (fill/cat1 FjC1@E0) I (fill/cat1 FjC1@E0')))
  %<- (thm10-2-1 RjE1 (cred/step FjC1@E0 I FjC1@E0')) %.
%term _
  %pi (thm10-2-1 (red/cat2 VjE1 RjE2) (cred/step (fill/cat2 VjE1 FjC2@E0) I (fill/cat2 VjE1 FjC2@E0')))
  %<- (thm10-2-1 RjE2 (cred/step FjC2@E0 I FjC2@E0')) %.
%term _ thm10-2-1 red/len/str (cred/step fill/hole instr/len fill/hole) %.
%term _
  %pi (thm10-2-1 (red/len RjE1) (cred/step (fill/len FjC1@E0) I (fill/len FjC1@E0')))
  %<- (thm10-2-1 RjE1 (cred/step FjC1@E0 I FjC1@E0')) %.
%term _ thm10-2-1 (red/let/val VjE1) (cred/step fill/hole (instr/let VjE1) fill/hole) %.
%term _
  %pi (thm10-2-1 (red/let RjE1) (cred/step (fill/let FjC1@E0) I (fill/let FjC1@E0')))
  %<- (thm10-2-1 RjE1 (cred/step FjC1@E0 I FjC1@E0')) %.
%worlds () (thm10-2-1 _ _) %.
%total RjE (thm10-2-1 RjE _) %.
%%%%%%%%%%%%%%%% Theorem 10.2.2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% If E |->c E', then E |-> E'.
%sort thm10-2-2 {_ cred E E'} {_ red E E'} %.
%mode thm10-2-2 %in %out %.
% Lemma.  If C{E0} = E, E0 ~> E0', and C{E0'} = E', then E |-> E'.
%sort lem10-2-2 {_ fill EC E0 E} {_ instr E0 E0'} {_ fill EC E0' E'} {_ red E E'} %.
%mode lem10-2-2 %in %in %in %out %.
%term _ lem10-2-2 fill/hole (instr/plus PjN) fill/hole (red/plus/num PjN) %.
%term _ lem10-2-2 fill/hole (instr/times TjN) fill/hole (red/times/num TjN) %.
%term _ lem10-2-2 fill/hole (instr/cat PjN) fill/hole (red/cat/str PjN) %.
%term _ lem10-2-2 fill/hole instr/len fill/hole red/len/str %.
%term _ lem10-2-2 fill/hole (instr/let VjE1) fill/hole (red/let/val VjE1) %.
%term _
  %pi (lem10-2-2 (fill/plus1 FjC1@E0) I (fill/plus1 FjC1@E0') (red/plus1 RjE))
  %<- (lem10-2-2 FjC1@E0 I FjC1@E0' RjE) %.
%term _
  %pi (lem10-2-2 (fill/plus2 VjE1 FjC2@E0) I (fill/plus2 VjE1 FjC2@E0') (red/plus2 VjE1 RjE))
  %<- (lem10-2-2 FjC2@E0 I FjC2@E0' RjE) %.
%term _
  %pi (lem10-2-2 (fill/times1 FjC1@E0) I (fill/times1 FjC1@E0') (red/times1 RjE))
  %<- (lem10-2-2 FjC1@E0 I FjC1@E0' RjE) %.
%term _
  %pi (lem10-2-2 (fill/times2 VjE1 FjC2@E0) I (fill/times2 VjE1 FjC2@E0') (red/times2 VjE1 RjE))
  %<- (lem10-2-2 FjC2@E0 I FjC2@E0' RjE) %.
%term _
  %pi (lem10-2-2 (fill/cat1 FjC1@E0) I (fill/cat1 FjC1@E0') (red/cat1 RjE))
  %<- (lem10-2-2 FjC1@E0 I FjC1@E0' RjE) %.
%term _
  %pi (lem10-2-2 (fill/cat2 VjE1 FjC2@E0) I (fill/cat2 VjE1 FjC2@E0') (red/cat2 VjE1 RjE))
  %<- (lem10-2-2 FjC2@E0 I FjC2@E0' RjE) %.
%term _
  %pi (lem10-2-2 (fill/len FjC1@E0) I (fill/len FjC1@E0') (red/len RjE))
  %<- (lem10-2-2 FjC1@E0 I FjC1@E0' RjE) %.
%term _
  %pi (lem10-2-2 (fill/let FjC2@E0) I (fill/let FjC2@E0') (red/let RjE))
  %<- (lem10-2-2 FjC2@E0 I FjC2@E0' RjE) %.
%worlds () (lem10-2-2 _ _ _ _) %.
%total FjE (lem10-2-2 FjE _ _ _) %.
% Proof of main theorem
%term _
  %pi (thm10-2-2 (cred/step FjC@E0 I FjC@E0') RjE)
  %<- (lem10-2-2 FjC@E0 I FjC@E0' RjE) %.
%worlds () (thm10-2-2 _ _) %.
%total {} (thm10-2-2 _ _) %.

STELF Output

The check="true">output for the above.