| DISP | action_set_df | ActionSet{<;i:le>;}(<;T:T:*>;)== ActionSet{<;i>;}(<;T>;)
ActionSet(<;T:T:*>;)== ActionSet(<;T>;) |
| ABS | action_set | ActionSet(T) == car:  (T   car car) |
| THM | action_set_wf |  T:. ActionSet(T)  ' |
| DISP | aset_car_df | <;a:aset:E>;.car== <;a>;.car |
| ABS | aset_car | a.car == a.1 |
| THM | aset_car_wf | T:. a:ActionSet(T). a.car |
| DISP | aset_act_df | <;a:aset:E>;.act== <;a>;.act |
| ABS | aset_act | a.act == a.2 |
| THM | aset_act_wf | T:. a:ActionSet(T). a.act T a.car a.car |
| ML | create_action_set | Class Declaration for: s ActionSet(T)
Long Name: action_set
Short Name: aset
Parameters:
T :
Fields:
([example]) car :
([example]) act : T car car
Universe: ' |
| THM | ex1_of_aset | <; ,  x,y.0>; ActionSet{1}() |
| THM | ex2_of_aset | <;, x,y.x + y>; ActionSet{1}() |
| THM | ex3_of_aset | T,S:. a:T S S. <;S, a>; ActionSet(T) |
| THM | ex4_of_aset | <; , x,y.x * y>; ActionSet{1}() |
| THM | ex5_of_aset | <; List, z,l.(z::l)>; ActionSet{1}() |
| THM | ex6_of_aset | <; List, u,l.rev(l)>; ActionSet{1}(Unit) |
| THM | nat_is_int | n:. n |
| DISP | factorial_df | (<;n:n:*>;)! == (<;n>;)! |
| ML | factorial_ml | (n)! ==r if (n = 0) then 1 else n * (n - 1)! fi |
| THM | factorial_wf | n:. (n)! |
| THM | ex1_of_factorial | (0)! = 1 |
| ABS | multi_action | multi_action(l; s; ASet) ==
Y
(multi_action,l,s,ASet.
if null(l)
then s
else ASet.act hd(rev(l)) (multi_action ASet.act rev(tl(rev(l))) s)
fi )
l
s
ASet |
| DISP | maction_df | (<;S:ActionSet:*>;:<;L:list:*>; <;s:init:*>;)== (<;S>;:<;L>;<;s>;) |
| ML | maction_ml | (S:Ls)==r if null(L) then s else S.act hd(L) (S:tl(L)s) fi |
| THM | maction_wf | Alph:. S:ActionSet(Alph). L:Alph List. s:S.car. (S:Ls) S.car |
| THM | comb_for_maction_wf | (Alph,S,L,s,z.(S:Ls)) Alph:
S:ActionSet(Alph)
L:Alph List
s:S.car
 True
S.car |
| THM | maction_lemma | Alph:. S:ActionSet(Alph). s:S.car. L1,L2,L:Alph List.
(S:L1s) = (S:L2s)   (S:L @ L1s) = (S:L @ L2s) |
| DISP | lpower_df | (<;L:L:*>; <;n:n:*>;)== (<;L>;<;n>;) |
| ML | lpower_ml | (Ln)==r if (n = 0) then [] else (Ln - 1) @ L fi |
| THM | lpower_wf | Alph:. L:Alph List. n:. (Ln) Alph List |
| THM | lpower_alt | Alph:. L:Alph List. n:.
(Ln) = if (n = 0) then [] else L @ (Ln - 1) fi |
| THM | pump_theorem | Alph:. S:ActionSet(Alph). N: . s:S.car.
#(S.car)=N
(A:Alph List
N <; ||A||
( a,b,c:Alph List
(0 <; ||b||  A = (a @ b) @ c)
(k:. (S:(a @ (bk)) @ cs) = (S:As)))) |
| THM | pump_thm_cor | n:. Alph:. S:ActionSet(Alph). s,f:S.car.
#(S.car)=n
(l:Alph List. (S:ls) = f)
(l:Alph List. ||l||  n (S:ls) = f) |
| THM | action_append | T:. S:ActionSet(T). s:S.car. tl1,tl2:T List.
(S:tl1 @ tl2s) = (S:tl1(S:tl2s)) |
| DISP | n0n1_df | n0n1(<;n:n:*>;)== n0n1(<;n>;) |
| ABS | n0n1 | n0n1(n) == (0::[]n) @ (1::[]n) |
| THM | n0n1_wf | n:. n0n1(n) List |
| THM | comb_for_n0n1_wf | (n,z.n0n1(n)) n: True List |
| DISP | el_counter_df | ||<;e:e:*>;:<;L:L:*>;||== ||<;e>;:<;L>;|| |
| ML | el_counter_ml | ||e:L||
==r if null(L) then 0
if (e = hd(L)) then 1 + ||e:tl(L)||
else ||e:tl(L)||
fi |
| THM | el_counter_wf | n:. L: List. ||n:L|| |
| THM | comb_for_el_counter_wf | (n,L,z.||n:L||) n: L: List True |
| THM | counter_of_nil | e:. ||e:[]|| = 0 |
| THM | counter_append | e:. L,M: List. ||e:L @ M|| = ||e:L|| + ||e:M|| |
| THM | counter_lpower | e:. L: List. n:. ||e:(Ln)|| = n * ||e:L|| |
| THM | n0n1_irregular | S:ActionSet(). s,q:S.car.
(n:. #(S.car)=n ) (k:. (S:n0n1(k)s) = q)
(L: List. (S:Ls) = q (k:.  (L = n0n1(k)))) |