Proof step 13 from proof ex-fits-validrefs (previous step)

User applied rule insert lemma

And obtained the following new goals

• Proof step 1:

  ¬ junkref(str, r, st), fits(r, sks, st) ⊦ ∃ refs. validrefs(str, r ' + refs, st[r -- _type] .type, st) ∧ # refs = # sks ∧ (∀ sks0. sks0 ⊑ sks ∧ sks0 ≠ [] → st[r -- sks0] .refval = (r ' + refs)[# sks0])

• Proof step 12:

  ∃ refs. validrefs(str, r ' + refs, st[r -- _type] .type, st) ∧ # refs = # sks ∧ (∀ sks0. sks0 ⊑ sks ∧ sks0 ≠ [] → st[r -- sks0] .refval = (r ' + refs)[# sks0]), fits(r, sks, st) ⊦ junkref(str, r, st), ∃ refs. validrefs(str, r ' + refs, st[r -- _type] .type, st) ∧ st[r -- sks] .refval = (r ' + refs) .last

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (str, r, st, sks)]]