src/Fierce.Mvc/wwwroot/content/easyui/insdep/plugin/highlight-9.9.0/test/detect/mizar/default.txt

这里只显示每个文件的开头 60 行。登录后可以解锁完整代码。

微信扫码关注公众号，代码整理好后第一时间通知你。

::: ## Lambda calculus

environ

  vocabularies LAMBDA,
      NUMBERS,
      NAT_1, XBOOLE_0, SUBSET_1, FINSEQ_1, XXREAL_0, CARD_1,
      ARYTM_1, ARYTM_3, TARSKI, RELAT_1, ORDINAL4, FUNCOP_1;

  :: etc...

begin

reserve D for DecoratedTree,
        p,q,r for FinSequence of NAT,
        x for set;

definition
  let D;

  attr D is LambdaTerm-like means
    (dom D qua Tree) is finite &
::>                          *143,306
    for r st r in dom D holds
      r is FinSequence of {0,1} &
      r^<*0*> in dom D implies D.r = 0;
end;

registration
  cluster LambdaTerm-like for DecoratedTree of NAT;
  existence;
::>       *4
end;

definition
  mode LambdaTerm is LambdaTerm-like DecoratedTree of NAT;
end;

::: Then we extend this ordinary one-step beta reduction, that is,
:::  any subterm is also allowed to reduce.
definition
  let M,N;

  pred M beta N means
    ex p st
      M|p beta_shallow N|p &
      for q st not p is_a_prefix_of q holds
        [r,x] in M iff [r,x] in N;
end;

theorem Th4:
  ProperPrefixes (v^<*x*>) = ProperPrefixes v \/ {v}
proof
  thus ProperPrefixes (v^<*x*>) c= ProperPrefixes v \/ {v}
  proof
    let y;
    assume y in ProperPrefixes (v^<*x*>);
    then consider v1 such that
A1: y = v1 and
A2: v1 is_a_proper_prefix_of v^<*x*> by TREES_1:def 2;